author | desharna |
Wed, 09 Feb 2022 13:02:59 +0100 | |
changeset 75067 | c23aa0d177b4 |
parent 75063 | 7ff39293e265 |
child 75069 | 455d886009b1 |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML |
56081 | 2 |
Author: Fabian Immler, TU Muenchen |
3 |
Author: Makarius |
|
4 |
Author: Jasmin Blanchette, TU Muenchen |
|
5 |
||
6 |
SMT solvers as Sledgehammer provers. |
|
7 |
*) |
|
8 |
||
58061 | 9 |
signature SLEDGEHAMMER_PROVER_SMT = |
56081 | 10 |
sig |
11 |
type stature = ATP_Problem_Generate.stature |
|
12 |
type mode = Sledgehammer_Prover.mode |
|
13 |
type prover = Sledgehammer_Prover.prover |
|
14 |
||
58061 | 15 |
val smt_builtins : bool Config.T |
16 |
val smt_triggers : bool Config.T |
|
56081 | 17 |
|
58061 | 18 |
val is_smt_prover : Proof.context -> string -> bool |
75036 | 19 |
val is_smt_prover_installed : Proof.context -> string -> bool |
58061 | 20 |
val run_smt_solver : mode -> string -> prover |
75036 | 21 |
|
22 |
val smts : Proof.context -> string list |
|
56081 | 23 |
end; |
24 |
||
58061 | 25 |
structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT = |
56081 | 26 |
struct |
27 |
||
28 |
open ATP_Util |
|
29 |
open ATP_Proof |
|
30 |
open ATP_Problem_Generate |
|
31 |
open ATP_Proof_Reconstruct |
|
32 |
open Sledgehammer_Util |
|
33 |
open Sledgehammer_Proof_Methods |
|
56083
b5d1d9c60341
have Sledgehammer generate Isar proofs from Z3 proofs
blanchet
parents:
56082
diff
changeset
|
34 |
open Sledgehammer_Isar |
72400 | 35 |
open Sledgehammer_ATP_Systems |
56081 | 36 |
open Sledgehammer_Prover |
37 |
||
69593 | 38 |
val smt_builtins = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_builtins\<close> (K true) |
39 |
val smt_triggers = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_triggers\<close> (K true) |
|
56081 | 40 |
|
75040 | 41 |
val smts = sort_strings o SMT_Config.all_solvers_of |
75036 | 42 |
|
43 |
val is_smt_prover = member (op =) o smts |
|
44 |
val is_smt_prover_installed = member (op =) o SMT_Config.available_solvers_of |
|
56081 | 45 |
|
58061 | 46 |
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out |
56081 | 47 |
properly in the SMT module, we must interpret these here. *) |
48 |
val z3_failures = |
|
49 |
[(101, OutOfResources), |
|
50 |
(103, MalformedInput), |
|
51 |
(110, MalformedInput), |
|
52 |
(112, TimedOut)] |
|
53 |
val unix_failures = |
|
59019 | 54 |
[(134, Crashed), |
55 |
(138, Crashed), |
|
56081 | 56 |
(139, Crashed)] |
58061 | 57 |
val smt_failures = z3_failures @ unix_failures |
56081 | 58 |
|
58061 | 59 |
fun failure_of_smt_failure (SMT_Failure.Counterexample genuine) = |
57158 | 60 |
if genuine then Unprovable else GaveUp |
58061 | 61 |
| failure_of_smt_failure SMT_Failure.Time_Out = TimedOut |
62 |
| failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) = |
|
63 |
(case AList.lookup (op =) smt_failures code of |
|
56081 | 64 |
SOME failure => failure |
63692 | 65 |
| NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code)) |
58061 | 66 |
| failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources |
67 |
| failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s |
|
56081 | 68 |
|
69 |
val is_boring_builtin_typ = |
|
69593 | 70 |
not o exists_subtype (member (op =) [\<^typ>\<open>nat\<close>, \<^typ>\<open>int\<close>, HOLogic.realT]) |
56081 | 71 |
|
75017
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
72 |
fun smt_filter name ({debug, overlord, max_mono_iters, max_new_mono_instances, |
75063
7ff39293e265
added possibility of extra options to SMT slices
blanchet
parents:
75060
diff
changeset
|
73 |
type_enc, slices, timeout, ...} : params) state goal i facts options = |
56081 | 74 |
let |
75023 | 75 |
val run_timeout = slice_timeout slices timeout |
74891
db4b8dd587a5
added support for higher-order SMT proof search in Sledgehammer
desharna
parents:
72798
diff
changeset
|
76 |
val (higher_order, nat_as_int) = |
db4b8dd587a5
added support for higher-order SMT proof search in Sledgehammer
desharna
parents:
72798
diff
changeset
|
77 |
(case type_enc of |
db4b8dd587a5
added support for higher-order SMT proof search in Sledgehammer
desharna
parents:
72798
diff
changeset
|
78 |
SOME s => (String.isSubstring "native_higher" s, String.isSubstring "arith" s) |
db4b8dd587a5
added support for higher-order SMT proof search in Sledgehammer
desharna
parents:
72798
diff
changeset
|
79 |
| NONE => (false, false)) |
75017
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
80 |
fun repair_context ctxt = ctxt |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
81 |
|> Context.proof_map (SMT_Config.select_solver name) |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
82 |
|> Config.put SMT_Config.higher_order higher_order |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
83 |
|> Config.put SMT_Config.nat_as_int nat_as_int |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
84 |
|> (if overlord then |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
85 |
Config.put SMT_Config.debug_files |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
86 |
(overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name)) |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
87 |
else |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
88 |
I) |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
89 |
|> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers) |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
90 |
|> not (Config.get ctxt smt_builtins) |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
91 |
? (SMT_Builtin.filter_builtins is_boring_builtin_typ |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
92 |
#> Config.put SMT_Systems.z3_extensions false) |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
93 |
|> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
94 |
default_max_new_mono_instances |
56081 | 95 |
|
96 |
val state = Proof.map_context (repair_context) state |
|
97 |
val ctxt = Proof.context_of state |
|
98 |
||
75017
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
99 |
val timer = Timer.startRealTimer () |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
100 |
val birth = Timer.checkRealTimer timer |
56081 | 101 |
|
75017
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
102 |
val filter_result as {outcome, ...} = |
75063
7ff39293e265
added possibility of extra options to SMT slices
blanchet
parents:
75060
diff
changeset
|
103 |
SMT_Solver.smt_filter ctxt goal facts i run_timeout options |
75017
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
104 |
handle exn => |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
105 |
if Exn.is_interrupt exn orelse debug then |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
106 |
Exn.reraise exn |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
107 |
else |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
108 |
{outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), fact_ids = NONE, |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
109 |
atp_proof = K []} |
56081 | 110 |
|
75017
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
111 |
val death = Timer.checkRealTimer timer |
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
112 |
val run_time = death - birth |
56081 | 113 |
in |
75017
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
114 |
{outcome = outcome, filter_result = filter_result, used_from = facts, run_time = run_time} |
56081 | 115 |
end |
116 |
||
75067
c23aa0d177b4
used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
desharna
parents:
75063
diff
changeset
|
117 |
fun run_smt_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, |
75017
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
118 |
smt_proofs, minimize, preplay_timeout, ...}) |
75025 | 119 |
({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) |
120 |
slice = |
|
56081 | 121 |
let |
122 |
val ctxt = Proof.context_of state |
|
123 |
||
75067
c23aa0d177b4
used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
desharna
parents:
75063
diff
changeset
|
124 |
val ((good_max_facts, good_fact_filter), SMT_Slice options) = slice |
75025 | 125 |
|
75067
c23aa0d177b4
used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
desharna
parents:
75063
diff
changeset
|
126 |
val facts = facts_of_filter good_fact_filter factss |
c23aa0d177b4
used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
desharna
parents:
75063
diff
changeset
|
127 |
|> take good_max_facts |
57243 | 128 |
|
57159 | 129 |
val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} = |
75063
7ff39293e265
added possibility of extra options to SMT slices
blanchet
parents:
75060
diff
changeset
|
130 |
smt_filter name params state goal subgoal facts options |
60201 | 131 |
val used_facts = |
132 |
(case fact_ids of |
|
133 |
NONE => map fst used_from |
|
60924
610794dff23c
tuned signature, in accordance to sortBy in Scala;
wenzelm
parents:
60201
diff
changeset
|
134 |
| SOME ids => sort_by fst (map (fst o snd) ids)) |
58061 | 135 |
val outcome = Option.map failure_of_smt_failure outcome |
56081 | 136 |
|
57738 | 137 |
val (preferred_methss, message) = |
56081 | 138 |
(case outcome of |
139 |
NONE => |
|
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
140 |
let |
75020
b087610592b4
rationalized output for forthcoming slicing model
blanchet
parents:
75017
diff
changeset
|
141 |
val _ = found_proof name; |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72400
diff
changeset
|
142 |
val preferred = |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72400
diff
changeset
|
143 |
if smt_proofs then |
72798
e732c98b02e6
tuned proof preplay to explicitly refer to Z3 backend
desharna
parents:
72518
diff
changeset
|
144 |
SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Z3) |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72400
diff
changeset
|
145 |
else |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72400
diff
changeset
|
146 |
Metis_Method (NONE, NONE); |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72400
diff
changeset
|
147 |
val methss = bunches_of_proof_methods ctxt try0 smt_proofs false liftingN; |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
148 |
in |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72400
diff
changeset
|
149 |
((preferred, methss), |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
150 |
fn preplay => |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
151 |
let |
58843 | 152 |
val _ = if verbose then writeln "Generating proof text..." else () |
57723
668322cd58f4
use parallel preplay machinery also for one-line proofs
blanchet
parents:
57721
diff
changeset
|
153 |
|
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
154 |
fun isar_params () = |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
155 |
(verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (), |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
156 |
goal) |
57056 | 157 |
|
57750 | 158 |
val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
159 |
val num_chained = length (#facts (Proof.goal state)) |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
160 |
in |
71931
0c8a9c028304
simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents:
69593
diff
changeset
|
161 |
proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params |
57738 | 162 |
end) |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
163 |
end |
57738 | 164 |
| SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) |
56081 | 165 |
in |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
166 |
{outcome = outcome, used_facts = used_facts, used_from = used_from, |
57738 | 167 |
preferred_methss = preferred_methss, run_time = run_time, message = message} |
56081 | 168 |
end |
169 |
||
170 |
end; |