normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
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 = Sledgehammer_Filter.locality
11 type params = Sledgehammer_Provers.params
13 val binary_min_facts : int Config.T
15 string -> params -> bool option -> bool -> int -> int -> Proof.state
16 -> ((string * locality) * thm list) list
17 -> ((string * locality) * thm list) list option * string
19 params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
22 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
26 open Sledgehammer_Util
27 open Sledgehammer_Filter
28 open Sledgehammer_Provers
30 (* wrapper for calling external prover *)
33 let val n = length names in
34 string_of_int n ^ " fact" ^ plural_s n ^
36 ": " ^ (names |> map fst
37 |> sort_distinct string_ord |> space_implode " ")
42 fun print silent f = if silent then () else Output.urgent_message (f ())
44 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
45 max_new_mono_instances, type_sys, isar_proof,
46 isar_shrink_factor, preplay_timeout, ...} : params)
47 explicit_apply_opt silent (prover : prover) timeout i n state facts =
49 val ctxt = Proof.context_of state
50 val thy = Proof.theory_of state
52 print silent (fn () =>
53 "Testing " ^ n_facts (map fst facts) ^
54 (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
56 val {goal, ...} = Proof.goal state
58 case explicit_apply_opt of
59 SOME explicit_apply => explicit_apply
61 let val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i in
62 not (forall (Meson.is_fol_term thy)
63 (concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
66 {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
67 provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
68 relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
69 max_mono_iters = max_mono_iters,
70 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
71 isar_shrink_factor = isar_shrink_factor, slicing = false,
72 timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
74 facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
76 {state = state, goal = goal, subgoal = i, subgoal_count = n,
77 facts = facts, smt_filter = NONE}
78 val result as {outcome, used_facts, ...} = prover params (K "") problem
80 print silent (fn () =>
82 SOME failure => string_for_failure failure
83 | NONE => if length used_facts = length facts then "Found proof."
84 else "Found proof with " ^ n_facts used_facts ^ ".");
88 (* minimalization of facts *)
90 (* The sublinear algorithm works well in almost all situations, except when the
91 external prover cannot return the list of used facts and hence returns all
92 facts as used. In that case, the binary algorithm is much more appropriate.
93 We can usually detect the situation by looking at the number of used facts
94 reported by the prover. *)
95 val binary_min_facts =
96 Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
99 fun sublinear_minimize _ [] p = p
100 | sublinear_minimize test (x :: xs) (seen, result) =
101 case test (xs @ seen) of
102 result as {outcome = NONE, used_facts, ...} : prover_result =>
103 sublinear_minimize test (filter_used_facts used_facts xs)
104 (filter_used_facts used_facts seen, result)
105 | _ => sublinear_minimize test xs (x :: seen, result)
107 fun binary_minimize test xs =
109 fun p xs = #outcome (test xs : prover_result) = NONE
111 | split [h] (l, r) = (h :: l, r)
112 | split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r)
113 fun min _ _ [] = raise Empty
114 | min _ _ [s0] = [s0]
118 val _ = warning (replicate_string depth " " ^ "{" ^ (" " ^
119 n_facts (map fst sup) ^ " and " ^
120 n_facts (map fst xs)))
122 val (l0, r0) = split xs ([], [])
125 min (depth + 1) sup l0
126 else if p (sup @ r0) then
127 min (depth + 1) sup r0
130 val l = min (depth + 1) (sup @ r0) l0
131 val r = min (depth + 1) (sup @ l) r0
135 |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
139 [x] => if p [] then [] else [x]
143 (* Give the external prover some slack. The ATP gets further slack because the
144 Sledgehammer preprocessing time is included in the estimate below but isn't
145 part of the timeout. *)
146 val slack_msecs = 200
148 fun minimize_facts prover_name (params as {timeout, ...}) explicit_apply_opt
149 silent i n state facts =
151 val ctxt = Proof.context_of state
152 val prover = get_prover ctxt Minimize prover_name
153 val msecs = Time.toMilliseconds timeout
154 val _ = print silent (fn () => "Sledgehammer minimize: " ^
155 quote prover_name ^ ".")
156 fun do_test timeout =
157 test_facts params explicit_apply_opt silent prover timeout i n state
158 val timer = Timer.startRealTimer ()
160 (case do_test timeout facts of
161 result as {outcome = NONE, used_facts, ...} =>
163 val time = Timer.checkRealTimer timer
165 Int.min (msecs, Time.toMilliseconds time + slack_msecs)
166 |> Time.fromMilliseconds
167 val facts = filter_used_facts used_facts facts
168 val (min_thms, {message, ...}) =
169 if length facts >= Config.get ctxt binary_min_facts then
170 binary_minimize (do_test new_timeout) facts
172 sublinear_minimize (do_test new_timeout) facts ([], result)
173 val n = length min_thms
174 val _ = print silent (fn () => cat_lines
175 ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
176 (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
178 | n => " (including " ^ string_of_int n ^ " chained)") ^ ".")
179 in (SOME min_thms, message) end
180 | {outcome = SOME TimedOut, ...} =>
181 (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
182 \option (e.g., \"timeout = " ^
183 string_of_int (10 + msecs div 1000) ^ "\").")
184 | {message, ...} => (NONE, "Prover error: " ^ message))
185 handle ERROR msg => (NONE, "Error: " ^ msg)
188 fun run_minimize (params as {provers, ...}) i refs state =
190 val ctxt = Proof.context_of state
191 val reserved = reserved_isar_keyword_table ()
192 val chained_ths = normalize_chained_theorems (#facts (Proof.goal state))
195 |> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths)
197 case subgoal_count state of
198 0 => Output.urgent_message "No subgoal!"
199 | n => case provers of
200 [] => error "No prover is set."
203 minimize_facts prover params NONE false i n state facts
204 |> snd |> Output.urgent_message)