# HG changeset patch
# User blanchet
# Date 1320576695 -3600
# Node ID 4339763edd553bb594a909f767cee02b5ed6b7f2
# Parent  c71e6980ad2849dfb97aaad3cef0b3c65ef47169
speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half

diff -r c71e6980ad28 -r 4339763edd55 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sun Nov 06 11:16:37 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sun Nov 06 11:51:35 2011 +0100
@@ -38,8 +38,8 @@
   let val n = length names in
     string_of_int n ^ " fact" ^ plural_s n ^
     (if n > 0 then
-       ": " ^ (names |> map fst
-                     |> sort_distinct string_ord |> space_implode " ")
+       ": " ^ (names |> map fst |> sort_distinct string_ord
+                     |> space_implode " ")
      else
        "")
   end
@@ -110,19 +110,21 @@
 fun binary_minimize test xs =
   let
     fun pred xs = #outcome (test xs : prover_result) = NONE
-    fun split [] p = p
-      | split [h] (l, r) = (h :: l, r)
-      | split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r)
     fun min _ _ [] = raise Empty
       | min _ _ [s0] = [s0]
       | min depth sup xs =
         let
+          val (l0, r0) = chop ((length xs + 1) div 2) xs
 (*
-          val _ = warning (replicate_string depth " " ^ "{" ^ ("  " ^
-                           n_facts (map fst sup) ^ " and " ^
-                           n_facts (map fst xs)))
+          val _ = warning (replicate_string depth " " ^ "{ " ^
+                           "sup: " ^ n_facts (map fst sup))
+          val _ = warning (replicate_string depth " " ^ "  " ^
+                           "xs: " ^ n_facts (map fst xs))
+          val _ = warning (replicate_string depth " " ^ "  " ^
+                           "l0: " ^ n_facts (map fst l0))
+          val _ = warning (replicate_string depth " " ^ "  " ^
+                           "r0: " ^ n_facts (map fst r0))
 *)
-          val (l0, r0) = split xs ([], [])
         in
           if pred (sup @ l0) then
             min (depth + 1) sup l0