--- 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
@@ -36,9 +36,6 @@
ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
(*
-lemma "1 + 1 = 3"
- sledgehammer[verbose]
-
lemma "1 + 1 = 2"
sledgehammer [slices = 40, max_proofs = 40]
--- 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
@@ -259,16 +259,15 @@
(outcome, message)
end
-fun string_of_facts facts =
- "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ": " ^
- (facts |> map (fst o fst) |> space_implode " ")
+fun string_of_facts filter facts =
+ "Selected " ^ string_of_int (length facts) ^ " " ^ (if filter = "" then "" else filter ^ " ") ^
+ "fact" ^ plural_s (length facts) ^ ": " ^ (space_implode " " (map (fst o fst) facts))
fun string_of_factss factss =
if forall (null o snd) factss then
"Found no relevant facts"
else
- cat_lines (map (fn (filter, facts) =>
- (if filter = "" then "" else filter ^ ": ") ^ string_of_facts facts) factss)
+ cat_lines (map (fn (filter, facts) => string_of_facts filter facts) factss)
val default_slice_schedule =
(* FUDGE (based on Seventeen evaluation) *)
@@ -278,10 +277,12 @@
fun schedule_of_provers provers num_slices =
let
- val num_default_slices = length default_slice_schedule
val (known_provers, unknown_provers) =
List.partition (member (op =) default_slice_schedule) provers
+ val default_slice_schedule = filter (member (op =) known_provers) default_slice_schedule
+ val num_default_slices = length default_slice_schedule
+
fun round_robin _ [] = []
| round_robin 0 _ = []
| round_robin n (prover :: provers) = prover :: round_robin (n - 1) (provers @ [prover])
@@ -293,7 +294,7 @@
@ round_robin (num_slices - num_default_slices) (unknown_provers @ known_provers)
end
-fun prover_slices_of_schedule ctxt schedule =
+fun prover_slices_of_schedule ctxt ({max_facts, fact_filter, ...} : params) schedule =
let
fun triplicate_slices original =
let
@@ -309,9 +310,21 @@
original @ shifted_once @ shifted_twice
end
+ fun adjust_extra XXX = XXX (* ### FIXME *)
+
+ fun adjust_slice ((num_facts0, fact_filter0), extra) =
+ ((case max_facts of
+ NONE => num_facts0
+ | SOME max_facts => Int.min (num_facts0, max_facts),
+ the_default fact_filter0 fact_filter),
+ Option.map adjust_extra extra)
+
val provers = distinct (op =) schedule
val prover_slices =
- map (fn prover => (prover, triplicate_slices (get_slices ctxt prover))) provers
+ map (fn prover => (prover,
+ (is_none fact_filter ? triplicate_slices)
+ (map adjust_slice (get_slices ctxt prover))))
+ provers
fun translate _ [] = []
| translate prover_slices (prover :: schedule) =
@@ -323,6 +336,7 @@
| _ => translate prover_slices schedule)
in
translate prover_slices schedule
+ |> distinct (op =)
end
fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, max_proofs,
@@ -375,6 +389,7 @@
fold (fn prover =>
fold (fn ((n, _), _) => Integer.max n) (get_slices ctxt prover))
provers 0)
+ * 51 div 50 (* some slack to account for filtering of induction facts below *)
val ({elapsed, ...}, factss) = Timing.timing
(relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t)
@@ -406,7 +421,7 @@
provers
else
schedule_of_provers provers slices
- val prover_slices = prover_slices_of_schedule ctxt schedule
+ val prover_slices = prover_slices_of_schedule ctxt params schedule
in
if mode = Auto_Try then
(SH_Unknown, "")
--- 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
@@ -299,8 +299,8 @@
(* FUDGE *)
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)),
+ ((128, mepoN), (format, type_enc, lam_trans, false, e_autoN)),
+ ((724, 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,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Jan 31 16:09:23 2022 +0100
@@ -183,7 +183,7 @@
fun try_command_line banner play command =
let val s = string_of_play_outcome play in
- banner ^ ": " ^ Active.sendback_markup_command command ^
+ banner ^ Active.sendback_markup_command command ^
(s |> s <> "" ? enclose " (" ")")
end
--- 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
@@ -160,8 +160,12 @@
filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false)
fun slice_timeout slices timeout =
- Time.toReal timeout * Real.fromInt (Multithreading.max_threads ()) / Real.fromInt slices
- |> seconds
+ let
+ val max_threads = Multithreading.max_threads ()
+ val batches = (slices + max_threads - 1) div max_threads
+ in
+ seconds (Time.toReal timeout / Real.fromInt batches)
+ end
type prover_problem =
{comment : string,
@@ -188,9 +192,9 @@
fun proof_banner mode prover_name =
(case mode of
- Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof"
- | Try => "Sledgehammer (" ^ prover_name ^ ") found a proof"
- | _ => "Try this")
+ Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof: "
+ | Try => "Sledgehammer (" ^ prover_name ^ ") found a proof: "
+ | _ => "")
fun bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types desperate_lam_trans =
let