# HG changeset patch
# User blanchet
# Date 1320584757 -3600
# Node ID c6f1add24843cb2c412ba168900ceb178422c9aa
# Parent  bab52dafa63a520b0df036d6981bf2dc68169182
tuning

diff -r bab52dafa63a -r c6f1add24843 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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
diff -r bab52dafa63a -r c6f1add24843 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- 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, "")))