src/HOL/Tools/ATP/reduce_axiomsN.ML
changeset 19231 c8879dd3a953
parent 19212 ec53c138277a
child 19315 b218cc3d1bb4
     1.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Fri Mar 10 04:03:48 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Fri Mar 10 12:27:36 2006 +0100
     1.3 @@ -6,7 +6,8 @@
     1.4  struct
     1.5  
     1.6  val pass_mark = ref 0.5;
     1.7 -val strategy = ref 1;
     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 @@ -36,6 +37,8 @@
    1.14  
    1.15  fun term_consts_rm ncs t = add_term_consts_rm ncs t [];
    1.16  
    1.17 +(*Including equality in this list might be expected to stop rules like subset_antisym from
    1.18 +  being chosen, but for some reason filtering works better with them listed.*)
    1.19  val standard_consts =
    1.20    ["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->","op =","==","True","False"];
    1.21  
    1.22 @@ -189,7 +192,7 @@
    1.23  (******************************************************************)
    1.24  
    1.25  (*** unit clauses ***)
    1.26 -datatype clause_type = Unit_neq | Unit_geq | Other
    1.27 +datatype clause_kind = Unit_neq | Unit_geq | Other
    1.28  
    1.29  (*Whether all "simple" unit clauses should be included*)
    1.30  val add_unit = ref true;
    1.31 @@ -207,13 +210,14 @@
    1.32  fun unit_clause_type (Const ("op =",_) $ P $ Q) = eq_clause_type (P,Q)
    1.33    | unit_clause_type _ = Unit_neq;
    1.34  
    1.35 -fun clause_type tm = 
    1.36 +fun clause_kind tm = 
    1.37      case literals_of_term [] tm of
    1.38          [lit] => unit_clause_type lit
    1.39        | _ => Other;
    1.40  
    1.41  (*** constants with types ***)
    1.42  
    1.43 +(*An abstraction of Isabelle types*)
    1.44  datatype const_typ =  CTVar | CType of string * const_typ list
    1.45  
    1.46  fun uni_type (CType(con1,args1)) (CType(con2,args2)) = con1=con2 andalso uni_types args1 args2
    1.47 @@ -224,15 +228,15 @@
    1.48    | uni_types (a1::as1) (a2::as2) = uni_type a1 a2 andalso uni_types as1 as2;
    1.49  
    1.50  
    1.51 -fun uni_constants (c1,ctp1) (c2,ctp2) = (c1 = c2) andalso (uni_types ctp1 ctp2);
    1.52 +fun uni_constants (c1,ctp1) (c2,ctp2) = (c1=c2) andalso uni_types ctp1 ctp2;
    1.53  
    1.54  fun uni_mem _ [] = false
    1.55    | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) =
    1.56        uni_constants (c1,c_typ1) (c,c_typ) orelse uni_mem (c,c_typ) ctyps;
    1.57  
    1.58 -fun const_typ_of (Type (c,typs)) = CType (c,map const_typ_of typs) 
    1.59 -  | const_typ_of (TFree(_,_)) = CTVar
    1.60 -  | const_typ_of (TVar(_,_)) = CTVar
    1.61 +fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 
    1.62 +  | const_typ_of (TFree _) = CTVar
    1.63 +  | const_typ_of (TVar _) = CTVar
    1.64  
    1.65  
    1.66  fun const_w_typ thy (c,typ) = 
    1.67 @@ -252,19 +256,39 @@
    1.68  
    1.69  fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs)
    1.70  
    1.71 -fun lookup_or_zero (c,tab) =
    1.72 -    case Symtab.lookup tab c of
    1.73 -        NONE => 0
    1.74 -      | SOME n => n
    1.75 +
    1.76 +(**** Constant / Type Frequencies ****)
    1.77 +
    1.78 +local
    1.79 +
    1.80 +fun cons_nr CTVar = 0
    1.81 +  | cons_nr (CType _) = 1;
    1.82 +
    1.83 +in
    1.84 +
    1.85 +fun const_typ_ord TU =
    1.86 +  case TU of
    1.87 +    (CType (a, Ts), CType (b, Us)) =>
    1.88 +      (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
    1.89 +  | (T, U) => int_ord (cons_nr T, cons_nr U);
    1.90  
    1.91 -fun count_term_consts (Const(c,_), tab) =
    1.92 -      Symtab.update (c, 1 + lookup_or_zero (c,tab)) tab
    1.93 -  | count_term_consts (t $ u, tab) =
    1.94 -      count_term_consts (t, count_term_consts (u, tab))
    1.95 -  | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
    1.96 -  | count_term_consts (_, tab) = tab;
    1.97 +end;
    1.98 +
    1.99 +structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
   1.100  
   1.101 -fun count_axiom_consts ((tm,_), tab) = count_term_consts (tm, tab);
   1.102 +fun count_axiom_consts thy ((tm,_), tab) = 
   1.103 +  let fun count_term_consts (Const cT, tab) =
   1.104 +	    let val (c, cts) = const_w_typ thy cT
   1.105 +		val cttab = Option.getOpt (Symtab.lookup tab c, CTtab.empty)
   1.106 +		val n = Option.getOpt (CTtab.lookup cttab cts, 0)
   1.107 +	    in 
   1.108 +		Symtab.update (c, CTtab.update (cts, n+1) cttab) tab
   1.109 +            end
   1.110 +	| count_term_consts (t $ u, tab) =
   1.111 +	    count_term_consts (t, count_term_consts (u, tab))
   1.112 +	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
   1.113 +	| count_term_consts (_, tab) = tab
   1.114 +  in  count_term_consts (tm, tab) end;
   1.115  
   1.116  
   1.117  (******** filter clauses ********)
   1.118 @@ -272,28 +296,35 @@
   1.119  (*The default ignores the constant-count and gives the old Strategy 3*)
   1.120  val weight_fn = ref (fn x : real => 1.0);
   1.121  
   1.122 -fun add_ct_weight ctab ((c,_), w) =
   1.123 -  w + !weight_fn (100.0 / real (Option.valOf (Symtab.lookup ctab c)));
   1.124 +fun const_weight ctab (c, cts) =
   1.125 +  let val pairs = CTtab.dest (Option.valOf (Symtab.lookup ctab c))
   1.126 +      fun add ((cts',m), n) = if uni_types cts cts' then m+n else n
   1.127 +  in  List.foldl add 0 pairs  end;
   1.128 +
   1.129 +fun add_ct_weight ctab ((c,T), w) =
   1.130 +  w + !weight_fn (real (const_weight ctab (c,T)));
   1.131  
   1.132  fun consts_typs_weight ctab =
   1.133      List.foldl (add_ct_weight ctab) 0.0;
   1.134  
   1.135 +(*Relevant constants are weighted according to frequency, 
   1.136 +  but irrelevant constants are simply counted. Otherwise, Skolem functions,
   1.137 +  which are rare, would harm a clause's chances of being picked.*)
   1.138  fun clause_weight_s_3 ctab gctyps consts_typs =
   1.139      let val rel = filter (fn s => uni_mem s gctyps) consts_typs
   1.140 +        val rel_weight = consts_typs_weight ctab rel
   1.141      in
   1.142 -	(consts_typs_weight ctab rel) / (consts_typs_weight ctab consts_typs)
   1.143 +	rel_weight / (rel_weight + real (length consts_typs - length rel))
   1.144      end;
   1.145  
   1.146 -fun find_clause_weight_s_3_alt ctab consts_typs (_,(refconsts_typs,wa)) =
   1.147 -    wa * clause_weight_s_3 ctab refconsts_typs consts_typs;
   1.148 -
   1.149  fun relevant_clauses_ax_3 ctab rel_axs [] P (addc,tmpc) keep =
   1.150        if null addc orelse null tmpc 
   1.151        then (addc @ rel_axs @ keep, tmpc)   (*termination!*)
   1.152        else relevant_clauses_ax_3 ctab addc tmpc P ([],[]) (rel_axs @ keep)
   1.153    | relevant_clauses_ax_3 ctab rel_axs ((clstm,(consts_typs,weight))::e_axs) P (addc,tmpc) keep =
   1.154 -      let val weights = map (find_clause_weight_s_3_alt ctab consts_typs) rel_axs
   1.155 -          val weight' = List.foldl Real.max weight weights
   1.156 +      let fun clause_weight_ax (_,(refconsts_typs,wa)) =
   1.157 +              wa * clause_weight_s_3 ctab refconsts_typs consts_typs;
   1.158 +          val weight' = List.foldl Real.max weight (map clause_weight_ax rel_axs)
   1.159  	  val e_ax' = (clstm, (consts_typs,weight'))
   1.160        in
   1.161  	if P <= weight' 
   1.162 @@ -301,35 +332,51 @@
   1.163  	else relevant_clauses_ax_3 ctab rel_axs e_axs P (addc, e_ax'::tmpc) keep
   1.164        end;
   1.165  
   1.166 -fun weight_of_axiom thy (tm,name) =
   1.167 +fun pair_consts_typs_axiom thy (tm,name) =
   1.168      ((tm,name), (consts_typs_of_term thy tm));
   1.169  
   1.170 -fun safe_unit_clause ((clstm,_), _) = 
   1.171 -      case clause_type clstm of
   1.172 +fun safe_unit_clause ((t,_), _) = 
   1.173 +      case clause_kind t of
   1.174  	  Unit_neq => true
   1.175  	| Unit_geq => true
   1.176  	| Other => false;
   1.177 +	
   1.178 +fun axiom_ord ((_,(_,w1)), (_,(_,w2))) = Real.compare (w2,w1);
   1.179  
   1.180 -fun relevance_filter3_aux thy axioms goals = 
   1.181 -    let val pass = !pass_mark
   1.182 -	val const_tab = List.foldl count_axiom_consts Symtab.empty axioms
   1.183 -	val goals_consts_typs = get_goal_consts_typs thy goals
   1.184 -	fun relevant [] (ax,r) = (ax,r)
   1.185 -	  | relevant ((clstm,consts_typs)::y) (ax,r) =
   1.186 -	      let val weight = clause_weight_s_3 const_tab goals_consts_typs consts_typs
   1.187 -		  val ccc = (clstm, (consts_typs,weight))
   1.188 -	      in
   1.189 -		if pass <= weight 
   1.190 -		then relevant y (ccc::ax, r)
   1.191 -		else relevant y (ax, ccc::r)
   1.192 -	      end
   1.193 -	val (rel_clauses,nrel_clauses) =
   1.194 -	    relevant (map (weight_of_axiom thy) axioms) ([],[]) 
   1.195 -	val (ax,r) = relevant_clauses_ax_3 const_tab rel_clauses nrel_clauses pass ([],[]) []
   1.196 -    in
   1.197 -	if !add_unit then (filter safe_unit_clause r) @ ax 
   1.198 -	else ax
   1.199 -    end;
   1.200 +fun showconst (c,cttab) = 
   1.201 +      List.app (fn n => Output.debug (Int.toString n ^ " occurrences of " ^ c))
   1.202 +	        (map #2 (CTtab.dest cttab))
   1.203 +
   1.204 +fun show_cname (name,k) = name ^ "__" ^ Int.toString k;
   1.205 +
   1.206 +fun showax ((_,cname), (_,w)) = 
   1.207 +    Output.debug ("Axiom " ^ show_cname cname ^ " has weight " ^ Real.toString w)
   1.208 +	      
   1.209 +	      fun relevance_filter3_aux thy axioms goals = 
   1.210 +  let val pass = !pass_mark
   1.211 +      val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
   1.212 +      val goals_consts_typs = get_goal_consts_typs thy goals
   1.213 +      fun relevant [] (ax,r) = (ax,r)
   1.214 +	| relevant ((clstm,consts_typs)::y) (ax,r) =
   1.215 +	    let val weight = clause_weight_s_3 const_tab goals_consts_typs consts_typs
   1.216 +		val ccc = (clstm, (consts_typs,weight))
   1.217 +	    in
   1.218 +	      if pass <= weight 
   1.219 +	      then relevant y (ccc::ax, r)
   1.220 +	      else relevant y (ax, ccc::r)
   1.221 +	    end
   1.222 +      val (rel_clauses,nrel_clauses) =
   1.223 +	  relevant (map (pair_consts_typs_axiom thy) axioms) ([],[]) 
   1.224 +      val (ax,r) = relevant_clauses_ax_3 const_tab rel_clauses nrel_clauses pass ([],[]) []
   1.225 +      val ax' = Library.take(!max_filtered, Library.sort axiom_ord ax)
   1.226 +  in
   1.227 +      if !Output.show_debug_msgs then
   1.228 +	   (List.app showconst (Symtab.dest const_tab);
   1.229 +	    List.app showax ax)
   1.230 +      else ();
   1.231 +      if !add_unit then (filter safe_unit_clause r) @ ax'
   1.232 +      else ax'
   1.233 +  end;
   1.234  
   1.235  fun relevance_filter3 thy axioms goals =
   1.236    map #1 (relevance_filter3_aux thy axioms goals);