# HG changeset patch # User blanchet # Date 1406757176 -7200 # Node ID e4858f85e6160495064b2ce6630da20a1a28429a # Parent 9df2757f5bec90381c31d4319e6d9459caaeeef9 always minimize Sledgehammer results by default diff -r 9df2757f5bec -r e4858f85e616 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- 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"])]) diff -r 9df2757f5bec -r e4858f85e616 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- 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} diff -r 9df2757f5bec -r e4858f85e616 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- 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 = diff -r 9df2757f5bec -r e4858f85e616 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- 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 diff -r 9df2757f5bec -r e4858f85e616 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- 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,