# HG changeset patch # User blanchet # Date 1643641763 -3600 # Node ID b49329185b828b7910deee5f28f469cfef0d54b3 # Parent a8efa30c380d7e500f74e32225548258f9fcf3d2 removed obscure E option diff -r a8efa30c380d -r b49329185b82 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100 @@ -20,7 +20,6 @@ (* NOTE: Do not forget to update the Sledgehammer documentation to reflect changes here. *) val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) -val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*) val keep_probsK = "keep_probs" (*=BOOL: keep temporary problem files created by sledgehammer*) val keep_proofsK = "keep_proofs" (*=BOOL: keep temporary proof files created by ATPs*) val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (e.g. using metis)*) @@ -272,7 +271,7 @@ local -fun run_sh params e_selection_heuristic term_order keep pos state = +fun run_sh params term_order keep pos state = let fun set_file_name (SOME (dir, keep_probs, keep_proofs)) = let @@ -290,8 +289,6 @@ state |> Proof.map_context (set_file_name keep - #> (Option.map (Config.put Sledgehammer_ATP_Systems.e_selection_heuristic) - e_selection_heuristic |> the_default I) #> (Option.map (Config.put Sledgehammer_ATP_Systems.term_order) term_order |> the_default I)) @@ -307,7 +304,7 @@ in -fun run_sledgehammer (params as {provers, ...}) output_dir e_selection_heuristic term_order +fun run_sledgehammer (params as {provers, ...}) output_dir term_order keep_probs keep_proofs proof_method_from_msg thy_index trivial pos st = let val thy = Proof.theory_of st @@ -324,8 +321,7 @@ else NONE val prover_name = hd provers - val (sledgehamer_outcome, msg, cpu_time) = - run_sh params e_selection_heuristic term_order keep pos st + val (sledgehamer_outcome, msg, cpu_time) = run_sh params term_order keep pos st val (time_prover, change_data, proof_method_and_used_thms) = (case sledgehamer_outcome of Sledgehammer.SH_Some {used_facts, run_time, ...} => @@ -444,7 +440,6 @@ Mirabelle.get_bool_argument arguments (check_trivialK, check_trivial_default) val keep_probs = Mirabelle.get_bool_argument arguments (keep_probsK, keep_probs_default) val keep_proofs = Mirabelle.get_bool_argument arguments (keep_proofsK, keep_proofs_default) - val e_selection_heuristic = AList.lookup (op =) arguments e_selection_heuristicK val term_order = AList.lookup (op =) arguments term_orderK val proof_method_from_msg = proof_method_from_msg arguments @@ -467,8 +462,8 @@ let val trivial = check_trivial andalso try0 pre handle Timeout.TIMEOUT _ => false val (outcome, log1, change_data1, proof_method_and_used_thms) = - run_sledgehammer params output_dir e_selection_heuristic term_order - keep_probs keep_proofs proof_method_from_msg theory_index trivial pos pre + run_sledgehammer params output_dir term_order keep_probs keep_proofs + proof_method_from_msg theory_index trivial pos pre val (log2, change_data2) = (case proof_method_and_used_thms of SOME (proof_method, used_thms) => diff -r a8efa30c380d -r b49329185b82 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Jan 31 16:09:23 2022 +0100 @@ -32,7 +32,6 @@ val e_autoN : string val e_fun_weightN : string val e_sym_offset_weightN : string - val e_selection_heuristic : string Config.T val e_default_fun_weight : real Config.T val e_fun_weight_base : real Config.T val e_fun_weight_span : real Config.T @@ -208,8 +207,6 @@ val e_fun_weightN = "fun_weight" val e_sym_offset_weightN = "sym_offset_weight" -val e_selection_heuristic = - Attrib.setup_config_string \<^binding>\atp_e_selection_heuristic\ (K e_smartN) (* FUDGE *) val e_default_fun_weight = Attrib.setup_config_real \<^binding>\atp_e_default_fun_weight\ (K 20.0) @@ -291,7 +288,6 @@ prem_role = Conjecture, good_slices = fn ctxt => let - val heuristic = Config.get ctxt e_selection_heuristic val (format, enc, main_lam_trans) = if string_ord (getenv "E_VERSION", "2.7") <> LESS then (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN) @@ -301,15 +297,12 @@ (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN) in (* FUDGE *) - if heuristic = e_smartN then - [((128, meshN), (format, enc, main_lam_trans, false, e_fun_weightN)), - ((128, mashN), (format, enc, main_lam_trans, false, e_sym_offset_weightN)), - ((91, mepoN), (format, enc, main_lam_trans, false, e_autoN)), - ((1000, meshN), (format, "poly_guards??", main_lam_trans, false, e_sym_offset_weightN)), - ((256, mepoN), (format, enc, liftingN, false, e_fun_weightN)), - ((64, mashN), (format, enc, combsN, false, e_fun_weightN))] - else - [((500, meshN), (format, enc, combsN, false, heuristic))] + [((128, meshN), (format, enc, main_lam_trans, false, e_fun_weightN)), + ((128, mashN), (format, enc, main_lam_trans, false, e_sym_offset_weightN)), + ((91, mepoN), (format, enc, main_lam_trans, false, e_autoN)), + ((1000, meshN), (format, "poly_guards??", main_lam_trans, false, e_sym_offset_weightN)), + ((256, mepoN), (format, enc, liftingN, false, e_fun_weightN)), + ((64, mashN), (format, enc, combsN, false, e_fun_weightN))] end, good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances}