--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 09:50:18 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 11:11:34 2010 +0200
@@ -29,8 +29,8 @@
lemmas: int,
max_lems: int,
time_isa: int,
- time_atp: int,
- time_atp_fail: int}
+ time_prover: int,
+ time_prover_fail: int}
datatype me_data = MeData of {
calls: int,
@@ -51,10 +51,11 @@
fun make_sh_data
(calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa,
- time_atp,time_atp_fail) =
+ time_prover,time_prover_fail) =
ShData{calls=calls, success=success, nontriv_calls=nontriv_calls,
nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems,
- time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail}
+ time_isa=time_isa, time_prover=time_prover,
+ time_prover_fail=time_prover_fail}
fun make_min_data (succs, ab_ratios) =
MinData{succs=succs, ab_ratios=ab_ratios}
@@ -71,8 +72,8 @@
fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success,
lemmas, max_lems, time_isa,
- time_atp, time_atp_fail}) = (calls, success, nontriv_calls, nontriv_success,
- lemmas, max_lems, time_isa, time_atp, time_atp_fail)
+ time_prover, time_prover_fail}) = (calls, success, nontriv_calls,
+ nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)
fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
@@ -127,40 +128,40 @@
fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n));
val inc_sh_calls = map_sh_data
- (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
- => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_atp, time_atp_fail))
+ (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
+ => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail))
val inc_sh_success = map_sh_data
- (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
- => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail))
+ (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
+ => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail))
val inc_sh_nontriv_calls = map_sh_data
- (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
- => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_atp, time_atp_fail))
+ (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
+ => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail))
val inc_sh_nontriv_success = map_sh_data
- (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
- => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_atp, time_atp_fail))
+ (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
+ => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail))
fun inc_sh_lemmas n = map_sh_data
- (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail)
- => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_atp,time_atp_fail))
+ (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
+ => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail))
fun inc_sh_max_lems n = map_sh_data
- (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail)
- => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_atp,time_atp_fail))
+ (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
+ => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail))
fun inc_sh_time_isa t = map_sh_data
- (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail)
- => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_atp,time_atp_fail))
+ (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
+ => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail))
-fun inc_sh_time_atp t = map_sh_data
- (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail)
- => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp + t,time_atp_fail))
+fun inc_sh_time_prover t = map_sh_data
+ (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
+ => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail))
-fun inc_sh_time_atp_fail t = map_sh_data
- (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail)
- => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail + t))
+fun inc_sh_time_prover_fail t = map_sh_data
+ (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
+ => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t))
val inc_min_succs = map_min_data
(fn (succs,ab_ratios) => (succs+1, ab_ratios))
@@ -214,7 +215,7 @@
if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0
fun log_sh_data log
- (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_atp, time_atp_fail) =
+ (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) =
(log ("Total number of sledgehammer calls: " ^ str calls);
log ("Number of successful sledgehammer calls: " ^ str success);
log ("Number of sledgehammer lemmas: " ^ str lemmas);
@@ -223,14 +224,14 @@
log ("Total number of nontrivial sledgehammer calls: " ^ str nontriv_calls);
log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success);
log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa));
- log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_atp));
- log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_atp_fail));
+ log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover));
+ log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail));
log ("Average time for sledgehammer calls (Isabelle): " ^
str3 (avg_time time_isa calls));
log ("Average time for successful sledgehammer calls (ATP): " ^
- str3 (avg_time time_atp success));
+ str3 (avg_time time_prover success));
log ("Average time for failed sledgehammer calls (ATP): " ^
- str3 (avg_time time_atp_fail (calls - success)))
+ str3 (avg_time time_prover_fail (calls - success)))
)
@@ -313,16 +314,16 @@
fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())
-fun get_atp thy args =
+fun get_prover thy args =
let
- fun default_atp_name () =
+ fun default_prover_name () =
hd (#provers (Sledgehammer_Isar.default_params thy []))
handle Empty => error "No ATP available."
- fun get_atp name = (name, Sledgehammer.run_atp thy name)
+ fun get_prover name = (name, Sledgehammer.get_prover thy name)
in
(case AList.lookup (op =) args proverK of
- SOME name => get_atp name
- | NONE => get_atp (default_atp_name ()))
+ SOME name => get_prover name
+ | NONE => get_prover (default_prover_name ()))
end
type locality = Sledgehammer_Filter.locality
@@ -349,7 +350,11 @@
Sledgehammer_Isar.default_params thy
[("timeout", Int.toString timeout ^ " s")]
val relevance_override = {add = [], del = [], only = false}
- val {default_max_relevant, ...} = ATP_Systems.get_atp thy prover_name
+ val default_max_relevant =
+ if member (op =) Sledgehammer.smt_prover_names prover_name then
+ Sledgehammer.smt_default_max_relevant
+ else
+ #default_max_relevant (ATP_Systems.get_atp thy prover_name)
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
val axioms =
Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds
@@ -362,14 +367,14 @@
(case hard_timeout of
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
- val ({outcome, message, used_axioms, run_time_in_msecs = time_atp, ...}
+ val ({outcome, message, used_axioms, run_time_in_msecs = SOME time_prover, ...}
: Sledgehammer.prover_result,
time_isa) = time_limit (Mirabelle.cpu_time
(prover params (K ""))) problem
in
case outcome of
- NONE => (message, SH_OK (time_isa, time_atp, used_axioms))
- | SOME _ => (message, SH_FAIL (time_isa, time_atp))
+ NONE => (message, SH_OK (time_isa, time_prover, used_axioms))
+ | SOME _ => (message, SH_FAIL (time_isa, time_prover))
end
handle ERROR msg => ("error: " ^ msg, SH_ERROR)
| TimeLimit.TimeOut => ("timeout", SH_ERROR)
@@ -394,7 +399,7 @@
val triv_str = if trivial then "[T] " else ""
val _ = change_data id inc_sh_calls
val _ = if trivial then () else change_data id inc_sh_nontriv_calls
- val (prover_name, prover) = get_atp (Proof.theory_of st) args
+ val (prover_name, prover) = get_prover (Proof.theory_of st) args
val dir = AList.lookup (op =) args keepK
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK
@@ -402,7 +407,7 @@
val (msg, result) = run_sh prover_name prover hard_timeout timeout dir st
in
case result of
- SH_OK (time_isa, time_atp, names) =>
+ SH_OK (time_isa, time_prover, names) =>
let
fun get_thms (_, Sledgehammer_Filter.Chained) = NONE
| get_thms (name, loc) =
@@ -413,15 +418,15 @@
change_data id (inc_sh_lemmas (length names));
change_data id (inc_sh_max_lems (length names));
change_data id (inc_sh_time_isa time_isa);
- change_data id (inc_sh_time_atp time_atp);
+ change_data id (inc_sh_time_prover time_prover);
named_thms := SOME (map_filter get_thms names);
log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
- string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
+ string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
end
- | SH_FAIL (time_isa, time_atp) =>
+ | SH_FAIL (time_isa, time_prover) =>
let
val _ = change_data id (inc_sh_time_isa time_isa)
- val _ = change_data id (inc_sh_time_atp_fail time_atp)
+ val _ = change_data id (inc_sh_time_prover_fail time_prover)
in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end
| SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)
end
@@ -436,7 +441,7 @@
open Metis_Translate
val thy = Proof.theory_of st
val n0 = length (these (!named_thms))
- val (prover_name, _) = get_atp thy args
+ val (prover_name, _) = get_prover thy args
val timeout =
AList.lookup (op =) args minimize_timeoutK
|> Option.map (fst o read_int o explode)