-
Notifications
You must be signed in to change notification settings - Fork 1
/
options.ml
43 lines (32 loc) · 1.21 KB
/
options.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
let usage = "./solver.native file.smt"
let file = ref "_stdin"
let solver_path = ref ""
let solver_option = ref ["--incremental"]
let set_options_solver s =
solver_option := s :: !solver_option
let verbose = ref false
let args = [
"--path-solver", Arg.Set_string solver_path, "Set the path to the solver";
"-ps", Arg.Set_string solver_path, "Alias for -path-solver";
"--op-solver", Arg.String set_options_solver, "Set options for the solver (can be called multiple times)";
"-os", Arg.String set_options_solver, "Alias for -op-solver";
"--verbose", Arg.Set verbose, "be verbose";
"-v", Arg.Set verbose, "be verbose";
]
let alargs = Arg.align args
let cin =
let ofile = ref None in
let set_file s = ofile := Some s in
Arg.parse alargs set_file usage;
match !ofile with
| Some f -> file := f ; open_in f
| None -> stdin
let file = !file
let solver_path =
let sp = match !solver_path with
| "" -> Find_yices.find ()
| p -> p in
Format.sprintf "%s" sp
let solver_command = Printf.sprintf "%s %s" solver_path
(String.concat " " !solver_option)
let verbose = !verbose