src/HOL/Tools/ATP/reduce_axiomsN.ML
author paulson
Wed Mar 08 10:19:57 2006 +0100 (2006-03-08)
changeset 19212 ec53c138277a
parent 19208 3e8006cbc925
child 19231 c8879dd3a953
permissions -rw-r--r--
Frequency strategy. Revised indentation, etc.
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;
mengj@18791
     9
val strategy = ref 1;
mengj@18791
    10
mengj@18791
    11
fun pol_to_int true = 1
mengj@18791
    12
  | pol_to_int false = ~1;
mengj@18791
    13
mengj@18791
    14
fun part refs [] (s1,s2) = (s1,s2)
paulson@19208
    15
  | part refs (s::ss) (s1,s2) = 
paulson@19208
    16
      if (s mem refs) then part refs ss (s::s1,s2) else part refs ss (s1,s::s2);
mengj@18791
    17
mengj@18791
    18
mengj@18791
    19
fun pol_mem _ [] = false
paulson@19208
    20
  | pol_mem (pol,const) ((p,c)::pcs) =
paulson@19208
    21
      (pol = not p andalso const = c) orelse pol_mem (pol,const) pcs;
mengj@18791
    22
mengj@18791
    23
mengj@18791
    24
fun part_w_pol refs [] (s1,s2) = (s1,s2)
paulson@19208
    25
  | part_w_pol refs (s::ss) (s1,s2) =
paulson@19208
    26
      if (pol_mem s refs) then part_w_pol refs ss (s::s1,s2) 
paulson@19208
    27
      else part_w_pol refs ss (s1,s::s2);
mengj@18791
    28
mengj@18791
    29
paulson@19208
    30
fun add_term_consts_rm ncs (Const(c, _)) cs =
paulson@19208
    31
      if (c mem ncs) then cs else (c ins_string cs)
mengj@18791
    32
  | add_term_consts_rm ncs (t $ u) cs =
mengj@18791
    33
      add_term_consts_rm ncs t (add_term_consts_rm ncs u cs)
mengj@18791
    34
  | add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs
mengj@18791
    35
  | add_term_consts_rm ncs _ cs = cs;
mengj@18791
    36
mengj@18791
    37
fun term_consts_rm ncs t = add_term_consts_rm ncs t [];
mengj@18791
    38
paulson@19208
    39
val standard_consts =
paulson@19208
    40
  ["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->","op =","==","True","False"];
paulson@19208
    41
paulson@19208
    42
val consts_of_term = term_consts_rm standard_consts;
mengj@18791
    43
mengj@18791
    44
paulson@19208
    45
fun add_term_pconsts_rm ncs (Const(c,_)) pol cs = if c mem ncs then cs else ((pol,c) ins cs)
mengj@18791
    46
  | add_term_pconsts_rm ncs (Const("Not",_)$P) pol cs = add_term_pconsts_rm ncs P (not pol) cs
mengj@18791
    47
  | add_term_pconsts_rm ncs (P$Q) pol cs = 
mengj@18791
    48
    add_term_pconsts_rm ncs P pol (add_term_pconsts_rm ncs Q pol cs)
mengj@18791
    49
  | add_term_pconsts_rm ncs (Abs(_,_,t)) pol cs = add_term_pconsts_rm ncs t pol cs
mengj@18791
    50
  | add_term_pconsts_rm ncs _ _ cs = cs;
mengj@18791
    51
mengj@18791
    52
mengj@18791
    53
fun term_pconsts_rm ncs t = add_term_pconsts_rm ncs t true [];
mengj@18791
    54
paulson@19208
    55
val pconsts_of_term = term_pconsts_rm standard_consts;
mengj@18791
    56
mengj@18791
    57
fun consts_in_goal goal = consts_of_term goal;
mengj@18791
    58
fun get_goal_consts cs = foldl (op union_string) [] (map consts_in_goal cs);
mengj@18791
    59
mengj@18791
    60
fun pconsts_in_goal goal = pconsts_of_term goal;
mengj@18791
    61
