author | blanchet |
Mon, 19 Jul 2021 14:47:52 +0200 | |
changeset 74048 | a0c9fc9c7dbe |
parent 73388 | a40e69fde2b4 |
child 74476 | 6424c54157d9 |
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 |
|
72478
b452242dce36
proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents:
72458
diff
changeset
|
18 |
fun check_tool var () = |
b452242dce36
proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents:
72458
diff
changeset
|
19 |
(case getenv var of |
b452242dce36
proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents:
72458
diff
changeset
|
20 |
"" => NONE |
72479 | 21 |
| s => |
22 |
if File.is_file (Path.variable var |> Path.expand |> Path.platform_exe) |
|
23 |
then SOME [s] else NONE); |
|
72478
b452242dce36
proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents:
72458
diff
changeset
|
24 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
25 |
fun make_avail name () = getenv (name ^ "_SOLVER") <> "" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
26 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
27 |
fun make_command name () = [getenv (name ^ "_SOLVER")] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
28 |
|
70327
c04d4951a155
handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)
blanchet
parents:
69593
diff
changeset
|
29 |
fun outcome_of unsat sat unknown timeout solver_name line = |
58061 | 30 |
if String.isPrefix unsat line then SMT_Solver.Unsat |
31 |
else if String.isPrefix sat line then SMT_Solver.Sat |
|
32 |
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
|
33 |
else if String.isPrefix timeout line then SMT_Solver.Time_Out |
58061 | 34 |
else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ quote solver_name ^ |
35 |
" failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^ |
|
56094 | 36 |
" option for details")) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
37 |
|
73104
6520d59fbdd7
ignore error messages produced by CVC4 when generating BV
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72667
diff
changeset
|
38 |
(* When used with bitvectors, CVC4 can produce error messages like: |
6520d59fbdd7
ignore error messages produced by CVC4 when generating BV
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72667
diff
changeset
|
39 |
|
6520d59fbdd7
ignore error messages produced by CVC4 when generating BV
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72667
diff
changeset
|
40 |
$ISABELLE_TMP_PREFIX/... No set-logic command was given before this point. |
6520d59fbdd7
ignore error messages produced by CVC4 when generating BV
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72667
diff
changeset
|
41 |
|
6520d59fbdd7
ignore error messages produced by CVC4 when generating BV
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72667
diff
changeset
|
42 |
These message should be ignored. |
6520d59fbdd7
ignore error messages produced by CVC4 when generating BV
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72667
diff
changeset
|
43 |
*) |
60201 | 44 |
fun is_blank_or_error_line "" = true |
73104
6520d59fbdd7
ignore error messages produced by CVC4 when generating BV
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72667
diff
changeset
|
45 |
| is_blank_or_error_line s = |
6520d59fbdd7
ignore error messages produced by CVC4 when generating BV
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72667
diff
changeset
|
46 |
String.isPrefix "(error " s orelse String.isPrefix (getenv "ISABELLE_TMP_PREFIX") s |
60201 | 47 |
|
57239 | 48 |
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
|
49 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
50 |
val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) |
67522 | 51 |
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
|
52 |
in (test_outcome solver_name l, ls) end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
53 |
|
57704 | 54 |
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
|
55 |
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
|
56 |
|
66551 | 57 |
|
57240 | 58 |
(* CVC4 *) |
59 |
||
69593 | 60 |
val cvc4_extensions = Attrib.setup_config_bool \<^binding>\<open>cvc4_extensions\<close> (K false) |
58360 | 61 |
|
57240 | 62 |
local |
73388
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
63 |
fun cvc4_options ctxt = |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
64 |
["--no-stats", |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
65 |
"--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
66 |
"--lang=smt2"] @ |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
67 |
(case SMT_Config.get_timeout ctxt of |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
68 |
NONE => [] |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
69 |
| SOME t => ["--tlimit", string_of_int (Time.toMilliseconds t)]) |
58360 | 70 |
|
71 |
fun select_class ctxt = |
|
66551 | 72 |
if Config.get ctxt cvc4_extensions then |
73 |
if Config.get ctxt SMT_Config.higher_order then |
|
74 |
CVC4_Interface.hosmtlib_cvc4C |
|
75 |
else |
|
76 |
CVC4_Interface.smtlib_cvc4C |
|
77 |
else |
|
78 |
if Config.get ctxt SMT_Config.higher_order then |
|
79 |
SMTLIB_Interface.hosmtlibC |
|
80 |
else |
|
81 |
SMTLIB_Interface.smtlibC |
|
57240 | 82 |
in |
83 |
||
58061 | 84 |
val cvc4: SMT_Solver.solver_config = { |
57240 | 85 |
name = "cvc4", |
58360 | 86 |
class = select_class, |
57240 | 87 |
avail = make_avail "CVC4", |
88 |
command = make_command "CVC4", |
|
89 |
options = cvc4_options, |
|
59015 | 90 |
smt_options = [(":produce-unsat-cores", "true")], |
57240 | 91 |
default_max_relevant = 400 (* FUDGE *), |
70327
c04d4951a155
handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)
blanchet
parents:
69593
diff
changeset
|
92 |
outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), |
59015 | 93 |
parse_proof = SOME (K CVC4_Proof_Parse.parse_proof), |
57240 | 94 |
replay = NONE } |
95 |
||
96 |
end |
|
97 |
||
66551 | 98 |
|
57704 | 99 |
(* veriT *) |
100 |
||
66551 | 101 |
local |
102 |
fun select_class ctxt = |
|
103 |
if Config.get ctxt SMT_Config.higher_order then |
|
104 |
SMTLIB_Interface.hosmtlibC |
|
105 |
else |
|
106 |
SMTLIB_Interface.smtlibC |
|
73388
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
107 |
|
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
108 |
fun veriT_options ctxt = |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
109 |
["--proof-with-sharing", |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
110 |
"--proof-define-skolems", |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
111 |
"--proof-prune", |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
112 |
"--proof-merge", |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
113 |
"--disable-print-success", |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
114 |
"--disable-banner"] @ |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
115 |
Verit_Proof.veriT_current_strategy (Context.Proof ctxt) |
66551 | 116 |
in |
117 |
||
58061 | 118 |
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
|
119 |
name = "verit", |
66551 | 120 |
class = select_class, |
72478
b452242dce36
proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents:
72458
diff
changeset
|
121 |
avail = is_some o check_tool "ISABELLE_VERIT", |
b452242dce36
proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents:
72458
diff
changeset
|
122 |
command = the o check_tool "ISABELLE_VERIT", |
73388
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
123 |
options = veriT_options, |
61587
c3974cd2d381
updating options to verit
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60201
diff
changeset
|
124 |
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
|
125 |
default_max_relevant = 200 (* FUDGE *), |
70327
c04d4951a155
handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)
blanchet
parents:
69593
diff
changeset
|
126 |
outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "timeout"), |
58491 | 127 |
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
|
128 |
replay = SOME Verit_Replay.replay } |
57240 | 129 |
|
66551 | 130 |
end |
131 |
||
132 |
||
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
133 |
(* Z3 *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
134 |
|
69593 | 135 |
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
|
136 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
137 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
138 |
fun z3_options ctxt = |
58061 | 139 |
["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), |
73388
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
140 |
"smt.refine_inj_axioms=false"] @ |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
141 |
(case SMT_Config.get_timeout ctxt of |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
142 |
NONE => [] |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
143 |
| SOME t => ["-T:" ^ string_of_int (Real.ceil (Time.toReal t))]) @ |
a40e69fde2b4
clarified smt: support Timeout.ignored and Timeout.scale_time;
wenzelm
parents:
73104
diff
changeset
|
144 |
["-smt2"] |
56078
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 |
fun select_class ctxt = |
58061 | 147 |
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
|
148 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
149 |
|
58061 | 150 |
val z3: SMT_Solver.solver_config = { |
57209
7ffa0f7e2775
removed '_new' sufffix in SMT2 solver names (in some cases)
blanchet
parents:
57168
diff
changeset
|
151 |
name = "z3", |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
152 |
class = select_class, |
59960
372ddff01244
updated SMT module and Sledgehammer to fully open source Z3
blanchet
parents:
59035
diff
changeset
|
153 |
avail = make_avail "Z3", |
372ddff01244
updated SMT module and Sledgehammer to fully open source Z3
blanchet
parents:
59035
diff
changeset
|
154 |
command = make_command "Z3", |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
155 |
options = z3_options, |
57239 | 156 |
smt_options = [(":produce-proofs", "true")], |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
157 |
default_max_relevant = 350 (* FUDGE *), |
70327
c04d4951a155
handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)
blanchet
parents:
69593
diff
changeset
|
158 |
outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), |
58061 | 159 |
parse_proof = SOME Z3_Replay.parse_proof, |
160 |
replay = SOME Z3_Replay.replay } |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
161 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
162 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
163 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
164 |
(* smt tactic *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
165 |
val parse_smt_options = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
166 |
Scan.optional |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
167 |
(Args.parens (Args.name -- Scan.option (\<^keyword>\<open>,\<close> |-- Args.name)) >> apfst SOME) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
168 |
(NONE, NONE) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
169 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
170 |
fun smt_method ((solver, stgy), thms) ctxt facts = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
171 |
let |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
172 |
val default_solver = SMT_Config.solver_of ctxt |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
173 |
val solver = the_default default_solver solver |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
174 |
val _ = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
175 |
if solver = "z3" andalso stgy <> NONE |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
176 |
then warning ("No strategy is available for z3. Ignoring " ^ quote (the stgy)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
177 |
else () |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
178 |
val ctxt = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
179 |
ctxt |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
180 |
|> (if stgy <> NONE then Context.proof_map (Verit_Proof.select_veriT_stgy (the stgy)) else I) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
181 |
|> Context.Proof |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
182 |
|> SMT_Config.select_solver solver |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
183 |
|> Context.proof_of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
184 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
185 |
HEADGOAL (SOLVED' (SMT_Solver.smt_tac ctxt (thms @ facts))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
186 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
187 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
188 |
val _ = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
189 |
Theory.setup |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
190 |
(Method.setup \<^binding>\<open>smt\<close> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
191 |
(Scan.lift parse_smt_options -- Attrib.thms >> (METHOD oo smt_method)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
70327
diff
changeset
|
192 |
"Call to the SMT solvers veriT or z3") |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
193 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
194 |
(* overall setup *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
195 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
196 |
val _ = Theory.setup ( |
58061 | 197 |
SMT_Solver.add_solver cvc4 #> |
198 |
SMT_Solver.add_solver veriT #> |
|
199 |
SMT_Solver.add_solver z3) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
200 |
|
57229 | 201 |
end; |