# HG changeset patch # User blanchet # Date 1648212743 -3600 # Node ID d9bb81999d2cb00fc0da8ab4e97ffa3cc090900d # Parent 73034d38568846e28ceb97973a7cdd47f7f26c1a first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size' diff -r 73034d385688 -r d9bb81999d2c src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Fri Mar 25 13:25:26 2022 +0100 +++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Mar 25 13:52:23 2022 +0100 @@ -21,7 +21,7 @@ command: unit -> string list, options: Proof.context -> string list, smt_options: (string * string) list, - good_slices: ((int * string) * string list) list, + good_slices: ((int * int * string) * string list) list, outcome: string -> string list -> outcome * string list, parse_proof: (Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> @@ -30,7 +30,7 @@ (*registry*) val add_solver: solver_config -> theory -> theory - val good_slices: Proof.context -> string -> ((int * string) * string list) list + val good_slices: Proof.context -> string -> ((int * int * string) * string list) list (*filter*) val smt_filter: Proof.context -> thm -> ((string * ATP_Problem_Generate.stature) * thm) list -> @@ -155,7 +155,7 @@ command: unit -> string list, options: Proof.context -> string list, smt_options: (string * string) list, - good_slices: ((int * string) * string list) list, + good_slices: ((int * int * string) * string list) list, outcome: string -> string list -> outcome * string list, parse_proof: (Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> @@ -180,7 +180,7 @@ type solver_info = { command: unit -> string list, smt_options: (string * string) list, - good_slices: ((int * string) * string list) list, + good_slices: ((int * int * string) * string list) list, parse_proof: Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> parsed_proof, diff -r 73034d385688 -r d9bb81999d2c src/HOL/Tools/SMT/smt_systems.ML --- a/src/HOL/Tools/SMT/smt_systems.ML Fri Mar 25 13:25:26 2022 +0100 +++ b/src/HOL/Tools/SMT/smt_systems.ML Fri Mar 25 13:52:23 2022 +0100 @@ -96,13 +96,13 @@ smt_options = [(":produce-unsat-cores", "true")], good_slices = (* FUDGE *) - [((512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]), - ((64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]), - ((1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]), - ((256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]), - ((32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]), - ((128, meshN), ["--no-e-matching", "--full-saturate-quant"]), - ((256, meshN), ["--finite-model-find", "--fmf-inst-engine"])], + [((1, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]), + ((1, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]), + ((1, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]), + ((1, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]), + ((1, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]), + ((1, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]), + ((1, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])], outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), parse_proof = SOME (K CVC4_Proof_Parse.parse_proof), replay = NONE } @@ -141,12 +141,12 @@ smt_options = [(":produce-proofs", "true")], good_slices = (* FUDGE *) - [((1024, meshN), []), - ((512, mashN), []), - ((64, meshN), []), - ((128, meshN), []), - ((256, mepoN), []), - ((32, meshN), [])], + [((1, 1024, meshN), []), + ((1, 512, mashN), []), + ((1, 64, meshN), []), + ((1, 128, meshN), []), + ((1, 256, mepoN), []), + ((1, 32, meshN), [])], outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "Time limit exceeded"), parse_proof = SOME (K Lethe_Proof_Parse.parse_proof), replay = SOME Verit_Replay.replay } @@ -182,12 +182,12 @@ smt_options = [(":produce-proofs", "true")], good_slices = (* FUDGE *) - [((1024, meshN), []), - ((512, mepoN), []), - ((64, meshN), []), - ((256, meshN), []), - ((128, mashN), []), - ((32, meshN), [])], + [((1, 1024, meshN), []), + ((1, 512, mepoN), []), + ((1, 64, meshN), []), + ((1, 256, meshN), []), + ((1, 128, mashN), []), + ((1, 32, meshN), [])], outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), parse_proof = SOME Z3_Replay.parse_proof, replay = SOME Z3_Replay.replay } diff -r 73034d385688 -r d9bb81999d2c src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Mar 25 13:25:26 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Mar 25 13:52:23 2022 +0100 @@ -136,7 +136,7 @@ fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn (problem as {state, subgoal, factss, ...} : prover_problem) - (slice as ((num_facts, fact_filter), _)) name = + (slice as ((_, num_facts, fact_filter), _)) name = let val ctxt = Proof.context_of state @@ -273,10 +273,10 @@ cat_lines (map (fn (filter, facts) => string_of_facts filter facts) factss) val default_slice_schedule = - (* FUDGE (based on Seventeen evaluation) *) - [cvc4N, zipperpositionN, vampireN, veritN, eN, cvc4N, zipperpositionN, cvc4N, vampireN, cvc4N, - cvc4N, vampireN, cvc4N, eN, iproverN, zipperpositionN, vampireN, eN, vampireN, zipperpositionN, - z3N, cvc4N, vampireN, iproverN, vampireN, zipperpositionN, z3N, z3N, cvc4N, cvc4N] + (* FUDGE (inspired by Seventeen evaluation) *) + [cvc4N, zipperpositionN, vampireN, eN, veritN, cvc4N, zipperpositionN, cvc4N, vampireN, cvc4N, + cvc4N, vampireN, cvc4N, iproverN, zipperpositionN, vampireN, vampireN, zipperpositionN, z3N, + cvc4N, vampireN, iproverN, vampireN, zipperpositionN, z3N, z3N, cvc4N, cvc4N] fun schedule_of_provers provers num_slices = let @@ -303,10 +303,11 @@ fun triplicate_slices original = let val shift = - map (apfst (apsnd (fn fact_filter => - if fact_filter = mashN then mepoN - else if fact_filter = mepoN then meshN - else mashN))) + map (apfst (fn (slice_size, num_facts, fact_filter) => + (slice_size, num_facts, + if fact_filter = mashN then mepoN + else if fact_filter = mepoN then meshN + else mashN))) val shifted_once = shift original val shifted_twice = shift shifted_once @@ -320,13 +321,13 @@ the_default uncurried_aliases0 uncurried_aliases, extra_extra0) | adjust_extra (extra as SMT_Slice _) = extra - fun adjust_slice ((num_facts0, fact_filter0), extra) = + fun adjust_slice ((slice_size0, num_facts0, fact_filter0), extra) = let val fact_filter = fact_filter |> the_default fact_filter0 val max_facts = max_facts |> the_default num_facts0 val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss)) in - ((num_facts, fact_filter), adjust_extra extra) + ((slice_size0, num_facts, fact_filter), adjust_extra extra) end val provers = distinct (op =) schedule @@ -397,7 +398,7 @@ SOME n => n | NONE => fold (fn prover => - fold (fn ((n, _), _) => Integer.max n) (get_slices ctxt prover)) + fold (fn ((_, n, _), _) => Integer.max n) (get_slices ctxt prover)) provers 0) * 51 div 50 (* some slack to account for filtering of induction facts below *) diff -r 73034d385688 -r d9bb81999d2c src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Mar 25 13:25:26 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Mar 25 13:52:23 2022 +0100 @@ -12,7 +12,7 @@ type atp_formula_role = ATP_Problem.atp_formula_role type atp_failure = ATP_Proof.atp_failure - type base_slice = int * string + type base_slice = int * int * string type atp_slice = atp_format * string * string * bool * string type atp_config = {exec : string list * string list, @@ -77,7 +77,11 @@ val default_max_mono_iters = 3 (* FUDGE *) val default_max_new_mono_instances = 100 (* FUDGE *) -type base_slice = int * string +(* desired slice size, desired number of facts, fact filter *) +type base_slice = int * int * string + +(* problem file format, type encoding, lambda translation scheme, uncurried aliases?, extra + arguments to prover *) type atp_slice = atp_format * string * string * bool * string type atp_config = @@ -91,22 +95,8 @@ good_max_mono_iters : int, good_max_new_mono_instances : int} -(* "good_slices" must be found empirically, taking a holistic approach since the - ATPs are run in parallel. Each slice has the format - - (time_frac, ((max_facts, fact_filter), format, type_enc, - lam_trans, uncurried_aliases), extra) - - where - - time_frac = faction of the time available given to the slice (which should - add up to 1.0) - - extra = extra information to the prover (e.g., SOS or no SOS). - - The last slice should be the most "normal" one, because it will get all the - time available if the other slices fail early and also because it is used if - slicing is disabled (e.g., by the minimizer). *) +(* "good_slices" must be found empirically, ideally taking a holistic approach since the ATPs are + run in parallel. *) val mepoN = "mepo" val mashN = "mash" @@ -172,7 +162,7 @@ prem_role = Hypothesis, good_slices = (* FUDGE *) - K [((60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], + K [((1, 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_max_new_mono_instances = default_max_new_mono_instances} @@ -194,7 +184,7 @@ prem_role = Hypothesis, good_slices = (* FUDGE *) - K [((100, meshN), (TF1, "poly_native", liftingN, false, ""))], + K [((1000 (* infinity *), 100, meshN), (TF1, "poly_native", liftingN, false, ""))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} @@ -297,12 +287,12 @@ (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN) in (* FUDGE *) - K [((512, meshN), (format, type_enc, lam_trans, false, e_fun_weightN)), - ((1024, meshN), (format, type_enc, lam_trans, false, e_sym_offset_weightN)), - ((128, mepoN), (format, type_enc, lam_trans, false, e_autoscheduleN)), - ((724, meshN), (format, "poly_guards??", lam_trans, false, e_sym_offset_weightN)), - ((256, mepoN), (format, type_enc, liftingN, false, e_fun_weightN)), - ((64, mashN), (format, type_enc, combsN, false, e_fun_weightN))] + K [((1, 512, meshN), (format, type_enc, lam_trans, false, e_fun_weightN)), + ((1, 1024, meshN), (format, type_enc, lam_trans, false, e_sym_offset_weightN)), + ((1, 128, mepoN), (format, type_enc, lam_trans, false, e_autoscheduleN)), + ((1, 724, meshN), (format, "poly_guards??", lam_trans, false, e_sym_offset_weightN)), + ((1, 256, mepoN), (format, type_enc, liftingN, false, e_fun_weightN)), + ((1, 64, mashN), (format, type_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} @@ -325,11 +315,11 @@ prem_role = Hypothesis, good_slices = (* FUDGE *) - K [((32, meshN), (TF0, "mono_native", liftingN, false, "")), - ((512, meshN), (TX0, "mono_native", liftingN, false, "")), - ((128, mashN), (TF0, "mono_native", combsN, false, "")), - ((1024, meshN), (TF0, "mono_native", liftingN, false, "")), - ((256, mepoN), (TF0, "mono_native", combsN, false, ""))], + K [((1, 32, meshN), (TF0, "mono_native", liftingN, false, "")), + ((1, 512, meshN), (TX0, "mono_native", liftingN, false, "")), + ((1, 128, mashN), (TF0, "mono_native", combsN, false, "")), + ((1, 1024, meshN), (TF0, "mono_native", liftingN, false, "")), + ((1, 256, mepoN), (TF0, "mono_native", combsN, false, ""))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} @@ -354,7 +344,7 @@ prem_role = Hypothesis, good_slices = (* FUDGE *) - K [((40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], + K [((1, 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_max_new_mono_instances = default_max_new_mono_instances} @@ -375,8 +365,8 @@ prem_role = Hypothesis, good_slices = (* FUDGE *) - K [((512, meshN), (TH0, "mono_native_higher", keep_lamsN, false, "")), - ((512, meshN), (TF0, "mono_native", liftingN, false, ""))], + K [((3, 512, meshN), (TH0, "mono_native_higher", keep_lamsN, false, "")), + ((3, 512, meshN), (TF0, "mono_native", liftingN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_max_new_mono_instances = default_max_new_mono_instances} @@ -399,7 +389,7 @@ prem_role = Hypothesis, good_slices = (* FUDGE *) - K [((256, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], + K [((6, 256, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_max_new_mono_instances = default_max_new_mono_instances} @@ -436,14 +426,14 @@ prem_role = Conjecture, good_slices = (* FUDGE *) - K [((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))], + K [((1, 150, meshN), (format, "mono_native", combsN, true, "")), + ((1, 500, meshN), (format, "mono_native", liftingN, true, spass_H2SOS)), + ((1, 50, meshN), (format, "mono_native", liftingN, true, spass_H2LR0LT0)), + ((1, 250, meshN), (format, "mono_native", combsN, true, spass_H2NuVS0)), + ((1, 1000, mepoN), (format, "mono_native", liftingN, true, spass_H1SOS)), + ((1, 150, meshN), (format, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)), + ((1, 300, meshN), (format, "mono_native", combsN, true, spass_H2SOS)), + ((1, 100, meshN), (format, "mono_native", combs_and_liftingN, true, spass_H2))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} end @@ -482,14 +472,14 @@ prem_role = Hypothesis, good_slices = (* FUDGE *) - K [((512, meshN), (TX1, "mono_native_fool", combsN, false, sosN)), - ((1024, meshN), (TX1, "mono_native_fool", liftingN, false, sosN)), - ((256, mashN), (TX1, "mono_native_fool", liftingN, false, no_sosN)), - ((512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)), - ((16, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN)), - ((32, meshN), (TX1, "mono_native_fool", combsN, false, no_sosN)), - ((64, meshN), (TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN)), - ((128, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN))], + K [((1, 512, meshN), (TX1, "mono_native_fool", combsN, false, sosN)), + ((1, 1024, meshN), (TX1, "mono_native_fool", liftingN, false, sosN)), + ((1, 256, mashN), (TX1, "mono_native_fool", liftingN, false, no_sosN)), + ((1, 512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)), + ((1, 16, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN)), + ((1, 32, meshN), (TX1, "mono_native_fool", combsN, false, no_sosN)), + ((1, 64, meshN), (TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN)), + ((1, 128, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} @@ -513,12 +503,12 @@ known_szs_status_failures, prem_role = Hypothesis, good_slices = - K [((1024, 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")), - ((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")), - ((512, 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")), - ((32, 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 --lazy-cnf-kind=simp")), - ((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 --lazy-cnf-kind=simp --trigger-bool-ind=1")), - ((256, 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"))], + K [((1, 1024, 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")), + ((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")), + ((1, 512, 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")), + ((1, 32, 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 --lazy-cnf-kind=simp")), + ((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 --lazy-cnf-kind=simp --trigger-bool-ind=1")), + ((1, 256, 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"))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} end @@ -595,30 +585,30 @@ (Crashed, "Unrecoverable Segmentation Fault")] @ known_szs_status_failures) Hypothesis - (K ((50, meshN), (CNF_UEQ, type_enc, combsN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), 50, meshN), (CNF_UEQ, type_enc, combsN, false, "")) (* FUDGE *)) val remote_agsyhol = remotify_atp agsyhol "agsyHOL" ["1.0", "1"] - (K ((60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), 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, meshN), (TF1, "poly_native", keep_lamsN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), 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, meshN), (TF0, "mono_native", combsN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), 750, meshN), (TF0, "mono_native", combsN, false, "")) (* FUDGE *)) val remote_iprover = remotify_atp iprover "iProver" ["0.99"] - (K ((150, meshN), (FOF, "mono_guards??", liftingN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), 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, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", liftingN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), 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, meshN), (THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "poly_native_higher", keep_lamsN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), 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, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), 512, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *)) (* Dummy prover *) @@ -630,7 +620,7 @@ known_failures = known_szs_status_failures, prem_role = prem_role, good_slices = - K [((200, "mepo"), (format, type_enc, + K [((1, 256, "mepo"), (format, type_enc, if is_format_higher_order format then keep_lamsN else combsN, uncurried_aliases, ""))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} diff -r 73034d385688 -r d9bb81999d2c src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Mar 25 13:25:26 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Mar 25 13:52:23 2022 +0100 @@ -239,7 +239,7 @@ SOME facts => facts | NONE => snd (hd factss)) -fun facts_of_basic_slice (num_facts, fact_filter) factss = +fun facts_of_basic_slice (desired_slices, num_facts, fact_filter) factss = facts_of_filter fact_filter factss |> take num_facts diff -r 73034d385688 -r d9bb81999d2c src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Mar 25 13:25:26 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Mar 25 13:52:23 2022 +0100 @@ -107,7 +107,8 @@ ({comment, state, goal, subgoal, subgoal_count, factss, found_proof} : prover_problem) slice = let - val (basic_slice, ATP_Slice (good_format, good_type_enc, good_lam_trans, good_uncurried_aliases, extra)) = + val (basic_slice, ATP_Slice (good_format, good_type_enc, good_lam_trans, + good_uncurried_aliases, extra)) = slice val facts = facts_of_basic_slice basic_slice factss val thy = Proof.theory_of state diff -r 73034d385688 -r d9bb81999d2c src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Fri Mar 25 13:25:26 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Fri Mar 25 13:52:23 2022 +0100 @@ -33,7 +33,7 @@ val params as {provers, induction_rules, max_facts, ...} = default_params thy override_params val name = hd provers val prover = get_prover ctxt mode name - val default_max_facts = fst (fst (hd (get_slices ctxt name))) + val default_max_facts = #2 (fst (hd (get_slices ctxt name))) val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt val keywords = Thy_Header.get_keywords' ctxt val css_table = clasimpset_rule_table_of ctxt