--- 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
@@ -137,31 +137,20 @@
(used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play)))
fun launch_prover (params as {verbose, spy, max_facts, induction_rules, ...}) mode only learn
- ({comment, state, goal, subgoal, subgoal_count, facts, found_proof} : prover_problem) name =
+ (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 max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
- val num_facts = length (snd facts) |> not only ? Integer.min max_facts
val induction_rules = the_default Exclude induction_rules
- val problem =
- {comment = comment, state = state, goal = goal, subgoal = subgoal,
- subgoal_count = subgoal_count,
- facts = facts
- (* We take "num_facts" because "facts" contains the maximum of all called provers. *)
- |> apsnd (take num_facts o maybe_filter_out_induction_rules induction_rules),
- found_proof = found_proof}
-
fun print_used_facts used_facts used_from =
tag_list 1 used_from
|> map (fn (j, fact) => fact |> apsnd (K j))
|> filter_used_facts false used_facts
|> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
|> commas
- |> prefix ("Fact" ^ plural_s num_facts ^ " in " ^ name ^
- " proof (of " ^ string_of_int num_facts ^ "): ")
+ |> prefix ("Facts in " ^ name ^ " proof: ")
|> writeln
fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
@@ -185,19 +174,18 @@
end
val filter_infos =
- map filter_info [("actual", used_from), facts]
+ map filter_info (("actual", used_from) :: factss)
|> AList.group (op =)
|> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices)
in
- "Success: Found proof with " ^ string_of_int num_used_facts ^ " of " ^
- string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
+ "Success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^
+ plural_s num_used_facts ^
(if num_used_facts = 0 then "" else ": " ^ commas filter_infos)
end
| spying_str_of_res {outcome = SOME failure, ...} =
"Failure: " ^ string_of_atp_failure failure
in
- problem
- |> get_minimizing_prover ctxt mode learn name params
+ get_minimizing_prover ctxt mode learn name params problem slice
|> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
print_used_facts used_facts used_from
| _ => ())
@@ -235,13 +223,13 @@
end
fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode writeln_result only
- learn (problem as {state, subgoal, ...}) prover_name =
+ 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 prover_name
+ launch_prover params mode only learn problem slice prover_name
|> preplay_prover_result params state subgoal
fun go () =
@@ -342,23 +330,22 @@
fun launch_provers () =
let
- val facts = hd (get_factss provers) (* temporary *)
val problem =
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
- facts = facts, found_proof = found_proof}
+ 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
in
if mode = Auto_Try then
(SH_Unknown, "")
|> fold (fn prover =>
- fn accum as (SH_Some _, _) => accum
- | _ => launch problem prover)
+ fn accum as (SH_Some _, _) => accum
+ | _ => launch problem (get_default_slice ctxt prover) prover)
provers
else
(learn chained_thms;
provers
- |> Par_List.map (launch problem)
+ |> Par_List.map (fn prover => launch problem (get_default_slice ctxt prover) prover)
|> max_outcome)
end
in
--- 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
@@ -12,7 +12,7 @@
type atp_formula_role = ATP_Problem.atp_formula_role
type atp_failure = ATP_Proof.atp_failure
- type atp_slice_spec = (int * string) * atp_format * string * string * bool * string
+ type atp_slice = (int * string) * atp_format * string * string * bool * string
type atp_config =
{exec : string list * string list,
arguments : Proof.context -> bool -> string -> Time.time -> Path.T ->
@@ -20,7 +20,7 @@
proof_delims : (string * string) list,
known_failures : (atp_failure * string) list,
prem_role : atp_formula_role,
- best_slices : Proof.context -> atp_slice_spec list,
+ best_slices : Proof.context -> atp_slice list,
best_max_mono_iters : int,
best_max_new_mono_instances : int}
@@ -46,7 +46,7 @@
val spass_H2SOS : string
val isabelle_scala_function: string list * string list
val remote_atp : string -> string -> string list -> (string * string) list ->
- (atp_failure * string) list -> atp_formula_role -> (Proof.context -> atp_slice_spec) ->
+ (atp_failure * string) list -> atp_formula_role -> (Proof.context -> atp_slice) ->
string * (unit -> atp_config)
val add_atp : string * (unit -> atp_config) -> theory -> theory
val get_atp : theory -> string -> (unit -> atp_config)
@@ -76,7 +76,7 @@
val default_max_mono_iters = 3 (* FUDGE *)
val default_max_new_mono_instances = 100 (* FUDGE *)
-type atp_slice_spec = (int * string) * atp_format * string * string * bool * string
+type atp_slice = (int * string) * atp_format * string * string * bool * string
type atp_config =
{exec : string list * string list,
@@ -85,7 +85,7 @@
proof_delims : (string * string) list,
known_failures : (atp_failure * string) list,
prem_role : atp_formula_role,
- best_slices : Proof.context -> atp_slice_spec list,
+ best_slices : Proof.context -> atp_slice list,
best_max_mono_iters : int,
best_max_new_mono_instances : int}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jan 31 16:09:23 2022 +0100
@@ -868,9 +868,10 @@
let
val problem =
{comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1,
- subgoal_count = 1, facts = ("", facts), found_proof = K ()}
+ subgoal_count = 1, factss = [("", facts)], found_proof = K ()}
+ val slice = get_default_slice ctxt prover
in
- get_minimizing_prover ctxt MaSh (K ()) prover params problem
+ get_minimizing_prover ctxt MaSh (K ()) prover params problem slice
end
val bad_types = [\<^type_name>\<open>prop\<close>, \<^type_name>\<open>bool\<close>, \<^type_name>\<open>fun\<close>]
--- 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
@@ -14,6 +14,7 @@
type fact = Sledgehammer_Fact.fact
type proof_method = Sledgehammer_Proof_Methods.proof_method
type play_outcome = Sledgehammer_Proof_Methods.play_outcome
+ type atp_slice = Sledgehammer_ATP_Systems.atp_slice
datatype mode = Auto_Try | Try | Normal | Minimize | MaSh
@@ -58,9 +59,13 @@
goal : thm,
subgoal : int,
subgoal_count : int,
- facts : string * fact list,
+ factss : (string * fact list) list,
found_proof : string -> unit}
+ datatype prover_slice =
+ ATP_Slice of atp_slice
+ | SMT_Slice of int * string
+
type prover_result =
{outcome : atp_failure option,
used_facts : (string * stature) list,
@@ -69,7 +74,7 @@
run_time : Time.time,
message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
- type prover = params -> prover_problem -> prover_result
+ type prover = params -> prover_problem -> prover_slice -> prover_result
val SledgehammerN : string
val str_of_mode : mode -> string
@@ -78,6 +83,7 @@
val is_atp : theory -> 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 is_fact_chained : (('a * stature) * 'b) -> bool
val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
((''a * stature) * 'b) list
@@ -190,9 +196,13 @@
goal : thm,
subgoal : int,
subgoal_count : int,
- facts : string * fact list,
+ factss : (string * fact list) list,
found_proof : string -> unit}
+datatype prover_slice =
+ ATP_Slice of atp_slice
+| SMT_Slice of int * string
+
type prover_result =
{outcome : atp_failure option,
used_facts : (string * stature) list,
@@ -201,7 +211,7 @@
run_time : Time.time,
message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
-type prover = params -> prover_problem -> prover_result
+type prover = params -> prover_problem -> prover_slice -> prover_result
fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
@@ -240,6 +250,11 @@
try0_methodss @ [metis_methods] @ smt_methodss
end
+fun get_facts_of_filter fact_filter factss =
+ (case AList.lookup (op =) factss fact_filter of
+ SOME facts => facts
+ | NONE => snd (hd factss))
+
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
fun filter_used_facts keep_chained used =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jan 31 16:09:23 2022 +0100
@@ -103,15 +103,19 @@
val atp_important_message_keep_quotient = 25
fun run_atp mode name
- ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, max_facts,
- max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize,
- slices, timeout, preplay_timeout, spy, ...} : params)
- ({comment, state, goal, subgoal, subgoal_count, facts, found_proof} : prover_problem) =
+ ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter,
+ max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs,
+ minimize, slices, timeout, preplay_timeout, spy, ...} : params)
+ ({comment, state, goal, subgoal, subgoal_count, factss, found_proof} : prover_problem)
+ slice =
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
- val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
+ val ATP_Slice ((best_max_facts, best_fact_filter), format, best_type_enc, best_lam_trans,
+ best_uncurried_aliases, extra) = slice
+
+ val {exec, arguments, proof_delims, known_failures, prem_role, best_max_mono_iters,
best_max_new_mono_instances, ...} = get_atp thy name ()
val full_proofs = isar_proofs |> the_default (mode = Minimize)
@@ -158,10 +162,6 @@
fun run () =
let
- val ((best_max_facts, _), format, best_type_enc, best_lam_trans, best_uncurried_aliases,
- extra) =
- List.last (best_slices ctxt)
-
fun monomorphize_facts facts =
let
val ctxt =
@@ -183,7 +183,8 @@
|> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths)
end
- val facts = snd facts
+ val effective_fact_filter = fact_filter |> the_default best_fact_filter
+ val facts = get_facts_of_filter effective_fact_filter factss
val num_facts =
(case max_facts of
NONE => best_max_facts
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Jan 31 16:09:23 2022 +0100
@@ -13,11 +13,13 @@
type mode = Sledgehammer_Prover.mode
type params = Sledgehammer_Prover.params
type prover = Sledgehammer_Prover.prover
+ type prover_slice = Sledgehammer_Prover.prover_slice
val is_prover_supported : Proof.context -> string -> bool
val is_prover_installed : Proof.context -> string -> bool
val default_max_facts_of_prover : Proof.context -> string -> int
val get_prover : Proof.context -> mode -> string -> prover
+ val get_default_slice : Proof.context -> string -> prover_slice
val binary_min_facts : int Config.T
val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
@@ -68,6 +70,16 @@
else error ("No such prover: " ^ name)
end
+fun get_default_slice ctxt name =
+ let val thy = Proof_Context.theory_of ctxt in
+ if is_atp thy name then
+ ATP_Slice (List.last (#best_slices (get_atp thy name ()) ctxt))
+ else if is_smt_prover ctxt name then
+ SMT_Slice (SMT_Solver.default_max_relevant ctxt name, "")
+ else
+ error ("No such prover: " ^ name)
+ end
+
(* wrapper for calling external prover *)
fun n_facts names =
@@ -81,7 +93,7 @@
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
minimize, preplay_timeout, induction_rules, ...} : params)
- silent (prover : prover) timeout i n state goal facts =
+ slice silent (prover : prover) timeout i n state goal facts =
let
val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
(if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
@@ -98,10 +110,10 @@
slices = 1, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
val problem =
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
- facts = ("", facts), found_proof = K ()}
+ factss = [("", facts)], found_proof = K ()}
val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time,
message} =
- prover params problem
+ prover params problem slice
val result as {outcome, ...} =
if is_none outcome0 andalso
forall (member (fn ((s, _), ((s', _), _)) => s = s') used_from) used_facts then
@@ -201,10 +213,11 @@
let
val ctxt = Proof.context_of state
val prover = get_prover ctxt Minimize prover_name
+ val slice = get_default_slice ctxt prover_name
val (chained, non_chained) = List.partition is_fact_chained facts
fun test timeout non_chained =
- test_facts params silent prover timeout i n state goal (chained @ non_chained)
+ test_facts params slice silent prover timeout i n state goal (chained @ non_chained)
in
(print silent (fn () => "Sledgehammer minimizer: " ^ prover_name);
(case test timeout non_chained of
@@ -258,8 +271,8 @@
| NONE => result)
end
-fun get_minimizing_prover ctxt mode do_learn name params problem =
- get_prover ctxt mode name params problem
+fun get_minimizing_prover ctxt mode do_learn name params problem slice =
+ get_prover ctxt mode name params problem slice
|> maybe_minimize mode do_learn name params problem
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Jan 31 16:09:23 2022 +0100
@@ -109,13 +109,17 @@
{outcome = outcome, filter_result = filter_result, used_from = facts, run_time = run_time}
end
-fun run_smt_solver mode name (params as {debug, verbose, isar_proofs, compress, try0,
+fun run_smt_solver mode name (params as {debug, verbose, fact_filter, isar_proofs, compress, try0,
smt_proofs, minimize, preplay_timeout, ...})
- ({state, goal, subgoal, subgoal_count, facts, found_proof, ...} : prover_problem) =
+ ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem)
+ slice =
let
val ctxt = Proof.context_of state
- val facts = snd facts
+ val SMT_Slice (best_max_facts, best_fact_filter) = slice
+
+ val effective_fact_filter = fact_filter |> the_default best_fact_filter
+ val facts = get_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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Mon Jan 31 16:09:23 2022 +0100
@@ -45,9 +45,10 @@
|> hd |> snd
val problem =
{comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
- facts = ("", facts), found_proof = K ()}
+ factss = [("", facts)], found_proof = K ()}
+ val slice = get_default_slice ctxt name
in
- (case prover params problem of
+ (case prover params problem slice of
{outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
| _ => NONE)
handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)