fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
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
14 val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
16 string -> params -> bool option -> bool -> int -> int -> Proof.state
17 -> ((string * locality) * thm list) list
18 -> ((string * locality) * thm list) list option * string
20 params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
23 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
27 open Sledgehammer_Util
28 open Sledgehammer_Filter
29 open Sledgehammer_Provers
31 (* wrapper for calling external prover *)
34 let val n = length names in
35 string_of_int n ^ " fact" ^ plural_s n ^
37 ": " ^ (names |> map fst
38 |> sort_distinct string_ord |> space_implode " ")
43 fun print silent f = if silent then () else Output.urgent_message (f ())
45 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
46 max_new_mono_instances, type_sys, isar_proof,
47 isar_shrink_factor, ...} : params)
48 explicit_apply_opt silent (prover : prover) timeout i n state facts =
50 val ctxt = Proof.context_of state
51 val thy = Proof.theory_of state
53 print silent (fn () =>
54 "Testing " ^ n_facts (map fst facts) ^
55 (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
57 val {goal, ...} = Proof.goal state
59 case explicit_apply_opt of
60 SOME explicit_apply => explicit_apply
62 let val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i in
63 not (forall (Meson.is_fol_term thy)
64 (concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
67 {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
68 provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
69 relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
70 max_mono_iters = max_mono_iters,
71 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
72 isar_shrink_factor = isar_shrink_factor, slicing = false,
73 timeout = timeout, expect = ""}
75 facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
77 {state = state, goal = goal, subgoal = i, subgoal_count = n,
78 facts = facts, smt_filter = NONE}
79 val result as {outcome, used_facts, ...} = prover params (K "") problem
81 print silent (fn () =>
83 SOME failure => string_for_failure failure
84 | NONE => if length used_facts = length facts then "Found proof."
85 else "Found proof with " ^ n_facts used_facts ^ ".");
89 (* minimalization of facts *)
91 (* The sublinear algorithm works well in almost all situations, except when the
92 external prover cannot return the list of used facts and hence returns all
93 facts as used. In that case, the binary algorithm is much more appropriate.
94 We can usually detect the situation by looking at the number of used facts
95 reported by the prover. *)
96 val binary_min_facts =
97 Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
100 fun filter_used_facts used = filter (member (op =) used o fst)
102 fun sublinear_minimize _ [] p = p
103 | sublinear_minimize test (x :: xs) (seen, result) =
104 case test (xs @ seen) of
105 result as {outcome = NONE, used_facts, ...} : prover_result =>
106 sublinear_minimize test (filter_used_facts used_facts xs)
107 (filter_used_facts used_facts seen, result)
108 | _ => sublinear_minimize test xs (x :: seen, result)
110 fun binary_minimize test xs =
112 fun p xs = #outcome (test xs : prover_result) = NONE
114 | split [h] (l, r) = (h :: l, r)
115 | split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r)
116 fun min _ _ [] = raise Empty
117 | min _ _ [s0] = [s0]
121 val _ = warning (replicate_string depth " " ^ "{" ^ (" " ^
122 n_facts (map fst sup) ^ " and " ^
123 n_facts (map fst xs)))
125 val (l0, r0) = split xs ([], [])
128 min (depth + 1) sup l0
129 else if p (sup @ r0) then
130 min (depth + 1) sup r0
133 val l = min (depth + 1) (sup @ r0) l0
134 val r = min (depth + 1) (sup @ l) r0
138 |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
142 [x] => if p [] then [] else [x]
146 (* Give the external prover some slack. The ATP gets further slack because the
147 Sledgehammer preprocessing time is included in the estimate below but isn't
148 part of the timeout. *)
149 val slack_msecs = 200
151 fun minimize_facts prover_name (params as {timeout, ...}) explicit_apply_opt
152 silent i n state facts =
154 val ctxt = Proof.context_of state
155 val prover = get_prover ctxt false prover_name
156 val msecs = Time.toMilliseconds timeout
157 val _ = print silent (fn () => "Sledgehammer minimize: " ^
158 quote prover_name ^ ".")
159 fun do_test timeout =
160 test_facts params explicit_apply_opt silent prover timeout i n state
161 val timer = Timer.startRealTimer ()
163 (case do_test timeout facts of
164 result as {outcome = NONE, used_facts, ...} =>
166 val time = Timer.checkRealTimer timer
168 Int.min (msecs, Time.toMilliseconds time + slack_msecs)
169 |> Time.fromMilliseconds
170 val facts = filter_used_facts used_facts facts
171 val (min_thms, {message, ...}) =
172 if length facts >= Config.get ctxt binary_min_facts then
173 binary_minimize (do_test new_timeout) facts
175 sublinear_minimize (do_test new_timeout) facts ([], result)
176 val n = length min_thms
177 val _ = print silent (fn () => cat_lines
178 ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
179 (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
181 | n => " (including " ^ string_of_int n ^ " chained)") ^ ".")
182 in (SOME min_thms, message) end
183 | {outcome = SOME TimedOut, ...} =>
184 (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
185 \option (e.g., \"timeout = " ^
186 string_of_int (10 + msecs div 1000) ^ "\").")
187 | {message, ...} => (NONE, "Prover error: " ^ message))
188 handle ERROR msg => (NONE, "Error: " ^ msg)
191 fun run_minimize (params as {provers, ...}) i refs state =
193 val ctxt = Proof.context_of state
194 val reserved = reserved_isar_keyword_table ()
195 val chained_ths = #facts (Proof.goal state)
198 |> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths)
200 case subgoal_count state of
201 0 => Output.urgent_message "No subgoal!"
202 | n => case provers of
203 [] => error "No prover is set."
206 minimize_facts prover params NONE false i n state facts
207 |> #2 |> Output.urgent_message)