--- 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
@@ -136,13 +136,12 @@
|> (fn (used_facts, (meth, play)) =>
(used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play)))
-fun launch_prover (params as {verbose, spy, max_facts, induction_rules, ...}) mode only learn
+fun launch_prover (params as {verbose, spy, ...}) mode learn
(problem as {state, subgoal, factss, ...} : prover_problem) slice name =
let
val ctxt = Proof.context_of state
val _ = spying spy (fn () => (state, subgoal, name, "Launched"))
- val induction_rules = the_default Exclude induction_rules
fun print_used_facts used_facts used_from =
tag_list 1 used_from
@@ -212,9 +211,8 @@
let
val outcome_code = short_string_of_sledgehammer_outcome outcome
in
- (* The "expect" argument is deliberately ignored if the prover is
- missing so that the "Metis_Examples" can be processed on any
- machine. *)
+ (* The "expect" argument is deliberately ignored if the prover is missing so that
+ "Metis_Examples" can be processed on any machine. *)
if expect = "" orelse outcome_code = expect orelse
not (is_prover_installed ctxt prover_name) then
()
@@ -222,14 +220,14 @@
error ("Unexpected outcome: " ^ quote outcome_code)
end
-fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode writeln_result only
- learn (problem as {state, subgoal, ...}) slice prover_name =
+fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode writeln_result learn
+ (problem as {state, subgoal, ...}) slice prover_name =
let
val ctxt = Proof.context_of state
val hard_timeout = Time.scale 5.0 timeout
fun really_go () =
- launch_prover params mode only learn problem slice prover_name
+ launch_prover params mode learn problem slice prover_name
|> preplay_prover_result params state subgoal
fun go () =
@@ -256,8 +254,6 @@
(outcome, message)
end
-val auto_try_max_facts_divisor = 2 (* FUDGE *)
-
fun string_of_facts facts =
"Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ": " ^
(facts |> map (fst o fst) |> space_implode " ")
@@ -313,12 +309,16 @@
(case max_facts of
SOME n => n
| NONE =>
- 0 |> fold (fn prover => Integer.max (fst (fst (get_default_slice ctxt prover))))
- provers
- |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor))
+ fold (fn prover => Integer.max (fst (fst (get_default_slice ctxt prover)))) provers
+ 0)
+
val ({elapsed, ...}, factss) = Timing.timing
(relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t)
all_facts
+
+ val induction_rules = the_default (if only then Include else Exclude) induction_rules
+ val factss = map (apsnd (maybe_filter_out_induction_rules induction_rules)) factss
+
val () = spying spy (fn () => (state, i, "All",
"Filtering facts in " ^ string_of_int (Time.toMilliseconds elapsed) ^
" ms (MaSh algorithm: " ^ str_of_mash_algorithm (the_mash_algorithm ()) ^ ")"));
@@ -335,7 +335,7 @@
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
factss = get_factss provers, 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 only learn
+ val launch = launch_prover_and_preplay params mode writeln_result learn
in
if mode = Auto_Try then
(SH_Unknown, "")