# HG changeset patch # User blanchet # Date 1643641763 -3600 # Node ID b61949cba32abbcf8fa4e90240dfd03587e4ac21 # Parent f741d55a81e5ed7dc87f0cd07daaa3100439b364 rationalize slicing format diff -r f741d55a81e5 -r b61949cba32a src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100 @@ -313,7 +313,8 @@ (case max_facts of SOME n => n | NONE => - 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers + 0 |> fold (fn prover => Integer.max (fst (fst (get_default_slice ctxt prover)))) + provers |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)) val ({elapsed, ...}, factss) = Timing.timing (relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t) diff -r f741d55a81e5 -r b61949cba32a 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,8 @@ type atp_formula_role = ATP_Problem.atp_formula_role type atp_failure = ATP_Proof.atp_failure - type atp_slice = (int * string) * atp_format * string * string * bool * string + type base_slice = int * string + type atp_slice = atp_format * string * string * bool * string type atp_config = {exec : string list * string list, arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> @@ -20,9 +21,9 @@ proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, - best_slices : Proof.context -> atp_slice list, - best_max_mono_iters : int, - best_max_new_mono_instances : int} + good_slices : Proof.context -> (base_slice * atp_slice) list, + good_max_mono_iters : int, + good_max_new_mono_instances : int} val default_max_mono_iters : int val default_max_new_mono_instances : int @@ -46,7 +47,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 -> atp_slice) -> + (atp_failure * string) list -> atp_formula_role -> (Proof.context -> base_slice * atp_slice) -> string * (unit -> atp_config) val add_atp : string * (unit -> atp_config) -> theory -> theory val get_atp : theory -> string -> (unit -> atp_config) @@ -76,7 +77,8 @@ val default_max_mono_iters = 3 (* FUDGE *) val default_max_new_mono_instances = 100 (* FUDGE *) -type atp_slice = (int * string) * atp_format * string * string * bool * string +type base_slice = int * string +type atp_slice = atp_format * string * string * bool * string type atp_config = {exec : string list * string list, @@ -85,11 +87,11 @@ proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, - best_slices : Proof.context -> atp_slice list, - best_max_mono_iters : int, - best_max_new_mono_instances : int} + good_slices : Proof.context -> (base_slice * atp_slice) list, + good_max_mono_iters : int, + good_max_new_mono_instances : int} -(* "best_slices" must be found empirically, taking a holistic approach since the +(* "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, @@ -168,11 +170,11 @@ proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, prem_role = Hypothesis, - best_slices = + good_slices = (* FUDGE *) - 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} + K [((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} val agsyhol = (agsyholN, fn () => agsyhol_config) @@ -190,11 +192,11 @@ (TimedOut, ": Timeout"), (GaveUp, ": Unknown")], prem_role = Hypothesis, - best_slices = fn _ => + good_slices = (* FUDGE *) - [((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} + K [((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} val alt_ergo = (alt_ergoN, fn () => alt_ergo_config) @@ -287,7 +289,7 @@ (TimedOut, "time limit exceeded")] @ known_szs_status_failures, prem_role = Conjecture, - best_slices = fn ctxt => + good_slices = fn ctxt => let val heuristic = Config.get ctxt e_selection_heuristic val (format, enc, main_lam_trans) = @@ -300,17 +302,17 @@ 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)] + [((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)] + [((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} + good_max_mono_iters = default_max_mono_iters, + good_max_new_mono_instances = default_max_new_mono_instances} val e = (eN, fn () => e_config) @@ -328,11 +330,11 @@ [(ProofIncomplete, "% SZS output start CNFRefutation")] @ known_szs_status_failures, prem_role = Hypothesis, - best_slices = + good_slices = (* FUDGE *) - 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} + K [((150, meshN), (FOF, "mono_guards??", liftingN, false, ""))], + good_max_mono_iters = default_max_mono_iters, + good_max_new_mono_instances = default_max_new_mono_instances} val iprover = (iproverN, fn () => iprover_config) @@ -353,11 +355,11 @@ (GaveUp, "No.of.Axioms")] @ known_szs_status_failures, prem_role = Hypothesis, - best_slices = + good_slices = (* FUDGE *) - 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} + K [((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} val leo2 = (leo2N, fn () => leo2_config) @@ -374,11 +376,11 @@ proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, prem_role = Hypothesis, - best_slices = + good_slices = (* FUDGE *) - 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} + K [((512, meshN), (TH1, "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} val leo3 = (leo3N, fn () => leo3_config) @@ -397,11 +399,11 @@ [("% SZS output start Proof", "% SZS output end Proof")], known_failures = known_szs_status_failures, prem_role = Hypothesis, - best_slices = + good_slices = (* FUDGE *) - 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} + K [((150, 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} val satallax = (satallaxN, fn () => satallax_config) @@ -434,18 +436,18 @@ (Unprovable, "No formulae and clauses found in input file"), (InternalError, "Please report this error")], prem_role = Conjecture, - best_slices = fn _ => + good_slices = (* FUDGE *) - [((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} + 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))], + good_max_mono_iters = default_max_mono_iters, + good_max_new_mono_instances = default_max_new_mono_instances} end val spass = (spassN, fn () => spass_config) @@ -480,13 +482,13 @@ (Interrupted, "Aborted by signal SIGINT")] @ known_szs_status_failures, prem_role = Hypothesis, - best_slices = fn ctxt => + good_slices = (* FUDGE *) - [((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 *)} + K [((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))], + good_max_mono_iters = default_max_mono_iters, + good_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} val vampire = (vampireN, fn () => vampire_config) @@ -500,14 +502,14 @@ proof_delims = [("SZS status Theorem", "")], known_failures = known_szs_status_failures, prem_role = Hypothesis, - best_slices = + good_slices = (* FUDGE *) - 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 *)} + 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, ""))], + good_max_mono_iters = default_max_mono_iters, + good_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} val z3_tptp = (z3_tptpN, fn () => z3_tptp_config) @@ -528,15 +530,15 @@ [(TimedOut, "SZS status ResourceOut")] @ (* odd way of timing out *) known_szs_status_failures, prem_role = Hypothesis, - best_slices = fn _ => - [((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} + good_slices = + K [((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"))], + good_max_mono_iters = default_max_mono_iters, + good_max_new_mono_instances = default_max_new_mono_instances} end val zipperposition = (zipperpositionN, fn () => zipperposition_config) @@ -581,7 +583,7 @@ val isabelle_scala_function = (["SCALA_HOME"], ["bin/scala"]) -fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice = +fun remote_config system_name system_versions proof_delims known_failures prem_role good_slice = {exec = isabelle_scala_function, arguments = fn _ => fn _ => fn command => fn timeout => fn problem => fn _ => [the_remote_system system_name system_versions, @@ -590,19 +592,19 @@ proof_delims = union (op =) tstp_proof_delims proof_delims, known_failures = known_failures @ known_says_failures, prem_role = prem_role, - 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 + good_slices = fn ctxt => [good_slice ctxt], + good_max_mono_iters = default_max_mono_iters, + good_max_new_mono_instances = default_max_new_mono_instances} : atp_config -fun remotify_config system_name system_versions best_slice +fun remotify_config system_name system_versions good_slice ({proof_delims, known_failures, prem_role, ...} : atp_config) = - remote_config system_name system_versions proof_delims known_failures prem_role best_slice + remote_config system_name system_versions proof_delims known_failures prem_role good_slice -fun remote_atp name system_name system_versions proof_delims known_failures prem_role best_slice = +fun remote_atp name system_name system_versions proof_delims known_failures prem_role good_slice = (remote_prefix ^ name, fn () => - remote_config system_name system_versions proof_delims known_failures prem_role best_slice) -fun remotify_atp (name, config) system_name system_versions best_slice = - (remote_prefix ^ name, remotify_config system_name system_versions best_slice o config) + remote_config system_name system_versions proof_delims known_failures prem_role good_slice) +fun remotify_atp (name, config) system_name system_versions good_slice = + (remote_prefix ^ name, remotify_config system_name system_versions good_slice o config) fun gen_remote_waldmeister name type_enc = remote_atp name "Waldmeister" ["710"] tstp_proof_delims @@ -611,30 +613,30 @@ (Crashed, "Unrecoverable Segmentation Fault")] @ known_szs_status_failures) Hypothesis - (K ((50, meshN), 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, meshN), 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, meshN), 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, meshN), 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, meshN), 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, meshN), 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, meshN), 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, meshN), 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 *) @@ -645,11 +647,11 @@ proof_delims = [], known_failures = known_szs_status_failures, prem_role = prem_role, - best_slices = - 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} + good_slices = + K [((200, "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} val dummy_fof = (dummy_fofN, fn () => dummy_config Hypothesis FOF "mono_guards??" false) diff -r f741d55a81e5 -r b61949cba32a src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jan 31 16:09:23 2022 +0100 @@ -14,6 +14,7 @@ type fact = Sledgehammer_Fact.fact type proof_method = Sledgehammer_Proof_Methods.proof_method type play_outcome = Sledgehammer_Proof_Methods.play_outcome + type base_slice = Sledgehammer_ATP_Systems.base_slice type atp_slice = Sledgehammer_ATP_Systems.atp_slice datatype mode = Auto_Try | Try | Normal | Minimize | MaSh @@ -62,9 +63,7 @@ factss : (string * fact list) list, found_proof : string -> unit} - datatype prover_slice = - ATP_Slice of atp_slice - | SMT_Slice of int * string + type prover_slice = base_slice * atp_slice option type prover_result = {outcome : atp_failure option, @@ -199,9 +198,7 @@ factss : (string * fact list) list, found_proof : string -> unit} -datatype prover_slice = - ATP_Slice of atp_slice -| SMT_Slice of int * string +type prover_slice = base_slice * atp_slice option type prover_result = {outcome : atp_failure option, diff -r f741d55a81e5 -r b61949cba32a 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 @@ -112,11 +112,11 @@ val thy = Proof.theory_of state val ctxt = Proof.context_of state - val ATP_Slice ((best_max_facts, best_fact_filter), format, best_type_enc, best_lam_trans, - best_uncurried_aliases, extra) = slice + val ((good_max_facts, good_fact_filter), SOME (good_format, good_type_enc, good_lam_trans, + good_uncurried_aliases, extra)) = slice - val {exec, arguments, proof_delims, known_failures, prem_role, best_max_mono_iters, - best_max_new_mono_instances, ...} = get_atp thy name () + val {exec, arguments, proof_delims, known_failures, prem_role, good_max_mono_iters, + good_max_new_mono_instances, ...} = get_atp thy name () val full_proofs = isar_proofs |> the_default (mode = Minimize) val local_name = perhaps (try (unprefix remote_prefix)) name @@ -166,8 +166,8 @@ let val ctxt = ctxt - |> repair_monomorph_context max_mono_iters best_max_mono_iters max_new_mono_instances - best_max_new_mono_instances + |> repair_monomorph_context max_mono_iters good_max_mono_iters max_new_mono_instances + good_max_new_mono_instances (* pseudo-theorem involving the same constants as the subgoal *) val subgoal_th = Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy @@ -183,31 +183,31 @@ |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) end - val effective_fact_filter = fact_filter |> the_default best_fact_filter + val effective_fact_filter = fact_filter |> the_default good_fact_filter val facts = get_facts_of_filter effective_fact_filter factss val num_facts = (case max_facts of - NONE => best_max_facts + NONE => good_max_facts | SOME max_facts => max_facts) |> 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 type_enc = type_enc |> choose_type_enc strictness good_type_enc good_format 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 val sound = is_type_enc_sound type_enc - val generate_info = (case format of DFG _ => true | _ => false) + val generate_info = (case good_format of DFG _ => true | _ => false) val readable_names = not (Config.get ctxt atp_full_names) - val lam_trans = lam_trans |> the_default best_lam_trans - val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases + val lam_trans = lam_trans |> the_default good_lam_trans + val uncurried_aliases = uncurried_aliases |> the_default good_uncurried_aliases in facts |> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) |> take num_facts |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd Thm.prop_of) - |> generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode + |> generate_atp_problem ctxt generate_info good_format prem_role type_enc atp_mode lam_trans uncurried_aliases readable_names true hyp_ts concl_t end) () @@ -233,7 +233,7 @@ val _ = atp_problem - |> lines_of_atp_problem format ord ord_info + |> lines_of_atp_problem good_format ord ord_info |> (exec <> isabelle_scala_function) ? cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path @@ -268,7 +268,7 @@ | NONE => (found_proof name; NONE)) | _ => outcome) in - (atp_problem_data, (output, run_time, facts, atp_proof, outcome), (format, type_enc)) + (atp_problem_data, (output, run_time, facts, atp_proof, outcome), (good_format, type_enc)) end (* If the problem file has not been exported, remove it; otherwise, export diff -r f741d55a81e5 -r b61949cba32a 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 @@ -17,7 +17,6 @@ val is_prover_supported : Proof.context -> string -> bool val is_prover_installed : Proof.context -> string -> bool - val default_max_facts_of_prover : Proof.context -> string -> int val get_prover : Proof.context -> mode -> string -> prover val get_default_slice : Proof.context -> string -> prover_slice @@ -53,16 +52,6 @@ fun is_prover_installed ctxt = is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt) -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) (#best_slices (get_atp thy name ()) ctxt) 0 - else if is_smt_prover ctxt name then - SMT_Solver.default_max_relevant ctxt name - else - error ("No such prover: " ^ name) - end - fun get_prover ctxt mode name = let val thy = Proof_Context.theory_of ctxt in if is_atp thy name then run_atp mode name @@ -73,9 +62,9 @@ fun get_default_slice ctxt name = let val thy = Proof_Context.theory_of ctxt in if is_atp thy name then - ATP_Slice (List.last (#best_slices (get_atp thy name ()) ctxt)) + apsnd SOME (List.last (#good_slices (get_atp thy name ()) ctxt)) else if is_smt_prover ctxt name then - SMT_Slice (SMT_Solver.default_max_relevant ctxt name, "") + ((SMT_Solver.default_max_relevant ctxt name, ""), NONE) else error ("No such prover: " ^ name) end diff -r f741d55a81e5 -r b61949cba32a src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Jan 31 16:09:23 2022 +0100 @@ -116,10 +116,10 @@ let val ctxt = Proof.context_of state - val SMT_Slice (best_max_facts, best_fact_filter) = slice + val ((best_max_facts, best_fact_filter), _) = slice val effective_fact_filter = fact_filter |> the_default best_fact_filter - val facts = get_facts_of_filter effective_fact_filter factss + val facts = take best_max_facts (get_facts_of_filter effective_fact_filter factss) val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} = smt_filter name params state goal subgoal facts diff -r f741d55a81e5 -r b61949cba32a src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Mon Jan 31 16:09: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 = default_max_facts_of_prover ctxt name + val default_max_facts = fst (fst (get_default_slice 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