author paulson Wed Aug 15 13:50:47 2007 +0200 (2007-08-15) changeset 24287 c857dac06da6 parent 24286 7619080e49f0 child 24288 4016baca4973
combining the relevance filter with res_atp
 src/HOL/Tools/ATP/reduce_axiomsN.ML file | annotate | diff | revisions src/HOL/Tools/res_atp.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Aug 15 12:52:56 2007 +0200
1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,256 +0,0 @@
1.4 -(* Authors: Jia Meng, NICTA and Lawrence C Paulson, Cambridge University Computer Laboratory
1.5 -   ID: \$Id\$
1.6 -   Filtering strategies *)
1.7 -
1.8 -(*A surprising number of theorems contain only a few significant constants.
1.9 -  These include all induction rules, and other general theorems. Filtering
1.10 -  theorems in clause form reveals these complexities in the form of Skolem
1.11 -  functions. If we were instead to filter theorems in their natural form,
1.12 -  some other method of measuring theorem complexity would become necessary.*)
1.13 -
1.14 -structure ReduceAxiomsN =
1.15 -struct
1.16 -
1.17 -val run_relevance_filter = ref true;
1.18 -val theory_const = ref true;
1.19 -val pass_mark = ref 0.5;
1.20 -val convergence = ref 3.2;    (*Higher numbers allow longer inference chains*)
1.21 -val max_new = ref 60;         (*Limits how many clauses can be picked up per stage*)
1.22 -val follow_defs = ref false;  (*Follow definitions. Makes problems bigger.*)
1.23 -
1.24 -fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0);
1.25 -
1.26 -(*The default seems best in practice. A constant function of one ignores
1.27 -  the constant frequencies.*)
1.28 -val weight_fn = ref log_weight2;
1.29 -
1.30 -
1.31 -(*Including equality in this list might be expected to stop rules like subset_antisym from
1.32 -  being chosen, but for some reason filtering works better with them listed. The
1.33 -  logical signs All, Ex, &, and --> are omitted because any remaining occurrrences
1.34 -  must be within comprehensions.*)
1.35 -val standard_consts = ["Trueprop","==>","all","==","op |","Not","op ="];
1.36 -
1.37 -
1.38 -(*** constants with types ***)
1.39 -
1.40 -(*An abstraction of Isabelle types*)
1.41 -datatype const_typ =  CTVar | CType of string * const_typ list
1.42 -
1.43 -(*Is the second type an instance of the first one?*)
1.44 -fun match_type (CType(con1,args1)) (CType(con2,args2)) =
1.45 -      con1=con2 andalso match_types args1 args2
1.46 -  | match_type CTVar _ = true
1.47 -  | match_type _ CTVar = false
1.48 -and match_types [] [] = true
1.49 -  | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
1.50 -
1.51 -(*Is there a unifiable constant?*)
1.52 -fun uni_mem gctab (c,c_typ) =
1.53 -  case Symtab.lookup gctab c of
1.54 -      NONE => false
1.55 -    | SOME ctyps_list => exists (match_types c_typ) ctyps_list;
1.56 -
1.57 -(*Maps a "real" type to a const_typ*)
1.58 -fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs)
1.59 -  | const_typ_of (TFree _) = CTVar
1.60 -  | const_typ_of (TVar _) = CTVar
1.61 -
1.62 -(*Pairs a constant with the list of its type instantiations (using const_typ)*)
1.63 -fun const_with_typ thy (c,typ) =
1.64 -    let val tvars = Sign.const_typargs thy (c,typ)
1.65 -    in (c, map const_typ_of tvars) end
1.66 -    handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)
1.67 -
1.68 -(*Add a const/type pair to the table, but a [] entry means a standard connective,
1.69 -  which we ignore.*)
1.70 -fun add_const_typ_table ((c,ctyps), tab) =
1.71 -  Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => insert (op =) ctyps ctyps_list)
1.72 -    tab;
1.73 -
1.74 -(*Free variables are included, as well as constants, to handle locales*)
1.75 -fun add_term_consts_typs_rm thy (Const(c, typ), tab) =
1.76 -      add_const_typ_table (const_with_typ thy (c,typ), tab)
1.77 -  | add_term_consts_typs_rm thy (Free(c, typ), tab) =
1.78 -      add_const_typ_table (const_with_typ thy (c,typ), tab)
1.79 -  | add_term_consts_typs_rm thy (t \$ u, tab) =
1.81 -  | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab)
1.82 -  | add_term_consts_typs_rm thy (_, tab) = tab;
1.83 -
1.84 -(*The empty list here indicates that the constant is being ignored*)
1.85 -fun add_standard_const (s,tab) = Symtab.update (s,[]) tab;
1.86 -
1.87 -val null_const_tab : const_typ list list Symtab.table =
1.88 -    foldl add_standard_const Symtab.empty standard_consts;
1.89 -
1.90 -fun get_goal_consts_typs thy = foldl (add_term_consts_typs_rm thy) null_const_tab;
1.91 -
1.92 -(*Inserts a dummy "constant" referring to the theory name, so that relevance
1.93 -  takes the given theory into account.*)
1.94 -fun const_prop_of th =
1.95 - if !theory_const then
1.96 -  let val name = Context.theory_name (theory_of_thm th)
1.97 -      val t = Const (name ^ ". 1", HOLogic.boolT)
1.98 -  in  t \$ prop_of th  end
1.99 - else prop_of th;
1.100 -
1.101 -(**** Constant / Type Frequencies ****)
1.102 -
1.103 -(*A two-dimensional symbol table counts frequencies of constants. It's keyed first by
1.104 -  constant name and second by its list of type instantiations. For the latter, we need
1.105 -  a linear ordering on type const_typ list.*)
1.106 -
1.107 -local
1.108 -
1.109 -fun cons_nr CTVar = 0
1.110 -  | cons_nr (CType _) = 1;
1.111 -
1.112 -in
1.113 -
1.114 -fun const_typ_ord TU =
1.115 -  case TU of
1.116 -    (CType (a, Ts), CType (b, Us)) =>
1.117 -      (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
1.118 -  | (T, U) => int_ord (cons_nr T, cons_nr U);
1.119 -
1.120 -end;
1.121 -
1.122 -structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
1.123 -
1.124 -fun count_axiom_consts thy ((thm,_), tab) =
1.125 -  let fun count_const (a, T, tab) =
1.126 -	let val (c, cts) = const_with_typ thy (a,T)
1.127 -	in  (*Two-dimensional table update. Constant maps to types maps to count.*)
1.128 -	    Symtab.map_default (c, CTtab.empty)
1.129 -	                       (CTtab.map_default (cts,0) (fn n => n+1)) tab
1.130 -	end
1.131 -      fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
1.132 -	| count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
1.133 -	| count_term_consts (t \$ u, tab) =
1.134 -	    count_term_consts (t, count_term_consts (u, tab))
1.135 -	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
1.136 -	| count_term_consts (_, tab) = tab
1.137 -  in  count_term_consts (const_prop_of thm, tab)  end;
1.138 -
1.139 -
1.140 -(**** Actual Filtering Code ****)
1.141 -
1.142 -(*The frequency of a constant is the sum of those of all instances of its type.*)
1.143 -fun const_frequency ctab (c, cts) =
1.144 -  let val pairs = CTtab.dest (the (Symtab.lookup ctab c))
1.145 -      fun add ((cts',m), n) = if match_types cts cts' then m+n else n
1.146 -  in  List.foldl add 0 pairs  end;
1.147 -
1.148 -(*Add in a constant's weight, as determined by its frequency.*)
1.149 -fun add_ct_weight ctab ((c,T), w) =
1.150 -  w + !weight_fn (real (const_frequency ctab (c,T)));
1.151 -
1.152 -(*Relevant constants are weighted according to frequency,
1.153 -  but irrelevant constants are simply counted. Otherwise, Skolem functions,
1.154 -  which are rare, would harm a clause's chances of being picked.*)
1.155 -fun clause_weight ctab gctyps consts_typs =
1.156 -    let val rel = filter (uni_mem gctyps) consts_typs
1.157 -        val rel_weight = List.foldl (add_ct_weight ctab) 0.0 rel
1.158 -    in
1.159 -	rel_weight / (rel_weight + real (length consts_typs - length rel))
1.160 -    end;
1.161 -
1.162 -(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
1.163 -fun add_expand_pairs (x,ys) xys = foldl (fn (y,acc) => (x,y)::acc) xys ys;
1.164 -
1.165 -fun consts_typs_of_term thy t =
1.166 -  let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
1.167 -  in  Symtab.fold add_expand_pairs tab []  end;
1.168 -
1.169 -fun pair_consts_typs_axiom thy (thm,name) =
1.170 -    ((thm,name), (consts_typs_of_term thy (const_prop_of thm)));
1.171 -
1.172 -exception ConstFree;
1.173 -fun dest_ConstFree (Const aT) = aT
1.174 -  | dest_ConstFree (Free aT) = aT
1.175 -  | dest_ConstFree _ = raise ConstFree;
1.176 -
1.177 -(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
1.178 -fun defines thy (thm,(name,n)) gctypes =
1.179 -    let val tm = prop_of thm
1.180 -	fun defs lhs rhs =
1.181 -            let val (rator,args) = strip_comb lhs
1.182 -		val ct = const_with_typ thy (dest_ConstFree rator)
1.183 -            in  forall is_Var args andalso uni_mem gctypes ct andalso
1.185 -            end
1.186 -	    handle ConstFree => false
1.187 -    in
1.188 -	case tm of Const ("Trueprop",_) \$ (Const("op =",_) \$ lhs \$ rhs) =>
1.189 -		   defs lhs rhs andalso
1.190 -		   (Output.debug (fn () => "Definition found: " ^ name ^ "_" ^ Int.toString n); true)
1.191 -		 | _ => false
1.192 -    end;
1.193 -
1.194 -type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
1.195 -
1.196 -(*For a reverse sort, putting the largest values first.*)
1.197 -fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1);
1.198 -
1.199 -(*Limit the number of new clauses, to prevent runaway acceptance.*)
1.200 -fun take_best (newpairs : (annotd_cls*real) list) =
1.201 -  let val nnew = length newpairs
1.202 -  in
1.203 -    if nnew <= !max_new then (map #1 newpairs, [])
1.204 -    else
1.205 -      let val cls = sort compare_pairs newpairs
1.206 -          val accepted = List.take (cls, !max_new)
1.207 -      in
1.208 -        Output.debug (fn () => ("Number of candidates, " ^ Int.toString nnew ^
1.209 -		       ", exceeds the limit of " ^ Int.toString (!max_new)));
1.210 -        Output.debug (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
1.211 -        Output.debug (fn () => "Actually passed: " ^
1.212 -          space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
1.213 -
1.214 -	(map #1 accepted, map #1 (List.drop (cls, !max_new)))
1.215 -      end
1.216 -  end;
1.217 -
1.218 -fun relevant_clauses thy ctab p rel_consts =
1.219 -  let fun relevant ([],_) [] = [] : (thm * (string * int)) list  (*Nothing added this iteration*)
1.220 -	| relevant (newpairs,rejects) [] =
1.221 -	    let val (newrels,more_rejects) = take_best newpairs
1.222 -		val new_consts = List.concat (map #2 newrels)
1.223 -		val rel_consts' = foldl add_const_typ_table rel_consts new_consts
1.224 -		val newp = p + (1.0-p) / !convergence
1.225 -	    in
1.226 -              Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
1.227 -	       (map #1 newrels) @
1.228 -	       (relevant_clauses thy ctab newp rel_consts' (more_rejects@rejects))
1.229 -	    end
1.230 -	| relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
1.231 -	    let val weight = clause_weight ctab rel_consts consts_typs
1.232 -	    in
1.233 -	      if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts)
1.234 -	      then (Output.debug (fn () => (name ^ " clause " ^ Int.toString n ^
1.235 -	                                    " passes: " ^ Real.toString weight));
1.236 -	            relevant ((ax,weight)::newrels, rejects) axs)
1.237 -	      else relevant (newrels, ax::rejects) axs
1.238 -	    end
1.239 -    in  Output.debug (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
1.240 -        relevant ([],[])
1.241 -    end;
1.242 -
1.243 -fun relevance_filter thy axioms goals =
1.244 - if !run_relevance_filter andalso !pass_mark >= 0.1
1.245 - then
1.246 -  let val _ = Output.debug (fn () => "Start of relevance filtering");
1.247 -      val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
1.248 -      val goal_const_tab = get_goal_consts_typs thy goals
1.249 -      val _ = Output.debug (fn () => ("Initial constants: " ^
1.250 -                                 space_implode ", " (Symtab.keys goal_const_tab)));
1.251 -      val rels = relevant_clauses thy const_tab (!pass_mark)
1.252 -                   goal_const_tab  (map (pair_consts_typs_axiom thy) axioms)
1.253 -  in
1.254 -      Output.debug (fn () => ("Total relevant: " ^ Int.toString (length rels)));
1.255 -      rels
1.256 -  end
1.257 - else axioms;
1.258 -
1.259 -end;
```
```     2.1 --- a/src/HOL/Tools/res_atp.ML	Wed Aug 15 12:52:56 2007 +0200
2.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Aug 15 13:50:47 2007 +0200
2.3 @@ -23,6 +23,11 @@
2.4    val include_all: bool ref
2.5    val run_relevance_filter: bool ref
2.6    val run_blacklist_filter: bool ref
2.7 +  val theory_const : bool ref
2.8 +  val pass_mark    : real ref
2.9 +  val convergence  : real ref
2.10 +  val max_new      : int ref
2.11 +  val follow_defs  : bool ref
2.12    val add_all : unit -> unit
2.13    val add_claset : unit -> unit
2.14    val add_simpset : unit -> unit
2.15 @@ -50,22 +55,31 @@
2.16  (********************************************************************)
2.17
2.19 +val run_blacklist_filter = ref true;
2.20  val time_limit = ref 60;
2.21  val prover = ref "";
2.22
2.23 +(*** relevance filter parameters ***)
2.24 +val run_relevance_filter = ref true;
2.25 +val theory_const = ref true;
2.26 +val pass_mark = ref 0.5;
2.27 +val convergence = ref 3.2;    (*Higher numbers allow longer inference chains*)
2.28 +val max_new = ref 60;         (*Limits how many clauses can be picked up per stage*)
2.29 +val follow_defs = ref false;  (*Follow definitions. Makes problems bigger.*)
2.30 +
2.31  fun set_prover atp =
2.32    case String.map Char.toLower atp of
2.33        "e" =>
2.34 -          (ReduceAxiomsN.max_new := 100;
2.35 -           ReduceAxiomsN.theory_const := false;
2.36 +          (max_new := 100;
2.37 +           theory_const := false;
2.38             prover := "E")
2.39      | "spass" =>
2.40 -          (ReduceAxiomsN.max_new := 40;
2.41 -           ReduceAxiomsN.theory_const := true;
2.42 +          (max_new := 40;
2.43 +           theory_const := true;
2.44             prover := "spass")
2.45      | "vampire" =>
2.46 -          (ReduceAxiomsN.max_new := 60;
2.47 -           ReduceAxiomsN.theory_const := false;
2.48 +          (max_new := 60;
2.49 +           theory_const := false;
2.50             prover := "vampire")
2.51      | _ => error ("No such prover: " ^ atp);
2.52
2.53 @@ -108,7 +122,7 @@
2.54  val include_atpset = ref true;
2.55
2.56  (*Tests show that follow_defs gives VERY poor results with "include_all"*)
2.57 -fun add_all() = (include_all:=true; ReduceAxiomsN.follow_defs := false);
2.58 +fun add_all() = (include_all:=true; follow_defs := false);
2.59  fun rm_all() = include_all:=false;
2.60
2.62 @@ -124,10 +138,6 @@
2.63  fun rm_atpset() = include_atpset:=false;
2.64
2.65
2.66 -(**** relevance filter ****)
2.67 -val run_relevance_filter = ReduceAxiomsN.run_relevance_filter;
2.68 -val run_blacklist_filter = ref true;
2.69 -
2.70  (******************************************************************)
2.71  (* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
2.72  (******************************************************************)
2.73 @@ -251,6 +261,251 @@
2.74  fun is_fol_thms ths = ((fst(logic_of_clauses (map prop_of ths) (FOL,[]))) = FOL);
2.75
2.76  (***************************************************************)
2.77 +(* Relevance Filtering                                         *)
2.78 +(***************************************************************)
2.79 +
2.80 +(*A surprising number of theorems contain only a few significant constants.
2.81 +  These include all induction rules, and other general theorems. Filtering
2.82 +  theorems in clause form reveals these complexities in the form of Skolem
2.83 +  functions. If we were instead to filter theorems in their natural form,
2.84 +  some other method of measuring theorem complexity would become necessary.*)
2.85 +
2.86 +fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0);
2.87 +
2.88 +(*The default seems best in practice. A constant function of one ignores
2.89 +  the constant frequencies.*)
2.90 +val weight_fn = ref log_weight2;
2.91 +
2.92 +
2.93 +(*Including equality in this list might be expected to stop rules like subset_antisym from
2.94 +  being chosen, but for some reason filtering works better with them listed. The
2.95 +  logical signs All, Ex, &, and --> are omitted because any remaining occurrrences
2.96 +  must be within comprehensions.*)
2.97 +val standard_consts = ["Trueprop","==>","all","==","op |","Not","op ="];
2.98 +
2.99 +
2.100 +(*** constants with types ***)
2.101 +
2.102 +(*An abstraction of Isabelle types*)
2.103 +datatype const_typ =  CTVar | CType of string * const_typ list
2.104 +
2.105 +(*Is the second type an instance of the first one?*)
2.106 +fun match_type (CType(con1,args1)) (CType(con2,args2)) =
2.107 +      con1=con2 andalso match_types args1 args2
2.108 +  | match_type CTVar _ = true
2.109 +  | match_type _ CTVar = false
2.110 +and match_types [] [] = true
2.111 +  | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
2.112 +
2.113 +(*Is there a unifiable constant?*)
2.114 +fun uni_mem gctab (c,c_typ) =
2.115 +  case Symtab.lookup gctab c of
2.116 +      NONE => false
2.117 +    | SOME ctyps_list => exists (match_types c_typ) ctyps_list;
2.118 +
2.119 +(*Maps a "real" type to a const_typ*)
2.120 +fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs)
2.121 +  | const_typ_of (TFree _) = CTVar
2.122 +  | const_typ_of (TVar _) = CTVar
2.123 +
2.124 +(*Pairs a constant with the list of its type instantiations (using const_typ)*)
2.125 +fun const_with_typ thy (c,typ) =
2.126 +    let val tvars = Sign.const_typargs thy (c,typ)
2.127 +    in (c, map const_typ_of tvars) end
2.128 +    handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)
2.129 +
2.130 +(*Add a const/type pair to the table, but a [] entry means a standard connective,
2.131 +  which we ignore.*)
2.132 +fun add_const_typ_table ((c,ctyps), tab) =
2.133 +  Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => insert (op =) ctyps ctyps_list)
2.134 +    tab;
2.135 +
2.136 +(*Free variables are included, as well as constants, to handle locales*)
2.137 +fun add_term_consts_typs_rm thy (Const(c, typ), tab) =
2.138 +      add_const_typ_table (const_with_typ thy (c,typ), tab)
2.139 +  | add_term_consts_typs_rm thy (Free(c, typ), tab) =
2.140 +      add_const_typ_table (const_with_typ thy (c,typ), tab)
2.141 +  | add_term_consts_typs_rm thy (t \$ u, tab) =
2.143 +  | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab)
2.144 +  | add_term_consts_typs_rm thy (_, tab) = tab;
2.145 +
2.146 +(*The empty list here indicates that the constant is being ignored*)
2.147 +fun add_standard_const (s,tab) = Symtab.update (s,[]) tab;
2.148 +
2.149 +val null_const_tab : const_typ list list Symtab.table =
2.150 +    foldl add_standard_const Symtab.empty standard_consts;
2.151 +
2.152 +fun get_goal_consts_typs thy = foldl (add_term_consts_typs_rm thy) null_const_tab;
2.153 +
2.154 +(*Inserts a dummy "constant" referring to the theory name, so that relevance
2.155 +  takes the given theory into account.*)
2.156 +fun const_prop_of th =
2.157 + if !theory_const then
2.158 +  let val name = Context.theory_name (theory_of_thm th)
2.159 +      val t = Const (name ^ ". 1", HOLogic.boolT)
2.160 +  in  t \$ prop_of th  end
2.161 + else prop_of th;
2.162 +
2.163 +(**** Constant / Type Frequencies ****)
2.164 +
2.165 +(*A two-dimensional symbol table counts frequencies of constants. It's keyed first by
2.166 +  constant name and second by its list of type instantiations. For the latter, we need
2.167 +  a linear ordering on type const_typ list.*)
2.168 +
2.169 +local
2.170 +
2.171 +fun cons_nr CTVar = 0
2.172 +  | cons_nr (CType _) = 1;
2.173 +
2.174 +in
2.175 +
2.176 +fun const_typ_ord TU =
2.177 +  case TU of
2.178 +    (CType (a, Ts), CType (b, Us)) =>
2.179 +      (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
2.180 +  | (T, U) => int_ord (cons_nr T, cons_nr U);
2.181 +
2.182 +end;
2.183 +
2.184 +structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
2.185 +
2.186 +fun count_axiom_consts thy ((thm,_), tab) =
2.187 +  let fun count_const (a, T, tab) =
2.188 +	let val (c, cts) = const_with_typ thy (a,T)
2.189 +	in  (*Two-dimensional table update. Constant maps to types maps to count.*)
2.190 +	    Symtab.map_default (c, CTtab.empty)
2.191 +	                       (CTtab.map_default (cts,0) (fn n => n+1)) tab
2.192 +	end
2.193 +      fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
2.194 +	| count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
2.195 +	| count_term_consts (t \$ u, tab) =
2.196 +	    count_term_consts (t, count_term_consts (u, tab))
2.197 +	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
2.198 +	| count_term_consts (_, tab) = tab
2.199 +  in  count_term_consts (const_prop_of thm, tab)  end;
2.200 +
2.201 +
2.202 +(**** Actual Filtering Code ****)
2.203 +
2.204 +(*The frequency of a constant is the sum of those of all instances of its type.*)
2.205 +fun const_frequency ctab (c, cts) =
2.206 +  let val pairs = CTtab.dest (the (Symtab.lookup ctab c))
2.207 +      fun add ((cts',m), n) = if match_types cts cts' then m+n else n
2.208 +  in  List.foldl add 0 pairs  end;
2.209 +
2.210 +(*Add in a constant's weight, as determined by its frequency.*)
2.211 +fun add_ct_weight ctab ((c,T), w) =
2.212 +  w + !weight_fn (real (const_frequency ctab (c,T)));
2.213 +
2.214 +(*Relevant constants are weighted according to frequency,
2.215 +  but irrelevant constants are simply counted. Otherwise, Skolem functions,
2.216 +  which are rare, would harm a clause's chances of being picked.*)
2.217 +fun clause_weight ctab gctyps consts_typs =
2.218 +    let val rel = filter (uni_mem gctyps) consts_typs
2.219 +        val rel_weight = List.foldl (add_ct_weight ctab) 0.0 rel
2.220 +    in
2.221 +	rel_weight / (rel_weight + real (length consts_typs - length rel))
2.222 +    end;
2.223 +
2.224 +(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
2.225 +fun add_expand_pairs (x,ys) xys = foldl (fn (y,acc) => (x,y)::acc) xys ys;
2.226 +
2.227 +fun consts_typs_of_term thy t =
2.228 +  let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
2.229 +  in  Symtab.fold add_expand_pairs tab []  end;
2.230 +
2.231 +fun pair_consts_typs_axiom thy (thm,name) =
2.232 +    ((thm,name), (consts_typs_of_term thy (const_prop_of thm)));
2.233 +
2.234 +exception ConstFree;
2.235 +fun dest_ConstFree (Const aT) = aT
2.236 +  | dest_ConstFree (Free aT) = aT
2.237 +  | dest_ConstFree _ = raise ConstFree;
2.238 +
2.239 +(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
2.240 +fun defines thy (thm,(name,n)) gctypes =
2.241 +    let val tm = prop_of thm
2.242 +	fun defs lhs rhs =
2.243 +            let val (rator,args) = strip_comb lhs
2.244 +		val ct = const_with_typ thy (dest_ConstFree rator)
2.245 +            in  forall is_Var args andalso uni_mem gctypes ct andalso
2.247 +            end
2.248 +	    handle ConstFree => false
2.249 +    in
2.250 +	case tm of Const ("Trueprop",_) \$ (Const("op =",_) \$ lhs \$ rhs) =>
2.251 +		   defs lhs rhs andalso
2.252 +		   (Output.debug (fn () => "Definition found: " ^ name ^ "_" ^ Int.toString n); true)
2.253 +		 | _ => false
2.254 +    end;
2.255 +
2.256 +type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
2.257 +
2.258 +(*For a reverse sort, putting the largest values first.*)
2.259 +fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1);
2.260 +
2.261 +(*Limit the number of new clauses, to prevent runaway acceptance.*)
2.262 +fun take_best (newpairs : (annotd_cls*real) list) =
2.263 +  let val nnew = length newpairs
2.264 +  in
2.265 +    if nnew <= !max_new then (map #1 newpairs, [])
2.266 +    else
2.267 +      let val cls = sort compare_pairs newpairs
2.268 +          val accepted = List.take (cls, !max_new)
2.269 +      in
2.270 +        Output.debug (fn () => ("Number of candidates, " ^ Int.toString nnew ^
2.271 +		       ", exceeds the limit of " ^ Int.toString (!max_new)));
2.272 +        Output.debug (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
2.273 +        Output.debug (fn () => "Actually passed: " ^
2.274 +          space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
2.275 +
2.276 +	(map #1 accepted, map #1 (List.drop (cls, !max_new)))
2.277 +      end
2.278 +  end;
2.279 +
2.280 +fun relevant_clauses thy ctab p rel_consts =
2.281 +  let fun relevant ([],_) [] = [] : (thm * (string * int)) list  (*Nothing added this iteration*)
2.282 +	| relevant (newpairs,rejects) [] =
2.283 +	    let val (newrels,more_rejects) = take_best newpairs
2.284 +		val new_consts = List.concat (map #2 newrels)
2.285 +		val rel_consts' = foldl add_const_typ_table rel_consts new_consts
2.286 +		val newp = p + (1.0-p) / !convergence
2.287 +	    in
2.288 +              Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
2.289 +	       (map #1 newrels) @
2.290 +	       (relevant_clauses thy ctab newp rel_consts' (more_rejects@rejects))
2.291 +	    end
2.292 +	| relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
2.293 +	    let val weight = clause_weight ctab rel_consts consts_typs
2.294 +	    in
2.295 +	      if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts)
2.296 +	      then (Output.debug (fn () => (name ^ " clause " ^ Int.toString n ^
2.297 +	                                    " passes: " ^ Real.toString weight));
2.298 +	            relevant ((ax,weight)::newrels, rejects) axs)
2.299 +	      else relevant (newrels, ax::rejects) axs
2.300 +	    end
2.301 +    in  Output.debug (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
2.302 +        relevant ([],[])
2.303 +    end;
2.304 +
2.305 +fun relevance_filter thy axioms goals =
2.306 + if !run_relevance_filter andalso !pass_mark >= 0.1
2.307 + then
2.308 +  let val _ = Output.debug (fn () => "Start of relevance filtering");
2.309 +      val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
2.310 +      val goal_const_tab = get_goal_consts_typs thy goals
2.311 +      val _ = Output.debug (fn () => ("Initial constants: " ^
2.312 +                                 space_implode ", " (Symtab.keys goal_const_tab)));
2.313 +      val rels = relevant_clauses thy const_tab (!pass_mark)
2.314 +                   goal_const_tab  (map (pair_consts_typs_axiom thy) axioms)
2.315 +  in
2.316 +      Output.debug (fn () => ("Total relevant: " ^ Int.toString (length rels)));
2.317 +      rels
2.318 +  end
2.319 + else axioms;
2.320 +
2.321 +(***************************************************************)
2.322  (* Retrieving and filtering lemmas                             *)
2.323  (***************************************************************)
2.324
2.325 @@ -320,11 +575,6 @@
2.326        filter (not o known) c_clauses
2.327    end;
2.328
2.329 -(*Filter axiom clauses, but keep supplied clauses and clauses in whitelist.
2.330 -  Duplicates are removed later.*)
2.331 -fun get_relevant_clauses thy cls_thms white_cls goals =
2.332 -  white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
2.333 -
2.334  fun all_valid_thms ctxt =
2.335    let
2.336      fun blacklisted s = !run_blacklist_filter andalso is_package_def s
2.337 @@ -534,7 +784,7 @@
2.338                                       |> restrict_to_logic thy logic
2.339                                       |> remove_unwanted_clauses
2.340          val user_cls = ResAxioms.cnf_rules_pairs user_rules
2.341 -        val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms)
2.342 +        val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms)
2.343          val subs = tfree_classes_of_terms goal_tms
2.344          and axtms = map (prop_of o #1) axclauses
2.345          val supers = tvar_classes_of_terms axtms
2.346 @@ -644,7 +894,7 @@
2.347        val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
2.348        val white_cls = ResAxioms.cnf_rules_pairs white_thms
2.349        (*clauses relevant to goal gl*)
2.350 -      val axcls_list = map (fn ngcls => get_relevant_clauses thy included_cls white_cls (map prop_of ngcls)) goal_cls
2.351 +      val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls
2.352        val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
2.353                    axcls_list
2.354        val writer = if !prover = "spass" then dfg_writer else tptp_writer
```