Added another filter strategy.
authormengj
Sat Feb 11 14:23:35 2006 +0100 (2006-02-11)
changeset 19009bb29bf9d3a72
parent 19008 14c1b2f5dda4
child 19010 fef9e4881e83
Added another filter strategy.
src/HOL/Tools/ATP/reduce_axiomsN.ML
     1.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Fri Feb 10 09:09:07 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Sat Feb 11 14:23:35 2006 +0100
     1.3 @@ -181,7 +181,157 @@
     1.4  
     1.5  fun relevance_filter2 axioms goals = map fst (relevance_filter2_aux axioms goals);
     1.6  
     1.7 +(******************************************************************)
     1.8 +(*       the third relevance filtering strategy                   *)
     1.9 +(******************************************************************)
    1.10  
    1.11 +(*** unit clauses ***)
    1.12 +datatype clause_type = Unit_neq | Unit_geq | Other
    1.13 +
    1.14 +val add_unit = ref true;
    1.15 +
    1.16 +
    1.17 +fun literals_of_term args (Const ("Trueprop",_) $ P) = literals_of_term args P
    1.18 +  | literals_of_term args (Const ("op |",_) $ P $ Q) = 
    1.19 +    literals_of_term (literals_of_term args P) Q
    1.20 +  | literals_of_term args P = (P::args);
    1.21 +
    1.22 +
    1.23 +fun is_ground t = if (term_vars t = []) then (term_frees t = []) else false;
    1.24 +
    1.25 +
    1.26 +fun eq_clause_type (P,Q) = 
    1.27 +    if ((is_ground P) orelse (is_ground Q)) then Unit_geq else Other;
    1.28 +
    1.29 +fun unit_clause_type (Const ("op =",_) $ P $ Q) = eq_clause_type (P,Q)
    1.30 +  | unit_clause_type _ = Unit_neq;
    1.31 +
    1.32 +fun clause_type tm = 
    1.33 +    let val lits = literals_of_term [] tm
    1.34 +	val nlits = length lits
    1.35 +    in 
    1.36 +	if (nlits > 1) then Other
    1.37 +	else unit_clause_type (hd lits)
    1.38 +    end;
    1.39 +
    1.40 +(*** constants with types ***)
    1.41 +
    1.42 +datatype const_typ =  CTVar | CType of string * const_typ list
    1.43 +
    1.44 +fun uni_type (CType (con1,args1)) (CType (con2,args2)) = (con1 = con2) andalso (uni_types args1 args2)
    1.45 +  | uni_type (CType (_,_)) CTVar = true
    1.46 +  | uni_type CTVar CTVar = true
    1.47 +  | uni_type CTVar _ = false
    1.48 +
    1.49 +and 
    1.50 +     uni_types [] [] = true
    1.51 +      | uni_types (a1::as1) (a2::as2) = (uni_type a1 a2) andalso (uni_types as1 as2);
    1.52 +
    1.53 +
    1.54 +
    1.55 +fun uni_constants (c1,ctp1) (c2,ctp2) = (c1 = c2) andalso (uni_types ctp1 ctp2);
    1.56 +
    1.57 +fun uni_mem _ [] = false
    1.58 +  | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) = (uni_constants (c,c_typ) (c1,c_typ1)) orelse (uni_mem (c,c_typ) ctyps);
    1.59 +
    1.60 +
    1.61 +
    1.62 +fun const_typ_of (Type (c,typs)) = CType (c,map const_typ_of typs) 
    1.63 +  | const_typ_of (TFree(_,_)) = CTVar
    1.64 +  | const_typ_of (TVar(_,_)) = CTVar
    1.65 +
    1.66 +
    1.67 +fun const_w_typ thy (c,tp) = 
    1.68 +    let val tvars = Sign.const_typargs thy (c,tp)
    1.69 +    in
    1.70 +	(c,map const_typ_of tvars)
    1.71 +    end;
    1.72 +
    1.73 +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)
    1.74 +  | add_term_consts_typs_rm thy ncs (t $ u) cs =
    1.75 +      add_term_consts_typs_rm thy ncs  t (add_term_consts_typs_rm thy ncs u cs)
    1.76 +  | add_term_consts_typs_rm thy ncs (Abs(_,_,t)) cs = add_term_consts_typs_rm thy ncs t cs
    1.77 +  | add_term_consts_typs_rm thy ncs _ cs = cs;
    1.78 +
    1.79 +fun term_consts_typs_rm thy ncs t = add_term_consts_typs_rm thy ncs t [];
    1.80 +
    1.81 +fun consts_typs_of_term thy term = term_consts_typs_rm thy ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term;
    1.82 +
    1.83 +
    1.84 +fun consts_typs_in_goal thy goal = consts_typs_of_term thy goal;
    1.85 +
    1.86 +fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_in_goal thy) cs)
    1.87 +
    1.88 +
    1.89 +(******** filter clauses ********)
    1.90 +
    1.91 +fun part3 gctyps [] (s1,s2) = (s1,s2)
    1.92 +  | 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);
    1.93 +
    1.94 +
    1.95 +fun find_clause_weight_s_3 gctyps consts_typs wa =
    1.96 +    let val (rel,irrel) = part3 gctyps consts_typs ([],[])
    1.97 +    in
    1.98 +	((real (length rel))/(real (length consts_typs))) * wa
    1.99 +    end;
   1.100 +
   1.101 +
   1.102 +fun find_clause_weight_m_3 [] (_,w) = w
   1.103 +  | find_clause_weight_m_3 ((_,(_,(refconsts_typs,wa)))::y) (consts_typs,w) =
   1.104 +    let val w' = find_clause_weight_s_3 refconsts_typs consts_typs wa
   1.105 +    in
   1.106 +	if (w < w') then find_clause_weight_m_3 y (consts_typs,w')
   1.107 +	else find_clause_weight_m_3 y (consts_typs,w)
   1.108 +    end;
   1.109 +
   1.110 +
   1.111 +fun relevant_clauses_ax_g_3 _ [] _ (ax,r) = (ax,r)
   1.112 +  | relevant_clauses_ax_g_3 gctyps ((cls_typ,(clsthm,(consts_typs,_)))::y) P (ax,r) =
   1.113 +    let val weight = find_clause_weight_s_3 gctyps consts_typs 1.0
   1.114 +    in
   1.115 +	if P <= weight then relevant_clauses_ax_g_3 gctyps y P ((cls_typ,(clsthm,(consts_typs,weight)))::ax,r)
   1.116 +	else relevant_clauses_ax_g_3 gctyps y P (ax,(cls_typ,(clsthm,(consts_typs,weight)))::r)
   1.117 +    end;
   1.118 +
   1.119 +fun relevant_clauses_ax_3 rel_axs [] P (addc,tmpc) keep =
   1.120 +    (case addc of [] => (rel_axs @ keep,tmpc)
   1.121 +		| _ => case tmpc of [] => (addc @ rel_axs @ keep,[])
   1.122 +				  | _ => relevant_clauses_ax_3 addc tmpc P ([],[]) (rel_axs @ keep))
   1.123 +  | relevant_clauses_ax_3 rel_axs ((cls_typ,(clsthm,(consts_typs,weight)))::e_axs) P (addc,tmpc) keep =
   1.124 +    let val weight' = find_clause_weight_m_3 rel_axs (consts_typs,weight)
   1.125 +	val e_ax' = (cls_typ,(clsthm,(consts_typs,weight')))
   1.126 +    in
   1.127 +	if P <= weight' then relevant_clauses_ax_3 rel_axs e_axs P (e_ax'::addc,tmpc) keep
   1.128 +	else relevant_clauses_ax_3 rel_axs e_axs P (addc,e_ax'::tmpc) keep
   1.129 +    end;
   1.130 +
   1.131 +fun initialize3 thy [] ax_weights = ax_weights
   1.132 +  | initialize3 thy ((cls,thm)::clss_thms) ax_weights =
   1.133 +    let val tm = prop_of thm
   1.134 +	val cls_type = clause_type tm
   1.135 +	val consts = consts_typs_of_term thy tm
   1.136 +    in
   1.137 +	initialize3 thy clss_thms ((cls_type,((cls,thm),(consts,0.0)))::ax_weights)
   1.138 +    end;
   1.139 +
   1.140 +fun add_unit_clauses ax [] = ax
   1.141 +  | add_unit_clauses ax ((cls_typ,consts_weight)::cs) =
   1.142 +    case cls_typ of Unit_neq => add_unit_clauses ((cls_typ,consts_weight)::ax) cs
   1.143 +		  | Unit_geq => add_unit_clauses ((cls_typ,consts_weight)::ax) cs
   1.144 +		  | Other => add_unit_clauses ax cs;
   1.145 +
   1.146 +fun relevance_filter3_aux thy axioms goals = 
   1.147 +    let val pass = !pass_mark
   1.148 +	val axioms_weights = initialize3 thy axioms []
   1.149 +	val goals_consts_typs = get_goal_consts_typs thy goals
   1.150 +	val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_3 goals_consts_typs axioms_weights pass ([],[]) 
   1.151 +	val (ax,r) = relevant_clauses_ax_3 rel_clauses nrel_clauses pass ([],[]) []
   1.152 +    in
   1.153 +	if (!add_unit) then add_unit_clauses ax r else ax
   1.154 +    end;
   1.155 +
   1.156 +fun relevance_filter3 thy axioms goals = map fst (map snd (relevance_filter3_aux thy axioms goals));
   1.157 +    
   1.158  
   1.159  
   1.160  (******************************************************************)
   1.161 @@ -190,9 +340,10 @@
   1.162  
   1.163  exception RELEVANCE_FILTER of string;
   1.164  
   1.165 -fun relevance_filter axioms goals = 
   1.166 +fun relevance_filter thy axioms goals = 
   1.167      let val cls = (case (!strategy) of 1 => relevance_filter1 axioms goals
   1.168  				     | 2 => relevance_filter2 axioms goals
   1.169 +				     | 3 => relevance_filter3 thy axioms goals
   1.170  				     | _ => raise RELEVANCE_FILTER("strategy doesn't exists"))
   1.171      in
   1.172  	cls