# HG changeset patch
# User desharna
# Date 1744009990 -7200
# Node ID 690a018f7370f554d35b578bf0f64a8840c6d23c
# Parent  eaf0b4673ab2bab1a772d800d29d5e78edfa61c8
added try0's schedule to sledgehammer's schedule

diff -r eaf0b4673ab2 -r 690a018f7370 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Apr 07 08:39:10 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Apr 07 09:13:10 2025 +0200
@@ -388,7 +388,11 @@
   else
     cat_lines (map (fn (filter, facts) => string_of_facts filter facts) factss)
 
-val default_slice_schedule =
+local
+
+fun default_slice_schedule (ctxt : Proof.context) : string list =
+  (* We want to subsume try0. *)
+  flat (Try0.get_schedule ctxt) @
   (* 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,
@@ -396,25 +400,30 @@
    iproverN, spassN, zipperpositionN, vampireN, cvc5N, zipperpositionN, z3N, z3N, cvc5N,
    zipperpositionN]
 
-fun schedule_of_provers provers num_slices =
+in
+
+fun schedule_of_provers (ctxt : Proof.context) (provers : string list) num_slices =
   let
+    val default_schedule = default_slice_schedule ctxt
     val (known_provers, unknown_provers) =
-      List.partition (member (op =) default_slice_schedule) provers
+      List.partition (member (op =) default_schedule) provers
 
-    val default_slice_schedule = filter (member (op =) known_provers) default_slice_schedule
-    val num_default_slices = length default_slice_schedule
+    val default_schedule = filter (member (op =) known_provers) default_schedule
+    val num_default_slices = length default_schedule
 
     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
+      take num_slices default_schedule
     else
-      default_slice_schedule
+      default_schedule
       @ round_robin (num_slices - num_default_slices) (unknown_provers @ known_provers)
   end
 
+end
+
 fun prover_slices_of_schedule ctxt goal subgoal factss
     ({abduce, falsify, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases,
       ...} : params)
@@ -641,7 +650,7 @@
 
             val schedule =
               if mode = Auto_Try then provers
-              else schedule_of_provers provers slices
+              else schedule_of_provers ctxt provers slices
             val prover_slices = prover_slices_of_schedule ctxt goal i factss params schedule
 
             val _ =
diff -r eaf0b4673ab2 -r 690a018f7370 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Apr 07 08:39:10 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Apr 07 09:13:10 2025 +0200
@@ -170,9 +170,13 @@
 
 (* The first ATP of the list is used by Auto Sledgehammer. *)
 fun default_provers_param_value ctxt =
-  \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
-  filter (is_prover_installed ctxt) (smt_solvers ctxt @ local_atps)
-  |> implode_param
+  let
+    val try0_provers = Try0.get_all_proof_method_names ()
+    \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
+    val installed_provers = filter (is_prover_installed ctxt) (smt_solvers ctxt @ local_atps)
+  in
+    implode_param (installed_provers @ try0_provers)
+  end
 
 fun set_default_raw_param param thy =
   let val ctxt = Proof_Context.init_global thy in