get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)
1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_run.ML
2 Author: Fabian Immler, TU Muenchen
4 Author: Jasmin Blanchette, TU Muenchen
9 signature SLEDGEHAMMER_RUN =
11 type minimize_command = ATP_Proof_Reconstruct.minimize_command
12 type relevance_override = Sledgehammer_Filter.relevance_override
13 type mode = Sledgehammer_Provers.mode
14 type params = Sledgehammer_Provers.params
15 type prover = Sledgehammer_Provers.prover
21 val auto_minimize_min_facts : int Config.T
22 val auto_minimize_max_time : real Config.T
23 val get_minimizing_prover : Proof.context -> mode -> string -> prover
24 val run_sledgehammer :
25 params -> mode -> int -> relevance_override
26 -> ((string * string list) list -> string -> minimize_command)
27 -> Proof.state -> bool * (string * Proof.state)
30 structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
34 open ATP_Problem_Generate
35 open ATP_Proof_Reconstruct
36 open Sledgehammer_Util
37 open Sledgehammer_Filter
38 open Sledgehammer_Provers
39 open Sledgehammer_Minimize
43 val timeoutN = "timeout"
44 val unknownN = "unknown"
46 val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN]
48 fun max_outcome_code codes =
50 |> fold (fn candidate =>
51 fn accum as SOME _ => accum
52 | NONE => if member (op =) codes candidate then SOME candidate
55 |> the_default unknownN
57 fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
61 " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
64 " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
66 else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
68 val auto_minimize_min_facts =
69 Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
70 (fn generic => Config.get_generic generic binary_min_facts)
71 val auto_minimize_max_time =
72 Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
75 fun adjust_reconstructor_params override_params
76 ({debug, verbose, overlord, blocking, provers, type_enc, strict,
77 lam_trans, uncurried_aliases, relevance_thresholds, max_relevant,
78 max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor,
79 slice, minimize, timeout, preplay_timeout, expect} : params) =
81 fun lookup_override name default_value =
82 case AList.lookup (op =) override_params name of
85 (* Only those options that reconstructors are interested in are considered
87 val type_enc = lookup_override "type_enc" type_enc
88 val lam_trans = lookup_override "lam_trans" lam_trans
90 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
91 provers = provers, type_enc = type_enc, strict = strict,
92 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
93 max_relevant = max_relevant, relevance_thresholds = relevance_thresholds,
94 max_mono_iters = max_mono_iters,
95 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
96 isar_shrink_factor = isar_shrink_factor, slice = slice,
97 minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
101 fun minimize ctxt mode name
102 (params as {debug, verbose, isar_proof, minimize, ...})
103 ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
104 (result as {outcome, used_facts, run_time, preplay, message,
105 message_tail} : prover_result) =
106 if is_some outcome orelse null used_facts then
110 val num_facts = length used_facts
111 val ((perhaps_minimize, (minimize_name, params)), preplay) =
112 if mode = Normal then
113 if num_facts >= Config.get ctxt auto_minimize_min_facts then
114 ((true, (name, params)), preplay)
117 fun can_min_fast_enough time =
119 * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
120 <= Config.get ctxt auto_minimize_max_time
121 fun prover_fast_enough () = can_min_fast_enough run_time
124 ((prover_fast_enough (), (name, params)), preplay)
126 let val preplay = preplay () in
128 Played (reconstr, timeout) =>
129 if can_min_fast_enough timeout then
130 (true, extract_reconstructor params reconstr
131 ||> (fn override_params =>
132 adjust_reconstructor_params
133 override_params params))
135 (prover_fast_enough (), (name, params))
136 | _ => (prover_fast_enough (), (name, params)),
141 ((false, (name, params)), preplay)
142 val minimize = minimize |> the_default perhaps_minimize
143 val (used_facts, (preplay, message, _)) =
145 minimize_facts minimize_name params (not verbose) subgoal
147 (filter_used_facts used_facts
148 (map (apsnd single o untranslated_fact) facts))
149 |>> Option.map (map fst)
151 (SOME used_facts, (preplay, message, ""))
155 (if debug andalso not (null used_facts) then
156 facts ~~ (0 upto length facts - 1)
157 |> map (fn (fact, j) => fact |> untranslated_fact |> apsnd (K j))
158 |> filter_used_facts used_facts
159 |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
161 |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
162 " proof (of " ^ string_of_int (length facts) ^ "): ") "."
163 |> Output.urgent_message
166 {outcome = NONE, used_facts = used_facts, run_time = run_time,
167 preplay = preplay, message = message, message_tail = message_tail})
171 fun get_minimizing_prover ctxt mode name params minimize_command problem =
172 get_prover ctxt mode name params minimize_command problem
173 |> minimize ctxt mode name params problem
175 fun is_induction_fact (Untranslated_Fact ((_, (_, Induction)), _)) = true
176 | is_induction_fact _ = false
178 fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,
179 timeout, expect, ...})
180 mode minimize_command only {state, goal, subgoal, subgoal_count, facts}
183 val ctxt = Proof.context_of state
184 val hard_timeout = Time.+ (timeout, timeout)
185 val birth_time = Time.now ()
186 val death_time = Time.+ (birth_time, hard_timeout)
189 |> the_default (default_max_relevant_for_prover ctxt slice name)
190 val num_facts = length facts |> not only ? Integer.min max_relevant
192 prover_description ctxt params name num_facts subgoal subgoal_count goal
195 val filter_induction = filter_out is_induction_fact
196 in {state = state, goal = goal, subgoal = subgoal,
197 subgoal_count = subgoal_count, facts =
198 ((Sledgehammer_Provers.is_ho_atp ctxt name |> not) ? filter_induction)
204 |> get_minimizing_prover ctxt mode name params minimize_command
205 |> (fn {outcome, preplay, message, message_tail, ...} =>
206 (if outcome = SOME ATP_Proof.TimedOut then timeoutN
207 else if is_some outcome then noneN
208 else someN, fn () => message (preplay ()) ^ message_tail))
211 val (outcome_code, message) =
216 handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
218 if Exn.is_interrupt exn then
221 (unknownN, fn () => "Internal error:\n" ^
222 ML_Compiler.exn_message exn ^ "\n"))
224 (* The "expect" argument is deliberately ignored if the prover is
225 missing so that the "Metis_Examples" can be processed on any
227 if expect = "" orelse outcome_code = expect orelse
228 not (is_prover_installed ctxt name) then
230 else if blocking then
231 error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
233 warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
234 in (outcome_code, message) end
236 if mode = Auto_Try then
237 let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
240 |> outcome_code = someN
241 ? Proof.goal_message (fn () =>
243 Pretty.mark Isabelle_Markup.hilite (Pretty.str (message ()))]
246 else if blocking then
248 val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
250 (if outcome_code = someN orelse mode = Normal then
251 quote name ^ ": " ^ message ()
254 |> Async_Manager.break_into_chunks
255 |> List.app Output.urgent_message;
256 (outcome_code, state)
259 (Async_Manager.launch das_tool birth_time death_time (desc ())
260 ((fn (outcome_code, message) =>
261 (verbose orelse outcome_code = someN,
266 fun class_of_smt_solver ctxt name =
267 ctxt |> select_smt_solver name
268 |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
270 val auto_try_max_relevant_divisor = 2 (* FUDGE *)
272 fun run_sledgehammer (params as {debug, verbose, blocking, provers,
273 relevance_thresholds, max_relevant, slice,
275 mode i (relevance_override as {only, ...}) minimize_command state =
277 error "No prover is set."
278 else case subgoal_count state of
279 0 => (Output.urgent_message "No subgoal!"; (false, (noneN, state)))
282 val _ = Proof.assert_backward state
283 val print = if mode = Normal then Output.urgent_message else K ()
285 state |> Proof.map_context (Config.put SMT_Config.verbose debug)
286 val ctxt = Proof.context_of state
287 val {facts = chained_ths, goal, ...} = Proof.goal state
288 val chained_ths = chained_ths |> normalize_chained_theorems
289 val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
290 val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
292 nearly_all_facts ctxt ho_atp relevance_override chained_ths hyp_ts
294 val _ = () |> not blocking ? kill_provers
295 val _ = case find_first (not o is_prover_supported ctxt) provers of
296 SOME name => error ("No such prover: " ^ name ^ ".")
298 val _ = print "Sledgehammering..."
299 val (smts, (ueq_atps, full_atps)) =
300 provers |> List.partition (is_smt_prover ctxt)
301 ||> List.partition (is_unit_equational_atp ctxt)
302 fun launch_provers state get_facts translate provers =
304 val facts = get_facts ()
305 val num_facts = length facts
306 val facts = facts ~~ (0 upto num_facts - 1)
307 |> map (translate num_facts)
309 {state = state, goal = goal, subgoal = i, subgoal_count = n,
311 val launch = launch_prover params mode minimize_command only
313 if mode = Auto_Try orelse mode = Try then
315 |> fold (fn prover => fn accum as (outcome_code, _) =>
316 if outcome_code = someN then accum
317 else launch problem prover)
321 |> (if blocking then Par_List.map else map)
322 (launch problem #> fst)
323 |> max_outcome_code |> rpair state
325 fun get_facts label is_appropriate_prop relevance_fudge provers =
327 val max_max_relevant =
331 0 |> fold (Integer.max
332 o default_max_relevant_for_prover ctxt slice)
335 ? (fn n => n div auto_try_max_relevant_divisor)
336 val is_built_in_const =
337 is_built_in_const_for_prover ctxt (hd provers)
340 |> (case is_appropriate_prop of
341 SOME is_app => filter (is_app o prop_of o snd)
343 |> relevant_facts ctxt relevance_thresholds max_max_relevant
344 is_built_in_const relevance_fudge relevance_override
345 chained_ths hyp_ts concl_t
348 label ^ plural_s (length provers) ^ ": " ^
350 "Found no relevant facts."
352 "Including (up to) " ^ string_of_int (length facts) ^
353 " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
354 (facts |> map (fst o fst) |> space_implode " ") ^ ".")
359 fun launch_atps label is_appropriate_prop atps accum =
362 else if is_some is_appropriate_prop andalso
363 not (the is_appropriate_prop concl_t) then
364 (if verbose orelse length atps = length provers then
365 "Goal outside the scope of " ^
366 space_implode " " (serial_commas "and" (map quote atps)) ^ "."
367 |> Output.urgent_message
373 (get_facts label is_appropriate_prop atp_relevance_fudge o K atps)
374 (K (Untranslated_Fact o fst)) atps
375 fun launch_smts accum =
380 val facts = get_facts "SMT solver" NONE smt_relevance_fudge smts
381 val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt
383 smts |> map (`(class_of_smt_solver ctxt))
384 |> AList.group (op =)
385 |> map (snd #> launch_provers state (K facts) weight #> fst)
386 |> max_outcome_code |> rpair state
388 val launch_full_atps = launch_atps "ATP" NONE full_atps
389 val launch_ueq_atps =
390 launch_atps "Unit equational provers" (SOME is_unit_equality) ueq_atps
391 fun launch_atps_and_smt_solvers () =
392 [launch_full_atps, launch_smts, launch_ueq_atps]
393 |> Par_List.map (fn f => ignore (f (unknownN, state)))
394 handle ERROR msg => (print ("Error: " ^ msg); error msg)
395 fun maybe f (accum as (outcome_code, _)) =
396 accum |> (mode = Normal orelse outcome_code <> someN) ? f
401 #> mode <> Auto_Try ? (maybe launch_ueq_atps #> maybe launch_smts)
403 (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
404 handle TimeLimit.TimeOut =>
405 (print "Sledgehammer ran out of time."; (unknownN, state))
407 |> `(fn (outcome_code, _) => outcome_code = someN)