src/HOL/Tools/ATP/reduce_axiomsN.ML
author paulson
Tue Mar 28 16:48:18 2006 +0200 (2006-03-28)
changeset 19334 96ca738055a6
parent 19321 30b5bb35dd33
child 19335 9e82f341a71b
permissions -rw-r--r--
Simplified version of Jia's filter. Now all constants are pooled, rather than
relevance being compared against separate clauses. Rejects are no longer noted,
and units cannot be added at the end.
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@19315
     9
val reduction_factor = ref 1.0;
paulson@19334
    10
val convergence = ref 4.0;   (*Higher numbers allow longer inference chains*)
mengj@18791
    11
paulson@19334
    12
(*FIXME DELETE Whether all "simple" unit clauses should be included*)
paulson@19315
    13
val add_unit = ref false;
paulson@19315
    14
val unit_pass_mark = ref 0.0;
mengj@18791
    15
paulson@19334
    16
(*The default ignores the constant-count and gives the old Strategy 3*)
paulson@19334
    17
val weight_fn = ref (fn x : real => 1.0);
paulson@19334
    18
mengj@18791
    19
paulson@19231
    20
(*Including equality in this list might be expected to stop rules like subset_antisym from
paulson@19231
    21
  being chosen, but for some reason filtering works better with them listed.*)
paulson@19208
    22
val standard_consts =
paulson@19315
    23
  ["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->",
paulson@19315
    24
   "op =","==","True","False"];
mengj@18791
    25
mengj@18791
    26
mengj@19009
    27
(*** unit clauses ***)
paulson@19231
    28
datatype clause_kind = Unit_neq | Unit_geq | Other
mengj@19009
    29
mengj@19009
    30
mengj@19009
    31
fun literals_of_term args (Const ("Trueprop",_) $ P) = literals_of_term args P
mengj@19009
    32
  | literals_of_term args (Const ("op |",_) $ P $ Q) = 
mengj@19009
    33
    literals_of_term (literals_of_term args P) Q
paulson@19208
    34
  | literals_of_term args P = P::args;
mengj@19009
    35
paulson@19208
    36
fun is_ground t = (term_vars t = []) andalso (term_frees t = []);
mengj@19009
    37
mengj@19009
    38
fun eq_clause_type (P,Q) = 
mengj@19009
    39
    if ((is_ground P) orelse (is_ground Q)) then Unit_geq else Other;
mengj@19009
    40
mengj@19009
    41
fun unit_clause_type (Const ("op =",_) $ P $ Q) = eq_clause_type (P,Q)
mengj@19009
    42
  | unit_clause_type _ = Unit_neq;
mengj@19009
    43
paulson@19231
    44
fun clause_kind tm = 
paulson@19208
    45
    case literals_of_term [] tm of
paulson@19208
    46
        [lit] => unit_clause_type lit
paulson@19208
    47
      | _ => Other;
mengj@19009
    48
mengj@19009
    49
(*** constants with types ***)
mengj@19009
    50
paulson@19231
    51
(*An abstraction of Isabelle types*)
mengj@19009
    52
datatype const_typ =  CTVar | CType of string * const_typ list
mengj@19009
    53
paulson@19208
    54
fun uni_type (CType(con1,args1)) (CType(con2,args2)) = con1=con2 andalso uni_types args1 args2
paulson@19208
    55
  | uni_type (CType _) CTVar = true
mengj@19009
    56
  | uni_type CTVar CTVar = true
mengj@19009
    57
  | uni_type CTVar _ = false
paulson@19208
    58
and uni_types [] [] = true
paulson@19208
    59
  | uni_types (a1::as1) (a2::as2) = uni_type a1 a2 andalso uni_types as1 as2;
mengj@19009
    60
mengj@19009
    61
paulson@19231
    62
fun uni_constants (c1,ctp1) (c2,ctp2) = (c1=c2) andalso uni_types ctp1 ctp2;
mengj@19009
    63
mengj@19009
    64
fun uni_mem _ [] = false
paulson@19208
    65
  | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) =
paulson@19208
    66
      uni_constants (c1,c_typ1) (c,c_typ) orelse uni_mem (c,c_typ) ctyps;
mengj@19009
    67
paulson@19231
    68
fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 
paulson@19231
    69
  | const_typ_of (TFree _) = CTVar
paulson@19231
    70
  | const_typ_of (TVar _) = CTVar
mengj@19009
    71
mengj@19009
    72
paulson@19315
    73
fun const_with_typ thy (c,typ) = 
paulson@19212
    74
    let val tvars = Sign.const_typargs thy (c,typ)
