18791

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 ((clsthm,(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 ((clsthm,(consts,weight))::ax,r)


82 
else relevant_clauses_ax_g_1 gconsts y P (ax,(clsthm,(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 ((clsthm,(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' = (clsthm,(consts, weight'))


93 
in


94 


95 
if P <= weight' then relevant_clauses_ax_1 rel_axs e_axs P ((clsthm,(consts,weight'))::addc,tmpc) keep


96 
else relevant_clauses_ax_1 rel_axs e_axs P (addc,(clsthm,(consts,weight'))::tmpc) keep


97 
end;


98 


99 


100 
fun initialize [] ax_weights = ax_weights


101 
 initialize ((cls,thm)::clss_thms) ax_weights =


102 
let val tm = prop_of thm


103 
val consts = consts_of_term tm


104 
in


105 
initialize clss_thms (((cls,thm),(consts,0.0))::ax_weights)


106 
end;


107 


108 
fun relevance_filter1_aux axioms goals =


109 
let val pass = !pass_mark


110 
val axioms_weights = initialize axioms []


111 
val goals_consts = get_goal_consts goals


112 
val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_1 goals_consts axioms_weights pass ([],[])


113 
in


114 
relevant_clauses_ax_1 rel_clauses nrel_clauses pass ([],[]) []


115 
end;


116 


117 
fun relevance_filter1 axioms goals = map fst (relevance_filter1_aux axioms goals);


118 


119 


120 


121 


122 
(*************************************************************************)


123 
(* the second relevance filtering strategy *)


124 
(*************************************************************************)


125 


126 
fun find_clause_weight_s_2 (refpconsts : (bool * string) list) pconsts wa =


127 
let val (rel,irrel) = part_w_pol refpconsts pconsts ([],[])


128 
in


129 
((real (length rel))/(real (length pconsts))) * wa


130 
end;


131 


132 
fun find_clause_weight_m_2 [] (_,w) = w


133 
 find_clause_weight_m_2 ((_,(refpconsts,wa))::y) (pconsts,w) =


134 
let val w' = find_clause_weight_s_2 refpconsts pconsts wa


135 
in


136 
if (w < w') then find_clause_weight_m_2 y (pconsts,w')


137 
else find_clause_weight_m_2 y (pconsts,w)


138 
end;


139 


140 


141 
fun relevant_clauses_ax_g_2 _ [] _ (ax,r) = (ax,r)


142 
 relevant_clauses_ax_g_2 gpconsts ((clsthm,(pconsts,_))::y) P (ax,r) =


143 
let val weight = find_clause_weight_s_2 gpconsts pconsts 1.0


144 
in


145 
if P <= weight then relevant_clauses_ax_g_2 gpconsts y P ((clsthm,(pconsts,weight))::ax,r)


146 
else relevant_clauses_ax_g_2 gpconsts y P (ax,(clsthm,(pconsts,weight))::r)


147 
end;


148 


149 


150 
fun relevant_clauses_ax_2 rel_axs [] P (addc,tmpc) keep =


151 
(case addc of [] => rel_axs @ keep


152 
 _ => case tmpc of [] => addc @ rel_axs @ keep


153 
 _ => relevant_clauses_ax_2 addc tmpc P ([],[]) (rel_axs @ keep))


154 
 relevant_clauses_ax_2 rel_axs ((clsthm,(pconsts,weight))::e_axs) P (addc,tmpc) keep =


155 
let val weight' = find_clause_weight_m_2 rel_axs (pconsts,weight)


156 
val e_ax' = (clsthm,(pconsts, weight'))


157 
in


158 


159 
if P <= weight' then relevant_clauses_ax_2 rel_axs e_axs P ((clsthm,(pconsts,weight'))::addc,tmpc) keep


160 
else relevant_clauses_ax_2 rel_axs e_axs P (addc,(clsthm,(pconsts,weight'))::tmpc) keep


161 
end;


162 


163 


164 
fun initialize_w_pol [] ax_weights = ax_weights


165 
 initialize_w_pol ((cls,thm)::clss_thms) ax_weights =


166 
let val tm = prop_of thm


167 
val consts = pconsts_of_term tm


168 
in


169 
initialize_w_pol clss_thms (((cls,thm),(consts,0.0))::ax_weights)


170 
end;


171 


172 


173 
fun relevance_filter2_aux axioms goals =


174 
let val pass = !pass_mark


175 
val axioms_weights = initialize_w_pol axioms []


176 
val goals_consts = get_goal_pconsts goals


177 
val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_2 goals_consts axioms_weights pass ([],[])


178 
in


179 
relevant_clauses_ax_2 rel_clauses nrel_clauses pass ([],[]) []


180 
end;


181 


182 
fun relevance_filter2 axioms goals = map fst (relevance_filter2_aux axioms goals);


183 

19009

184 
(******************************************************************)


185 
(* the third relevance filtering strategy *)


186 
(******************************************************************)

18791

187 

19009

188 
(*** unit clauses ***)


189 
datatype clause_type = Unit_neq  Unit_geq  Other


190 


191 
val add_unit = ref true;


192 


193 


194 
fun literals_of_term args (Const ("Trueprop",_) $ P) = literals_of_term args P


195 
 literals_of_term args (Const ("op ",_) $ P $ Q) =


196 
literals_of_term (literals_of_term args P) Q


197 
 literals_of_term args P = (P::args);


198 


199 


200 
fun is_ground t = if (term_vars t = []) then (term_frees t = []) else false;


201 


202 


203 
fun eq_clause_type (P,Q) =


204 
if ((is_ground P) orelse (is_ground Q)) then Unit_geq else Other;


205 


206 
fun unit_clause_type (Const ("op =",_) $ P $ Q) = eq_clause_type (P,Q)


207 
 unit_clause_type _ = Unit_neq;


208 


209 
fun clause_type tm =


210 
let val lits = literals_of_term [] tm


211 
val nlits = length lits


212 
in


213 
if (nlits > 1) then Other


214 
else unit_clause_type (hd lits)


215 
end;


216 


217 
(*** constants with types ***)


218 


219 
datatype const_typ = CTVar  CType of string * const_typ list


220 


221 
fun uni_type (CType (con1,args1)) (CType (con2,args2)) = (con1 = con2) andalso (uni_types args1 args2)


222 
 uni_type (CType (_,_)) CTVar = true


223 
 uni_type CTVar CTVar = true


224 
 uni_type CTVar _ = false


225 


226 
and


227 
uni_types [] [] = true


228 
 uni_types (a1::as1) (a2::as2) = (uni_type a1 a2) andalso (uni_types as1 as2);


229 


230 


231 


232 
fun uni_constants (c1,ctp1) (c2,ctp2) = (c1 = c2) andalso (uni_types ctp1 ctp2);


233 


234 
fun uni_mem _ [] = false

19035

235 
 uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) = (uni_constants (c1,c_typ1) (c,c_typ)) orelse (uni_mem (c,c_typ) ctyps);

19009

236 


237 


238 


239 
fun const_typ_of (Type (c,typs)) = CType (c,map const_typ_of typs)


240 
 const_typ_of (TFree(_,_)) = CTVar


241 
 const_typ_of (TVar(_,_)) = CTVar


242 


243 


244 
fun const_w_typ thy (c,tp) =


245 
let val tvars = Sign.const_typargs thy (c,tp)


246 
in


247 
(c,map const_typ_of tvars)


248 
end;


249 


250 
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)


251 
 add_term_consts_typs_rm thy ncs (t $ u) cs =


252 
add_term_consts_typs_rm thy ncs t (add_term_consts_typs_rm thy ncs u cs)


253 
 add_term_consts_typs_rm thy ncs (Abs(_,_,t)) cs = add_term_consts_typs_rm thy ncs t cs


254 
 add_term_consts_typs_rm thy ncs _ cs = cs;


255 


256 
fun term_consts_typs_rm thy ncs t = add_term_consts_typs_rm thy ncs t [];


257 


258 
fun consts_typs_of_term thy term = term_consts_typs_rm thy ["Trueprop","==>","all","Ex","op &", "op ", "Not", "All", "op >", "op =", "==", "True", "False"] term;


259 


260 


261 
fun consts_typs_in_goal thy goal = consts_typs_of_term thy goal;


262 


263 
fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_in_goal thy) cs)


264 


265 


266 
(******** filter clauses ********)


267 


268 
fun part3 gctyps [] (s1,s2) = (s1,s2)


269 
 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);


