src/HOL/Tools/ATP/reduce_axiomsN.ML
author paulson
Tue Mar 28 16:48:18 2006 +0200 (2006-03-28)
changeset 19334 96ca738055a6
parent 19321 30b5bb35dd33
child 19335 9e82f341a71b
permissions -rw-r--r--
Simplified version of Jia's filter. Now all constants are pooled, rather than
relevance being compared against separate clauses. Rejects are no longer noted,
and units cannot be added at the end.
     1 (* Authors: Jia Meng, NICTA and Lawrence C Paulson, Cambridge University Computer Laboratory
     2    ID: $Id$
     3    Filtering strategies *)
     4 
     5 structure ReduceAxiomsN =
     6 struct
     7 
     8 val pass_mark = ref 0.6;
     9 val reduction_factor = ref 1.0;
    10 val convergence = ref 4.0;   (*Higher numbers allow longer inference chains*)
    11 
    12 (*FIXME DELETE Whether all "simple" unit clauses should be included*)
    13 val add_unit = ref false;
    14 val unit_pass_mark = ref 0.0;
    15 
    16 (*The default ignores the constant-count and gives the old Strategy 3*)
    17 val weight_fn = ref (fn x : real => 1.0);
    18 
    19 
    20 (*Including equality in this list might be expected to stop rules like subset_antisym from
    21   being chosen, but for some reason filtering works better with them listed.*)
    22 val standard_consts =
    23   ["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->",
    24    "op =","==","True","False"];
    25 
    26 
    27 (*** unit clauses ***)
    28 datatype clause_kind = Unit_neq | Unit_geq | Other
    29 
    30 
    31 fun literals_of_term args (Const ("Trueprop",_) $ P) = literals_of_term args P
    32   | literals_of_term args (Const ("op |",_) $ P $ Q) = 
    33     literals_of_term (literals_of_term args P) Q
    34   | literals_of_term args P = P::args;
    35 
    36 fun is_ground t = (term_vars t = []) andalso (term_frees t = []);
    37 
    38 fun eq_clause_type (P,Q) = 
    39     if ((is_ground P) orelse (is_ground Q)) then Unit_geq else Other;
    40 
    41 fun unit_clause_type (Const ("op =",_) $ P $ Q) = eq_clause_type (P,Q)
    42   | unit_clause_type _ = Unit_neq;
    43 
    44 fun clause_kind tm = 
    45     case literals_of_term [] tm of
    46         [lit] => unit_clause_type lit
    47       | _ => Other;
    48 
    49 (*** constants with types ***)
    50 
    51 (*An abstraction of Isabelle types*)
    52 datatype const_typ =  CTVar | CType of string * const_typ list
    53 
    54 fun uni_type (CType(con1,args1)) (CType(con2,args2)) = con1=con2 andalso uni_types args1 args2
    55   | uni_type (CType _) CTVar = true
    56   | uni_type CTVar CTVar = true
    57   | uni_type CTVar _ = false
    58 and uni_types [] [] = true
    59   | uni_types (a1::as1) (a2::as2) = uni_type a1 a2 andalso uni_types as1 as2;
    60 
    61 
    62 fun uni_constants (c1,ctp1) (c2,ctp2) = (c1=c2) andalso uni_types ctp1 ctp2;
    63 
    64 fun uni_mem _ [] = false
    65   | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) =
    66       uni_constants (c1,c_typ1) (c,c_typ) orelse uni_mem (c,c_typ) ctyps;
    67 
    68 fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 
    69   | const_typ_of (TFree _) = CTVar
    70   | const_typ_of (TVar _) = CTVar
    71 
    72 
    73 fun const_with_typ thy (c,typ) = 
    74     let val tvars = Sign.const_typargs thy (c,typ)
    75     in (c, map const_typ_of tvars) end
    76     handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)   
    77 
    78 (*Free variables are counted, as well as constants, to handle locales*)
    79 fun add_term_consts_typs_rm thy (Const(c, typ)) cs =
    80       if (c mem standard_consts) then cs 
    81       else const_with_typ thy (c,typ) ins cs
    82   | add_term_consts_typs_rm thy (Free(c, typ)) cs =
    83       const_with_typ thy (c,typ) ins cs
    84   | add_term_consts_typs_rm thy (t $ u) cs =
    85       add_term_consts_typs_rm thy t (add_term_consts_typs_rm thy u cs)
    86   | add_term_consts_typs_rm thy (Abs(_,_,t)) cs = add_term_consts_typs_rm thy t cs
    87   | add_term_consts_typs_rm thy _ cs = cs;
    88 
    89 fun consts_typs_of_term thy t = add_term_consts_typs_rm thy t [];
    90 
    91 fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs)
    92 
    93 
    94 (**** Constant / Type Frequencies ****)
    95 
    96 local
    97 
    98 fun cons_nr CTVar = 0
    99   | cons_nr (CType _) = 1;
   100 
   101 in
   102 
   103 fun const_typ_ord TU =
   104   case TU of
   105     (CType (a, Ts), CType (b, Us)) =>
   106       (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
   107   | (T, U) => int_ord (cons_nr T, cons_nr U);
   108 
   109 end;
   110 
   111 structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
   112 
   113 fun count_axiom_consts thy ((t,_), tab) = 
   114   let fun count_const (a, T, tab) =
   115 	let val (c, cts) = const_with_typ thy (a,T)
   116 	    val cttab = Option.getOpt (Symtab.lookup tab c, CTtab.empty)
   117 	    val n = Option.getOpt (CTtab.lookup cttab cts, 0)
   118 	in 
   119 	    Symtab.update (c, CTtab.update (cts, n+1) cttab) tab
   120 	end
   121       fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
   122 	| count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
   123 	| count_term_consts (t $ u, tab) =
   124 	    count_term_consts (t, count_term_consts (u, tab))
   125 	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
   126 	| count_term_consts (_, tab) = tab
   127   in  count_term_consts (t, tab)  end;
   128 
   129 
   130 (******** filter clauses ********)
   131 
   132 fun const_weight ctab (c, cts) =
   133   let val pairs = CTtab.dest (Option.valOf (Symtab.lookup ctab c))
   134       fun add ((cts',m), n) = if uni_types cts cts' then m+n else n
   135   in  List.foldl add 0 pairs  end;
   136 
   137 fun add_ct_weight ctab ((c,T), w) =
   138   w + !weight_fn (real (const_weight ctab (c,T)));
   139 
   140 fun consts_typs_weight ctab =
   141     List.foldl (add_ct_weight ctab) 0.0;
   142 
   143 (*Relevant constants are weighted according to frequency, 
   144   but irrelevant constants are simply counted. Otherwise, Skolem functions,
   145   which are rare, would harm a clause's chances of being picked.*)
   146 fun clause_weight ctab gctyps consts_typs =
   147     let val rel = filter (fn s => uni_mem s gctyps) consts_typs
   148         val rel_weight = consts_typs_weight ctab rel
   149     in
   150 	rel_weight / (rel_weight + real (length consts_typs - length rel))
   151     end;
   152     
   153 fun pair_consts_typs_axiom thy (tm,name) =
   154     ((tm,name), (consts_typs_of_term thy tm));
   155 
   156 fun relevant_clauses ctab p rel_consts =
   157   let fun relevant (newrels,rejects) []  =
   158 	    if null newrels then [] 
   159 	    else 
   160 	      let val new_consts = map #2 newrels
   161 	          val rel_consts' = foldl (op union) rel_consts new_consts
   162                   val newp = p + (1.0-p) / !convergence
   163 	      in Output.debug ("found relevant: " ^ Int.toString (length newrels));
   164                  newrels @ relevant_clauses ctab newp rel_consts' rejects
   165 	      end
   166 	| relevant (newrels,rejects) ((ax as (clstm,consts_typs)) :: axs) =
   167 	    let val weight = clause_weight ctab rel_consts consts_typs
   168 	    in
   169 	      if p <= weight 
   170 	      then relevant (ax::newrels, rejects) axs
   171 	      else relevant (newrels, ax::rejects) axs
   172 	    end
   173     in  Output.debug ("relevant_clauses: " ^ Real.toString p);
   174         relevant ([],[]) end;
   175 
   176 (*Unit clauses other than non-trivial equations can be included subject to
   177   a separate (presumably lower) mark. *)
   178 fun good_unit_clause ((t,_), (_,w)) = 
   179      !unit_pass_mark <= w andalso
   180      (case clause_kind t of
   181 	  Unit_neq => true
   182 	| Unit_geq => true
   183 	| Other => false);
   184 	
   185 fun showconst (c,cttab) = 
   186       List.app (fn n => Output.debug (Int.toString n ^ " occurrences of " ^ c))
   187 	        (map #2 (CTtab.dest cttab))
   188 	      
   189 exception ConstFree;
   190 fun dest_ConstFree (Const aT) = aT
   191   | dest_ConstFree (Free aT) = aT
   192   | dest_ConstFree _ = raise ConstFree;
   193 
   194 (*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
   195 fun defines thy (tm,(name,n)) gctypes =
   196   let fun defs hs =
   197         let val (rator,args) = strip_comb hs
   198             val ct = const_with_typ thy (dest_ConstFree rator)
   199         in  forall is_Var args andalso uni_mem ct gctypes  end
   200         handle ConstFree => false
   201   in    
   202     case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ _) => 
   203           defs lhs andalso
   204           (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true)
   205       | _ => false
   206   end
   207 
   208 fun relevance_filter_aux thy axioms goals = 
   209   let val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
   210       val goals_consts_typs = get_goal_consts_typs thy goals
   211       val rels = relevant_clauses const_tab (!pass_mark) goals_consts_typs 
   212                    (map (pair_consts_typs_axiom thy) axioms)
   213   in
   214       Output.debug ("Total relevant: " ^ Int.toString (length rels));
   215       rels
   216   end;
   217 
   218 fun relevance_filter thy axioms goals =
   219   map #1 (relevance_filter_aux thy axioms goals);
   220     
   221 
   222 end;