# HG changeset patch # User blanchet # Date 1282807401 -7200 # Node ID 01c4d14b2a618688a871b9ebc28bcb2056a22288 # Parent e752ce15990377af6501d5293259967bc4dfdcae add a bonus for chained facts, since they are likely to be relevant; (especially in a Mirabelle run!) -- chained facts used to be included forcibly, then were treated as any other fact; the current approach seems more flexible diff -r e752ce159903 -r 01c4d14b2a61 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 26 09:03:18 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 26 09:23:21 2010 +0200 @@ -255,7 +255,9 @@ fun irrel_weight _ _ = 1.0 *) -fun axiom_weight const_tab relevant_consts axiom_consts = +val chained_bonus_factor = 2.0 + +fun axiom_weight chained const_tab relevant_consts axiom_consts = case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts) ||> filter_out (pseudoconst_mem swap relevant_consts) of ([], []) => 0.0 @@ -263,6 +265,7 @@ | (rel, irrel) => let val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0 + |> chained ? curry Real.* chained_bonus_factor val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0 val res = rel_weight / (rel_weight + irrel_weight) in if Real.isFinite res then res else 0.0 end @@ -395,7 +398,8 @@ val weight = case cached_weight of SOME w => w - | NONE => axiom_weight const_tab rel_const_tab axiom_consts + | NONE => axiom_weight (snd (name ())) const_tab rel_const_tab + axiom_consts (* TODO: experiment val _ = if String.isPrefix "lift.simps(3" (fst (name ())) then tracing ("*** " ^ (fst (name ())) ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))