# HG changeset patch # User blanchet # Date 1643641763 -3600 # Node ID dc6769b86fd67daa9d7975f4ba70ef454cf3cc80 # Parent b49329185b828b7910deee5f28f469cfef0d54b3 crude implementation of centralized slicing diff -r b49329185b82 -r dc6769b86fd6 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Sledgehammer.thy Mon Jan 31 16:09:23 2022 +0100 @@ -35,4 +35,22 @@ ML_file \Tools/Sledgehammer/sledgehammer_commands.ML\ ML_file \Tools/Sledgehammer/sledgehammer_tactics.ML\ +(* +lemma "1 + 1 = 2 \ 0 + (x::nat) = x" + sledgehammer +*) + +(* +declare nat_induct[no_atp] +declare nat_induct_non_zero[no_atp] + +lemma "P 0 \ (\n. P n \ P (Suc n)) \ P n" + sledgehammer [cvc4] (add: nat.induct) +*) + +(* +lemma "1 + 1 = 2 \ 0 + (x::nat) = x" + sledgehammer [verbose, e, dont_preplay, max_facts = 2] (add_0_left one_add_one) +*) + end diff -r b49329185b82 -r dc6769b86fd6 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Jan 31 16:09:23 2022 +0100 @@ -43,6 +43,7 @@ val agsyholN : string val alt_ergoN : string + val cvc4N : string val eN : string val iproverN : string val leo2N : string @@ -50,7 +51,9 @@ val satallaxN : string val spassN : string val vampireN : string + val veritN : string val waldmeisterN : string + val z3N : string val z3_tptpN : string val zipperpositionN : string val remote_prefix : string @@ -107,6 +110,7 @@ val agsyholN = "agsyhol" val alt_ergoN = "alt_ergo" +val cvc4N = "cvc4" val eN = "e" val iproverN = "iprover" val leo2N = "leo2" @@ -114,10 +118,13 @@ val satallaxN = "satallax" val spassN = "spass" val vampireN = "vampire" +val veritN = "verit" val waldmeisterN = "waldmeister" +val z3N = "z3" val z3_tptpN = "z3_tptp" val zipperpositionN = "zipperposition" val remote_prefix = "remote_" + val dummy_fofN = "dummy_fof" val dummy_tfxN = "dummy_tfx" val dummy_thfN = "dummy_thf" diff -r b49329185b82 -r dc6769b86fd6 src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Jan 31 16:09:23 2022 +0100 @@ -21,7 +21,7 @@ command: unit -> string list, options: Proof.context -> string list, smt_options: (string * string) list, - default_max_relevant: int, + good_slices: (int * string) 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 default_max_relevant: Proof.context -> string -> int + val good_slices: Proof.context -> string -> (int * string) 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, - default_max_relevant: int, + good_slices: (int * string) 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, - default_max_relevant: int, + good_slices: (int * string) list, parse_proof: Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> parsed_proof, @@ -220,13 +220,13 @@ val cfalse = Thm.cterm_of \<^context> \<^prop>\False\ in -fun add_solver ({name, class, avail, command, options, smt_options, default_max_relevant, outcome, +fun add_solver ({name, class, avail, command, options, smt_options, good_slices, outcome, parse_proof = parse_proof0, replay = replay0} : solver_config) = let fun solver oracle = { command = command, smt_options = smt_options, - default_max_relevant = default_max_relevant, + good_slices = good_slices, parse_proof = parse_proof (outcome name) parse_proof0, replay = replay (outcome name) replay0 oracle} @@ -245,7 +245,7 @@ let val name = SMT_Config.solver_of ctxt in (name, get_info ctxt name) end -val default_max_relevant = #default_max_relevant oo get_info +val good_slices = #good_slices oo get_info fun apply_solver_and_replay ctxt thms0 = let diff -r b49329185b82 -r dc6769b86fd6 src/HOL/Tools/SMT/smt_systems.ML --- a/src/HOL/Tools/SMT/smt_systems.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/SMT/smt_systems.ML Mon Jan 31 16:09:23 2022 +0100 @@ -13,6 +13,10 @@ structure SMT_Systems: SMT_SYSTEMS = struct +val mashN = "mash" +val mepoN = "mepo" +val meshN = "mesh" + (* helper functions *) fun check_tool var () = @@ -90,7 +94,14 @@ command = make_command "CVC4", options = cvc4_options, smt_options = [(":produce-unsat-cores", "true")], - default_max_relevant = 400 (* FUDGE *), + good_slices = + (* FUDGE *) + [(512, meshN), + (64, meshN), + (1024, meshN), + (256, mepoN), + (32, meshN), + (128, meshN)], outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), parse_proof = SOME (K CVC4_Proof_Parse.parse_proof), replay = NONE } @@ -127,7 +138,14 @@ command = the o check_tool "ISABELLE_VERIT", options = veriT_options, smt_options = [(":produce-proofs", "true")], - default_max_relevant = 200 (* FUDGE *), + good_slices = + (* FUDGE *) + [(1024, meshN), + (512, mashN), + (64, meshN), + (128, meshN), + (256, mepoN), + (32, meshN)], outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "Time limit exceeded"), parse_proof = SOME (K VeriT_Proof_Parse.parse_proof), replay = SOME Verit_Replay.replay } @@ -161,7 +179,14 @@ command = make_command "Z3", options = z3_options, smt_options = [(":produce-proofs", "true")], - default_max_relevant = 350 (* FUDGE *), + good_slices = + (* FUDGE *) + [(1024, meshN), + (512, mepoN), + (64, meshN), + (256, meshN), + (128, mashN), + (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 b49329185b82 -r dc6769b86fd6 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 @@ -38,6 +38,7 @@ struct open ATP_Util +open ATP_Problem open ATP_Proof open ATP_Problem_Generate open Sledgehammer_Util @@ -46,6 +47,7 @@ open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay open Sledgehammer_Isar_Minimize +open Sledgehammer_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_Minimize @@ -81,9 +83,6 @@ |> the_default (SH_Unknown, "") end -fun is_metis_method (Metis_Method _) = true - | is_metis_method _ = false - fun play_one_line_proof minimize timeout used_facts state i (preferred_meth, methss) = (if timeout = Time.zeroTime then (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) @@ -116,8 +115,7 @@ in (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of (res as (meth, Played time)) :: _ => - (* if a fact is needed by an ATP, it will be needed by "metis" *) - if not minimize orelse is_metis_method meth then + if not minimize then (used_facts, res) else let @@ -265,6 +263,59 @@ cat_lines (map (fn (filter, facts) => (if filter = "" then "" else filter ^ ": ") ^ string_of_facts 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] + +fun schedule_of_provers provers num_slices = + let + val num_default_slices = length default_slice_schedule + val unknown_provers = filter_out (member (op =) default_slice_schedule) provers + + fun round_robin _ [] = [] + | round_robin 0 _ = [] + | round_robin n (prover :: provers) = prover :: round_robin (n - 1) (provers @ [prover]) + in + if num_slices <= num_default_slices then + take num_slices default_slice_schedule + else + default_slice_schedule @ round_robin (num_slices - num_default_slices) unknown_provers + end + +fun prover_slices_of_schedule ctxt schedule = + let + 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))) + + val shifted_once = shift original + val shifted_twice = shift shifted_once + in + original @ shifted_once @ shifted_twice + end + + val provers = distinct (op =) schedule + val prover_slices = + map (fn prover => (prover, triplicate_slices (get_slices ctxt prover))) provers + + fun translate _ [] = [] + | translate prover_slices (prover :: schedule) = + (case AList.lookup (op =) prover_slices prover of + SOME (slice :: slices) => + let val prover_slices' = AList.update (op =) (prover, slices) prover_slices in + (prover, slice) :: translate prover_slices' schedule + end + | _ => translate prover_slices schedule) + in + translate prover_slices schedule + end + fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, ...}) mode writeln_result i (fact_override as {only, ...}) state = if null provers then @@ -309,8 +360,9 @@ (case max_facts of SOME n => n | NONE => - fold (fn prover => Integer.max (fst (fst (get_default_slice ctxt prover)))) provers - 0) + fold (fn prover => + fold (fn ((n, _), _) => Integer.max n) (get_slices ctxt prover)) + provers 0) val ({elapsed, ...}, factss) = Timing.timing (relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t) @@ -336,17 +388,25 @@ factss = get_factss provers, found_proof = found_proof} val learn = mash_learn_proof ctxt params (Thm.prop_of goal) val launch = launch_prover_and_preplay params mode writeln_result learn + + val schedule = + if mode = Auto_Try then + provers + else + let val num_slices = 50 (* FIXME *) in + schedule_of_provers provers num_slices + end + val prover_slices = prover_slices_of_schedule ctxt schedule in if mode = Auto_Try then (SH_Unknown, "") - |> fold (fn prover => + |> fold (fn (prover, slice) => fn accum as (SH_Some _, _) => accum - | _ => launch problem (get_default_slice ctxt prover) prover) - provers + | _ => launch problem slice prover) + prover_slices else (learn chained_thms; - provers - |> Par_List.map (fn prover => launch problem (get_default_slice ctxt prover) prover) + Par_List.map (fn (prover, slice) => launch problem slice prover) prover_slices |> max_outcome) end in diff -r b49329185b82 -r dc6769b86fd6 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 @@ -286,9 +286,9 @@ (TimedOut, "time limit exceeded")] @ known_szs_status_failures, prem_role = Conjecture, - good_slices = fn ctxt => + good_slices = let - val (format, enc, main_lam_trans) = + val (format, type_enc, lam_trans) = if string_ord (getenv "E_VERSION", "2.7") <> LESS then (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN) else if string_ord (getenv "E_VERSION", "2.6") <> LESS then @@ -297,12 +297,12 @@ (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN) in (* FUDGE *) - [((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))] + K [((512, meshN), (format, type_enc, lam_trans, false, e_fun_weightN)), + ((1024, meshN), (format, type_enc, lam_trans, false, e_sym_offset_weightN)), + ((91, mepoN), (format, type_enc, lam_trans, false, e_autoN)), + ((1000, 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))] end, good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} @@ -325,7 +325,11 @@ prem_role = Hypothesis, good_slices = (* FUDGE *) - K [((150, meshN), (FOF, "mono_guards??", liftingN, false, ""))], + 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, ""))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} @@ -371,7 +375,8 @@ prem_role = Hypothesis, good_slices = (* FUDGE *) - K [((512, meshN), (TH1, "mono_native_higher", keep_lamsN, false, ""))], + K [((512, meshN), (TH0, "mono_native_higher", keep_lamsN, false, "")), + ((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} @@ -394,7 +399,7 @@ prem_role = Hypothesis, good_slices = (* FUDGE *) - K [((150, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], + K [((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} @@ -477,9 +482,14 @@ prem_role = Hypothesis, good_slices = (* 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))], + 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))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} @@ -524,12 +534,12 @@ known_szs_status_failures, prem_role = Hypothesis, 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")), + 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")), - ((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")), + ((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")), ((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"))], + ((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 diff -r b49329185b82 -r dc6769b86fd6 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jan 31 16:09:23 2022 +0100 @@ -28,10 +28,6 @@ open Sledgehammer_MaSh open Sledgehammer -val cvc4N = "cvc4" -val veritN = "verit" -val z3N = "z3" - val runN = "run" val supported_proversN = "supported_provers" val refresh_tptpN = "refresh_tptp" diff -r b49329185b82 -r dc6769b86fd6 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jan 31 16:09:23 2022 +0100 @@ -869,7 +869,7 @@ val problem = {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, factss = [("", facts)], found_proof = K ()} - val slice = get_default_slice ctxt prover + val slice = hd (get_slices ctxt prover) in get_minimizing_prover ctxt MaSh (K ()) prover params problem slice end diff -r b49329185b82 -r dc6769b86fd6 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 @@ -18,7 +18,7 @@ val is_prover_supported : Proof.context -> string -> bool val is_prover_installed : Proof.context -> string -> bool val get_prover : Proof.context -> mode -> string -> prover - val get_default_slice : Proof.context -> string -> prover_slice + val get_slices : Proof.context -> string -> prover_slice list val binary_min_facts : int Config.T val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int -> @@ -59,12 +59,12 @@ else error ("No such prover: " ^ name) end -fun get_default_slice ctxt name = +fun get_slices ctxt name = let val thy = Proof_Context.theory_of ctxt in if is_atp thy name then - apsnd SOME (List.last (#good_slices (get_atp thy name ()) ctxt)) + map (apsnd SOME) (#good_slices (get_atp thy name ()) ctxt) else if is_smt_prover ctxt name then - ((SMT_Solver.default_max_relevant ctxt name, ""), NONE) + map (rpair NONE) (SMT_Solver.good_slices ctxt name) else error ("No such prover: " ^ name) end @@ -202,7 +202,7 @@ let val ctxt = Proof.context_of state val prover = get_prover ctxt Minimize prover_name - val slice = get_default_slice ctxt prover_name + val slice = hd (get_slices ctxt prover_name) val (chained, non_chained) = List.partition is_fact_chained facts fun test timeout non_chained = diff -r b49329185b82 -r dc6769b86fd6 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 = fst (fst (get_default_slice ctxt name)) + val default_max_facts = fst (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 @@ -46,7 +46,7 @@ val problem = {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, factss = [("", facts)], found_proof = K ()} - val slice = get_default_slice ctxt name + val slice = hd (get_slices ctxt name) in (case prover params problem slice of {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME