Relevance filtering. Has replaced the previous version.
authormengj
Fri Jan 27 05:34:20 2006 +0100 (2006-01-27)
changeset 187919b4ae9fa67a4
parent 18790 418131f631fc
child 18792 fb427f4a01f2
Relevance filtering. Has replaced the previous version.
src/HOL/Tools/ATP/reduce_axiomsN.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Fri Jan 27 05:34:20 2006 +0100
     1.3 @@ -0,0 +1,202 @@
     1.4 +structure ReduceAxiomsN =
     1.5 +(* Author: Jia Meng, Cambridge University Computer Laboratory
     1.6 +   
     1.7 +   Two filtering strategies *)
     1.8 +
     1.9 +struct
    1.10 +
    1.11 +val pass_mark = ref 0.5;
    1.12 +val strategy = ref 1;
    1.13 +
    1.14 +fun pol_to_int true = 1
    1.15 +  | pol_to_int false = ~1;
    1.16 +
    1.17 +fun part refs [] (s1,s2) = (s1,s2)
    1.18 +  | part refs (s::ss) (s1,s2) = if (s mem refs) then (part refs ss (s::s1,s2)) else (part refs ss (s1,s::s2));
    1.19 +
    1.20 +
    1.21 +fun pol_mem _ [] = false
    1.22 +  | pol_mem (pol,const) ((p,c)::pcs) = if ((pol = not p) andalso (const = c)) then true else pol_mem (pol,const) pcs;
    1.23 +
    1.24 +
    1.25 +fun part_w_pol refs [] (s1,s2) = (s1,s2)
    1.26 +  | 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));
    1.27 +
    1.28 +
    1.29 +fun add_term_consts_rm ncs (Const(c, _)) cs = if (c mem ncs) then cs else (c ins_string cs)
    1.30 +  | add_term_consts_rm ncs (t $ u) cs =
    1.31 +      add_term_consts_rm ncs t (add_term_consts_rm ncs u cs)
    1.32 +  | add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs
    1.33 +  | add_term_consts_rm ncs _ cs = cs;
    1.34 +
    1.35 +fun term_consts_rm ncs t = add_term_consts_rm ncs t [];
    1.36 +
    1.37 +fun consts_of_term term = term_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term;
    1.38 +
    1.39 +
    1.40 +fun add_term_pconsts_rm ncs (Const(c,_)) pol cs = if (c mem ncs) then cs else ((pol,c) ins cs)
    1.41 +  | add_term_pconsts_rm ncs (Const("Not",_)$P) pol cs = add_term_pconsts_rm ncs P (not pol) cs
    1.42 +  | add_term_pconsts_rm ncs (P$Q) pol cs = 
    1.43 +    add_term_pconsts_rm ncs P pol (add_term_pconsts_rm ncs Q pol cs)
    1.44 +  | add_term_pconsts_rm ncs (Abs(_,_,t)) pol cs = add_term_pconsts_rm ncs t pol cs
    1.45 +  | add_term_pconsts_rm ncs _ _ cs = cs;
    1.46 +
    1.47 +
    1.48 +fun term_pconsts_rm ncs t = add_term_pconsts_rm ncs t true [];
    1.49 +
    1.50 +
    1.51 +fun pconsts_of_term term = term_pconsts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term;
    1.52 +
    1.53 +fun consts_in_goal goal = consts_of_term goal;
    1.54 +fun get_goal_consts cs = foldl (op union_string) [] (map consts_in_goal cs);
    1.55 +
    1.56 +
    1.57 +fun pconsts_in_goal goal = pconsts_of_term goal;
    1.58 +fun get_goal_pconsts cs = foldl (op union) [] (map pconsts_in_goal cs);
    1.59 +
    1.60 +
    1.61 +(*************************************************************************)
    1.62 +(*            the first relevance filtering strategy                     *)
    1.63 +(*************************************************************************)
    1.64 +
    1.65 +fun find_clause_weight_s_1 (refconsts : string list) consts wa = 
    1.66 +    let val (rel,irrel) = part refconsts consts ([],[])
    1.67 +    in
    1.68 +	((real (length rel))/(real (length consts))) * wa
    1.69 +    end;
    1.70 +
    1.71 +fun find_clause_weight_m_1 [] (_,w) = w 
    1.72 +  | find_clause_weight_m_1 ((_,(refconsts,wa))::y) (consts,w) =
    1.73 +    let val w' = find_clause_weight_s_1 refconsts consts wa
    1.74 +    in
    1.75 +	if (w < w') then find_clause_weight_m_1 y (consts,w')
    1.76 +	else find_clause_weight_m_1 y (consts,w)
    1.77 +    end;
    1.78 +
    1.79 +
    1.80 +fun relevant_clauses_ax_g_1 _ []  _ (ax,r) = (ax,r)
    1.81 +  | relevant_clauses_ax_g_1 gconsts  ((clsthm,(consts,_))::y) P (ax,r) =
    1.82 +    let val weight = find_clause_weight_s_1 gconsts consts 1.0
    1.83 +    in
    1.84 +	if  P <= weight then relevant_clauses_ax_g_1 gconsts y P ((clsthm,(consts,weight))::ax,r)
    1.85 +	else relevant_clauses_ax_g_1 gconsts y P (ax,(clsthm,(consts,weight))::r)
    1.86 +    end;
    1.87 +
    1.88 +
    1.89 +fun relevant_clauses_ax_1 rel_axs  [] P (addc,tmpc) keep = 
    1.90 +    (case addc of [] => rel_axs @ keep
    1.91 +		| _ => case tmpc of [] => addc @ rel_axs @ keep
    1.92 +				  | _ => relevant_clauses_ax_1 addc tmpc P ([],[]) (rel_axs @ keep))
    1.93 +  | relevant_clauses_ax_1 rel_axs ((clsthm,(consts,weight))::e_axs) P (addc,tmpc) keep = 
    1.94 +    let val weight' = find_clause_weight_m_1 rel_axs (consts,weight) 
    1.95 +	val e_ax' = (clsthm,(consts, weight'))
    1.96 +    in
    1.97 +	
    1.98 +	if P <= weight' then relevant_clauses_ax_1 rel_axs e_axs P ((clsthm,(consts,weight'))::addc,tmpc) keep
    1.99 +	else relevant_clauses_ax_1 rel_axs e_axs P (addc,(clsthm,(consts,weight'))::tmpc) keep 
   1.100 +    end;
   1.101 +
   1.102 +
   1.103 +fun initialize [] ax_weights = ax_weights
   1.104 +  | initialize ((cls,thm)::clss_thms) ax_weights =
   1.105 +    let val tm = prop_of thm
   1.106 +	val consts = consts_of_term tm
   1.107 +    in
   1.108 +	initialize clss_thms (((cls,thm),(consts,0.0))::ax_weights)
   1.109 +    end;
   1.110 +
   1.111 +fun relevance_filter1_aux axioms goals = 
   1.112 +    let val pass = !pass_mark
   1.113 +	val axioms_weights = initialize axioms []
   1.114 +	val goals_consts = get_goal_consts goals
   1.115 +	val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_1 goals_consts axioms_weights pass ([],[]) 
   1.116 +    in
   1.117 +	relevant_clauses_ax_1 rel_clauses nrel_clauses pass ([],[]) []
   1.118 +    end;
   1.119 +
   1.120 +fun relevance_filter1 axioms goals = map fst (relevance_filter1_aux axioms goals);
   1.121 +
   1.122 +
   1.123 +
   1.124 +
   1.125 +(*************************************************************************)
   1.126 +(*            the second relevance filtering strategy                    *)
   1.127 +(*************************************************************************)
   1.128 +
   1.129 +fun find_clause_weight_s_2 (refpconsts : (bool * string) list) pconsts wa = 
   1.130 +    let val (rel,irrel) = part_w_pol refpconsts pconsts ([],[])
   1.131 +    in
   1.132 +	((real (length rel))/(real (length pconsts))) * wa
   1.133 +    end;
   1.134 +
   1.135 +fun find_clause_weight_m_2 [] (_,w) = w 
   1.136 +  | find_clause_weight_m_2 ((_,(refpconsts,wa))::y) (pconsts,w) =
   1.137 +    let val w' = find_clause_weight_s_2 refpconsts pconsts wa
   1.138 +    in
   1.139 +	if (w < w') then find_clause_weight_m_2 y (pconsts,w')
   1.140 +	else find_clause_weight_m_2 y (pconsts,w)
   1.141 +    end;
   1.142 +
   1.143 +
   1.144 +fun relevant_clauses_ax_g_2 _ []  _ (ax,r) = (ax,r)
   1.145 +  | relevant_clauses_ax_g_2 gpconsts  ((clsthm,(pconsts,_))::y) P (ax,r) =
   1.146 +    let val weight = find_clause_weight_s_2 gpconsts pconsts 1.0
   1.147 +    in
   1.148 +	if  P <= weight then relevant_clauses_ax_g_2 gpconsts y P ((clsthm,(pconsts,weight))::ax,r)
   1.149 +	else relevant_clauses_ax_g_2 gpconsts y P (ax,(clsthm,(pconsts,weight))::r)
   1.150 +    end;
   1.151 +
   1.152 +
   1.153 +fun relevant_clauses_ax_2 rel_axs  [] P (addc,tmpc) keep = 
   1.154 +    (case addc of [] => rel_axs @ keep
   1.155 +		| _ => case tmpc of [] => addc @ rel_axs @ keep
   1.156 +				  | _ => relevant_clauses_ax_2 addc tmpc P ([],[]) (rel_axs @ keep))
   1.157 +  | relevant_clauses_ax_2 rel_axs ((clsthm,(pconsts,weight))::e_axs) P (addc,tmpc) keep = 
   1.158 +    let val weight' = find_clause_weight_m_2 rel_axs (pconsts,weight) 
   1.159 +	val e_ax' = (clsthm,(pconsts, weight'))
   1.160 +    in
   1.161 +	
   1.162 +	if P <= weight' then relevant_clauses_ax_2 rel_axs e_axs P ((clsthm,(pconsts,weight'))::addc,tmpc) keep
   1.163 +	else relevant_clauses_ax_2 rel_axs e_axs P (addc,(clsthm,(pconsts,weight'))::tmpc) keep 
   1.164 +    end;
   1.165 +
   1.166 +
   1.167 +fun initialize_w_pol [] ax_weights = ax_weights
   1.168 +  | initialize_w_pol ((cls,thm)::clss_thms) ax_weights =
   1.169 +    let val tm = prop_of thm
   1.170 +	val consts = pconsts_of_term tm
   1.171 +    in
   1.172 +	initialize_w_pol clss_thms (((cls,thm),(consts,0.0))::ax_weights)
   1.173 +    end;
   1.174 +
   1.175 +
   1.176 +fun relevance_filter2_aux axioms goals = 
   1.177 +    let val pass = !pass_mark
   1.178 +	val axioms_weights = initialize_w_pol axioms []
   1.179 +	val goals_consts = get_goal_pconsts goals
   1.180 +	val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_2 goals_consts axioms_weights pass ([],[]) 
   1.181 +    in
   1.182 +	relevant_clauses_ax_2 rel_clauses nrel_clauses pass ([],[]) []
   1.183 +    end;
   1.184 +
   1.185 +fun relevance_filter2 axioms goals = map fst (relevance_filter2_aux axioms goals);
   1.186 +
   1.187 +
   1.188 +
   1.189 +
   1.190 +(******************************************************************)
   1.191 +(* Generic functions for relevance filtering                      *)
   1.192 +(******************************************************************)
   1.193 +
   1.194 +exception RELEVANCE_FILTER of string;
   1.195 +
   1.196 +fun relevance_filter axioms goals = 
   1.197 +    let val cls = (case (!strategy) of 1 => relevance_filter1 axioms goals
   1.198 +				     | 2 => relevance_filter2 axioms goals
   1.199 +				     | _ => raise RELEVANCE_FILTER("strategy doesn't exists"))
   1.200 +    in
   1.201 +	cls
   1.202 +    end;
   1.203 +
   1.204 +
   1.205 +end;
   1.206 \ No newline at end of file