--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Nov 18 11:47:12 2011 +0100
@@ -172,7 +172,8 @@
facts =
let
val ctxt = Proof.context_of state
- val prover = get_prover ctxt Minimize prover_name
+ val prover =
+ get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
val _ = print silent (fn () => "Sledgehammer minimizer: " ^
quote prover_name ^ ".")
fun test timeout = test_facts params silent prover timeout i n state
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Nov 18 11:47:12 2011 +0100
@@ -16,7 +16,7 @@
type minimize_command = ATP_Reconstruct.minimize_command
type relevance_fudge = Sledgehammer_Filter.relevance_fudge
- datatype mode = Auto_Try | Try | Normal | Minimize
+ datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
type params =
{debug: bool,
@@ -126,7 +126,7 @@
(** The Sledgehammer **)
-datatype mode = Auto_Try | Try | Normal | Minimize
+datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
(* Identifier that distinguishes Sledgehammer from other tools that could use
"Async_Manager". *)
@@ -566,6 +566,7 @@
fun suffix_for_mode Auto_Try = "_auto_try"
| suffix_for_mode Try = "_try"
| suffix_for_mode Normal = ""
+ | suffix_for_mode Auto_Minimize = "_auto_min"
| suffix_for_mode Minimize = "_min"
(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on