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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
open Smtml
open Cmdliner
let fpath =
let open Cmdliner in
let parser = Arg.(conv_parser file) in
Arg.conv
( (fun file ->
if String.equal "-" file then Ok (Fpath.v file)
else
match parser file with
| Ok file -> Ok (Fpath.v file)
| Error _ as err -> err )
, Fpath.pp )
let filename =
let doc = "Input file" in
let docv = "FILE" in
Arg.(required & pos 0 (some fpath) None & info [] ~doc ~docv)
let filenames =
let doc = "Input files" in
let docv = "FILES" in
Arg.(value & pos_all fpath [] & info [] ~docv ~doc)
let solver_type =
let doc =
Fmt.str "Configure which SMT solver to use. Available options are: %a"
(Fmt.list ~sep:Fmt.comma (fun fmt v ->
Fmt.pf fmt "$(b,%a)" Solver_type.pp v ) )
Solver_dispatcher.available
in
Arg.(value & opt Solver_type.conv Z3_solver & info [ "s"; "solver" ] ~doc)
let solver_mode =
let doc = "SMT solver mode" in
Arg.(value & opt Solver_mode.conv Batch & info [ "mode" ] ~doc)
let debug =
let doc = "Print debugging messages" in
Arg.(value & flag & info [ "debug" ] ~doc)
let dry =
let doc = "Dry run on tests" in
Arg.(value & flag & info [ "dry" ] ~doc)
let print_statistics =
let doc = "Print statistics" in
Arg.(value & flag & info [ "print-statistics" ] ~doc)
let no_strict_status =
let doc = "Disable strict status checking" in
Arg.(value & flag & info [ "no-strict-status" ] ~doc)
let from_file =
let doc =
"File containing a list of files to run. This argument discards any \
positional arguments provided."
in
Arg.(
value & opt (some fpath) None & info [ "F"; "from-file" ] ~doc ~docv:"VAL" )
let version = Cmd_version.version
let commands =
let open Term.Syntax in
let cmd_run =
let info =
let doc =
"Runs one or more scripts using. Also supports directory inputs"
in
Cmd.info ~version "run" ~doc
in
let term =
let+ debug
and+ dry
and+ print_statistics
and+ no_strict_status
and+ solver_type
and+ solver_mode
and+ from_file
and+ filenames in
let settings =
Settings.Run.make ~debug ~dry ~print_statistics ~no_strict_status
~solver_type ~solver_mode ?from_file filenames
in
Cmd_run.run settings
in
Cmd.v info term
in
let cmd_to_smt2 =
let info =
let doc = "Convert .smtml into .smt2" in
Cmd.info ~version "to-smt2" ~doc
in
let term =
let+ debug
and+ solver_type
and+ filename in
let settings = Settings.To_smt2.make ~debug ~solver_type filename in
Cmd_to_smt2.run settings
in
Cmd.v info term
in
let cmd_to_smtml =
let info =
let doc = "Print/Format the content of an .smtml file" in
Cmd.info ~version "to-smtml" ~doc
in
let term =
let+ filename in
Cmd_to_smt2.run_to_smtml ~filename
in
Cmd.v info term
in
let cmd_version =
let info =
let doc = "Print smtml version and linked libraries" in
Cmd.info ~version "version" ~doc
in
let term = Term.(const Cmd_version.run $ const ()) in
Cmd.v info term
in
let cmd_smtzilla =
let info =
let doc = "Using machine learning to select SMT solvers" in
Cmd.info "smtzilla" ~doc
in
let default = Term.(ret (const (`Help (`Plain, None)))) in
Cmd.group info ~default
Cmd_smtzilla.
[ extract_features_cmd; extract_queries_cmd; regression_cmd; train_cmd ]
in
let info = Cmd.info ~version "smtml" in
Cmd.group info
[ cmd_run; cmd_to_smt2; cmd_to_smtml; cmd_version; cmd_smtzilla ]