src/HOL/Tools/ATP/reduce_axiomsN.ML
author paulson
Fri Mar 10 12:27:36 2006 +0100 (2006-03-10)
changeset 19231 c8879dd3a953
parent 19212 ec53c138277a
child 19315 b218cc3d1bb4
permissions -rw-r--r--
Frequency analysis of constants (with types).

Ability to restrict the number of accepted clauses.
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
mengj@18791
     8
val pass_mark = ref 0.5;
paulson@19231
     9
val strategy = ref 3;
paulson@19231
    10
val max_filtered = ref 2000;
mengj@18791
    11
mengj@18791
    12
fun pol_to_int true = 1
mengj@18791
    13
  | pol_to_int false = ~1;
mengj@18791
    14
mengj@18791
    15
fun part refs [] (s1,s2) = (s1,s2)
paulson@19208
    16
  | part refs (s::ss) (s1,s2) = 
paulson@19208
    17
      if (s mem refs) then part refs ss (s::s1,s2) else part refs ss (s1,s::s2);
mengj@18791
    18
mengj@18791
    19
mengj@18791
    20
fun pol_mem _ [] = false
paulson@19208
    21
  | pol_mem (pol,const) ((p,c)::pcs) =
paulson@19208
    22
      (pol = not p andalso const = c) orelse pol_mem (pol,const) pcs;
mengj@18791
    23
mengj@18791
    24
mengj@18791
    25
fun part_w_pol refs [] (s1,s2) = (s1,s2)
paulson@19208
    26
  | part_w_pol refs (s::ss) (s1,s2) =
paulson@19208
    27
      if (pol_mem s refs) then part_w_pol refs ss (s::s1,s2) 
paulson@19208
    28
      else part_w_pol refs ss (s1,s::s2);
mengj@18791
    29
mengj@18791
    30
paulson@19208
    31
fun add_term_consts_rm ncs (Const(c, _)) cs =
paulson@19208
    32
      if (c mem ncs) then cs else (c ins_string cs)
mengj@18791
    33
  | add_term_consts_rm ncs (t $ u) cs =
mengj@18791
    34
      add_term_consts_rm ncs t (add_term_consts_rm ncs u cs)
mengj@18791
    35
  | add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs
mengj@18791
    36
  | add_term_consts_rm ncs _ cs = cs;
mengj@18791
    37
mengj@18791
    38
fun term_consts_rm ncs t = add_term_consts_rm ncs t [];
mengj@18791
    39
paulson@19231
    40
(*Including equality in this list might be expected to stop rules like subset_antisym from
paulson@19231
    41
  being chosen, but for some reason filtering works better with them listed.*)
paulson@19208
    42
val standard_consts =
paulson@19208
    43
  ["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->","op =","==","True","False"];
paulson@19208
    44
paulson@19208
    45
val consts_of_term = term_consts_rm standard_consts;
mengj@18791
    46
mengj@18791
    47
paulson@19208
    48
fun add_term_pconsts_rm ncs (Const(c,_)) pol cs = if c mem ncs then cs else ((pol,c) ins cs)
mengj@18791
    49
  | add_term_pconsts_rm ncs (Const("Not",_)$P) pol cs = add_term_pconsts_rm ncs P (not pol) cs
mengj@18791
    50
  | add_term_pconsts_rm ncs (P$Q) pol cs = 
mengj@18791
    51
    add_term_pconsts_rm ncs P pol (add_term_pconsts_rm ncs Q pol cs)
mengj@18791
    52
  | add_term_pconsts_rm ncs (Abs(_,_,t)) pol cs = add_term_pconsts_rm ncs t pol cs
mengj@18791
    53
  | add_term_pconsts_rm ncs _ _ cs = cs;
mengj@18791
    54
mengj@18791
    55
mengj@18791
    56
fun term_pconsts_rm ncs t = add_term_pconsts_rm ncs t true [];
mengj@18791
    57
