# HG changeset patch # User blanchet # Date 1643641763 -3600 # Node ID 114eb0af123dde4dd219a5f25d84233efacdf518 # Parent fdda7e754f4590ff2a0fd935d21f04520f2af102 simplified 'best_slice' data structure and made minor changes to slices diff -r fdda7e754f45 -r 114eb0af123d 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 @@ -21,7 +21,6 @@ val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*) -val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*) 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)*) @@ -273,7 +272,7 @@ local -fun run_sh params e_selection_heuristic term_order force_sos keep pos state = +fun run_sh params e_selection_heuristic term_order keep pos state = let fun set_file_name (SOME (dir, keep_probs, keep_proofs)) = let @@ -294,9 +293,7 @@ #> (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) - #> (Option.map (Config.put Sledgehammer_ATP_Systems.force_sos) - force_sos |> the_default I)) + term_order |> the_default I)) val ((_, (sledgehammer_outcome, msg)), cpu_time) = Mirabelle.cpu_time (fn () => Sledgehammer.run_sledgehammer params Sledgehammer_Prover.Normal NONE 1 @@ -311,7 +308,7 @@ in fun run_sledgehammer (params as {provers, ...}) output_dir e_selection_heuristic term_order - force_sos keep_probs keep_proofs proof_method_from_msg thy_index trivial pos st = + keep_probs keep_proofs proof_method_from_msg thy_index trivial pos st = let val thy = Proof.theory_of st val thy_name = Context.theory_name thy @@ -328,7 +325,7 @@ NONE val prover_name = hd provers val (sledgehamer_outcome, msg, cpu_time) = - run_sh params e_selection_heuristic term_order force_sos keep pos st + run_sh params e_selection_heuristic 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, ...} => @@ -449,8 +446,6 @@ 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 force_sos = AList.lookup (op =) arguments force_sosK - |> Option.map (curry (op <>) "false") val proof_method_from_msg = proof_method_from_msg arguments (* Parse Sledgehammer parameters *) @@ -473,7 +468,7 @@ 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 - force_sos keep_probs keep_proofs proof_method_from_msg theory_index trivial pos pre + 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 fdda7e754f45 -r 114eb0af123d 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 @@ -12,7 +12,7 @@ type atp_formula_role = ATP_Problem.atp_formula_role type atp_failure = ATP_Proof.atp_failure - type slice_spec = (int * string) * atp_format * string * string * bool + type atp_slice_spec = (int * string) * atp_format * string * string * bool * string type atp_config = {exec : string list * string list, arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> @@ -20,13 +20,12 @@ proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, - best_slices : Proof.context -> (real * (slice_spec * string)) list, + best_slices : Proof.context -> atp_slice_spec list, best_max_mono_iters : int, best_max_new_mono_instances : int} val default_max_mono_iters : int val default_max_new_mono_instances : int - val force_sos : bool Config.T val term_order : string Config.T val e_smartN : string val e_autoN : string @@ -47,7 +46,7 @@ val spass_H2SOS : string val isabelle_scala_function: string list * string list val remote_atp : string -> string -> string list -> (string * string) list -> - (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) -> + (atp_failure * string) list -> atp_formula_role -> (Proof.context -> atp_slice_spec) -> string * (unit -> atp_config) val add_atp : string * (unit -> atp_config) -> theory -> theory val get_atp : theory -> string -> (unit -> atp_config) @@ -77,7 +76,7 @@ val default_max_mono_iters = 3 (* FUDGE *) val default_max_new_mono_instances = 100 (* FUDGE *) -type slice_spec = (int * string) * atp_format * string * string * bool +type atp_slice_spec = (int * string) * atp_format * string * string * bool * string type atp_config = {exec : string list * string list, @@ -86,7 +85,7 @@ proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, - best_slices : Proof.context -> (real * (slice_spec * string)) list, + best_slices : Proof.context -> atp_slice_spec list, best_max_mono_iters : int, best_max_new_mono_instances : int} @@ -145,16 +144,9 @@ fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000) -fun normalize_weights xs = - let val total_weight = real (fold (curry op + o fst) xs 0) in - map (apfst (fn weight => real weight / total_weight)) xs - end - val sosN = "sos" val no_sosN = "no_sos" -val force_sos = Attrib.setup_config_bool \<^binding>\atp_force_sos\ (K false) - val smartN = "smart" (* val kboN = "kbo" *) val lpoN = "lpo" @@ -178,7 +170,7 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (((60, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], + K [((60, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} @@ -200,7 +192,7 @@ prem_role = Hypothesis, best_slices = fn _ => (* FUDGE *) - [(1.0, (((100, ""), TF1, "poly_native", liftingN, false), ""))], + [((100, meshN), TF1, "poly_native", liftingN, false, "")], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} @@ -308,14 +300,14 @@ in (* FUDGE *) if heuristic = e_smartN then - [(0.15, (((128, meshN), format, enc, main_lam_trans, false), e_fun_weightN)), - (0.15, (((128, mashN), format, enc, main_lam_trans, false), e_sym_offset_weightN)), - (0.15, (((91, mepoN), format, enc, main_lam_trans, false), e_autoN)), - (0.15, (((1000, meshN), format, "poly_guards??", main_lam_trans, false), e_sym_offset_weightN)), - (0.15, (((256, mepoN), format, enc, liftingN, false), e_fun_weightN)), - (0.25, (((64, mashN), format, enc, combsN, false), e_fun_weightN))] + [((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 - [(1.0, (((500, ""), format, enc, combsN, false), heuristic))] + [((500, meshN), format, enc, combsN, false, heuristic)] end, best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} @@ -338,7 +330,7 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (((150, ""), FOF, "mono_guards??", liftingN, false), ""))], + K [((150, meshN), FOF, "mono_guards??", liftingN, false, "")], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} @@ -363,7 +355,7 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (((40, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], + K [((40, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} @@ -384,7 +376,7 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (((512, ""), TH1, "mono_native_higher", keep_lamsN, false), ""))], + K [((512, meshN), TH1, "mono_native_higher", keep_lamsN, false, "")], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} @@ -407,7 +399,7 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (((150, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], + K [((150, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} @@ -444,14 +436,14 @@ prem_role = Conjecture, best_slices = fn _ => (* FUDGE *) - [(0.1667, (((150, meshN), format, "mono_native", combsN, true), "")), - (0.1667, (((500, meshN), format, "mono_native", liftingN, true), spass_H2SOS)), - (0.1666, (((50, meshN), format, "mono_native", liftingN, true), spass_H2LR0LT0)), - (0.1000, (((250, meshN), format, "mono_native", combsN, true), spass_H2NuVS0)), - (0.1000, (((1000, mepoN), format, "mono_native", liftingN, true), spass_H1SOS)), - (0.1000, (((150, meshN), format, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)), - (0.1000, (((300, meshN), format, "mono_native", combsN, true), spass_H2SOS)), - (0.1000, (((100, meshN), format, "mono_native", combs_and_liftingN, true), spass_H2))], + [((150, meshN), format, "mono_native", combsN, true, ""), + ((500, meshN), format, "mono_native", liftingN, true, spass_H2SOS), + ((50, meshN), format, "mono_native", liftingN, true, spass_H2LR0LT0), + ((250, meshN), format, "mono_native", combsN, true, spass_H2NuVS0), + ((1000, mepoN), format, "mono_native", liftingN, true, spass_H1SOS), + ((150, meshN), format, "poly_guards??", liftingN, false, spass_H2NuVS0Red2), + ((300, meshN), format, "mono_native", combsN, true, spass_H2SOS), + ((100, meshN), format, "mono_native", combs_and_liftingN, true, spass_H2)], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} end @@ -490,10 +482,9 @@ prem_role = Hypothesis, best_slices = fn ctxt => (* FUDGE *) - [(0.333, (((500, meshN), TX1, "mono_native_fool", combs_or_liftingN, false), sosN)), - (0.333, (((150, meshN), TX1, "poly_native_fool", combs_or_liftingN, false), sosN)), - (0.334, (((50, meshN), TX1, "mono_native_fool", combs_or_liftingN, false), no_sosN))] - |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single), + [((500, meshN), TX1, "mono_native_fool", combs_or_liftingN, false, sosN), + ((150, meshN), TX1, "poly_native_fool", combs_or_liftingN, false, sosN), + ((50, meshN), TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN)], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} @@ -511,10 +502,10 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(0.5, (((250, meshN), TF0, "mono_native", combsN, false), "")), - (0.25, (((125, mepoN), TF0, "mono_native", combsN, false), "")), - (0.125, (((62, mashN), TF0, "mono_native", combsN, false), "")), - (0.125, (((31, meshN), TF0, "mono_native", combsN, false), ""))], + K [((250, meshN), TF0, "mono_native", combsN, false, ""), + ((125, mepoN), TF0, "mono_native", combsN, false, ""), + ((62, mashN), TF0, "mono_native", combsN, false, ""), + ((31, meshN), TF0, "mono_native", combsN, false, "")], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} @@ -527,7 +518,6 @@ let val format = THF (Polymorphic, {with_ite = true, with_let = false}, THF_Without_Choice) - val enc = ((512, "meshN"), format, "mono_native_higher_fool", keep_lamsN, false) in {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]), arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ => @@ -539,13 +529,12 @@ known_szs_status_failures, prem_role = Hypothesis, best_slices = fn _ => - [(1, (enc, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" -q \"6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|fifo\" -q \"4|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-struct(1,5,2,3)\" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1")), - (1, (enc, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=2 --ho-unif-max-depth=1 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection16 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true --ho-unif-level=pragmatic-framework --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=lambda-def-invfreqrank --e-call-point=0.1")), - (1, (enc, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=off --ho-prim-enum=full --ho-prim-max=1 --avatar=off --recognize-injectivity=true --ho-elim-leibniz=4 --ho-unif-level=full-framework --no-max-vars -q \"2|prefer-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1)\" -q \"4|const|conjecture-relative-e(0.1,1,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1.5)\" -q \"4|prefer-sos|pnrefined(1,1,1,1,2,1.5,2)\" --select=ho-selection5 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=5 --e-call-point=0.25 --e-auto=true --sine=50 --sine-tolerance=2 --sine-depth-max=4 --sine-depth-min=1 --e-max-derived=96 --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=arity0 --prec-gen-fun=invfreq_conj")), - (1, (enc, "--mode=ho-pragmatic -nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=3 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=7 --sine=50 --sine-tolerance=1 --sine-depth-max=2 --sine-depth-min=1 --e-max-derived=64 --sine-ignore-k-most-common-syms=2 --sine-trim-implications=true --e-encode-lambdas=lift --scan-clause-ac=false --lambdasup=0 --kbo-weight-fun=lambda-def-invfreqrank --demod-in-var-args=true --bool-demod=true --lambda-demod=true --e-call-point=0.1")), - (1, (enc, "--mode=ho-comb-complete --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-sqarity --ho-prim-enum=none --tptp-def-as-rewrite -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --select=NoSelection --solve-formulas=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=8 --sine=60 --sine-tolerance=2 --sine-depth-max=5 --sine-depth-min=1 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --e-max-derived=50 --e-encode-lambdas=ignore --scan-clause-ac=false --presaturate=true --comb-b-penalty=3 --comb-c-penalty=3 --comb-k-penalty=1 --comb-s-penalty=5 --subvarsup=false --e-call-point=0.15")), - (1, (enc, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=0 --ho-prim-enum=none -q \"2|prefer-ho-steps|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|default\" -q \"2|prefer-empty-trail|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" --select=bb+e-selection7 --ho-pattern-decider=false --ho-fixpoint-decider=true --ho-solid-decider=false --sine=150 --sine-tolerance=2 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=2 --fluid-log-hoist=false --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-prim-enum=eq --ho-prim-enum-add-var=true --ho-prim-max=1 --ho-prim-enum-early-bird=true -o tptp --avatar=eager --split-only-ground=true"))] - |> normalize_weights, + [((512, meshN), format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" -q \"6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|fifo\" -q \"4|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-struct(1,5,2,3)\" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1"), + ((256, mashN), format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=2 --ho-unif-max-depth=1 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection16 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true --ho-unif-level=pragmatic-framework --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=lambda-def-invfreqrank --e-call-point=0.1"), + ((128, mepoN), format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=off --ho-prim-enum=full --ho-prim-max=1 --avatar=off --recognize-injectivity=true --ho-elim-leibniz=4 --ho-unif-level=full-framework --no-max-vars -q \"2|prefer-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1)\" -q \"4|const|conjecture-relative-e(0.1,1,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1.5)\" -q \"4|prefer-sos|pnrefined(1,1,1,1,2,1.5,2)\" --select=ho-selection5 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=5 --e-call-point=0.25 --e-auto=true --sine=50 --sine-tolerance=2 --sine-depth-max=4 --sine-depth-min=1 --e-max-derived=96 --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=arity0 --prec-gen-fun=invfreq_conj"), + ((1024, meshN), format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic -nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=3 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=7 --sine=50 --sine-tolerance=1 --sine-depth-max=2 --sine-depth-min=1 --e-max-derived=64 --sine-ignore-k-most-common-syms=2 --sine-trim-implications=true --e-encode-lambdas=lift --scan-clause-ac=false --lambdasup=0 --kbo-weight-fun=lambda-def-invfreqrank --demod-in-var-args=true --bool-demod=true --lambda-demod=true --e-call-point=0.1"), + ((64, meshN), format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-comb-complete --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-sqarity --ho-prim-enum=none --tptp-def-as-rewrite -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --select=NoSelection --solve-formulas=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=8 --sine=60 --sine-tolerance=2 --sine-depth-max=5 --sine-depth-min=1 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --e-max-derived=50 --e-encode-lambdas=ignore --scan-clause-ac=false --presaturate=true --comb-b-penalty=3 --comb-c-penalty=3 --comb-k-penalty=1 --comb-s-penalty=5 --subvarsup=false --e-call-point=0.15"), + ((512, meshN), format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=0 --ho-prim-enum=none -q \"2|prefer-ho-steps|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|default\" -q \"2|prefer-empty-trail|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" --select=bb+e-selection7 --ho-pattern-decider=false --ho-fixpoint-decider=true --ho-solid-decider=false --sine=150 --sine-tolerance=2 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=2 --fluid-log-hoist=false --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-prim-enum=eq --ho-prim-enum-add-var=true --ho-prim-max=1 --ho-prim-enum-early-bird=true -o tptp --avatar=eager --split-only-ground=true")], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} end @@ -601,7 +590,7 @@ proof_delims = union (op =) tstp_proof_delims proof_delims, known_failures = known_failures @ known_says_failures, prem_role = prem_role, - best_slices = fn ctxt => [(1.0, best_slice ctxt)], + best_slices = fn ctxt => [best_slice ctxt], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} : atp_config @@ -622,30 +611,30 @@ (Crashed, "Unrecoverable Segmentation Fault")] @ known_szs_status_failures) Hypothesis - (K (((50, ""), CNF_UEQ, type_enc, combsN, false), "") (* FUDGE *)) + (K ((50, meshN), CNF_UEQ, type_enc, combsN, false, "") (* FUDGE *)) val remote_agsyhol = remotify_atp agsyhol "agsyHOL" ["1.0", "1"] - (K (((60, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) + (K ((60, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "") (* FUDGE *)) val remote_alt_ergo = remotify_atp alt_ergo "Alt-Ergo" ["0.95.2"] - (K (((250, ""), TF1, "poly_native", keep_lamsN, false), "") (* FUDGE *)) + (K ((250, meshN), TF1, "poly_native", keep_lamsN, false, "") (* FUDGE *)) val remote_e = remotify_atp e "E" ["2.0", "1.9.1", "1.8"] - (K (((750, ""), TF0, "mono_native", combsN, false), "") (* FUDGE *)) + (K ((750, meshN), TF0, "mono_native", combsN, false, "") (* FUDGE *)) val remote_iprover = remotify_atp iprover "iProver" ["0.99"] - (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) + (K ((150, meshN), FOF, "mono_guards??", liftingN, false, "") (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"] - (K (((40, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *)) + (K ((40, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", liftingN, false, "") (* FUDGE *)) val remote_leo3 = remotify_atp leo3 "Leo-III" ["1.1"] - (K (((150, ""), THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *)) + (K ((150, meshN), THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "poly_native_higher", keep_lamsN, false, "") (* FUDGE *)) val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" val remote_zipperposition = remotify_atp zipperposition "Zipperpin" ["2.1", "2.0"] - (K (((512, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) + (K ((512, meshN), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "") (* FUDGE *)) (* Dummy prover *) @@ -657,26 +646,19 @@ known_failures = known_szs_status_failures, prem_role = prem_role, best_slices = - K [(1.0, (((200, "mepo"), format, type_enc, - if is_format_higher_order format then keep_lamsN - else combsN, uncurried_aliases), ""))], + K [((200, "mepo"), format, type_enc, + if is_format_higher_order format then keep_lamsN else combsN, uncurried_aliases, "")], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val dummy_fof = - let - val config = dummy_config Hypothesis FOF "mono_guards??" false - in (dummy_fofN, fn () => config) end + (dummy_fofN, fn () => dummy_config Hypothesis FOF "mono_guards??" false) val dummy_tfx = - let - val config = dummy_config Hypothesis TX1 "poly_native_fool" false - in (dummy_tfxN, fn () => config) end + (dummy_tfxN, fn () => dummy_config Hypothesis TX1 "poly_native_fool" false) val dummy_thf = - let - val config = dummy_config Hypothesis TH1 "poly_native_higher" false - in (dummy_thfN, fn () => config) end + (dummy_thfN, fn () => dummy_config Hypothesis TH1 "poly_native_higher" false) val dummy_thf_reduced = let diff -r fdda7e754f45 -r 114eb0af123d src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jan 31 16:09:23 2022 +0100 @@ -105,7 +105,7 @@ fun run_atp mode name ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, - slice, timeout, preplay_timeout, spy, ...} : params) + slices, timeout, preplay_timeout, spy, ...} : params) ({comment, state, goal, subgoal, subgoal_count, facts, found_proof} : prover_problem) = let val thy = Proof.theory_of state @@ -158,8 +158,8 @@ fun run () = let - val (_, (((best_max_facts, _), format, best_type_enc, best_lam_trans, - best_uncurried_aliases), extra)) = + val ((best_max_facts, _), format, best_type_enc, best_lam_trans, best_uncurried_aliases, + extra) = List.last (best_slices ctxt) fun monomorphize_facts facts = @@ -191,7 +191,7 @@ |> Integer.min (length facts) val strictness = if strict then Strict else Non_Strict val type_enc = type_enc |> choose_type_enc strictness best_type_enc format - val run_timeout = if slice = Time.zeroTime then timeout else slice + val run_timeout = slice_timeout slices timeout val generous_run_timeout = if mode = MaSh then one_day else run_timeout val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () => let diff -r fdda7e754f45 -r 114eb0af123d src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Jan 31 16:09:23 2022 +0100 @@ -54,7 +54,7 @@ fun default_max_facts_of_prover ctxt name = let val thy = Proof_Context.theory_of ctxt in if is_atp thy name then - fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0 + fold (Integer.max o fst o #1) (#best_slices (get_atp thy name ()) ctxt) 0 else if is_smt_prover ctxt name then SMT_Solver.default_max_relevant ctxt name else