wenzelm@32564
|
1 |
(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
|
wenzelm@32564
|
2 |
Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich
|
boehmes@32385
|
3 |
*)
|
boehmes@32385
|
4 |
|
boehmes@32385
|
5 |
structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
|
boehmes@32385
|
6 |
struct
|
boehmes@32385
|
7 |
|
boehmes@32521
|
8 |
val proverK = "prover"
|
boehmes@32541
|
9 |
val prover_timeoutK = "prover_timeout"
|
boehmes@32573
|
10 |
val prover_hard_timeoutK = "prover_hard_timeout"
|
boehmes@32521
|
11 |
val keepK = "keep"
|
boehmes@32521
|
12 |
val full_typesK = "full_types"
|
boehmes@32525
|
13 |
val minimizeK = "minimize"
|
boehmes@32525
|
14 |
val minimize_timeoutK = "minimize_timeout"
|
boehmes@34033
|
15 |
val metis_ftK = "metis_ft"
|
boehmes@32521
|
16 |
|
boehmes@32521
|
17 |
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
|
boehmes@32525
|
18 |
fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
|
boehmes@32521
|
19 |
fun metis_tag id = "#" ^ string_of_int id ^ " metis (sledgehammer): "
|
boehmes@32521
|
20 |
|
boehmes@32525
|
21 |
val separator = "-----"
|
boehmes@32525
|
22 |
|
boehmes@32521
|
23 |
|
nipkow@32549
|
24 |
datatype sh_data = ShData of {
|
nipkow@32549
|
25 |
calls: int,
|
nipkow@32549
|
26 |
success: int,
|
nipkow@32585
|
27 |
lemmas: int,
|
nipkow@32810
|
28 |
max_lems: int,
|
nipkow@32549
|
29 |
time_isa: int,
|
nipkow@32549
|
30 |
time_atp: int,
|
nipkow@32549
|
31 |
time_atp_fail: int}
|
boehmes@32521
|
32 |
|
nipkow@32549
|
33 |
datatype me_data = MeData of {
|
nipkow@32549
|
34 |
calls: int,
|
nipkow@32549
|
35 |
success: int,
|
nipkow@32676
|
36 |
proofs: int,
|
nipkow@32549
|
37 |
time: int,
|
nipkow@32550
|
38 |
timeout: int,
|
nipkow@32990
|
39 |
lemmas: int * int * int,
|
nipkow@32551
|
40 |
posns: Position.T list
|
nipkow@32550
|
41 |
}
|
boehmes@32521
|
42 |
|
nipkow@32571
|
43 |
datatype min_data = MinData of {
|
nipkow@32609
|
44 |
succs: int,
|
blanchet@35866
|
45 |
ab_ratios: int
|
nipkow@32571
|
46 |
}
|
boehmes@32521
|
47 |
|
nipkow@32810
|
48 |
fun make_sh_data
|
nipkow@32810
|
49 |
(calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail) =
|
nipkow@32810
|
50 |
ShData{calls=calls, success=success, lemmas=lemmas, max_lems=max_lems,
|
nipkow@32810
|
51 |
time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail}
|
boehmes@32521
|
52 |
|
blanchet@35866
|
53 |
fun make_min_data (succs, ab_ratios) =
|
blanchet@35866
|
54 |
MinData{succs=succs, ab_ratios=ab_ratios}
|
nipkow@32571
|
55 |
|
nipkow@32990
|
56 |
fun make_me_data (calls,success,proofs,time,timeout,lemmas,posns) =
|
nipkow@32810
|
57 |
MeData{calls=calls, success=success, proofs=proofs, time=time,
|
nipkow@32990
|
58 |
timeout=timeout, lemmas=lemmas, posns=posns}
|
boehmes@32521
|
59 |
|
boehmes@34033
|
60 |
val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0)
|
boehmes@34033
|
61 |
val empty_min_data = make_min_data(0, 0, 0)
|
boehmes@34033
|
62 |
val empty_me_data = make_me_data(0, 0, 0, 0, 0, (0,0,0), [])
|
boehmes@32521
|
63 |
|
boehmes@34033
|
64 |
fun tuple_of_sh_data (ShData {calls, success, lemmas, max_lems, time_isa,
|
boehmes@34033
|
65 |
time_atp, time_atp_fail}) = (calls, success, lemmas, max_lems, time_isa,
|
boehmes@34033
|
66 |
time_atp, time_atp_fail)
|
boehmes@32521
|
67 |
|
blanchet@35866
|
68 |
fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
|
nipkow@32533
|
69 |
|
boehmes@34033
|
70 |
fun tuple_of_me_data (MeData {calls, success, proofs, time, timeout, lemmas,
|
boehmes@34033
|
71 |
posns}) = (calls, success, proofs, time, timeout, lemmas, posns)
|
nipkow@32571
|
72 |
|
boehmes@34033
|
73 |
|
boehmes@34033
|
74 |
datatype metis = Unminimized | Minimized | UnminimizedFT | MinimizedFT
|
boehmes@34033
|
75 |
|
boehmes@34033
|
76 |
datatype data = Data of {
|
boehmes@34033
|
77 |
sh: sh_data,
|
boehmes@34033
|
78 |
min: min_data,
|
boehmes@34033
|
79 |
me_u: me_data, (* metis with unminimized set of lemmas *)
|
boehmes@34033
|
80 |
me_m: me_data, (* metis with minimized set of lemmas *)
|
boehmes@34033
|
81 |
me_uft: me_data, (* metis with unminimized set of lemmas and fully-typed *)
|
boehmes@34033
|
82 |
me_mft: me_data, (* metis with minimized set of lemmas and fully-typed *)
|
boehmes@34033
|
83 |
mini: bool (* with minimization *)
|
boehmes@34033
|
84 |
}
|
boehmes@34033
|
85 |
|
boehmes@34033
|
86 |
fun make_data (sh, min, me_u, me_m, me_uft, me_mft, mini) =
|
boehmes@34033
|
87 |
Data {sh=sh, min=min, me_u=me_u, me_m=me_m, me_uft=me_uft, me_mft=me_mft,
|
boehmes@34033
|
88 |
mini=mini}
|
boehmes@34033
|
89 |
|
boehmes@34033
|
90 |
val empty_data = make_data (empty_sh_data, empty_min_data,
|
boehmes@34033
|
91 |
empty_me_data, empty_me_data, empty_me_data, empty_me_data, false)
|
boehmes@34033
|
92 |
|
boehmes@34033
|
93 |
fun map_sh_data f (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
|
boehmes@34033
|
94 |
let val sh' = make_sh_data (f (tuple_of_sh_data sh))
|
boehmes@34033
|
95 |
in make_data (sh', min, me_u, me_m, me_uft, me_mft, mini) end
|
boehmes@34033
|
96 |
|
boehmes@34033
|
97 |
fun map_min_data f (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
|
boehmes@34033
|
98 |
let val min' = make_min_data (f (tuple_of_min_data min))
|
boehmes@34033
|
99 |
in make_data (sh, min', me_u, me_m, me_uft, me_mft, mini) end
|
boehmes@34033
|
100 |
|
boehmes@34033
|
101 |
fun map_me_data f m (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
|
boehmes@34033
|
102 |
let
|
boehmes@34033
|
103 |
fun map_me g Unminimized (u, m, uft, mft) = (g u, m, uft, mft)
|
boehmes@34033
|
104 |
| map_me g Minimized (u, m, uft, mft) = (u, g m, uft, mft)
|
boehmes@34033
|
105 |
| map_me g UnminimizedFT (u, m, uft, mft) = (u, m, g uft, mft)
|
boehmes@34033
|
106 |
| map_me g MinimizedFT (u, m, uft, mft) = (u, m, uft, g mft)
|
boehmes@34033
|
107 |
|
boehmes@34033
|
108 |
val f' = make_me_data o f o tuple_of_me_data
|
boehmes@34033
|
109 |
|
boehmes@34033
|
110 |
val (me_u', me_m', me_uft', me_mft') =
|
boehmes@34033
|
111 |
map_me f' m (me_u, me_m, me_uft, me_mft)
|
boehmes@34033
|
112 |
in make_data (sh, min, me_u', me_m', me_uft', me_mft', mini) end
|
boehmes@34033
|
113 |
|
boehmes@34033
|
114 |
fun set_mini mini (Data {sh, min, me_u, me_m, me_uft, me_mft, ...}) =
|
boehmes@34033
|
115 |
make_data (sh, min, me_u, me_m, me_uft, me_mft, mini)
|
nipkow@32990
|
116 |
|
nipkow@32990
|
117 |
fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n));
|
nipkow@32536
|
118 |
|
nipkow@32810
|
119 |
val inc_sh_calls = map_sh_data
|
nipkow@32810
|
120 |
(fn (calls, success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
|
nipkow@32810
|
121 |
=> (calls + 1, success, lemmas,max_lems, time_isa, time_atp, time_atp_fail))
|
boehmes@32521
|
122 |
|
nipkow@32810
|
123 |
val inc_sh_success = map_sh_data
|
nipkow@32810
|
124 |
(fn (calls, success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
|
nipkow@32810
|
125 |
=> (calls, success + 1, lemmas,max_lems, time_isa, time_atp, time_atp_fail))
|
nipkow@32585
|
126 |
|
nipkow@32810
|
127 |
fun inc_sh_lemmas n = map_sh_data
|
nipkow@32810
|
128 |
(fn (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail)
|
nipkow@32810
|
129 |
=> (calls,success,lemmas+n,max_lems,time_isa,time_atp,time_atp_fail))
|
boehmes@32521
|
130 |
|
nipkow@32810
|
131 |
fun inc_sh_max_lems n = map_sh_data
|
nipkow@32810
|
132 |
(fn (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail)
|
nipkow@32810
|
133 |
=> (calls,success,lemmas,Int.max(max_lems,n),time_isa,time_atp,time_atp_fail))
|
nipkow@32549
|
134 |
|
nipkow@32810
|
135 |
fun inc_sh_time_isa t = map_sh_data
|
nipkow@32810
|
136 |
(fn (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail)
|
nipkow@32810
|
137 |
=> (calls,success,lemmas,max_lems,time_isa + t,time_atp,time_atp_fail))
|
nipkow@32549
|
138 |
|
nipkow@32810
|
139 |
fun inc_sh_time_atp t = map_sh_data
|
nipkow@32810
|
140 |
(fn (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail)
|
nipkow@32810
|
141 |
=> (calls,success,lemmas,max_lems,time_isa,time_atp + t,time_atp_fail))
|
nipkow@32571
|
142 |
|
nipkow@32810
|
143 |
fun inc_sh_time_atp_fail t = map_sh_data
|
nipkow@32810
|
144 |
(fn (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail)
|
nipkow@32810
|
145 |
=> (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail + t))
|
nipkow@32571
|
146 |
|
nipkow@32810
|
147 |
val inc_min_succs = map_min_data
|
blanchet@35866
|
148 |
(fn (succs,ab_ratios) => (succs+1, ab_ratios))
|
nipkow@32609
|
149 |
|
nipkow@32810
|
150 |
fun inc_min_ab_ratios r = map_min_data
|
blanchet@35866
|
151 |
(fn (succs, ab_ratios) => (succs, ab_ratios+r))
|
nipkow@32549
|
152 |
|
nipkow@32551
|
153 |
val inc_metis_calls = map_me_data
|
nipkow@32990
|
154 |
(fn (calls,success,proofs,time,timeout,lemmas,posns)
|
nipkow@32990
|
155 |
=> (calls + 1, success, proofs, time, timeout, lemmas,posns))
|
nipkow@32549
|
156 |
|
nipkow@32551
|
157 |
val inc_metis_success = map_me_data
|
nipkow@32990
|
158 |
(fn (calls,success,proofs,time,timeout,lemmas,posns)
|
nipkow@32990
|
159 |
=> (calls, success + 1, proofs, time, timeout, lemmas,posns))
|
nipkow@32676
|
160 |
|
nipkow@32676
|
161 |
val inc_metis_proofs = map_me_data
|
nipkow@32990
|
162 |
(fn (calls,success,proofs,time,timeout,lemmas,posns)
|
nipkow@32990
|
163 |
=> (calls, success, proofs + 1, time, timeout, lemmas,posns))
|
nipkow@32549
|
164 |
|
boehmes@34033
|
165 |
fun inc_metis_time m t = map_me_data
|
nipkow@32990
|
166 |
(fn (calls,success,proofs,time,timeout,lemmas,posns)
|
boehmes@34033
|
167 |
=> (calls, success, proofs, time + t, timeout, lemmas,posns)) m
|
nipkow@32549
|
168 |
|
nipkow@32551
|
169 |
val inc_metis_timeout = map_me_data
|
nipkow@32990
|
170 |
(fn (calls,success,proofs,time,timeout,lemmas,posns)
|
nipkow@32990
|
171 |
=> (calls, success, proofs, time, timeout + 1, lemmas,posns))
|
nipkow@32549
|
172 |
|
boehmes@34033
|
173 |
fun inc_metis_lemmas m n = map_me_data
|
nipkow@32990
|
174 |
(fn (calls,success,proofs,time,timeout,lemmas,posns)
|
boehmes@34033
|
175 |
=> (calls, success, proofs, time, timeout, inc_max n lemmas, posns)) m
|
nipkow@32549
|
176 |
|
boehmes@34033
|
177 |
fun inc_metis_posns m pos = map_me_data
|
nipkow@32990
|
178 |
(fn (calls,success,proofs,time,timeout,lemmas,posns)
|
boehmes@34033
|
179 |
=> (calls, success, proofs, time, timeout, lemmas, pos::posns)) m
|
boehmes@32521
|
180 |
|
boehmes@32521
|
181 |
local
|
boehmes@32521
|
182 |
|
boehmes@32521
|
183 |
val str = string_of_int
|
boehmes@32521
|
184 |
val str3 = Real.fmt (StringCvt.FIX (SOME 3))
|
boehmes@32521
|
185 |
fun percentage a b = string_of_int (a * 100 div b)
|
boehmes@32521
|
186 |
fun time t = Real.fromInt t / 1000.0
|
boehmes@32521
|
187 |
fun avg_time t n =
|
boehmes@32521
|
188 |
if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0
|
boehmes@32521
|
189 |
|
boehmes@34033
|
190 |
fun log_sh_data log
|
boehmes@34033
|
191 |
(calls, success, lemmas, max_lems, time_isa, time_atp, time_atp_fail) =
|
nipkow@32810
|
192 |
(log ("Total number of sledgehammer calls: " ^ str calls);
|
nipkow@32810
|
193 |
log ("Number of successful sledgehammer calls: " ^ str success);
|
nipkow@32810
|
194 |
log ("Number of sledgehammer lemmas: " ^ str lemmas);
|
nipkow@32810
|
195 |
log ("Max number of sledgehammer lemmas: " ^ str max_lems);
|
nipkow@32810
|
196 |
log ("Success rate: " ^ percentage success calls ^ "%");
|
nipkow@32810
|
197 |
log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa));
|
nipkow@32810
|
198 |
log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_atp));
|
nipkow@32810
|
199 |
log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_atp_fail));
|
nipkow@32536
|
200 |
log ("Average time for sledgehammer calls (Isabelle): " ^
|
nipkow@32810
|
201 |
str3 (avg_time time_isa calls));
|
nipkow@32533
|
202 |
log ("Average time for successful sledgehammer calls (ATP): " ^
|
nipkow@32810
|
203 |
str3 (avg_time time_atp success));
|
nipkow@32536
|
204 |
log ("Average time for failed sledgehammer calls (ATP): " ^
|
nipkow@32810
|
205 |
str3 (avg_time time_atp_fail (calls - success)))
|
nipkow@32533
|
206 |
)
|
boehmes@32521
|
207 |
|
nipkow@32551
|
208 |
|
nipkow@32551
|
209 |
fun str_of_pos pos =
|
nipkow@32551
|
210 |
let val str0 = string_of_int o the_default 0
|
nipkow@32551
|
211 |
in str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) end
|
nipkow@32551
|
212 |
|
boehmes@34033
|
213 |
fun log_me_data log tag sh_calls (metis_calls, metis_success,
|
boehmes@34033
|
214 |
metis_proofs, metis_time, metis_timeout, (lemmas, lems_sos, lems_max),
|
boehmes@34033
|
215 |
metis_posns) =
|
nipkow@32549
|
216 |
(log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls);
|
wenzelm@32740
|
217 |
log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^
|
wenzelm@32740
|
218 |
" (proof: " ^ str metis_proofs ^ ")");
|
nipkow@32549
|
219 |
log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout);
|
nipkow@32533
|
220 |
log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
|
nipkow@32990
|
221 |
log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str lemmas);
|
nipkow@32990
|
222 |
log ("SOS of successful " ^ tag ^ "metis lemmas: " ^ str lems_sos);
|
nipkow@32990
|
223 |
log ("Max number of successful " ^ tag ^ "metis lemmas: " ^ str lems_max);
|
nipkow@32990
|
224 |
log ("Total time for successful " ^ tag ^ "metis calls: " ^ str3 (time metis_time));
|
boehmes@34033
|
225 |
log ("Average time for successful " ^ tag ^ "metis calls: " ^
|
nipkow@32551
|
226 |
str3 (avg_time metis_time metis_success));
|
nipkow@32551
|
227 |
if tag=""
|
nipkow@32551
|
228 |
then log ("Proved: " ^ space_implode " " (map str_of_pos metis_posns))
|
nipkow@32551
|
229 |
else ()
|
nipkow@32551
|
230 |
)
|
nipkow@32571
|
231 |
|
blanchet@35866
|
232 |
fun log_min_data log (succs, ab_ratios) =
|
nipkow@32609
|
233 |
(log ("Number of successful minimizations: " ^ string_of_int succs);
|
blanchet@35866
|
234 |
log ("After/before ratios: " ^ string_of_int ab_ratios)
|
nipkow@32571
|
235 |
)
|
nipkow@32571
|
236 |
|
boehmes@32521
|
237 |
in
|
boehmes@32521
|
238 |
|
boehmes@34033
|
239 |
fun log_data id log (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
|
boehmes@34033
|
240 |
let
|
boehmes@34033
|
241 |
val ShData {calls=sh_calls, ...} = sh
|
boehmes@34033
|
242 |
|
boehmes@34033
|
243 |
fun app_if (MeData {calls, ...}) f = if calls > 0 then f () else ()
|
boehmes@34033
|
244 |
fun log_me tag m =
|
boehmes@34033
|
245 |
log_me_data log tag sh_calls (tuple_of_me_data m)
|
boehmes@34033
|
246 |
fun log_metis (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
|
boehmes@34033
|
247 |
(log_me tag1 m1; log ""; app_if m2 (fn () => log_me tag2 m2)))
|
boehmes@34033
|
248 |
in
|
boehmes@34033
|
249 |
if sh_calls > 0
|
boehmes@34033
|
250 |
then
|
boehmes@34033
|
251 |
(log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
|
boehmes@34033
|
252 |
log_sh_data log (tuple_of_sh_data sh);
|
boehmes@34033
|
253 |
log "";
|
boehmes@34033
|
254 |
if not mini
|
boehmes@34033
|
255 |
then log_metis ("", me_u) ("fully-typed ", me_uft)
|
boehmes@34033
|
256 |
else
|
boehmes@34033
|
257 |
app_if me_u (fn () =>
|
boehmes@34033
|
258 |
(log_metis ("unminimized ", me_u) ("unminimized fully-typed ", me_uft);
|
boehmes@34033
|
259 |
log "";
|
boehmes@34033
|
260 |
app_if me_m (fn () =>
|
boehmes@34033
|
261 |
(log_min_data log (tuple_of_min_data min); log "";
|
boehmes@34033
|
262 |
log_metis ("", me_m) ("fully-typed ", me_mft))))))
|
boehmes@34033
|
263 |
else ()
|
boehmes@34033
|
264 |
end
|
boehmes@32521
|
265 |
|
boehmes@32521
|
266 |
end
|
boehmes@32521
|
267 |
|
boehmes@32521
|
268 |
|
boehmes@32521
|
269 |
(* Warning: we implicitly assume single-threaded execution here! *)
|
wenzelm@32740
|
270 |
val data = Unsynchronized.ref ([] : (int * data) list)
|
boehmes@32521
|
271 |
|
wenzelm@32740
|
272 |
fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy)
|
wenzelm@32567
|
273 |
fun done id ({log, ...}: Mirabelle.done_args) =
|
boehmes@32521
|
274 |
AList.lookup (op =) (!data) id
|
boehmes@32521
|
275 |
|> Option.map (log_data id log)
|
boehmes@32521
|
276 |
|> K ()
|
boehmes@32521
|
277 |
|
wenzelm@32740
|
278 |
fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())
|
boehmes@32521
|
279 |
|
boehmes@32521
|
280 |
|
boehmes@32525
|
281 |
fun get_atp thy args =
|
boehmes@33016
|
282 |
let
|
boehmes@33016
|
283 |
fun default_atp_name () = hd (ATP_Manager.get_atps ())
|
boehmes@33016
|
284 |
handle Empty => error "No ATP available."
|
boehmes@33016
|
285 |
fun get_prover name =
|
boehmes@33016
|
286 |
(case ATP_Manager.get_prover thy name of
|
boehmes@33016
|
287 |
SOME prover => (name, prover)
|
boehmes@33016
|
288 |
| NONE => error ("Bad ATP: " ^ quote name))
|
boehmes@33016
|
289 |
in
|
boehmes@33016
|
290 |
(case AList.lookup (op =) args proverK of
|
boehmes@33016
|
291 |
SOME name => get_prover name
|
boehmes@33016
|
292 |
| NONE => get_prover (default_atp_name ()))
|
boehmes@33016
|
293 |
end
|
boehmes@32525
|
294 |
|
boehmes@32521
|
295 |
local
|
boehmes@32521
|
296 |
|
nipkow@32536
|
297 |
datatype sh_result =
|
nipkow@32536
|
298 |
SH_OK of int * int * string list |
|
nipkow@32536
|
299 |
SH_FAIL of int * int |
|
nipkow@32536
|
300 |
SH_ERROR
|
nipkow@32536
|
301 |
|
boehmes@32864
|
302 |
fun run_sh prover hard_timeout timeout dir st =
|
boehmes@32521
|
303 |
let
|
wenzelm@35596
|
304 |
val {context = ctxt, facts, goal} = Proof.goal st
|
boehmes@33239
|
305 |
val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d | _ => I)
|
boehmes@33239
|
306 |
val ctxt' =
|
boehmes@33239
|
307 |
ctxt
|
boehmes@33239
|
308 |
|> change_dir dir
|
boehmes@33239
|
309 |
|> Config.put ATP_Wrapper.measure_runtime true
|
blanchet@35867
|
310 |
val problem = ATP_Manager.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
|
boehmes@32864
|
311 |
|
boehmes@32573
|
312 |
val time_limit =
|
boehmes@32573
|
313 |
(case hard_timeout of
|
boehmes@32573
|
314 |
NONE => I
|
boehmes@32573
|
315 |
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
|
blanchet@35867
|
316 |
val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Manager.prover_result,
|
wenzelm@32985
|
317 |
time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout
|
boehmes@32521
|
318 |
in
|
boehmes@32864
|
319 |
if success then (message, SH_OK (time_isa, time_atp, theorem_names))
|
nipkow@32536
|
320 |
else (message, SH_FAIL(time_isa, time_atp))
|
boehmes@32521
|
321 |
end
|
blanchet@35830
|
322 |
handle Sledgehammer_HOL_Clause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
|
nipkow@32536
|
323 |
| ERROR msg => ("error: " ^ msg, SH_ERROR)
|
boehmes@32573
|
324 |
| TimeLimit.TimeOut => ("timeout", SH_ERROR)
|
boehmes@32521
|
325 |
|
boehmes@32454
|
326 |
fun thms_of_name ctxt name =
|
boehmes@32454
|
327 |
let
|
boehmes@32454
|
328 |
val lex = OuterKeyword.get_lexicons
|
boehmes@32454
|
329 |
val get = maps (ProofContext.get_fact ctxt o fst)
|
boehmes@32454
|
330 |
in
|
boehmes@32454
|
331 |
Source.of_string name
|
boehmes@32454
|
332 |
|> Symbol.source {do_recover=false}
|
boehmes@32454
|
333 |
|> OuterLex.source {do_recover=SOME false} lex Position.start
|
boehmes@32454
|
334 |
|> OuterLex.source_proper
|
boehmes@32454
|
335 |
|> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE
|
boehmes@32454
|
336 |
|> Source.exhaust
|
boehmes@32454
|
337 |
end
|
boehmes@32452
|
338 |
|
boehmes@32498
|
339 |
in
|
boehmes@32498
|
340 |
|
wenzelm@32567
|
341 |
fun run_sledgehammer args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
|
boehmes@32385
|
342 |
let
|
nipkow@32536
|
343 |
val _ = change_data id inc_sh_calls
|
boehmes@32864
|
344 |
val (prover_name, prover) = get_atp (Proof.theory_of st) args
|
boehmes@32525
|
345 |
val dir = AList.lookup (op =) args keepK
|
boehmes@32541
|
346 |
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
|
boehmes@32573
|
347 |
val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK
|
boehmes@32573
|
348 |
|> Option.map (fst o read_int o explode)
|
boehmes@32864
|
349 |
val (msg, result) = run_sh prover hard_timeout timeout dir st
|
boehmes@32525
|
350 |
in
|
nipkow@32536
|
351 |
case result of
|
nipkow@32536
|
352 |
SH_OK (time_isa, time_atp, names) =>
|
nipkow@32810
|
353 |
let fun get_thms name = (name, thms_of_name (Proof.context_of st) name)
|
boehmes@32525
|
354 |
in
|
nipkow@32810
|
355 |
change_data id inc_sh_success;
|
nipkow@32810
|
356 |
change_data id (inc_sh_lemmas (length names));
|
nipkow@32810
|
357 |
change_data id (inc_sh_max_lems (length names));
|
nipkow@32810
|
358 |
change_data id (inc_sh_time_isa time_isa);
|
nipkow@32810
|
359 |
change_data id (inc_sh_time_atp time_atp);
|
nipkow@32810
|
360 |
named_thms := SOME (map get_thms names);
|
nipkow@32536
|
361 |
log (sh_tag id ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
|
nipkow@32536
|
362 |
string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
|
boehmes@32525
|
363 |
end
|
nipkow@32536
|
364 |
| SH_FAIL (time_isa, time_atp) =>
|
nipkow@32536
|
365 |
let
|
nipkow@32536
|
366 |
val _ = change_data id (inc_sh_time_isa time_isa)
|
nipkow@32536
|
367 |
val _ = change_data id (inc_sh_time_atp_fail time_atp)
|
nipkow@32536
|
368 |
in log (sh_tag id ^ "failed: " ^ msg) end
|
nipkow@32536
|
369 |
| SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)
|
boehmes@32525
|
370 |
end
|
boehmes@32525
|
371 |
|
boehmes@32525
|
372 |
end
|
boehmes@32525
|
373 |
|
boehmes@32525
|
374 |
|
wenzelm@32567
|
375 |
fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
|
boehmes@32525
|
376 |
let
|
blanchet@35866
|
377 |
open ATP_Minimal
|
nipkow@32571
|
378 |
val n0 = length (these (!named_thms))
|
boehmes@32525
|
379 |
val (prover_name, prover) = get_atp (Proof.theory_of st) args
|
blanchet@35866
|
380 |
val minimize = minimize_theorems linear_minimize prover prover_name
|
boehmes@32525
|
381 |
val timeout =
|
boehmes@32525
|
382 |
AList.lookup (op =) args minimize_timeoutK
|
boehmes@32525
|
383 |
|> Option.map (fst o read_int o explode)
|
boehmes@32525
|
384 |
|> the_default 5
|
boehmes@32525
|
385 |
val _ = log separator
|
boehmes@32525
|
386 |
in
|
nipkow@32571
|
387 |
case minimize timeout st (these (!named_thms)) of
|
nipkow@32571
|
388 |
(SOME (named_thms',its), msg) =>
|
nipkow@32609
|
389 |
(change_data id inc_min_succs;
|
nipkow@32609
|
390 |
change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
|
nipkow@32571
|
391 |
if length named_thms' = n0
|
nipkow@32571
|
392 |
then log (minimize_tag id ^ "already minimal")
|
nipkow@32571
|
393 |
else (named_thms := SOME named_thms';
|
nipkow@32571
|
394 |
log (minimize_tag id ^ "succeeded:\n" ^ msg))
|
nipkow@32571
|
395 |
)
|
nipkow@32571
|
396 |
| (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg)
|
boehmes@32525
|
397 |
end
|
boehmes@32525
|
398 |
|
boehmes@32525
|
399 |
|
boehmes@34033
|
400 |
fun run_metis full m name named_thms id
|
wenzelm@32567
|
401 |
({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
|
boehmes@32525
|
402 |
let
|
boehmes@34033
|
403 |
fun metis thms ctxt =
|
blanchet@35830
|
404 |
if full then Metis_Tactics.metisFT_tac ctxt thms
|
blanchet@35830
|
405 |
else Metis_Tactics.metis_tac ctxt thms
|
boehmes@32521
|
406 |
fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
|
boehmes@32521
|
407 |
|
boehmes@32521
|
408 |
fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
|
boehmes@34033
|
409 |
| with_time (true, t) = (change_data id (inc_metis_success m);
|
boehmes@34033
|
410 |
change_data id (inc_metis_lemmas m (length named_thms));
|
boehmes@34033
|
411 |
change_data id (inc_metis_time m t);
|
boehmes@34033
|
412 |
change_data id (inc_metis_posns m pos);
|
boehmes@34033
|
413 |
if name = "proof" then change_data id (inc_metis_proofs m) else ();
|
boehmes@32521
|
414 |
"succeeded (" ^ string_of_int t ^ ")")
|
boehmes@34048
|
415 |
fun timed_metis thms =
|
boehmes@34048
|
416 |
(with_time (Mirabelle.cpu_time apply_metis thms), true)
|
boehmes@34048
|
417 |
handle TimeLimit.TimeOut => (change_data id (inc_metis_timeout m);
|
boehmes@34048
|
418 |
("timeout", false))
|
boehmes@34048
|
419 |
| ERROR msg => ("error: " ^ msg, false)
|
boehmes@32521
|
420 |
|
boehmes@32525
|
421 |
val _ = log separator
|
boehmes@34033
|
422 |
val _ = change_data id (inc_metis_calls m)
|
boehmes@32521
|
423 |
in
|
boehmes@32525
|
424 |
maps snd named_thms
|
boehmes@32521
|
425 |
|> timed_metis
|
boehmes@34048
|
426 |
|>> log o prefix (metis_tag id)
|
boehmes@34048
|
427 |
|> snd
|
boehmes@32521
|
428 |
end
|
boehmes@32432
|
429 |
|
boehmes@34033
|
430 |
fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
|
wenzelm@35596
|
431 |
let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
|
wenzelm@35596
|
432 |
if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
|
wenzelm@35596
|
433 |
then () else
|
wenzelm@35596
|
434 |
let
|
wenzelm@35596
|
435 |
val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option)
|
wenzelm@35596
|
436 |
val minimize = AList.defined (op =) args minimizeK
|
wenzelm@35596
|
437 |
val metis_ft = AList.defined (op =) args metis_ftK
|
wenzelm@35596
|
438 |
|
wenzelm@35596
|
439 |
fun apply_metis m1 m2 =
|
wenzelm@35596
|
440 |
if metis_ft
|
wenzelm@35596
|
441 |
then
|
wenzelm@35596
|
442 |
if not (Mirabelle.catch_result metis_tag false
|
wenzelm@35596
|
443 |
(run_metis false m1 name (these (!named_thms))) id st)
|
wenzelm@35596
|
444 |
then
|
wenzelm@35596
|
445 |
(Mirabelle.catch_result metis_tag false
|
wenzelm@35596
|
446 |
(run_metis true m2 name (these (!named_thms))) id st; ())
|
wenzelm@35596
|
447 |
else ()
|
wenzelm@35596
|
448 |
else
|
wenzelm@35596
|
449 |
(Mirabelle.catch_result metis_tag false
|
wenzelm@35596
|
450 |
(run_metis false m1 name (these (!named_thms))) id st; ())
|
wenzelm@35596
|
451 |
in
|
wenzelm@35596
|
452 |
change_data id (set_mini minimize);
|
wenzelm@35596
|
453 |
Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st;
|
wenzelm@35596
|
454 |
if is_some (!named_thms)
|
boehmes@34033
|
455 |
then
|
wenzelm@35596
|
456 |
(apply_metis Unminimized UnminimizedFT;
|
wenzelm@35596
|
457 |
if minimize andalso not (null (these (!named_thms)))
|
boehmes@34048
|
458 |
then
|
wenzelm@35596
|
459 |
(Mirabelle.catch minimize_tag (run_minimize args named_thms) id st;
|
wenzelm@35596
|
460 |
apply_metis Minimized MinimizedFT)
|
wenzelm@35596
|
461 |
else ())
|
wenzelm@35596
|
462 |
else ()
|
wenzelm@35596
|
463 |
end
|
nipkow@32810
|
464 |
end
|
boehmes@32385
|
465 |
|
boehmes@32511
|
466 |
fun invoke args =
|
boehmes@32515
|
467 |
let
|
wenzelm@32937
|
468 |
val _ = ATP_Manager.full_types := AList.defined (op =) args full_typesK
|
boehmes@32521
|
469 |
in Mirabelle.register (init, sledgehammer_action args, done) end
|
boehmes@32385
|
470 |
|
boehmes@32385
|
471 |
end
|