author blanchet Sat, 18 Dec 2010 13:43:46 +0100 changeset 41267 958fee9ec275 parent 41266 b6b77c963f11 child 41268 56b7e277fd7d
lower threshold where the binary algorithm kick in and use the same value for automatic minimization
```--- 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)```
```--- 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```