second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size

--- a/src/HOL/Sledgehammer.thy	Fri Mar 25 13:52:23 2022 +0100
+++ b/src/HOL/Sledgehammer.thy	Fri Mar 25 13:52:23 2022 +0100
@@ -35,4 +35,7 @@
 ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
 
+lemma "2 + 2 = 5"
+  sledgehammer[verbose, mepo, overlord]
+
 end

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Mar 25 13:52:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Mar 25 13:52:23 2022 +0100
@@ -136,7 +136,7 @@
 
 fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn
     (problem as {state, subgoal, factss, ...} : prover_problem)
-    (slice as ((_, num_facts, fact_filter), _)) name =
+    (slice as ((slice_size, num_facts, fact_filter), _)) name =
   let
     val ctxt = Proof.context_of state
 
@@ -145,7 +145,8 @@
     val _ =
       if verbose then
         writeln (name ^ " with " ^ string_of_int num_facts ^ " " ^ fact_filter ^ " fact" ^
-          plural_s num_facts ^ " for " ^ string_of_time (slice_timeout slices timeout)  ^ "...")
+          plural_s num_facts ^ " for " ^ string_of_time (slice_timeout slice_size slices timeout) ^
+          "...")
       else
         ()
 
@@ -274,7 +275,7 @@
 
 val default_slice_schedule =
   (* FUDGE (inspired by Seventeen evaluation) *)
-  [cvc4N, zipperpositionN, vampireN, eN, veritN, cvc4N, zipperpositionN, cvc4N, vampireN, cvc4N,
+  [cvc4N, zipperpositionN, vampireN, veritN, eN, cvc4N, zipperpositionN, cvc4N, vampireN, cvc4N,
    cvc4N, vampireN, cvc4N, iproverN, zipperpositionN, vampireN, vampireN, zipperpositionN, z3N,
    cvc4N, vampireN, iproverN, vampireN, zipperpositionN, z3N, z3N, cvc4N, cvc4N]
 
@@ -321,33 +322,41 @@
           the_default uncurried_aliases0 uncurried_aliases, extra_extra0)
       | adjust_extra (extra as SMT_Slice _) = extra
 
-    fun adjust_slice ((slice_size0, num_facts0, fact_filter0), extra) =
+    fun adjust_slice max_slice_size ((slice_size0, num_facts0, fact_filter0), extra) =
       let
+        val slice_size = Int.min (max_slice_size, slice_size0)
         val fact_filter = fact_filter |> the_default fact_filter0
         val max_facts = max_facts |> the_default num_facts0
         val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss))
       in
-        ((slice_size0, num_facts, fact_filter), adjust_extra extra)
+        ((slice_size, num_facts, fact_filter), adjust_extra extra)
       end
 
     val provers = distinct (op =) schedule
     val prover_slices =
       map (fn prover => (prover,
-          (is_none fact_filter ? triplicate_slices)
-            (map adjust_slice (get_slices ctxt prover))))
+          (is_none fact_filter ? triplicate_slices) (get_slices ctxt prover)))
         provers
 
-    fun translate _ [] = []
-      | translate prover_slices (prover :: schedule) =
+    val max_threads = Multithreading.max_threads ()
+
+    fun translate_schedule _ 0 _ = []
+      | translate_schedule _ _ [] = []
+      | translate_schedule prover_slices slices_left (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
+          SOME (slice0 :: slices) =>
+          let
+            val prover_slices' = AList.update (op =) (prover, slices) prover_slices
+            val slice as ((slice_size, _, _), _) =
+              adjust_slice ((slices_left + max_threads - 1) div max_threads) slice0
+          in
+            (prover, slice) :: translate_schedule prover_slices' (slices_left - slice_size) schedule
           end
-        | _ => translate prover_slices schedule)
+        | _ => translate_schedule prover_slices slices_left schedule)
   in
-    translate prover_slices schedule
+    translate_schedule prover_slices (length schedule) schedule
     |> distinct (op =)
