1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 19:47:25 2010 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 26 00:49:04 2010 +0200
1.3 @@ -101,36 +101,40 @@
1.4 | string_for_super_pseudoconst (s, Tss) =
1.5 s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}"
1.6
1.7 -(*Add a const/type pair to the table, but a [] entry means a standard connective,
1.8 - which we ignore.*)
1.9 -fun add_const_to_table (c, ctyps) =
1.10 - Symtab.map_default (c, [ctyps])
1.11 - (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
1.12 +val skolem_prefix = "Sledgehammer."
1.13 +
1.14 +(* Add a pseudoconstant to the table, but a [] entry means a standard
1.15 + connective, which we ignore.*)
1.16 +fun add_pseudoconst_to_table also_skolem (c, ctyps) =
1.17 + if also_skolem orelse not (String.isPrefix skolem_prefix c) then
1.18 + Symtab.map_default (c, [ctyps])
1.19 + (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
1.20 + else
1.21 + I
1.22
1.23 fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
1.24
1.25 -val fresh_prefix = "Sledgehammer.skolem."
1.26 val flip = Option.map not
1.27 (* These are typically simplified away by "Meson.presimplify". *)
1.28 val boring_consts =
1.29 [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}]
1.30
1.31 -fun get_consts thy pos ts =
1.32 +fun get_pseudoconsts thy also_skolems pos ts =
1.33 let
1.34 (* We include free variables, as well as constants, to handle locales. For
1.35 each quantifiers that must necessarily be skolemized by the ATP, we
1.36 introduce a fresh constant to simulate the effect of Skolemization. *)
1.37 fun do_term t =
1.38 case t of
1.39 - Const x => add_const_to_table (pseudoconst_for thy x)
1.40 - | Free (s, _) => add_const_to_table (s, [])
1.41 + Const x => add_pseudoconst_to_table also_skolems (pseudoconst_for thy x)
1.42 + | Free (s, _) => add_pseudoconst_to_table also_skolems (s, [])
1.43 | t1 $ t2 => fold do_term [t1, t2]
1.44 - | Abs (_, _, t') => do_term t'
1.45 + | Abs (_, _, t') => do_term t' (* FIXME: add penalty? *)
1.46 | _ => I
1.47 fun do_quantifier will_surely_be_skolemized body_t =
1.48 do_formula pos body_t
1.49 - #> (if will_surely_be_skolemized then
1.50 - add_const_to_table (gensym fresh_prefix, [])
1.51 + #> (if also_skolems andalso will_surely_be_skolemized then
1.52 + add_pseudoconst_to_table true (gensym skolem_prefix, [])
1.53 else
1.54 I)
1.55 and do_term_or_formula T =
1.56 @@ -233,14 +237,20 @@
1.57
1.58 (* "log" seems best in practice. A constant function of one ignores the constant
1.59 frequencies. *)
1.60 -fun rel_log (x : real) = 1.0 + 2.0 / Math.ln (x + 1.0)
1.61 -fun irrel_log (x : real) = Math.ln (x + 19.0) / 6.4
1.62 +fun rel_log n = 1.0 + 2.0 / Math.ln (Real.fromInt n + 1.0)
1.63 +(* TODO: experiment
1.64 +fun irrel_log n = 0.5 + 1.0 / Math.ln (Real.fromInt n + 1.0)
1.65 +*)
1.66 +fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4
1.67
1.68 (* Computes a constant's weight, as determined by its frequency. *)
1.69 -val rel_weight = rel_log o real oo pseudoconst_freq match_pseudotypes
1.70 -val irrel_weight =
1.71 - irrel_log o real oo pseudoconst_freq (match_pseudotypes o swap)
1.72 -(* fun irrel_weight _ _ = 1.0 FIXME: OLD CODE *)
1.73 +val rel_weight = rel_log oo pseudoconst_freq match_pseudotypes
1.74 +fun irrel_weight const_tab (c as (s, _)) =
1.75 + if String.isPrefix skolem_prefix s then 1.0
1.76 + else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c)
1.77 +(* TODO: experiment
1.78 +fun irrel_weight _ _ = 1.0
1.79 +*)
1.80
1.81 fun axiom_weight const_tab relevant_consts axiom_consts =
1.82 case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
1.83 @@ -254,40 +264,60 @@
1.84 val res = rel_weight / (rel_weight + irrel_weight)
1.85 in if Real.isFinite res then res else 0.0 end
1.86
1.87 -fun consts_of_term thy t =
1.88 +(* TODO: experiment
1.89 +fun debug_axiom_weight const_tab relevant_consts axiom_consts =
1.90 + case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
1.91 + ||> filter_out (pseudoconst_mem swap relevant_consts) of
1.92 + ([], []) => 0.0
1.93 + | (_, []) => 1.0
1.94 + | (rel, irrel) =>
1.95 + let
1.96 +val _ = tracing (PolyML.makestring ("REL: ", rel))
1.97 +val _ = tracing (PolyML.makestring ("IRREL: ", irrel))
1.98 + val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
1.99 + val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
1.100 + val res = rel_weight / (rel_weight + irrel_weight)
1.101 + in if Real.isFinite res then res else 0.0 end
1.102 +*)
1.103 +
1.104 +fun pseudoconsts_of_term thy t =
1.105 Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys)
1.106 - (get_consts thy (SOME true) [t]) []
1.107 -
1.108 + (get_pseudoconsts thy true (SOME true) [t]) []
1.109 fun pair_consts_axiom theory_relevant thy axiom =
1.110 (axiom, axiom |> snd |> theory_const_prop_of theory_relevant
1.111 - |> consts_of_term thy)
1.112 + |> pseudoconsts_of_term thy)
1.113
1.114 type annotated_thm =
1.115 ((unit -> string * bool) * thm) * (string * pseudotype list) list
1.116
1.117 -fun take_best max (candidates : (annotated_thm * real) list) =
1.118 +fun take_most_relevant max_max_imperfect max_relevant remaining_max
1.119 + (candidates : (annotated_thm * real) list) =
1.120 let
1.121 - val ((perfect, more_perfect), imperfect) =
1.122 - candidates |> List.partition (fn (_, w) => w > 0.99999) |>> chop (max - 1)
1.123 + val max_imperfect =
1.124 + Real.ceil (Math.pow (max_max_imperfect,
1.125 + Real.fromInt remaining_max
1.126 + / Real.fromInt max_relevant))
1.127 + val (perfect, imperfect) =
1.128 + candidates |> List.partition (fn (_, w) => w > 0.99999)
1.129 ||> sort (Real.compare o swap o pairself snd)
1.130 - val (accepts, rejects) =
1.131 - case more_perfect @ imperfect of
1.132 - [] => (perfect, [])
1.133 - | (q :: qs) => (q :: perfect, qs)
1.134 + val ((accepts, more_rejects), rejects) =
1.135 + chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
1.136 in
1.137 trace_msg (fn () => "Number of candidates: " ^
1.138 string_of_int (length candidates));
1.139 trace_msg (fn () => "Effective threshold: " ^
1.140 Real.toString (#2 (hd accepts)));
1.141 - trace_msg (fn () => "Actually passed: " ^
1.142 - (accepts |> map (fn (((name, _), _), weight) =>
1.143 + trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^
1.144 + "): " ^ (accepts
1.145 + |> map (fn (((name, _), _), weight) =>
1.146 fst (name ()) ^ " [" ^ Real.toString weight ^ "]")
1.147 |> commas));
1.148 - (accepts, rejects)
1.149 + (accepts, more_rejects @ rejects)
1.150 end
1.151
1.152 val threshold_divisor = 2.0
1.153 val ridiculous_threshold = 0.1
1.154 +val max_max_imperfect_fudge_factor = 0.66
1.155
1.156 fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant
1.157 ({add, del, ...} : relevance_override) axioms goal_ts =
1.158 @@ -297,30 +327,35 @@
1.159 Symtab.empty
1.160 val add_thms = maps (ProofContext.get_fact ctxt) add
1.161 val del_thms = maps (ProofContext.get_fact ctxt) del
1.162 - fun iter j max threshold rel_const_tab hopeless hopeful =
1.163 + val max_max_imperfect =
1.164 + Math.sqrt (Real.fromInt max_relevant * max_max_imperfect_fudge_factor)
1.165 + fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
1.166 let
1.167 fun game_over rejects =
1.168 - if j = 0 andalso threshold >= ridiculous_threshold then
1.169 - (* First iteration? Try again. *)
1.170 - iter 0 max (threshold / threshold_divisor) rel_const_tab hopeless
1.171 - hopeful
1.172 + (* Add "add:" facts. *)
1.173 + if null add_thms then
1.174 + []
1.175 else
1.176 - (* Add "add:" facts. *)
1.177 - if null add_thms then
1.178 - []
1.179 + map_filter (fn ((p as (_, th), _), _) =>
1.180 + if member Thm.eq_thm add_thms th then SOME p
1.181 + else NONE) rejects
1.182 + fun relevant [] rejects hopeless [] =
1.183 + (* Nothing has been added this iteration. *)
1.184 + if j = 0 andalso threshold >= ridiculous_threshold then
1.185 + (* First iteration? Try again. *)
1.186 + iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
1.187 + hopeless hopeful
1.188 else
1.189 - map_filter (fn ((p as (_, th), _), _) =>
1.190 - if member Thm.eq_thm add_thms th then SOME p
1.191 - else NONE) rejects
1.192 - fun relevant [] rejects [] hopeless =
1.193 - (* Nothing has been added this iteration. *)
1.194 - game_over (map (apsnd SOME) (rejects @ hopeless))
1.195 - | relevant candidates rejects [] hopeless =
1.196 + game_over (rejects @ hopeless)
1.197 + | relevant candidates rejects hopeless [] =
1.198 let
1.199 - val (accepts, more_rejects) = take_best max candidates
1.200 + val (accepts, more_rejects) =
1.201 + take_most_relevant max_max_imperfect max_relevant remaining_max
1.202 + candidates
1.203 val rel_const_tab' =
1.204 rel_const_tab
1.205 - |> fold add_const_to_table (maps (snd o fst) accepts)
1.206 + |> fold (add_pseudoconst_to_table false)
1.207 + (maps (snd o fst) accepts)
1.208 fun is_dirty (c, _) =
1.209 Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
1.210 val (hopeful_rejects, hopeless_rejects) =
1.211 @@ -334,33 +369,41 @@
1.212 |> map (fn (ax as (_, consts), old_weight) =>
1.213 (ax, if exists is_dirty consts then NONE
1.214 else SOME old_weight)))
1.215 - val threshold = threshold + (1.0 - threshold) * decay
1.216 - val max = max - length accepts
1.217 + val threshold =
1.218 + threshold + (1.0 - threshold)
1.219 + * Math.pow (decay, Real.fromInt (length accepts))
1.220 + val remaining_max = remaining_max - length accepts
1.221 in
1.222 trace_msg (fn () => "New or updated constants: " ^
1.223 commas (rel_const_tab' |> Symtab.dest
1.224 |> subtract (op =) (Symtab.dest rel_const_tab)
1.225 |> map string_for_super_pseudoconst));
1.226 map (fst o fst) accepts @
1.227 - (if max = 0 then
1.228 + (if remaining_max = 0 then
1.229 game_over (hopeful_rejects @ map (apsnd SOME) hopeless_rejects)
1.230 else
1.231 - iter (j + 1) max threshold rel_const_tab' hopeless_rejects
1.232 - hopeful_rejects)
1.233 + iter (j + 1) remaining_max threshold rel_const_tab'
1.234 + hopeless_rejects hopeful_rejects)
1.235 end
1.236 - | relevant candidates rejects
1.237 + | relevant candidates rejects hopeless
1.238 (((ax as ((name, th), axiom_consts)), cached_weight)
1.239 - :: hopeful) hopeless =
1.240 + :: hopeful) =
1.241 let
1.242 val weight =
1.243 case cached_weight of
1.244 SOME w => w
1.245 | NONE => axiom_weight const_tab rel_const_tab axiom_consts
1.246 +(* TODO: experiment
1.247 +val _ = if String.isPrefix "lift.simps(3" (fst (name ())) then
1.248 +tracing ("*** " ^ (fst (name ())) ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))
1.249 +else
1.250 +()
1.251 +*)
1.252 in
1.253 if weight >= threshold then
1.254 - relevant ((ax, weight) :: candidates) rejects hopeful hopeless
1.255 + relevant ((ax, weight) :: candidates) rejects hopeless hopeful
1.256 else
1.257 - relevant candidates ((ax, weight) :: rejects) hopeful hopeless
1.258 + relevant candidates ((ax, weight) :: rejects) hopeless hopeful
1.259 end
1.260 in
1.261 trace_msg (fn () =>
1.262 @@ -369,13 +412,13 @@
1.263 commas (rel_const_tab |> Symtab.dest
1.264 |> filter (curry (op <>) [] o snd)
1.265 |> map string_for_super_pseudoconst));
1.266 - relevant [] [] hopeful hopeless
1.267 + relevant [] [] hopeless hopeful
1.268 end
1.269 in
1.270 axioms |> filter_out (member Thm.eq_thm del_thms o snd)
1.271 |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
1.272 |> iter 0 max_relevant threshold0
1.273 - (get_consts thy (SOME false) goal_ts) []
1.274 + (get_pseudoconsts thy false (SOME false) goal_ts) []
1.275 |> tap (fn res => trace_msg (fn () =>
1.276 "Total relevant: " ^ Int.toString (length res)))
1.277 end