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