blanchet@39232
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
|
immler@31037
|
2 |
Author: Philipp Meyer, TU Muenchen
|
blanchet@36370
|
3 |
Author: Jasmin Blanchette, TU Muenchen
|
immler@31037
|
4 |
|
blanchet@41223
|
5 |
Minimization of fact list for Metis using external provers.
|
immler@31037
|
6 |
*)
|
immler@31037
|
7 |
|
blanchet@39232
|
8 |
signature SLEDGEHAMMER_MINIMIZE =
|
boehmes@32525
|
9 |
sig
|
blanchet@43926
|
10 |
type locality = ATP_Translate.locality
|
blanchet@43926
|
11 |
type play = ATP_Reconstruct.play
|
blanchet@41335
|
12 |
type params = Sledgehammer_Provers.params
|
blanchet@35867
|
13 |
|
blanchet@43517
|
14 |
val binary_min_facts : int Config.T
|
blanchet@40242
|
15 |
val minimize_facts :
|
blanchet@43905
|
16 |
string -> params -> bool -> int -> int -> Proof.state
|
blanchet@41339
|
17 |
-> ((string * locality) * thm list) list
|
blanchet@43893
|
18 |
-> ((string * locality) * thm list) list option
|
blanchet@44102
|
19 |
* ((unit -> play) * (play -> string) * string)
|
blanchet@39240
|
20 |
val run_minimize :
|
blanchet@39240
|
21 |
params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
|
blanchet@35866
|
22 |
end;
|
boehmes@32525
|
23 |
|
blanchet@39232
|
24 |
structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
|
immler@31037
|
25 |
struct
|
immler@31037
|
26 |
|
blanchet@43926
|
27 |
open ATP_Util
|
blanchet@39736
|
28 |
open ATP_Proof
|
blanchet@43926
|
29 |
open ATP_Translate
|
blanchet@43926
|
30 |
open ATP_Reconstruct
|
blanchet@36140
|
31 |
open Sledgehammer_Util
|
blanchet@39232
|
32 |
open Sledgehammer_Filter
|
blanchet@41335
|
33 |
open Sledgehammer_Provers
|
nipkow@33492
|
34 |
|
blanchet@36370
|
35 |
(* wrapper for calling external prover *)
|
wenzelm@31236
|
36 |
|
blanchet@40242
|
37 |
fun n_facts names =
|
blanchet@38937
|
38 |
let val n = length names in
|
blanchet@40242
|
39 |
string_of_int n ^ " fact" ^ plural_s n ^
|
blanchet@38338
|
40 |
(if n > 0 then
|
blanchet@46227
|
41 |
": " ^ (names |> map fst |> sort_distinct string_ord
|
blanchet@46227
|
42 |
|> space_implode " ")
|
blanchet@38338
|
43 |
else
|
blanchet@38338
|
44 |
"")
|
blanchet@38338
|
45 |
end
|
blanchet@38338
|
46 |
|
blanchet@41339
|
47 |
fun print silent f = if silent then () else Output.urgent_message (f ())
|
blanchet@41339
|
48 |
|
blanchet@43589
|
49 |
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
|
blanchet@46385
|
50 |
max_new_mono_instances, type_enc, lam_trans, isar_proof,
|
blanchet@43856
|
51 |
isar_shrink_factor, preplay_timeout, ...} : params)
|
blanchet@43905
|
52 |
silent (prover : prover) timeout i n state facts =
|
wenzelm@31236
|
53 |
let
|
blanchet@41525
|
54 |
val _ =
|
blanchet@41525
|
55 |
print silent (fn () =>
|
blanchet@41525
|
56 |
"Testing " ^ n_facts (map fst facts) ^
|
blanchet@41525
|
57 |
(if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
|
blanchet@43926
|
58 |
else "") ^ "...")
|
blanchet@42613
|
59 |
val {goal, ...} = Proof.goal state
|
blanchet@45320
|
60 |
val facts =
|
blanchet@45320
|
61 |
facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
|
blanchet@38346
|
62 |
val params =
|
blanchet@42915
|
63 |
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
|
blanchet@44493
|
64 |
provers = provers, type_enc = type_enc, sound = true,
|
blanchet@46385
|
65 |
lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01),
|
blanchet@46385
|
66 |
max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
|
blanchet@43605
|
67 |
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
|
blanchet@43605
|
68 |
isar_shrink_factor = isar_shrink_factor, slicing = false,
|
blanchet@43856
|
69 |
timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
|
blanchet@40246
|
70 |
val problem =
|
blanchet@40246
|
71 |
{state = state, goal = goal, subgoal = i, subgoal_count = n,
|
blanchet@42612
|
72 |
facts = facts, smt_filter = NONE}
|
blanchet@46231
|
73 |
val result as {outcome, used_facts, run_time, ...} =
|
blanchet@46391
|
74 |
prover params (K (K (K ""))) problem
|
blanchet@36223
|
75 |
in
|
blanchet@44100
|
76 |
print silent
|
blanchet@44100
|
77 |
(fn () =>
|
blanchet@44100
|
78 |
case outcome of
|
blanchet@44100
|
79 |
SOME failure => string_for_failure failure
|
blanchet@44100
|
80 |
| NONE =>
|
blanchet@44100
|
81 |
"Found proof" ^
|
blanchet@44100
|
82 |
(if length used_facts = length facts then ""
|
blanchet@46231
|
83 |
else " with " ^ n_facts used_facts) ^
|
blanchet@46231
|
84 |
" (" ^ string_from_time run_time ^ ").");
|
blanchet@38338
|
85 |
result
|
blanchet@36223
|
86 |
end
|
wenzelm@31236
|
87 |
|
blanchet@40445
|
88 |
(* minimalization of facts *)
|
wenzelm@31236
|
89 |
|
blanchet@46233
|
90 |
(* Give the external prover some slack. The ATP gets further slack because the
|
blanchet@46233
|
91 |
Sledgehammer preprocessing time is included in the estimate below but isn't
|
blanchet@46233
|
92 |
part of the timeout. *)
|
blanchet@46233
|
93 |
val slack_msecs = 200
|
blanchet@46233
|
94 |
|
blanchet@46233
|
95 |
fun new_timeout timeout run_time =
|
blanchet@46233
|
96 |
Int.min (Time.toMilliseconds timeout,
|
blanchet@46233
|
97 |
Time.toMilliseconds run_time + slack_msecs)
|
blanchet@46233
|
98 |
|> Time.fromMilliseconds
|
blanchet@46233
|
99 |
|
blanchet@46228
|
100 |
(* The linear algorithm usually outperforms the binary algorithm when over 60%
|
blanchet@46228
|
101 |
of the facts are actually needed. The binary algorithm is much more
|
blanchet@46228
|
102 |
appropriate for provers that cannot return the list of used facts and hence
|
blanchet@46228
|
103 |
returns all facts as used. Since we cannot know in advance how many facts are
|
blanchet@46228
|
104 |
actually needed, we heuristically set the threshold to 10 facts. *)
|
blanchet@43517
|
105 |
val binary_min_facts =
|
blanchet@43517
|
106 |
Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
|
blanchet@46229
|
107 |
(K 20)
|
blanchet@41223
|
108 |
|
blanchet@46229
|
109 |
fun linear_minimize test timeout result xs =
|
blanchet@46229
|
110 |
let
|
blanchet@46229
|
111 |
fun min _ [] p = p
|
blanchet@46229
|
112 |
| min timeout (x :: xs) (seen, result) =
|
blanchet@46229
|
113 |
case test timeout (xs @ seen) of
|
blanchet@46233
|
114 |
result as {outcome = NONE, used_facts, run_time, ...}
|
blanchet@46233
|
115 |
: prover_result =>
|
blanchet@46233
|
116 |
min (new_timeout timeout run_time) (filter_used_facts used_facts xs)
|
blanchet@46233
|
117 |
(filter_used_facts used_facts seen, result)
|
blanchet@46229
|
118 |
| _ => min timeout xs (x :: seen, result)
|
blanchet@46229
|
119 |
in min timeout xs ([], result) end
|
blanchet@38249
|
120 |
|
blanchet@46229
|
121 |
fun binary_minimize test timeout result xs =
|
blanchet@41223
|
122 |
let
|
blanchet@46233
|
123 |
fun min depth (result as {run_time, ...} : prover_result) sup
|
blanchet@46233
|
124 |
(xs as _ :: _ :: _) =
|
blanchet@42614
|
125 |
let
|
blanchet@46228
|
126 |
val (l0, r0) = chop (length xs div 2) xs
|
blanchet@42614
|
127 |
(*
|
blanchet@46227
|
128 |
val _ = warning (replicate_string depth " " ^ "{ " ^
|
blanchet@46227
|
129 |
"sup: " ^ n_facts (map fst sup))
|
blanchet@46227
|
130 |
val _ = warning (replicate_string depth " " ^ " " ^
|
blanchet@46227
|
131 |
"xs: " ^ n_facts (map fst xs))
|
blanchet@46227
|
132 |
val _ = warning (replicate_string depth " " ^ " " ^
|
blanchet@46227
|
133 |
"l0: " ^ n_facts (map fst l0))
|
blanchet@46227
|
134 |
val _ = warning (replicate_string depth " " ^ " " ^
|
blanchet@46227
|
135 |
"r0: " ^ n_facts (map fst r0))
|
blanchet@42614
|
136 |
*)
|
blanchet@46228
|
137 |
val depth = depth + 1
|
blanchet@46233
|
138 |
val timeout = new_timeout timeout run_time
|
blanchet@42614
|
139 |
in
|
blanchet@46229
|
140 |
case test timeout (sup @ l0) of
|
blanchet@46233
|
141 |
result as {outcome = NONE, used_facts, ...} =>
|
blanchet@46228
|
142 |
min depth result (filter_used_facts used_facts sup)
|
blanchet@46228
|
143 |
(filter_used_facts used_facts l0)
|
blanchet@46228
|
144 |
| _ =>
|
blanchet@46229
|
145 |
case test timeout (sup @ r0) of
|
blanchet@46228
|
146 |
result as {outcome = NONE, used_facts, ...} =>
|
blanchet@46228
|
147 |
min depth result (filter_used_facts used_facts sup)
|
blanchet@46228
|
148 |
(filter_used_facts used_facts r0)
|
blanchet@46228
|
149 |
| _ =>
|
blanchet@46228
|
150 |
let
|
blanchet@46228
|
151 |
val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
|
blanchet@46228
|
152 |
val (sup, r0) =
|
blanchet@46228
|
153 |
(sup, r0) |> pairself (filter_used_facts (map fst sup_r0))
|
blanchet@46228
|
154 |
val (sup_l, (r, result)) = min depth result (sup @ l) r0
|
blanchet@46228
|
155 |
val sup = sup |> filter_used_facts (map fst sup_l)
|
blanchet@46228
|
156 |
in (sup, (l @ r, result)) end
|
blanchet@41223
|
157 |
end
|
blanchet@42614
|
158 |
(*
|
blanchet@42614
|
159 |
|> tap (fn _ => warning (replicate_string depth " " ^ "}"))
|
blanchet@42614
|
160 |
*)
|
blanchet@46228
|
161 |
| min _ result sup xs = (sup, (xs, result))
|
blanchet@46228
|
162 |
in
|
blanchet@46228
|
163 |
case snd (min 0 result [] xs) of
|
blanchet@46233
|
164 |
([x], result as {run_time, ...}) =>
|
blanchet@46233
|
165 |
(case test (new_timeout timeout run_time) [] of
|
blanchet@46228
|
166 |
result as {outcome = NONE, ...} => ([], result)
|
blanchet@46228
|
167 |
| _ => ([x], result))
|
blanchet@46228
|
168 |
| p => p
|
blanchet@46228
|
169 |
end
|
blanchet@41223
|
170 |
|
blanchet@43905
|
171 |
fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
|
blanchet@43905
|
172 |
facts =
|
wenzelm@31236
|
173 |
let
|
blanchet@41189
|
174 |
val ctxt = Proof.context_of state
|
blanchet@46445
|
175 |
val prover =
|
blanchet@46445
|
176 |
get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
|
blanchet@43899
|
177 |
val _ = print silent (fn () => "Sledgehammer minimizer: " ^
|
blanchet@41223
|
178 |
quote prover_name ^ ".")
|
blanchet@46229
|
179 |
fun test timeout = test_facts params silent prover timeout i n state
|
wenzelm@31236
|
180 |
in
|
blanchet@46229
|
181 |
(case test timeout facts of
|
blanchet@46232
|
182 |
result as {outcome = NONE, used_facts, run_time, ...} =>
|
blanchet@38249
|
183 |
let
|
blanchet@41223
|
184 |
val facts = filter_used_facts used_facts facts
|
blanchet@46233
|
185 |
val min =
|
blanchet@46229
|
186 |
if length facts >= Config.get ctxt binary_min_facts then
|
blanchet@46229
|
187 |
binary_minimize
|
blanchet@46229
|
188 |
else
|
blanchet@46229
|
189 |
linear_minimize
|
blanchet@44439
|
190 |
val (min_facts, {preplay, message, message_tail, ...}) =
|
blanchet@46232
|
191 |
min test (new_timeout timeout run_time) result facts
|
blanchet@41339
|
192 |
val _ = print silent (fn () => cat_lines
|
blanchet@44497
|
193 |
["Minimized to " ^ n_facts (map fst min_facts)] ^
|
blanchet@44439
|
194 |
(case length (filter (curry (op =) Chained o snd o fst) min_facts) of
|
blanchet@38937
|
195 |
0 => ""
|
blanchet@44439
|
196 |
| n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".")
|
blanchet@44439
|
197 |
in (SOME min_facts, (preplay, message, message_tail)) end
|
blanchet@43893
|
198 |
| {outcome = SOME TimedOut, preplay, ...} =>
|
blanchet@43893
|
199 |
(NONE,
|
blanchet@43893
|
200 |
(preplay,
|
blanchet@43893
|
201 |
fn _ => "Timeout: You can increase the time limit using the \
|
blanchet@43893
|
202 |
\\"timeout\" option (e.g., \"timeout = " ^
|
blanchet@46232
|
203 |
string_of_int (10 + Time.toMilliseconds timeout div 1000) ^
|
blanchet@46232
|
204 |
"\").",
|
blanchet@44102
|
205 |
""))
|
blanchet@43893
|
206 |
| {preplay, message, ...} =>
|
blanchet@44102
|
207 |
(NONE, (preplay, prefix "Prover error: " o message, "")))
|
blanchet@44007
|
208 |
handle ERROR msg =>
|
blanchet@46390
|
209 |
(NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, ""))
|
immler@31037
|
210 |
end
|
immler@31037
|
211 |
|
blanchet@41513
|
212 |
fun run_minimize (params as {provers, ...}) i refs state =
|
blanchet@38291
|
213 |
let
|
blanchet@38291
|
214 |
val ctxt = Proof.context_of state
|
blanchet@38935
|
215 |
val reserved = reserved_isar_keyword_table ()
|
blanchet@43884
|
216 |
val chained_ths = normalize_chained_theorems (#facts (Proof.goal state))
|
blanchet@40445
|
217 |
val facts =
|
blanchet@41339
|
218 |
refs
|
blanchet@41339
|
219 |
|> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths)
|
blanchet@38291
|
220 |
in
|
blanchet@38291
|
221 |
case subgoal_count state of
|
wenzelm@40392
|
222 |
0 => Output.urgent_message "No subgoal!"
|
blanchet@41513
|
223 |
| n => case provers of
|
blanchet@41513
|
224 |
[] => error "No prover is set."
|
blanchet@41513
|
225 |
| prover :: _ =>
|
blanchet@41513
|
226 |
(kill_provers ();
|
blanchet@43905
|
227 |
minimize_facts prover params false i n state facts
|
blanchet@44102
|
228 |
|> (fn (_, (preplay, message, message_tail)) =>
|
blanchet@44102
|
229 |
message (preplay ()) ^ message_tail
|
blanchet@44102
|
230 |
|> Output.urgent_message))
|
blanchet@38291
|
231 |
end
|
blanchet@38291
|
232 |
|
blanchet@35866
|
233 |
end;
|