270 


271 


272 
fun find_clause_weight_s_3 gctyps consts_typs wa =


273 
let val (rel,irrel) = part3 gctyps consts_typs ([],[])


274 
in


275 
((real (length rel))/(real (length consts_typs))) * wa


276 
end;


277 


278 


279 
fun find_clause_weight_m_3 [] (_,w) = w


280 
 find_clause_weight_m_3 ((_,(_,(refconsts_typs,wa)))::y) (consts_typs,w) =


281 
let val w' = find_clause_weight_s_3 refconsts_typs consts_typs wa


282 
in


283 
if (w < w') then find_clause_weight_m_3 y (consts_typs,w')


284 
else find_clause_weight_m_3 y (consts_typs,w)


285 
end;


286 


287 


288 
fun relevant_clauses_ax_g_3 _ [] _ (ax,r) = (ax,r)


289 
 relevant_clauses_ax_g_3 gctyps ((cls_typ,(clsthm,(consts_typs,_)))::y) P (ax,r) =


290 
let val weight = find_clause_weight_s_3 gctyps consts_typs 1.0


291 
in


292 
if P <= weight then relevant_clauses_ax_g_3 gctyps y P ((cls_typ,(clsthm,(consts_typs,weight)))::ax,r)


293 
else relevant_clauses_ax_g_3 gctyps y P (ax,(cls_typ,(clsthm,(consts_typs,weight)))::r)


