crude implementation of centralized slicing

--- 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 \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
 
+(*
+lemma "1 + 1 = 2 \<and> 0 + (x::nat) = x"
+  sledgehammer
+*)
+
+(*
+declare nat_induct[no_atp]
+declare nat_induct_non_zero[no_atp]
+
+lemma "P 0 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n"
+  sledgehammer [cvc4] (add: nat.induct)
+*)
+
+(*
+lemma "1 + 1 = 2 \<and> 0 + (x::nat) = x"
+  sledgehammer [verbose, e, dont_preplay, max_facts = 2] (add_0_left one_add_one)
+*)
+
 end

--- 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"

--- 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>\<open>False\<close>
 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

--- 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 }

--- 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

--- 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

--- 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"

--- 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

--- 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 =

--- 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