# HG changeset patch # User blanchet # Date 1282154232 -7200 # Node ID af205f4fd0f3cfa0f299698cc64995c00ca55543 # Parent 85aef7587cf1fd582d818470c79d5e2c338203fa tuning of relevance filter diff -r 85aef7587cf1 -r af205f4fd0f3 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 18 18:01:54 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 18 19:57:12 2010 +0200 @@ -104,7 +104,8 @@ introduce a fresh constant to simulate the effect of Skolemization. *) fun do_term t = case t of - Const x => add_const_type_to_table (const_with_typ thy x) + Const (@{const_name Let}, _) => I + | Const x => add_const_type_to_table (const_with_typ thy x) | Free x => add_const_type_to_table (const_with_typ thy x) | t1 $ t2 => do_term t1 #> do_term t2 | Abs (_, _, t) => @@ -297,56 +298,9 @@ end end; -fun relevant_facts ctxt relevance_convergence defs_relevant max_new - ({add, del, ...} : relevance_override) const_tab = - let - val thy = ProofContext.theory_of ctxt - val add_thms = maps (ProofContext.get_fact ctxt) add - val del_thms = maps (ProofContext.get_fact ctxt) del - fun iter threshold rel_const_tab = - let - fun relevant ([], _) [] = [] (* Nothing added this iteration *) - | relevant (newpairs, rejects) [] = - let - val (newrels, more_rejects) = take_best max_new newpairs - val new_consts = maps #2 newrels - val rel_const_tab = - rel_const_tab |> fold add_const_type_to_table new_consts - val threshold = - threshold + (1.0 - threshold) / relevance_convergence - in - trace_msg (fn () => "relevant this iteration: " ^ - Int.toString (length newrels)); - map #1 newrels @ iter threshold rel_const_tab - (more_rejects @ rejects) - end - | relevant (newrels, rejects) - ((ax as ((name, th), consts_typs)) :: axs) = - let - val weight = - if member Thm.eq_thm add_thms th then 1.0 - else if member Thm.eq_thm del_thms th then 0.0 - else formula_weight const_tab rel_const_tab consts_typs - in - if weight >= threshold orelse - (defs_relevant andalso defines thy th rel_const_tab) then - (trace_msg (fn () => - name ^ " passes: " ^ Real.toString weight - (* ^ " consts: " ^ commas (map fst consts_typs) *)); - relevant ((ax, weight) :: newrels, rejects) axs) - else - relevant (newrels, ax :: rejects) axs - end - in - trace_msg (fn () => "relevant_facts, current threshold: " ^ - Real.toString threshold); - relevant ([], []) - end - in iter end - fun relevance_filter ctxt relevance_threshold relevance_convergence - defs_relevant max_new theory_relevant relevance_override - axioms goal_ts = + defs_relevant max_new theory_relevant + ({add, del, ...} : relevance_override) axioms goal_ts = if relevance_threshold > 1.0 then [] else if relevance_threshold < 0.0 then @@ -364,12 +318,56 @@ |> Symtab.dest |> filter (curry (op <>) [] o snd) |> map fst)) - val relevant = - relevant_facts ctxt relevance_convergence defs_relevant max_new - relevance_override const_tab relevance_threshold - goal_const_tab - (map (pair_consts_typs_axiom theory_relevant thy) - axioms) + val add_thms = maps (ProofContext.get_fact ctxt) add + val del_thms = maps (ProofContext.get_fact ctxt) del + fun iter threshold rel_const_tab = + let + fun relevant ([], rejects) [] = + (* Nothing was added this iteration: Add "add:" facts. *) + if null add_thms then + [] + else + map_filter (fn (p as (name, th), _) => + if member Thm.eq_thm add_thms th then SOME p + else NONE) rejects + | relevant (newpairs, rejects) [] = + let + val (newrels, more_rejects) = take_best max_new newpairs + val new_consts = maps #2 newrels + val rel_const_tab = + rel_const_tab |> fold add_const_type_to_table new_consts + val threshold = + threshold + (1.0 - threshold) / relevance_convergence + in + trace_msg (fn () => "relevant this iteration: " ^ + Int.toString (length newrels)); + map #1 newrels @ iter threshold rel_const_tab + (more_rejects @ rejects) + end + | relevant (newrels, rejects) + ((ax as ((name, th), consts_typs)) :: axs) = + let + val weight = + if member Thm.eq_thm del_thms th then 0.0 + else formula_weight const_tab rel_const_tab consts_typs + in + if weight >= threshold orelse + (defs_relevant andalso defines thy th rel_const_tab) then + (trace_msg (fn () => + name ^ " passes: " ^ Real.toString weight + (* ^ " consts: " ^ commas (map fst consts_typs) *)); + relevant ((ax, weight) :: newrels, rejects) axs) + else + relevant (newrels, ax :: rejects) axs + end + in + trace_msg (fn () => "relevant_facts, current threshold: " ^ + Real.toString threshold); + relevant ([], []) + end + val relevant = iter relevance_threshold goal_const_tab + (map (pair_consts_typs_axiom theory_relevant thy) + axioms) in trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant)); relevant @@ -559,20 +557,17 @@ (ctxt, (chained_ths, _)) hyp_ts concl_t = let val add_thms = maps (ProofContext.get_fact ctxt) add - val has_override = not (null add) orelse not (null del) val axioms = checked_name_thm_pairs (respect_no_atp andalso not only) ctxt (map (name_thms_pair_from_ref ctxt chained_ths) add @ (if only then [] else all_name_thms_pairs ctxt chained_ths)) - |> not has_override ? make_unique |> filter (fn (_, th) => member Thm.eq_thm add_thms th orelse not (is_dangerous_term full_types (prop_of th))) in relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override axioms (concl_t :: hyp_ts) - |> has_override ? make_unique - |> sort_wrt fst + |> make_unique |> sort_wrt fst end end;