src/HOL/Tools/ATP/reduce_axiomsN.ML
author paulson
Fri Nov 24 16:38:42 2006 +0100 (2006-11-24)
changeset 21513 9e9fff87dc6c
parent 20854 f9cf9e62d11c
child 21677 8ce2e9ef0bd2
permissions -rw-r--r--
Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson@19208
     1
(* Authors: Jia Meng, NICTA and Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@19208
     2
   ID: $Id$
paulson@19208
     3
   Filtering strategies *)
paulson@19208
     4
paulson@20457
     5
(*A surprising number of theorems contain only a few significant constants.
paulson@20457
     6
  These include all induction rules, and other general theorems. Filtering
paulson@20457
     7
  theorems in clause form reveals these complexities in the form of Skolem 
paulson@20457
     8
  functions. If we were instead to filter theorems in their natural form,
paulson@20457
     9
  some other method of measuring theorem complexity would become necessary.*)
paulson@20457
    10
mengj@18791
    11
structure ReduceAxiomsN =
mengj@18791
    12
struct
mengj@18791
    13
paulson@20457
    14
val run_relevance_filter = ref true;
paulson@20825
    15
val theory_const = ref true;
paulson@20566
    16
val pass_mark = ref 0.5;
paulson@20566
    17
val convergence = ref 3.2;    (*Higher numbers allow longer inference chains*)
paulson@20566
    18
val max_new = ref 60;         (*Limits how many clauses can be picked up per stage*)
paulson@20423
    19
val follow_defs = ref false;  (*Follow definitions. Makes problems bigger.*)
mengj@18791
    20
paulson@19337
    21
fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0);
paulson@19337
    22
paulson@19337
    23
(*The default seems best in practice. A constant function of one ignores
paulson@19337
    24
  the constant frequencies.*)
paulson@19337
    25
val weight_fn = ref log_weight2;
paulson@19334
    26
mengj@18791
    27
paulson@19231
    28
(*Including equality in this list might be expected to stop rules like subset_antisym from
paulson@20527
    29
  being chosen, but for some reason filtering works better with them listed. The
paulson@20527
    30
  logical signs All, Ex, &, and --> are omitted because any remaining occurrrences
paulson@20527
    31
  must be within comprehensions.*)
paulson@20527
    32
val standard_consts = ["Trueprop","==>","all","==","op |","Not","op ="];
mengj@18791
    33
mengj@18791
    34
mengj@19009
    35
(*** constants with types ***)
mengj@19009
    36
paulson@19231
    37
(*An abstraction of Isabelle types*)
mengj@19009
    38
datatype const_typ =  CTVar | CType of string * const_typ list
mengj@19009
    39
paulson@20153
    40
(*Is the second type an instance of the first one?*)
paulson@20153
    41
fun match_type (CType(con1,args1)) (CType(con2,args2)) = 
paulson@20153
    42
      con1=con2 andalso match_types args1 args2
paulson@20566
    43
  | match_type CTVar _ = true
paulson@20153
    44
  | match_type _ CTVar = false
paulson@20153
    45
and match_types [] [] = true
paulson@20153
    46
  | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
mengj@19009
    47
paulson@20132
    48
(*Is there a unifiable constant?*)
paulson@20132
    49
fun uni_mem gctab (c,c_typ) =
paulson@20132
    50
  case Symtab.lookup gctab c of
paulson@20132
    51
      NONE => false
paulson@20153
    52
    | SOME ctyps_list => exists (match_types c_typ) ctyps_list;
paulson@20132
    53
  
paulson@20566
    54
(*Maps a "real" type to a const_typ*)
paulson@19231
    55
fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 
paulson@19231
    56
  | const_typ_of (TFree _) = CTVar
paulson@19231
    57
  | const_typ_of (TVar _) = CTVar
mengj@19009
    58
paulson@20566
    59
(*Pairs a constant with the list of its type instantiations (using const_typ)*)
paulson@19315
    60
