# HG changeset patch
# User blanchet
# Date 1322742854 -3600
# Node ID 6bf7eec9b153d071e73238e8924ac32a8d2e4305
# Parent  418846ea4f99655620b0464d077bdea63e6596dc
added "minimize" option for more control over automatic minimization

diff -r 418846ea4f99 -r 6bf7eec9b153 NEWS
--- a/NEWS	Thu Dec 01 13:34:13 2011 +0100
+++ b/NEWS	Thu Dec 01 13:34:14 2011 +0100
@@ -147,7 +147,7 @@
     affecting 'rat' and 'real'.
 
 * Sledgehammer:
-  - Added "lam_trans" option.
+  - Added "lam_trans" and "minimize" options.
   - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
 
 * Metis:
diff -r 418846ea4f99 -r 6bf7eec9b153 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Dec 01 13:34:13 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Dec 01 13:34:14 2011 +0100
@@ -96,6 +96,7 @@
    ("isar_proof", "false"),
    ("isar_shrink_factor", "1"),
    ("slice", "true"),
+   ("minimize", "smart"),
    ("preplay_timeout", "4")]
 
 val alias_params =
@@ -107,7 +108,8 @@
    ("non_blocking", "blocking"),
    ("unsound", "sound"),
    ("no_isar_proof", "isar_proof"),
-   ("dont_slice", "slice")]
+   ("dont_slice", "slice"),
+   ("dont_minimize", "minimize")]
 
 val params_for_minimize =
   ["debug", "verbose", "overlord", "type_enc", "sound", "lam_trans",
@@ -290,6 +292,8 @@
     val isar_proof = lookup_bool "isar_proof"
     val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
+    val minimize =
+      if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
     val timeout =
       (if mode = Auto_Try then NONE else lookup_time "timeout") |> the_timeout
     val preplay_timeout =
@@ -302,8 +306,9 @@
      lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
      max_relevant = max_relevant, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
-     isar_shrink_factor = isar_shrink_factor, slice = slice, timeout = timeout,
-     preplay_timeout = preplay_timeout, expect = expect}
+     isar_shrink_factor = isar_shrink_factor, slice = slice,
+     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
+     expect = expect}
   end
 
 fun get_params mode = extract_params mode o default_raw_params
diff -r 418846ea4f99 -r 6bf7eec9b153 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Dec 01 13:34:13 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Dec 01 13:34:14 2011 +0100
@@ -66,7 +66,8 @@
        max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
        max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
        isar_shrink_factor = isar_shrink_factor, slice = false,
-       timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
+       minimize = SOME false, timeout = timeout,
+       preplay_timeout = preplay_timeout, expect = ""}
     val problem =
       {state = state, goal = goal, subgoal = i, subgoal_count = n,
        facts = facts, smt_filter = NONE}
diff -r 418846ea4f99 -r 6bf7eec9b153 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 01 13:34:13 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 01 13:34:14 2011 +0100
@@ -34,6 +34,7 @@
      isar_proof: bool,
      isar_shrink_factor: int,
      slice: bool,
+     minimize: bool option,
      timeout: Time.time,
      preplay_timeout: Time.time,
      expect: string}
@@ -297,6 +298,7 @@
    isar_proof: bool,
    isar_shrink_factor: int,
    slice: bool,
+   minimize: bool option,
    timeout: Time.time,
    preplay_timeout: Time.time,
    expect: string}
diff -r 418846ea4f99 -r 6bf7eec9b153 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Dec 01 13:34:13 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Dec 01 13:34:14 2011 +0100
@@ -75,8 +75,8 @@
 fun adjust_reconstructor_params override_params
         ({debug, verbose, overlord, blocking, provers, type_enc, sound,
          lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
-         max_new_mono_instances, isar_proof, isar_shrink_factor, slice, timeout,
-         preplay_timeout, expect} : params) =
+         max_new_mono_instances, isar_proof, isar_shrink_factor, slice,
+         minimize, timeout, preplay_timeout, expect} : params) =
   let
     fun lookup_override name default_value =
       case AList.lookup (op =) override_params name of
@@ -93,11 +93,13 @@
      relevance_thresholds = relevance_thresholds,
      max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
-     isar_shrink_factor = isar_shrink_factor, slice = slice, timeout = timeout,
-     preplay_timeout = preplay_timeout, expect = expect}
+     isar_shrink_factor = isar_shrink_factor, slice = slice,
+     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
+     expect = expect}
   end
 
-fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
+fun minimize ctxt mode name
+             (params as {debug, verbose, isar_proof, minimize, ...})
              ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
              (result as {outcome, used_facts, run_time, preplay, message,
                          message_tail} : prover_result) =
@@ -106,7 +108,7 @@
   else
     let
       val num_facts = length used_facts
-      val ((minimize, (minimize_name, params)), preplay) =
+      val ((perhaps_minimize, (minimize_name, params)), preplay) =
         if mode = Normal then
           if num_facts >= Config.get ctxt auto_minimize_min_facts then
             ((true, (name, params)), preplay)
@@ -116,10 +118,10 @@
                 0.001
                 * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
                 <= Config.get ctxt auto_minimize_max_time
-              val prover_fast_enough = can_min_fast_enough run_time
+              fun prover_fast_enough () = can_min_fast_enough run_time
             in
               if isar_proof then
-                ((prover_fast_enough, (name, params)), preplay)
+                ((prover_fast_enough (), (name, params)), preplay)
               else
                 let val preplay = preplay () in
                   (case preplay of
@@ -130,13 +132,14 @@
                                       adjust_reconstructor_params
                                           override_params params))
                      else
-                       (prover_fast_enough, (name, params))
-                   | _ => (prover_fast_enough, (name, params)),
+                       (prover_fast_enough (), (name, params))
+                   | _ => (prover_fast_enough (), (name, params)),
                    K preplay)
                 end
             end
         else
           ((false, (name, params)), preplay)
+      val minimize = minimize |> the_default perhaps_minimize
       val (used_facts, (preplay, message, _)) =
         if minimize then
           minimize_facts minimize_name params (not verbose) subgoal