# HG changeset patch # User blanchet # Date 1307700075 -7200 # Node ID b19d95b4d7365e7bd4c1b915fd214b1b15250626 # Parent 165188299a25a760adcd2fdecaf13e4a01098e39 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 diff -r 165188299a25 -r b19d95b4d736 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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, diff -r 165188299a25 -r b19d95b4d736 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- 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 diff -r 165188299a25 -r b19d95b4d736 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- 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"); diff -r 165188299a25 -r b19d95b4d736 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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))) diff -r 165188299a25 -r b19d95b4d736 src/HOL/ex/atp_export.ML --- 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 diff -r 165188299a25 -r b19d95b4d736 src/HOL/ex/sledgehammer_tactics.ML --- 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,