author blanchet Mon, 06 Dec 2010 09:54:58 +0100 changeset 40977 9140c5950494 parent 40965 54b6c9e1c157 child 40978 79d2ea0e1fdb
[mq]: sledge_binary_minimizer
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sun Dec 05 14:02:16 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon Dec 06 09:54:58 2010 +0100
@@ -2,7 +2,7 @@
Author:     Philipp Meyer, TU Muenchen
Author:     Jasmin Blanchette, TU Muenchen

-Minimization of fact list for Metis using ATPs.
+Minimization of fact list for Metis using external provers.
*)

signature SLEDGEHAMMER_MINIMIZE =
@@ -62,16 +62,24 @@
facts = facts, only = true}
val result as {outcome, used_facts, ...} = prover params (K "") problem
in
-    Output.urgent_message (case outcome of
-                SOME failure => string_for_failure failure
-              | NONE =>
-                if length used_facts = length facts then "Found proof."
-                else "Found proof with " ^ n_facts used_facts ^ ".");
+    Output.urgent_message
+        (case outcome of
+           SOME failure => string_for_failure failure
+         | NONE =>
+           if length used_facts = length facts then "Found proof."
+           else "Found proof with " ^ n_facts used_facts ^ ".");
result
end

(* 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 that situation just by looking at the
+   number of used facts reported by the prover. *)
+val binary_threshold = 50
+
fun filter_used_facts used = filter (member (op =) used o fst)

fun sublinear_minimize _ [] p = p
@@ -82,9 +90,35 @@
(filter_used_facts used_facts seen, result)
| _ => sublinear_minimize test xs (x :: seen, result)

-(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
-   preprocessing time is included in the estimate below but isn't part of the
-   timeout. *)
+fun binary_minimize test xs =
+  let
+    fun p 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 sup xs =
+        let val (l0, r0) = split xs ([], []) in
+          if p (sup @ l0) then
+            min sup l0
+          else if p (sup @ r0) then
+            min sup r0
+          else
+            let
+              val l = min (sup @ r0) l0
+              val r = min (sup @ l) r0
+            in l @ r end
+        end
+    val xs =
+      case min [] xs of
+        [x] => if p [] then [] else [x]
+      | xs => xs
+  in (xs, test xs) 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
+   part of the timeout. *)
val fudge_msecs = 1000

fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set."
@@ -95,7 +129,8 @@
val ctxt = Proof.context_of state
val prover = get_prover ctxt false prover_name
val msecs = Time.toMilliseconds timeout
-    val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
+    val _ = Output.urgent_message ("Sledgehammer minimize: " ^
+                                   quote prover_name ^ ".")
val {goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val explicit_apply =
@@ -112,9 +147,12 @@
val new_timeout =
Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
|> Time.fromMilliseconds
+         val facts = filter_used_facts used_facts facts
val (min_thms, {message, ...}) =
-           sublinear_minimize (do_test new_timeout)
-               (filter_used_facts used_facts facts) ([], result)
+           if length facts >= binary_threshold then
+             binary_minimize (do_test new_timeout) facts
+           else
+             sublinear_minimize (do_test new_timeout) facts ([], result)
val n = length min_thms
val _ = Output.urgent_message (cat_lines
["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
@@ -132,7 +170,7 @@
\can increase the time limit using the \"timeout\" \
\option (e.g., \"timeout = " ^
string_of_int (10 + msecs div 1000) ^ "\").")
-     | {message, ...} => (NONE, "ATP error: " ^ message))
+     | {message, ...} => (NONE, "Prover error: " ^ message))
handle ERROR msg => (NONE, "Error: " ^ msg)
end
```