src/HOL/Tools/ATP/reduce_axiomsN.ML
author haftmann
Tue May 09 10:09:37 2006 +0200 (2006-05-09)
changeset 19599 a5c7eb37d14f
parent 19448 72dab71cb11e
child 20132 de3c295000b2
permissions -rw-r--r--
added DatatypeHooks
     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 convergence = ref 2.4;   (*Higher numbers allow longer inference chains*)
    10 val follow_defs = ref true;  (*Follow definitions. Makes problems bigger.*)
    11 
    12 fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0);
    13 
    14 (*The default seems best in practice. A constant function of one ignores
    15   the constant frequencies.*)
    16 val weight_fn = ref log_weight2;
    17 
    18 
    19 (*Including equality in this list might be expected to stop rules like subset_antisym from
    20   being chosen, but for some reason filtering works better with them listed.*)
    21 val standard_consts =
    22   ["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->",
    23    "op =","==","True","False"];
    24 
    25 
    26 (*** constants with types ***)
    27 
    28 (*An abstraction of Isabelle types*)
    29 datatype const_typ =  CTVar | CType of string * const_typ list
    30 
    31 fun uni_type (CType(con1,args1)) (CType(con2,args2)) = con1=con2 andalso uni_types args1 args2
    32   | uni_type (CType _) CTVar = true
    33   | uni_type CTVar CTVar = true
    34   | uni_type CTVar _ = false
    35 and uni_types [] [] = true
    36   | uni_types (a1::as1) (a2::as2) = uni_type a1 a2 andalso uni_types as1 as2;
    37 
    38 
    39 fun uni_constants (c1,ctp1) (c2,ctp2) = (c1=c2) andalso uni_types ctp1 ctp2;
    40 
    41 fun uni_mem _ [] = false
    42   | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) =
    43       uni_constants (c1,c_typ1) (c,c_typ) orelse uni_mem (c,c_typ) ctyps;
    44 
    45 fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 
    46   | const_typ_of (TFree _) = CTVar
    47   | const_typ_of (TVar _) = CTVar
    48 
    49 
    50 fun const_with_typ thy (c,typ) = 
    51     let val tvars = Sign.const_typargs thy (c,typ)
    52     in (c, map const_typ_of tvars) end
    53     handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)   
    54 
    55 (*Free variables are counted, as well as constants, to handle locales*)
    56 fun add_term_consts_typs_rm thy (Const(c, typ)) cs =
    57       if (c mem standard_consts) then cs 
    58       else const_with_typ thy (c,typ) ins cs   (*suppress multiples*)
    59   | add_term_consts_typs_rm thy (Free(c, typ)) cs =
    60       const_with_typ thy (c,typ) ins cs
    61   | add_term_consts_typs_rm thy (t $ u) cs =
    62       add_term_consts_typs_rm thy t (add_term_consts_typs_rm thy u cs)
    63   | add_term_consts_typs_rm thy (Abs(_,_,t)) cs = add_term_consts_typs_rm thy t cs
    64   | add_term_consts_typs_rm thy _ cs = cs;
    65 
    66 fun consts_typs_of_term thy t = add_term_consts_typs_rm thy t [];
    67 
    68 fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs)
    69 
    70 
    71 (**** Constant / Type Frequencies ****)
    72 
    73 local
    74 
    75 fun cons_nr CTVar = 0
    76   | cons_nr (CType _) = 1;
    77 
    78 in
    79 
    80 fun const_typ_ord TU =
    81   case TU of
    82     (CType (a, Ts), CType (b, Us)) =>
    83       (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
    84   | (T, U) => int_ord (cons_nr T, cons_nr U);
    85 
    86 end;
    87 
    88 structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
    89 
    90 fun count_axiom_consts thy ((thm,_), tab) = 
    91   let fun count_const (a, T, tab) =
    92 	let val (c, cts) = const_with_typ thy (a,T)
    93 	    val cttab = Option.getOpt (Symtab.lookup tab c, CTtab.empty)
    94 	    val n = Option.getOpt (CTtab.lookup cttab cts, 0)
    95 	in 
    96 	    Symtab.update (c, CTtab.update (cts, n+1) cttab) tab
    97 	end
    98       fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
    99 	| count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
   100 	| count_term_consts (t $ u, tab) =
   101 	    count_term_consts (t, count_term_consts (u, tab))
   102 	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
   103 	| count_term_consts (_, tab) = tab
   104   in  count_term_consts (prop_of thm, tab)  end;
   105 
   106 
   107 (******** filter clauses ********)
   108 
   109 fun const_weight ctab (c, cts) =
   110   let val pairs = CTtab.dest (Option.valOf (Symtab.lookup ctab c))
   111       fun add ((cts',m), n) = if uni_types cts cts' then m+n else n
   112   in  List.foldl add 0 pairs  end;
   113 
   114 fun add_ct_weight ctab ((c,T), w) =
   115   w + !weight_fn (real (const_weight ctab (c,T)));
   116 
   117 fun consts_typs_weight ctab =
   118     List.foldl (add_ct_weight ctab) 0.0;
   119 
   120 (*Relevant constants are weighted according to frequency, 
   121   but irrelevant constants are simply counted. Otherwise, Skolem functions,
   122   which are rare, would harm a clause's chances of being picked.*)
   123 fun clause_weight ctab gctyps consts_typs =
   124     let val rel = filter (fn s => uni_mem s gctyps) consts_typs
   125         val rel_weight = consts_typs_weight ctab rel
   126     in
   127 	rel_weight / (rel_weight + real (length consts_typs - length rel))
   128     end;
   129     
   130 fun pair_consts_typs_axiom thy (thm,name) =
   131     ((thm,name), (consts_typs_of_term thy (prop_of thm)));
   132 
   133 exception ConstFree;
   134 fun dest_ConstFree (Const aT) = aT
   135   | dest_ConstFree (Free aT) = aT
   136   | dest_ConstFree _ = raise ConstFree;
   137 
   138 (*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
   139 fun defines thy (thm,(name,n)) gctypes =
   140     let val tm = prop_of thm
   141 	fun defs lhs rhs =
   142             let val (rator,args) = strip_comb lhs
   143 		val ct = const_with_typ thy (dest_ConstFree rator)
   144             in  forall is_Var args andalso uni_mem ct gctypes andalso
   145                 term_varnames rhs subset term_varnames lhs
   146             end
   147 	    handle ConstFree => false
   148     in    
   149 	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 
   150 		   defs lhs rhs andalso
   151 		   (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true)
   152 		 | _ => false
   153     end
   154 
   155 fun relevant_clauses thy ctab p rel_consts =
   156   let fun relevant (newrels,rejects) []  =
   157 	    if null newrels then [] 
   158 	    else 
   159 	      let val new_consts = map #2 newrels
   160 	          val rel_consts' = foldl (op union) rel_consts new_consts
   161                   val newp = p + (1.0-p) / !convergence
   162 	      in Output.debug ("found relevant: " ^ Int.toString (length newrels));
   163                  newrels @ relevant_clauses thy ctab newp rel_consts' rejects
   164 	      end
   165 	| relevant (newrels,rejects) ((ax as (clsthm,consts_typs)) :: axs) =
   166 	    let val weight = clause_weight ctab rel_consts consts_typs
   167 	    in
   168 	      if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts)
   169 	      then relevant (ax::newrels, rejects) axs
   170 	      else relevant (newrels, ax::rejects) axs
   171 	    end
   172     in  Output.debug ("relevant_clauses: " ^ Real.toString p);
   173         relevant ([],[]) end;
   174 	
   175      
   176 fun relevance_filter_aux thy axioms goals = 
   177   let val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
   178       val goals_consts_typs = get_goal_consts_typs thy goals
   179       val rels = relevant_clauses thy const_tab (!pass_mark) goals_consts_typs 
   180                    (map (pair_consts_typs_axiom thy) axioms)
   181   in
   182       Output.debug ("Total relevant: " ^ Int.toString (length rels));
   183       rels
   184   end;
   185 
   186 fun relevance_filter thy axioms goals =
   187   if !pass_mark < 0.1 then axioms
   188   else map #1 (relevance_filter_aux thy axioms goals);
   189     
   190 
   191 end;