1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML |
|
2 Author: Philipp Meyer, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 |
|
5 Minimization of theorem list for Metis using automatic theorem provers. |
|
6 *) |
|
7 |
|
8 signature SLEDGEHAMMER_FACT_MINIMIZER = |
|
9 sig |
|
10 type params = Sledgehammer.params |
|
11 |
|
12 val minimize_theorems : |
|
13 params -> int -> int -> Proof.state -> (string * thm list) list |
|
14 -> (string * thm list) list option * string |
|
15 val run_minimizer : params -> int -> Facts.ref list -> Proof.state -> unit |
|
16 end; |
|
17 |
|
18 structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER = |
|
19 struct |
|
20 |
|
21 open ATP_Systems |
|
22 open Sledgehammer_Util |
|
23 open Sledgehammer_Fact_Filter |
|
24 open Sledgehammer_Proof_Reconstruct |
|
25 open Sledgehammer |
|
26 |
|
27 (* wrapper for calling external prover *) |
|
28 |
|
29 fun string_for_failure Unprovable = "Unprovable." |
|
30 | string_for_failure TimedOut = "Timed out." |
|
31 | string_for_failure _ = "Unknown error." |
|
32 |
|
33 fun n_theorems name_thms_pairs = |
|
34 let val n = length name_thms_pairs in |
|
35 string_of_int n ^ " theorem" ^ plural_s n ^ |
|
36 (if n > 0 then |
|
37 ": " ^ space_implode " " |
|
38 (name_thms_pairs |
|
39 |> map (perhaps (try (unprefix chained_prefix))) |
|
40 |> sort_distinct string_ord) |
|
41 else |
|
42 "") |
|
43 end |
|
44 |
|
45 fun test_theorems ({debug, verbose, overlord, atps, full_types, |
|
46 relevance_threshold, relevance_convergence, theory_relevant, |
|
47 defs_relevant, isar_proof, isar_shrink_factor, |
|
48 ...} : params) |
|
49 (prover : prover) explicit_apply timeout subgoal state |
|
50 name_thms_pairs = |
|
51 let |
|
52 val _ = |
|
53 priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...") |
|
54 val params = |
|
55 {debug = debug, verbose = verbose, overlord = overlord, atps = atps, |
|
56 full_types = full_types, explicit_apply = explicit_apply, |
|
57 relevance_threshold = relevance_threshold, |
|
58 relevance_convergence = relevance_convergence, |
|
59 theory_relevant = theory_relevant, defs_relevant = defs_relevant, |
|
60 isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, |
|
61 timeout = timeout, minimize_timeout = timeout} |
|
62 val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs |
|
63 val {context = ctxt, facts, goal} = Proof.goal state |
|
64 val problem = |
|
65 {subgoal = subgoal, goal = (ctxt, (facts, goal)), |
|
66 relevance_override = {add = [], del = [], only = false}, |
|
67 axioms = SOME axioms} |
|
68 val result as {outcome, used_thm_names, ...} = |
|
69 prover params (K "") problem |
|
70 in |
|
71 priority (case outcome of |
|
72 NONE => |
|
73 if length used_thm_names = length name_thms_pairs then |
|
74 "Found proof." |
|
75 else |
|
76 "Found proof with " ^ n_theorems used_thm_names ^ "." |
|
77 | SOME failure => string_for_failure failure); |
|
78 result |
|
79 end |
|
80 |
|
81 (* minimalization of thms *) |
|
82 |
|
83 fun filter_used_facts used = |
|
84 filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst) |
|
85 |
|
86 fun sublinear_minimize _ [] p = p |
|
87 | sublinear_minimize test (x :: xs) (seen, result) = |
|
88 case test (xs @ seen) of |
|
89 result as {outcome = NONE, proof, used_thm_names, ...} |
|
90 : prover_result => |
|
91 sublinear_minimize test (filter_used_facts used_thm_names xs) |
|
92 (filter_used_facts used_thm_names seen, result) |
|
93 | _ => sublinear_minimize test xs (x :: seen, result) |
|
94 |
|
95 (* Give the ATP some slack. The ATP gets further slack because the Sledgehammer |
|
96 preprocessing time is included in the estimate below but isn't part of the |
|
97 timeout. *) |
|
98 val fudge_msecs = 250 |
|
99 |
|
100 fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set." |
|
101 | minimize_theorems |
|
102 (params as {debug, verbose, overlord, atps as atp :: _, full_types, |
|
103 relevance_threshold, relevance_convergence, theory_relevant, |
|
104 defs_relevant, isar_proof, isar_shrink_factor, |
|
105 minimize_timeout, ...}) |
|
106 i n state name_thms_pairs = |
|
107 let |
|
108 val thy = Proof.theory_of state |
|
109 val prover = get_prover_fun thy atp |
|
110 val msecs = Time.toMilliseconds minimize_timeout |
|
111 val _ = |
|
112 priority ("Sledgehammer minimizer: ATP " ^ quote atp ^ |
|
113 " with a time limit of " ^ string_of_int msecs ^ " ms.") |
|
114 val {context = ctxt, goal, ...} = Proof.goal state |
|
115 val (_, hyp_ts, concl_t) = strip_subgoal goal i |
|
116 val explicit_apply = |
|
117 not (forall (Meson.is_fol_term thy) |
|
118 (concl_t :: hyp_ts @ maps (map prop_of o snd) name_thms_pairs)) |
|
119 fun do_test timeout = |
|
120 test_theorems params prover explicit_apply timeout i state |
|
121 val timer = Timer.startRealTimer () |
|
122 in |
|
123 (case do_test minimize_timeout name_thms_pairs of |
|
124 result as {outcome = NONE, pool, used_thm_names, |
|
125 conjecture_shape, ...} => |
|
126 let |
|
127 val time = Timer.checkRealTimer timer |
|
128 val new_timeout = |
|
129 Int.min (msecs, Time.toMilliseconds time + fudge_msecs) |
|
130 |> Time.fromMilliseconds |
|
131 val (min_thms, {proof, internal_thm_names, ...}) = |
|
132 sublinear_minimize (do_test new_timeout) |
|
133 (filter_used_facts used_thm_names name_thms_pairs) ([], result) |
|
134 val n = length min_thms |
|
135 val _ = priority (cat_lines |
|
136 ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ |
|
137 (case filter (String.isPrefix chained_prefix o fst) min_thms of |
|
138 [] => "" |
|
139 | chained => " (including " ^ Int.toString (length chained) ^ |
|
140 " chained)") ^ ".") |
|
141 in |
|
142 (SOME min_thms, |
|
143 proof_text isar_proof |
|
144 (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) |
|
145 (full_types, K "", proof, internal_thm_names, goal, i) |> fst) |
|
146 end |
|
147 | {outcome = SOME TimedOut, ...} => |
|
148 (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ |
|
149 \option (e.g., \"timeout = " ^ |
|
150 string_of_int (10 + msecs div 1000) ^ " s\").") |
|
151 | {outcome = SOME UnknownError, ...} => |
|
152 (* Failure sometimes mean timeout, unfortunately. *) |
|
153 (NONE, "Failure: No proof was found with the current time limit. You \ |
|
154 \can increase the time limit using the \"timeout\" \ |
|
155 \option (e.g., \"timeout = " ^ |
|
156 string_of_int (10 + msecs div 1000) ^ " s\").") |
|
157 | {message, ...} => (NONE, "ATP error: " ^ message)) |
|
158 handle ERROR msg => (NONE, "Error: " ^ msg) |
|
159 end |
|
160 |
|
161 fun run_minimizer params i refs state = |
|
162 let |
|
163 val ctxt = Proof.context_of state |
|
164 val chained_ths = #facts (Proof.goal state) |
|
165 val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs |
|
166 in |
|
167 case subgoal_count state of |
|
168 0 => priority "No subgoal!" |
|
169 | n => |
|
170 (kill_atps (); |
|
171 priority (#2 (minimize_theorems params i n state name_thms_pairs))) |
|
172 end |
|
173 |
|
174 end; |
|