src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sat Dec 18 23:31:22 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sun Dec 19 00:13:25 2010 +0100
@@ -30,10 +30,10 @@
 
 (* wrapper for calling external prover *)
 
-fun string_for_failure ATP_Proof.Unprovable = "Unprovable."
-  | string_for_failure ATP_Proof.TimedOut = "Timed out."
-  | string_for_failure ATP_Proof.Interrupted = "Interrupted."
-  | string_for_failure _ = "Error."
+fun short_string_for_failure ATP_Proof.Unprovable = "Unprovable."
+  | short_string_for_failure ATP_Proof.TimedOut = "Timed out."
+  | short_string_for_failure ATP_Proof.Interrupted = "Interrupted."
+  | short_string_for_failure _ = "Error."
 
 fun n_facts names =
   let val n = length names in
@@ -47,11 +47,15 @@
 
 fun print silent f = if silent then () else Output.urgent_message (f ())
 
-fun test_facts ({debug, overlord, provers, type_sys, isar_proof,
+fun test_facts ({debug, verbose, overlord, provers, type_sys, isar_proof,
                  isar_shrink_factor, ...} : params) silent (prover : prover)
                explicit_apply timeout i n state facts =
   let
-    val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ "...")
+    val _ =
+      print silent (fn () =>
+          "Testing " ^ n_facts (map fst facts) ^
+          (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
+          else "") ^ "...")
     val params =
       {debug = debug, verbose = false, overlord = overlord, blocking = true,
        provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
@@ -66,12 +70,12 @@
        facts = facts, smt_head = NONE}
     val result as {outcome, used_facts, ...} = prover params (K "") problem
   in
-    print silent
-        (fn () => case outcome of
-                    SOME failure => string_for_failure failure
-                  | NONE =>
-                    if length used_facts = length facts then "Found proof."
-                    else "Found proof with " ^ n_facts used_facts ^ ".");
+    print silent (fn () =>
+        case outcome of
+          SOME failure => short_string_for_failure failure
+        | NONE =>
+          if length used_facts = length facts then "Found proof."
+          else "Found proof with " ^ n_facts used_facts ^ ".");
     result
   end
 
@@ -123,7 +127,7 @@
 (* Give the external prover some slack. The ATP gets further slack because the
    Sledgehammer preprocessing time is included in the estimate below but isn't
    part of the timeout. *)
-val fudge_msecs = 1000
+val slack_msecs = 200
 
 fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
                    facts =
@@ -148,7 +152,7 @@
        let
          val time = Timer.checkRealTimer timer
          val new_timeout =
-           Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
+           Int.min (msecs, Time.toMilliseconds time + slack_msecs)
            |> Time.fromMilliseconds
          val facts = filter_used_facts used_facts facts
          val (min_thms, {message, ...}) =