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 locality = ATP_Translate.locality
11 type play = ATP_Reconstruct.play
12 type params = Sledgehammer_Provers.params
14 val binary_min_facts : int Config.T
16 string -> params -> bool -> int -> int -> Proof.state
17 -> ((string * locality) * thm list) list
18 -> ((string * locality) * thm list) list option
19 * ((unit -> play) * (play -> string) * string)
21 params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
24 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
31 open Sledgehammer_Util
32 open Sledgehammer_Filter
33 open Sledgehammer_Provers
35 (* wrapper for calling external prover *)
38 let val n = length names in
39 string_of_int n ^ " fact" ^ plural_s n ^
41 ": " ^ (names |> map fst |> sort_distinct string_ord
47 fun print silent f = if silent then () else Output.urgent_message (f ())
49 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
50 max_new_mono_instances, type_enc, lam_trans, isar_proof,
51 isar_shrink_factor, preplay_timeout, ...} : params)
52 silent (prover : prover) timeout i n state facts =
55 print silent (fn () =>
56 "Testing " ^ n_facts (map fst facts) ^
57 (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
59 val {goal, ...} = Proof.goal state
61 facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
63 {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
64 provers = provers, type_enc = type_enc, sound = true,
65 lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01),
66 max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
67 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
68 isar_shrink_factor = isar_shrink_factor, slicing = false,
69 timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
71 {state = state, goal = goal, subgoal = i, subgoal_count = n,
72 facts = facts, smt_filter = NONE}
73 val result as {outcome, used_facts, run_time, ...} =
74 prover params (K (K (K ""))) problem
79 SOME failure => string_for_failure failure
82 (if length used_facts = length facts then ""
83 else " with " ^ n_facts used_facts) ^
84 " (" ^ string_from_time run_time ^ ").");
88 (* minimalization of facts *)
90 (* Give the external prover some slack. The ATP gets further slack because the
91 Sledgehammer preprocessing time is included in the estimate below but isn't
92 part of the timeout. *)
95 fun new_timeout timeout run_time =
96 Int.min (Time.toMilliseconds timeout,
97 Time.toMilliseconds run_time + slack_msecs)
98 |> Time.fromMilliseconds
100 (* The linear algorithm usually outperforms the binary algorithm when over 60%
101 of the facts are actually needed. The binary algorithm is much more
102 appropriate for provers that cannot return the list of used facts and hence
103 returns all facts as used. Since we cannot know in advance how many facts are
104 actually needed, we heuristically set the threshold to 10 facts. *)
105 val binary_min_facts =
106 Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
109 fun linear_minimize test timeout result xs =
112 | min timeout (x :: xs) (seen, result) =
113 case test timeout (xs @ seen) of
114 result as {outcome = NONE, used_facts, run_time, ...}
116 min (new_timeout timeout run_time) (filter_used_facts used_facts xs)
117 (filter_used_facts used_facts seen, result)
118 | _ => min timeout xs (x :: seen, result)
119 in min timeout xs ([], result) end
121 fun binary_minimize test timeout result xs =
123 fun min depth (result as {run_time, ...} : prover_result) sup
124 (xs as _ :: _ :: _) =
126 val (l0, r0) = chop (length xs div 2) xs
128 val _ = warning (replicate_string depth " " ^ "{ " ^
129 "sup: " ^ n_facts (map fst sup))
130 val _ = warning (replicate_string depth " " ^ " " ^
131 "xs: " ^ n_facts (map fst xs))
132 val _ = warning (replicate_string depth " " ^ " " ^
133 "l0: " ^ n_facts (map fst l0))
134 val _ = warning (replicate_string depth " " ^ " " ^
135 "r0: " ^ n_facts (map fst r0))
137 val depth = depth + 1
138 val timeout = new_timeout timeout run_time
140 case test timeout (sup @ l0) of
141 result as {outcome = NONE, used_facts, ...} =>
142 min depth result (filter_used_facts used_facts sup)
143 (filter_used_facts used_facts l0)
145 case test timeout (sup @ r0) of
146 result as {outcome = NONE, used_facts, ...} =>
147 min depth result (filter_used_facts used_facts sup)
148 (filter_used_facts used_facts r0)
151 val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
153 (sup, r0) |> pairself (filter_used_facts (map fst sup_r0))
154 val (sup_l, (r, result)) = min depth result (sup @ l) r0
155 val sup = sup |> filter_used_facts (map fst sup_l)
156 in (sup, (l @ r, result)) end
159 |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
161 | min _ result sup xs = (sup, (xs, result))
163 case snd (min 0 result [] xs) of
164 ([x], result as {run_time, ...}) =>
165 (case test (new_timeout timeout run_time) [] of
166 result as {outcome = NONE, ...} => ([], result)
167 | _ => ([x], result))
171 fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
174 val ctxt = Proof.context_of state
176 get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
177 val _ = print silent (fn () => "Sledgehammer minimizer: " ^
178 quote prover_name ^ ".")
179 fun test timeout = test_facts params silent prover timeout i n state
181 (case test timeout facts of
182 result as {outcome = NONE, used_facts, run_time, ...} =>
184 val facts = filter_used_facts used_facts facts
186 if length facts >= Config.get ctxt binary_min_facts then
190 val (min_facts, {preplay, message, message_tail, ...}) =
191 min test (new_timeout timeout run_time) result facts
192 val _ = print silent (fn () => cat_lines
193 ["Minimized to " ^ n_facts (map fst min_facts)] ^
194 (case length (filter (curry (op =) Chained o snd o fst) min_facts) of
196 | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".")
197 in (SOME min_facts, (preplay, message, message_tail)) end
198 | {outcome = SOME TimedOut, preplay, ...} =>
201 fn _ => "Timeout: You can increase the time limit using the \
202 \\"timeout\" option (e.g., \"timeout = " ^
203 string_of_int (10 + Time.toMilliseconds timeout div 1000) ^
206 | {preplay, message, ...} =>
207 (NONE, (preplay, prefix "Prover error: " o message, "")))
209 (NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, ""))
212 fun run_minimize (params as {provers, ...}) i refs state =
214 val ctxt = Proof.context_of state
215 val reserved = reserved_isar_keyword_table ()
216 val chained_ths = normalize_chained_theorems (#facts (Proof.goal state))
219 |> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths)
221 case subgoal_count state of
222 0 => Output.urgent_message "No subgoal!"
223 | n => case provers of
224 [] => error "No prover is set."
227 minimize_facts prover params false i n state facts
228 |> (fn (_, (preplay, message, message_tail)) =>
229 message (preplay ()) ^ message_tail
230 |> Output.urgent_message))