--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 30 17:00:38 2011 +0200
@@ -397,9 +397,10 @@
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
fun failed failure =
- ({outcome = SOME failure, message = "", used_facts = [],
- run_time_in_msecs = NONE}, ~1)
- val ({outcome, message, used_facts, run_time_in_msecs}
+ ({outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
+ preplay = K Sledgehammer_ATP_Reconstruct.Failed_to_Play,
+ message = K ""}, ~1)
+ val ({outcome, used_facts, run_time_in_msecs, preplay, message}
: Sledgehammer_Provers.prover_result,
time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
let
@@ -419,10 +420,11 @@
handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
| Fail "inappropriate" => failed ATP_Proof.Inappropriate
val time_prover = run_time_in_msecs |> the_default ~1
+ val msg = message (preplay ())
in
case outcome of
- NONE => (message, SH_OK (time_isa, time_prover, used_facts))
- | SOME _ => (message, SH_FAIL (time_isa, time_prover))
+ NONE => (msg, SH_OK (time_isa, time_prover, used_facts))
+ | SOME _ => (msg, SH_FAIL (time_isa, time_prover))
end
handle ERROR msg => ("error: " ^ msg, SH_ERROR)
@@ -512,9 +514,11 @@
Sledgehammer_Minimize.minimize_facts prover_name params
(SOME explicit_apply) true 1 (Sledgehammer_Util.subgoal_count st)
val _ = log separator
+ val (used_facts, (preplay, message)) = minimize st (these (!named_thms))
+ val msg = message (preplay ())
in
- case minimize st (these (!named_thms)) of
- (SOME named_thms', msg) =>
+ case used_facts of
+ SOME named_thms' =>
(change_data id inc_min_succs;
change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
if length named_thms' = n0
@@ -523,7 +527,7 @@
named_thms := SOME named_thms';
log (minimize_tag id ^ "succeeded:\n" ^ msg))
)
- | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg)
+ | NONE => log (minimize_tag id ^ "failed: " ^ msg)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 30 17:00:38 2011 +0200
@@ -8,13 +8,15 @@
signature SLEDGEHAMMER_MINIMIZE =
sig
type locality = Sledgehammer_Filter.locality
+ type play = Sledgehammer_ATP_Reconstruct.play
type params = Sledgehammer_Provers.params
val binary_min_facts : int Config.T
val minimize_facts :
string -> params -> bool option -> bool -> int -> int -> Proof.state
-> ((string * locality) * thm list) list
- -> ((string * locality) * thm list) list option * string
+ -> ((string * locality) * thm list) list option
+ * ((unit -> play) * (play -> string))
val run_minimize :
params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
end;
@@ -25,6 +27,7 @@
open ATP_Proof
open Sledgehammer_Util
open Sledgehammer_Filter
+open Sledgehammer_ATP_Reconstruct
open Sledgehammer_Provers
(* wrapper for calling external prover *)
@@ -171,7 +174,7 @@
Int.min (msecs, Time.toMilliseconds time + slack_msecs)
|> Time.fromMilliseconds
val facts = filter_used_facts used_facts facts
- val (min_thms, {message, ...}) =
+ val (min_thms, {preplay, message, ...}) =
if length facts >= Config.get ctxt binary_min_facts then
binary_minimize (do_test new_timeout) facts
else
@@ -182,13 +185,16 @@
(case length (filter (curry (op =) Chained o snd o fst) min_thms) of
0 => ""
| n => " (including " ^ string_of_int n ^ " chained)") ^ ".")
- in (SOME min_thms, message) end
- | {outcome = SOME TimedOut, ...} =>
- (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
- \option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ "\").")
- | {message, ...} => (NONE, "Prover error: " ^ message))
- handle ERROR msg => (NONE, "Error: " ^ msg)
+ in (SOME min_thms, (preplay, message)) end
+ | {outcome = SOME TimedOut, preplay, ...} =>
+ (NONE,
+ (preplay,
+ fn _ => "Timeout: You can increase the time limit using the \
+ \\"timeout\" option (e.g., \"timeout = " ^
+ string_of_int (10 + msecs div 1000) ^ "\")."))
+ | {preplay, message, ...} =>
+ (NONE, (preplay, prefix "Prover error: " o message)))
+ handle ERROR msg => (NONE, (K Failed_to_Play, fn _ => "Error: " ^ msg))
end
fun run_minimize (params as {provers, ...}) i refs state =
@@ -207,7 +213,8 @@
| prover :: _ =>
(kill_provers ();
minimize_facts prover params NONE false i n state facts
- |> snd |> Output.urgent_message)
+ |> (fn (_, (preplay, message)) =>
+ Output.urgent_message (message (preplay ()))))
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 30 17:00:38 2011 +0200
@@ -13,6 +13,7 @@
type relevance_fudge = Sledgehammer_Filter.relevance_fudge
type translated_formula = Sledgehammer_ATP_Translate.translated_formula
type type_system = Sledgehammer_ATP_Translate.type_system
+ type play = Sledgehammer_ATP_Reconstruct.play
type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
datatype mode = Auto_Try | Try | Normal | Minimize
@@ -56,7 +57,8 @@
{outcome: failure option,
used_facts: (string * locality) list,
run_time_in_msecs: int option,
- message: string}
+ preplay: unit -> play,
+ message: play -> string}
type prover =
params -> (string -> minimize_command) -> prover_problem -> prover_result
@@ -315,9 +317,10 @@
type prover_result =
{outcome: failure option,
- message: string,
used_facts: (string * locality) list,
- run_time_in_msecs: int option}
+ run_time_in_msecs: int option,
+ preplay: unit -> play,
+ message: play -> string}
type prover =
params -> (string -> minimize_command) -> prover_problem -> prover_result
@@ -388,13 +391,11 @@
|> Exn.release
|> tap (after path)
-fun proof_banner mode blocking name =
+fun proof_banner mode name =
case mode of
Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
| Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
- | Normal => if blocking then quote name ^ " found a proof"
- else "Try this"
- | Minimize => "Try this"
+ | _ => "Try this"
(* based on "Mirabelle.can_apply" and generalized *)
fun timed_apply timeout tac state i =
@@ -547,8 +548,8 @@
fun run_atp mode name
({exec, required_execs, arguments, proof_delims, known_failures,
conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
- ({debug, verbose, overlord, blocking, type_sys, max_relevant,
- max_mono_iters, max_new_mono_instances, explicit_apply, isar_proof,
+ ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
+ max_new_mono_instances, explicit_apply, isar_proof,
isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
minimize_command
({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
@@ -772,50 +773,57 @@
extract_important_message output
else
""
- val (message, used_facts) =
+ val (used_facts, preplay, message) =
case outcome of
NONE =>
let
val used_facts =
used_facts_in_atp_proof ctxt type_sys facts_offset fact_names
atp_proof
- val reconstructors =
- if uses_typed_helpers typed_helpers atp_proof then [MetisFT, Metis]
- else [Metis, MetisFT]
- val used_ths =
- facts |> map untranslated_fact
- |> filter_used_facts used_facts
- |> map snd
- val preplay =
- play_one_line_proof debug preplay_timeout used_ths state subgoal
- reconstructors
- val full_types = uses_typed_helpers typed_helpers atp_proof
- val isar_params =
- (debug, full_types, isar_shrink_factor, type_sys, pool,
- conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof,
- goal)
- val one_line_params =
- (preplay, proof_banner mode blocking name, used_facts,
- choose_minimize_command minimize_command name preplay,
- subgoal, subgoal_count)
in
- (proof_text ctxt isar_proof isar_params one_line_params ^
- (if verbose then
- "\nATP real CPU time: " ^
- string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
- else
- "") ^
- (if important_message <> "" then
- "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
- important_message
- else
- ""),
- used_facts)
+ (used_facts,
+ fn () =>
+ let
+ val used_ths =
+ facts |> map untranslated_fact |> filter_used_facts used_facts
+ |> map snd
+ val reconstructors =
+ [Metis, MetisFT]
+ |> uses_typed_helpers typed_helpers atp_proof ? rev
+ in
+ play_one_line_proof debug preplay_timeout used_ths state subgoal
+ reconstructors
+ end,
+ fn preplay =>
+ let
+ val full_types = uses_typed_helpers typed_helpers atp_proof
+ val isar_params =
+ (debug, full_types, isar_shrink_factor, type_sys, pool,
+ conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof,
+ goal)
+ val one_line_params =
+ (preplay, proof_banner mode name, used_facts,
+ choose_minimize_command minimize_command name preplay,
+ subgoal, subgoal_count)
+ in
+ proof_text ctxt isar_proof isar_params one_line_params ^
+ (if verbose then
+ "\nATP real CPU time: " ^
+ string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
+ else
+ "") ^
+ (if important_message <> "" then
+ "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
+ important_message
+ else
+ "")
+ end)
end
- | SOME failure => (string_for_failure failure, [])
+ | SOME failure =>
+ ([], K Failed_to_Play, fn _ => string_for_failure failure)
in
- {outcome = outcome, message = message, used_facts = used_facts,
- run_time_in_msecs = msecs}
+ {outcome = outcome, used_facts = used_facts, run_time_in_msecs = msecs,
+ preplay = preplay, message = message}
end
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
@@ -956,8 +964,7 @@
end
in do_slice timeout 1 NONE Time.zeroTime end
-fun run_smt_solver mode name
- (params as {debug, verbose, blocking, preplay_timeout, ...})
+fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...})
minimize_command
({state, subgoal, subgoal_count, facts, smt_filter, ...}
: prover_problem) =
@@ -970,39 +977,43 @@
smt_filter_loop ctxt name params state subgoal smt_filter facts
val (used_facts, used_ths) = used_facts |> ListPair.unzip
val outcome = outcome |> Option.map failure_from_smt_failure
- val message =
+ val (preplay, message) =
case outcome of
NONE =>
- let
- fun smt_settings () =
- if name = SMT_Solver.solver_name_of ctxt then ""
- else "smt_solver = " ^ maybe_quote name
- val preplay =
- case play_one_line_proof debug preplay_timeout used_ths state
- subgoal [Metis, MetisFT] of
- p as Played _ => p
- | _ => Trust_Playable (SMT (smt_settings ()), NONE)
- val one_line_params =
- (preplay, proof_banner mode blocking name, used_facts,
- choose_minimize_command minimize_command name preplay,
- subgoal, subgoal_count)
- in
- one_line_proof_text one_line_params ^
- (if verbose then
- "\nSMT solver real CPU time: " ^
- string_from_time (Time.fromMilliseconds (the run_time_in_msecs)) ^
- "."
- else
- "")
- end
- | SOME failure => string_for_failure failure
+ (fn () =>
+ let
+ fun smt_settings () =
+ if name = SMT_Solver.solver_name_of ctxt then ""
+ else "smt_solver = " ^ maybe_quote name
+ in
+ case play_one_line_proof debug preplay_timeout used_ths state
+ subgoal [Metis, MetisFT] of
+ p as Played _ => p
+ | _ => Trust_Playable (SMT (smt_settings ()), NONE)
+ end,
+ fn preplay =>
+ let
+ val one_line_params =
+ (preplay, proof_banner mode name, used_facts,
+ choose_minimize_command minimize_command name preplay,
+ subgoal, subgoal_count)
+ in
+ one_line_proof_text one_line_params ^
+ (if verbose then
+ "\nSMT solver real CPU time: " ^
+ string_from_time (Time.fromMilliseconds
+ (the run_time_in_msecs)) ^ "."
+ else
+ "")
+ end)
+ | SOME failure => (K Failed_to_Play, fn _ => string_for_failure failure)
in
{outcome = outcome, used_facts = used_facts,
- run_time_in_msecs = run_time_in_msecs, message = message}
+ run_time_in_msecs = run_time_in_msecs, preplay = preplay,
+ message = message}
end
-fun run_metis mode name ({debug, blocking, timeout, ...} : params)
- minimize_command
+fun run_metis mode name ({debug, timeout, ...} : params) minimize_command
({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
let
val reconstructor = if name = Metis_Tactics.metisN then Metis
@@ -1014,30 +1025,28 @@
case play_one_line_proof debug timeout used_ths state subgoal
[reconstructor] of
play as Played (_, time) =>
- let
- val one_line_params =
- (play, proof_banner mode blocking name, used_facts,
- minimize_command name, subgoal, subgoal_count)
- in
- {outcome = NONE, used_facts = used_facts,
- run_time_in_msecs = SOME (Time.toMilliseconds time),
- message = one_line_proof_text one_line_params}
+ {outcome = NONE, used_facts = used_facts,
+ run_time_in_msecs = SOME (Time.toMilliseconds time),
+ preplay = K play,
+ message = fn play =>
+ let
+ val one_line_params =
+ (play, proof_banner mode name, used_facts,
+ minimize_command name, subgoal, subgoal_count)
+ in one_line_proof_text one_line_params end}
+ | play =>
+ let val failure = if play = Failed_to_Play then GaveUp else TimedOut in
+ {outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
+ preplay = K play, message = fn _ => string_for_failure failure}
end
- | play =>
- {outcome = SOME (if play = Failed_to_Play then GaveUp else TimedOut),
- used_facts = [], run_time_in_msecs = NONE, message = ""}
end
fun get_prover ctxt mode name =
let val thy = Proof_Context.theory_of ctxt in
- if is_metis_prover name then
- run_metis mode name
- else if is_atp thy name then
- run_atp mode name (get_atp thy name)
- else if is_smt_prover ctxt name then
- run_smt_solver mode name
- else
- error ("No such prover: " ^ name ^ ".")
+ if is_metis_prover name then run_metis mode name
+ else if is_atp thy name then run_atp mode name (get_atp thy name)
+ else if is_smt_prover ctxt name then run_smt_solver mode name
+ else error ("No such prover: " ^ name ^ ".")
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 30 17:00:38 2011 +0200
@@ -31,6 +31,7 @@
open Sledgehammer_Util
open Sledgehammer_Filter
open Sledgehammer_ATP_Translate
+open Sledgehammer_ATP_Reconstruct
open Sledgehammer_Provers
open Sledgehammer_Minimize
@@ -67,25 +68,45 @@
Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
(fn generic => Config.get_generic generic binary_min_facts)
+val auto_minimize_max_seconds =
+ Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_seconds}
+ (K 5.0)
+
fun get_minimizing_prover ctxt mode name
(params as {debug, verbose, explicit_apply, ...}) minimize_command
(problem as {state, subgoal, subgoal_count, facts, ...}) =
get_prover ctxt mode name params minimize_command problem
- |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
+ |> (fn result as {outcome, used_facts, run_time_in_msecs, preplay, message} =>
if is_some outcome then
result
else
let
- val (used_facts, message) =
- if length used_facts
- >= Config.get ctxt auto_minimize_min_facts then
- minimize_facts name params (SOME explicit_apply) (not verbose)
- subgoal subgoal_count state
+ val num_facts = length used_facts
+ val ((minimize, minimize_name), preplay) =
+ if mode = Normal then
+ if num_facts >= Config.get ctxt auto_minimize_min_facts then
+ ((true, name), preplay)
+ else
+ let val preplay = preplay () in
+ (case preplay of
+ Played (reconstructor, timeout) =>
+ (0.001 * Real.fromInt ((num_facts + 2)
+ * Time.toMilliseconds timeout)
+ <= Config.get ctxt auto_minimize_max_seconds,
+ reconstructor_name reconstructor)
+ | _ => (false, name), K preplay)
+ end
+ else
+ ((false, name), preplay)
+ val (used_facts, (preplay, message)) =
+ if minimize then
+ minimize_facts minimize_name params (SOME explicit_apply)
+ (not verbose) subgoal subgoal_count state
(filter_used_facts used_facts
(map (apsnd single o untranslated_fact) facts))
|>> Option.map (map fst)
else
- (SOME used_facts, message)
+ (SOME used_facts, (preplay, message))
in
case used_facts of
SOME used_facts =>
@@ -103,7 +124,8 @@
else
();
{outcome = NONE, used_facts = used_facts,
- run_time_in_msecs = run_time_in_msecs, message = message})
+ run_time_in_msecs = run_time_in_msecs, preplay = preplay,
+ message = message})
| NONE => result
end)
@@ -129,10 +151,10 @@
fun really_go () =
problem
|> get_minimizing_prover ctxt mode name params minimize_command
- |> (fn {outcome, message, ...} =>
+ |> (fn {outcome, preplay, message, ...} =>
(if outcome = SOME ATP_Proof.TimedOut then timeoutN
else if is_some outcome then noneN
- else someN, message))
+ else someN, message o preplay))
fun go () =
let
val (outcome_code, message) =
@@ -140,13 +162,13 @@
really_go ()
else
(really_go ()
- handle ERROR message => (unknownN, "Error: " ^ message ^ "\n")
+ handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
| exn =>
if Exn.is_interrupt exn then
reraise exn
else
- (unknownN, "Internal error:\n" ^
- ML_Compiler.exn_message exn ^ "\n"))
+ (unknownN, fn () => "Internal error:\n" ^
+ ML_Compiler.exn_message exn ^ "\n"))
val _ =
(* The "expect" argument is deliberately ignored if the prover is
missing so that the "Metis_Examples" can be processed on any
@@ -167,15 +189,15 @@
|> outcome_code = someN
? Proof.goal_message (fn () =>
[Pretty.str "",
- Pretty.mark Markup.hilite (Pretty.str message)]
+ Pretty.mark Markup.hilite (Pretty.str (message ()))]
|> Pretty.chunks))
end
else if blocking then
let
val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
in
- (if outcome_code = someN then message
- else if mode = Normal then quote name ^ ": " ^ message
+ (if outcome_code = someN then message ()
+ else if mode = Normal then quote name ^ ": " ^ message ()
else "")
|> Async_Manager.break_into_chunks
|> List.app Output.urgent_message;
@@ -183,7 +205,8 @@
end
else
(Async_Manager.launch das_tool birth_time death_time (desc ())
- (apfst (curry (op =) someN) o go);
+ ((fn (outcome_code, message) =>
+ (outcome_code = someN, message ())) o go);
(unknownN, state))
end