15 |
15 |
16 val binary_min_facts : int Config.T |
16 val binary_min_facts : int Config.T |
17 val auto_minimize_min_facts : int Config.T |
17 val auto_minimize_min_facts : int Config.T |
18 val auto_minimize_max_time : real Config.T |
18 val auto_minimize_max_time : real Config.T |
19 val minimize_facts : |
19 val minimize_facts : |
20 string -> params -> bool -> int -> int -> Proof.state |
20 (thm list -> unit) -> string -> params -> bool -> int -> int -> Proof.state |
21 -> ((string * stature) * thm list) list |
21 -> ((string * stature) * thm list) list |
22 -> ((string * stature) * thm list) list option |
22 -> ((string * stature) * thm list) list option |
23 * ((unit -> play) * (play -> string) * string) |
23 * ((unit -> play) * (play -> string) * string) |
24 val get_minimizing_prover : Proof.context -> mode -> string -> prover |
24 val get_minimizing_prover : |
|
25 Proof.context -> mode -> (thm list -> unit) -> string -> prover |
25 val run_minimize : |
26 val run_minimize : |
26 params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit |
27 params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list |
|
28 -> Proof.state -> unit |
27 end; |
29 end; |
28 |
30 |
29 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE = |
31 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE = |
30 struct |
32 struct |
31 |
33 |
66 facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) |
68 facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) |
67 val params = |
69 val params = |
68 {debug = debug, verbose = verbose, overlord = overlord, blocking = true, |
70 {debug = debug, verbose = verbose, overlord = overlord, blocking = true, |
69 provers = provers, type_enc = type_enc, strict = strict, |
71 provers = provers, type_enc = type_enc, strict = strict, |
70 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, |
72 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, |
71 fact_filter = NONE, max_facts = SOME (length facts), |
73 learn = false, fact_filter = NONE, max_facts = SOME (length facts), |
72 fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, |
74 fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, |
73 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
75 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
74 isar_shrink_factor = isar_shrink_factor, slice = false, |
76 isar_shrink_factor = isar_shrink_factor, slice = false, |
75 minimize = SOME false, timeout = timeout, |
77 minimize = SOME false, timeout = timeout, |
76 preplay_timeout = preplay_timeout, expect = ""} |
78 preplay_timeout = preplay_timeout, expect = ""} |
179 result as {outcome = NONE, ...} => ([], result) |
181 result as {outcome = NONE, ...} => ([], result) |
180 | _ => ([x], result)) |
182 | _ => ([x], result)) |
181 | p => p |
183 | p => p |
182 end |
184 end |
183 |
185 |
184 fun minimize_facts prover_name (params as {timeout, ...}) silent i n state |
186 fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent |
185 facts = |
187 i n state facts = |
186 let |
188 let |
187 val ctxt = Proof.context_of state |
189 val ctxt = Proof.context_of state |
188 val prover = |
190 val prover = |
189 get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name |
191 get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name |
190 val _ = print silent (fn () => "Sledgehammer minimizer: " ^ |
192 val _ = print silent (fn () => "Sledgehammer minimizer: " ^ |
200 binary_minimize |
202 binary_minimize |
201 else |
203 else |
202 linear_minimize |
204 linear_minimize |
203 val (min_facts, {preplay, message, message_tail, ...}) = |
205 val (min_facts, {preplay, message, message_tail, ...}) = |
204 min test (new_timeout timeout run_time) result facts |
206 min test (new_timeout timeout run_time) result facts |
205 val _ = print silent (fn () => cat_lines |
207 in |
206 ["Minimized to " ^ n_facts (map fst min_facts)] ^ |
208 print silent (fn () => cat_lines |
207 (case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained) |
209 ["Minimized to " ^ n_facts (map fst min_facts)] ^ |
208 |> length of |
210 (case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained) |
209 0 => "" |
211 |> length of |
210 | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".") |
212 0 => "" |
211 in (SOME min_facts, (preplay, message, message_tail)) end |
213 | n => "\n(including " ^ string_of_int n ^ " chained)") ^ "."); |
|
214 (if learn then do_learn (maps snd min_facts) else ()); |
|
215 (SOME min_facts, (preplay, message, message_tail)) |
|
216 end |
212 | {outcome = SOME TimedOut, preplay, ...} => |
217 | {outcome = SOME TimedOut, preplay, ...} => |
213 (NONE, |
218 (NONE, |
214 (preplay, |
219 (preplay, |
215 fn _ => "Timeout: You can increase the time limit using the \ |
220 fn _ => "Timeout: You can increase the time limit using the \ |
216 \\"timeout\" option (e.g., \"timeout = " ^ |
221 \\"timeout\" option (e.g., \"timeout = " ^ |
223 (NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, "")) |
228 (NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, "")) |
224 end |
229 end |
225 |
230 |
226 fun adjust_reconstructor_params override_params |
231 fun adjust_reconstructor_params override_params |
227 ({debug, verbose, overlord, blocking, provers, type_enc, strict, |
232 ({debug, verbose, overlord, blocking, provers, type_enc, strict, |
228 lam_trans, uncurried_aliases, fact_filter, max_facts, fact_thresholds, |
233 lam_trans, uncurried_aliases, learn, fact_filter, max_facts, |
229 max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor, |
234 fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proof, |
230 slice, minimize, timeout, preplay_timeout, expect} : params) = |
235 isar_shrink_factor, slice, minimize, timeout, preplay_timeout, expect} |
|
236 : params) = |
231 let |
237 let |
232 fun lookup_override name default_value = |
238 fun lookup_override name default_value = |
233 case AList.lookup (op =) override_params name of |
239 case AList.lookup (op =) override_params name of |
234 SOME [s] => SOME s |
240 SOME [s] => SOME s |
235 | _ => default_value |
241 | _ => default_value |
239 val lam_trans = lookup_override "lam_trans" lam_trans |
245 val lam_trans = lookup_override "lam_trans" lam_trans |
240 in |
246 in |
241 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, |
247 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, |
242 provers = provers, type_enc = type_enc, strict = strict, |
248 provers = provers, type_enc = type_enc, strict = strict, |
243 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, |
249 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, |
244 fact_filter = fact_filter, max_facts = max_facts, |
250 learn = learn, fact_filter = fact_filter, max_facts = max_facts, |
245 fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, |
251 fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, |
246 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
252 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
247 isar_shrink_factor = isar_shrink_factor, slice = slice, |
253 isar_shrink_factor = isar_shrink_factor, slice = slice, |
248 minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
254 minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
249 expect = expect} |
255 expect = expect} |
250 end |
256 end |
251 |
257 |
252 fun minimize ctxt mode name |
258 fun minimize ctxt mode do_learn name |
253 (params as {debug, verbose, isar_proof, minimize, ...}) |
259 (params as {debug, verbose, isar_proof, minimize, ...}) |
254 ({state, subgoal, subgoal_count, facts, ...} : prover_problem) |
260 ({state, subgoal, subgoal_count, facts, ...} : prover_problem) |
255 (result as {outcome, used_facts, run_time, preplay, message, |
261 (result as {outcome, used_facts, run_time, preplay, message, |
256 message_tail} : prover_result) = |
262 message_tail} : prover_result) = |
257 if is_some outcome orelse null used_facts then |
263 if is_some outcome orelse null used_facts then |
291 else |
297 else |
292 ((false, (name, params)), preplay) |
298 ((false, (name, params)), preplay) |
293 val minimize = minimize |> the_default perhaps_minimize |
299 val minimize = minimize |> the_default perhaps_minimize |
294 val (used_facts, (preplay, message, _)) = |
300 val (used_facts, (preplay, message, _)) = |
295 if minimize then |
301 if minimize then |
296 minimize_facts minimize_name params (not verbose) subgoal |
302 minimize_facts do_learn minimize_name params (not verbose) subgoal |
297 subgoal_count state |
303 subgoal_count state |
298 (filter_used_facts used_facts |
304 (filter_used_facts used_facts |
299 (map (apsnd single o untranslated_fact) facts)) |
305 (map (apsnd single o untranslated_fact) facts)) |
300 |>> Option.map (map fst) |
306 |>> Option.map (map fst) |
301 else |
307 else |
317 {outcome = NONE, used_facts = used_facts, run_time = run_time, |
323 {outcome = NONE, used_facts = used_facts, run_time = run_time, |
318 preplay = preplay, message = message, message_tail = message_tail}) |
324 preplay = preplay, message = message, message_tail = message_tail}) |
319 | NONE => result |
325 | NONE => result |
320 end |
326 end |
321 |
327 |
322 fun get_minimizing_prover ctxt mode name params minimize_command problem = |
328 fun get_minimizing_prover ctxt mode do_learn name params minimize_command |
|
329 problem = |
323 get_prover ctxt mode name params minimize_command problem |
330 get_prover ctxt mode name params minimize_command problem |
324 |> minimize ctxt mode name params problem |
331 |> minimize ctxt mode do_learn name params problem |
325 |
332 |
326 fun run_minimize (params as {provers, ...}) i refs state = |
333 fun run_minimize (params as {provers, ...}) do_learn i refs state = |
327 let |
334 let |
328 val ctxt = Proof.context_of state |
335 val ctxt = Proof.context_of state |
329 val reserved = reserved_isar_keyword_table () |
336 val reserved = reserved_isar_keyword_table () |
330 val chained_ths = #facts (Proof.goal state) |
337 val chained_ths = #facts (Proof.goal state) |
331 val css_table = clasimpset_rule_table_of ctxt |
338 val css_table = clasimpset_rule_table_of ctxt |
337 0 => Output.urgent_message "No subgoal!" |
344 0 => Output.urgent_message "No subgoal!" |
338 | n => case provers of |
345 | n => case provers of |
339 [] => error "No prover is set." |
346 [] => error "No prover is set." |
340 | prover :: _ => |
347 | prover :: _ => |
341 (kill_provers (); |
348 (kill_provers (); |
342 minimize_facts prover params false i n state facts |
349 minimize_facts do_learn prover params false i n state facts |
343 |> (fn (_, (preplay, message, message_tail)) => |
350 |> (fn (_, (preplay, message, message_tail)) => |
344 message (preplay ()) ^ message_tail |
351 message (preplay ()) ^ message_tail |
345 |> Output.urgent_message)) |
352 |> Output.urgent_message)) |
346 end |
353 end |
347 |
354 |