paulson@19208
    58
val pconsts_of_term = term_pconsts_rm standard_consts;
mengj@18791
    59
mengj@18791
    60
fun consts_in_goal goal = consts_of_term goal;
mengj@18791
    61
fun get_goal_consts cs = foldl (op union_string) [] (map consts_in_goal cs);
mengj@18791
    62
mengj@18791
    63
fun pconsts_in_goal goal = pconsts_of_term goal;
mengj@18791
    64
fun get_goal_pconsts cs = foldl (op union) [] (map pconsts_in_goal cs);
mengj@18791
    65
mengj@18791
    66
mengj@18791
    67
(*************************************************************************)
mengj@18791
    68
(*            the first relevance filtering strategy                     *)
mengj@18791
    69
(*************************************************************************)
mengj@18791
    70
mengj@18791
    71
fun find_clause_weight_s_1 (refconsts : string list) consts wa = 
mengj@18791
    72
    let val (rel,irrel) = part refconsts consts ([],[])
mengj@18791
    73
    in
paulson@19208
    74
	(real (length rel) / real (length consts)) * wa
mengj@18791
    75
    end;
mengj@18791
    76
mengj@18791
    77
fun find_clause_weight_m_1 [] (_,w) = w 
mengj@18791
    78
  | find_clause_weight_m_1 ((_,(refconsts,wa))::y) (consts,w) =
paulson@19208
    79
      let val w' = find_clause_weight_s_1 refconsts consts wa
paulson@19208
    80
      in
paulson@19208
    81
	if w < w' then find_clause_weight_m_1 y (consts,w')
mengj@18791
    82
	else find_clause_weight_m_1 y (consts,w)
paulson@19208
    83
      end;
mengj@18791
    84
mengj@18791
    85
mengj@18791
    86
fun relevant_clauses_ax_g_1 _ []  _ (ax,r) = (ax,r)
mengj@19200
    87
  | relevant_clauses_ax_g_1 gconsts  ((clstm,(consts,_))::y) P (ax,r) =
paulson@19208
    88
      let val weight = find_clause_weight_s_1 gconsts consts 1.0
paulson@19208
    89
      in
paulson@19208
    90
	if  P <= weight 
paulson@19208
    91
	then relevant_clauses_ax_g_1 gconsts y P ((clstm,(consts,weight))::ax,r)
mengj@19200
    92
	else relevant_clauses_ax_g_1 gconsts y P (ax,(clstm,(consts,weight))::r)
paulson@19208
    93
      end;
mengj@18791
    94
mengj@18791
    95
mengj@18791
    96
fun relevant_clauses_ax_1 rel_axs  [] P (addc,tmpc) keep = 
mengj@18791
    97
    (case addc of [] => rel_axs @ keep
mengj@18791
    98
		| _ => case tmpc of [] => addc @ rel_axs @ keep
mengj@18791
    99
				  | _ => relevant_clauses_ax_1 addc tmpc P ([],[]) (rel_axs @ keep))
mengj@19200
   100
  | relevant_clauses_ax_1 rel_axs ((clstm,(consts,weight))::e_axs) P (addc,tmpc) keep = 
paulson@19208
   101
      let val weight' = find_clause_weight_m_1 rel_axs (consts,weight) 
paulson@19208
   102
	  val e_ax' = (clstm,(consts, weight'))
paulson@19208
   103
      in
paulson@19208
   104
	if P <= weight' 