294 
end;


295 


296 
fun relevant_clauses_ax_3 rel_axs [] P (addc,tmpc) keep =


297 
(case addc of [] => (rel_axs @ keep,tmpc)


298 
 _ => case tmpc of [] => (addc @ rel_axs @ keep,[])


299 
 _ => relevant_clauses_ax_3 addc tmpc P ([],[]) (rel_axs @ keep))


300 
 relevant_clauses_ax_3 rel_axs ((cls_typ,(clsthm,(consts_typs,weight)))::e_axs) P (addc,tmpc) keep =


301 
let val weight' = find_clause_weight_m_3 rel_axs (consts_typs,weight)


302 
val e_ax' = (cls_typ,(clsthm,(consts_typs,weight')))


303 
in


304 
if P <= weight' then relevant_clauses_ax_3 rel_axs e_axs P (e_ax'::addc,tmpc) keep


305 
else relevant_clauses_ax_3 rel_axs e_axs P (addc,e_ax'::tmpc) keep


306 
end;


307 


308 
fun initialize3 thy [] ax_weights = ax_weights


309 
 initialize3 thy ((cls,thm)::clss_thms) ax_weights =


310 
let val tm = prop_of thm


311 
val cls_type = clause_type tm


312 
val consts = consts_typs_of_term thy tm


313 
in


314 
initialize3 thy clss_thms ((cls_type,((cls,thm),(consts,0.0)))::ax_weights)


315 
end;


316 


317 
fun add_unit_clauses ax [] = ax


318 
 add_unit_clauses ax ((cls_typ,consts_weight)::cs) =


319 
case cls_typ of Unit_neq => add_unit_clauses ((cls_typ,consts_weight)::ax) cs


320 
 Unit_geq => add_unit_clauses ((cls_typ,consts_weight)::ax) cs


321 
 Other => add_unit_clauses ax cs;


322 


323 
fun relevance_filter3_aux thy axioms goals =


324 
let val pass = !pass_mark


325 
val axioms_weights = initialize3 thy axioms []


326 
val goals_consts_typs = get_goal_consts_typs thy goals


327 
val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_3 goals_consts_typs axioms_weights pass ([],[])


328 
val (ax,r) = relevant_clauses_ax_3 rel_clauses nrel_clauses pass ([],[]) []


329 
in


330 
if (!add_unit) then add_unit_clauses ax r else ax


331 
end;


332 


333 
fun relevance_filter3 thy axioms goals = map fst (map snd (relevance_filter3_aux thy axioms goals));


334 

18791

335 


336 


337 
(******************************************************************)


338 
(* Generic functions for relevance filtering *)


339 
(******************************************************************)


340 


341 
exception RELEVANCE_FILTER of string;


342 

19009

343 
fun relevance_filter thy axioms goals =

18791

344 
let val cls = (case (!strategy) of 1 => relevance_filter1 axioms goals


345 
 2 => relevance_filter2 axioms goals

19009

346 
 3 => relevance_filter3 thy axioms goals

18791

347 
 _ => raise RELEVANCE_FILTER("strategy doesn't exists"))


348 
in


349 
cls


350 
end;


351 


352 


353 
end; 