40 |
42 |
41 fun make_sh_data (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) = |
43 fun make_sh_data (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) = |
42 ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa, |
44 ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa, |
43 time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail} |
45 time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail} |
44 |
46 |
45 fun make_me_data (metis_calls, metis_success, metis_time, metis_timeout) = |
47 fun make_me_data (me_calls, me_success, me_time, me_timeout, me_lemmas) = |
46 MeData{calls=metis_calls, success=metis_success, |
48 MeData{calls=me_calls, success=me_success, time=me_time, timeout=me_timeout, lemmas=me_lemmas} |
47 time=metis_time, timeout=metis_timeout} |
49 |
48 |
50 val empty_data = Data(make_sh_data (0, 0, 0, 0, 0), make_me_data(0, 0, 0, 0, 0), make_me_data(0, 0, 0, 0, 0)) |
49 val empty_data = Data(make_sh_data (0, 0, 0, 0, 0), make_me_data(0, 0, 0, 0), make_me_data(0, 0, 0, 0)) |
|
50 |
51 |
51 fun map_sh_data f |
52 fun map_sh_data f |
52 (Data (ShData{calls, success, time_isa, time_atp, time_atp_fail}, meda0, meda)) = |
53 (Data (ShData{calls, success, time_isa, time_atp, time_atp_fail}, meda0, meda)) = |
53 Data (make_sh_data (f (calls, success, time_isa, time_atp, time_atp_fail)), |
54 Data (make_sh_data (f (calls, success, time_isa, time_atp, time_atp_fail)), |
54 meda0, meda) |
55 meda0, meda) |
55 |
56 |
56 fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout}, meda)) = |
57 fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas}, meda)) = |
57 Data(shda, make_me_data(f (calls,success,time,timeout)), meda) |
58 Data(shda, make_me_data(f (calls,success,time,timeout,lemmas)), meda) |
58 |
59 |
59 fun map_me_data f (Data (shda, meda0, MeData{calls,success,time,timeout})) = |
60 fun map_me_data f (Data (shda, meda0, MeData{calls,success,time,timeout,lemmas})) = |
60 Data(shda, meda0, make_me_data(f (calls,success,time,timeout))) |
61 Data(shda, meda0, make_me_data(f (calls,success,time,timeout,lemmas))) |
61 |
62 |
62 val inc_sh_calls = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) |
63 val inc_sh_calls = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) |
63 => (sh_calls + 1, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)) |
64 => (sh_calls + 1, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)) |
64 |
65 |
65 val inc_sh_success = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) |
66 val inc_sh_success = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) |
72 => (sh_calls, sh_success, sh_time_isa, sh_time_atp + t, sh_time_atp_fail)) |
73 => (sh_calls, sh_success, sh_time_isa, sh_time_atp + t, sh_time_atp_fail)) |
73 |
74 |
74 fun inc_sh_time_atp_fail t = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) |
75 fun inc_sh_time_atp_fail t = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) |
75 => (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail + t)) |
76 => (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail + t)) |
76 |
77 |
77 val inc_metis_calls = map_me_data (fn (metis_calls, metis_success, metis_time, metis_timeout) |
78 val inc_metis_calls = map_me_data (fn (calls, success, time, timeout, lemmas) |
78 => (metis_calls + 1, metis_success, metis_time, metis_timeout)) |
79 => (calls + 1, success, time, timeout, lemmas)) |
79 |
80 |
80 val inc_metis_success = map_me_data (fn (metis_calls, metis_success, metis_time, metis_timeout) |
81 val inc_metis_success = map_me_data (fn (calls,success,time,timeout,lemmas) |
81 => (metis_calls, metis_success + 1, metis_time, metis_timeout)) |
82 => (calls, success + 1, time, timeout, lemmas)) |
82 |
83 |
83 fun inc_metis_time t = map_me_data (fn (metis_calls, metis_success, metis_time, metis_timeout) |
84 fun inc_metis_time t = map_me_data (fn (calls,success,time,timeout,lemmas) |
84 => (metis_calls, metis_success, metis_time + t, metis_timeout)) |
85 => (calls, success, time + t, timeout, lemmas)) |
85 |
86 |
86 val inc_metis_timeout = map_me_data (fn (metis_calls, metis_success, metis_time, metis_timeout) |
87 val inc_metis_timeout = map_me_data (fn (calls,success,time,timeout,lemmas) |
87 => (metis_calls, metis_success, metis_time, metis_timeout + 1)) |
88 => (calls, success, time, timeout + 1, lemmas)) |
88 |
89 |
89 val inc_metis_calls0 = map_me_data0 (fn (metis_calls, metis_success, metis_time, metis_timeout) |
90 fun inc_metis_lemmas n = map_me_data (fn (calls,success,time,timeout,lemmas) |
90 => (metis_calls + 1, metis_success, metis_time, metis_timeout)) |
91 => (calls, success, time, timeout, lemmas + n)) |
91 |
92 |
92 val inc_metis_success0 = map_me_data0 (fn (metis_calls, metis_success, metis_time, metis_timeout) |
93 val inc_metis_calls0 = map_me_data0 (fn (calls, success, time, timeout, lemmas) |
93 => (metis_calls, metis_success + 1, metis_time, metis_timeout)) |
94 => (calls + 1, success, time, timeout, lemmas)) |
94 |
95 |
95 fun inc_metis_time0 t = map_me_data0 (fn (metis_calls, metis_success, metis_time, metis_timeout) |
96 val inc_metis_success0 = map_me_data0 (fn (calls,success,time,timeout,lemmas) |
96 => (metis_calls, metis_success, metis_time + t, metis_timeout)) |
97 => (calls, success + 1, time, timeout, lemmas)) |
97 |
98 |
98 val inc_metis_timeout0 = map_me_data0 (fn (metis_calls, metis_success, metis_time, metis_timeout) |
99 fun inc_metis_time0 t = map_me_data0 (fn (calls,success,time,timeout,lemmas) |
99 => (metis_calls, metis_success, metis_time, metis_timeout + 1)) |
100 => (calls, success, time + t, timeout, lemmas)) |
100 |
101 |
|
102 val inc_metis_timeout0 = map_me_data0 (fn (calls,success,time,timeout,lemmas) |
|
103 => (calls, success, time, timeout + 1, lemmas)) |
|
104 |
|
105 fun inc_metis_lemmas0 n = map_me_data0 (fn (calls,success,time,timeout,lemmas) |
|
106 => (calls, success, time, timeout, lemmas + n)) |
101 |
107 |
102 local |
108 local |
103 |
109 |
104 val str = string_of_int |
110 val str = string_of_int |
105 val str3 = Real.fmt (StringCvt.FIX (SOME 3)) |
111 val str3 = Real.fmt (StringCvt.FIX (SOME 3)) |
122 log ("Average time for failed sledgehammer calls (ATP): " ^ |
128 log ("Average time for failed sledgehammer calls (ATP): " ^ |
123 str3 (avg_time sh_time_atp_fail (sh_calls - sh_success))) |
129 str3 (avg_time sh_time_atp_fail (sh_calls - sh_success))) |
124 ) |
130 ) |
125 |
131 |
126 fun log_metis_data log tag sh_calls sh_success metis_calls metis_success metis_time |
132 fun log_metis_data log tag sh_calls sh_success metis_calls metis_success metis_time |
127 metis_timeout = |
133 metis_timeout metis_lemmas = |
128 (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls); |
134 (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls); |
129 log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success); |
135 log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success); |
130 log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout); |
136 log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout); |
131 log ("Number of " ^ tag ^ "metis exceptions: " ^ |
137 log ("Number of " ^ tag ^ "metis exceptions: " ^ |
132 str (sh_success - metis_success - metis_timeout)); |
138 str (sh_success - metis_success - metis_timeout)); |
133 log ("Success rate: " ^ percentage metis_success sh_calls ^ "%"); |
139 log ("Success rate: " ^ percentage metis_success sh_calls ^ "%"); |
|
140 log ("Number of " ^ tag ^ "metis lemmas: " ^ str metis_lemmas); |
134 log ("Total time for successful metis calls: " ^ str3 (time metis_time)); |
141 log ("Total time for successful metis calls: " ^ str3 (time metis_time)); |
135 log ("Average time for successful metis calls: " ^ |
142 log ("Average time for successful metis calls: " ^ |
136 str3 (avg_time metis_time metis_success))) |
143 str3 (avg_time metis_time metis_success))) |
137 |
144 |
138 in |
145 in |
139 |
146 |
140 fun log_data id log (Data (ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa, time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail}, MeData{calls=metis_calls0, |
147 fun log_data id log (Data (ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa, time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail}, MeData{calls=metis_calls0, |
141 success=metis_success0, time=metis_time0, timeout=metis_timeout0}, MeData{calls=metis_calls, |
148 success=metis_success0, time=metis_time0, timeout=metis_timeout0, lemmas=metis_lemmas0}, MeData{calls=metis_calls, |
142 success=metis_success, time=metis_time, timeout=metis_timeout})) = |
149 success=metis_success, time=metis_time, timeout=metis_timeout, lemmas=metis_lemmas})) = |
143 if sh_calls > 0 |
150 if sh_calls > 0 |
144 then |
151 then |
145 (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n"); |
152 (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n"); |
146 log_sh_data log sh_calls sh_success sh_time_isa sh_time_atp sh_time_atp_fail; |
153 log_sh_data log sh_calls sh_success sh_time_isa sh_time_atp sh_time_atp_fail; |
147 log ""; |
154 log ""; |
148 if metis_calls > 0 then log_metis_data log "" sh_calls sh_success metis_calls |
155 if metis_calls > 0 then log_metis_data log "" sh_calls sh_success metis_calls |
149 metis_success metis_time metis_timeout else (); |
156 metis_success metis_time metis_timeout metis_lemmas else (); |
150 log ""; |
157 log ""; |
151 if metis_calls0 > 0 |
158 if metis_calls0 > 0 |
152 then log_metis_data log "unminimized " sh_calls sh_success metis_calls0 |
159 then log_metis_data log "unminimized " sh_calls sh_success metis_calls0 |
153 metis_success0 metis_time0 metis_timeout0 |
160 metis_success0 metis_time0 metis_timeout0 metis_lemmas0 |
154 else () |
161 else () |
155 ) |
162 ) |
156 else () |
163 else () |
157 |
164 |
158 end |
165 end |
292 handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout") |
299 handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout") |
293 | ERROR msg => "error: " ^ msg |
300 | ERROR msg => "error: " ^ msg |
294 |
301 |
295 val _ = log separator |
302 val _ = log separator |
296 val _ = change_data id inc_metis_calls |
303 val _ = change_data id inc_metis_calls |
|
304 val _ = change_data id (inc_metis_lemmas (length named_thms)) |
297 in |
305 in |
298 maps snd named_thms |
306 maps snd named_thms |
299 |> timed_metis |
307 |> timed_metis |
300 |> log o prefix (metis_tag id) |
308 |> log o prefix (metis_tag id) |
301 end |
309 end |
302 |
310 |
303 fun sledgehammer_action args id (st as {log, ...}) = |
311 fun sledgehammer_action args id (st as {log, ...}) = |
304 let |
312 let |
305 val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout) |
313 val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout, inc_metis_lemmas) |
306 val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0, inc_metis_timeout0) |
314 val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0, inc_metis_timeout0, inc_metis_lemmas0) |
307 val named_thms = ref (NONE : (string * thm list) list option) |
315 val named_thms = ref (NONE : (string * thm list) list option) |
308 |
316 |
309 fun if_enabled k f = |
317 fun if_enabled k f = |
310 if AList.defined (op =) args k andalso is_some (!named_thms) |
318 if AList.defined (op =) args k andalso is_some (!named_thms) |
311 then f id st else () |
319 then f id st else () |