author | wenzelm |
Fri, 31 Oct 2014 11:36:41 +0100 | |
changeset 58843 | 521cea5fa777 |
parent 58498 | 59bdd4f57255 |
child 59019 | 0c58b5cf989a |
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 |
|
17 |
val smt_max_slices : int Config.T |
|
18 |
val smt_slice_fact_frac : real Config.T |
|
19 |
val smt_slice_time_frac : real Config.T |
|
20 |
val smt_slice_min_secs : int Config.T |
|
56081 | 21 |
|
58061 | 22 |
val is_smt_prover : Proof.context -> string -> bool |
23 |
val run_smt_solver : mode -> string -> prover |
|
56081 | 24 |
end; |
25 |
||
58061 | 26 |
structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT = |
56081 | 27 |
struct |
28 |
||
29 |
open ATP_Util |
|
30 |
open ATP_Proof |
|
31 |
open ATP_Systems |
|
32 |
open ATP_Problem_Generate |
|
33 |
open ATP_Proof_Reconstruct |
|
34 |
open Sledgehammer_Util |
|
35 |
open Sledgehammer_Proof_Methods |
|
56083
b5d1d9c60341
have Sledgehammer generate Isar proofs from Z3 proofs
blanchet
parents:
56082
diff
changeset
|
36 |
open Sledgehammer_Isar |
56081 | 37 |
open Sledgehammer_Prover |
38 |
||
58061 | 39 |
val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true) |
40 |
val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true) |
|
56081 | 41 |
|
58061 | 42 |
val is_smt_prover = member (op =) o SMT_Config.available_solvers_of |
56081 | 43 |
|
58061 | 44 |
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out |
56081 | 45 |
properly in the SMT module, we must interpret these here. *) |
46 |
val z3_failures = |
|
47 |
[(101, OutOfResources), |
|
48 |
(103, MalformedInput), |
|
49 |
(110, MalformedInput), |
|
50 |
(112, TimedOut)] |
|
51 |
val unix_failures = |
|
52 |
[(138, Crashed), |
|
53 |
(139, Crashed)] |
|
58061 | 54 |
val smt_failures = z3_failures @ unix_failures |
56081 | 55 |
|
58061 | 56 |
fun failure_of_smt_failure (SMT_Failure.Counterexample genuine) = |
57158 | 57 |
if genuine then Unprovable else GaveUp |
58061 | 58 |
| failure_of_smt_failure SMT_Failure.Time_Out = TimedOut |
59 |
| failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) = |
|
60 |
(case AList.lookup (op =) smt_failures code of |
|
56081 | 61 |
SOME failure => failure |
62 |
| NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ ".")) |
|
58061 | 63 |
| failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources |
64 |
| failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s |
|
56081 | 65 |
|
66 |
(* FUDGE *) |
|
58061 | 67 |
val smt_max_slices = Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8) |
68 |
val smt_slice_fact_frac = |
|
69 |
Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.667) |
|
70 |
val smt_slice_time_frac = |
|
71 |
Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333) |
|
72 |
val smt_slice_min_secs = Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3) |
|
56081 | 73 |
|
74 |
val is_boring_builtin_typ = |
|
75 |
not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT]) |
|
76 |
||
58061 | 77 |
fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice, |
56081 | 78 |
...} : params) state goal i = |
79 |
let |
|
80 |
fun repair_context ctxt = |
|
58061 | 81 |
ctxt |> Context.proof_map (SMT_Config.select_solver name) |
82 |
|> Config.put SMT_Config.verbose debug |
|
56081 | 83 |
|> (if overlord then |
58061 | 84 |
Config.put SMT_Config.debug_files |
56081 | 85 |
(overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name)) |
86 |
else |
|
87 |
I) |
|
58061 | 88 |
|> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers) |
89 |
|> not (Config.get ctxt smt_builtins) |
|
90 |
? (SMT_Builtin.filter_builtins is_boring_builtin_typ |
|
91 |
#> Config.put SMT_Systems.z3_extensions false) |
|
56081 | 92 |
|> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances |
93 |
default_max_new_mono_instances |
|
94 |
||
95 |
val state = Proof.map_context (repair_context) state |
|
96 |
val ctxt = Proof.context_of state |
|
58061 | 97 |
val max_slices = if slice then Config.get ctxt smt_max_slices else 1 |
56081 | 98 |
|
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
57159
diff
changeset
|
99 |
fun do_slice timeout slice outcome0 time_so_far (factss as (fact_filter, facts) :: _) = |
56081 | 100 |
let |
101 |
val timer = Timer.startRealTimer () |
|
102 |
val slice_timeout = |
|
103 |
if slice < max_slices then |
|
104 |
let val ms = Time.toMilliseconds timeout in |
|
58061 | 105 |
Int.min (ms, Int.max (1000 * Config.get ctxt smt_slice_min_secs, |
106 |
Real.ceil (Config.get ctxt smt_slice_time_frac * Real.fromInt ms))) |
|
56081 | 107 |
|> Time.fromMilliseconds |
108 |
end |
|
109 |
else |
|
110 |
timeout |
|
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
57159
diff
changeset
|
111 |
val num_facts = length facts |
56081 | 112 |
val _ = |
113 |
if debug then |
|
114 |
quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^ |
|
115 |
" fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout |
|
58843 | 116 |
|> writeln |
56081 | 117 |
else |
118 |
() |
|
119 |
val birth = Timer.checkRealTimer timer |
|
120 |
||
56104
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
56099
diff
changeset
|
121 |
val filter_result as {outcome, ...} = |
58061 | 122 |
SMT_Solver.smt_filter ctxt goal facts i slice_timeout |
56081 | 123 |
handle exn => |
56094 | 124 |
if Exn.is_interrupt exn orelse debug then |
56083
b5d1d9c60341
have Sledgehammer generate Isar proofs from Z3 proofs
blanchet
parents:
56082
diff
changeset
|
125 |
reraise exn |
b5d1d9c60341
have Sledgehammer generate Isar proofs from Z3 proofs
blanchet
parents:
56082
diff
changeset
|
126 |
else |
58061 | 127 |
{outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), |
57159 | 128 |
fact_ids = [], atp_proof = K []} |
56081 | 129 |
|
130 |
val death = Timer.checkRealTimer timer |
|
131 |
val outcome0 = if is_none outcome0 then SOME outcome else outcome0 |
|
132 |
val time_so_far = Time.+ (time_so_far, Time.- (death, birth)) |
|
56083
b5d1d9c60341
have Sledgehammer generate Isar proofs from Z3 proofs
blanchet
parents:
56082
diff
changeset
|
133 |
val timeout = Time.- (timeout, Timer.checkRealTimer timer) |
56081 | 134 |
|
135 |
val too_many_facts_perhaps = |
|
136 |
(case outcome of |
|
137 |
NONE => false |
|
58061 | 138 |
| SOME (SMT_Failure.Counterexample _) => false |
139 |
| SOME SMT_Failure.Time_Out => slice_timeout <> timeout |
|
140 |
| SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *) |
|
141 |
| SOME SMT_Failure.Out_Of_Memory => true |
|
142 |
| SOME (SMT_Failure.Other_Failure _) => true) |
|
56081 | 143 |
in |
144 |
if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso |
|
145 |
Time.> (timeout, Time.zeroTime) then |
|
146 |
let |
|
147 |
val new_num_facts = |
|
58061 | 148 |
Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts) |
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
57159
diff
changeset
|
149 |
val factss as (new_fact_filter, _) :: _ = |
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
57159
diff
changeset
|
150 |
factss |
56081 | 151 |
|> (fn (x :: xs) => xs @ [x]) |
152 |
|> app_hd (apsnd (take new_num_facts)) |
|
153 |
val show_filter = fact_filter <> new_fact_filter |
|
154 |
||
155 |
fun num_of_facts fact_filter num_facts = |
|
156 |
string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^ |
|
157 |
" fact" ^ plural_s num_facts |
|
158 |
||
159 |
val _ = |
|
160 |
if debug then |
|
161 |
quote name ^ " invoked with " ^ |
|
162 |
num_of_facts fact_filter num_facts ^ ": " ^ |
|
58061 | 163 |
string_of_atp_failure (failure_of_smt_failure (the outcome)) ^ |
56081 | 164 |
" Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^ |
165 |
"..." |
|
58843 | 166 |
|> writeln |
56081 | 167 |
else |
168 |
() |
|
169 |
in |
|
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
57159
diff
changeset
|
170 |
do_slice timeout (slice + 1) outcome0 time_so_far factss |
56081 | 171 |
end |
172 |
else |
|
56104
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
56099
diff
changeset
|
173 |
{outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result, |
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
57159
diff
changeset
|
174 |
used_from = facts, run_time = time_so_far} |
56081 | 175 |
end |
176 |
in |
|
177 |
do_slice timeout 1 NONE Time.zeroTime |
|
178 |
end |
|
179 |
||
58061 | 180 |
fun run_smt_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs, |
57245 | 181 |
minimize, preplay_timeout, ...}) |
57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57734
diff
changeset
|
182 |
({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = |
56081 | 183 |
let |
184 |
val thy = Proof.theory_of state |
|
185 |
val ctxt = Proof.context_of state |
|
186 |
||
57243 | 187 |
val factss = map (apsnd (map (apsnd (Thm.transfer thy)))) factss |
188 |
||
57159 | 189 |
val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} = |
58061 | 190 |
smt_filter_loop name params state goal subgoal factss |
56104
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
56099
diff
changeset
|
191 |
val used_named_facts = map snd fact_ids |
57776
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57750
diff
changeset
|
192 |
val used_facts = sort_wrt fst (map fst used_named_facts) |
58061 | 193 |
val outcome = Option.map failure_of_smt_failure outcome |
56081 | 194 |
|
57738 | 195 |
val (preferred_methss, message) = |
56081 | 196 |
(case outcome of |
197 |
NONE => |
|
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
198 |
let |
58498 | 199 |
val smt_method = smt_proofs <> SOME false |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
200 |
val preferred_methss = |
58498 | 201 |
(if smt_method then SMT_Method else Metis_Method (NONE, NONE), |
202 |
bunches_of_proof_methods try0 smt_method false liftingN) |
|
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
203 |
in |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
204 |
(preferred_methss, |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
205 |
fn preplay => |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
206 |
let |
58843 | 207 |
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
|
208 |
|
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
209 |
fun isar_params () = |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
210 |
(verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (), |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
211 |
goal) |
57056 | 212 |
|
57750 | 213 |
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
|
214 |
val num_chained = length (#facts (Proof.goal state)) |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
215 |
in |
57738 | 216 |
proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained |
217 |
one_line_params |
|
218 |
end) |
|
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
219 |
end |
57738 | 220 |
| SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) |
56081 | 221 |
in |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
222 |
{outcome = outcome, used_facts = used_facts, used_from = used_from, |
57738 | 223 |
preferred_methss = preferred_methss, run_time = run_time, message = message} |
56081 | 224 |
end |
225 |
||
226 |
end; |