more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Feb 02 13:34:52 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Feb 02 13:43:48 2022 +0100
@@ -297,7 +297,7 @@
@ round_robin (num_slices - num_default_slices) (unknown_provers @ known_provers)
end
-fun prover_slices_of_schedule ctxt
+fun prover_slices_of_schedule ctxt factss
({max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases, ...} : params) schedule =
let
fun triplicate_slices original =
@@ -319,11 +319,13 @@
the_default uncurried_aliases0 uncurried_aliases, extra_extra0)
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)
+ let
+ 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
+ ((num_facts, fact_filter), Option.map adjust_extra extra)
+ end
val provers = distinct (op =) schedule
val prover_slices =
@@ -416,16 +418,17 @@
fun launch_provers () =
let
+ val factss = get_factss provers
val problem =
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
- factss = get_factss provers, found_proof = found_proof}
+ factss = factss, found_proof = found_proof}
val learn = mash_learn_proof ctxt params (Thm.prop_of goal)
val launch = launch_prover_and_preplay params mode writeln_result learn
val schedule =
if mode = Auto_Try then provers
else schedule_of_provers provers slices
- val prover_slices = prover_slices_of_schedule ctxt params schedule
+ val prover_slices = prover_slices_of_schedule ctxt factss params schedule
val _ =
if verbose then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Feb 02 13:34:52 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Feb 02 13:43:48 2022 +0100
@@ -82,7 +82,7 @@
val is_atp : string -> bool
val bunches_of_proof_methods : Proof.context -> bool -> bool -> bool -> string ->
proof_method list list
- val get_facts_of_filter : string -> (string * fact list) list -> fact list
+ val facts_of_filter : string -> (string * fact list) list -> fact list
val is_fact_chained : (('a * stature) * 'b) -> bool
val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
((''a * stature) * 'b) list
@@ -225,7 +225,7 @@
try0_methodss @ [metis_methods] @ smt_methodss
end
-fun get_facts_of_filter fact_filter factss =
+fun facts_of_filter fact_filter factss =
(case AList.lookup (op =) factss fact_filter of
SOME facts => facts
| NONE => snd (hd factss))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Feb 02 13:34:52 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Feb 02 13:43:48 2022 +0100
@@ -183,7 +183,7 @@
end
val effective_fact_filter = fact_filter |> the_default good_fact_filter
- val facts = get_facts_of_filter effective_fact_filter factss
+ val facts = facts_of_filter effective_fact_filter factss
val num_facts =
(case max_facts of
NONE => good_max_facts
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Wed Feb 02 13:34:52 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Wed Feb 02 13:43:48 2022 +0100
@@ -124,7 +124,7 @@
val ((best_max_facts, best_fact_filter), _) = slice
val effective_fact_filter = fact_filter |> the_default best_fact_filter
- val facts = take best_max_facts (get_facts_of_filter effective_fact_filter factss)
+ val facts = take best_max_facts (facts_of_filter effective_fact_filter factss)
val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
smt_filter name params state goal subgoal facts