# HG changeset patch
# User blanchet
# Date 1643641763 -3600
# Node ID fdda7e754f4590ff2a0fd935d21f04520f2af102
# Parent  e9e27d2e61a1868ae754e4c5a8e2341f8aabacd6
changed logic of 'slice' option to 'slices'

diff -r e9e27d2e61a1 -r fdda7e754f45 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
@@ -72,14 +72,14 @@
    ("try0", "true"),
    ("smt_proofs", "true"),
    ("minimize", "true"),
-   ("slice", "5"),
+   ("slices", string_of_int (6 * Multithreading.max_threads ())),
    ("preplay_timeout", "1")]
 
 val alias_params =
   [("prover", ("provers", [])), (* undocumented *)
    ("dont_preplay", ("preplay_timeout", ["0"])),
    ("dont_compress", ("compress", ["1"])),
-   ("dont_slice", ("slice", ["0"])),
+   ("dont_slice", ("slices", ["1"])),
    ("isar_proof", ("isar_proofs", [])) (* legacy *)]
 val negated_alias_params =
   [("no_debug", "debug"),
@@ -268,7 +268,7 @@
     val try0 = lookup_bool "try0"
     val smt_proofs = lookup_bool "smt_proofs"
     val minimize = lookup_bool "minimize"
-    val slice = if mode = Auto_Try then Time.zeroTime else lookup_time "slice"
+    val slices = if mode = Auto_Try then 1 else Int.max (1, lookup_int "slices")
     val timeout = lookup_time "timeout"
     val preplay_timeout = lookup_time "preplay_timeout"
     val expect = lookup_string "expect"
@@ -279,7 +279,7 @@
      induction_rules = induction_rules, max_facts = max_facts, fact_thresholds = fact_thresholds,
      max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
      isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
-     minimize = minimize, slice = slice, timeout = timeout, preplay_timeout = preplay_timeout,
+     minimize = minimize, slices = slices, timeout = timeout, preplay_timeout = preplay_timeout,
      expect = expect}
   end
 
diff -r e9e27d2e61a1 -r fdda7e754f45 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
@@ -43,13 +43,14 @@
      try0 : bool,
      smt_proofs : bool,
      minimize : bool,
-     slice : Time.time,
+     slices : int,
      timeout : Time.time,
      preplay_timeout : Time.time,
      expect : string}
 
   val string_of_params : params -> string
   val set_params_provers : params -> string list -> params
+  val slice_timeout : int -> Time.time -> Time.time
 
   type prover_problem =
     {comment : string,
@@ -140,7 +141,7 @@
    try0 : bool,
    smt_proofs : bool,
    minimize : bool,
-   slice : Time.time,
+   slices : int,
    timeout : Time.time,
    preplay_timeout : Time.time,
    expect : string}
@@ -174,11 +175,15 @@
    try0 = #try0 params,
    smt_proofs = #smt_proofs params,
    minimize = #minimize params,
-   slice = #slice params,
+   slices = #slices params,
    timeout = #timeout params,
    preplay_timeout = #preplay_timeout params,
    expect = #expect params}
 
+fun slice_timeout slices timeout =
+  Time.toReal timeout * Real.fromInt (Multithreading.max_threads ()) / Real.fromInt slices
+  |> seconds
+
 type prover_problem =
   {comment : string,
    state : Proof.state,
diff -r e9e27d2e61a1 -r fdda7e754f45 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
@@ -95,7 +95,7 @@
        fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
        max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
        compress = compress, try0 = try0, smt_proofs = smt_proofs, minimize = minimize,
-       slice = Time.zeroTime, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
+       slices = 1, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
     val problem =
       {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
        facts = ("", facts), found_proof = K ()}
diff -r e9e27d2e61a1 -r fdda7e754f45 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
@@ -64,9 +64,9 @@
   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, slice, timeout, ...} : params) state goal i facts =
+    type_enc, slices, timeout, ...} : params) state goal i facts =
   let
-    val run_timeout = if slice = Time.zeroTime then timeout else slice
+    val run_timeout = slice_timeout slices timeout
     val (higher_order, nat_as_int) =
       (case type_enc of
         SOME s =>  (String.isSubstring "native_higher" s, String.isSubstring "arith" s)