# HG changeset patch
# User desharna
# Date 1744022216 -7200
# Node ID 5a0d1075911cdf330a0a47af37cac09c16c27df3
# Parent  690a018f7370f554d35b578bf0f64a8840c6d23c
expanded Sledgehammer's schedule (loosely inspired by "Hammering without ATPs" evaluation)

diff -r 690a018f7370 -r 5a0d1075911c src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Apr 07 09:13:10 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Apr 07 12:36:56 2025 +0200
@@ -97,7 +97,7 @@
     |> the_default (SH_Unknown, "")
   end
 
-fun play_one_line_proofs minimize timeout used_facts state goal i methss =
+fun play_one_line_proofs minimize timeout used_facts state goal i methss : preplay_result list =
   (if timeout = Time.zeroTime then
      []
    else
@@ -393,6 +393,8 @@
 fun default_slice_schedule (ctxt : Proof.context) : string list =
   (* We want to subsume try0. *)
   flat (Try0.get_schedule ctxt) @
+  (* FUDGE (loosely inspired by "Hammering without ATPs" evaluation) *)
+  ["metis", "fastforce", "metis", "simp", "auto"] @
   (* FUDGE (loosely inspired by Seventeen evaluation) *)
   [cvc5N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc5N, zipperpositionN,
    cvc5N, eN, zipperpositionN, vampireN, cvc5N, cvc5N, vampireN, cvc5N, iproverN, zipperpositionN,
diff -r 690a018f7370 -r 5a0d1075911c src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Mon Apr 07 09:13:10 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Mon Apr 07 12:36:56 2025 +0200
@@ -26,14 +26,20 @@
 
 val is_tactic_prover : string -> bool = is_some o Try0.get_proof_method
 
-val meshN = "mesh"
+local
+
+val slices_of_max_facts = map (fn max_facts => (1, false, false, max_facts, "mesh"))
+
+in
 
-fun good_slices_of_tactic_prover _ =
-  (* FUDGE *)
-  [(1, false, false, 0, meshN),
-   (1, false, false, 2, meshN),
-   (1, false, false, 8, meshN),
-   (1, false, false, 32, meshN)]
+(* FUDGE *)
+fun good_slices_of_tactic_prover "metis" = slices_of_max_facts [0, 64, 32, 8, 16, 4, 2, 1]
+  | good_slices_of_tactic_prover "fastforce" = slices_of_max_facts [0, 16, 32, 8, 4, 64, 2, 1]
+  | good_slices_of_tactic_prover "simp" = slices_of_max_facts [0, 16, 32, 8, 64, 4, 1, 2]
+  | good_slices_of_tactic_prover "auto" = slices_of_max_facts [0, 16, 32, 8, 4, 64, 2, 1]
+  | good_slices_of_tactic_prover _ = slices_of_max_facts [0, 2, 8, 16, 32, 64]
+
+end
 
 fun meth_of "algebra" = Algebra_Method
   | meth_of "argo" = Argo_Method