paulson@19315
    75
    in (c, map const_typ_of tvars) end
paulson@19315
    76
    handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)   
mengj@19009
    77
paulson@19315
    78
(*Free variables are counted, as well as constants, to handle locales*)
paulson@19315
    79
fun add_term_consts_typs_rm thy (Const(c, typ)) cs =
paulson@19315
    80
      if (c mem standard_consts) then cs 
paulson@19315
    81
      else const_with_typ thy (c,typ) ins cs
paulson@19315
    82
  | add_term_consts_typs_rm thy (Free(c, typ)) cs =
paulson@19315
    83
      const_with_typ thy (c,typ) ins cs
paulson@19315
    84
  | add_term_consts_typs_rm thy (t $ u) cs =
paulson@19315
    85
      add_term_consts_typs_rm thy t (add_term_consts_typs_rm thy u cs)
paulson@19315
    86
  | add_term_consts_typs_rm thy (Abs(_,_,t)) cs = add_term_consts_typs_rm thy t cs
paulson@19315
    87
  | add_term_consts_typs_rm thy _ cs = cs;
mengj@19009
    88
paulson@19315
    89
fun consts_typs_of_term thy t = add_term_consts_typs_rm thy t [];
mengj@19009
    90
paulson@19208
    91
fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs)
mengj@19009
    92
paulson@19231
    93
paulson@19231
    94
(**** Constant / Type Frequencies ****)
paulson@19231
    95
paulson@19231
    96
local
paulson@19231
    97
paulson@19231
    98
fun cons_nr CTVar = 0
paulson@19231
    99
  | cons_nr (CType _) = 1;
paulson@19231
   100
paulson@19231
   101
in
paulson@19231
   102
paulson@19231
   103
fun const_typ_ord TU =
paulson@19231
   104
  case TU of
paulson@19231
   105
    (CType (a, Ts), CType (b, Us)) =>
