src/HOL/Tools/ATP/reduce_axiomsN.ML
author paulson
Sat Jul 15 15:26:50 2006 +0200 (2006-07-15)
changeset 20132 de3c295000b2
parent 19448 72dab71cb11e
child 20153 6ff5d35749b0
permissions -rw-r--r--
Replaced a-lists by tables to improve efficiency
     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 (*Is there a unifiable constant?*)
    39 fun uni_mem gctab (c,c_typ) =
    40   case Symtab.lookup gctab c of
    41       NONE => false
    42     | SOME ctyps_list => exists (uni_types c_typ) ctyps_list;
    43   
    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 fun add_const_typ_table ((c,ctyps), tab) =
    56   case Symtab.lookup tab c of
    57       NONE => Symtab.update (c, [ctyps]) tab
    58     | SOME [] => tab  (*ignore!*)
    59     | SOME ctyps_list => Symtab.update (c, ctyps ins ctyps_list) tab;
    60 
    61 (*Free variables are counted, as well as constants, to handle locales*)
    62 fun add_term_consts_typs_rm thy (Const(c, typ), tab) =
    63       add_const_typ_table (const_with_typ thy (c,typ), tab) 
    64   | add_term_consts_typs_rm thy (Free(c, typ), tab) =
    65       add_const_typ_table (const_with_typ thy (c,typ), tab) 
    66   | add_term_consts_typs_rm thy (t $ u, tab) =
    67       add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab))
    68   | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab)
    69   | add_term_consts_typs_rm thy (_, tab) = tab;
    70 
    71 (*The empty list here indicates that the constant is being ignored*)
    72 fun add_standard_const (s,tab) = Symtab.update (s,[]) tab;
    73 
    74 val null_const_tab : const_typ list list Symtab.table = 
    75     foldl add_standard_const Symtab.empty standard_consts;
    76 
    77 fun get_goal_consts_typs thy cs = foldl (add_term_consts_typs_rm thy) null_const_tab cs;
    78 
    79 
    80 (**** Constant / Type Frequencies ****)
    81 
    82 local
    83 
    84 fun cons_nr CTVar = 0
    85   | cons_nr (CType _) = 1;
    86 
    87 in
    88 
    89 fun const_typ_ord TU =
    90   case TU of
    91     (CType (a, Ts), CType (b, Us)) =>
    92       (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
    93   | (T, U) => int_ord (cons_nr T, cons_nr U);
    94 
    95 end;
    96 
    97 structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
    98 
    99 fun count_axiom_consts thy ((thm,_), tab) = 
   100   let fun count_const (a, T, tab) =
   101 	let val (c, cts) = const_with_typ thy (a,T)
   102 	    val cttab = Option.getOpt (Symtab.lookup tab c, CTtab.empty)
   103 	    val n = Option.getOpt (CTtab.lookup cttab cts, 0)
   104 	in 
   105 	    Symtab.update (c, CTtab.update (cts, n+1) cttab) tab
   106 	end
   107       fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
   108 	| count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
   109 	| count_term_consts (t $ u, tab) =
   110 	    count_term_consts (t, count_term_consts (u, tab))
   111 	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
   112 	| count_term_consts (_, tab) = tab
   113   in  count_term_consts (prop_of thm, tab)  end;
   114 
   115 
   116 (******** filter clauses ********)
   117 
   118 fun const_weight ctab (c, cts) =
   119   let val pairs = CTtab.dest (Option.valOf (Symtab.lookup ctab c))
   120       fun add ((cts',m), n) = if uni_types cts cts' then m+n else n
   121   in  List.foldl add 0 pairs  end;
   122 
   123 fun add_ct_weight ctab ((c,T), w) =
   124   w + !weight_fn (real (const_weight ctab (c,T)));
   125 
   126 fun consts_typs_weight ctab =
   127     List.foldl (add_ct_weight ctab) 0.0;
   128 
   129 (*Relevant constants are weighted according to frequency, 
   130   but irrelevant constants are simply counted. Otherwise, Skolem functions,
   131   which are rare, would harm a clause's chances of being picked.*)
   132 fun clause_weight ctab gctyps consts_typs =
   133     let val rel = filter (uni_mem gctyps) consts_typs
   134         val rel_weight = consts_typs_weight ctab rel
   135     in
   136 	rel_weight / (rel_weight + real (length consts_typs - length rel))
   137     end;
   138     
   139 fun add_consts_with_typs (c,[]) cpairs = cpairs
   140   | add_consts_with_typs (c, ctyps_list) cpairs =
   141       foldl (fn (ctyps,cpairs) => (c,ctyps)::cpairs) cpairs ctyps_list;
   142 
   143 fun consts_typs_of_term thy t = 
   144   let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
   145   in  Symtab.fold add_consts_with_typs tab []  end;
   146 
   147 fun pair_consts_typs_axiom thy (thm,name) =
   148     ((thm,name), (consts_typs_of_term thy (prop_of thm)));
   149 
   150 exception ConstFree;
   151 fun dest_ConstFree (Const aT) = aT
   152   | dest_ConstFree (Free aT) = aT
   153   | dest_ConstFree _ = raise ConstFree;
   154 
   155 (*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
   156 fun defines thy (thm,(name,n)) gctypes =
   157     let val tm = prop_of thm
   158 	fun defs lhs rhs =
   159             let val (rator,args) = strip_comb lhs
   160 		val ct = const_with_typ thy (dest_ConstFree rator)
   161             in  forall is_Var args andalso 
   162                 term_varnames rhs subset term_varnames lhs andalso
   163                 uni_mem gctypes ct 
   164             end
   165 	    handle ConstFree => false
   166     in    
   167 	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 
   168 		   defs lhs rhs andalso
   169 		   (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true)
   170 		 | _ => false
   171     end;
   172 
   173 fun relevant_clauses thy ctab p rel_consts =
   174   let fun relevant (newrels,rejects) []  =
   175 	    if null newrels then [] 
   176 	    else 
   177 	      let val new_consts = List.concat (map #2 newrels)
   178 	          val rel_consts' = foldl add_const_typ_table rel_consts new_consts
   179                   val newp = p + (1.0-p) / !convergence
   180 	      in Output.debug ("found relevant: " ^ Int.toString (length newrels));
   181                  newrels @ relevant_clauses thy ctab newp rel_consts' rejects
   182 	      end
   183 	| relevant (newrels,rejects) ((ax as (clsthm,consts_typs)) :: axs) =
   184 	    let val weight = clause_weight ctab rel_consts consts_typs
   185 	    in
   186 	      if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts)
   187 	      then relevant (ax::newrels, rejects) axs
   188 	      else relevant (newrels, ax::rejects) axs
   189 	    end
   190     in  Output.debug ("relevant_clauses: " ^ Real.toString p);
   191         relevant ([],[]) end;
   192 	
   193      
   194 fun relevance_filter_aux thy axioms goals = 
   195   let val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
   196       val goals_consts_typs = get_goal_consts_typs thy goals
   197       val rels = relevant_clauses thy const_tab (!pass_mark) goals_consts_typs 
   198                    (map (pair_consts_typs_axiom thy) axioms)
   199   in
   200       Output.debug ("Total relevant: " ^ Int.toString (length rels));
   201       rels
   202   end;
   203 
   204 fun relevance_filter thy axioms goals =
   205   if !pass_mark < 0.1 then axioms
   206   else map #1 (relevance_filter_aux thy axioms goals);
   207     
   208 
   209 end;