# HG changeset patch
# User blanchet
# Date 1292676226 -3600
# Node ID 958fee9ec2757ba907a17f4a028e8d820c2e9c8f
# Parent  b6b77c963f11b6bd063e976dfeab08e4db041a7d
lower threshold where the binary algorithm kick in and use the same value for automatic minimization

diff -r b6b77c963f11 -r 958fee9ec275 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sat Dec 18 13:38:14 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sat Dec 18 13:43:46 2010 +0100
@@ -10,6 +10,7 @@
   type locality = Sledgehammer_Filter.locality
   type params = Sledgehammer_Provers.params
 
+  val binary_threshold : int Unsynchronized.ref
   val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
   val minimize_facts :
     string -> params -> bool -> int -> int -> Proof.state
@@ -78,10 +79,10 @@
 
 (* 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 that situation just by looking at the
-   number of used facts reported by the prover. *)
-val binary_threshold = 50
+   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. *)
+val binary_threshold = Unsynchronized.ref 20
 
 fun filter_used_facts used = filter (member (op =) used o fst)
 
@@ -151,7 +152,7 @@
            |> Time.fromMilliseconds
          val facts = filter_used_facts used_facts facts
          val (min_thms, {message, ...}) =
-           if length facts >= binary_threshold then
+           if length facts >= !binary_threshold then
              binary_minimize (do_test new_timeout) facts
            else
              sublinear_minimize (do_test new_timeout) facts ([], result)
diff -r b6b77c963f11 -r 958fee9ec275 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Dec 18 13:38:14 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Dec 18 13:43:46 2010 +0100
@@ -42,7 +42,7 @@
    else
      "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
 
-val auto_minimization_threshold = Unsynchronized.ref 50
+val auto_minimization_threshold = Unsynchronized.ref (!binary_threshold)
 
 fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...})
         minimize_command