Newer
Older
let coldir = Filename.dirname Sys.executable_name
let conf = ref "true"
let default_memlimit = 3000
let memlimit = ref default_memlimit
let interpreter = ref false
let get_steps = ref false
let max_steps = ref 0
let exec_cmd = 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.Int (fun i -> if i <= 0 then memlimit := default_memlimit else memlimit := i)
, " 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)
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 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))
(* Keep space for other stuff a fixed 300M and 10% of given argument *)
let memlimit = (!memlimit - 300) * 9 / 10 in
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