--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Nov 06 13:57:17 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Nov 06 14:05:57 2011 +0100
@@ -405,11 +405,11 @@
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
fun failed failure =
- ({outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
+ ({outcome = SOME failure, used_facts = [], run_time = Time.zeroTime,
preplay = K (ATP_Reconstruct.Failed_to_Play ATP_Reconstruct.Metis),
message = K "", message_tail = ""}, ~1)
- val ({outcome, used_facts, run_time_in_msecs, preplay, message,
- message_tail} : Sledgehammer_Provers.prover_result,
+ val ({outcome, used_facts, run_time, preplay, message, message_tail}
+ : Sledgehammer_Provers.prover_result,
time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
let
val _ = if is_appropriate_prop concl_t then ()
@@ -431,7 +431,7 @@
in prover params (K (K "")) problem end)) ()
handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
| Fail "inappropriate" => failed ATP_Proof.Inappropriate
- val time_prover = run_time_in_msecs |> the_default ~1
+ val time_prover = run_time |> Time.toMilliseconds
val msg = message (preplay ()) ^ message_tail
in
case outcome of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun Nov 06 13:57:17 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun Nov 06 14:05:57 2011 +0100
@@ -160,24 +160,23 @@
part of the timeout. *)
val slack_msecs = 200
+fun new_timeout timeout run_time =
+ Int.min (Time.toMilliseconds timeout,
+ Time.toMilliseconds run_time + slack_msecs)
+ |> Time.fromMilliseconds
+
fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
facts =
let
val ctxt = Proof.context_of state
val prover = get_prover ctxt Minimize prover_name
- val msecs = Time.toMilliseconds timeout
val _ = print silent (fn () => "Sledgehammer minimizer: " ^
quote prover_name ^ ".")
fun test timeout = test_facts params silent prover timeout i n state
- val timer = Timer.startRealTimer ()
in
(case test timeout facts of
- result as {outcome = NONE, used_facts, ...} =>
+ result as {outcome = NONE, used_facts, run_time, ...} =>
let
- val time = Timer.checkRealTimer timer
- val timeout =
- Int.min (msecs, Time.toMilliseconds time + slack_msecs)
- |> Time.fromMilliseconds
val facts = filter_used_facts used_facts facts
val min =
if length facts >= Config.get ctxt binary_min_facts then
@@ -185,7 +184,7 @@
else
linear_minimize
val (min_facts, {preplay, message, message_tail, ...}) =
- min test timeout result facts
+ min test (new_timeout timeout run_time) result facts
val _ = print silent (fn () => cat_lines
["Minimized to " ^ n_facts (map fst min_facts)] ^
(case length (filter (curry (op =) Chained o snd o fst) min_facts) of
@@ -197,7 +196,8 @@
(preplay,
fn _ => "Timeout: You can increase the time limit using the \
\\"timeout\" option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ "\").",
+ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^
+ "\").",
""))
| {preplay, message, ...} =>
(NONE, (preplay, prefix "Prover error: " o message, "")))