fun get_goal_pconsts cs = foldl (op union) [] (map pconsts_in_goal cs);
mengj@18791
    62
mengj@18791
    63
mengj@18791
    64
(*************************************************************************)
mengj@18791
    65
(*            the first relevance filtering strategy                     *)
mengj@18791
    66
(*************************************************************************)
mengj@18791
    67
mengj@18791
    68
fun find_clause_weight_s_1 (refconsts : string list) consts wa = 
mengj@18791
    69
    let val (rel,irrel) = part refconsts consts ([],[])
mengj@18791
    70
    in
paulson@19208
    71
	(real (length rel) / real (length consts)) * wa
mengj@18791
    72
    end;
mengj@18791
    73
mengj@18791
    74
fun find_clause_weight_m_1 [] (_,w) = w 
mengj@18791
    75
  | find_clause_weight_m_1 ((_,(refconsts,wa))::y) (consts,w) =
paulson@19208
    76
      let val w' = find_clause_weight_s_1 refconsts consts wa
paulson@19208
    77
      in
paulson@19208
    78
	if w < w' then find_clause_weight_m_1 y (consts,w')
mengj@18791
    79
	else find_clause_weight_m_1 y (consts,w)
paulson@19208
    80
      end;
mengj@18791
    81
mengj@18791
    82
mengj@18791
    83
fun relevant_clauses_ax_g_1 _ []  _ (ax,r) = (ax,r)
mengj@19200
    84
  | relevant_clauses_ax_g_1 gconsts  ((clstm,(consts,_))::y) P (ax,r) =
paulson@19208
    85
      let val weight = find_clause_weight_s_1 gconsts consts 1.0
paulson@19208
    86
      in
paulson@19208
    87
	if  P <= weight 
paulson@19208
    88
	then relevant_clauses_ax_g_1 gconsts y P ((clstm,(consts,weight))::ax,r)
mengj@19200
    89
	else relevant_clauses_ax_g_1 gconsts y P (ax,(clstm,(consts,weight))::r)
paulson@19208
    90
      end;
mengj@18791
    91
mengj@18791
    92
mengj@18791
    93
fun relevant_clauses_ax_1 rel_axs  [] P (addc,tmpc) keep = 
mengj@18791
    94
    (case addc of [] => rel_axs @ keep
mengj@18791
    95
		| _ => case tmpc of [] => addc @ rel_axs @ keep
mengj@18791
    96
				  | _ => relevant_clauses_ax_1 addc tmpc P ([],[]) (rel_axs @ keep))
mengj@19200
    97
  | relevant_clauses_ax_1 rel_axs ((clstm,(consts,weight))::e_axs) P (addc,tmpc) keep = 
paulson@19208
    98
      let val weight' = find_clause_weight_m_1 rel_axs (consts,weight) 
paulson@19208
    99
	  val e_ax' = (clstm,(consts, weight'))
paulson@19208
   100
      in
paulson@19208
   101
	if P <= weight' 