+    |> @{print} (*###*)
   end
 
 fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, max_proofs,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Mar 25 13:52:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Mar 25 13:52:23 2022 +0100
@@ -80,8 +80,8 @@
 (* desired slice size, desired number of facts, fact filter *)
 type base_slice = int * int * string
 
-(* problem file format, type encoding, lambda translation scheme, uncurried aliases?, extra
-   arguments to prover *)
+(* problem file format, type encoding, lambda translation scheme, uncurried aliases?,
+   prover-specific extra information *)
 type atp_slice = atp_format * string * string * bool * string
 
 type atp_config =
@@ -287,12 +287,12 @@
            (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN)
      in
        (* FUDGE *)
-       K [((1, 512, meshN), (format, type_enc, lam_trans, false, e_fun_weightN)),
-        ((1, 1024, meshN), (format, type_enc, lam_trans, false, e_sym_offset_weightN)),
-        ((1, 128, mepoN), (format, type_enc, lam_trans, false, e_autoscheduleN)),
-        ((1, 724, meshN), (format, "poly_guards??", lam_trans, false, e_sym_offset_weightN)),
-        ((1, 256, mepoN), (format, type_enc, liftingN, false, e_fun_weightN)),
-        ((1, 64, mashN), (format, type_enc, combsN, false, e_fun_weightN))]
+       K [((1000 (* infinity *), 1024, meshN), (format, type_enc, lam_trans, false, e_autoscheduleN)),
+         ((1, 512, meshN), (format, type_enc, lam_trans, false, e_sym_offset_weightN)),
+         ((1, 128, mepoN), (format, type_enc, lam_trans, false, e_fun_weightN)),
+         ((1, 724, meshN), (format, "poly_guards??", lam_trans, false, e_sym_offset_weightN)),
+         ((1, 256, mepoN), (format, type_enc, liftingN, false, e_fun_weightN)),
+         ((1, 64, mashN), (format, type_enc, combsN, false, e_fun_weightN))]
      end,
    good_max_mono_iters = default_max_mono_iters,
    good_max_new_mono_instances = default_max_new_mono_instances}

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Mar 25 13:52:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Mar 25 13:52:23 2022 +0100
@@ -52,7 +52,7 @@
      expect : string}
 
   val string_of_params : params -> string
-  val slice_timeout : int -> Time.time -> Time.time
+  val slice_timeout : int -> int -> Time.time -> Time.time
 
   type prover_problem =
     {comment : string,
@@ -164,12 +164,12 @@
     induction_rules = Exclude ?
       filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false)
 
-fun slice_timeout slices timeout =
+fun slice_timeout slice_size slices timeout =
   let
     val max_threads = Multithreading.max_threads ()
     val batches = (slices + max_threads - 1) div max_threads
   in
-    seconds (Time.toReal timeout / Real.fromInt batches)
+    seconds (Real.fromInt slice_size * Time.toReal timeout / Real.fromInt batches)
   end
 
 type prover_problem =
@@ -239,7 +239,7 @@
     SOME facts => facts
   | NONE => snd (hd factss))
 
-fun facts_of_basic_slice (desired_slices, num_facts, fact_filter) factss =
+fun facts_of_basic_slice (_, num_facts, fact_filter) factss =
   facts_of_filter fact_filter factss
   |> take num_facts
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Mar 25 13:52:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Mar 25 13:52:23 2022 +0100
@@ -107,8 +107,8 @@
     ({comment, state, goal, subgoal, subgoal_count, factss, found_proof} : prover_problem)
     slice =
   let
-    val (basic_slice, ATP_Slice (good_format, good_type_enc, good_lam_trans,
-        good_uncurried_aliases, extra)) =
+    val (basic_slice as (slice_size, _, _),
+        ATP_Slice (good_format, good_type_enc, good_lam_trans, good_uncurried_aliases, extra)) =
       slice
     val facts = facts_of_basic_slice basic_slice factss
     val thy = Proof.theory_of state
@@ -184,7 +184,7 @@
 
         val strictness = if strict then Strict else Non_Strict
         val type_enc = choose_type_enc strictness good_format good_type_enc
-        val run_timeout = slice_timeout slices timeout
+        val run_timeout = slice_timeout slice_size 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

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Mar 25 13:52:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Mar 25 13:52:23 2022 +0100
@@ -69,10 +69,10 @@
 val is_boring_builtin_typ =
   not o exists_subtype (member (op =) [\<^typ>\<open>nat\<close>, \<^typ>\<open>int\<close>, HOLogic.realT])
 
-fun smt_filter name ({debug, overlord, max_mono_iters, max_new_mono_instances,
-    type_enc, slices, timeout, ...} : params) state goal i facts options =
+fun smt_filter name ({debug, overlord, max_mono_iters, max_new_mono_instances, type_enc, slices,
+    timeout, ...} : params) state goal i slice_size facts options =
   let
-    val run_timeout = slice_timeout slices timeout
+    val run_timeout = slice_timeout slice_size slices timeout
     val (higher_order, nat_as_int) =
       (case type_enc of
         SOME s => (SOME (String.isSubstring "native_higher" s), SOME (String.isSubstring "arith" s))
@@ -123,12 +123,12 @@
     ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem)
     slice =
   let
-    val (basic_slice, SMT_Slice options) = slice
+    val (basic_slice as (slice_size, _, _), SMT_Slice options) = slice
     val facts = facts_of_basic_slice basic_slice factss
     val ctxt = Proof.context_of state
 
     val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
-      smt_filter name params state goal subgoal facts options
+      smt_filter name params state goal subgoal slice_size facts options
     val used_facts =
       (case fact_ids of
         NONE => map fst used_from