colibri_for_bundle.ml

let coldir = Filename.dirname Sys.executable_name

let conf = ref "true"
let memlimit = ref 3000
let interpreter = ref false
let get_steps = ref false
let max_steps = ref 0
let exec_cmd = ref ""

let goal = ref ""

let path_sep = if Sys.win32 then ";" else ":"

let print_version () =
  let cin = open_in (Filename.concat coldir "version") in
  let s = input_line cin in
  close_in cin;
  Printf.printf "%s%!" s;
  exit 0

let add_to_conf s =
  conf := (!conf)^","^s

let argspec =
  ["--version", Arg.Unit print_version, " print version";
   "--memlimit", Arg.Set_int memlimit, " set memlimit in Megabyte (default 3000)";
   "--conf", Arg.String add_to_conf, " evaluate the prolog expression (default true)";
   "--per-call-simplex-timeout",
   Arg.Int (fun sec -> add_to_conf (Printf.sprintf "set_simplex_timeout(%i)" sec)) ,
   " timeout for each call of the rational simplex";
   "--delay-simplex-deactivation",
   Arg.Int (fun sec -> add_to_conf (Printf.sprintf "setval(simplex_delay_deactivation,%i)" sec)),
   " stop delta and simplex algorithm after the given time (0 always activated)";
   "--external-simplex",
   Arg.Symbol (["z3";"z3-debug"],
               (fun s -> Unix.putenv "COLIBRI_USE_SOLVER" s;
                 let path = (try Unix.getenv "PATH" with Not_found -> "") in
                 Unix.putenv "PATH" ((Filename.concat coldir "qf_lra_solver")^path_sep^path)
               )),
   " use the specified external solver \
    (QF_LRA) instead of internal simplex \
    acceptable values are (z3, z3-debug \
    -- prints z3 inputs outputs to \
    /tmp/{input,output}.smt2)";
   "--get-steps", Arg.Set get_steps,
   " output the number of steps at the end";
   "--max-steps", Arg.Set_int max_steps,
   " limit the number of steps";
   "--interpreter-mode", Arg.Set interpreter,
   " run the prolog interactive interpreter";
   "--exec", Arg.Set_string exec_cmd,
   " exec a command in interpreter mode"
  ]

let () = Arg.parse (Arg.align argspec)
    (fun s -> goal := s)
    "colibri <file>"

let () = if !goal = "" then begin
    print_endline "No input file given.";
    exit 1
  end

let eclipsedir = Filename.concat coldir "ECLIPSE"
let eclipselib = Filename.concat eclipsedir "lib"
let colibridir = Filename.concat coldir "COLIBRI"

let arch = if Sys.win32 then "x86_64_nt" else "x86_64_linux"

let () = Unix.putenv "ECLIPSEDIR" eclipsedir
let () = Unix.putenv "FILTER_SMTLIB_FILE" (Filename.concat colibridir "filter_smtlib_file")
let () = Unix.putenv "ARCH" arch

let extend_env var value =
  match Unix.getenv var with
  | exception Not_found -> Unix.putenv var value
  | s -> Unix.putenv var (value^path_sep^s)

let eclipseexe = Filename.concat eclipselib arch

let () =
  if Sys.win32
  then begin
    extend_env "PATH" eclipseexe;
    extend_env "PATH" colibridir;
    extend_env "PATH" (List.fold_left Filename.concat colibridir ["lib";"v7";arch])
  end
  else
    extend_env "LD_LIBRARY_PATH" eclipseexe

let quote_for_prolog f =
  let s = Printf.sprintf "%S" f in
  Printf.sprintf "'%s'" (String.sub s 1 (String.length s - 2))

let () =
    let exe = Filename.concat eclipseexe "eclipse.exe" in
    Unix.execv exe
      (Array.concat
         [
           [| exe;
              "-b"; Filename.concat colibridir "compile_flag";
              "-b"; Filename.concat colibridir "col_solve";
              "-g"; Printf.sprintf "%iM" !memlimit;
           |];
           (if !exec_cmd = ""
            then [| |]
            else [| "-e"; !exec_cmd |])
           ;
           (if !interpreter
            then [| |]
            else [| "-e"; Printf.sprintf
                      "seed(0),%s,smt_solve%s(%s)"
                      !conf
                      (if !get_steps then "_stats" else "")
                      (quote_for_prolog !goal)
                 |])
         ]
      )