author | blanchet |
Mon, 02 Jun 2014 17:34:27 +0200 | |
changeset 57159 | 24cbdebba35a |
parent 57158 | f028d93798e6 |
child 57165 | 7b1bf424ec5f |
permissions | -rw-r--r-- |
56081 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML |
2 |
Author: Fabian Immler, TU Muenchen |
|
3 |
Author: Makarius |
|
4 |
Author: Jasmin Blanchette, TU Muenchen |
|
5 |
||
6 |
SMT solvers as Sledgehammer provers. |
|
7 |
*) |
|
8 |
||
9 |
signature SLEDGEHAMMER_PROVER_SMT2 = |
|
10 |
sig |
|
11 |
type stature = ATP_Problem_Generate.stature |
|
12 |
type mode = Sledgehammer_Prover.mode |
|
13 |
type prover = Sledgehammer_Prover.prover |
|
14 |
||
15 |
val smt2_builtins : bool Config.T |
|
16 |
val smt2_triggers : bool Config.T |
|
17 |
val smt2_weights : bool Config.T |
|
18 |
val smt2_weight_min_facts : int Config.T |
|
19 |
val smt2_min_weight : int Config.T |
|
20 |
val smt2_max_weight : int Config.T |
|
21 |
val smt2_max_weight_index : int Config.T |
|
22 |
val smt2_weight_curve : (int -> int) Unsynchronized.ref |
|
23 |
val smt2_max_slices : int Config.T |
|
24 |
val smt2_slice_fact_frac : real Config.T |
|
25 |
val smt2_slice_time_frac : real Config.T |
|
26 |
val smt2_slice_min_secs : int Config.T |
|
27 |
||
28 |
val is_smt2_prover : Proof.context -> string -> bool |
|
29 |
val run_smt2_solver : mode -> string -> prover |
|
30 |
end; |
|
31 |
||
32 |
structure Sledgehammer_Prover_SMT2 : SLEDGEHAMMER_PROVER_SMT2 = |
|
33 |
struct |
|
34 |
||
35 |
open ATP_Util |
|
36 |
open ATP_Proof |
|
37 |
open ATP_Systems |
|
38 |
open ATP_Problem_Generate |
|
39 |
open ATP_Proof_Reconstruct |
|
40 |
open Sledgehammer_Util |
|
41 |
open Sledgehammer_Proof_Methods |
|
56083
b5d1d9c60341
have Sledgehammer generate Isar proofs from Z3 proofs
blanchet
parents:
56082
diff
changeset
|
42 |
open Sledgehammer_Isar |
56081 | 43 |
open Sledgehammer_Prover |
44 |
||
45 |
val smt2_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt2_builtins} (K true) |
|
46 |
val smt2_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt2_triggers} (K true) |
|
47 |
val smt2_weights = Attrib.setup_config_bool @{binding sledgehammer_smt2_weights} (K true) |
|
48 |
val smt2_weight_min_facts = |
|
49 |
Attrib.setup_config_int @{binding sledgehammer_smt2_weight_min_facts} (K 20) |
|
50 |
||
56132
64eeda68e693
delayed construction of command (and of noncommercial check) + tuning
blanchet
parents:
56128
diff
changeset
|
51 |
val is_smt2_prover = member (op =) o SMT2_Config.available_solvers_of |
56081 | 52 |
|
53 |
(* FUDGE *) |
|
54 |
val smt2_min_weight = Attrib.setup_config_int @{binding sledgehammer_smt2_min_weight} (K 0) |
|
55 |
val smt2_max_weight = Attrib.setup_config_int @{binding sledgehammer_smt2_max_weight} (K 10) |
|
56 |
val smt2_max_weight_index = |
|
57 |
Attrib.setup_config_int @{binding sledgehammer_smt2_max_weight_index} (K 200) |
|
58 |
val smt2_weight_curve = Unsynchronized.ref (fn x : int => x * x) |
|
59 |
||
60 |
fun smt2_fact_weight ctxt j num_facts = |
|
61 |
if Config.get ctxt smt2_weights andalso num_facts >= Config.get ctxt smt2_weight_min_facts then |
|
62 |
let |
|
63 |
val min = Config.get ctxt smt2_min_weight |
|
64 |
val max = Config.get ctxt smt2_max_weight |
|
65 |
val max_index = Config.get ctxt smt2_max_weight_index |
|
66 |
val curve = !smt2_weight_curve |
|
67 |
in |
|
68 |
SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1)) div curve max_index) |
|
69 |
end |
|
70 |
else |
|
71 |
NONE |
|
72 |
||
73 |
fun weight_smt2_fact ctxt num_facts ((info, th), j) = |
|
56984 | 74 |
(info, (smt2_fact_weight ctxt j num_facts, th)) |
56081 | 75 |
|
76 |
(* "SMT2_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out |
|
77 |
properly in the SMT module, we must interpret these here. *) |
|
78 |
val z3_failures = |
|
79 |
[(101, OutOfResources), |
|
80 |
(103, MalformedInput), |
|
81 |
(110, MalformedInput), |
|
82 |
(112, TimedOut)] |
|
83 |
val unix_failures = |
|
84 |
[(138, Crashed), |
|
85 |
(139, Crashed)] |
|
86 |
val smt2_failures = z3_failures @ unix_failures |
|
87 |
||
57158 | 88 |
fun failure_of_smt2_failure (SMT2_Failure.Counterexample genuine) = |
89 |
if genuine then Unprovable else GaveUp |
|
56081 | 90 |
| failure_of_smt2_failure SMT2_Failure.Time_Out = TimedOut |
91 |
| failure_of_smt2_failure (SMT2_Failure.Abnormal_Termination code) = |
|
92 |
(case AList.lookup (op =) smt2_failures code of |
|
93 |
SOME failure => failure |
|
94 |
| NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ ".")) |
|
95 |
| failure_of_smt2_failure SMT2_Failure.Out_Of_Memory = OutOfResources |
|
96 |
| failure_of_smt2_failure (SMT2_Failure.Other_Failure s) = UnknownError s |
|
97 |
||
98 |
(* FUDGE *) |
|
99 |
val smt2_max_slices = Attrib.setup_config_int @{binding sledgehammer_smt2_max_slices} (K 8) |
|
100 |
val smt2_slice_fact_frac = |
|
101 |
Attrib.setup_config_real @{binding sledgehammer_smt2_slice_fact_frac} (K 0.667) |
|
102 |
val smt2_slice_time_frac = |
|
103 |
Attrib.setup_config_real @{binding sledgehammer_smt2_slice_time_frac} (K 0.333) |
|
104 |
val smt2_slice_min_secs = Attrib.setup_config_int @{binding sledgehammer_smt2_slice_min_secs} (K 3) |
|
105 |
||
106 |
val is_boring_builtin_typ = |
|
107 |
not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT]) |
|
108 |
||
109 |
fun smt2_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice, |
|
110 |
...} : params) state goal i = |
|
111 |
let |
|
112 |
fun repair_context ctxt = |
|
113 |
ctxt |> Context.proof_map (SMT2_Config.select_solver name) |
|
114 |
|> Config.put SMT2_Config.verbose debug |
|
115 |
|> (if overlord then |
|
116 |
Config.put SMT2_Config.debug_files |
|
117 |
(overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name)) |
|
118 |
else |
|
119 |
I) |
|
120 |
|> Config.put SMT2_Config.infer_triggers (Config.get ctxt smt2_triggers) |
|
121 |
|> not (Config.get ctxt smt2_builtins) |
|
122 |
? (SMT2_Builtin.filter_builtins is_boring_builtin_typ |
|
56090 | 123 |
#> Config.put SMT2_Systems.z3_extensions false) |
56081 | 124 |
|> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances |
125 |
default_max_new_mono_instances |
|
126 |
||
127 |
val state = Proof.map_context (repair_context) state |
|
128 |
val ctxt = Proof.context_of state |
|
129 |
val max_slices = if slice then Config.get ctxt smt2_max_slices else 1 |
|
130 |
||
131 |
fun do_slice timeout slice outcome0 time_so_far |
|
132 |
(weighted_factss as (fact_filter, weighted_facts) :: _) = |
|
133 |
let |
|
134 |
val timer = Timer.startRealTimer () |
|
135 |
val slice_timeout = |
|
136 |
if slice < max_slices then |
|
137 |
let val ms = Time.toMilliseconds timeout in |
|
138 |
Int.min (ms, Int.max (1000 * Config.get ctxt smt2_slice_min_secs, |
|
139 |
Real.ceil (Config.get ctxt smt2_slice_time_frac * Real.fromInt ms))) |
|
140 |
|> Time.fromMilliseconds |
|
141 |
end |
|
142 |
else |
|
143 |
timeout |
|
144 |
val num_facts = length weighted_facts |
|
145 |
val _ = |
|
146 |
if debug then |
|
147 |
quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^ |
|
148 |
" fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout |
|
149 |
|> Output.urgent_message |
|
150 |
else |
|
151 |
() |
|
152 |
val birth = Timer.checkRealTimer timer |
|
153 |
||
56104
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
56099
diff
changeset
|
154 |
val filter_result as {outcome, ...} = |
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
56099
diff
changeset
|
155 |
SMT2_Solver.smt2_filter ctxt goal weighted_facts i slice_timeout |
56081 | 156 |
handle exn => |
56094 | 157 |
if Exn.is_interrupt exn orelse debug then |
56083
b5d1d9c60341
have Sledgehammer generate Isar proofs from Z3 proofs
blanchet
parents:
56082
diff
changeset
|
158 |
reraise exn |
b5d1d9c60341
have Sledgehammer generate Isar proofs from Z3 proofs
blanchet
parents:
56082
diff
changeset
|
159 |
else |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56132
diff
changeset
|
160 |
{outcome = SOME (SMT2_Failure.Other_Failure (Runtime.exn_message exn)), |
57159 | 161 |
fact_ids = [], atp_proof = K []} |
56081 | 162 |
|
163 |
val death = Timer.checkRealTimer timer |
|
164 |
val outcome0 = if is_none outcome0 then SOME outcome else outcome0 |
|
165 |
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
|
166 |
val timeout = Time.- (timeout, Timer.checkRealTimer timer) |
56081 | 167 |
|
168 |
val too_many_facts_perhaps = |
|
169 |
(case outcome of |
|
170 |
NONE => false |
|
171 |
| SOME (SMT2_Failure.Counterexample _) => false |
|
172 |
| SOME SMT2_Failure.Time_Out => slice_timeout <> timeout |
|
173 |
| SOME (SMT2_Failure.Abnormal_Termination _) => true (* kind of *) |
|
174 |
| SOME SMT2_Failure.Out_Of_Memory => true |
|
175 |
| SOME (SMT2_Failure.Other_Failure _) => true) |
|
176 |
in |
|
177 |
if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso |
|
178 |
Time.> (timeout, Time.zeroTime) then |
|
179 |
let |
|
180 |
val new_num_facts = |
|
181 |
Real.ceil (Config.get ctxt smt2_slice_fact_frac * Real.fromInt num_facts) |
|
182 |
val weighted_factss as (new_fact_filter, _) :: _ = |
|
183 |
weighted_factss |
|
184 |
|> (fn (x :: xs) => xs @ [x]) |
|
185 |
|> app_hd (apsnd (take new_num_facts)) |
|
186 |
val show_filter = fact_filter <> new_fact_filter |
|
187 |
||
188 |
fun num_of_facts fact_filter num_facts = |
|
189 |
string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^ |
|
190 |
" fact" ^ plural_s num_facts |
|
191 |
||
192 |
val _ = |
|
193 |
if debug then |
|
194 |
quote name ^ " invoked with " ^ |
|
195 |
num_of_facts fact_filter num_facts ^ ": " ^ |
|
196 |
string_of_atp_failure (failure_of_smt2_failure (the outcome)) ^ |
|
197 |
" Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^ |
|
198 |
"..." |
|
199 |
|> Output.urgent_message |
|
200 |
else |
|
201 |
() |
|
202 |
in |
|
203 |
do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss |
|
204 |
end |
|
205 |
else |
|
56104
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
56099
diff
changeset
|
206 |
{outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result, |
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
56099
diff
changeset
|
207 |
used_from = map (apsnd snd) weighted_facts, run_time = time_so_far} |
56081 | 208 |
end |
209 |
in |
|
210 |
do_slice timeout 1 NONE Time.zeroTime |
|
211 |
end |
|
212 |
||
56083
b5d1d9c60341
have Sledgehammer generate Isar proofs from Z3 proofs
blanchet
parents:
56082
diff
changeset
|
213 |
fun run_smt2_solver mode name (params as {debug, verbose, isar_proofs, compress_isar, |
b5d1d9c60341
have Sledgehammer generate Isar proofs from Z3 proofs
blanchet
parents:
56082
diff
changeset
|
214 |
try0_isar, smt_proofs, minimize, preplay_timeout, ...}) |
56081 | 215 |
minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = |
216 |
let |
|
217 |
val thy = Proof.theory_of state |
|
218 |
val ctxt = Proof.context_of state |
|
219 |
||
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56981
diff
changeset
|
220 |
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56981
diff
changeset
|
221 |
|
56081 | 222 |
fun weight_facts facts = |
223 |
let val num_facts = length facts in |
|
224 |
map (weight_smt2_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1)) |
|
225 |
end |
|
226 |
||
56099 | 227 |
val weighted_factss = map (apsnd weight_facts) factss |
57159 | 228 |
val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} = |
56128 | 229 |
smt2_filter_loop name params state goal subgoal weighted_factss |
56104
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
56099
diff
changeset
|
230 |
val used_named_facts = map snd fact_ids |
56099 | 231 |
val used_facts = map fst used_named_facts |
232 |
val outcome = Option.map failure_of_smt2_failure outcome |
|
56081 | 233 |
|
234 |
val (preplay, message, message_tail) = |
|
235 |
(case outcome of |
|
236 |
NONE => |
|
237 |
(Lazy.lazy (fn () => |
|
57054 | 238 |
play_one_line_proof mode verbose preplay_timeout used_named_facts state subgoal |
56081 | 239 |
SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)), |
240 |
fn preplay => |
|
241 |
let |
|
57056 | 242 |
fun isar_params () = |
57159 | 243 |
(verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar, |
244 |
minimize <> SOME false, atp_proof (), goal) |
|
57056 | 245 |
|
56081 | 246 |
val one_line_params = |
247 |
(preplay, proof_banner mode name, used_facts, |
|
248 |
choose_minimize_command thy params minimize_command name preplay, subgoal, |
|
249 |
subgoal_count) |
|
250 |
val num_chained = length (#facts (Proof.goal state)) |
|
251 |
in |
|
56083
b5d1d9c60341
have Sledgehammer generate Isar proofs from Z3 proofs
blanchet
parents:
56082
diff
changeset
|
252 |
proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params |
56081 | 253 |
end, |
254 |
if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "") |
|
255 |
| SOME failure => |
|
256 |
(Lazy.value (Metis_Method (NONE, NONE), Play_Failed), |
|
257 |
fn _ => string_of_atp_failure failure, "")) |
|
258 |
in |
|
259 |
{outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time, |
|
260 |
preplay = preplay, message = message, message_tail = message_tail} |
|
261 |
end |
|
262 |
||
263 |
end; |