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