paulson@19208
   102
	then relevant_clauses_ax_1 rel_axs e_axs P ((clstm,(consts,weight'))::addc,tmpc) keep
mengj@19200
   103
	else relevant_clauses_ax_1 rel_axs e_axs P (addc,(clstm,(consts,weight'))::tmpc) keep 
paulson@19208
   104
      end;
mengj@18791
   105
mengj@18791
   106
mengj@18791
   107
fun initialize [] ax_weights = ax_weights
mengj@19200
   108
  | initialize ((tm,name)::tms_names) ax_weights =
paulson@19208
   109
      let val consts = consts_of_term tm
paulson@19208
   110
      in
paulson@19208
   111
	  initialize tms_names (((tm,name),(consts,0.0))::ax_weights)
paulson@19208
   112
      end;
mengj@18791
   113
mengj@18791
   114
fun relevance_filter1_aux axioms goals = 
mengj@18791
   115
    let val pass = !pass_mark
mengj@18791
   116
	val axioms_weights = initialize axioms []
mengj@18791
   117
	val goals_consts = get_goal_consts goals
mengj@18791
   118
	val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_1 goals_consts axioms_weights pass ([],[]) 
mengj@18791
   119
    in
mengj@18791
   120
	relevant_clauses_ax_1 rel_clauses nrel_clauses pass ([],[]) []
mengj@18791
   121
    end;
mengj@18791
   122
mengj@18791
   123
fun relevance_filter1 axioms goals = map fst (relevance_filter1_aux axioms goals);
mengj@18791
   124
mengj@18791
   125
mengj@18791
   126
(*************************************************************************)
mengj@18791
   127
(*            the second relevance filtering strategy                    *)
mengj@18791
   128
(*************************************************************************)
mengj@18791
   129
mengj@18791
   130
fun find_clause_weight_s_2 (refpconsts : (bool * string) list) pconsts wa = 
mengj@18791
   131
    let val (rel,irrel) = part_w_pol refpconsts pconsts ([],[])
mengj@18791
   132
    in
mengj@18791
   133
	((real (length rel))/(real (length pconsts))) * wa
mengj@18791
   134
    end;
mengj@18791
   135
mengj@18791
   136
fun find_clause_weight_m_2 [] (_,w) = w 
mengj@18791
   137
  | find_clause_weight_m_2 ((_,(refpconsts,wa))::y) (pconsts,w) =
mengj@18791
   138
    let val w' = find_clause_weight_s_2 refpconsts pconsts wa
mengj@18791
   139
    in
mengj@18791
   140
	if (w < w') then find_clause_weight_m_2 y (pconsts,w')
mengj@18791
   141
	else find_clause_weight_m_2 y (pconsts,w)
mengj@18791
   142
    end;
mengj@18791
   143
mengj@18791
   144
mengj@18791
   145
fun relevant_clauses_ax_g_2 _ []  _ (ax,r) = (ax,r)
mengj@19200
   146
  | relevant_clauses_ax_g_2 gpconsts  ((clstm,(pconsts,_))::y) P (ax,r) =
mengj@18791
   147
    let val weight = find_clause_weight_s_2 gpconsts pconsts 1.0
mengj@18791
   148
    in
mengj@19200
   149
	if  P <= weight then relevant_clauses_ax_g_2 gpconsts y P ((clstm,(pconsts,weight))::ax,r)
mengj@19200
   150
	else relevant_clauses_ax_g_2 gpconsts y P (ax,(clstm,(pconsts,weight))::r)
mengj@18791
   151
    end;
mengj@18791
   152
mengj@18791
   153
mengj@18791
   154
fun relevant_clauses_ax_2 rel_axs  [] P (addc,tmpc) keep = 
mengj@18791
   155
    (case addc of [] => rel_axs @ keep
mengj@18791
   156
		| _ => case tmpc of [] => addc @ rel_axs @ keep
mengj@18791
   157
				  | _ => relevant_clauses_ax_2 addc tmpc P ([],[]) (rel_axs @ keep))
mengj@19200
   158
  | relevant_clauses_ax_2 rel_axs ((clstm,(pconsts,weight))::e_axs) P (addc,tmpc) keep = 
mengj@18791
   159
    let val weight' = find_clause_weight_m_2 rel_axs (pconsts,weight) 
mengj@19200
   160
	val e_ax' = (clstm,(pconsts, weight'))
mengj@18791
   161
    in
mengj@18791
   162
	
mengj@19200
   163
	if P <= weight' then relevant_clauses_ax_2 rel_axs e_axs P ((clstm,(pconsts,weight'))::addc,tmpc) keep
mengj@19200
   164
	else relevant_clauses_ax_2 rel_axs e_axs P (addc,(clstm,(pconsts,weight'))::tmpc) keep 
mengj@18791
   165
    end;
mengj@18791
   166
mengj@18791
   167
mengj@18791
   168
fun initialize_w_pol [] ax_weights = ax_weights
mengj@19200
   169
  | initialize_w_pol ((tm,name)::tms_names) ax_weights =
mengj@19200
   170
    let val consts = pconsts_of_term tm
mengj@18791
   171
    in
mengj@19200
   172
	initialize_w_pol tms_names (((tm,name),(consts,0.0))::ax_weights)
mengj@18791
   173
    end;
mengj@18791
   174
mengj@18791
   175
mengj@18791
   176
fun relevance_filter2_aux axioms goals = 
mengj@18791
   177
    let val pass = !pass_mark
mengj@18791
   178
	val axioms_weights = initialize_w_pol axioms []
mengj@18791
   179
	val goals_consts = get_goal_pconsts goals
mengj@18791
   180
	val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_2 goals_consts axioms_weights pass ([],[]) 
mengj@18791
   181
    in
mengj@18791
   182
	relevant_clauses_ax_2 rel_clauses nrel_clauses pass ([],[]) []
mengj@18791
   183
    end;
mengj@18791
   184
mengj@18791
   185
fun relevance_filter2 axioms goals = map fst (relevance_filter2_aux axioms goals);
mengj@18791
   186
mengj@19009
   187
(******************************************************************)
mengj@19009
   188
(*       the third relevance filtering strategy                   *)
mengj@19009
   189
(******************************************************************)
mengj@18791
   190
mengj@19009
   191
(*** unit clauses ***)
mengj@19009
   192
datatype clause_type = Unit_neq | Unit_geq | Other
mengj@19009
   193
paulson@19208
   194
(*Whether all "simple" unit clauses should be included*)
mengj@19009
   195
val add_unit = ref true;
mengj@19009
   196
mengj@19009
   197
fun literals_of_term args (Const ("Trueprop",_) $ P) = literals_of_term args P
mengj@19009
   198
  | literals_of_term args (Const ("op |",_) $ P $ Q) = 
mengj@19009
   199
    literals_of_term (literals_of_term args P) Q
paulson@19208
   200
  | literals_of_term args P = P::args;
mengj@19009
   201
paulson@19208
   202
fun is_ground t = (term_vars t = []) andalso (term_frees t = []);
mengj@19009
   203
mengj@19009
   204
fun eq_clause_type (P,Q) = 
mengj@19009
   205
    if ((is_ground P) orelse (is_ground Q)) then Unit_geq else Other;
mengj@19009
   206
mengj@19009
   207
fun unit_clause_type (Const ("op =",_) $ P $ Q) = eq_clause_type (P,Q)
mengj@19009
   208
  | unit_clause_type _ = Unit_neq;
mengj@19009
   209
mengj@19009
   210
fun clause_type tm = 
paulson@19208
   211
    case literals_of_term [] tm of
paulson@19208
   212
        [lit] => unit_clause_type lit
paulson@19208
   213
      | _ => Other;
mengj@19009
   214
mengj@19009
   215
(*** constants with types ***)
mengj@19009
   216
mengj@19009
   217
datatype const_typ =  CTVar | CType of string * const_typ list
mengj@19009
   218
paulson@19208
   219
fun uni_type (CType(con1,args1)) (CType(con2,args2)) = con1=con2 andalso uni_types args1 args2
paulson@19208
   220
  | uni_type (CType _) CTVar = true
mengj@19009
   221
  | uni_type CTVar CTVar = true
mengj@19009
   222
  | uni_type CTVar _ = false
paulson@19208
   223
and uni_types [] [] = true
paulson@19208
   224
  | uni_types (a1::as1) (a2::as2) = uni_type a1 a2 andalso uni_types as1 as2;
mengj@19009
   225
mengj@19009
   226
mengj@19009
   227
fun uni_constants (c1,ctp1) (c2,ctp2) = (c1 = c2) andalso (uni_types ctp1 ctp2);
mengj@19009
   228
mengj@19009
   229
fun uni_mem _ [] = false
paulson@19208
   230
  | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) =
paulson@19208
   231
      uni_constants (c1,c_typ1) (c,c_typ) orelse uni_mem (c,c_typ) ctyps;
mengj@19009
   232
mengj@19009
   233
fun const_typ_of (Type (c,typs)) = CType (c,map const_typ_of typs) 
mengj@19009
   234
  | const_typ_of (TFree(_,_)) = CTVar
mengj@19009
   235
  | const_typ_of (TVar(_,_)) = CTVar
mengj@19009
   236
mengj@19009
   237
paulson@19212
   238
fun const_w_typ thy (c,typ) = 
paulson@19212
   239
    let val tvars = Sign.const_typargs thy (c,typ)
paulson@19212
   240
    in (c, map const_typ_of tvars) end;
mengj@19009
   241
paulson@19212
   242
fun add_term_consts_typs_rm thy ncs (Const(c, typ)) cs =
paulson@19212
   243
      if (c mem ncs) then cs else (const_w_typ thy (c,typ) ins cs)
mengj@19009
   244
  | add_term_consts_typs_rm thy ncs (t $ u) cs =
mengj@19009
   245
      add_term_consts_typs_rm thy ncs  t (add_term_consts_typs_rm thy ncs u cs)
mengj@19009
   246
  | add_term_consts_typs_rm thy ncs (Abs(_,_,t)) cs = add_term_consts_typs_rm thy ncs t cs
mengj@19009
   247
  | add_term_consts_typs_rm thy ncs _ cs = cs;
mengj@19009
   248
mengj@19009
   249
fun term_consts_typs_rm thy ncs t = add_term_consts_typs_rm thy ncs t [];
mengj@19009
   250
paulson@19208
   251
fun consts_typs_of_term thy = term_consts_typs_rm thy standard_consts;
mengj@19009
   252
paulson@19208
   253
fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs)
mengj@19009
   254
paulson@19212
   255
fun lookup_or_zero (c,tab) =
paulson@19212
   256
    case Symtab.lookup tab c of
paulson@19212
   257
        NONE => 0
paulson@19212
   258
      | SOME n => n
paulson@19212
   259
paulson@19212
   260
fun count_term_consts (Const(c,_), tab) =
paulson@19212
   261
      Symtab.update (c, 1 + lookup_or_zero (c,tab)) tab
paulson@19212
   262
  | count_term_consts (t $ u, tab) =
paulson@19212
   263
      count_term_consts (t, count_term_consts (u, tab))
paulson@19212
   264
  | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
paulson@19212
   265
  | count_term_consts (_, tab) = tab;
paulson@19212
   266
paulson@19212
   267
fun count_axiom_consts ((tm,_), tab) = count_term_consts (tm, tab);
paulson@19212
   268
mengj@19009
   269
mengj@19009
   270
(******** filter clauses ********)
mengj@19009
   271
paulson@19212
   272
(*The default ignores the constant-count and gives the old Strategy 3*)
paulson@19212
   273
val weight_fn = ref (fn x : real => 1.0);
paulson@19212
   274
paulson@19212
   275
fun add_ct_weight ctab ((c,_), w) =
paulson@19212
   276
  w + !weight_fn (100.0 / real (Option.valOf (Symtab.lookup ctab c)));
paulson@19212
   277
paulson@19212
   278
fun consts_typs_weight ctab =
paulson@19212
   279
    List.foldl (add_ct_weight ctab) 0.0;
paulson@19212
   280
paulson@19212
   281
fun clause_weight_s_3 ctab gctyps consts_typs =
paulson@19208
   282
    let val rel = filter (fn s => uni_mem s gctyps) consts_typs
mengj@19009
   283
    in
paulson@19212
   284
	(consts_typs_weight ctab rel) / (consts_typs_weight ctab consts_typs)
mengj@19009
   285
    end;
mengj@19009
   286
paulson@19212
   287
fun find_clause_weight_s_3_alt ctab consts_typs (_,(refconsts_typs,wa)) =
paulson@19212
   288
    wa * clause_weight_s_3 ctab refconsts_typs consts_typs;
paulson@19208
   289
paulson@19212
   290
fun relevant_clauses_ax_3 ctab rel_axs [] P (addc,tmpc) keep =
paulson@19208
   291
      if null addc orelse null tmpc 
paulson@19208
   292
      then (addc @ rel_axs @ keep, tmpc)   (*termination!*)
paulson@19212
   293
      else relevant_clauses_ax_3 ctab addc tmpc P ([],[]) (rel_axs @ keep)
paulson@19212
   294
  | relevant_clauses_ax_3 ctab rel_axs ((clstm,(consts_typs,weight))::e_axs) P (addc,tmpc) keep =
paulson@19212
   295
      let val weights = map (find_clause_weight_s_3_alt ctab consts_typs) rel_axs
paulson@19208
   296
          val weight' = List.foldl Real.max weight weights
paulson@19212
   297
	  val e_ax' = (clstm, (consts_typs,weight'))
