src/HOL/Tools/ATP/reduce_axiomsN.ML
changeset 19315 b218cc3d1bb4
parent 19231 c8879dd3a953
child 19321 30b5bb35dd33
     1.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Mar 22 11:54:54 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Mar 22 12:30:29 2006 +0100
     1.3 @@ -5,197 +5,24 @@
     1.4  structure ReduceAxiomsN =
     1.5  struct
     1.6  
     1.7 -val pass_mark = ref 0.5;
     1.8 -val strategy = ref 3;
     1.9 -val max_filtered = ref 2000;
    1.10 -
    1.11 -fun pol_to_int true = 1
    1.12 -  | pol_to_int false = ~1;
    1.13 -
    1.14 -fun part refs [] (s1,s2) = (s1,s2)
    1.15 -  | part refs (s::ss) (s1,s2) = 
    1.16 -      if (s mem refs) then part refs ss (s::s1,s2) else part refs ss (s1,s::s2);
    1.17 -
    1.18 -
    1.19 -fun pol_mem _ [] = false
    1.20 -  | pol_mem (pol,const) ((p,c)::pcs) =
    1.21 -      (pol = not p andalso const = c) orelse pol_mem (pol,const) pcs;
    1.22 +val pass_mark = ref 0.6;
    1.23 +val reduction_factor = ref 1.0;
    1.24  
    1.25 -
    1.26 -fun part_w_pol refs [] (s1,s2) = (s1,s2)
    1.27 -  | part_w_pol refs (s::ss) (s1,s2) =
    1.28 -      if (pol_mem s refs) then part_w_pol refs ss (s::s1,s2) 
    1.29 -      else part_w_pol refs ss (s1,s::s2);
    1.30 -
    1.31 +(*Whether all "simple" unit clauses should be included*)
    1.32 +val add_unit = ref false;
    1.33 +val unit_pass_mark = ref 0.0;
    1.34  
    1.35 -fun add_term_consts_rm ncs (Const(c, _)) cs =
    1.36 -      if (c mem ncs) then cs else (c ins_string cs)
    1.37 -  | add_term_consts_rm ncs (t $ u) cs =
    1.38 -      add_term_consts_rm ncs t (add_term_consts_rm ncs u cs)
    1.39 -  | add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs
    1.40 -  | add_term_consts_rm ncs _ cs = cs;
    1.41 -
    1.42 -fun term_consts_rm ncs t = add_term_consts_rm ncs t [];
    1.43  
    1.44  (*Including equality in this list might be expected to stop rules like subset_antisym from
    1.45    being chosen, but for some reason filtering works better with them listed.*)
    1.46  val standard_consts =
    1.47 -  ["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->","op =","==","True","False"];
    1.48 -
    1.49 -val consts_of_term = term_consts_rm standard_consts;
    1.50 -
    1.51 -
    1.52 -fun add_term_pconsts_rm ncs (Const(c,_)) pol cs = if c mem ncs then cs else ((pol,c) ins cs)
    1.53 -  | add_term_pconsts_rm ncs (Const("Not",_)$P) pol cs = add_term_pconsts_rm ncs P (not pol) cs
    1.54 -  | add_term_pconsts_rm ncs (P$Q) pol cs = 
    1.55 -    add_term_pconsts_rm ncs P pol (add_term_pconsts_rm ncs Q pol cs)
    1.56 -  | add_term_pconsts_rm ncs (Abs(_,_,t)) pol cs = add_term_pconsts_rm ncs t pol cs
    1.57 -  | add_term_pconsts_rm ncs _ _ cs = cs;
    1.58 -
    1.59 -
    1.60 -fun term_pconsts_rm ncs t = add_term_pconsts_rm ncs t true [];
    1.61 -
    1.62 -val pconsts_of_term = term_pconsts_rm standard_consts;
    1.63 -
    1.64 -fun consts_in_goal goal = consts_of_term goal;
    1.65 -fun get_goal_consts cs = foldl (op union_string) [] (map consts_in_goal cs);
    1.66 -
    1.67 -fun pconsts_in_goal goal = pconsts_of_term goal;
    1.68 -fun get_goal_pconsts cs = foldl (op union) [] (map pconsts_in_goal cs);
    1.69 -
    1.70 -
    1.71 -(*************************************************************************)
    1.72 -(*            the first relevance filtering strategy                     *)
    1.73 -(*************************************************************************)
    1.74 -
    1.75 -fun find_clause_weight_s_1 (refconsts : string list) consts wa = 
    1.76 -    let val (rel,irrel) = part refconsts consts ([],[])
    1.77 -    in
    1.78 -	(real (length rel) / real (length consts)) * wa
    1.79 -    end;
    1.80 -
    1.81 -fun find_clause_weight_m_1 [] (_,w) = w 
    1.82 -  | find_clause_weight_m_1 ((_,(refconsts,wa))::y) (consts,w) =
    1.83 -      let val w' = find_clause_weight_s_1 refconsts consts wa
    1.84 -      in
    1.85 -	if w < w' then find_clause_weight_m_1 y (consts,w')
    1.86 -	else find_clause_weight_m_1 y (consts,w)
    1.87 -      end;
    1.88 -
    1.89 -
    1.90 -fun relevant_clauses_ax_g_1 _ []  _ (ax,r) = (ax,r)
    1.91 -  | relevant_clauses_ax_g_1 gconsts  ((clstm,(consts,_))::y) P (ax,r) =
    1.92 -      let val weight = find_clause_weight_s_1 gconsts consts 1.0
    1.93 -      in
    1.94 -	if  P <= weight 
    1.95 -	then relevant_clauses_ax_g_1 gconsts y P ((clstm,(consts,weight))::ax,r)
    1.96 -	else relevant_clauses_ax_g_1 gconsts y P (ax,(clstm,(consts,weight))::r)
    1.97 -      end;
    1.98 -
    1.99 -
   1.100 -fun relevant_clauses_ax_1 rel_axs  [] P (addc,tmpc) keep = 
   1.101 -    (case addc of [] => rel_axs @ keep
   1.102 -		| _ => case tmpc of [] => addc @ rel_axs @ keep
   1.103 -				  | _ => relevant_clauses_ax_1 addc tmpc P ([],[]) (rel_axs @ keep))
   1.104 -  | relevant_clauses_ax_1 rel_axs ((clstm,(consts,weight))::e_axs) P (addc,tmpc) keep = 
   1.105 -      let val weight' = find_clause_weight_m_1 rel_axs (consts,weight) 
   1.106 -	  val e_ax' = (clstm,(consts, weight'))
   1.107 -      in
   1.108 -	if P <= weight' 
   1.109 -	then relevant_clauses_ax_1 rel_axs e_axs P ((clstm,(consts,weight'))::addc,tmpc) keep
   1.110 -	else relevant_clauses_ax_1 rel_axs e_axs P (addc,(clstm,(consts,weight'))::tmpc) keep 
   1.111 -      end;
   1.112 -
   1.113 -
   1.114 -fun initialize [] ax_weights = ax_weights
   1.115 -  | initialize ((tm,name)::tms_names) ax_weights =
   1.116 -      let val consts = consts_of_term tm
   1.117 -      in
   1.118 -	  initialize tms_names (((tm,name),(consts,0.0))::ax_weights)
   1.119 -      end;
   1.120 +  ["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->",
   1.121 +   "op =","==","True","False"];
   1.122  
   1.123 -fun relevance_filter1_aux axioms goals = 
   1.124 -    let val pass = !pass_mark
   1.125 -	val axioms_weights = initialize axioms []
   1.126 -	val goals_consts = get_goal_consts goals
   1.127 -	val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_1 goals_consts axioms_weights pass ([],[]) 
   1.128 -    in
   1.129 -	relevant_clauses_ax_1 rel_clauses nrel_clauses pass ([],[]) []
   1.130 -    end;
   1.131 -
   1.132 -fun relevance_filter1 axioms goals = map fst (relevance_filter1_aux axioms goals);
   1.133 -
   1.134 -
   1.135 -(*************************************************************************)
   1.136 -(*            the second relevance filtering strategy                    *)
   1.137 -(*************************************************************************)
   1.138 -
   1.139 -fun find_clause_weight_s_2 (refpconsts : (bool * string) list) pconsts wa = 
   1.140 -    let val (rel,irrel) = part_w_pol refpconsts pconsts ([],[])
   1.141 -    in
   1.142 -	((real (length rel))/(real (length pconsts))) * wa
   1.143 -    end;
   1.144 -
   1.145 -fun find_clause_weight_m_2 [] (_,w) = w 
   1.146 -  | find_clause_weight_m_2 ((_,(refpconsts,wa))::y) (pconsts,w) =
   1.147 -    let val w' = find_clause_weight_s_2 refpconsts pconsts wa
   1.148 -    in
   1.149 -	if (w < w') then find_clause_weight_m_2 y (pconsts,w')
   1.150 -	else find_clause_weight_m_2 y (pconsts,w)
   1.151 -    end;
   1.152 -
   1.153 -
   1.154 -fun relevant_clauses_ax_g_2 _ []  _ (ax,r) = (ax,r)
   1.155 -  | relevant_clauses_ax_g_2 gpconsts  ((clstm,(pconsts,_))::y) P (ax,r) =
   1.156 -    let val weight = find_clause_weight_s_2 gpconsts pconsts 1.0
   1.157 -    in
   1.158 -	if  P <= weight then relevant_clauses_ax_g_2 gpconsts y P ((clstm,(pconsts,weight))::ax,r)
   1.159 -	else relevant_clauses_ax_g_2 gpconsts y P (ax,(clstm,(pconsts,weight))::r)
   1.160 -    end;
   1.161 -
   1.162 -
   1.163 -fun relevant_clauses_ax_2 rel_axs  [] P (addc,tmpc) keep = 
   1.164 -    (case addc of [] => rel_axs @ keep
   1.165 -		| _ => case tmpc of [] => addc @ rel_axs @ keep
   1.166 -				  | _ => relevant_clauses_ax_2 addc tmpc P ([],[]) (rel_axs @ keep))
   1.167 -  | relevant_clauses_ax_2 rel_axs ((clstm,(pconsts,weight))::e_axs) P (addc,tmpc) keep = 
   1.168 -    let val weight' = find_clause_weight_m_2 rel_axs (pconsts,weight) 
   1.169 -	val e_ax' = (clstm,(pconsts, weight'))
   1.170 -    in
   1.171 -	
   1.172 -	if P <= weight' then relevant_clauses_ax_2 rel_axs e_axs P ((clstm,(pconsts,weight'))::addc,tmpc) keep
   1.173 -	else relevant_clauses_ax_2 rel_axs e_axs P (addc,(clstm,(pconsts,weight'))::tmpc) keep 
   1.174 -    end;
   1.175 -
   1.176 -
   1.177 -fun initialize_w_pol [] ax_weights = ax_weights
   1.178 -  | initialize_w_pol ((tm,name)::tms_names) ax_weights =
   1.179 -    let val consts = pconsts_of_term tm
   1.180 -    in
   1.181 -	initialize_w_pol tms_names (((tm,name),(consts,0.0))::ax_weights)
   1.182 -    end;
   1.183 -
   1.184 -
   1.185 -fun relevance_filter2_aux axioms goals = 
   1.186 -    let val pass = !pass_mark
   1.187 -	val axioms_weights = initialize_w_pol axioms []
   1.188 -	val goals_consts = get_goal_pconsts goals
   1.189 -	val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_2 goals_consts axioms_weights pass ([],[]) 
   1.190 -    in
   1.191 -	relevant_clauses_ax_2 rel_clauses nrel_clauses pass ([],[]) []
   1.192 -    end;
   1.193 -
   1.194 -fun relevance_filter2 axioms goals = map fst (relevance_filter2_aux axioms goals);
   1.195 -
   1.196 -(******************************************************************)
   1.197 -(*       the third relevance filtering strategy                   *)
   1.198 -(******************************************************************)
   1.199  
   1.200  (*** unit clauses ***)
   1.201  datatype clause_kind = Unit_neq | Unit_geq | Other
   1.202  
   1.203 -(*Whether all "simple" unit clauses should be included*)
   1.204 -val add_unit = ref true;
   1.205  
   1.206  fun literals_of_term args (Const ("Trueprop",_) $ P) = literals_of_term args P
   1.207    | literals_of_term args (Const ("op |",_) $ P $ Q) = 
   1.208 @@ -239,20 +66,23 @@
   1.209    | const_typ_of (TVar _) = CTVar
   1.210  
   1.211  
   1.212 -fun const_w_typ thy (c,typ) = 
   1.213 +fun const_with_typ thy (c,typ) = 
   1.214      let val tvars = Sign.const_typargs thy (c,typ)
   1.215 -    in (c, map const_typ_of tvars) end;
   1.216 +    in (c, map const_typ_of tvars) end
   1.217 +    handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)   
   1.218  
   1.219 -fun add_term_consts_typs_rm thy ncs (Const(c, typ)) cs =
   1.220 -      if (c mem ncs) then cs else (const_w_typ thy (c,typ) ins cs)
   1.221 -  | add_term_consts_typs_rm thy ncs (t $ u) cs =
   1.222 -      add_term_consts_typs_rm thy ncs  t (add_term_consts_typs_rm thy ncs u cs)
   1.223 -  | add_term_consts_typs_rm thy ncs (Abs(_,_,t)) cs = add_term_consts_typs_rm thy ncs t cs
   1.224 -  | add_term_consts_typs_rm thy ncs _ cs = cs;
   1.225 +(*Free variables are counted, as well as constants, to handle locales*)
   1.226 +fun add_term_consts_typs_rm thy (Const(c, typ)) cs =
   1.227 +      if (c mem standard_consts) then cs 
   1.228 +      else const_with_typ thy (c,typ) ins cs
   1.229 +  | add_term_consts_typs_rm thy (Free(c, typ)) cs =
   1.230 +      const_with_typ thy (c,typ) ins cs
   1.231 +  | add_term_consts_typs_rm thy (t $ u) cs =
   1.232 +      add_term_consts_typs_rm thy t (add_term_consts_typs_rm thy u cs)
   1.233 +  | add_term_consts_typs_rm thy (Abs(_,_,t)) cs = add_term_consts_typs_rm thy t cs
   1.234 +  | add_term_consts_typs_rm thy _ cs = cs;
   1.235  
   1.236 -fun term_consts_typs_rm thy ncs t = add_term_consts_typs_rm thy ncs t [];
   1.237 -
   1.238 -fun consts_typs_of_term thy = term_consts_typs_rm thy standard_consts;
   1.239 +fun consts_typs_of_term thy t = add_term_consts_typs_rm thy t [];
   1.240  
   1.241  fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs)
   1.242  
   1.243 @@ -276,19 +106,21 @@
   1.244  
   1.245  structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
   1.246  
   1.247 -fun count_axiom_consts thy ((tm,_), tab) = 
   1.248 -  let fun count_term_consts (Const cT, tab) =
   1.249 -	    let val (c, cts) = const_w_typ thy cT
   1.250 -		val cttab = Option.getOpt (Symtab.lookup tab c, CTtab.empty)
   1.251 -		val n = Option.getOpt (CTtab.lookup cttab cts, 0)
   1.252 -	    in 
   1.253 -		Symtab.update (c, CTtab.update (cts, n+1) cttab) tab
   1.254 -            end
   1.255 +fun count_axiom_consts thy ((t,_), tab) = 
   1.256 +  let fun count_const (a, T, tab) =
   1.257 +	let val (c, cts) = const_with_typ thy (a,T)
   1.258 +	    val cttab = Option.getOpt (Symtab.lookup tab c, CTtab.empty)
   1.259 +	    val n = Option.getOpt (CTtab.lookup cttab cts, 0)
   1.260 +	in 
   1.261 +	    Symtab.update (c, CTtab.update (cts, n+1) cttab) tab
   1.262 +	end
   1.263 +      fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
   1.264 +	| count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
   1.265  	| count_term_consts (t $ u, tab) =
   1.266  	    count_term_consts (t, count_term_consts (u, tab))
   1.267  	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
   1.268  	| count_term_consts (_, tab) = tab
   1.269 -  in  count_term_consts (tm, tab) end;
   1.270 +  in  count_term_consts (t, tab)  end;
   1.271  
   1.272  
   1.273  (******** filter clauses ********)
   1.274 @@ -310,36 +142,39 @@
   1.275  (*Relevant constants are weighted according to frequency, 
   1.276    but irrelevant constants are simply counted. Otherwise, Skolem functions,
   1.277    which are rare, would harm a clause's chances of being picked.*)
   1.278 -fun clause_weight_s_3 ctab gctyps consts_typs =
   1.279 +fun clause_weight ctab gctyps consts_typs =
   1.280      let val rel = filter (fn s => uni_mem s gctyps) consts_typs
   1.281          val rel_weight = consts_typs_weight ctab rel
   1.282      in
   1.283  	rel_weight / (rel_weight + real (length consts_typs - length rel))
   1.284      end;
   1.285 -
   1.286 -fun relevant_clauses_ax_3 ctab rel_axs [] P (addc,tmpc) keep =
   1.287 +    
   1.288 +fun relevant_clauses ctab rel_axs [] (addc,tmpc) keep =
   1.289        if null addc orelse null tmpc 
   1.290        then (addc @ rel_axs @ keep, tmpc)   (*termination!*)
   1.291 -      else relevant_clauses_ax_3 ctab addc tmpc P ([],[]) (rel_axs @ keep)
   1.292 -  | relevant_clauses_ax_3 ctab rel_axs ((clstm,(consts_typs,weight))::e_axs) P (addc,tmpc) keep =
   1.293 +      else relevant_clauses ctab addc tmpc ([],[]) (rel_axs @ keep)
   1.294 +  | relevant_clauses ctab rel_axs ((clstm,(consts_typs,w))::e_axs) (addc,tmpc) keep =
   1.295        let fun clause_weight_ax (_,(refconsts_typs,wa)) =
   1.296 -              wa * clause_weight_s_3 ctab refconsts_typs consts_typs;
   1.297 -          val weight' = List.foldl Real.max weight (map clause_weight_ax rel_axs)
   1.298 +              wa * clause_weight ctab refconsts_typs consts_typs;
   1.299 +          val weight' = List.foldl Real.max w (map clause_weight_ax rel_axs)
   1.300  	  val e_ax' = (clstm, (consts_typs,weight'))
   1.301        in
   1.302 -	if P <= weight' 
   1.303 -	then relevant_clauses_ax_3 ctab rel_axs e_axs P (e_ax'::addc, tmpc) keep
   1.304 -	else relevant_clauses_ax_3 ctab rel_axs e_axs P (addc, e_ax'::tmpc) keep
   1.305 +	if !pass_mark <= weight' 
   1.306 +	then relevant_clauses ctab rel_axs e_axs (e_ax'::addc, tmpc) keep
   1.307 +	else relevant_clauses ctab rel_axs e_axs (addc, e_ax'::tmpc) keep
   1.308        end;
   1.309  
   1.310  fun pair_consts_typs_axiom thy (tm,name) =
   1.311      ((tm,name), (consts_typs_of_term thy tm));
   1.312  
   1.313 -fun safe_unit_clause ((t,_), _) = 
   1.314 -      case clause_kind t of
   1.315 +(*Unit clauses other than non-trivial equations can be included subject to
   1.316 +  a separate (presumably lower) mark. *)
   1.317 +fun good_unit_clause ((t,_), (_,w)) = 
   1.318 +     !unit_pass_mark <= w andalso
   1.319 +     (case clause_kind t of
   1.320  	  Unit_neq => true
   1.321  	| Unit_geq => true
   1.322 -	| Other => false;
   1.323 +	| Other => false);
   1.324  	
   1.325  fun axiom_ord ((_,(_,w1)), (_,(_,w2))) = Real.compare (w2,w1);
   1.326  
   1.327 @@ -352,46 +187,34 @@
   1.328  fun showax ((_,cname), (_,w)) = 
   1.329      Output.debug ("Axiom " ^ show_cname cname ^ " has weight " ^ Real.toString w)
   1.330  	      
   1.331 -	      fun relevance_filter3_aux thy axioms goals = 
   1.332 -  let val pass = !pass_mark
   1.333 -      val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
   1.334 +fun relevance_filter_aux thy axioms goals = 
   1.335 +  let val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
   1.336        val goals_consts_typs = get_goal_consts_typs thy goals
   1.337        fun relevant [] (ax,r) = (ax,r)
   1.338  	| relevant ((clstm,consts_typs)::y) (ax,r) =
   1.339 -	    let val weight = clause_weight_s_3 const_tab goals_consts_typs consts_typs
   1.340 +	    let val weight = clause_weight const_tab goals_consts_typs consts_typs
   1.341  		val ccc = (clstm, (consts_typs,weight))
   1.342  	    in
   1.343 -	      if pass <= weight 
   1.344 +	      if !pass_mark <= weight 
   1.345  	      then relevant y (ccc::ax, r)
   1.346  	      else relevant y (ax, ccc::r)
   1.347  	    end
   1.348        val (rel_clauses,nrel_clauses) =
   1.349  	  relevant (map (pair_consts_typs_axiom thy) axioms) ([],[]) 
   1.350 -      val (ax,r) = relevant_clauses_ax_3 const_tab rel_clauses nrel_clauses pass ([],[]) []
   1.351 -      val ax' = Library.take(!max_filtered, Library.sort axiom_ord ax)
   1.352 +      val (ax,r) = relevant_clauses const_tab rel_clauses nrel_clauses ([],[]) []
   1.353 +      val max_filtered = floor (!reduction_factor * real (length ax))
   1.354 +      val ax' = Library.take(max_filtered, Library.sort axiom_ord ax)
   1.355    in
   1.356        if !Output.show_debug_msgs then
   1.357  	   (List.app showconst (Symtab.dest const_tab);
   1.358  	    List.app showax ax)
   1.359        else ();
   1.360 -      if !add_unit then (filter safe_unit_clause r) @ ax'
   1.361 +      if !add_unit then (filter good_unit_clause r) @ ax'
   1.362        else ax'
   1.363    end;
   1.364  
   1.365 -fun relevance_filter3 thy axioms goals =
   1.366 -  map #1 (relevance_filter3_aux thy axioms goals);
   1.367 +fun relevance_filter thy axioms goals =
   1.368 +  map #1 (relevance_filter_aux thy axioms goals);
   1.369      
   1.370  
   1.371 -(******************************************************************)
   1.372 -(* Generic functions for relevance filtering                      *)
   1.373 -(******************************************************************)
   1.374 -
   1.375 -exception RELEVANCE_FILTER of string;
   1.376 -
   1.377 -fun relevance_filter thy axioms goals = 
   1.378 -  case (!strategy) of 1 => relevance_filter1 axioms goals
   1.379 -		    | 2 => relevance_filter2 axioms goals
   1.380 -		    | 3 => relevance_filter3 thy axioms goals
   1.381 -		    | _ => raise RELEVANCE_FILTER("strategy doesn't exist");
   1.382 -
   1.383  end;
   1.384 \ No newline at end of file