--- 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)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 09:50:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 11:11:34 2010 +0200
@@ -42,13 +42,15 @@
type prover_result =
{outcome: failure option,
- message: string,
used_axioms: (string * locality) list,
- run_time_in_msecs: int}
+ run_time_in_msecs: int option,
+ message: string}
type prover = params -> minimize_command -> prover_problem -> prover_result
val smtN : string
+ val smt_prover_names : string list
+ val smt_default_max_relevant : int
val dest_dir : string Config.T
val problem_prefix : string Config.T
val measure_run_time : bool Config.T
@@ -56,11 +58,7 @@
val kill_provers : unit -> unit
val running_provers : unit -> unit
val messages : int option -> unit
- val run_atp : theory -> string -> prover
- val is_smt_solver_installed : unit -> bool
- val run_smt_solver :
- bool -> params -> minimize_command -> prover_problem
- -> string * (string * locality) list
+ val get_prover : theory -> string -> prover
val run_sledgehammer :
params -> bool -> int -> relevance_override -> (string -> minimize_command)
-> Proof.state -> bool * Proof.state
@@ -87,12 +85,15 @@
val das_Tool = "Sledgehammer"
val smtN = "smt"
-val smt_names = [smtN, remote_prefix ^ smtN]
+val smt_prover_names = [smtN, remote_prefix ^ smtN]
+
+val smt_default_max_relevant = 300 (* FUDGE *)
+val auto_max_relevant_divisor = 2 (* FUDGE *)
fun available_provers thy =
let
val (remote_provers, local_provers) =
- sort_strings (available_atps thy) @ smt_names
+ sort_strings (available_atps thy) @ smt_prover_names
|> List.partition (String.isPrefix remote_prefix)
in
priority ("Available provers: " ^ commas (local_provers @ remote_provers) ^
@@ -135,7 +136,7 @@
{outcome: failure option,
message: string,
used_axioms: (string * locality) list,
- run_time_in_msecs: int}
+ run_time_in_msecs: int option}
type prover = params -> minimize_command -> prover_problem -> prover_result
@@ -180,6 +181,9 @@
fun prepared_axiom ctxt (Unprepared p) = prepare_axiom ctxt p
| prepared_axiom _ (Prepared p) = p
+fun int_option_add (SOME m) (SOME n) = SOME (m + n)
+ | int_option_add _ _ = NONE
+
(* Important messages are important but not so important that users want to see
them each time. *)
val important_message_keep_factor = 0.1
@@ -232,7 +236,7 @@
val digit = Scan.one Symbol.is_ascii_digit;
val num3 = as_num (digit ::: digit ::: (digit >> single));
val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
- val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
+ val as_time = Scan.read Symbol.stopper time o explode
in (output, as_time t) end;
fun run_on probfile =
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
@@ -250,7 +254,7 @@
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
else
I)
- |>> (if measure_run_time then split_time else rpair 0)
+ |>> (if measure_run_time then split_time else rpair NONE)
val (tstplike_proof, outcome) =
extract_tstplike_proof_and_outcome complete res_code
proof_delims known_failures output
@@ -277,7 +281,8 @@
? (fn (_, msecs0, _, SOME _) =>
run true (Time.- (timeout, Timer.checkRealTimer timer))
|> (fn (output, msecs, tstplike_proof, outcome) =>
- (output, msecs0 + msecs, tstplike_proof, outcome))
+ (output, int_option_add msecs0 msecs,
+ tstplike_proof, outcome))
| result => result)
in ((pool, conjecture_shape, axiom_names), result) end
else
@@ -312,8 +317,8 @@
axiom_names, goal, subgoal)
|>> (fn message =>
message ^ (if verbose then
- "\nATP real CPU time: " ^ string_of_int msecs ^
- " ms."
+ "\nATP real CPU time: " ^
+ string_of_int (the msecs) ^ " ms."
else
"") ^
(if important_message <> "" then
@@ -327,12 +332,12 @@
run_time_in_msecs = msecs}
end
-fun run_atp thy name = atp_fun false name (get_atp thy name)
+fun get_atp_as_prover thy name = atp_fun false name (get_atp thy name)
fun run_atp_somehow (params as {blocking, debug, max_relevant, timeout,
expect, ...})
auto i n minimize_command
- (prover_problem as {state, goal, axioms, ...})
+ (problem as {state, goal, axioms, ...})
(prover as {default_max_relevant, ...}, atp_name) =
let
val ctxt = Proof.context_of state
@@ -345,7 +350,7 @@
let
fun really_go () =
atp_fun auto atp_name prover params (minimize_command atp_name)
- prover_problem
+ problem
|> (fn {outcome, message, ...} =>
(if is_some outcome then "none" else "some", message))
val (outcome_code, message) =
@@ -383,37 +388,49 @@
end
(* FIXME: dummy *)
-fun is_smt_solver_installed () = true
-
-(* FIXME: dummy *)
-fun raw_run_smt_solver remote timeout state axioms i =
- ("", axioms |> take 5 |> map fst)
+fun run_smt_solver remote timeout state axioms i =
+ {outcome = NONE, used_axioms = axioms |> take 5 |> map fst,
+ run_time_in_msecs = NONE}
-fun run_smt_solver remote ({timeout, ...} : params) minimize_command
- ({state, subgoal, axioms, ...} : prover_problem) =
- raw_run_smt_solver remote timeout state
+fun get_smt_solver_as_prover remote ({timeout, ...} : params) minimize_command
+ ({state, subgoal, axioms, ...} : prover_problem) =
+ let
+ val {outcome, used_axioms, run_time_in_msecs} =
+ run_smt_solver remote timeout state
(map_filter (try dest_Unprepared) axioms) subgoal
+ val message =
+ if outcome = NONE then
+ sendback_line (proof_banner false)
+ (apply_on_subgoal subgoal (subgoal_count state) ^
+ command_call smtN (map fst used_axioms))
+ else
+ ""
+ in
+ {outcome = outcome, used_axioms = used_axioms,
+ run_time_in_msecs = run_time_in_msecs, message = message}
+ end
-fun run_smt_solver_somehow state (params as {timeout, ...}) i n goal axioms
+fun get_prover thy name =
+ if member (op =) smt_prover_names name then
+ get_smt_solver_as_prover (String.isPrefix remote_prefix)
+ else
+ get_atp_as_prover thy name
+
+fun run_smt_solver_somehow state params minimize_command i n goal axioms
(remote, name) =
let
val ctxt = Proof.context_of state
val desc = prover_description ctxt params name (length axioms) i n goal
- val (failure, used_axioms) =
- raw_run_smt_solver remote timeout state axioms i
- val success = (failure = "")
- val message =
- das_Tool ^ ": " ^ desc ^ "\n" ^
- (if success then
- sendback_line (proof_banner false)
- (apply_on_subgoal i n ^
- command_call "smt" (map fst used_axioms))
- else
- "Error: " ^ failure)
- in priority message; success end
-
-val smt_default_max_relevant = 300 (* FUDGE *)
-val auto_max_relevant_divisor = 2 (* FUDGE *)
+ val problem =
+ {state = state, goal = goal, subgoal = i,
+ axioms = axioms |> map Unprepared, only = true}
+ val {outcome, used_axioms, message, ...} =
+ get_smt_solver_as_prover remote params minimize_command problem
+ val _ =
+ priority (das_Tool ^ ": " ^ desc ^ "\n" ^
+ (if outcome = NONE then message
+ else "An unknown error occurred."))
+ in outcome = NONE end
fun run_sledgehammer (params as {blocking, provers, full_types,
relevance_thresholds, max_relevant, timeout,
@@ -433,7 +450,7 @@
val _ = () |> not blocking ? kill_provers
val _ = if auto then () else priority "Sledgehammering..."
val (smts, atps) =
- provers |> List.partition (member (op =) smt_names)
+ provers |> List.partition (member (op =) smt_prover_names)
|>> (take 1 #> map (`(String.isPrefix remote_prefix)))
||> map (`(get_atp thy))
fun run_atps (res as (success, state)) =
@@ -451,12 +468,12 @@
relevant_facts ctxt full_types relevance_thresholds
max_max_relevant relevance_override chained_ths
hyp_ts concl_t
- val prover_problem =
+ val problem =
{state = state, goal = goal, subgoal = i,
axioms = axioms |> map (Prepared o prepare_axiom ctxt),
only = only}
val run_atp_somehow =
- run_atp_somehow params auto i n minimize_command prover_problem
+ run_atp_somehow params auto i n minimize_command problem
in
if auto then
fold (fn prover => fn (true, state) => (true, state)
@@ -478,7 +495,8 @@
max_relevant relevance_override chained_ths
hyp_ts concl_t
in
- smts |> map (run_smt_solver_somehow state params i n goal axioms)
+ smts |> map (run_smt_solver_somehow state params minimize_command i
+ n goal axioms)
|> exists I |> rpair state
end
fun run_atps_and_smt_solvers () =