src/HOL/Tools/res_atp.ML
changeset 24287 c857dac06da6
parent 24286 7619080e49f0
child 24300 e170cee91c66
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Aug 15 12:52:56 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Aug 15 13:50:47 2007 +0200
     1.3 @@ -23,6 +23,11 @@
     1.4    val include_all: bool ref
     1.5    val run_relevance_filter: bool ref
     1.6    val run_blacklist_filter: bool ref
     1.7 +  val theory_const : bool ref
     1.8 +  val pass_mark    : real ref
     1.9 +  val convergence  : real ref
    1.10 +  val max_new      : int ref
    1.11 +  val follow_defs  : bool ref
    1.12    val add_all : unit -> unit
    1.13    val add_claset : unit -> unit
    1.14    val add_simpset : unit -> unit
    1.15 @@ -50,22 +55,31 @@
    1.16  (********************************************************************)
    1.17  
    1.18  (*** background linkup ***)
    1.19 +val run_blacklist_filter = ref true;
    1.20  val time_limit = ref 60;
    1.21  val prover = ref "";
    1.22  
    1.23 +(*** relevance filter parameters ***)
    1.24 +val run_relevance_filter = ref true;
    1.25 +val theory_const = ref true;
    1.26 +val pass_mark = ref 0.5;
    1.27 +val convergence = ref 3.2;    (*Higher numbers allow longer inference chains*)
    1.28 +val max_new = ref 60;         (*Limits how many clauses can be picked up per stage*)
    1.29 +val follow_defs = ref false;  (*Follow definitions. Makes problems bigger.*)
    1.30 +
    1.31  fun set_prover atp =
    1.32    case String.map Char.toLower atp of
    1.33        "e" =>
    1.34 -          (ReduceAxiomsN.max_new := 100;
    1.35 -           ReduceAxiomsN.theory_const := false;
    1.36 +          (max_new := 100;
    1.37 +           theory_const := false;
    1.38             prover := "E")
    1.39      | "spass" =>
    1.40 -          (ReduceAxiomsN.max_new := 40;
    1.41 -           ReduceAxiomsN.theory_const := true;
    1.42 +          (max_new := 40;
    1.43 +           theory_const := true;
    1.44             prover := "spass")
    1.45      | "vampire" =>
    1.46 -          (ReduceAxiomsN.max_new := 60;
    1.47 -           ReduceAxiomsN.theory_const := false;
    1.48 +          (max_new := 60;
    1.49 +           theory_const := false;
    1.50             prover := "vampire")
    1.51      | _ => error ("No such prover: " ^ atp);
    1.52  
    1.53 @@ -108,7 +122,7 @@
    1.54  val include_atpset = ref true;
    1.55  
    1.56  (*Tests show that follow_defs gives VERY poor results with "include_all"*)
    1.57 -fun add_all() = (include_all:=true; ReduceAxiomsN.follow_defs := false);
    1.58 +fun add_all() = (include_all:=true; follow_defs := false);
    1.59  fun rm_all() = include_all:=false;
    1.60  
    1.61  fun add_simpset() = include_simpset:=true;
    1.62 @@ -124,10 +138,6 @@
    1.63  fun rm_atpset() = include_atpset:=false;
    1.64  
    1.65  
    1.66 -(**** relevance filter ****)
    1.67 -val run_relevance_filter = ReduceAxiomsN.run_relevance_filter;
    1.68 -val run_blacklist_filter = ref true;
    1.69 -
    1.70  (******************************************************************)
    1.71  (* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
    1.72  (******************************************************************)
    1.73 @@ -251,6 +261,251 @@
    1.74  fun is_fol_thms ths = ((fst(logic_of_clauses (map prop_of ths) (FOL,[]))) = FOL);
    1.75  
    1.76  (***************************************************************)
    1.77 +(* Relevance Filtering                                         *)
    1.78 +(***************************************************************)
    1.79 +
    1.80 +(*A surprising number of theorems contain only a few significant constants.
    1.81 +  These include all induction rules, and other general theorems. Filtering
    1.82 +  theorems in clause form reveals these complexities in the form of Skolem 
    1.83 +  functions. If we were instead to filter theorems in their natural form,
    1.84 +  some other method of measuring theorem complexity would become necessary.*)
    1.85 +
    1.86 +fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0);
    1.87 +
    1.88 +(*The default seems best in practice. A constant function of one ignores
    1.89 +  the constant frequencies.*)
    1.90 +val weight_fn = ref log_weight2;
    1.91 +
    1.92 +
    1.93 +(*Including equality in this list might be expected to stop rules like subset_antisym from
    1.94 +  being chosen, but for some reason filtering works better with them listed. The
    1.95 +  logical signs All, Ex, &, and --> are omitted because any remaining occurrrences
    1.96 +  must be within comprehensions.*)
    1.97 +val standard_consts = ["Trueprop","==>","all","==","op |","Not","op ="];
    1.98 +
    1.99 +
   1.100 +(*** constants with types ***)
   1.101 +
   1.102 +(*An abstraction of Isabelle types*)
   1.103 +datatype const_typ =  CTVar | CType of string * const_typ list
   1.104 +
   1.105 +(*Is the second type an instance of the first one?*)
   1.106 +fun match_type (CType(con1,args1)) (CType(con2,args2)) = 
   1.107 +      con1=con2 andalso match_types args1 args2
   1.108 +  | match_type CTVar _ = true
   1.109 +  | match_type _ CTVar = false
   1.110 +and match_types [] [] = true
   1.111 +  | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
   1.112 +
   1.113 +(*Is there a unifiable constant?*)
   1.114 +fun uni_mem gctab (c,c_typ) =
   1.115 +  case Symtab.lookup gctab c of
   1.116 +      NONE => false
   1.117 +    | SOME ctyps_list => exists (match_types c_typ) ctyps_list;
   1.118 +  
   1.119 +(*Maps a "real" type to a const_typ*)
   1.120 +fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 
   1.121 +  | const_typ_of (TFree _) = CTVar
   1.122 +  | const_typ_of (TVar _) = CTVar
   1.123 +
   1.124 +(*Pairs a constant with the list of its type instantiations (using const_typ)*)
   1.125 +fun const_with_typ thy (c,typ) = 
   1.126 +    let val tvars = Sign.const_typargs thy (c,typ)
   1.127 +    in (c, map const_typ_of tvars) end
   1.128 +    handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)   
   1.129 +
   1.130 +(*Add a const/type pair to the table, but a [] entry means a standard connective,
   1.131 +  which we ignore.*)
   1.132 +fun add_const_typ_table ((c,ctyps), tab) =
   1.133 +  Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => insert (op =) ctyps ctyps_list) 
   1.134 +    tab;
   1.135 +
   1.136 +(*Free variables are included, as well as constants, to handle locales*)
   1.137 +fun add_term_consts_typs_rm thy (Const(c, typ), tab) =
   1.138 +      add_const_typ_table (const_with_typ thy (c,typ), tab) 
   1.139 +  | add_term_consts_typs_rm thy (Free(c, typ), tab) =
   1.140 +      add_const_typ_table (const_with_typ thy (c,typ), tab) 
   1.141 +  | add_term_consts_typs_rm thy (t $ u, tab) =
   1.142 +      add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab))
   1.143 +  | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab)
   1.144 +  | add_term_consts_typs_rm thy (_, tab) = tab;
   1.145 +
   1.146 +(*The empty list here indicates that the constant is being ignored*)
   1.147 +fun add_standard_const (s,tab) = Symtab.update (s,[]) tab;
   1.148 +
   1.149 +val null_const_tab : const_typ list list Symtab.table = 
   1.150 +    foldl add_standard_const Symtab.empty standard_consts;
   1.151 +
   1.152 +fun get_goal_consts_typs thy = foldl (add_term_consts_typs_rm thy) null_const_tab;
   1.153 +
   1.154 +(*Inserts a dummy "constant" referring to the theory name, so that relevance
   1.155 +  takes the given theory into account.*)
   1.156 +fun const_prop_of th =
   1.157 + if !theory_const then
   1.158 +  let val name = Context.theory_name (theory_of_thm th)
   1.159 +      val t = Const (name ^ ". 1", HOLogic.boolT)
   1.160 +  in  t $ prop_of th  end
   1.161 + else prop_of th;
   1.162 +
   1.163 +(**** Constant / Type Frequencies ****)
   1.164 +
   1.165 +(*A two-dimensional symbol table counts frequencies of constants. It's keyed first by
   1.166 +  constant name and second by its list of type instantiations. For the latter, we need
   1.167 +  a linear ordering on type const_typ list.*)
   1.168 +  
   1.169 +local
   1.170 +
   1.171 +fun cons_nr CTVar = 0
   1.172 +  | cons_nr (CType _) = 1;
   1.173 +
   1.174 +in
   1.175 +
   1.176 +fun const_typ_ord TU =
   1.177 +  case TU of
   1.178 +    (CType (a, Ts), CType (b, Us)) =>
   1.179 +      (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
   1.180 +  | (T, U) => int_ord (cons_nr T, cons_nr U);
   1.181 +
   1.182 +end;
   1.183 +
   1.184 +structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
   1.185 +
   1.186 +fun count_axiom_consts thy ((thm,_), tab) = 
   1.187 +  let fun count_const (a, T, tab) =
   1.188 +	let val (c, cts) = const_with_typ thy (a,T)
   1.189 +	in  (*Two-dimensional table update. Constant maps to types maps to count.*)
   1.190 +	    Symtab.map_default (c, CTtab.empty) 
   1.191 +	                       (CTtab.map_default (cts,0) (fn n => n+1)) tab
   1.192 +	end
   1.193 +      fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
   1.194 +	| count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
   1.195 +	| count_term_consts (t $ u, tab) =
   1.196 +	    count_term_consts (t, count_term_consts (u, tab))
   1.197 +	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
   1.198 +	| count_term_consts (_, tab) = tab
   1.199 +  in  count_term_consts (const_prop_of thm, tab)  end;
   1.200 +
   1.201 +
   1.202 +(**** Actual Filtering Code ****)
   1.203 +
   1.204 +(*The frequency of a constant is the sum of those of all instances of its type.*)
   1.205 +fun const_frequency ctab (c, cts) =
   1.206 +  let val pairs = CTtab.dest (the (Symtab.lookup ctab c))
   1.207 +      fun add ((cts',m), n) = if match_types cts cts' then m+n else n
   1.208 +  in  List.foldl add 0 pairs  end;
   1.209 +
   1.210 +(*Add in a constant's weight, as determined by its frequency.*)
   1.211 +fun add_ct_weight ctab ((c,T), w) =
   1.212 +  w + !weight_fn (real (const_frequency ctab (c,T)));
   1.213 +
   1.214 +(*Relevant constants are weighted according to frequency, 
   1.215 +  but irrelevant constants are simply counted. Otherwise, Skolem functions,
   1.216 +  which are rare, would harm a clause's chances of being picked.*)
   1.217 +fun clause_weight ctab gctyps consts_typs =
   1.218 +    let val rel = filter (uni_mem gctyps) consts_typs
   1.219 +        val rel_weight = List.foldl (add_ct_weight ctab) 0.0 rel
   1.220 +    in
   1.221 +	rel_weight / (rel_weight + real (length consts_typs - length rel))
   1.222 +    end;
   1.223 +    
   1.224 +(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
   1.225 +fun add_expand_pairs (x,ys) xys = foldl (fn (y,acc) => (x,y)::acc) xys ys;
   1.226 +
   1.227 +fun consts_typs_of_term thy t = 
   1.228 +  let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
   1.229 +  in  Symtab.fold add_expand_pairs tab []  end;
   1.230 +
   1.231 +fun pair_consts_typs_axiom thy (thm,name) =
   1.232 +    ((thm,name), (consts_typs_of_term thy (const_prop_of thm)));
   1.233 +
   1.234 +exception ConstFree;
   1.235 +fun dest_ConstFree (Const aT) = aT
   1.236 +  | dest_ConstFree (Free aT) = aT
   1.237 +  | dest_ConstFree _ = raise ConstFree;
   1.238 +
   1.239 +(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
   1.240 +fun defines thy (thm,(name,n)) gctypes =
   1.241 +    let val tm = prop_of thm
   1.242 +	fun defs lhs rhs =
   1.243 +            let val (rator,args) = strip_comb lhs
   1.244 +		val ct = const_with_typ thy (dest_ConstFree rator)
   1.245 +            in  forall is_Var args andalso uni_mem gctypes ct andalso
   1.246 +                Term.add_vars rhs [] subset Term.add_vars lhs []
   1.247 +            end
   1.248 +	    handle ConstFree => false
   1.249 +    in    
   1.250 +	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 
   1.251 +		   defs lhs rhs andalso
   1.252 +		   (Output.debug (fn () => "Definition found: " ^ name ^ "_" ^ Int.toString n); true)
   1.253 +		 | _ => false
   1.254 +    end;
   1.255 +
   1.256 +type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
   1.257 +       
   1.258 +(*For a reverse sort, putting the largest values first.*)
   1.259 +fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1);
   1.260 +
   1.261 +(*Limit the number of new clauses, to prevent runaway acceptance.*)
   1.262 +fun take_best (newpairs : (annotd_cls*real) list) =
   1.263 +  let val nnew = length newpairs
   1.264 +  in
   1.265 +    if nnew <= !max_new then (map #1 newpairs, [])
   1.266 +    else 
   1.267 +      let val cls = sort compare_pairs newpairs
   1.268 +          val accepted = List.take (cls, !max_new)
   1.269 +      in
   1.270 +        Output.debug (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
   1.271 +		       ", exceeds the limit of " ^ Int.toString (!max_new)));
   1.272 +        Output.debug (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
   1.273 +        Output.debug (fn () => "Actually passed: " ^
   1.274 +          space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
   1.275 +
   1.276 +	(map #1 accepted, map #1 (List.drop (cls, !max_new)))
   1.277 +      end
   1.278 +  end;
   1.279 +
   1.280 +fun relevant_clauses thy ctab p rel_consts =
   1.281 +  let fun relevant ([],_) [] = [] : (thm * (string * int)) list  (*Nothing added this iteration*)
   1.282 +	| relevant (newpairs,rejects) [] =
   1.283 +	    let val (newrels,more_rejects) = take_best newpairs
   1.284 +		val new_consts = List.concat (map #2 newrels)
   1.285 +		val rel_consts' = foldl add_const_typ_table rel_consts new_consts
   1.286 +		val newp = p + (1.0-p) / !convergence
   1.287 +	    in
   1.288 +              Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
   1.289 +	       (map #1 newrels) @ 
   1.290 +	       (relevant_clauses thy ctab newp rel_consts' (more_rejects@rejects))
   1.291 +	    end
   1.292 +	| relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
   1.293 +	    let val weight = clause_weight ctab rel_consts consts_typs
   1.294 +	    in
   1.295 +	      if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts)
   1.296 +	      then (Output.debug (fn () => (name ^ " clause " ^ Int.toString n ^ 
   1.297 +	                                    " passes: " ^ Real.toString weight));
   1.298 +	            relevant ((ax,weight)::newrels, rejects) axs)
   1.299 +	      else relevant (newrels, ax::rejects) axs
   1.300 +	    end
   1.301 +    in  Output.debug (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
   1.302 +        relevant ([],[]) 
   1.303 +    end;
   1.304 +	
   1.305 +fun relevance_filter thy axioms goals = 
   1.306 + if !run_relevance_filter andalso !pass_mark >= 0.1
   1.307 + then
   1.308 +  let val _ = Output.debug (fn () => "Start of relevance filtering");
   1.309 +      val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
   1.310 +      val goal_const_tab = get_goal_consts_typs thy goals
   1.311 +      val _ = Output.debug (fn () => ("Initial constants: " ^
   1.312 +                                 space_implode ", " (Symtab.keys goal_const_tab)));
   1.313 +      val rels = relevant_clauses thy const_tab (!pass_mark) 
   1.314 +                   goal_const_tab  (map (pair_consts_typs_axiom thy) axioms)
   1.315 +  in
   1.316 +      Output.debug (fn () => ("Total relevant: " ^ Int.toString (length rels)));
   1.317 +      rels
   1.318 +  end
   1.319 + else axioms;
   1.320 +
   1.321 +(***************************************************************)
   1.322  (* Retrieving and filtering lemmas                             *)
   1.323  (***************************************************************)
   1.324  
   1.325 @@ -320,11 +575,6 @@
   1.326        filter (not o known) c_clauses
   1.327    end;
   1.328  
   1.329 -(*Filter axiom clauses, but keep supplied clauses and clauses in whitelist.
   1.330 -  Duplicates are removed later.*)
   1.331 -fun get_relevant_clauses thy cls_thms white_cls goals =
   1.332 -  white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
   1.333 -
   1.334  fun all_valid_thms ctxt =
   1.335    let
   1.336      fun blacklisted s = !run_blacklist_filter andalso is_package_def s
   1.337 @@ -534,7 +784,7 @@
   1.338                                       |> restrict_to_logic thy logic
   1.339                                       |> remove_unwanted_clauses
   1.340          val user_cls = ResAxioms.cnf_rules_pairs user_rules
   1.341 -        val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms)
   1.342 +        val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms)
   1.343          val subs = tfree_classes_of_terms goal_tms
   1.344          and axtms = map (prop_of o #1) axclauses
   1.345          val supers = tvar_classes_of_terms axtms
   1.346 @@ -644,7 +894,7 @@
   1.347        val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
   1.348        val white_cls = ResAxioms.cnf_rules_pairs white_thms
   1.349        (*clauses relevant to goal gl*)
   1.350 -      val axcls_list = map (fn ngcls => get_relevant_clauses thy included_cls white_cls (map prop_of ngcls)) goal_cls
   1.351 +      val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls
   1.352        val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
   1.353                    axcls_list
   1.354        val writer = if !prover = "spass" then dfg_writer else tptp_writer