# HG changeset patch
# User blanchet
# Date 1307385394 -7200
# Node ID 8cf188ff76a3bbc090c1eaa97a67702b2cf0dc03
# Parent  b4edfe260d54bfcb2e32c00061587422baef8aea
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow

diff -r b4edfe260d54 -r 8cf188ff76a3 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -73,7 +73,7 @@
   Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_seconds}
       (K 5.0)
 
-fun minimize ctxt mode name (params as {debug, verbose, ...})
+fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
              ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
              (result as {outcome, used_facts, run_time_in_msecs, preplay,
                          message} : prover_result) =
@@ -82,24 +82,32 @@
   else
     let
       val num_facts = length used_facts
-      fun can_minimize_fast_enough msecs =
-        0.001 * Real.fromInt ((num_facts + 2) * msecs)
-        <= Config.get ctxt auto_minimize_max_seconds
       val ((minimize, minimize_name), preplay) =
         if mode = Normal then
           if num_facts >= Config.get ctxt auto_minimize_min_facts then
             ((true, name), preplay)
           else
-            let val preplay = preplay () in
-              (case preplay of
-                 Played (reconstructor, timeout) =>
-                 (can_minimize_fast_enough (Time.toMilliseconds timeout),
-                  reconstructor_name reconstructor)
-               | _ =>
-                 case run_time_in_msecs of
-                   SOME msecs => (can_minimize_fast_enough msecs, name)
-                 | NONE => (false, name),
-               K preplay)
+            let
+              fun can_min_fast_enough msecs =
+                0.001 * Real.fromInt ((num_facts + 2) * msecs)
+                <= Config.get ctxt auto_minimize_max_seconds
+              val prover_fast_enough =
+                run_time_in_msecs |> Option.map can_min_fast_enough
+                                  |> the_default false
+            in
+              if isar_proof then
+                ((prover_fast_enough, name), preplay)
+              else
+                let val preplay = preplay () in
+                  (case preplay of
+                     Played (reconstructor, timeout) =>
+                     if can_min_fast_enough (Time.toMilliseconds timeout) then
+                       (true, reconstructor_name reconstructor)
+                     else
+                       (prover_fast_enough, name)
+                   | _ => (prover_fast_enough, name),
+                   K preplay)
+                end
             end
         else
           ((false, name), preplay)