compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jun 09 23:30:18 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jun 10 12:01:15 2011 +0200
@@ -408,10 +408,13 @@
val _ = if is_appropriate_prop concl_t then ()
else raise Fail "inappropriate"
val facts =
- Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
- (the_default default_max_relevant max_relevant)
- is_appropriate_prop is_built_in_const relevance_fudge
- relevance_override chained_ths hyp_ts concl_t
+ Sledgehammer_Filter.nearly_all_facts ctxt relevance_override
+ chained_ths hyp_ts concl_t
+ |> filter (is_appropriate_prop o prop_of o snd)
+ |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
+ (the_default default_max_relevant max_relevant)
+ is_built_in_const relevance_fudge relevance_override
+ chained_ths hyp_ts concl_t
val problem =
{state = st', goal = goal, subgoal = i,
subgoal_count = Sledgehammer_Util.subgoal_count st,
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Jun 09 23:30:18 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Jun 10 12:01:15 2011 +0200
@@ -110,7 +110,7 @@
(case Prooftab.lookup (!proof_table) (line_num, col_num) of
SOME proofs =>
let
- val {context = ctxt, facts, goal} = Proof.goal pre
+ val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre
val prover = AList.lookup (op =) args "prover"
|> the_default default_prover
val {relevance_thresholds, max_relevant, slicing, ...} =
@@ -130,10 +130,13 @@
val subgoal = 1
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
val facts =
- Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
- (the_default default_max_relevant max_relevant)
- is_appropriate_prop is_built_in_const relevance_fudge
- relevance_override facts hyp_ts concl_t
+ Sledgehammer_Filter.nearly_all_facts ctxt relevance_override
+ chained_ths hyp_ts concl_t
+ |> filter (is_appropriate_prop o prop_of o snd)
+ |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
+ (the_default default_max_relevant max_relevant)
+ is_built_in_const relevance_fudge relevance_override
+ chained_ths hyp_ts concl_t
|> map (fst o fst)
val (found_facts, lost_facts) =
flat proofs |> sort_distinct string_ord
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Jun 09 23:30:18 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Jun 10 12:01:15 2011 +0200
@@ -39,19 +39,23 @@
val new_monomorphizer : bool Config.T
val ignore_no_atp : bool Config.T
val instantiate_inducts : bool Config.T
+ val const_names_in_fact :
+ theory -> (string * typ -> term list -> bool * term list) -> term
+ -> string list
val fact_from_ref :
Proof.context -> unit Symtab.table -> thm list
-> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
val all_facts :
- Proof.context -> 'a Symtab.table -> bool -> (term -> bool) -> thm list
- -> thm list -> (((unit -> string) * locality) * thm) list
- val const_names_in_fact :
- theory -> (string * typ -> term list -> bool * term list) -> term
- -> string list
+ Proof.context -> 'a Symtab.table -> bool -> thm list -> thm list
+ -> (((unit -> string) * locality) * thm) list
+ val nearly_all_facts :
+ Proof.context -> relevance_override -> thm list -> term list -> term
+ -> (((unit -> string) * locality) * thm) list
val relevant_facts :
- Proof.context -> real * real -> int -> (term -> bool)
+ Proof.context -> real * real -> int
-> (string * typ -> term list -> bool * term list) -> relevance_fudge
-> relevance_override -> thm list -> term list -> term
+ -> (((unit -> string) * locality) * thm) list
-> ((string * locality) * thm) list
end;
@@ -778,12 +782,11 @@
(**** Predicates to detect unwanted facts (prolific or likely to cause
unsoundness) ****)
-fun is_theorem_bad_for_atps is_appropriate_prop thm =
+fun is_theorem_bad_for_atps thm =
let val t = prop_of thm in
- not (is_appropriate_prop t) orelse is_formula_too_complex t orelse
- exists_type type_has_top_sort t orelse exists_sledgehammer_const t orelse
- exists_low_level_class_const t orelse is_metastrange_theorem thm orelse
- is_that_fact thm
+ is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
+ exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
+ is_metastrange_theorem thm orelse is_that_fact thm
end
fun meta_equify (@{const Trueprop}
@@ -810,7 +813,7 @@
|> add Simp normalize_simp_prop snd simps
end
-fun all_facts ctxt reserved really_all is_appropriate_prop add_ths chained_ths =
+fun all_facts ctxt reserved really_all add_ths chained_ths =
let
val thy = Proof_Context.theory_of ctxt
val global_facts = Global_Theory.facts_of thy
@@ -860,7 +863,7 @@
#> fold (fn th => fn (j, (multis, unis)) =>
(j + 1,
if not (member Thm.eq_thm_prop add_ths th) andalso
- is_theorem_bad_for_atps is_appropriate_prop th then
+ is_theorem_bad_for_atps th then
(multis, unis)
else
let
@@ -894,30 +897,36 @@
fun external_frees t =
[] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
+fun nearly_all_facts ctxt ({add, only, ...} : relevance_override) chained_ths
+ hyp_ts concl_t =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val reserved = reserved_isar_keyword_table ()
+ val add_ths = Attrib.eval_thms ctxt add
+ val ind_stmt =
+ Logic.list_implies (hyp_ts |> filter_out (null o external_frees), concl_t)
+ |> Object_Logic.atomize_term thy
+ val ind_stmt_xs = external_frees ind_stmt
+ in
+ (if only then
+ maps (map (fn ((name, loc), th) => ((K name, loc), th))
+ o fact_from_ref ctxt reserved chained_ths) add
+ else
+ all_facts ctxt reserved false add_ths chained_ths)
+ |> Config.get ctxt instantiate_inducts
+ ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
+ |> (not (Config.get ctxt ignore_no_atp) andalso not only)
+ ? filter_out (No_ATPs.member ctxt o snd)
+ |> uniquify
+ end
+
fun relevant_facts ctxt (threshold0, threshold1) max_relevant
- is_appropriate_prop is_built_in_const fudge
- (override as {add, only, ...}) chained_ths hyp_ts concl_t =
+ is_built_in_const fudge (override as {only, ...}) chained_ths
+ hyp_ts concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
1.0 / Real.fromInt (max_relevant + 1))
- val add_ths = Attrib.eval_thms ctxt add
- val reserved = reserved_isar_keyword_table ()
- val ind_stmt =
- Logic.list_implies (hyp_ts |> filter_out (null o external_frees), concl_t)
- |> Object_Logic.atomize_term thy
- val ind_stmt_xs = external_frees ind_stmt
- val facts =
- (if only then
- maps (map (fn ((name, loc), th) => ((K name, loc), th))
- o fact_from_ref ctxt reserved chained_ths) add
- else
- all_facts ctxt reserved false is_appropriate_prop add_ths chained_ths)
- |> Config.get ctxt instantiate_inducts
- ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
- |> (not (Config.get ctxt ignore_no_atp) andalso not only)
- ? filter_out (No_ATPs.member ctxt o snd)
- |> uniquify
in
trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
" facts");
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jun 09 23:30:18 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jun 10 12:01:15 2011 +0200
@@ -260,6 +260,8 @@
val {facts = chained_ths, goal, ...} = Proof.goal state
val chained_ths = chained_ths |> normalize_chained_theorems
val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
+ val facts = nearly_all_facts ctxt relevance_override chained_ths hyp_ts
+ concl_t
val _ = () |> not blocking ? kill_provers
val _ = case find_first (not o is_prover_supported ctxt) provers of
SOME name => error ("No such prover: " ^ name ^ ".")
@@ -307,9 +309,13 @@
val is_built_in_const =
is_built_in_const_for_prover ctxt (hd provers)
in
- relevant_facts ctxt relevance_thresholds max_max_relevant
- is_appropriate_prop is_built_in_const relevance_fudge
- relevance_override chained_ths hyp_ts concl_t
+ facts
+ |> (case is_appropriate_prop of
+ SOME is_app => filter (is_app o prop_of o snd)
+ | NONE => I)
+ |> relevant_facts ctxt relevance_thresholds max_max_relevant
+ is_built_in_const relevance_fudge relevance_override
+ chained_ths hyp_ts concl_t
|> tap (fn facts =>
if debug then
label ^ plural_s (length provers) ^ ": " ^
@@ -326,7 +332,8 @@
fun launch_atps label is_appropriate_prop atps accum =
if null atps then
accum
- else if not (is_appropriate_prop concl_t) then
+ else if is_some is_appropriate_prop andalso
+ not (the is_appropriate_prop concl_t) then
(if verbose orelse length atps = length provers then
"Goal outside the scope of " ^
space_implode " " (serial_commas "and" (map quote atps)) ^ "."
@@ -343,7 +350,7 @@
accum
else
let
- val facts = get_facts "SMT solver" (K true) smt_relevance_fudge smts
+ val facts = get_facts "SMT solver" NONE smt_relevance_fudge smts
val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt
fun smt_filter facts =
(if debug then curry (op o) SOME
@@ -356,9 +363,9 @@
#> fst)
|> max_outcome_code |> rpair state
end
- val launch_full_atps = launch_atps "ATP" (K true) full_atps
+ val launch_full_atps = launch_atps "ATP" NONE full_atps
val launch_ueq_atps =
- launch_atps "Unit equational provers" is_unit_equality ueq_atps
+ launch_atps "Unit equational provers" (SOME is_unit_equality) ueq_atps
fun launch_atps_and_smt_solvers () =
[launch_full_atps, launch_smts, launch_ueq_atps]
|> smart_par_list_map (fn f => ignore (f (unknownN, state)))
--- a/src/HOL/ex/atp_export.ML Thu Jun 09 23:30:18 2011 +0200
+++ b/src/HOL/ex/atp_export.ML Fri Jun 10 12:01:15 2011 +0200
@@ -23,7 +23,7 @@
fun facts_of thy =
Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty
- true (K true) [] []
+ true [] []
fun fold_body_thms f =
let
--- a/src/HOL/ex/sledgehammer_tactics.ML Thu Jun 09 23:30:18 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Fri Jun 10 12:01:15 2011 +0200
@@ -34,10 +34,11 @@
val relevance_override = {add = [], del = [], only = false}
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
val facts =
- Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
- (the_default default_max_relevant max_relevant) (K true)
- is_built_in_const relevance_fudge relevance_override chained_ths
- hyp_ts concl_t
+ Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths
+ hyp_ts concl_t
+ |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
+ (the_default default_max_relevant max_relevant) is_built_in_const
+ relevance_fudge relevance_override chained_ths hyp_ts concl_t
val problem =
{state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
facts = map Sledgehammer_Provers.Untranslated_Fact facts,