combining the relevance filter with res_atp
authorpaulson
Wed Aug 15 13:50:47 2007 +0200 (2007-08-15)
changeset 24287c857dac06da6
parent 24286 7619080e49f0
child 24288 4016baca4973
combining the relevance filter with res_atp
src/HOL/Tools/ATP/reduce_axiomsN.ML
src/HOL/Tools/res_atp.ML
     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.80 -      add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (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.184 -                Term.add_vars rhs [] subset Term.add_vars lhs []
   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.18  (*** background linkup ***)
    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.61  fun add_simpset() = include_simpset:=true;
    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.142 +      add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (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.246 +                Term.add_vars rhs [] subset Term.add_vars lhs []
   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