author | blanchet |
Wed, 17 Sep 2014 16:53:39 +0200 | |
changeset 58360 | dee1fd1cc631 |
parent 58061 | 3d060f43accb |
child 58491 | 5ddbc170e46c |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/SMT/smt_systems.ML |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
3 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
4 |
Setup SMT solvers. |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
5 |
*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
6 |
|
58061 | 7 |
signature SMT_SYSTEMS = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
8 |
sig |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
9 |
datatype z3_non_commercial = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
10 |
Z3_Non_Commercial_Unknown | |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
11 |
Z3_Non_Commercial_Accepted | |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
12 |
Z3_Non_Commercial_Declined |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
13 |
val z3_non_commercial: unit -> z3_non_commercial |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
14 |
val z3_extensions: bool Config.T |
57229 | 15 |
end; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
16 |
|
58061 | 17 |
structure SMT_Systems: SMT_SYSTEMS = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
18 |
struct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
19 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
20 |
(* helper functions *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
21 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
22 |
fun make_avail name () = getenv (name ^ "_SOLVER") <> "" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
23 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
24 |
fun make_command name () = [getenv (name ^ "_SOLVER")] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
25 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
26 |
fun outcome_of unsat sat unknown solver_name line = |
58061 | 27 |
if String.isPrefix unsat line then SMT_Solver.Unsat |
28 |
else if String.isPrefix sat line then SMT_Solver.Sat |
|
29 |
else if String.isPrefix unknown line then SMT_Solver.Unknown |
|
30 |
else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ quote solver_name ^ |
|
31 |
" failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^ |
|
56094 | 32 |
" option for details")) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
33 |
|
57239 | 34 |
fun on_first_line test_outcome solver_name lines = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
35 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
36 |
val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) |
57239 | 37 |
val (l, ls) = split_first (snd (take_prefix (curry (op =) "") lines)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
38 |
in (test_outcome solver_name l, ls) end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
39 |
|
57704 | 40 |
fun on_first_non_unsupported_line test_outcome solver_name lines = |
41 |
on_first_line test_outcome solver_name (filter (curry (op <>) "unsupported") lines) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
42 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
43 |
(* CVC3 *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
44 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
45 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
46 |
fun cvc3_options ctxt = [ |
58061 | 47 |
"-seed", string_of_int (Config.get ctxt SMT_Config.random_seed), |
57239 | 48 |
"-lang", "smt2", |
58061 | 49 |
"-timeout", string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
50 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
51 |
|
58061 | 52 |
val cvc3: SMT_Solver.solver_config = { |
57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57168
diff
changeset
|
53 |
name = "cvc3", |
58061 | 54 |
class = K SMTLIB_Interface.smtlibC, |
57210
5d61d875076a
rationalized CVC3 and Yices environment variable -- no need (unlike for Z3) to distinguish between old and new versions
blanchet
parents:
57209
diff
changeset
|
55 |
avail = make_avail "CVC3", |
5d61d875076a
rationalized CVC3 and Yices environment variable -- no need (unlike for Z3) to distinguish between old and new versions
blanchet
parents:
57209
diff
changeset
|
56 |
command = make_command "CVC3", |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
57 |
options = cvc3_options, |
57239 | 58 |
smt_options = [], |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
59 |
default_max_relevant = 400 (* FUDGE *), |
57239 | 60 |
outcome = on_first_line (outcome_of "unsat" "sat" "unknown"), |
57157 | 61 |
parse_proof = NONE, |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
62 |
replay = NONE } |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
63 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
64 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
65 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
66 |
|
57240 | 67 |
(* CVC4 *) |
68 |
||
58360 | 69 |
val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false) |
70 |
||
57240 | 71 |
local |
72 |
fun cvc4_options ctxt = [ |
|
58061 | 73 |
"--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), |
57240 | 74 |
"--lang=smt2", |
58061 | 75 |
"--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))] |
58360 | 76 |
|
77 |
fun select_class ctxt = |
|
78 |
if Config.get ctxt cvc4_extensions then CVC4_Interface.smtlib_cvc4C |
|
79 |
else SMTLIB_Interface.smtlibC |
|
57240 | 80 |
in |
81 |
||
58061 | 82 |
val cvc4: SMT_Solver.solver_config = { |
57240 | 83 |
name = "cvc4", |
58360 | 84 |
class = select_class, |
57240 | 85 |
avail = make_avail "CVC4", |
86 |
command = make_command "CVC4", |
|
87 |
options = cvc4_options, |
|
88 |
smt_options = [], |
|
89 |
default_max_relevant = 400 (* FUDGE *), |
|
90 |
outcome = on_first_line (outcome_of "unsat" "sat" "unknown"), |
|
91 |
parse_proof = NONE, |
|
92 |
replay = NONE } |
|
93 |
||
94 |
end |
|
95 |
||
57704 | 96 |
(* veriT *) |
97 |
||
58061 | 98 |
val veriT: SMT_Solver.solver_config = { |
57704 | 99 |
name = "veriT", |
58061 | 100 |
class = K SMTLIB_Interface.smtlibC, |
57704 | 101 |
avail = make_avail "VERIT", |
102 |
command = make_command "VERIT", |
|
103 |
options = (fn ctxt => [ |
|
104 |
"--proof-version=1", |
|
105 |
"--proof=-", |
|
106 |
"--proof-prune", |
|
107 |
"--proof-merge", |
|
108 |
"--disable-print-success", |
|
109 |
"--disable-banner", |
|
58061 | 110 |
"--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]), |
57704 | 111 |
smt_options = [], |
57709 | 112 |
default_max_relevant = 120 (* FUDGE *), |
113 |
outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" |
|
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57709
diff
changeset
|
114 |
"warning : proof_done: status is still open"), |
57704 | 115 |
parse_proof = SOME VeriT_Proof_Parse.parse_proof, |
116 |
replay = NONE } |
|
57240 | 117 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
118 |
(* Z3 *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
119 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
120 |
datatype z3_non_commercial = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
121 |
Z3_Non_Commercial_Unknown | |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
122 |
Z3_Non_Commercial_Accepted | |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
123 |
Z3_Non_Commercial_Declined |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
124 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
125 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
126 |
val accepted = member (op =) ["yes", "Yes", "YES"] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
127 |
val declined = member (op =) ["no", "No", "NO"] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
128 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
129 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
130 |
fun z3_non_commercial () = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
131 |
let |
56467 | 132 |
val flag1 = Options.default_string @{system_option z3_non_commercial} |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
133 |
val flag2 = getenv "Z3_NON_COMMERCIAL" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
134 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
135 |
if accepted flag1 then Z3_Non_Commercial_Accepted |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
136 |
else if declined flag1 then Z3_Non_Commercial_Declined |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
137 |
else if accepted flag2 then Z3_Non_Commercial_Accepted |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
138 |
else if declined flag2 then Z3_Non_Commercial_Declined |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
139 |
else Z3_Non_Commercial_Unknown |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
140 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
141 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
142 |
fun if_z3_non_commercial f = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
143 |
(case z3_non_commercial () of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
144 |
Z3_Non_Commercial_Accepted => f () |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
145 |
| Z3_Non_Commercial_Declined => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
146 |
error (Pretty.string_of (Pretty.para |
56131 | 147 |
"The SMT solver Z3 may be used only for non-commercial applications.")) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
148 |
| Z3_Non_Commercial_Unknown => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
149 |
error (Pretty.string_of (Pretty.para |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
150 |
("The SMT solver Z3 is not activated. To activate it, set the Isabelle \ |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
151 |
\system option \"z3_non_commercial\" to \"yes\" (e.g. via \ |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
152 |
\the Isabelle/jEdit menu Plugin Options / Isabelle / General).")))) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
153 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
154 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
155 |
|
58061 | 156 |
val z3_extensions = Attrib.setup_config_bool @{binding z3_extensions} (K false) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
157 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
158 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
159 |
fun z3_make_command name () = if_z3_non_commercial (make_command name) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
160 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
161 |
fun z3_options ctxt = |
58061 | 162 |
["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), |
57168 | 163 |
"smt.refine_inj_axioms=false", |
58061 | 164 |
"-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout)), |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
165 |
"-smt2"] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
166 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
167 |
fun select_class ctxt = |
58061 | 168 |
if Config.get ctxt z3_extensions then Z3_Interface.smtlib_z3C else SMTLIB_Interface.smtlibC |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
169 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
170 |
|
58061 | 171 |
val z3: SMT_Solver.solver_config = { |
57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57168
diff
changeset
|
172 |
name = "z3", |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
173 |
class = select_class, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
174 |
avail = make_avail "Z3_NEW", |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
175 |
command = z3_make_command "Z3_NEW", |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
176 |
options = z3_options, |
57239 | 177 |
smt_options = [(":produce-proofs", "true")], |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
178 |
default_max_relevant = 350 (* FUDGE *), |
57239 | 179 |
outcome = on_first_line (outcome_of "unsat" "sat" "unknown"), |
58061 | 180 |
parse_proof = SOME Z3_Replay.parse_proof, |
181 |
replay = SOME Z3_Replay.replay } |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
182 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
183 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
184 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
185 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
186 |
(* overall setup *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
187 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
188 |
val _ = Theory.setup ( |
58061 | 189 |
SMT_Solver.add_solver cvc3 #> |
190 |
SMT_Solver.add_solver cvc4 #> |
|
191 |
SMT_Solver.add_solver veriT #> |
|
192 |
SMT_Solver.add_solver z3) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
193 |
|
57229 | 194 |
end; |