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@38937
|
41 |
": " ^ (names |> map fst
|
blanchet@38937
|
42 |
|> sort_distinct string_ord |> 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@44100
|
50 |
max_new_mono_instances, type_sys, 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@38346
|
60 |
val params =
|
blanchet@42915
|
61 |
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
|
blanchet@44434
|
62 |
provers = provers, type_sys = type_sys, sound = true,
|
blanchet@41386
|
63 |
relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
|
blanchet@43605
|
64 |
max_mono_iters = max_mono_iters,
|
blanchet@43605
|
65 |
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
|
blanchet@43605
|
66 |
isar_shrink_factor = isar_shrink_factor, slicing = false,
|
blanchet@43856
|
67 |
timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
|
blanchet@40445
|
68 |
val facts =
|
blanchet@41338
|
69 |
facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
|
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@43891
|
73 |
val result as {outcome, used_facts, run_time_in_msecs, ...} =
|
blanchet@43892
|
74 |
prover params (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@44100
|
83 |
else " with " ^ n_facts used_facts) ^
|
blanchet@44100
|
84 |
(case run_time_in_msecs of
|
blanchet@44100
|
85 |
SOME ms =>
|
blanchet@44100
|
86 |
" (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")"
|
blanchet@44100
|
87 |
| NONE => "") ^ ".");
|
blanchet@38338
|
88 |
result
|
blanchet@36223
|
89 |
end
|
wenzelm@31236
|
90 |
|
blanchet@40445
|
91 |
(* minimalization of facts *)
|
wenzelm@31236
|
92 |
|
blanchet@41223
|
93 |
(* The sublinear algorithm works well in almost all situations, except when the
|
blanchet@41223
|
94 |
external prover cannot return the list of used facts and hence returns all
|
blanchet@41515
|
95 |
facts as used. In that case, the binary algorithm is much more appropriate.
|
blanchet@41515
|
96 |
We can usually detect the situation by looking at the number of used facts
|
blanchet@41515
|
97 |
reported by the prover. *)
|
blanchet@43517
|
98 |
val binary_min_facts =
|
blanchet@43517
|
99 |
Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
|
blanchet@43517
|
100 |
(K 20)
|
blanchet@41223
|
101 |
|
blanchet@38249
|
102 |
fun sublinear_minimize _ [] p = p
|
blanchet@38249
|
103 |
| sublinear_minimize test (x :: xs) (seen, result) =
|
blanchet@38249
|
104 |
case test (xs @ seen) of
|
blanchet@40445
|
105 |
result as {outcome = NONE, used_facts, ...} : prover_result =>
|
blanchet@40445
|
106 |
sublinear_minimize test (filter_used_facts used_facts xs)
|
blanchet@40445
|
107 |
(filter_used_facts used_facts seen, result)
|
blanchet@38249
|
108 |
| _ => sublinear_minimize test xs (x :: seen, result)
|
blanchet@38249
|
109 |
|
blanchet@41223
|
110 |
fun binary_minimize test xs =
|
blanchet@41223
|
111 |
let
|
blanchet@44177
|
112 |
fun pred xs = #outcome (test xs : prover_result) = NONE
|
blanchet@41223
|
113 |
fun split [] p = p
|
blanchet@41223
|
114 |
| split [h] (l, r) = (h :: l, r)
|
blanchet@41223
|
115 |
| split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r)
|
blanchet@42614
|
116 |
fun min _ _ [] = raise Empty
|
blanchet@42614
|
117 |
| min _ _ [s0] = [s0]
|
blanchet@42614
|
118 |
| min depth sup xs =
|
blanchet@42614
|
119 |
let
|
blanchet@42614
|
120 |
(*
|
blanchet@42614
|
121 |
val _ = warning (replicate_string depth " " ^ "{" ^ (" " ^
|
blanchet@42614
|
122 |
n_facts (map fst sup) ^ " and " ^
|
blanchet@42614
|
123 |
n_facts (map fst xs)))
|
blanchet@42614
|
124 |
*)
|
blanchet@42614
|
125 |
val (l0, r0) = split xs ([], [])
|
blanchet@42614
|
126 |
in
|
blanchet@44177
|
127 |
if pred (sup @ l0) then
|
blanchet@42614
|
128 |
min (depth + 1) sup l0
|
blanchet@44177
|
129 |
else if pred (sup @ r0) then
|
blanchet@42614
|
130 |
min (depth + 1) sup r0
|
blanchet@41223
|
131 |
else
|
blanchet@41223
|
132 |
let
|
blanchet@42614
|
133 |
val l = min (depth + 1) (sup @ r0) l0
|
blanchet@42614
|
134 |
val r = min (depth + 1) (sup @ l) r0
|
blanchet@41223
|
135 |
in l @ r end
|
blanchet@41223
|
136 |
end
|
blanchet@42614
|
137 |
(*
|
blanchet@42614
|
138 |
|> tap (fn _ => warning (replicate_string depth " " ^ "}"))
|
blanchet@42614
|
139 |
*)
|
blanchet@41223
|
140 |
val xs =
|
blanchet@42614
|
141 |
case min 0 [] xs of
|
blanchet@44177
|
142 |
[x] => if pred [] then [] else [x]
|
blanchet@41223
|
143 |
| xs => xs
|
blanchet@41223
|
144 |
in (xs, test xs) end
|
blanchet@41223
|
145 |
|
blanchet@41223
|
146 |
(* Give the external prover some slack. The ATP gets further slack because the
|
blanchet@41223
|
147 |
Sledgehammer preprocessing time is included in the estimate below but isn't
|
blanchet@41223
|
148 |
part of the timeout. *)
|
blanchet@41525
|
149 |
val slack_msecs = 200
|
blanchet@38338
|
150 |
|
blanchet@43905
|
151 |
fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
|
blanchet@43905
|
152 |
facts =
|
wenzelm@31236
|
153 |
let
|
blanchet@41189
|
154 |
val ctxt = Proof.context_of state
|
blanchet@43862
|
155 |
val prover = get_prover ctxt Minimize prover_name
|
blanchet@38813
|
156 |
val msecs = Time.toMilliseconds timeout
|
blanchet@43899
|
157 |
val _ = print silent (fn () => "Sledgehammer minimizer: " ^
|
blanchet@41223
|
158 |
quote prover_name ^ ".")
|
blanchet@43905
|
159 |
fun do_test timeout = test_facts params silent prover timeout i n state
|
blanchet@38338
|
160 |
val timer = Timer.startRealTimer ()
|
wenzelm@31236
|
161 |
in
|
blanchet@40445
|
162 |
(case do_test timeout facts of
|
blanchet@40445
|
163 |
result as {outcome = NONE, used_facts, ...} =>
|
blanchet@38249
|
164 |
let
|
blanchet@38338
|
165 |
val time = Timer.checkRealTimer timer
|
blanchet@38338
|
166 |
val new_timeout =
|
blanchet@41525
|
167 |
Int.min (msecs, Time.toMilliseconds time + slack_msecs)
|
blanchet@38338
|
168 |
|> Time.fromMilliseconds
|
blanchet@41223
|
169 |
val facts = filter_used_facts used_facts facts
|
blanchet@44102
|
170 |
val (min_thms, {preplay, message, message_tail, ...}) =
|
blanchet@43517
|
171 |
if length facts >= Config.get ctxt binary_min_facts then
|
blanchet@41223
|
172 |
binary_minimize (do_test new_timeout) facts
|
blanchet@41223
|
173 |
else
|
blanchet@41223
|
174 |
sublinear_minimize (do_test new_timeout) facts ([], result)
|
blanchet@38340
|
175 |
val n = length min_thms
|
blanchet@41339
|
176 |
val _ = print silent (fn () => cat_lines
|
blanchet@40242
|
177 |
["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
|
blanchet@38991
|
178 |
(case length (filter (curry (op =) Chained o snd o fst) min_thms) of
|
blanchet@38937
|
179 |
0 => ""
|
wenzelm@41739
|
180 |
| n => " (including " ^ string_of_int n ^ " chained)") ^ ".")
|
blanchet@44102
|
181 |
in (SOME min_thms, (preplay, message, message_tail)) end
|
blanchet@43893
|
182 |
| {outcome = SOME TimedOut, preplay, ...} =>
|
blanchet@43893
|
183 |
(NONE,
|
blanchet@43893
|
184 |
(preplay,
|
blanchet@43893
|
185 |
fn _ => "Timeout: You can increase the time limit using the \
|
blanchet@43893
|
186 |
\\"timeout\" option (e.g., \"timeout = " ^
|
blanchet@44102
|
187 |
string_of_int (10 + msecs div 1000) ^ "\").",
|
blanchet@44102
|
188 |
""))
|
blanchet@43893
|
189 |
| {preplay, message, ...} =>
|
blanchet@44102
|
190 |
(NONE, (preplay, prefix "Prover error: " o message, "")))
|
blanchet@44007
|
191 |
handle ERROR msg =>
|
blanchet@44102
|
192 |
(NONE, (K (Failed_to_Play Metis), fn _ => "Error: " ^ msg, ""))
|
immler@31037
|
193 |
end
|
immler@31037
|
194 |
|
blanchet@41513
|
195 |
fun run_minimize (params as {provers, ...}) i refs state =
|
blanchet@38291
|
196 |
let
|
blanchet@38291
|
197 |
val ctxt = Proof.context_of state
|
blanchet@38935
|
198 |
val reserved = reserved_isar_keyword_table ()
|
blanchet@43884
|
199 |
val chained_ths = normalize_chained_theorems (#facts (Proof.goal state))
|
blanchet@40445
|
200 |
val facts =
|
blanchet@41339
|
201 |
refs
|
blanchet@41339
|
202 |
|> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths)
|
blanchet@38291
|
203 |
in
|
blanchet@38291
|
204 |
case subgoal_count state of
|
wenzelm@40392
|
205 |
0 => Output.urgent_message "No subgoal!"
|
blanchet@41513
|
206 |
| n => case provers of
|
blanchet@41513
|
207 |
[] => error "No prover is set."
|
blanchet@41513
|
208 |
| prover :: _ =>
|
blanchet@41513
|
209 |
(kill_provers ();
|
blanchet@43905
|
210 |
minimize_facts prover params false i n state facts
|
blanchet@44102
|
211 |
|> (fn (_, (preplay, message, message_tail)) =>
|
blanchet@44102
|
212 |
message (preplay ()) ^ message_tail
|
blanchet@44102
|
213 |
|> Output.urgent_message))
|
blanchet@38291
|
214 |
end
|
blanchet@38291
|
215 |
|
blanchet@35866
|
216 |
end;
|