--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Dec 15 18:48:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Dec 15 19:57:12 2012 +0100
@@ -61,8 +61,12 @@
val _ =
print silent (fn () =>
"Testing " ^ n_facts (map fst facts) ^
- (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
- else "") ^ "...")
+ (if verbose then
+ case timeout of
+ SOME timeout => " (timeout: " ^ string_from_time timeout ^ ")"
+ | _ => ""
+ else
+ "") ^ "...")
val {goal, ...} = Proof.goal state
val facts =
facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
@@ -101,10 +105,11 @@
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 new_timeout NONE _ = NONE
+ | new_timeout (SOME timeout) run_time =
+ Int.min (Time.toMilliseconds timeout,
+ Time.toMilliseconds run_time + slack_msecs)
+ |> Time.fromMilliseconds |> SOME
(* The linear algorithm usually outperforms the binary algorithm when over 60%
of the facts are actually needed. The binary algorithm is much more
@@ -222,11 +227,12 @@
| {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 + Time.toMilliseconds timeout div 1000) ^
- "\").",
- ""))
+ fn _ =>
+ "Timeout: You can increase the time limit using the \"timeout\" \
+ \option (e.g., \"timeout = " ^
+ string_of_int (10 + Time.toMilliseconds
+ (timeout |> the_default (seconds 60.0)) div 1000) ^
+ "\").", ""))
| {preplay, message, ...} =>
(NONE, (preplay, prefix "Prover error: " o message, "")))
handle ERROR msg =>