1(*  Title:      HOL/Tools/SMT/smt_systems.ML
2    Author:     Sascha Boehme, TU Muenchen
3
4Setup SMT solvers.
5*)
6
7signature SMT_SYSTEMS =
8sig
9  val cvc4_extensions: bool Config.T
10  val z3_extensions: bool Config.T
11end;
12
13structure SMT_Systems: SMT_SYSTEMS =
14struct
15
16(* helper functions *)
17
18fun make_avail name () = getenv (name ^ "_SOLVER") <> ""
19
20fun make_command name () = [getenv (name ^ "_SOLVER")]
21
22fun outcome_of unsat sat unknown timeout solver_name line =
23  if String.isPrefix unsat line then SMT_Solver.Unsat
24  else if String.isPrefix sat line then SMT_Solver.Sat
25  else if String.isPrefix unknown line then SMT_Solver.Unknown
26  else if String.isPrefix timeout line then SMT_Solver.Time_Out
27  else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ quote solver_name ^
28    " failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^
29    " option for details"))
30
31fun is_blank_or_error_line "" = true
32  | is_blank_or_error_line s = String.isPrefix "(error " s
33
34fun on_first_line test_outcome solver_name lines =
35  let
36    val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
37    val (l, ls) = split_first (drop_prefix is_blank_or_error_line lines)
38  in (test_outcome solver_name l, ls) end
39
40fun on_first_non_unsupported_line test_outcome solver_name lines =
41  on_first_line test_outcome solver_name (filter (curry (op <>) "unsupported") lines)
42
43(* CVC3 *)
44
45local
46  fun cvc3_options ctxt = [
47    "-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
48    "-lang", "smt2",
49    "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]
50in
51
52val cvc3: SMT_Solver.solver_config = {
53  name = "cvc3",
54  class = K SMTLIB_Interface.smtlibC,
55  avail = make_avail "CVC3",
56  command = make_command "CVC3",
57  options = cvc3_options,
58  smt_options = [],
59  default_max_relevant = 400 (* FUDGE *),
60  outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
61  parse_proof = NONE,
62  replay = NONE }
63
64end
65
66
67(* CVC4 *)
68
69val cvc4_extensions = Attrib.setup_config_bool \<^binding>\<open>cvc4_extensions\<close> (K false)
70
71local
72  fun cvc4_options ctxt = [
73    "--no-statistics",
74    "--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
75    "--lang=smt2",
76    "--continued-execution",
77    "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
78
79  fun select_class ctxt =
80    if Config.get ctxt cvc4_extensions then
81      if Config.get ctxt SMT_Config.higher_order then
82        CVC4_Interface.hosmtlib_cvc4C
83      else
84        CVC4_Interface.smtlib_cvc4C
85    else
86      if Config.get ctxt SMT_Config.higher_order then
87        SMTLIB_Interface.hosmtlibC
88      else
89        SMTLIB_Interface.smtlibC
90in
91
92val cvc4: SMT_Solver.solver_config = {
93  name = "cvc4",
94  class = select_class,
95  avail = make_avail "CVC4",
96  command = make_command "CVC4",
97  options = cvc4_options,
98  smt_options = [(":produce-unsat-cores", "true")],
99  default_max_relevant = 400 (* FUDGE *),
100  outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
101  parse_proof = SOME (K CVC4_Proof_Parse.parse_proof),
102  replay = NONE }
103
104end
105
106
107(* veriT *)
108
109local
110  fun select_class ctxt =
111    if Config.get ctxt SMT_Config.higher_order then
112      SMTLIB_Interface.hosmtlibC
113    else
114      SMTLIB_Interface.smtlibC
115in
116
117val veriT: SMT_Solver.solver_config = {
118  name = "verit",
119  class = select_class,
120  avail = make_avail "VERIT",
121  command = make_command "VERIT",
122  options = (fn ctxt => [
123    "--proof-version=2",
124    "--proof-prune",
125    "--proof-merge",
126    "--disable-print-success",
127    "--disable-banner",
128    "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]),
129  smt_options = [(":produce-proofs", "true")],
130  default_max_relevant = 200 (* FUDGE *),
131  outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "timeout"),
132  parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
133  replay = SOME Verit_Replay.replay }
134
135end
136
137
138(* Z3 *)
139
140val z3_extensions = Attrib.setup_config_bool \<^binding>\<open>z3_extensions\<close> (K false)
141
142local
143  fun z3_options ctxt =
144    ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
145     "smt.refine_inj_axioms=false",
146     "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout)),
147     "-smt2"]
148
149  fun select_class ctxt =
150    if Config.get ctxt z3_extensions then Z3_Interface.smtlib_z3C else SMTLIB_Interface.smtlibC
151in
152
153val z3: SMT_Solver.solver_config = {
154  name = "z3",
155  class = select_class,
156  avail = make_avail "Z3",
157  command = make_command "Z3",
158  options = z3_options,
159  smt_options = [(":produce-proofs", "true")],
160  default_max_relevant = 350 (* FUDGE *),
161  outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
162  parse_proof = SOME Z3_Replay.parse_proof,
163  replay = SOME Z3_Replay.replay }
164
165end
166
167
168(* overall setup *)
169
170val _ = Theory.setup (
171  SMT_Solver.add_solver cvc3 #>
172  SMT_Solver.add_solver cvc4 #>
173  SMT_Solver.add_solver veriT #>
174  SMT_Solver.add_solver z3)
175
176end;
177