src/HOL/Tools/ATP/reduce_axiomsN.ML
changeset 19212 ec53c138277a
parent 19208 3e8006cbc925
child 19231 c8879dd3a953
     1.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Mar 08 10:06:31 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Mar 08 10:19:57 2006 +0100
     1.3 @@ -235,14 +235,12 @@
     1.4    | const_typ_of (TVar(_,_)) = CTVar
     1.5  
     1.6  
     1.7 -fun const_w_typ thy (c,tp) = 
     1.8 -    let val tvars = Sign.const_typargs thy (c,tp)
     1.9 -    in
    1.10 -	(c,map const_typ_of tvars)
    1.11 -    end;
    1.12 +fun const_w_typ thy (c,typ) = 
    1.13 +    let val tvars = Sign.const_typargs thy (c,typ)
    1.14 +    in (c, map const_typ_of tvars) end;
    1.15  
    1.16 -fun add_term_consts_typs_rm thy ncs (Const(c, tp)) cs =
    1.17 -      if (c mem ncs) then cs else (const_w_typ thy (c,tp) ins cs)
    1.18 +fun add_term_consts_typs_rm thy ncs (Const(c, typ)) cs =
    1.19 +      if (c mem ncs) then cs else (const_w_typ thy (c,typ) ins cs)
    1.20    | add_term_consts_typs_rm thy ncs (t $ u) cs =
    1.21        add_term_consts_typs_rm thy ncs  t (add_term_consts_typs_rm thy ncs u cs)
    1.22    | add_term_consts_typs_rm thy ncs (Abs(_,_,t)) cs = add_term_consts_typs_rm thy ncs t cs
    1.23 @@ -254,68 +252,87 @@
    1.24  
    1.25  fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs)
    1.26  
    1.27 +fun lookup_or_zero (c,tab) =
    1.28 +    case Symtab.lookup tab c of
    1.29 +        NONE => 0
    1.30 +      | SOME n => n
    1.31 +
    1.32 +fun count_term_consts (Const(c,_), tab) =
    1.33 +      Symtab.update (c, 1 + lookup_or_zero (c,tab)) tab
    1.34 +  | count_term_consts (t $ u, tab) =
    1.35 +      count_term_consts (t, count_term_consts (u, tab))
    1.36 +  | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
    1.37 +  | count_term_consts (_, tab) = tab;
    1.38 +
    1.39 +fun count_axiom_consts ((tm,_), tab) = count_term_consts (tm, tab);
    1.40 +
    1.41  
    1.42  (******** filter clauses ********)
    1.43  
    1.44 -fun find_clause_weight_s_3 gctyps consts_typs wa =
    1.45 +(*The default ignores the constant-count and gives the old Strategy 3*)
    1.46 +val weight_fn = ref (fn x : real => 1.0);
    1.47 +
    1.48 +fun add_ct_weight ctab ((c,_), w) =
    1.49 +  w + !weight_fn (100.0 / real (Option.valOf (Symtab.lookup ctab c)));
    1.50 +
    1.51 +fun consts_typs_weight ctab =
    1.52 +    List.foldl (add_ct_weight ctab) 0.0;
    1.53 +
    1.54 +fun clause_weight_s_3 ctab gctyps consts_typs =
    1.55      let val rel = filter (fn s => uni_mem s gctyps) consts_typs
    1.56      in
    1.57 -	(real (length rel) / real (length consts_typs)) * wa
    1.58 +	(consts_typs_weight ctab rel) / (consts_typs_weight ctab consts_typs)
    1.59      end;
    1.60  
    1.61 -fun relevant_clauses_ax_g_3 _ [] _ (ax,r) = (ax,r)
    1.62 -  | relevant_clauses_ax_g_3 gctyps ((cls_typ,(clstm,(consts_typs,_)))::y) P (ax,r) =
    1.63 -      let val weight = find_clause_weight_s_3 gctyps consts_typs 1.0
    1.64 -          val ccc = (cls_typ, (clstm, (consts_typs,weight)))
    1.65 -      in
    1.66 -	if P <= weight 
    1.67 -	then relevant_clauses_ax_g_3 gctyps y P (ccc::ax, r)
    1.68 -	else relevant_clauses_ax_g_3 gctyps y P (ax, ccc::r)
    1.69 -      end;
    1.70 +fun find_clause_weight_s_3_alt ctab consts_typs (_,(refconsts_typs,wa)) =
    1.71 +    wa * clause_weight_s_3 ctab refconsts_typs consts_typs;
    1.72  
    1.73 -fun find_clause_weight_s_3_alt consts_typs (_,(_,(refconsts_typs,wa))) =
    1.74 -    find_clause_weight_s_3 refconsts_typs consts_typs wa;
    1.75 -
    1.76 -fun relevant_clauses_ax_3 rel_axs [] P (addc,tmpc) keep =
    1.77 +fun relevant_clauses_ax_3 ctab rel_axs [] P (addc,tmpc) keep =
    1.78        if null addc orelse null tmpc 
    1.79        then (addc @ rel_axs @ keep, tmpc)   (*termination!*)
    1.80 -      else relevant_clauses_ax_3 addc tmpc P ([],[]) (rel_axs @ keep)
    1.81 -  | relevant_clauses_ax_3 rel_axs ((cls_typ,(clstm,(consts_typs,weight)))::e_axs) P (addc,tmpc) keep =
    1.82 -      let val weights = map (find_clause_weight_s_3_alt consts_typs) rel_axs
    1.83 +      else relevant_clauses_ax_3 ctab addc tmpc P ([],[]) (rel_axs @ keep)
    1.84 +  | relevant_clauses_ax_3 ctab rel_axs ((clstm,(consts_typs,weight))::e_axs) P (addc,tmpc) keep =
    1.85 +      let val weights = map (find_clause_weight_s_3_alt ctab consts_typs) rel_axs
    1.86            val weight' = List.foldl Real.max weight weights
    1.87 -	  val e_ax' = (cls_typ,(clstm,(consts_typs,weight')))
    1.88 +	  val e_ax' = (clstm, (consts_typs,weight'))
    1.89        in
    1.90 -	if P <= weight' then relevant_clauses_ax_3 rel_axs e_axs P (e_ax'::addc,tmpc) keep
    1.91 -	else relevant_clauses_ax_3 rel_axs e_axs P (addc,e_ax'::tmpc) keep
    1.92 +	if P <= weight' 
    1.93 +	then relevant_clauses_ax_3 ctab rel_axs e_axs P (e_ax'::addc, tmpc) keep
    1.94 +	else relevant_clauses_ax_3 ctab rel_axs e_axs P (addc, e_ax'::tmpc) keep
    1.95        end;
    1.96  
    1.97 -fun initialize3 thy [] ax_weights = ax_weights
    1.98 -  | initialize3 thy ((tm,name)::tms_names) ax_weights =
    1.99 -    let val cls_type = clause_type tm
   1.100 -	val consts = consts_typs_of_term thy tm
   1.101 -    in
   1.102 -	initialize3 thy tms_names ((cls_type,((tm,name),(consts,0.0)))::ax_weights)
   1.103 -    end;
   1.104 +fun weight_of_axiom thy (tm,name) =
   1.105 +    ((tm,name), (consts_typs_of_term thy tm));
   1.106  
   1.107 -fun add_unit_clauses ax [] = ax
   1.108 -  | add_unit_clauses ax ((cls_typ,consts_weight)::cs) =
   1.109 -    case cls_typ of Unit_neq => add_unit_clauses ((cls_typ,consts_weight)::ax) cs
   1.110 -		  | Unit_geq => add_unit_clauses ((cls_typ,consts_weight)::ax) cs
   1.111 -		  | Other => add_unit_clauses ax cs;
   1.112 +fun safe_unit_clause ((clstm,_), _) = 
   1.113 +      case clause_type clstm of
   1.114 +	  Unit_neq => true
   1.115 +	| Unit_geq => true
   1.116 +	| Other => false;
   1.117  
   1.118  fun relevance_filter3_aux thy axioms goals = 
   1.119      let val pass = !pass_mark
   1.120 -	val axioms_weights = initialize3 thy axioms []
   1.121 +	val const_tab = List.foldl count_axiom_consts Symtab.empty axioms
   1.122  	val goals_consts_typs = get_goal_consts_typs thy goals
   1.123 +	fun relevant [] (ax,r) = (ax,r)
   1.124 +	  | relevant ((clstm,consts_typs)::y) (ax,r) =
   1.125 +	      let val weight = clause_weight_s_3 const_tab goals_consts_typs consts_typs
   1.126 +		  val ccc = (clstm, (consts_typs,weight))
   1.127 +	      in
   1.128 +		if pass <= weight 
   1.129 +		then relevant y (ccc::ax, r)
   1.130 +		else relevant y (ax, ccc::r)
   1.131 +	      end
   1.132  	val (rel_clauses,nrel_clauses) =
   1.133 -	    relevant_clauses_ax_g_3 goals_consts_typs axioms_weights pass ([],[]) 
   1.134 -	val (ax,r) = relevant_clauses_ax_3 rel_clauses nrel_clauses pass ([],[]) []
   1.135 +	    relevant (map (weight_of_axiom thy) axioms) ([],[]) 
   1.136 +	val (ax,r) = relevant_clauses_ax_3 const_tab rel_clauses nrel_clauses pass ([],[]) []
   1.137      in
   1.138 -	if !add_unit then add_unit_clauses ax r else ax
   1.139 +	if !add_unit then (filter safe_unit_clause r) @ ax 
   1.140 +	else ax
   1.141      end;
   1.142  
   1.143  fun relevance_filter3 thy axioms goals =
   1.144 -  map (#1 o #2) (relevance_filter3_aux thy axioms goals);
   1.145 +  map #1 (relevance_filter3_aux thy axioms goals);
   1.146      
   1.147  
   1.148  (******************************************************************)