author | blanchet |
Sat, 25 Apr 2015 09:48:06 +0200 | |
changeset 60201 | 90e88e521e0e |
parent 59960 | 372ddff01244 |
child 61587 | c3974cd2d381 |
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 |
59960
372ddff01244
updated SMT module and Sledgehammer to fully open source Z3
blanchet
parents:
59035
diff
changeset
|
9 |
val cvc4_extensions: bool Config.T |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
10 |
val z3_extensions: bool Config.T |
57229 | 11 |
end; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
12 |
|
58061 | 13 |
structure SMT_Systems: SMT_SYSTEMS = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
14 |
struct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
15 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
16 |
(* helper functions *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
17 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
18 |
fun make_avail name () = getenv (name ^ "_SOLVER") <> "" |
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 |
fun make_command name () = [getenv (name ^ "_SOLVER")] |
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 outcome_of unsat sat unknown solver_name line = |
58061 | 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 raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ quote solver_name ^ |
|
27 |
" failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^ |
|
56094 | 28 |
" option for details")) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
29 |
|
60201 | 30 |
fun is_blank_or_error_line "" = true |
31 |
| is_blank_or_error_line s = String.isPrefix "(error " s |
|
32 |
||
57239 | 33 |
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
|
34 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
35 |
val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) |
60201 | 36 |
val (l, ls) = split_first (snd (take_prefix is_blank_or_error_line lines)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
37 |
in (test_outcome solver_name l, ls) end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
38 |
|
57704 | 39 |
fun on_first_non_unsupported_line test_outcome solver_name lines = |
40 |
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
|
41 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
42 |
(* CVC3 *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
43 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
44 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
45 |
fun cvc3_options ctxt = [ |
58061 | 46 |
"-seed", string_of_int (Config.get ctxt SMT_Config.random_seed), |
57239 | 47 |
"-lang", "smt2", |
58061 | 48 |
"-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
|
49 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
50 |
|
58061 | 51 |
val cvc3: SMT_Solver.solver_config = { |
57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57168
diff
changeset
|
52 |
name = "cvc3", |
58061 | 53 |
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
|
54 |
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
|
55 |
command = make_command "CVC3", |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
56 |
options = cvc3_options, |
57239 | 57 |
smt_options = [], |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
58 |
default_max_relevant = 400 (* FUDGE *), |
57239 | 59 |
outcome = on_first_line (outcome_of "unsat" "sat" "unknown"), |
57157 | 60 |
parse_proof = NONE, |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
61 |
replay = NONE } |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
62 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
63 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
64 |
|
57240 | 65 |
(* CVC4 *) |
66 |
||
58360 | 67 |
val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false) |
68 |
||
57240 | 69 |
local |
70 |
fun cvc4_options ctxt = [ |
|
58061 | 71 |
"--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), |
57240 | 72 |
"--lang=smt2", |
60201 | 73 |
"--continued-execution", |
58061 | 74 |
"--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))] |
58360 | 75 |
|
76 |
fun select_class ctxt = |
|
77 |
if Config.get ctxt cvc4_extensions then CVC4_Interface.smtlib_cvc4C |
|
78 |
else SMTLIB_Interface.smtlibC |
|
57240 | 79 |
in |
80 |
||
58061 | 81 |
val cvc4: SMT_Solver.solver_config = { |
57240 | 82 |
name = "cvc4", |
58360 | 83 |
class = select_class, |
57240 | 84 |
avail = make_avail "CVC4", |
85 |
command = make_command "CVC4", |
|
86 |
options = cvc4_options, |
|
59015 | 87 |
smt_options = [(":produce-unsat-cores", "true")], |
57240 | 88 |
default_max_relevant = 400 (* FUDGE *), |
89 |
outcome = on_first_line (outcome_of "unsat" "sat" "unknown"), |
|
59015 | 90 |
parse_proof = SOME (K CVC4_Proof_Parse.parse_proof), |
57240 | 91 |
replay = NONE } |
92 |
||
93 |
end |
|
94 |
||
57704 | 95 |
(* veriT *) |
96 |
||
58061 | 97 |
val veriT: SMT_Solver.solver_config = { |
59035
3a2153676705
renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names
blanchet
parents:
59015
diff
changeset
|
98 |
name = "verit", |
58061 | 99 |
class = K SMTLIB_Interface.smtlibC, |
57704 | 100 |
avail = make_avail "VERIT", |
101 |
command = make_command "VERIT", |
|
102 |
options = (fn ctxt => [ |
|
103 |
"--proof-version=1", |
|
104 |
"--proof=-", |
|
105 |
"--proof-prune", |
|
106 |
"--proof-merge", |
|
107 |
"--disable-print-success", |
|
108 |
"--disable-banner", |
|
58061 | 109 |
"--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]), |
57704 | 110 |
smt_options = [], |
58496
2ba52ecc4996
give more facts to veriT -- it seems to be able to cope with them
blanchet
parents:
58491
diff
changeset
|
111 |
default_max_relevant = 200 (* FUDGE *), |
57709 | 112 |
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
|
113 |
"warning : proof_done: status is still open"), |
58491 | 114 |
parse_proof = SOME (K VeriT_Proof_Parse.parse_proof), |
57704 | 115 |
replay = NONE } |
57240 | 116 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
117 |
(* Z3 *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
118 |
|
58061 | 119 |
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
|
120 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
121 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
122 |
fun z3_options ctxt = |
58061 | 123 |
["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), |
57168 | 124 |
"smt.refine_inj_axioms=false", |
58061 | 125 |
"-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
|
126 |
"-smt2"] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
127 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
128 |
fun select_class ctxt = |
58061 | 129 |
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
|
130 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
131 |
|
58061 | 132 |
val z3: SMT_Solver.solver_config = { |
57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57168
diff
changeset
|
133 |
name = "z3", |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
134 |
class = select_class, |
59960
372ddff01244
updated SMT module and Sledgehammer to fully open source Z3
blanchet
parents:
59035
diff
changeset
|
135 |
avail = make_avail "Z3", |
372ddff01244
updated SMT module and Sledgehammer to fully open source Z3
blanchet
parents:
59035
diff
changeset
|
136 |
command = make_command "Z3", |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
137 |
options = z3_options, |
57239 | 138 |
smt_options = [(":produce-proofs", "true")], |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
139 |
default_max_relevant = 350 (* FUDGE *), |
57239 | 140 |
outcome = on_first_line (outcome_of "unsat" "sat" "unknown"), |
58061 | 141 |
parse_proof = SOME Z3_Replay.parse_proof, |
142 |
replay = SOME Z3_Replay.replay } |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
143 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
144 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
145 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
146 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
147 |
(* overall setup *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
148 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
149 |
val _ = Theory.setup ( |
58061 | 150 |
SMT_Solver.add_solver cvc3 #> |
151 |
SMT_Solver.add_solver cvc4 #> |
|
152 |
SMT_Solver.add_solver veriT #> |
|
153 |
SMT_Solver.add_solver z3) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
154 |
|
57229 | 155 |
end; |