fun const_with_typ thy (c,typ) = 
paulson@19212
    61
    let val tvars = Sign.const_typargs thy (c,typ)
paulson@19315
    62
    in (c, map const_typ_of tvars) end
paulson@19315
    63
    handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)   
mengj@19009
    64
paulson@20153
    65
(*Add a const/type pair to the table, but a [] entry means a standard connective,
paulson@20153
    66
  which we ignore.*)
paulson@20132
    67
fun add_const_typ_table ((c,ctyps), tab) =
haftmann@20854
    68
  Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => insert (op =) ctyps ctyps_list) 
paulson@20153
    69
    tab;
paulson@20132
    70
paulson@20566
    71
(*Free variables are included, as well as constants, to handle locales*)
paulson@20132
    72
fun add_term_consts_typs_rm thy (Const(c, typ), tab) =
paulson@20132
    73
      add_const_typ_table (const_with_typ thy (c,typ), tab) 
paulson@20132
    74
  | add_term_consts_typs_rm thy (Free(c, typ), tab) =
paulson@20132
    75
      add_const_typ_table (const_with_typ thy (c,typ), tab) 
paulson@20132
    76
  | add_term_consts_typs_rm thy (t $ u, tab) =
paulson@20132
    77
      add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab))
paulson@20132
    78
  | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab)
paulson@20132
    79
  | add_term_consts_typs_rm thy (_, tab) = tab;
mengj@19009
    80
paulson@20132
    81
(*The empty list here indicates that the constant is being ignored*)
paulson@20132
    82
fun add_standard_const (s,tab) = Symtab.update (s,[]) tab;
mengj@19009
    83
paulson@20132
    84
val null_const_tab : const_typ list list Symtab.table = 
paulson@20132
    85
    foldl add_standard_const Symtab.empty standard_consts;
paulson@20132
    86
paulson@20457
    87
fun get_goal_consts_typs thy = foldl (add_term_consts_typs_rm thy) null_const_tab;
mengj@19009
    88
paulson@20527
    89
(*Inserts a dummy "constant" referring to the theory name, so that relevance
paulson@20527
    90
  takes the given theory into account.*)
paulson@20527
    91
fun const_prop_of th =
paulson@20527
    92
 if !theory_const then
paulson@20527
    93
  let val name = Context.theory_name (theory_of_thm th)
paulson@20527
    94
      val t = Const (name ^ ". 1", HOLogic.boolT)
paulson@20527
    95
  in  t $ prop_of th  end
paulson@20527
    96
 else prop_of th;
paulson@19231
    97
paulson@19231
    98
(**** Constant / Type Frequencies ****)
paulson@19231
    99
paulson@20566
   100
(*A two-dimensional symbol table counts frequencies of constants. It's keyed first by
paulson@20566
   101
  constant name and second by its list of type instantiations. For the latter, we need
paulson@20566
   102
  a linear ordering on type const_typ list.*)
paulson@20566
   103
  
paulson@19231
   104
local
paulson@19231
   105
paulson@19231
   106
fun cons_nr CTVar = 0
paulson@19231
   107
  | cons_nr (CType _) = 1;
paulson@19231
   108
paulson@19231
   109
in
paulson@19231
   110
paulson@19231
   111
fun const_typ_ord TU =
paulson@19231
   112
  case TU of
paulson@19231
   113
    (CType (a, Ts), CType (b, Us)) =>
