--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Jul 30 23:52:56 2014 +0200
@@ -96,7 +96,7 @@
("try0", "true"),
("smt_proofs", "smart"),
("slice", "true"),
- ("minimize", "smart"),
+ ("minimize", "true"),
("preplay_timeout", "1")]
val alias_params =
@@ -299,7 +299,7 @@
val try0 = lookup_bool "try0"
val smt_proofs = lookup_option lookup_bool "smt_proofs"
val slice = mode <> Auto_Try andalso lookup_bool "slice"
- val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
+ val minimize = mode <> Auto_Try andalso lookup_bool "minimize"
val timeout = lookup_time "timeout"
val preplay_timeout = if mode = Auto_Try then Time.zeroTime else lookup_time "preplay_timeout"
val expect = lookup_string "expect"
@@ -391,8 +391,7 @@
([("timeout", [string_of_real default_learn_prover_timeout]),
("slice", ["false"])] @
override_params @
- [("minimize", ["true"]),
- ("preplay_timeout", ["0"])]))
+ [("preplay_timeout", ["0"])]))
fact_override (#facts (Proof.goal state))
(subcommand = learn_proverN orelse subcommand = relearn_proverN))
else if subcommand = running_learnersN then
@@ -465,7 +464,6 @@
((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
[("isar_proofs", [isar_proofs_arg]),
("blocking", ["true"]),
- ("minimize", ["true"]),
("debug", ["false"]),
("verbose", ["false"]),
("overlord", ["false"])])
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Jul 30 23:52:56 2014 +0200
@@ -40,7 +40,7 @@
try0 : bool,
smt_proofs : bool option,
slice : bool,
- minimize : bool option,
+ minimize : bool,
timeout : Time.time,
preplay_timeout : Time.time,
expect : string}
@@ -147,7 +147,7 @@
try0 : bool,
smt_proofs : bool option,
slice : bool,
- minimize : bool option,
+ minimize : bool,
timeout : Time.time,
preplay_timeout : Time.time,
expect : string}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Jul 30 23:52:56 2014 +0200
@@ -388,7 +388,7 @@
|> factify_atp_proof (map fst used_from) hyp_ts concl_t
in
(verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,
- minimize <> SOME false, atp_proof, goal)
+ minimize, atp_proof, goal)
end
val one_line_params =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Wed Jul 30 23:52:56 2014 +0200
@@ -20,8 +20,6 @@
val get_prover : Proof.context -> mode -> string -> prover
val binary_min_facts : int Config.T
- val auto_minimize_min_facts : int Config.T
- val auto_minimize_max_time : real Config.T
val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
Proof.state -> thm -> (proof_method * play_outcome) Lazy.lazy option ->
((string * stature) * thm list) list ->
@@ -180,11 +178,6 @@
actually needed, we heuristically set the threshold to 10 facts. *)
val binary_min_facts =
Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts} (K 20)
-val auto_minimize_min_facts =
- Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
- (fn generic => Config.get_generic generic binary_min_facts)
-val auto_minimize_max_time =
- Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time} (K 5.0)
fun linear_minimize test timeout result xs =
let
@@ -317,42 +310,22 @@
else
let
val thy = Proof_Context.theory_of ctxt
- val num_facts = length used_facts
- val ((perhaps_minimize, (minimize_name, params)), preplay) =
+ val (minimize_name, params) =
if mode = Normal then
- if num_facts >= Config.get ctxt auto_minimize_min_facts then
- ((true, (name, params)), preplay)
- else
- let
- fun can_min_fast_enough time =
- 0.001
- * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
- <= Config.get ctxt auto_minimize_max_time
- fun prover_fast_enough () = can_min_fast_enough run_time
- in
- (case Lazy.force preplay of
- (meth as Metis_Method _, Played timeout) =>
- if isar_proofs = SOME true then
- (* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved
- itself. *)
- (can_min_fast_enough timeout, (isar_supported_prover_of thy name, params))
- else if can_min_fast_enough timeout then
- (true, extract_proof_method params meth
- ||> (fn override_params =>
- adjust_proof_method_params override_params params))
- else
- (prover_fast_enough (), (name, params))
- | (SMT2_Method, Played timeout) =>
- (* Cheat: Assume the original prover is as fast as "smt" for the goal it proved
- itself. *)
- (can_min_fast_enough timeout, (name, params))
- | _ => (prover_fast_enough (), (name, params)),
- preplay)
- end
+ (case Lazy.force preplay of
+ (meth as Metis_Method _, Played _) =>
+ if isar_proofs = SOME true then
+ (* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved
+ itself. *)
+ (isar_supported_prover_of thy name, params)
+ else
+ extract_proof_method params meth
+ ||> (fn override_params => adjust_proof_method_params override_params params)
+ | _ => (name, params))
else
- ((false, (name, params)), preplay)
- val minimize = minimize |> the_default perhaps_minimize
+ (name, params)
+
val (used_facts, (preplay, message, _)) =
if minimize then
minimize_facts do_learn minimize_name params
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Wed Jul 30 23:52:56 2014 +0200
@@ -201,8 +201,8 @@
fn preplay =>
let
fun isar_params () =
- (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize <> SOME false,
- atp_proof (), goal)
+ (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
+ goal)
val one_line_params =
(preplay, proof_banner mode name, used_facts,