paulson@19208
   105
	then relevant_clauses_ax_1 rel_axs e_axs P ((clstm,(consts,weight'))::addc,tmpc) keep
mengj@19200
   106
	else relevant_clauses_ax_1 rel_axs e_axs P (addc,(clstm,(consts,weight'))::tmpc) keep 
paulson@19208
   107
      end;
mengj@18791
   108
mengj@18791
   109
mengj@18791
   110
fun initialize [] ax_weights = ax_weights
mengj@19200
   111
  | initialize ((tm,name)::tms_names) ax_weights =
paulson@19208
   112
      let val consts = consts_of_term tm
paulson@19208
   113
      in
paulson@19208
   114
	  initialize tms_names (((tm,name),(consts,0.0))::ax_weights)
paulson@19208
   115
      end;
mengj@18791
   116
mengj@18791
   117
fun relevance_filter1_aux axioms goals = 
mengj@18791
   118
    let val pass = !pass_mark
mengj@18791
   119
	val axioms_weights = initialize axioms []
mengj@18791
   120
	val goals_consts = get_goal_consts goals
mengj@18791
   121
	val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_1 goals_consts axioms_weights pass ([],[]) 
mengj@18791
   122
    in
mengj@18791
   123
	relevant_clauses_ax_1 rel_clauses nrel_clauses pass ([],[]) []
mengj@18791
   124
    end;
mengj@18791
   125
mengj@18791
   126
fun relevance_filter1 axioms goals = map fst (relevance_filter1_aux axioms goals);
mengj@18791
   127
mengj@18791
   128
mengj@18791
   129
(*************************************************************************)
mengj@18791
   130
(*            the second relevance filtering strategy                    *)
mengj@18791
   131
(*************************************************************************)
mengj@18791
   132
mengj@18791
   133
fun find_clause_weight_s_2 (refpconsts : (bool * string) list) pconsts wa = 
mengj@18791
   134
    let val (rel,irrel) = part_w_pol refpconsts pconsts ([],[])
mengj@18791
   135
    in
mengj@18791
   136
	((real (length rel))/(real (length pconsts))) * wa
mengj@18791
   137
    end;
mengj@18791
   138
mengj@18791
   139
fun find_clause_weight_m_2 [] (_,w) = w 
mengj@18791
   140
  | find_clause_weight_m_2 ((_,(refpconsts,wa))::y) (pconsts,w) =
mengj@18791
   141
    let val w' = find_clause_weight_s_2 refpconsts pconsts wa
mengj@18791
   142
    in
mengj@18791
   143
	if (w < w') then find_clause_weight_m_2 y (pconsts,w')
mengj@18791
   144
	else find_clause_weight_m_2 y (pconsts,w)
mengj@18791
   145
    end;
mengj@18791
   146
mengj@18791
   147
mengj@18791
   148
fun relevant_clauses_ax_g_2 _ []  _ (ax,r) = (ax,r)
mengj@19200
   149
  | relevant_clauses_ax_g_2 gpconsts  ((clstm,(pconsts,_))::y) P (ax,r) =
mengj@18791
   150
    let val weight = find_clause_weight_s_2 gpconsts pconsts 1.0
mengj@18791
   151
    in
mengj@19200
   152
	if  P <= weight then relevant_clauses_ax_g_2 gpconsts y P ((clstm,(pconsts,weight))::ax,r)
mengj@19200
   153
	else relevant_clauses_ax_g_2 gpconsts y P (ax,(clstm,(pconsts,weight))::r)
mengj@18791
   154
    end;
mengj@18791
   155
mengj@18791
   156
mengj@18791
   157
fun relevant_clauses_ax_2 rel_axs  [] P (addc,tmpc) keep = 
mengj@18791
   158
    (case addc of [] => rel_axs @ keep
mengj@18791
   159
		| _ => case tmpc of [] => addc @ rel_axs @ keep
mengj@18791
   160
				  | _ => relevant_clauses_ax_2 addc tmpc P ([],[]) (rel_axs @ keep))
mengj@19200
   161
  | relevant_clauses_ax_2 rel_axs ((clstm,(pconsts,weight))::e_axs) P (addc,tmpc) keep = 
mengj@18791
   162
    let val weight' = find_clause_weight_m_2 rel_axs (pconsts,weight) 
mengj@19200
   163
	val e_ax' = (clstm,(pconsts, weight'))
mengj@18791
   164
    in
mengj@18791
   165
	
mengj@19200
   166
	if P <= weight' then relevant_clauses_ax_2 rel_axs e_axs P ((clstm,(pconsts,weight'))::addc,tmpc) keep
mengj@19200
   167
	else relevant_clauses_ax_2 rel_axs e_axs P (addc,(clstm,(pconsts,weight'))::tmpc) keep 
mengj@18791
   168
    end;
mengj@18791
   169
mengj@18791
   170
mengj@18791
   171
fun initialize_w_pol [] ax_weights = ax_weights
mengj@19200
   172
  | initialize_w_pol ((tm,name)::tms_names) ax_weights =
mengj@19200
   173
    let val consts = pconsts_of_term tm
mengj@18791
   174
    in
mengj@19200
   175
	initialize_w_pol tms_names (((tm,name),(consts,0.0))::ax_weights)
mengj@18791
   176
    end;
mengj@18791
   177
mengj@18791
   178
mengj@18791
   179
fun relevance_filter2_aux axioms goals = 
mengj@18791
   180
    let val pass = !pass_mark
mengj@18791
   181
	val axioms_weights = initialize_w_pol axioms []
mengj@18791
   182
	val goals_consts = get_goal_pconsts goals
mengj@18791
   183
	val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_2 goals_consts axioms_weights pass ([],[]) 
mengj@18791
   184
    in
mengj@18791
   185
	relevant_clauses_ax_2 rel_clauses nrel_clauses pass ([],[]) []
mengj@18791
   186
    end;
mengj@18791
   187
mengj@18791
   188
fun relevance_filter2 axioms goals = map fst (relevance_filter2_aux axioms goals);
mengj@18791
   189
mengj@19009
   190
(******************************************************************)
mengj@19009
   191
(*       the third relevance filtering strategy                   *)
mengj@19009
   192
(******************************************************************)
mengj@18791
   193
mengj@19009
   194
(*** unit clauses ***)
paulson@19231
   195
datatype clause_kind = Unit_neq | Unit_geq | Other
mengj@19009
   196
paulson@19208
   197
(*Whether all "simple" unit clauses should be included*)
mengj@19009
   198
val add_unit = ref true;
mengj@19009
   199
mengj@19009
   200
fun literals_of_term args (Const ("Trueprop",_) $ P) = literals_of_term args P
mengj@19009
   201
  | literals_of_term args (Const ("op |",_) $ P $ Q) = 
mengj@19009
   202
    literals_of_term (literals_of_term args P) Q
paulson@19208
   203
  | literals_of_term args P = P::args;
mengj@19009
   204
paulson@19208
   205
fun is_ground t = (term_vars t = []) andalso (term_frees t = []);
mengj@19009
   206
mengj@19009
   207
fun eq_clause_type (P,Q) = 
mengj@19009
   208
    if ((is_ground P) orelse (is_ground Q)) then Unit_geq else Other;
mengj@19009
   209
mengj@19009
   210
fun unit_clause_type (Const ("op =",_) $ P $ Q) = eq_clause_type (P,Q)
mengj@19009
   211
  | unit_clause_type _ = Unit_neq;
mengj@19009
   212
paulson@19231
   213
fun clause_kind tm = 
paulson@19208
   214
    case literals_of_term [] tm of
paulson@19208
   215
        [lit] => unit_clause_type lit
paulson@19208
   216
      | _ => Other;
mengj@19009
   217
mengj@19009
   218
(*** constants with types ***)
mengj@19009
   219
paulson@19231
   220
(*An abstraction of Isabelle types*)
mengj@19009
   221
datatype const_typ =  CTVar | CType of string * const_typ list
mengj@19009
   222
paulson@19208
   223
fun uni_type (CType(con1,args1)) (CType(con2,args2)) = con1=con2 andalso uni_types args1 args2
paulson@19208
   224
  | uni_type (CType _) CTVar = true
mengj@19009
   225
  | uni_type CTVar CTVar = true
mengj@19009
   226
  | uni_type CTVar _ = false
paulson@19208
   227
and uni_types [] [] = true
paulson@19208
   228
  | uni_types (a1::as1) (a2::as2) = uni_type a1 a2 andalso uni_types as1 as2;
mengj@19009
   229
mengj@19009
   230
paulson@19231
   231
fun uni_constants (c1,ctp1) (c2,ctp2) = (c1=c2) andalso uni_types ctp1 ctp2;
mengj@19009
   232
mengj@19009
   233
fun uni_mem _ [] = false
paulson@19208
   234
  | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) =
paulson@19208
   235
      uni_constants (c1,c_typ1) (c,c_typ) orelse uni_mem (c,c_typ) ctyps;
mengj@19009
   236
paulson@19231
   237
fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 
paulson@19231
   238
  | const_typ_of (TFree _) = CTVar
paulson@19231
   239
  | const_typ_of (TVar _) = CTVar
mengj@19009
   240
mengj@19009
   241
paulson@19212
   242
fun const_w_typ thy (c,typ) = 
paulson@19212
   243
    let val tvars = Sign.const_typargs thy (c,typ)
paulson@19212
   244
    in (c, map const_typ_of tvars) end;
mengj@19009
   245
paulson@19212
   246
fun add_term_consts_typs_rm thy ncs (Const(c, typ)) cs =
paulson@19212
   247
      if (c mem ncs) then cs else (const_w_typ thy (c,typ) ins cs)
mengj@19009
   248
  | add_term_consts_typs_rm thy ncs (t $ u) cs =
mengj@19009
   249
      add_term_consts_typs_rm thy ncs  t (add_term_consts_typs_rm thy ncs u cs)
mengj@19009
   250
  | add_term_consts_typs_rm thy ncs (Abs(_,_,t)) cs = add_term_consts_typs_rm thy ncs t cs
mengj@19009
   251
  | add_term_consts_typs_rm thy ncs _ cs = cs;
mengj@19009
   252
mengj@19009
   253
fun term_consts_typs_rm thy ncs t = add_term_consts_typs_rm thy ncs t [];
mengj@19009
   254
paulson@19208
   255
fun consts_typs_of_term thy = term_consts_typs_rm thy standard_consts;
mengj@19009
   256
paulson@19208
   257
fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs)
mengj@19009
   258
paulson@19231
   259
paulson@19231
   260
(**** Constant / Type Frequencies ****)
paulson@19231
   261
paulson@19231
   262
local
paulson@19231
   263
paulson@19231
   264
fun cons_nr CTVar = 0
paulson@19231
   265
  | cons_nr (CType _) = 1;
paulson@19231
   266
paulson@19231
   267
in
paulson@19231
   268
paulson@19231
   269
fun const_typ_ord TU =
paulson@19231
   270
  case TU of
paulson@19231
   271
    (CType (a, Ts), CType (b, Us)) =>
paulson@19231
   272
      (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
paulson@19231
   273
  | (T, U) => int_ord (cons_nr T, cons_nr U);
paulson@19212
   274
paulson@19231
   275
end;
paulson@19231
   276
paulson@19231
   277
structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
paulson@19212
   278
paulson@19231
   279
fun count_axiom_consts thy ((tm,_), tab) = 
paulson@19231
   280
  let fun count_term_consts (Const cT, tab) =
paulson@19231
   281
	    let val (c, cts) = const_w_typ thy cT
paulson@19231
   282
		val cttab = Option.getOpt (Symtab.lookup tab c, CTtab.empty)
paulson@19231
   283
		val n = Option.getOpt (CTtab.lookup cttab cts, 0)
paulson@19231
   284
	    in 
paulson@19231
   285
		Symtab.update (c, CTtab.update (cts, n+1) cttab) tab
paulson@19231
   286
            end
paulson@19231
   287
	| count_term_consts (t $ u, tab) =
paulson@19231
   288
	    count_term_consts (t, count_term_consts (u, tab))
paulson@19231
   289
	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
paulson@19231
   290
	| count_term_consts (_, tab) = tab
paulson@19231
   291
  in  count_term_consts (tm, tab) end;
paulson@19212
   292
mengj@19009
   293
mengj@19009
   294
(******** filter clauses ********)
mengj@19009
   295
paulson@19212
   296
(*The default ignores the constant-count and gives the old Strategy 3*)
paulson@19212
   297
val weight_fn = ref (fn x : real => 1.0);
paulson@19212
   298
paulson@19231
   299
fun const_weight ctab (c, cts) =
paulson@19231
   300
  let val pairs = CTtab.dest (Option.valOf (Symtab.lookup ctab c))
paulson@19231
   301
      fun add ((cts',m), n) = if uni_types cts cts' then m+n else n
paulson@19231
   302
  in  List.foldl add 0 pairs  end;
paulson@19231
   303
paulson@19231
   304
fun add_ct_weight ctab ((c,T), w) =
paulson@19231
   305
  w + !weight_fn (real (const_weight ctab (c,T)));
paulson@19212
   306
paulson@19212
   307
fun consts_typs_weight ctab =
paulson@19212
   308
    List.foldl (add_ct_weight ctab) 0.0;
paulson@19212
   309
paulson@19231
   310
(*Relevant constants are weighted according to frequency, 
paulson@19231
   311
  but irrelevant constants are simply counted. Otherwise, Skolem functions,
paulson@19231
   312
  which are rare, would harm a clause's chances of being picked.*)
paulson@19212
   313
fun clause_weight_s_3 ctab gctyps consts_typs =
paulson@19208
   314
    let val rel = filter (fn s => uni_mem s gctyps) consts_typs
paulson@19231
   315
        val rel_weight = consts_typs_weight ctab rel
mengj@19009
   316
    in
paulson@19231
   317
	rel_weight / (rel_weight + real (length consts_typs - length rel))
mengj@19009
   318
    end;
mengj@19009
   319
paulson@19212
   320
fun relevant_clauses_ax_3 ctab rel_axs [] P (addc,tmpc) keep =
paulson@19208
   321
      if null addc orelse null tmpc 
paulson@19208
   322
      then (addc @ rel_axs @ keep, tmpc)   (*termination!*)
paulson@19212
   323
      else relevant_clauses_ax_3 ctab addc tmpc P ([],[]) (rel_axs @ keep)
paulson@19212
   324
  | relevant_clauses_ax_3 ctab rel_axs ((clstm,(consts_typs,weight))::e_axs) P (addc,tmpc) keep =
paulson@19231
   325
      let fun clause_weight_ax (_,(refconsts_typs,wa)) =
paulson@19231
   326
              wa * clause_weight_s_3 ctab refconsts_typs consts_typs;
paulson@19231
   327
          val weight' = List.foldl Real.max weight (map clause_weight_ax rel_axs)
paulson@19212
   328
	  val e_ax' = (clstm, (consts_typs,weight'))
paulson@19208
   329
      in
paulson@19212
   330
	if P <= weight' 
paulson@19212
   331
	then relevant_clauses_ax_3 ctab rel_axs e_axs P (e_ax'::addc, tmpc) keep
paulson@19212
   332
	else relevant_clauses_ax_3 ctab rel_axs e_axs P (addc, e_ax'::tmpc) keep
paulson@19208
   333
      end;
mengj@19009
   334
paulson@19231
   335
fun pair_consts_typs_axiom thy (tm,name) =
paulson@19212
   336
    ((tm,name), (consts_typs_of_term thy tm));
mengj@19009
   337
paulson@19231
   338
fun safe_unit_clause ((t,_), _) = 
paulson@19231
   339
      case clause_kind t of
paulson@19212
   340
	  Unit_neq => true
paulson@19212
   341
	| Unit_geq => true
paulson@19212
   342
	| Other => false;
paulson@19231
   343
	
paulson@19231
   344
fun axiom_ord ((_,(_,w1)), (_,(_,w2))) = Real.compare (w2,w1);
mengj@19009
   345
paulson@19231
   346
fun showconst (c,cttab) = 
paulson@19231
   347
      List.app (fn n => Output.debug (Int.toString n ^ " occurrences of " ^ c))
paulson@19231
   348
	        (map #2 (CTtab.dest cttab))
paulson@19231
   349
paulson@19231
   350
fun show_cname (name,k) = name ^ "__" ^ Int.toString k;
paulson@19231
   351
paulson@19231
   352
fun showax ((_,cname), (_,w)) = 
paulson@19231
   353
    Output.debug ("Axiom " ^ show_cname cname ^ " has weight " ^ Real.toString w)
paulson@19231
   354
	      
paulson@19231
   355
	      fun relevance_filter3_aux thy axioms goals = 
paulson@19231
   356
  let val pass = !pass_mark
paulson@19231
   357
      val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
paulson@19231
   358
      val goals_consts_typs = get_goal_consts_typs thy goals
paulson@19231
   359
      fun relevant [] (ax,r) = (ax,r)
paulson@19231
   360
	| relevant ((clstm,consts_typs)::y) (ax,r) =
paulson@19231
   361
	    let val weight = clause_weight_s_3 const_tab goals_consts_typs consts_typs
paulson@19231
   362
		val ccc = (clstm, (consts_typs,weight))
paulson@19231
   363
	    in
paulson@19231
   364
	      if pass <= weight 
paulson@19231
   365
	      then relevant y (ccc::ax, r)
paulson@19231
   366
	      else relevant y (ax, ccc::r)
paulson@19231
   367
	    end
paulson@19231
   368
      val (rel_clauses,nrel_clauses) =
paulson@19231
   369
	  relevant (map (pair_consts_typs_axiom thy) axioms) ([],[]) 
paulson@19231
   370
      val (ax,r) = relevant_clauses_ax_3 const_tab rel_clauses nrel_clauses pass ([],[]) []
paulson@19231
   371
      val ax' = Library.take(!max_filtered, Library.sort axiom_ord ax)
paulson@19231
   372
  in
paulson@19231
   373
      if !Output.show_debug_msgs then
paulson@19231
   374
	   (List.app showconst (Symtab.dest const_tab);
paulson@19231
   375
	    List.app showax ax)
paulson@19231
   376
      else ();
paulson@19231
   377
      if !add_unit then (filter safe_unit_clause r) @ ax'
paulson@19231
   378
      else ax'
paulson@19231
   379
  end;
mengj@19009
   380
paulson@19208
   381
fun relevance_filter3 thy axioms goals =
paulson@19212
   382
  map #1 (relevance_filter3_aux thy axioms goals);
mengj@19009
   383
    
mengj@18791
   384
mengj@18791
   385
(******************************************************************)
mengj@18791
   386
(* Generic functions for relevance filtering                      *)
mengj@18791
   387
(******************************************************************)
mengj@18791
   388
mengj@18791
   389
exception RELEVANCE_FILTER of string;
mengj@18791
   390
mengj@19009
   391
fun relevance_filter thy axioms goals = 
paulson@19208
   392
  case (!strategy) of 1 => relevance_filter1 axioms goals
paulson@19208
   393
		    | 2 => relevance_filter2 axioms goals
paulson@19208
   394
		    | 3 => relevance_filter3 thy axioms goals
paulson@19208
   395
		    | _ => raise RELEVANCE_FILTER("strategy doesn't exist");
mengj@18791
   396
mengj@18791
   397
end;