src/HOL/Tools/ATP/reduce_axiomsN.ML
author paulson
Wed Mar 08 10:19:57 2006 +0100 (2006-03-08)
changeset 19212 ec53c138277a
parent 19208 3e8006cbc925
child 19231 c8879dd3a953
permissions -rw-r--r--
Frequency strategy. Revised indentation, etc.
     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.5;
     9 val strategy = ref 1;
    10 
    11 fun pol_to_int true = 1
    12   | pol_to_int false = ~1;
    13 
    14 fun part refs [] (s1,s2) = (s1,s2)
    15   | part refs (s::ss) (s1,s2) = 
    16       if (s mem refs) then part refs ss (s::s1,s2) else part refs ss (s1,s::s2);
    17 
    18 
    19 fun pol_mem _ [] = false
    20   | pol_mem (pol,const) ((p,c)::pcs) =
    21       (pol = not p andalso const = c) orelse pol_mem (pol,const) pcs;
    22 
    23 
    24 fun part_w_pol refs [] (s1,s2) = (s1,s2)
    25   | part_w_pol refs (s::ss) (s1,s2) =
    26       if (pol_mem s refs) then part_w_pol refs ss (s::s1,s2) 
    27       else part_w_pol refs ss (s1,s::s2);
    28 
    29 
    30 fun add_term_consts_rm ncs (Const(c, _)) cs =
    31       if (c mem ncs) then cs else (c ins_string cs)
    32   | add_term_consts_rm ncs (t $ u) cs =
    33       add_term_consts_rm ncs t (add_term_consts_rm ncs u cs)
    34   | add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs
    35   | add_term_consts_rm ncs _ cs = cs;
    36 
    37 fun term_consts_rm ncs t = add_term_consts_rm ncs t [];
    38 
    39 val standard_consts =
    40   ["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->","op =","==","True","False"];
    41 
    42 val consts_of_term = term_consts_rm standard_consts;
    43 
    44 
    45 fun add_term_pconsts_rm ncs (Const(c,_)) pol cs = if c mem ncs then cs else ((pol,c) ins cs)
    46   | add_term_pconsts_rm ncs (Const("Not",_)$P) pol cs = add_term_pconsts_rm ncs P (not pol) cs
    47   | add_term_pconsts_rm ncs (P$Q) pol cs = 
    48     add_term_pconsts_rm ncs P pol (add_term_pconsts_rm ncs Q pol cs)
    49   | add_term_pconsts_rm ncs (Abs(_,_,t)) pol cs = add_term_pconsts_rm ncs t pol cs
    50   | add_term_pconsts_rm ncs _ _ cs = cs;
    51 
    52 
    53 fun term_pconsts_rm ncs t = add_term_pconsts_rm ncs t true [];
    54 
    55 val pconsts_of_term = term_pconsts_rm standard_consts;
    56 
    57 fun consts_in_goal goal = consts_of_term goal;
    58 fun get_goal_consts cs = foldl (op union_string) [] (map consts_in_goal cs);
    59 
    60 fun pconsts_in_goal goal = pconsts_of_term goal;
    61 fun get_goal_pconsts cs = foldl (op union) [] (map pconsts_in_goal cs);
    62 
    63 
    64 (*************************************************************************)
    65 (*            the first relevance filtering strategy                     *)
    66 (*************************************************************************)
    67 
    68 fun find_clause_weight_s_1 (refconsts : string list) consts wa = 
    69     let val (rel,irrel) = part refconsts consts ([],[])
    70     in
    71 	(real (length rel) / real (length consts)) * wa
    72     end;
    73 
    74 fun find_clause_weight_m_1 [] (_,w) = w 
    75   | find_clause_weight_m_1 ((_,(refconsts,wa))::y) (consts,w) =
    76       let val w' = find_clause_weight_s_1 refconsts consts wa
    77       in
    78 	if w < w' then find_clause_weight_m_1 y (consts,w')
    79 	else find_clause_weight_m_1 y (consts,w)
    80       end;
    81 
    82 
    83 fun relevant_clauses_ax_g_1 _ []  _ (ax,r) = (ax,r)
    84   | relevant_clauses_ax_g_1 gconsts  ((clstm,(consts,_))::y) P (ax,r) =
    85       let val weight = find_clause_weight_s_1 gconsts consts 1.0
    86       in
    87 	if  P <= weight 
    88 	then relevant_clauses_ax_g_1 gconsts y P ((clstm,(consts,weight))::ax,r)
    89 	else relevant_clauses_ax_g_1 gconsts y P (ax,(clstm,(consts,weight))::r)
    90       end;
    91 
    92 
    93 fun relevant_clauses_ax_1 rel_axs  [] P (addc,tmpc) keep = 
    94     (case addc of [] => rel_axs @ keep
    95 		| _ => case tmpc of [] => addc @ rel_axs @ keep
    96 				  | _ => relevant_clauses_ax_1 addc tmpc P ([],[]) (rel_axs @ keep))
    97   | relevant_clauses_ax_1 rel_axs ((clstm,(consts,weight))::e_axs) P (addc,tmpc) keep = 
    98       let val weight' = find_clause_weight_m_1 rel_axs (consts,weight) 
    99 	  val e_ax' = (clstm,(consts, weight'))
   100       in
   101 	if P <= weight' 
   102 	then relevant_clauses_ax_1 rel_axs e_axs P ((clstm,(consts,weight'))::addc,tmpc) keep
   103 	else relevant_clauses_ax_1 rel_axs e_axs P (addc,(clstm,(consts,weight'))::tmpc) keep 
   104       end;
   105 
   106 
   107 fun initialize [] ax_weights = ax_weights
   108   | initialize ((tm,name)::tms_names) ax_weights =
   109       let val consts = consts_of_term tm
   110       in
   111 	  initialize tms_names (((tm,name),(consts,0.0))::ax_weights)
   112       end;
   113 
   114 fun relevance_filter1_aux axioms goals = 
   115     let val pass = !pass_mark
   116 	val axioms_weights = initialize axioms []
   117 	val goals_consts = get_goal_consts goals
   118 	val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_1 goals_consts axioms_weights pass ([],[]) 
   119     in
   120 	relevant_clauses_ax_1 rel_clauses nrel_clauses pass ([],[]) []
   121     end;
   122 
   123 fun relevance_filter1 axioms goals = map fst (relevance_filter1_aux axioms goals);
   124 
   125 
   126 (*************************************************************************)
   127 (*            the second relevance filtering strategy                    *)
   128 (*************************************************************************)
   129 
   130 fun find_clause_weight_s_2 (refpconsts : (bool * string) list) pconsts wa = 
   131     let val (rel,irrel) = part_w_pol refpconsts pconsts ([],[])
   132     in
   133 	((real (length rel))/(real (length pconsts))) * wa
   134     end;
   135 
   136 fun find_clause_weight_m_2 [] (_,w) = w 
   137   | find_clause_weight_m_2 ((_,(refpconsts,wa))::y) (pconsts,w) =
   138     let val w' = find_clause_weight_s_2 refpconsts pconsts wa
   139     in
   140 	if (w < w') then find_clause_weight_m_2 y (pconsts,w')
   141 	else find_clause_weight_m_2 y (pconsts,w)
   142     end;
   143 
   144 
   145 fun relevant_clauses_ax_g_2 _ []  _ (ax,r) = (ax,r)
   146   | relevant_clauses_ax_g_2 gpconsts  ((clstm,(pconsts,_))::y) P (ax,r) =
   147     let val weight = find_clause_weight_s_2 gpconsts pconsts 1.0
   148     in
   149 	if  P <= weight then relevant_clauses_ax_g_2 gpconsts y P ((clstm,(pconsts,weight))::ax,r)
   150 	else relevant_clauses_ax_g_2 gpconsts y P (ax,(clstm,(pconsts,weight))::r)
   151     end;
   152 
   153 
   154 fun relevant_clauses_ax_2 rel_axs  [] P (addc,tmpc) keep = 
   155     (case addc of [] => rel_axs @ keep
   156 		| _ => case tmpc of [] => addc @ rel_axs @ keep
   157 				  | _ => relevant_clauses_ax_2 addc tmpc P ([],[]) (rel_axs @ keep))
   158   | relevant_clauses_ax_2 rel_axs ((clstm,(pconsts,weight))::e_axs) P (addc,tmpc) keep = 
   159     let val weight' = find_clause_weight_m_2 rel_axs (pconsts,weight) 
   160 	val e_ax' = (clstm,(pconsts, weight'))
   161     in
   162 	
   163 	if P <= weight' then relevant_clauses_ax_2 rel_axs e_axs P ((clstm,(pconsts,weight'))::addc,tmpc) keep
   164 	else relevant_clauses_ax_2 rel_axs e_axs P (addc,(clstm,(pconsts,weight'))::tmpc) keep 
   165     end;
   166 
   167 
   168 fun initialize_w_pol [] ax_weights = ax_weights
   169   | initialize_w_pol ((tm,name)::tms_names) ax_weights =
   170     let val consts = pconsts_of_term tm
   171     in
   172 	initialize_w_pol tms_names (((tm,name),(consts,0.0))::ax_weights)
   173     end;
   174 
   175 
   176 fun relevance_filter2_aux axioms goals = 
   177     let val pass = !pass_mark
   178 	val axioms_weights = initialize_w_pol axioms []
   179 	val goals_consts = get_goal_pconsts goals
   180 	val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_2 goals_consts axioms_weights pass ([],[]) 
   181     in
   182 	relevant_clauses_ax_2 rel_clauses nrel_clauses pass ([],[]) []
   183     end;
   184 
   185 fun relevance_filter2 axioms goals = map fst (relevance_filter2_aux axioms goals);
   186 
   187 (******************************************************************)
   188 (*       the third relevance filtering strategy                   *)
   189 (******************************************************************)
   190 
   191 (*** unit clauses ***)
   192 datatype clause_type = Unit_neq | Unit_geq | Other
   193 
   194 (*Whether all "simple" unit clauses should be included*)
   195 val add_unit = ref true;
   196 
   197 fun literals_of_term args (Const ("Trueprop",_) $ P) = literals_of_term args P
   198   | literals_of_term args (Const ("op |",_) $ P $ Q) = 
   199     literals_of_term (literals_of_term args P) Q
   200   | literals_of_term args P = P::args;
   201 
   202 fun is_ground t = (term_vars t = []) andalso (term_frees t = []);
   203 
   204 fun eq_clause_type (P,Q) = 
   205     if ((is_ground P) orelse (is_ground Q)) then Unit_geq else Other;
   206 
   207 fun unit_clause_type (Const ("op =",_) $ P $ Q) = eq_clause_type (P,Q)
   208   | unit_clause_type _ = Unit_neq;
   209 
   210 fun clause_type tm = 
   211     case literals_of_term [] tm of
   212         [lit] => unit_clause_type lit
   213       | _ => Other;
   214 
   215 (*** constants with types ***)
   216 
   217 datatype const_typ =  CTVar | CType of string * const_typ list
   218 
   219 fun uni_type (CType(con1,args1)) (CType(con2,args2)) = con1=con2 andalso uni_types args1 args2
   220   | uni_type (CType _) CTVar = true
   221   | uni_type CTVar CTVar = true
   222   | uni_type CTVar _ = false
   223 and uni_types [] [] = true
   224   | uni_types (a1::as1) (a2::as2) = uni_type a1 a2 andalso uni_types as1 as2;
   225 
   226 
   227 fun uni_constants (c1,ctp1) (c2,ctp2) = (c1 = c2) andalso (uni_types ctp1 ctp2);
   228 
   229 fun uni_mem _ [] = false
   230   | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) =
   231       uni_constants (c1,c_typ1) (c,c_typ) orelse uni_mem (c,c_typ) ctyps;
   232 
   233 fun const_typ_of (Type (c,typs)) = CType (c,map const_typ_of typs) 
   234   | const_typ_of (TFree(_,_)) = CTVar
   235   | const_typ_of (TVar(_,_)) = CTVar
   236 
   237 
   238 fun const_w_typ thy (c,typ) = 
   239     let val tvars = Sign.const_typargs thy (c,typ)
   240     in (c, map const_typ_of tvars) end;
   241 
   242 fun add_term_consts_typs_rm thy ncs (Const(c, typ)) cs =
   243       if (c mem ncs) then cs else (const_w_typ thy (c,typ) ins cs)
   244   | add_term_consts_typs_rm thy ncs (t $ u) cs =
   245       add_term_consts_typs_rm thy ncs  t (add_term_consts_typs_rm thy ncs u cs)
   246   | add_term_consts_typs_rm thy ncs (Abs(_,_,t)) cs = add_term_consts_typs_rm thy ncs t cs
   247   | add_term_consts_typs_rm thy ncs _ cs = cs;
   248 
   249 fun term_consts_typs_rm thy ncs t = add_term_consts_typs_rm thy ncs t [];
   250 
   251 fun consts_typs_of_term thy = term_consts_typs_rm thy standard_consts;
   252 
   253 fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs)
   254 
   255 fun lookup_or_zero (c,tab) =
   256     case Symtab.lookup tab c of
   257         NONE => 0
   258       | SOME n => n
   259 
   260 fun count_term_consts (Const(c,_), tab) =
   261       Symtab.update (c, 1 + lookup_or_zero (c,tab)) tab
   262   | count_term_consts (t $ u, tab) =
   263       count_term_consts (t, count_term_consts (u, tab))
   264   | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
   265   | count_term_consts (_, tab) = tab;
   266 
   267 fun count_axiom_consts ((tm,_), tab) = count_term_consts (tm, tab);
   268 
   269 
   270 (******** filter clauses ********)
   271 
   272 (*The default ignores the constant-count and gives the old Strategy 3*)
   273 val weight_fn = ref (fn x : real => 1.0);
   274 
   275 fun add_ct_weight ctab ((c,_), w) =
   276   w + !weight_fn (100.0 / real (Option.valOf (Symtab.lookup ctab c)));
   277 
   278 fun consts_typs_weight ctab =
   279     List.foldl (add_ct_weight ctab) 0.0;
   280 
   281 fun clause_weight_s_3 ctab gctyps consts_typs =
   282     let val rel = filter (fn s => uni_mem s gctyps) consts_typs
   283     in
   284 	(consts_typs_weight ctab rel) / (consts_typs_weight ctab consts_typs)
   285     end;
   286 
   287 fun find_clause_weight_s_3_alt ctab consts_typs (_,(refconsts_typs,wa)) =
   288     wa * clause_weight_s_3 ctab refconsts_typs consts_typs;
   289 
   290 fun relevant_clauses_ax_3 ctab rel_axs [] P (addc,tmpc) keep =
   291       if null addc orelse null tmpc 
   292       then (addc @ rel_axs @ keep, tmpc)   (*termination!*)
   293       else relevant_clauses_ax_3 ctab addc tmpc P ([],[]) (rel_axs @ keep)
   294   | relevant_clauses_ax_3 ctab rel_axs ((clstm,(consts_typs,weight))::e_axs) P (addc,tmpc) keep =
   295       let val weights = map (find_clause_weight_s_3_alt ctab consts_typs) rel_axs
   296           val weight' = List.foldl Real.max weight weights
   297 	  val e_ax' = (clstm, (consts_typs,weight'))
   298       in
   299 	if P <= weight' 
   300 	then relevant_clauses_ax_3 ctab rel_axs e_axs P (e_ax'::addc, tmpc) keep
   301 	else relevant_clauses_ax_3 ctab rel_axs e_axs P (addc, e_ax'::tmpc) keep
   302       end;
   303 
   304 fun weight_of_axiom thy (tm,name) =
   305     ((tm,name), (consts_typs_of_term thy tm));
   306 
   307 fun safe_unit_clause ((clstm,_), _) = 
   308       case clause_type clstm of
   309 	  Unit_neq => true
   310 	| Unit_geq => true
   311 	| Other => false;
   312 
   313 fun relevance_filter3_aux thy axioms goals = 
   314     let val pass = !pass_mark
   315 	val const_tab = List.foldl count_axiom_consts Symtab.empty axioms
   316 	val goals_consts_typs = get_goal_consts_typs thy goals
   317 	fun relevant [] (ax,r) = (ax,r)
   318 	  | relevant ((clstm,consts_typs)::y) (ax,r) =
   319 	      let val weight = clause_weight_s_3 const_tab goals_consts_typs consts_typs
   320 		  val ccc = (clstm, (consts_typs,weight))
   321 	      in
   322 		if pass <= weight 
   323 		then relevant y (ccc::ax, r)
   324 		else relevant y (ax, ccc::r)
   325 	      end
   326 	val (rel_clauses,nrel_clauses) =
   327 	    relevant (map (weight_of_axiom thy) axioms) ([],[]) 
   328 	val (ax,r) = relevant_clauses_ax_3 const_tab rel_clauses nrel_clauses pass ([],[]) []
   329     in
   330 	if !add_unit then (filter safe_unit_clause r) @ ax 
   331 	else ax
   332     end;
   333 
   334 fun relevance_filter3 thy axioms goals =
   335   map #1 (relevance_filter3_aux thy axioms goals);
   336     
   337 
   338 (******************************************************************)
   339 (* Generic functions for relevance filtering                      *)
   340 (******************************************************************)
   341 
   342 exception RELEVANCE_FILTER of string;
   343 
   344 fun relevance_filter thy axioms goals = 
   345   case (!strategy) of 1 => relevance_filter1 axioms goals
   346 		    | 2 => relevance_filter2 axioms goals
   347 		    | 3 => relevance_filter3 thy axioms goals
   348 		    | _ => raise RELEVANCE_FILTER("strategy doesn't exist");
   349 
   350 end;