src/HOL/Tools/ATP/reduce_axiomsN.ML
author paulson
Wed Apr 19 10:43:09 2006 +0200 (2006-04-19)
changeset 19448 72dab71cb11e
parent 19355 3140daf6863d
child 20132 de3c295000b2
permissions -rw-r--r--
definition expansion checks for excess variables
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
mengj@18791
     5
structure ReduceAxiomsN =
mengj@18791
     6
struct
mengj@18791
     7
paulson@19315
     8
val pass_mark = ref 0.6;
paulson@19337
     9
val convergence = ref 2.4;   (*Higher numbers allow longer inference chains*)
paulson@19337
    10
val follow_defs = ref true;  (*Follow definitions. Makes problems bigger.*)
mengj@18791
    11
paulson@19337
    12
fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0);
paulson@19337
    13
paulson@19337
    14
(*The default seems best in practice. A constant function of one ignores
paulson@19337
    15
  the constant frequencies.*)
paulson@19337
    16
val weight_fn = ref log_weight2;
paulson@19334
    17
mengj@18791
    18
paulson@19231
    19
(*Including equality in this list might be expected to stop rules like subset_antisym from
paulson@19231
    20
  being chosen, but for some reason filtering works better with them listed.*)
paulson@19208
    21
val standard_consts =
paulson@19315
    22
  ["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->",
paulson@19315
    23
   "op =","==","True","False"];
mengj@18791
    24
mengj@18791
    25
mengj@19009
    26
(*** constants with types ***)
mengj@19009
    27
paulson@19231
    28
(*An abstraction of Isabelle types*)
mengj@19009
    29
datatype const_typ =  CTVar | CType of string * const_typ list
mengj@19009
    30
paulson@19208
    31
fun uni_type (CType(con1,args1)) (CType(con2,args2)) = con1=con2 andalso uni_types args1 args2
paulson@19208
    32
  | uni_type (CType _) CTVar = true
mengj@19009
    33
  | uni_type CTVar CTVar = true
mengj@19009
    34
  | uni_type CTVar _ = false
paulson@19208
    35
and uni_types [] [] = true
paulson@19208
    36
  | uni_types (a1::as1) (a2::as2) = uni_type a1 a2 andalso uni_types as1 as2;
mengj@19009
    37
mengj@19009
    38
paulson@19231
    39
fun uni_constants (c1,ctp1) (c2,ctp2) = (c1=c2) andalso uni_types ctp1 ctp2;
mengj@19009
    40
mengj@19009
    41
fun uni_mem _ [] = false
paulson@19208
    42
  | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) =
paulson@19208
    43
      uni_constants (c1,c_typ1) (c,c_typ) orelse uni_mem (c,c_typ) ctyps;
mengj@19009
    44
paulson@19231
    45
fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 
paulson@19231
    46
  | const_typ_of (TFree _) = CTVar
paulson@19231
    47
  | const_typ_of (TVar _) = CTVar
mengj@19009
    48
mengj@19009
    49
paulson@19315
    50
fun const_with_typ thy (c,typ) = 
paulson@19212
    51
    let val tvars = Sign.const_typargs thy (c,typ)
paulson@19315
    52
    in (c, map const_typ_of tvars) end
paulson@19315
    53
    handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)   
mengj@19009
    54
paulson@19315
    55
(*Free variables are counted, as well as constants, to handle locales*)
paulson@19315
    56
fun add_term_consts_typs_rm thy (Const(c, typ)) cs =
paulson@19315
    57
      if (c mem standard_consts) then cs 
paulson@19335
    58
      else const_with_typ thy (c,typ) ins cs   (*suppress multiples*)
paulson@19315
    59
  | add_term_consts_typs_rm thy (Free(c, typ)) cs =
paulson@19315
    60
      const_with_typ thy (c,typ) ins cs
paulson@19315
    61
  | add_term_consts_typs_rm thy (t $ u) cs =
