1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
2 Author: Philipp Meyer, TU Muenchen
3 Author: Jasmin Blanchette, TU Muenchen
5 Minimization of fact list for Metis using external provers.
8 signature SLEDGEHAMMER_MINIMIZE =
10 type stature = ATP_Problem_Generate.stature
11 type play = ATP_Proof_Reconstruct.play
12 type mode = Sledgehammer_Provers.mode
13 type params = Sledgehammer_Provers.params
14 type prover = Sledgehammer_Provers.prover
16 val binary_min_facts : int Config.T
17 val auto_minimize_min_facts : int Config.T
18 val auto_minimize_max_time : real Config.T
20 (thm list -> unit) -> string -> params -> bool -> int -> int -> Proof.state
21 -> ((string * stature) * thm list) list
22 -> ((string * stature) * thm list) list option
23 * ((unit -> play) * (play -> string) * string)
24 val get_minimizing_prover :
25 Proof.context -> mode -> (thm list -> unit) -> string -> prover
27 params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list
28 -> Proof.state -> unit
31 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
36 open ATP_Problem_Generate
37 open ATP_Proof_Reconstruct
38 open Sledgehammer_Util
39 open Sledgehammer_Fact
40 open Sledgehammer_Provers
42 (* wrapper for calling external prover *)
45 let val n = length names in
46 string_of_int n ^ " fact" ^ plural_s n ^
48 ": " ^ (names |> map fst |> sort string_ord |> space_implode " ")
53 fun print silent f = if silent then () else Output.urgent_message (f ())
55 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
56 max_new_mono_instances, type_enc, strict, lam_trans,
57 uncurried_aliases, isar_proof, isar_shrink_factor,
58 preplay_timeout, ...} : params)
59 silent (prover : prover) timeout i n state facts =
62 print silent (fn () =>
63 "Testing " ^ n_facts (map fst facts) ^
64 (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
66 val {goal, ...} = Proof.goal state
68 facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
70 {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
71 provers = provers, type_enc = type_enc, strict = strict,
72 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
73 learn = false, fact_filter = NONE, max_facts = SOME (length facts),
74 fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
75 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
76 isar_shrink_factor = isar_shrink_factor, slice = false,
77 minimize = SOME false, timeout = timeout,
78 preplay_timeout = preplay_timeout, expect = ""}
80 {state = state, goal = goal, subgoal = i, subgoal_count = n,
82 val result as {outcome, used_facts, run_time, ...} =
83 prover params (K (K (K ""))) problem
88 SOME failure => string_for_failure failure
91 (if length used_facts = length facts then ""
92 else " with " ^ n_facts used_facts) ^
93 " (" ^ string_from_time run_time ^ ").");
97 (* minimalization of facts *)
99 (* Give the external prover some slack. The ATP gets further slack because the
100 Sledgehammer preprocessing time is included in the estimate below but isn't
101 part of the timeout. *)
102 val slack_msecs = 200
104 fun new_timeout timeout run_time =
105 Int.min (Time.toMilliseconds timeout,
106 Time.toMilliseconds run_time + slack_msecs)
107 |> Time.fromMilliseconds
109 (* The linear algorithm usually outperforms the binary algorithm when over 60%
110 of the facts are actually needed. The binary algorithm is much more
111 appropriate for provers that cannot return the list of used facts and hence
112 returns all facts as used. Since we cannot know in advance how many facts are
113 actually needed, we heuristically set the threshold to 10 facts. *)
114 val binary_min_facts =
115 Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
117 val auto_minimize_min_facts =
118 Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
119 (fn generic => Config.get_generic generic binary_min_facts)
120 val auto_minimize_max_time =
121 Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
124 fun linear_minimize test timeout result xs =
127 | min timeout (x :: xs) (seen, result) =
128 case test timeout (xs @ seen) of
129 result as {outcome = NONE, used_facts, run_time, ...}
131 min (new_timeout timeout run_time) (filter_used_facts used_facts xs)
132 (filter_used_facts used_facts seen, result)
133 | _ => min timeout xs (x :: seen, result)
134 in min timeout xs ([], result) end
136 fun binary_minimize test timeout result xs =
138 fun min depth (result as {run_time, ...} : prover_result) sup
139 (xs as _ :: _ :: _) =
141 val (l0, r0) = chop (length xs div 2) xs
143 val _ = warning (replicate_string depth " " ^ "{ " ^
144 "sup: " ^ n_facts (map fst sup))
145 val _ = warning (replicate_string depth " " ^ " " ^
146 "xs: " ^ n_facts (map fst xs))
147 val _ = warning (replicate_string depth " " ^ " " ^
148 "l0: " ^ n_facts (map fst l0))
149 val _ = warning (replicate_string depth " " ^ " " ^
150 "r0: " ^ n_facts (map fst r0))
152 val depth = depth + 1
153 val timeout = new_timeout timeout run_time
155 case test timeout (sup @ l0) of
156 result as {outcome = NONE, used_facts, ...} =>
157 min depth result (filter_used_facts used_facts sup)
158 (filter_used_facts used_facts l0)
160 case test timeout (sup @ r0) of
161 result as {outcome = NONE, used_facts, ...} =>
162 min depth result (filter_used_facts used_facts sup)
163 (filter_used_facts used_facts r0)
166 val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
168 (sup, r0) |> pairself (filter_used_facts (map fst sup_r0))
169 val (sup_l, (r, result)) = min depth result (sup @ l) r0
170 val sup = sup |> filter_used_facts (map fst sup_l)
171 in (sup, (l @ r, result)) end
174 |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
176 | min _ result sup xs = (sup, (xs, result))
178 case snd (min 0 result [] xs) of
179 ([x], result as {run_time, ...}) =>
180 (case test (new_timeout timeout run_time) [] of
181 result as {outcome = NONE, ...} => ([], result)
182 | _ => ([x], result))
186 fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent
189 val ctxt = Proof.context_of state
191 get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
192 val _ = print silent (fn () => "Sledgehammer minimizer: " ^
193 quote prover_name ^ ".")
194 fun test timeout = test_facts params silent prover timeout i n state
196 (case test timeout facts of
197 result as {outcome = NONE, used_facts, run_time, ...} =>
199 val facts = filter_used_facts used_facts facts
201 if length facts >= Config.get ctxt binary_min_facts then
205 val (min_facts, {preplay, message, message_tail, ...}) =
206 min test (new_timeout timeout run_time) result facts
208 print silent (fn () => cat_lines
209 ["Minimized to " ^ n_facts (map fst min_facts)] ^
210 (case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained)
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))
217 | {outcome = SOME TimedOut, preplay, ...} =>
220 fn _ => "Timeout: You can increase the time limit using the \
221 \\"timeout\" option (e.g., \"timeout = " ^
222 string_of_int (10 + Time.toMilliseconds timeout div 1000) ^
225 | {preplay, message, ...} =>
226 (NONE, (preplay, prefix "Prover error: " o message, "")))
228 (NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, ""))
231 fun adjust_reconstructor_params override_params
232 ({debug, verbose, overlord, blocking, provers, type_enc, strict,
233 lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
234 fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proof,
235 isar_shrink_factor, slice, minimize, timeout, preplay_timeout, expect}
238 fun lookup_override name default_value =
239 case AList.lookup (op =) override_params name of
242 (* Only those options that reconstructors are interested in are considered
244 val type_enc = lookup_override "type_enc" type_enc
245 val lam_trans = lookup_override "lam_trans" lam_trans
247 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
248 provers = provers, type_enc = type_enc, strict = strict,
249 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
250 learn = learn, fact_filter = fact_filter, max_facts = max_facts,
251 fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
252 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
253 isar_shrink_factor = isar_shrink_factor, slice = slice,
254 minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
258 fun maybe_minimize ctxt mode do_learn name
259 (params as {debug, verbose, isar_proof, minimize, ...})
260 ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
261 (result as {outcome, used_facts, run_time, preplay, message,
262 message_tail} : prover_result) =
263 if is_some outcome orelse null used_facts then
267 val num_facts = length used_facts
268 val ((perhaps_minimize, (minimize_name, params)), preplay) =
269 if mode = Normal then
270 if num_facts >= Config.get ctxt auto_minimize_min_facts then
271 ((true, (name, params)), preplay)
274 fun can_min_fast_enough time =
276 * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
277 <= Config.get ctxt auto_minimize_max_time
278 fun prover_fast_enough () = can_min_fast_enough run_time
281 ((prover_fast_enough (), (name, params)), preplay)
283 let val preplay = preplay () in
285 Played (reconstr, timeout) =>
286 if can_min_fast_enough timeout then
287 (true, extract_reconstructor params reconstr
288 ||> (fn override_params =>
289 adjust_reconstructor_params
290 override_params params))
292 (prover_fast_enough (), (name, params))
293 | _ => (prover_fast_enough (), (name, params)),
298 ((false, (name, params)), preplay)
299 val minimize = minimize |> the_default perhaps_minimize
300 val (used_facts, (preplay, message, _)) =
302 minimize_facts do_learn minimize_name params
303 (mode <> Normal orelse not verbose) subgoal
305 (filter_used_facts used_facts
306 (map (apsnd single o untranslated_fact) facts))
307 |>> Option.map (map fst)
309 (SOME used_facts, (preplay, message, ""))
313 (if debug andalso not (null used_facts) then
315 |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
316 |> filter_used_facts used_facts
317 |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
319 |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
320 " proof (of " ^ string_of_int (length facts) ^ "): ") "."
321 |> Output.urgent_message
324 {outcome = NONE, used_facts = used_facts, run_time = run_time,
325 preplay = preplay, message = message, message_tail = message_tail})
329 fun get_minimizing_prover ctxt mode do_learn name params minimize_command
331 get_prover ctxt mode name params minimize_command problem
332 |> maybe_minimize ctxt mode do_learn name params problem
334 fun run_minimize (params as {provers, ...}) do_learn i refs state =
336 val ctxt = Proof.context_of state
337 val reserved = reserved_isar_keyword_table ()
338 val chained_ths = #facts (Proof.goal state)
339 val css_table = clasimpset_rule_table_of ctxt
341 refs |> maps (map (apsnd single)
342 o fact_from_ref ctxt reserved chained_ths css_table)
344 case subgoal_count state of
345 0 => Output.urgent_message "No subgoal!"
346 | n => case provers of
347 [] => error "No prover is set."
350 minimize_facts do_learn prover params false i n state facts
351 |> (fn (_, (preplay, message, message_tail)) =>
352 message (preplay ()) ^ message_tail
353 |> Output.urgent_message))