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