# HG changeset patch # User blanchet # Date 1282925089 -7200 # Node ID d0e3f68dde632f96c03fc3b6b1c0b77eef717234 # Parent c18e8f90f4dc39a00245c4e7bb0eb191bf7229d1 fiddle with the relevance filter diff -r c18e8f90f4dc -r d0e3f68dde63 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 27 16:05:46 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 27 18:04:49 2010 +0200 @@ -13,7 +13,6 @@ only: bool} val trace : bool Unsynchronized.ref - val term_patterns : bool Unsynchronized.ref val name_thm_pairs_from_ref : Proof.context -> unit Symtab.table -> thm list -> Facts.ref -> ((string * locality) * thm) list @@ -32,7 +31,7 @@ fun trace_msg msg = if !trace then tracing (msg ()) else () (* experimental feature *) -val term_patterns = Unsynchronized.ref false +val term_patterns = false val respect_no_atp = true @@ -108,7 +107,7 @@ and pconst_args thy const (s, T) ts = (if const then map ptype (these (try (Sign.const_typargs thy) (s, T))) else []) @ - (if !term_patterns then map (pterm thy) ts else []) + (if term_patterns then map (pterm thy) ts else []) and pconst thy const (s, T) ts = (s, pconst_args thy const (s, T) ts) fun string_for_hyper_pconst (s, pss) = @@ -272,27 +271,24 @@ swap (* FUDGE *) -fun locality_multiplier General = 1.0 - | locality_multiplier Theory = 1.1 - | locality_multiplier Local = 1.3 - | locality_multiplier Chained = 2.0 +fun locality_bonus General = 0.0 + | locality_bonus Theory = 0.5 + | locality_bonus Local = 1.0 + | locality_bonus Chained = 2.0 fun axiom_weight loc const_tab relevant_consts axiom_consts = case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts) ||> filter_out (pconst_hyper_mem swap relevant_consts) of ([], _) => 0.0 | (rel, irrel) => - case irrel |> filter_out (pconst_mem swap rel) of - [] => 1.0 - | irrel => - let - val rel_weight = - fold (curry Real.+ o rel_weight const_tab) rel 0.0 - |> curry Real.* (locality_multiplier loc) - 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 + let + val irrel = irrel |> filter_out (pconst_mem swap rel) + val rel_weight = 0.0 |> fold (curry (op +) o rel_weight const_tab) rel + val irrel_weight = + ~ (locality_bonus loc) + |> fold (curry (op +) o irrel_weight const_tab) irrel + val res = rel_weight / (rel_weight + irrel_weight) + in if Real.isFinite res then res else 0.0 end fun pconsts_in_axiom thy t = Symtab.fold (fn (s, pss) => fold (cons o pair s) pss) @@ -306,22 +302,25 @@ type annotated_thm = (((unit -> string) * locality) * thm) * (string * pattern list) list +val max_imperfect_exp = 4.0 + fun take_most_relevant max_max_imperfect max_relevant remaining_max (candidates : (annotated_thm * real) list) = let val max_imperfect = Real.ceil (Math.pow (max_max_imperfect, - Real.fromInt remaining_max - / Real.fromInt max_relevant)) + Math.pow (Real.fromInt remaining_max + / Real.fromInt max_relevant, max_imperfect_exp))) val (perfect, imperfect) = - candidates |> List.partition (fn (_, w) => w > 0.99999) - ||> sort (Real.compare o swap o pairself snd) + candidates |> sort (Real.compare o swap o pairself snd) + |> take_prefix (fn (_, w) => w > 0.99999) val ((accepts, more_rejects), rejects) = chop max_imperfect imperfect |>> append perfect |>> chop remaining_max in - trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^ - " of " ^ Int.toString (length candidates) ^ "): " ^ (accepts - |> map (fn ((((name, _), _), _), weight) => + trace_msg (fn () => + "Actually passed (" ^ Int.toString (length accepts) ^ " of " ^ + Int.toString (length candidates) ^ "): " ^ + (accepts |> map (fn ((((name, _), _), _), weight) => name () ^ " [" ^ Real.toString weight ^ "]") |> commas)); (accepts, more_rejects @ rejects) @@ -338,7 +337,7 @@ (* FUDGE *) val threshold_divisor = 2.0 val ridiculous_threshold = 0.1 -val max_max_imperfect_fudge_factor = 0.66 +val max_max_imperfect_fudge_factor = 0.5 fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant ({add, del, ...} : relevance_override) axioms goal_ts = @@ -353,7 +352,7 @@ val add_thms = maps (ProofContext.get_fact ctxt) add val del_thms = maps (ProofContext.get_fact ctxt) del val max_max_imperfect = - Math.sqrt (Real.fromInt max_relevant * max_max_imperfect_fudge_factor) + Math.sqrt (Real.fromInt max_relevant) * max_max_imperfect_fudge_factor fun iter j remaining_max threshold rel_const_tab hopeless hopeful = let fun game_over rejects = @@ -364,7 +363,7 @@ map_filter (fn ((p as (_, th), _), _) => if member Thm.eq_thm add_thms th then SOME p else NONE) rejects - fun relevant [] rejects hopeless [] = + fun relevant [] rejects [] = (* Nothing has been added this iteration. *) if j = 0 andalso threshold >= ridiculous_threshold then (* First iteration? Try again. *) @@ -372,7 +371,7 @@ hopeless hopeful else game_over (rejects @ hopeless) - | relevant candidates rejects hopeless [] = + | relevant candidates rejects [] = let val (accepts, more_rejects) = take_most_relevant max_max_imperfect max_relevant remaining_max @@ -410,7 +409,7 @@ iter (j + 1) remaining_max threshold rel_const_tab' hopeless_rejects hopeful_rejects) end - | relevant candidates rejects hopeless + | relevant candidates rejects (((ax as (((_, loc), th), axiom_consts)), cached_weight) :: hopeful) = let @@ -427,9 +426,9 @@ *) in if weight >= threshold then - relevant ((ax, weight) :: candidates) rejects hopeless hopeful + relevant ((ax, weight) :: candidates) rejects hopeful else - relevant candidates ((ax, weight) :: rejects) hopeless hopeful + relevant candidates ((ax, weight) :: rejects) hopeful end in trace_msg (fn () => @@ -438,7 +437,7 @@ commas (rel_const_tab |> Symtab.dest |> filter (curry (op <>) [] o snd) |> map string_for_hyper_pconst)); - relevant [] [] hopeless hopeful + relevant [] [] hopeful end in axioms |> filter_out (member Thm.eq_thm del_thms o snd)