paulson@19208
   298
      in
paulson@19212
   299
	if P <= weight' 
paulson@19212
   300
	then relevant_clauses_ax_3 ctab rel_axs e_axs P (e_ax'::addc, tmpc) keep
paulson@19212
   301
	else relevant_clauses_ax_3 ctab rel_axs e_axs P (addc, e_ax'::tmpc) keep
paulson@19208
   302
      end;
mengj@19009
   303
paulson@19212
   304
fun weight_of_axiom thy (tm,name) =
paulson@19212
   305
    ((tm,name), (consts_typs_of_term thy tm));
mengj@19009
   306
paulson@19212
   307
fun safe_unit_clause ((clstm,_), _) = 
paulson@19212
   308
      case clause_type clstm of
paulson@19212
   309
	  Unit_neq => true
paulson@19212
   310
	| Unit_geq => true
paulson@19212
   311
	| Other => false;
mengj@19009
   312
mengj@19009
   313
fun relevance_filter3_aux thy axioms goals = 
mengj@19009
   314
    let val pass = !pass_mark
paulson@19212
   315
	val const_tab = List.foldl count_axiom_consts Symtab.empty axioms
mengj@19009
   316
	val goals_consts_typs = get_goal_consts_typs thy goals
paulson@19212
   317
	fun relevant [] (ax,r) = (ax,r)
paulson@19212
   318
	  | relevant ((clstm,consts_typs)::y) (ax,r) =
paulson@19212
   319
	      let val weight = clause_weight_s_3 const_tab goals_consts_typs consts_typs
paulson@19212
   320
		  val ccc = (clstm, (consts_typs,weight))
paulson@19212
   321
	      in
paulson@19212
   322
		if pass <= weight 
paulson@19212
   323
		then relevant y (ccc::ax, r)
paulson@19212
   324
		else relevant y (ax, ccc::r)
paulson@19212
   325
	      end
paulson@19208
   326
	val (rel_clauses,nrel_clauses) =
paulson@19212
   327
	    relevant (map (weight_of_axiom thy) axioms) ([],[]) 
paulson@19212
   328
	val (ax,r) = relevant_clauses_ax_3 const_tab rel_clauses nrel_clauses pass ([],[]) []
mengj@19009
   329
    in
paulson@19212
   330
	if !add_unit then (filter safe_unit_clause r) @ ax 
paulson@19212
   331
	else ax
mengj@19009
   332
    end;
mengj@19009
   333
paulson@19208
   334
fun relevance_filter3 thy axioms goals =
paulson@19212
   335
  map #1 (relevance_filter3_aux thy axioms goals);
mengj@19009
   336
    
mengj@18791
   337
mengj@18791
   338
(******************************************************************)
mengj@18791
   339
(* Generic functions for relevance filtering                      *)
mengj@18791
   340
(******************************************************************)
mengj@18791
   341
mengj@18791
   342
exception RELEVANCE_FILTER of string;
mengj@18791
   343
mengj@19009
   344
fun relevance_filter thy axioms goals = 
paulson@19208
   345
  case (!strategy) of 1 => relevance_filter1 axioms goals
paulson@19208
   346
		    | 2 => relevance_filter2 axioms goals
paulson@19208
   347
		    | 3 => relevance_filter3 thy axioms goals
paulson@19208
   348
		    | _ => raise RELEVANCE_FILTER("strategy doesn't exist");
mengj@18791
   349
mengj@18791
   350
end;