pool of constants; definition expansion; current best settings
authorpaulson
Wed Apr 05 12:47:38 2006 +0200 (2006-04-05)
changeset 19337146b25b893bb
parent 19336 fb5e19d26d5e
child 19338 952b12ebfdff
pool of constants; definition expansion; current best settings
src/HOL/Tools/ATP/reduce_axiomsN.ML
     1.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Fri Mar 31 10:53:33 2006 +0200
     1.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Apr 05 12:47:38 2006 +0200
     1.3 @@ -6,10 +6,14 @@
     1.4  struct
     1.5  
     1.6  val pass_mark = ref 0.6;
     1.7 -val convergence = ref 1.6;   (*Higher numbers allow longer inference chains*)
     1.8 +val convergence = ref 2.4;   (*Higher numbers allow longer inference chains*)
     1.9 +val follow_defs = ref true;  (*Follow definitions. Makes problems bigger.*)
    1.10  
    1.11 -(*The default ignores the constant-count and gives the old Strategy 3*)
    1.12 -val weight_fn = ref (fn x : real => 1.0);
    1.13 +fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0);
    1.14 +
    1.15 +(*The default seems best in practice. A constant function of one ignores
    1.16 +  the constant frequencies.*)
    1.17 +val weight_fn = ref log_weight2;
    1.18  
    1.19  
    1.20  (*Including equality in this list might be expected to stop rules like subset_antisym from
    1.21 @@ -126,27 +130,6 @@
    1.22  fun pair_consts_typs_axiom thy (tm,name) =
    1.23      ((tm,name), (consts_typs_of_term thy tm));
    1.24  
    1.25 -fun relevant_clauses ctab p rel_consts =
    1.26 -  let fun relevant (newrels,rejects) []  =
    1.27 -	    if null newrels then [] 
    1.28 -	    else 
    1.29 -	      let val new_consts = map #2 newrels
    1.30 -	          val rel_consts' = foldl (op union) rel_consts new_consts
    1.31 -                  val newp = p + (1.0-p) / !convergence
    1.32 -	      in Output.debug ("found relevant: " ^ Int.toString (length newrels));
    1.33 -                 newrels @ relevant_clauses ctab newp rel_consts' rejects
    1.34 -	      end
    1.35 -	| relevant (newrels,rejects) ((ax as (clstm,consts_typs)) :: axs) =
    1.36 -	    let val weight = clause_weight ctab rel_consts consts_typs
    1.37 -	    in
    1.38 -	      if p <= weight 
    1.39 -	      then relevant (ax::newrels, rejects) axs
    1.40 -	      else relevant (newrels, ax::rejects) axs
    1.41 -	    end
    1.42 -    in  Output.debug ("relevant_clauses: " ^ Real.toString p);
    1.43 -        relevant ([],[]) end;
    1.44 -	
    1.45 -     
    1.46  exception ConstFree;
    1.47  fun dest_ConstFree (Const aT) = aT
    1.48    | dest_ConstFree (Free aT) = aT
    1.49 @@ -166,10 +149,31 @@
    1.50        | _ => false
    1.51    end
    1.52  
    1.53 +fun relevant_clauses thy ctab p rel_consts =
    1.54 +  let fun relevant (newrels,rejects) []  =
    1.55 +	    if null newrels then [] 
    1.56 +	    else 
    1.57 +	      let val new_consts = map #2 newrels
    1.58 +	          val rel_consts' = foldl (op union) rel_consts new_consts
    1.59 +                  val newp = p + (1.0-p) / !convergence
    1.60 +	      in Output.debug ("found relevant: " ^ Int.toString (length newrels));
    1.61 +                 newrels @ relevant_clauses thy ctab newp rel_consts' rejects
    1.62 +	      end
    1.63 +	| relevant (newrels,rejects) ((ax as (clstm,consts_typs)) :: axs) =
    1.64 +	    let val weight = clause_weight ctab rel_consts consts_typs
    1.65 +	    in
    1.66 +	      if p <= weight orelse (!follow_defs andalso defines thy clstm rel_consts)
    1.67 +	      then relevant (ax::newrels, rejects) axs
    1.68 +	      else relevant (newrels, ax::rejects) axs
    1.69 +	    end
    1.70 +    in  Output.debug ("relevant_clauses: " ^ Real.toString p);
    1.71 +        relevant ([],[]) end;
    1.72 +	
    1.73 +     
    1.74  fun relevance_filter_aux thy axioms goals = 
    1.75    let val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
    1.76        val goals_consts_typs = get_goal_consts_typs thy goals
    1.77 -      val rels = relevant_clauses const_tab (!pass_mark) goals_consts_typs 
    1.78 +      val rels = relevant_clauses thy const_tab (!pass_mark) goals_consts_typs 
    1.79                     (map (pair_consts_typs_axiom thy) axioms)
    1.80    in
    1.81        Output.debug ("Total relevant: " ^ Int.toString (length rels));
    1.82 @@ -177,7 +181,8 @@
    1.83    end;
    1.84  
    1.85  fun relevance_filter thy axioms goals =
    1.86 -  map #1 (relevance_filter_aux thy axioms goals);
    1.87 +  if !pass_mark < 0.1 then axioms
    1.88 +  else map #1 (relevance_filter_aux thy axioms goals);
    1.89      
    1.90  
    1.91  end;
    1.92 \ No newline at end of file