paulson@19231
   106
      (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
paulson@19231
   107
  | (T, U) => int_ord (cons_nr T, cons_nr U);
paulson@19212
   108
paulson@19231
   109
end;
paulson@19231
   110
paulson@19231
   111
structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
paulson@19212
   112
paulson@19315
   113
fun count_axiom_consts thy ((t,_), tab) = 
paulson@19315
   114
  let fun count_const (a, T, tab) =
paulson@19315
   115
	let val (c, cts) = const_with_typ thy (a,T)
paulson@19315
   116
	    val cttab = Option.getOpt (Symtab.lookup tab c, CTtab.empty)
paulson@19315
   117
	    val n = Option.getOpt (CTtab.lookup cttab cts, 0)
paulson@19315
   118
	in 
paulson@19315
   119
	    Symtab.update (c, CTtab.update (cts, n+1) cttab) tab
paulson@19315
   120
	end
paulson@19315
   121
      fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
paulson@19315
   122
	| count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
paulson@19231
   123
	| count_term_consts (t $ u, tab) =
paulson@19231
   124
	    count_term_consts (t, count_term_consts (u, tab))
paulson@19231
   125
	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
paulson@19231
   126
	| count_term_consts (_, tab) = tab
paulson@19315
   127
  in  count_term_consts (t, tab)  end;
paulson@19212
   128
mengj@19009
   129
mengj@19009
   130
(******** filter clauses ********)
mengj@19009
   131
paulson@19231
   132
fun const_weight ctab (c, cts) =
paulson@19231
   133
  let val pairs = CTtab.dest (Option.valOf (Symtab.lookup ctab c))
paulson@19231
   134
      fun add ((cts',m), n) = if uni_types cts cts' then m+n else n
paulson@19231
   135
  in  List.foldl add 0 pairs  end;
paulson@19231
   136
paulson@19231
   137
fun add_ct_weight ctab ((c,T), w) =
paulson@19231
   138
  w + !weight_fn (real (const_weight ctab (c,T)));
paulson@19212
   139
paulson@19212
   140
fun consts_typs_weight ctab =
paulson@19212
   141
    List.foldl (add_ct_weight ctab) 0.0;
paulson@19212
   142
paulson@19231
   143
(*Relevant constants are weighted according to frequency, 
paulson@19231
   144
  but irrelevant constants are simply counted. Otherwise, Skolem functions,
paulson@19231
   145
  which are rare, would harm a clause's chances of being picked.*)
paulson@19315
   146
fun clause_weight ctab gctyps consts_typs =
paulson@19208
   147
    let val rel = filter (fn s => uni_mem s gctyps) consts_typs
paulson@19231
   148
        val rel_weight = consts_typs_weight ctab rel
mengj@19009
   149
    in
paulson@19231
   150
	rel_weight / (rel_weight + real (length consts_typs - length rel))
mengj@19009
   151
    end;
paulson@19315
   152
    
paulson@19231
   153
fun pair_consts_typs_axiom thy (tm,name) =
paulson@19212
   154
    ((tm,name), (consts_typs_of_term thy tm));
mengj@19009
   155
paulson@19334
   156
fun relevant_clauses ctab p rel_consts =
paulson@19334
   157
  let fun relevant (newrels,rejects) []  =
paulson@19334
   158
	    if null newrels then [] 
paulson@19334
   159
	    else 
paulson@19334
   160
	      let val new_consts = map #2 newrels
paulson@19334
   161
	          val rel_consts' = foldl (op union) rel_consts new_consts
paulson@19334
   162
                  val newp = p + (1.0-p) / !convergence
paulson@19334
   163
	      in Output.debug ("found relevant: " ^ Int.toString (length newrels));
paulson@19334
   164
                 newrels @ relevant_clauses ctab newp rel_consts' rejects
paulson@19334
   165
	      end
paulson@19334
   166
	| relevant (newrels,rejects) ((ax as (clstm,consts_typs)) :: axs) =
paulson@19334
   167
	    let val weight = clause_weight ctab rel_consts consts_typs
paulson@19334
   168
	    in
paulson@19334
   169
	      if p <= weight 
paulson@19334
   170
	      then relevant (ax::newrels, rejects) axs
paulson@19334
   171
	      else relevant (newrels, ax::rejects) axs
paulson@19334
   172
	    end
paulson@19334
   173
    in  Output.debug ("relevant_clauses: " ^ Real.toString p);
paulson@19334
   174
        relevant ([],[]) end;
paulson@19334
   175
paulson@19315
   176
(*Unit clauses other than non-trivial equations can be included subject to
paulson@19315
   177
  a separate (presumably lower) mark. *)
paulson@19315
   178
fun good_unit_clause ((t,_), (_,w)) = 
paulson@19315
   179
     !unit_pass_mark <= w andalso
paulson@19315
   180
     (case clause_kind t of
paulson@19212
   181
	  Unit_neq => true
paulson@19212
   182
	| Unit_geq => true
paulson@19315
   183
	| Other => false);
paulson@19231
   184
	
paulson@19231
   185
fun showconst (c,cttab) = 
paulson@19231
   186
      List.app (fn n => Output.debug (Int.toString n ^ " occurrences of " ^ c))
paulson@19231
   187
	        (map #2 (CTtab.dest cttab))
paulson@19231
   188
	      
paulson@19321
   189
exception ConstFree;
paulson@19321
   190
fun dest_ConstFree (Const aT) = aT
paulson@19321
   191
  | dest_ConstFree (Free aT) = aT
paulson@19321
   192
  | dest_ConstFree _ = raise ConstFree;
paulson@19321
   193
paulson@19321
   194
(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
paulson@19321
   195
fun defines thy (tm,(name,n)) gctypes =
paulson@19321
   196
  let fun defs hs =
paulson@19321
   197
        let val (rator,args) = strip_comb hs
paulson@19321
   198
            val ct = const_with_typ thy (dest_ConstFree rator)
paulson@19321
   199
        in  forall is_Var args andalso uni_mem ct gctypes  end
paulson@19321
   200
        handle ConstFree => false
paulson@19321
   201
  in    
paulson@19321
   202
    case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ _) => 
paulson@19321
   203
          defs lhs andalso
paulson@19321
   204
          (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true)
paulson@19321
   205
      | _ => false
paulson@19321
   206
  end
paulson@19321
   207
paulson@19315
   208
fun relevance_filter_aux thy axioms goals = 
paulson@19315
   209
  let val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
paulson@19231
   210
      val goals_consts_typs = get_goal_consts_typs thy goals
paulson@19334
   211
      val rels = relevant_clauses const_tab (!pass_mark) goals_consts_typs 
paulson@19334
   212
                   (map (pair_consts_typs_axiom thy) axioms)
paulson@19231
   213
  in
paulson@19334
   214
      Output.debug ("Total relevant: " ^ Int.toString (length rels));
paulson@19334
   215
      rels
paulson@19231
   216
  end;
mengj@19009
   217
paulson@19315
   218
fun relevance_filter thy axioms goals =
paulson@19315
   219
  map #1 (relevance_filter_aux thy axioms goals);
mengj@19009
   220
    
mengj@18791
   221
mengj@18791
   222
end;