# HG changeset patch
# User blanchet
# Date 1320583069 -3600
# Node ID ff2edf24e83a344b43dde68e99f86a78d15dd5bb
# Parent  cb54f1b34cf95e6c96f29ae2a8484626a767fb81
cascading timeouts in minimizer

diff -r cb54f1b34cf9 -r ff2edf24e83a src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sun Nov 06 13:32:13 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sun Nov 06 13:37:49 2011 +0100
@@ -97,17 +97,20 @@
    actually needed, we heuristically set the threshold to 10 facts. *)
 val binary_min_facts =
   Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
-                          (K 10)
+                          (K 20)
 
-fun linear_minimize _ [] p = p
-  | linear_minimize test (x :: xs) (seen, result) =
-    case test (xs @ seen) of
-      result as {outcome = NONE, used_facts, ...} : prover_result =>
-      linear_minimize test (filter_used_facts used_facts xs)
+fun linear_minimize test timeout result xs =
+  let
+    fun min _ [] p = p
+      | min timeout (x :: xs) (seen, result) =
+        case test timeout (xs @ seen) of
+          result as {outcome = NONE, used_facts, ...} : prover_result =>
+          min timeout (filter_used_facts used_facts xs)
                       (filter_used_facts used_facts seen, result)
-    | _ => linear_minimize test xs (x :: seen, result)
+        | _ => min timeout xs (x :: seen, result)
+  in min timeout xs ([], result) end
 
-fun binary_minimize test result xs =
+fun binary_minimize test timeout result xs =
   let
     fun min depth result sup (xs as _ :: _ :: _) =
         let
@@ -124,12 +127,12 @@
 *)
           val depth = depth + 1
         in
-          case test (sup @ l0) of
+          case test timeout (sup @ l0) of
             result as {outcome = NONE, used_facts, ...} : prover_result =>
             min depth result (filter_used_facts used_facts sup)
                       (filter_used_facts used_facts l0)
           | _ =>
-            case test (sup @ r0) of
+            case test timeout (sup @ r0) of
               result as {outcome = NONE, used_facts, ...} =>
               min depth result (filter_used_facts used_facts sup)
                         (filter_used_facts used_facts r0)
@@ -149,7 +152,7 @@
   in
     case snd (min 0 result [] xs) of
       ([x], result) =>
-      (case test [] of
+      (case test timeout [] of
          result as {outcome = NONE, ...} => ([], result)
        | _ => ([x], result))
     | p => p
@@ -168,22 +171,24 @@
     val msecs = Time.toMilliseconds timeout
     val _ = print silent (fn () => "Sledgehammer minimizer: " ^
                                    quote prover_name ^ ".")
-    fun do_test timeout = test_facts params silent prover timeout i n state
+    fun test timeout = test_facts params silent prover timeout i n state
     val timer = Timer.startRealTimer ()
   in
-    (case do_test timeout facts of
+    (case test timeout facts of
        result as {outcome = NONE, used_facts, ...} =>
        let
          val time = Timer.checkRealTimer timer
-         val new_timeout =
+         val timeout =
            Int.min (msecs, Time.toMilliseconds time + slack_msecs)
            |> Time.fromMilliseconds
          val facts = filter_used_facts used_facts facts
-         val (min_facts, {preplay, message, message_tail, ...}) =
+         val min = 
            if length facts >= Config.get ctxt binary_min_facts then
-             binary_minimize (do_test new_timeout) result facts
+             binary_minimize
            else
-             linear_minimize (do_test new_timeout) facts ([], result)
+             linear_minimize
+         val (min_facts, {preplay, message, message_tail, ...}) =
+           min test timeout 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