author | blanchet |
Fri, 07 Jun 2019 11:08:29 +0200 | |
changeset 70327 | c04d4951a155 |
parent 69593 | 3dda49e08b9d |
child 72458 | b44e894796d5 |
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 |
|
70327
c04d4951a155
handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)
blanchet
parents:
69593
diff
changeset
|
22 |
fun outcome_of unsat sat unknown timeout 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 |
|
70327
c04d4951a155
handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)
blanchet
parents:
69593
diff
changeset
|
26 |
else if String.isPrefix timeout line then SMT_Solver.Time_Out |
58061 | 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) ^ |
|
56094 | 29 |
" option for details")) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
30 |
|
60201 | 31 |
fun is_blank_or_error_line "" = true |
32 |
| is_blank_or_error_line s = String.isPrefix "(error " s |
|
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)) |
67522 | 37 |
val (l, ls) = split_first (drop_prefix is_blank_or_error_line 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 = |
67405
e9ab4ad7bd15
uniform use of Standard ML op-infix -- eliminated warnings;
wenzelm
parents:
67399
diff
changeset
|
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 *), |
70327
c04d4951a155
handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)
blanchet
parents:
69593
diff
changeset
|
60 |
outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), |
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 |
|
66551 | 66 |
|
57240 | 67 |
(* CVC4 *) |
68 |
||
69593 | 69 |
val cvc4_extensions = Attrib.setup_config_bool \<^binding>\<open>cvc4_extensions\<close> (K false) |
58360 | 70 |
|
57240 | 71 |
local |
72 |
fun cvc4_options ctxt = [ |
|
64461
be149db8207a
disable CVC4 statistics, and hence crashes upon user interruptions
blanchet
parents:
63102
diff
changeset
|
73 |
"--no-statistics", |
58061 | 74 |
"--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), |
57240 | 75 |
"--lang=smt2", |
60201 | 76 |
"--continued-execution", |
58061 | 77 |
"--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))] |
58360 | 78 |
|
79 |
fun select_class ctxt = |
|
66551 | 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 |
|
57240 | 90 |
in |
91 |
||
58061 | 92 |
val cvc4: SMT_Solver.solver_config = { |
57240 | 93 |
name = "cvc4", |
58360 | 94 |
class = select_class, |
57240 | 95 |
avail = make_avail "CVC4", |
96 |
command = make_command "CVC4", |
|
97 |
options = cvc4_options, |
|
59015 | 98 |
smt_options = [(":produce-unsat-cores", "true")], |
57240 | 99 |
default_max_relevant = 400 (* FUDGE *), |
70327
c04d4951a155
handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)
blanchet
parents:
69593
diff
changeset
|
100 |
outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), |
59015 | 101 |
parse_proof = SOME (K CVC4_Proof_Parse.parse_proof), |
57240 | 102 |
replay = NONE } |
103 |
||
104 |
end |
|
105 |
||
66551 | 106 |
|
57704 | 107 |
(* veriT *) |
108 |
||
66551 | 109 |
local |
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 |
|
115 |
in |
|
116 |
||
58061 | 117 |
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
|
118 |
name = "verit", |
66551 | 119 |
class = select_class, |
57704 | 120 |
avail = make_avail "VERIT", |
121 |
command = make_command "VERIT", |
|
122 |
options = (fn ctxt => [ |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67522
diff
changeset
|
123 |
"--proof-version=2", |
57704 | 124 |
"--proof-prune", |
125 |
"--proof-merge", |
|
126 |
"--disable-print-success", |
|
127 |
"--disable-banner", |
|
58061 | 128 |
"--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]), |
61587
c3974cd2d381
updating options to verit
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60201
diff
changeset
|
129 |
smt_options = [(":produce-proofs", "true")], |
58496
2ba52ecc4996
give more facts to veriT -- it seems to be able to cope with them
blanchet
parents:
58491
diff
changeset
|
130 |
default_max_relevant = 200 (* FUDGE *), |
70327
c04d4951a155
handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)
blanchet
parents:
69593
diff
changeset
|
131 |
outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "timeout"), |
58491 | 132 |
parse_proof = SOME (K VeriT_Proof_Parse.parse_proof), |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67522
diff
changeset
|
133 |
replay = SOME Verit_Replay.replay } |
57240 | 134 |
|
66551 | 135 |
end |
136 |
||
137 |
||
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
138 |
(* Z3 *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
139 |
|
69593 | 140 |
val z3_extensions = Attrib.setup_config_bool \<^binding>\<open>z3_extensions\<close> (K false) |
56078
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 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
143 |
fun z3_options ctxt = |
58061 | 144 |
["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), |
57168 | 145 |
"smt.refine_inj_axioms=false", |
58061 | 146 |
"-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
|
147 |
"-smt2"] |
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 |
fun select_class ctxt = |
58061 | 150 |
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
|
151 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
152 |
|
58061 | 153 |
val z3: SMT_Solver.solver_config = { |
57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57168
diff
changeset
|
154 |
name = "z3", |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
155 |
class = select_class, |
59960
372ddff01244
updated SMT module and Sledgehammer to fully open source Z3
blanchet
parents:
59035
diff
changeset
|
156 |
avail = make_avail "Z3", |
372ddff01244
updated SMT module and Sledgehammer to fully open source Z3
blanchet
parents:
59035
diff
changeset
|
157 |
command = make_command "Z3", |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
158 |
options = z3_options, |
57239 | 159 |
smt_options = [(":produce-proofs", "true")], |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
160 |
default_max_relevant = 350 (* FUDGE *), |
70327
c04d4951a155
handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)
blanchet
parents:
69593
diff
changeset
|
161 |
outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), |
58061 | 162 |
parse_proof = SOME Z3_Replay.parse_proof, |
163 |
replay = SOME Z3_Replay.replay } |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
164 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
165 |
end |
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 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
168 |
(* overall setup *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
169 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
170 |
val _ = Theory.setup ( |
58061 | 171 |
SMT_Solver.add_solver cvc3 #> |
172 |
SMT_Solver.add_solver cvc4 #> |
|
173 |
SMT_Solver.add_solver veriT #> |
|
174 |
SMT_Solver.add_solver z3) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
175 |
|
57229 | 176 |
end; |