# HG changeset patch
# User blanchet
# Date 1320582733 -3600
# Node ID cb54f1b34cf95e6c96f29ae2a8484626a767fb81
# Parent  4339763edd553bb594a909f767cee02b5ed6b7f2
shortcut binary minimization algorithm

diff -r 4339763edd55 -r cb54f1b34cf9 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sun Nov 06 11:51:35 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sun Nov 06 13:32:13 2011 +0100
@@ -90,31 +90,28 @@
 
 (* minimalization of facts *)
 
-(* The sublinear algorithm works well in almost all situations, except when the
-   external prover cannot return the list of used facts and hence returns all
-   facts as used. In that case, the binary algorithm is much more appropriate.
-   We can usually detect the situation by looking at the number of used facts
-   reported by the prover. *)
+(* The linear algorithm usually outperforms the binary algorithm when over 60%
+   of the facts are actually needed. The binary algorithm is much more
+   appropriate for provers that cannot return the list of used facts and hence
+   returns all facts as used. Since we cannot know in advance how many facts are
+   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 20)
+                          (K 10)
 
-fun sublinear_minimize _ [] p = p
-  | sublinear_minimize test (x :: xs) (seen, result) =
+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 =>
-      sublinear_minimize test (filter_used_facts used_facts xs)
-                         (filter_used_facts used_facts seen, result)
-    | _ => sublinear_minimize test xs (x :: seen, result)
+      linear_minimize test (filter_used_facts used_facts xs)
+                      (filter_used_facts used_facts seen, result)
+    | _ => linear_minimize test xs (x :: seen, result)
 
-fun binary_minimize test xs =
+fun binary_minimize test result xs =
   let
-    fun pred xs = #outcome (test xs : prover_result) = NONE
-    fun min _ _ [] = raise Empty
-      | min _ _ [s0] = [s0]
-      | min depth sup xs =
+    fun min depth result sup (xs as _ :: _ :: _) =
         let
-          val (l0, r0) = chop ((length xs + 1) div 2) xs
+          val (l0, r0) = chop (length xs div 2) xs
 (*
           val _ = warning (replicate_string depth " " ^ "{ " ^
                            "sup: " ^ n_facts (map fst sup))
@@ -125,25 +122,38 @@
           val _ = warning (replicate_string depth " " ^ "  " ^
                            "r0: " ^ n_facts (map fst r0))
 *)
+          val depth = depth + 1
         in
-          if pred (sup @ l0) then
-            min (depth + 1) sup l0
-          else if pred (sup @ r0) then
-            min (depth + 1) sup r0
-          else
-            let
-              val l = min (depth + 1) (sup @ r0) l0
-              val r = min (depth + 1) (sup @ l) r0
-            in l @ r end
+          case test (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
+              result as {outcome = NONE, used_facts, ...} =>
+              min depth result (filter_used_facts used_facts sup)
+                        (filter_used_facts used_facts r0)
+            | _ =>
+              let
+                val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
+                val (sup, r0) =
+                  (sup, r0) |> pairself (filter_used_facts (map fst sup_r0))
+                val (sup_l, (r, result)) = min depth result (sup @ l) r0
+                val sup = sup |> filter_used_facts (map fst sup_l)
+              in (sup, (l @ r, result)) end
         end
 (*
         |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
 *)
-    val xs =
-      case min 0 [] xs of
-        [x] => if pred [] then [] else [x]
-      | xs => xs
-  in (xs, test xs) end
+      | min _ result sup xs = (sup, (xs, result))
+  in
+    case snd (min 0 result [] xs) of
+      ([x], result) =>
+      (case test [] of
+         result as {outcome = NONE, ...} => ([], result)
+       | _ => ([x], result))
+    | p => p
+  end
 
 (* 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
@@ -171,9 +181,9 @@
          val facts = filter_used_facts used_facts facts
          val (min_facts, {preplay, message, message_tail, ...}) =
            if length facts >= Config.get ctxt binary_min_facts then
-             binary_minimize (do_test new_timeout) facts
+             binary_minimize (do_test new_timeout) result facts
            else
-             sublinear_minimize (do_test new_timeout) facts ([], result)
+             linear_minimize (do_test new_timeout) facts ([], result)
          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