paulson@19231
   114
      (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
paulson@19231
   115
  | (T, U) => int_ord (cons_nr T, cons_nr U);
paulson@19212
   116
paulson@19231
   117
end;
paulson@19231
   118
paulson@19231
   119
structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
paulson@19212
   120
mengj@19355
   121
fun count_axiom_consts thy ((thm,_), tab) = 
paulson@19315
   122
  let fun count_const (a, T, tab) =
paulson@19315
   123
	let val (c, cts) = const_with_typ thy (a,T)
paulson@20153
   124
	in  (*Two-dimensional table update. Constant maps to types maps to count.*)
paulson@20153
   125
	    Symtab.map_default (c, CTtab.empty) 
paulson@20153
   126
	                       (CTtab.map_default (cts,0) (fn n => n+1)) tab
paulson@19315
   127
	end
paulson@19315
   128
      fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
paulson@19315
   129
	| count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
paulson@19231
   130
	| count_term_consts (t $ u, tab) =
paulson@19231
   131
	    count_term_consts (t, count_term_consts (u, tab))
paulson@19231
   132
	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
paulson@19231
   133
	| count_term_consts (_, tab) = tab
paulson@20527
   134
  in  count_term_consts (const_prop_of thm, tab)  end;
paulson@19212
   135
mengj@19009
   136
paulson@20566
   137
(**** Actual Filtering Code ****)
mengj@19009
   138
paulson@20566
   139
(*The frequency of a constant is the sum of those of all instances of its type.*)
paulson@20566
   140
fun const_frequency ctab (c, cts) =
paulson@19231
   141
  let val pairs = CTtab.dest (Option.valOf (Symtab.lookup ctab c))
paulson@20153
   142
      fun add ((cts',m), n) = if match_types cts cts' then m+n else n
paulson@19231
   143
  in  List.foldl add 0 pairs  end;
paulson@19231
   144
paulson@20566
   145
(*Add in a constant's weight, as determined by its frequency.*)
paulson@19231
   146
fun add_ct_weight ctab ((c,T), w) =
paulson@20566
   147
  w + !weight_fn (real (const_frequency ctab (c,T)));
paulson@19212
   148
paulson@19231
   149
(*Relevant constants are weighted according to frequency, 
paulson@19231
   150
  but irrelevant constants are simply counted. Otherwise, Skolem functions,
paulson@19231
   151
  which are rare, would harm a clause's chances of being picked.*)
paulson@19315
   152
fun clause_weight ctab gctyps consts_typs =
paulson@20132
   153
    let val rel = filter (uni_mem gctyps) consts_typs
paulson@20566
   154
        val rel_weight = List.foldl (add_ct_weight ctab) 0.0 rel
mengj@19009
   155
    in
paulson@19231
   156
	rel_weight / (rel_weight + real (length consts_typs - length rel))
mengj@19009
   157
    end;
paulson@19315
   158
    
paulson@20153
   159
(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
paulson@20566
   160
fun add_expand_pairs (x,ys) xys = foldl (fn (y,acc) => (x,y)::acc) xys ys;
paulson@20132
   161
paulson@20132
   162
fun consts_typs_of_term thy t = 
paulson@20132
   163
  let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
paulson@20153
   164
  in  Symtab.fold add_expand_pairs tab []  end;
paulson@20132
   165
mengj@19355
   166
fun pair_consts_typs_axiom thy (thm,name) =
paulson@20527
   167
    ((thm,name), (consts_typs_of_term thy (const_prop_of thm)));
mengj@19009
   168
paulson@19321
   169
exception ConstFree;
paulson@19321
   170
fun dest_ConstFree (Const aT) = aT
paulson@19321
   171
  | dest_ConstFree (Free aT) = aT
paulson@19321
   172
  | dest_ConstFree _ = raise ConstFree;
paulson@19321
   173
paulson@19321
   174
(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
mengj@19355
   175
fun defines thy (thm,(name,n)) gctypes =
mengj@19355
   176
    let val tm = prop_of thm
paulson@19448
   177
	fun defs lhs rhs =
paulson@19448
   178
            let val (rator,args) = strip_comb lhs
mengj@19355
   179
		val ct = const_with_typ thy (dest_ConstFree rator)
paulson@20153
   180
            in  forall is_Var args andalso uni_mem gctypes ct andalso
wenzelm@20197
   181
                Term.add_vars rhs [] subset Term.add_vars lhs []
paulson@19448
   182
            end
paulson@19448
   183
	    handle ConstFree => false
mengj@19355
   184
    in    
paulson@19448
   185
	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 
paulson@19448
   186
		   defs lhs rhs andalso
mengj@19355
   187
		   (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true)
mengj@19355
   188
		 | _ => false
paulson@20132
   189
    end;
paulson@19321
   190
paulson@20566
   191
(*For a reverse sort, putting the largest values first.*)
paulson@20566
   192
fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1);
paulson@20566
   193
paulson@20566
   194
(*Limit the number of new clauses, to prevent runaway acceptance.*)
paulson@20566
   195
fun take_best newpairs =
paulson@20566
   196
  let val nnew = length newpairs
paulson@20566
   197
  in
paulson@20566
   198
    if nnew <= !max_new then (map #1 newpairs, [])
paulson@20566
   199
    else 
paulson@20566
   200
      let val cls = map #1 (sort compare_pairs newpairs)
paulson@20566
   201
      in  Output.debug ("Number of candidates, " ^ Int.toString nnew ^ 
paulson@20566
   202
			", exceeds the limit of " ^ Int.toString (!max_new));
paulson@20566
   203
	  (List.take (cls, !max_new), List.drop (cls, !max_new))
paulson@20566
   204
      end
paulson@20566
   205
  end;
paulson@20566
   206
paulson@19337
   207
fun relevant_clauses thy ctab p rel_consts =
paulson@20566
   208
  let fun relevant ([],rejects) [] = []     (*Nothing added this iteration, so stop*)
paulson@20566
   209
	| relevant (newpairs,rejects) [] =
paulson@20566
   210
	    let val (newrels,more_rejeccts) = take_best newpairs
paulson@20566
   211
		val new_consts = List.concat (map #2 newrels)
paulson@20566
   212
		val rel_consts' = foldl add_const_typ_table rel_consts new_consts
paulson@20566
   213
		val newp = p + (1.0-p) / !convergence
paulson@20566
   214
	    in Output.debug ("relevant this iteration: " ^ Int.toString (length newrels));
paulson@20566
   215
	       (map #1 newrels) @ 
paulson@20566
   216
	       (relevant_clauses thy ctab newp rel_consts' (more_rejeccts@rejects))
paulson@20566
   217
	    end
paulson@20153
   218
	| relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
paulson@19337
   219
	    let val weight = clause_weight ctab rel_consts consts_typs
paulson@19337
   220
	    in
mengj@19355
   221
	      if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts)
paulson@20566
   222
	      then (Output.debug name; 
paulson@20566
   223
	            relevant ((ax,weight)::newrels, rejects) axs)
paulson@19337
   224
	      else relevant (newrels, ax::rejects) axs
paulson@19337
   225
	    end
paulson@19337
   226
    in  Output.debug ("relevant_clauses: " ^ Real.toString p);
paulson@20566
   227
        relevant ([],[]) 
paulson@20566
   228
    end;
paulson@19337
   229
	
paulson@20566
   230
fun relevance_filter thy axioms goals = 
paulson@20566
   231
 if !run_relevance_filter andalso !pass_mark >= 0.1
paulson@20566
   232
 then
paulson@20566
   233
  let val _ = Output.debug "Start of relevance filtering";
paulson@20566
   234
      val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
paulson@20566
   235
      val rels = relevant_clauses thy const_tab (!pass_mark) 
paulson@20566
   236
                   (get_goal_consts_typs thy goals)
paulson@19334
   237
                   (map (pair_consts_typs_axiom thy) axioms)
paulson@19231
   238
  in
paulson@19334
   239
      Output.debug ("Total relevant: " ^ Int.toString (length rels));
paulson@19334
   240
      rels
paulson@20566
   241
  end
paulson@20566
   242
 else axioms;
mengj@18791
   243
wenzelm@20197
   244
end;