src/HOL/Tools/ATP/reduce_axiomsN.ML
changeset 19208 3e8006cbc925
parent 19200 1da6b9a1575d
child 19212 ec53c138277a
     1.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Tue Mar 07 16:49:12 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Tue Mar 07 16:49:48 2006 +0100
     1.3 @@ -1,8 +1,8 @@
     1.4 +(* Authors: Jia Meng, NICTA and Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5 +   ID: $Id$
     1.6 +   Filtering strategies *)
     1.7 +
     1.8  structure ReduceAxiomsN =
     1.9 -(* Author: Jia Meng, Cambridge University Computer Laboratory
    1.10 -   
    1.11 -   Two filtering strategies *)
    1.12 -
    1.13  struct
    1.14  
    1.15  val pass_mark = ref 0.5;
    1.16 @@ -12,18 +12,23 @@
    1.17    | pol_to_int false = ~1;
    1.18  
    1.19  fun part refs [] (s1,s2) = (s1,s2)
    1.20 -  | 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.21 +  | part refs (s::ss) (s1,s2) = 
    1.22 +      if (s mem refs) then part refs ss (s::s1,s2) else part refs ss (s1,s::s2);
    1.23  
    1.24  
    1.25  fun pol_mem _ [] = false
    1.26 -  | pol_mem (pol,const) ((p,c)::pcs) = if ((pol = not p) andalso (const = c)) then true else pol_mem (pol,const) pcs;
    1.27 +  | pol_mem (pol,const) ((p,c)::pcs) =
    1.28 +      (pol = not p andalso const = c) orelse pol_mem (pol,const) pcs;
    1.29  
    1.30  
    1.31  fun part_w_pol refs [] (s1,s2) = (s1,s2)
    1.32 -  | 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.33 +  | part_w_pol refs (s::ss) (s1,s2) =
    1.34 +      if (pol_mem s refs) then part_w_pol refs ss (s::s1,s2) 
    1.35 +      else part_w_pol refs ss (s1,s::s2);
    1.36  
    1.37  
    1.38 -fun add_term_consts_rm ncs (Const(c, _)) cs = if (c mem ncs) then cs else (c ins_string cs)
    1.39 +fun add_term_consts_rm ncs (Const(c, _)) cs =
    1.40 +      if (c mem ncs) then cs else (c ins_string cs)
    1.41    | add_term_consts_rm ncs (t $ u) cs =
    1.42        add_term_consts_rm ncs t (add_term_consts_rm ncs u cs)
    1.43    | add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs
    1.44 @@ -31,10 +36,13 @@
    1.45  
    1.46  fun term_consts_rm ncs t = add_term_consts_rm ncs t [];
    1.47  
    1.48 -fun consts_of_term term = term_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term;
    1.49 +val standard_consts =
    1.50 +  ["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->","op =","==","True","False"];
    1.51 +
    1.52 +val consts_of_term = term_consts_rm standard_consts;
    1.53  
    1.54  
    1.55 -fun add_term_pconsts_rm ncs (Const(c,_)) pol cs = if (c mem ncs) then cs else ((pol,c) ins cs)
    1.56 +fun add_term_pconsts_rm ncs (Const(c,_)) pol cs = if c mem ncs then cs else ((pol,c) ins cs)
    1.57    | add_term_pconsts_rm ncs (Const("Not",_)$P) pol cs = add_term_pconsts_rm ncs P (not pol) cs
    1.58    | add_term_pconsts_rm ncs (P$Q) pol cs = 
    1.59      add_term_pconsts_rm ncs P pol (add_term_pconsts_rm ncs Q pol cs)
    1.60 @@ -44,13 +52,11 @@
    1.61  
    1.62  fun term_pconsts_rm ncs t = add_term_pconsts_rm ncs t true [];
    1.63  
    1.64 -
    1.65 -fun pconsts_of_term term = term_pconsts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term;
    1.66 +val pconsts_of_term = term_pconsts_rm standard_consts;
    1.67  
    1.68  fun consts_in_goal goal = consts_of_term goal;
    1.69  fun get_goal_consts cs = foldl (op union_string) [] (map consts_in_goal cs);
    1.70  
    1.71 -
    1.72  fun pconsts_in_goal goal = pconsts_of_term goal;
    1.73  fun get_goal_pconsts cs = foldl (op union) [] (map pconsts_in_goal cs);
    1.74  
    1.75 @@ -62,25 +68,26 @@
    1.76  fun find_clause_weight_s_1 (refconsts : string list) consts wa = 
    1.77      let val (rel,irrel) = part refconsts consts ([],[])
    1.78      in
    1.79 -	((real (length rel))/(real (length consts))) * wa
    1.80 +	(real (length rel) / real (length consts)) * wa
    1.81      end;
    1.82  
    1.83  fun find_clause_weight_m_1 [] (_,w) = w 
    1.84    | find_clause_weight_m_1 ((_,(refconsts,wa))::y) (consts,w) =
    1.85 -    let val w' = find_clause_weight_s_1 refconsts consts wa
    1.86 -    in
    1.87 -	if (w < w') then find_clause_weight_m_1 y (consts,w')
    1.88 +      let val w' = find_clause_weight_s_1 refconsts consts wa
    1.89 +      in
    1.90 +	if w < w' then find_clause_weight_m_1 y (consts,w')
    1.91  	else find_clause_weight_m_1 y (consts,w)
    1.92 -    end;
    1.93 +      end;
    1.94  
    1.95  
    1.96  fun relevant_clauses_ax_g_1 _ []  _ (ax,r) = (ax,r)
    1.97    | relevant_clauses_ax_g_1 gconsts  ((clstm,(consts,_))::y) P (ax,r) =
    1.98 -    let val weight = find_clause_weight_s_1 gconsts consts 1.0
    1.99 -    in
   1.100 -	if  P <= weight then relevant_clauses_ax_g_1 gconsts y P ((clstm,(consts,weight))::ax,r)
   1.101 +      let val weight = find_clause_weight_s_1 gconsts consts 1.0
   1.102 +      in
   1.103 +	if  P <= weight 
   1.104 +	then relevant_clauses_ax_g_1 gconsts y P ((clstm,(consts,weight))::ax,r)
   1.105  	else relevant_clauses_ax_g_1 gconsts y P (ax,(clstm,(consts,weight))::r)
   1.106 -    end;
   1.107 +      end;
   1.108  
   1.109  
   1.110  fun relevant_clauses_ax_1 rel_axs  [] P (addc,tmpc) keep = 
   1.111 @@ -88,21 +95,21 @@
   1.112  		| _ => case tmpc of [] => addc @ rel_axs @ keep
   1.113  				  | _ => relevant_clauses_ax_1 addc tmpc P ([],[]) (rel_axs @ keep))
   1.114    | relevant_clauses_ax_1 rel_axs ((clstm,(consts,weight))::e_axs) P (addc,tmpc) keep = 
   1.115 -    let val weight' = find_clause_weight_m_1 rel_axs (consts,weight) 
   1.116 -	val e_ax' = (clstm,(consts, weight'))
   1.117 -    in
   1.118 -	
   1.119 -	if P <= weight' then relevant_clauses_ax_1 rel_axs e_axs P ((clstm,(consts,weight'))::addc,tmpc) keep
   1.120 +      let val weight' = find_clause_weight_m_1 rel_axs (consts,weight) 
   1.121 +	  val e_ax' = (clstm,(consts, weight'))
   1.122 +      in
   1.123 +	if P <= weight' 
   1.124 +	then relevant_clauses_ax_1 rel_axs e_axs P ((clstm,(consts,weight'))::addc,tmpc) keep
   1.125  	else relevant_clauses_ax_1 rel_axs e_axs P (addc,(clstm,(consts,weight'))::tmpc) keep 
   1.126 -    end;
   1.127 +      end;
   1.128  
   1.129  
   1.130  fun initialize [] ax_weights = ax_weights
   1.131    | initialize ((tm,name)::tms_names) ax_weights =
   1.132 -    let val consts = consts_of_term tm
   1.133 -    in
   1.134 -	initialize tms_names (((tm,name),(consts,0.0))::ax_weights)
   1.135 -    end;
   1.136 +      let val consts = consts_of_term tm
   1.137 +      in
   1.138 +	  initialize tms_names (((tm,name),(consts,0.0))::ax_weights)
   1.139 +      end;
   1.140  
   1.141  fun relevance_filter1_aux axioms goals = 
   1.142      let val pass = !pass_mark
   1.143 @@ -116,8 +123,6 @@
   1.144  fun relevance_filter1 axioms goals = map fst (relevance_filter1_aux axioms goals);
   1.145  
   1.146  
   1.147 -
   1.148 -
   1.149  (*************************************************************************)
   1.150  (*            the second relevance filtering strategy                    *)
   1.151  (*************************************************************************)
   1.152 @@ -186,17 +191,15 @@
   1.153  (*** unit clauses ***)
   1.154  datatype clause_type = Unit_neq | Unit_geq | Other
   1.155  
   1.156 +(*Whether all "simple" unit clauses should be included*)
   1.157  val add_unit = ref true;
   1.158  
   1.159 -
   1.160  fun literals_of_term args (Const ("Trueprop",_) $ P) = literals_of_term args P
   1.161    | literals_of_term args (Const ("op |",_) $ P $ Q) = 
   1.162      literals_of_term (literals_of_term args P) Q
   1.163 -  | literals_of_term args P = (P::args);
   1.164 -
   1.165 +  | literals_of_term args P = P::args;
   1.166  
   1.167 -fun is_ground t = if (term_vars t = []) then (term_frees t = []) else false;
   1.168 -
   1.169 +fun is_ground t = (term_vars t = []) andalso (term_frees t = []);
   1.170  
   1.171  fun eq_clause_type (P,Q) = 
   1.172      if ((is_ground P) orelse (is_ground Q)) then Unit_geq else Other;
   1.173 @@ -205,34 +208,27 @@
   1.174    | unit_clause_type _ = Unit_neq;
   1.175  
   1.176  fun clause_type tm = 
   1.177 -    let val lits = literals_of_term [] tm
   1.178 -	val nlits = length lits
   1.179 -    in 
   1.180 -	if (nlits > 1) then Other
   1.181 -	else unit_clause_type (hd lits)
   1.182 -    end;
   1.183 +    case literals_of_term [] tm of
   1.184 +        [lit] => unit_clause_type lit
   1.185 +      | _ => Other;
   1.186  
   1.187  (*** constants with types ***)
   1.188  
   1.189  datatype const_typ =  CTVar | CType of string * const_typ list
   1.190  
   1.191 -fun uni_type (CType (con1,args1)) (CType (con2,args2)) = (con1 = con2) andalso (uni_types args1 args2)
   1.192 -  | uni_type (CType (_,_)) CTVar = true
   1.193 +fun uni_type (CType(con1,args1)) (CType(con2,args2)) = con1=con2 andalso uni_types args1 args2
   1.194 +  | uni_type (CType _) CTVar = true
   1.195    | uni_type CTVar CTVar = true
   1.196    | uni_type CTVar _ = false
   1.197 -
   1.198 -and 
   1.199 -     uni_types [] [] = true
   1.200 -      | uni_types (a1::as1) (a2::as2) = (uni_type a1 a2) andalso (uni_types as1 as2);
   1.201 -
   1.202 +and uni_types [] [] = true
   1.203 +  | uni_types (a1::as1) (a2::as2) = uni_type a1 a2 andalso uni_types as1 as2;
   1.204  
   1.205  
   1.206  fun uni_constants (c1,ctp1) (c2,ctp2) = (c1 = c2) andalso (uni_types ctp1 ctp2);
   1.207  
   1.208  fun uni_mem _ [] = false
   1.209 -  | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) = (uni_constants (c1,c_typ1) (c,c_typ)) orelse (uni_mem (c,c_typ) ctyps);
   1.210 -
   1.211 -
   1.212 +  | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) =
   1.213 +      uni_constants (c1,c_typ1) (c,c_typ) orelse uni_mem (c,c_typ) ctyps;
   1.214  
   1.215  fun const_typ_of (Type (c,typs)) = CType (c,map const_typ_of typs) 
   1.216    | const_typ_of (TFree(_,_)) = CTVar
   1.217 @@ -245,7 +241,8 @@
   1.218  	(c,map const_typ_of tvars)
   1.219      end;
   1.220  
   1.221 -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.222 +fun add_term_consts_typs_rm thy ncs (Const(c, tp)) cs =
   1.223 +      if (c mem ncs) then cs else (const_w_typ thy (c,tp) ins cs)
   1.224    | add_term_consts_typs_rm thy ncs (t $ u) cs =
   1.225        add_term_consts_typs_rm thy ncs  t (add_term_consts_typs_rm thy ncs u cs)
   1.226    | add_term_consts_typs_rm thy ncs (Abs(_,_,t)) cs = add_term_consts_typs_rm thy ncs t cs
   1.227 @@ -253,55 +250,44 @@
   1.228  
   1.229  fun term_consts_typs_rm thy ncs t = add_term_consts_typs_rm thy ncs t [];
   1.230  
   1.231 -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.232 -
   1.233 +fun consts_typs_of_term thy = term_consts_typs_rm thy standard_consts;
   1.234  
   1.235 -fun consts_typs_in_goal thy goal = consts_typs_of_term thy goal;
   1.236 -
   1.237 -fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_in_goal thy) cs)
   1.238 +fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs)
   1.239  
   1.240  
   1.241  (******** filter clauses ********)
   1.242  
   1.243 -fun part3 gctyps [] (s1,s2) = (s1,s2)
   1.244 -  | 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.245 -
   1.246 -
   1.247  fun find_clause_weight_s_3 gctyps consts_typs wa =
   1.248 -    let val (rel,irrel) = part3 gctyps consts_typs ([],[])
   1.249 +    let val rel = filter (fn s => uni_mem s gctyps) consts_typs
   1.250      in
   1.251 -	((real (length rel))/(real (length consts_typs))) * wa
   1.252 +	(real (length rel) / real (length consts_typs)) * wa
   1.253      end;
   1.254  
   1.255 -
   1.256 -fun find_clause_weight_m_3 [] (_,w) = w
   1.257 -  | find_clause_weight_m_3 ((_,(_,(refconsts_typs,wa)))::y) (consts_typs,w) =
   1.258 -    let val w' = find_clause_weight_s_3 refconsts_typs consts_typs wa
   1.259 -    in
   1.260 -	if (w < w') then find_clause_weight_m_3 y (consts_typs,w')
   1.261 -	else find_clause_weight_m_3 y (consts_typs,w)
   1.262 -    end;
   1.263 -
   1.264 -
   1.265  fun relevant_clauses_ax_g_3 _ [] _ (ax,r) = (ax,r)
   1.266    | relevant_clauses_ax_g_3 gctyps ((cls_typ,(clstm,(consts_typs,_)))::y) P (ax,r) =
   1.267 -    let val weight = find_clause_weight_s_3 gctyps consts_typs 1.0
   1.268 -    in
   1.269 -	if P <= weight then relevant_clauses_ax_g_3 gctyps y P ((cls_typ,(clstm,(consts_typs,weight)))::ax,r)
   1.270 -	else relevant_clauses_ax_g_3 gctyps y P (ax,(cls_typ,(clstm,(consts_typs,weight)))::r)
   1.271 -    end;
   1.272 +      let val weight = find_clause_weight_s_3 gctyps consts_typs 1.0
   1.273 +          val ccc = (cls_typ, (clstm, (consts_typs,weight)))
   1.274 +      in
   1.275 +	if P <= weight 
   1.276 +	then relevant_clauses_ax_g_3 gctyps y P (ccc::ax, r)
   1.277 +	else relevant_clauses_ax_g_3 gctyps y P (ax, ccc::r)
   1.278 +      end;
   1.279 +
   1.280 +fun find_clause_weight_s_3_alt consts_typs (_,(_,(refconsts_typs,wa))) =
   1.281 +    find_clause_weight_s_3 refconsts_typs consts_typs wa;
   1.282  
   1.283  fun relevant_clauses_ax_3 rel_axs [] P (addc,tmpc) keep =
   1.284 -    (case addc of [] => (rel_axs @ keep,tmpc)
   1.285 -		| _ => case tmpc of [] => (addc @ rel_axs @ keep,[])
   1.286 -				  | _ => relevant_clauses_ax_3 addc tmpc P ([],[]) (rel_axs @ keep))
   1.287 +      if null addc orelse null tmpc 
   1.288 +      then (addc @ rel_axs @ keep, tmpc)   (*termination!*)
   1.289 +      else relevant_clauses_ax_3 addc tmpc P ([],[]) (rel_axs @ keep)
   1.290    | relevant_clauses_ax_3 rel_axs ((cls_typ,(clstm,(consts_typs,weight)))::e_axs) P (addc,tmpc) keep =
   1.291 -    let val weight' = find_clause_weight_m_3 rel_axs (consts_typs,weight)
   1.292 -	val e_ax' = (cls_typ,(clstm,(consts_typs,weight')))
   1.293 -    in
   1.294 +      let val weights = map (find_clause_weight_s_3_alt consts_typs) rel_axs
   1.295 +          val weight' = List.foldl Real.max weight weights
   1.296 +	  val e_ax' = (cls_typ,(clstm,(consts_typs,weight')))
   1.297 +      in
   1.298  	if P <= weight' then relevant_clauses_ax_3 rel_axs e_axs P (e_ax'::addc,tmpc) keep
   1.299  	else relevant_clauses_ax_3 rel_axs e_axs P (addc,e_ax'::tmpc) keep
   1.300 -    end;
   1.301 +      end;
   1.302  
   1.303  fun initialize3 thy [] ax_weights = ax_weights
   1.304    | initialize3 thy ((tm,name)::tms_names) ax_weights =
   1.305 @@ -321,16 +307,17 @@
   1.306      let val pass = !pass_mark
   1.307  	val axioms_weights = initialize3 thy axioms []
   1.308  	val goals_consts_typs = get_goal_consts_typs thy goals
   1.309 -	val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_3 goals_consts_typs axioms_weights pass ([],[]) 
   1.310 +	val (rel_clauses,nrel_clauses) =
   1.311 +	    relevant_clauses_ax_g_3 goals_consts_typs axioms_weights pass ([],[]) 
   1.312  	val (ax,r) = relevant_clauses_ax_3 rel_clauses nrel_clauses pass ([],[]) []
   1.313      in
   1.314 -	if (!add_unit) then add_unit_clauses ax r else ax
   1.315 +	if !add_unit then add_unit_clauses ax r else ax
   1.316      end;
   1.317  
   1.318 -fun relevance_filter3 thy axioms goals = map fst (map snd (relevance_filter3_aux thy axioms goals));
   1.319 +fun relevance_filter3 thy axioms goals =
   1.320 +  map (#1 o #2) (relevance_filter3_aux thy axioms goals);
   1.321      
   1.322  
   1.323 -
   1.324  (******************************************************************)
   1.325  (* Generic functions for relevance filtering                      *)
   1.326  (******************************************************************)
   1.327 @@ -338,13 +325,9 @@
   1.328  exception RELEVANCE_FILTER of string;
   1.329  
   1.330  fun relevance_filter thy axioms goals = 
   1.331 -    let val cls = (case (!strategy) of 1 => relevance_filter1 axioms goals
   1.332 -				     | 2 => relevance_filter2 axioms goals
   1.333 -				     | 3 => relevance_filter3 thy axioms goals
   1.334 -				     | _ => raise RELEVANCE_FILTER("strategy doesn't exists"))
   1.335 -    in
   1.336 -	cls
   1.337 -    end;
   1.338 -
   1.339 +  case (!strategy) of 1 => relevance_filter1 axioms goals
   1.340 +		    | 2 => relevance_filter2 axioms goals
   1.341 +		    | 3 => relevance_filter3 thy axioms goals
   1.342 +		    | _ => raise RELEVANCE_FILTER("strategy doesn't exist");
   1.343  
   1.344  end;
   1.345 \ No newline at end of file