paulson@19315
    62
      add_term_consts_typs_rm thy t (add_term_consts_typs_rm thy u cs)
paulson@19315
    63
  | add_term_consts_typs_rm thy (Abs(_,_,t)) cs = add_term_consts_typs_rm thy t cs
paulson@19315
    64
  | add_term_consts_typs_rm thy _ cs = cs;
mengj@19009
    65
paulson@19315
    66
fun consts_typs_of_term thy t = add_term_consts_typs_rm thy t [];
mengj@19009
    67
paulson@19208
    68
fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs)
mengj@19009
    69
paulson@19231
    70
paulson@19231
    71
(**** Constant / Type Frequencies ****)
paulson@19231
    72
paulson@19231
    73
local
paulson@19231
    74
paulson@19231
    75
fun cons_nr CTVar = 0
paulson@19231
    76
  | cons_nr (CType _) = 1;
paulson@19231
    77
paulson@19231
    78
in
paulson@19231
    79
paulson@19231
    80
fun const_typ_ord TU =
paulson@19231
    81
  case TU of
paulson@19231
    82
    (CType (a, Ts), CType (b, Us)) =>
paulson@19231
    83
      (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
paulson@19231
    84
  | (T, U) => int_ord (cons_nr T, cons_nr U);
paulson@19212
    85
paulson@19231
    86
end;
paulson@19231
    87
paulson@19231
    88
structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
paulson@19212
    89
mengj@19355
    90
fun count_axiom_consts thy ((thm,_), tab) = 
paulson@19315
    91
  let fun count_const (a, T, tab) =
paulson@19315
    92
	let val (c, cts) = const_with_typ thy (a,T)
paulson@19315
    93
	    val cttab = Option.getOpt (Symtab.lookup tab c, CTtab.empty)
paulson@19315
    94
	    val n = Option.getOpt (CTtab.lookup cttab cts, 0)
paulson@19315
    95
	in 
paulson@19315
    96
	    Symtab.update (c, CTtab.update (cts, n+1) cttab) tab
paulson@19315
    97
	end
paulson@19315
    98
      fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
paulson@19315
    99
	| count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
paulson@19231
   100
	| count_term_consts (t $ u, tab) =
paulson@19231
   101
	    count_term_consts (t, count_term_consts (u, tab))
paulson@19231
   102
	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
paulson@19231
   103
	| count_term_consts (_, tab) = tab
mengj@19355
   104
  in  count_term_consts (prop_of thm, tab)  end;
paulson@19212
   105
mengj@19009
   106
mengj@19009
   107
(******** filter clauses ********)
mengj@19009
   108
paulson@19231
   109
fun const_weight ctab (c, cts) =
paulson@19231
   110
  let val pairs = CTtab.dest (Option.valOf (Symtab.lookup ctab c))
paulson@19231
   111
      fun add ((cts',m), n) = if uni_types cts cts' then m+n else n
paulson@19231
   112
  in  List.foldl add 0 pairs  end;
paulson@19231
   113
paulson@19231
   114
fun add_ct_weight ctab ((c,T), w) =
paulson@19231
   115
  w + !weight_fn (real (const_weight ctab (c,T)));
paulson@19212
   116
paulson@19212
   117
fun consts_typs_weight ctab =
paulson@19212
   118
    List.foldl (add_ct_weight ctab) 0.0;
paulson@19212
   119
paulson@19231
   120
(*Relevant constants are weighted according to frequency, 
paulson@19231
   121
  but irrelevant constants are simply counted. Otherwise, Skolem functions,
paulson@19231
   122
  which are rare, would harm a clause's chances of being picked.*)
paulson@19315
   123
fun clause_weight ctab gctyps consts_typs =
paulson@19208
   124
    let val rel = filter (fn s => uni_mem s gctyps) consts_typs
paulson@19231
   125
        val rel_weight = consts_typs_weight ctab rel
mengj@19009
   126
    in
paulson@19231
   127
	rel_weight / (rel_weight + real (length consts_typs - length rel))
mengj@19009
   128
    end;
paulson@19315
   129
    
mengj@19355
   130
fun pair_consts_typs_axiom thy (thm,name) =
mengj@19355
   131
    ((thm,name), (consts_typs_of_term thy (prop_of thm)));
mengj@19009
   132
paulson@19321
   133
exception ConstFree;
paulson@19321
   134
fun dest_ConstFree (Const aT) = aT
paulson@19321
   135
  | dest_ConstFree (Free aT) = aT
paulson@19321
   136
  | dest_ConstFree _ = raise ConstFree;
paulson@19321
   137
paulson@19321
   138
(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
mengj@19355
   139
fun defines thy (thm,(name,n)) gctypes =
mengj@19355
   140
    let val tm = prop_of thm
paulson@19448
   141
	fun defs lhs rhs =
paulson@19448
   142
            let val (rator,args) = strip_comb lhs
mengj@19355
   143
		val ct = const_with_typ thy (dest_ConstFree rator)
paulson@19448
   144
            in  forall is_Var args andalso uni_mem ct gctypes andalso
paulson@19448
   145
                term_varnames rhs subset term_varnames lhs
paulson@19448
   146
            end
paulson@19448
   147
	    handle ConstFree => false
mengj@19355
   148
    in    
paulson@19448
   149
	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 
paulson@19448
   150
		   defs lhs rhs andalso
mengj@19355
   151
		   (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true)
mengj@19355
   152
		 | _ => false
mengj@19355
   153
    end
paulson@19321
   154
paulson@19337
   155
fun relevant_clauses thy ctab p rel_consts =
paulson@19337
   156
  let fun relevant (newrels,rejects) []  =
paulson@19337
   157
	    if null newrels then [] 
paulson@19337
   158
	    else 
paulson@19337
   159
	      let val new_consts = map #2 newrels
paulson@19337
   160
	          val rel_consts' = foldl (op union) rel_consts new_consts
paulson@19337
   161
                  val newp = p + (1.0-p) / !convergence
paulson@19337
   162
	      in Output.debug ("found relevant: " ^ Int.toString (length newrels));
paulson@19337
   163
                 newrels @ relevant_clauses thy ctab newp rel_consts' rejects
paulson@19337
   164
	      end
mengj@19355
   165
	| relevant (newrels,rejects) ((ax as (clsthm,consts_typs)) :: axs) =
paulson@19337
   166
	    let val weight = clause_weight ctab rel_consts consts_typs
paulson@19337
   167
	    in
mengj@19355
   168
	      if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts)
paulson@19337
   169
	      then relevant (ax::newrels, rejects) axs
paulson@19337
   170
	      else relevant (newrels, ax::rejects) axs
paulson@19337
   171
	    end
paulson@19337
   172
    in  Output.debug ("relevant_clauses: " ^ Real.toString p);
paulson@19337
   173
        relevant ([],[]) end;
paulson@19337
   174
	
paulson@19337
   175
     
paulson@19315
   176
fun relevance_filter_aux thy axioms goals = 
paulson@19315
   177
  let val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
paulson@19231
   178
      val goals_consts_typs = get_goal_consts_typs thy goals
paulson@19337
   179
      val rels = relevant_clauses thy const_tab (!pass_mark) goals_consts_typs 
paulson@19334
   180
                   (map (pair_consts_typs_axiom thy) axioms)
paulson@19231
   181
  in
paulson@19334
   182
      Output.debug ("Total relevant: " ^ Int.toString (length rels));
paulson@19334
   183
      rels
paulson@19231
   184
  end;
mengj@19009
   185
paulson@19315
   186
fun relevance_filter thy axioms goals =
paulson@19337
   187
  if !pass_mark < 0.1 then axioms
paulson@19337
   188
  else map #1 (relevance_filter_aux thy axioms goals);
mengj@19009
   189
    
mengj@18791
   190
mengj@18791
   191
end;