src/HOL/Tools/ATP/reduce_axiomsN.ML
author paulson
Tue Mar 07 16:49:48 2006 +0100 (2006-03-07)
changeset 19208 3e8006cbc925
parent 19200 1da6b9a1575d
child 19212 ec53c138277a
permissions -rw-r--r--
Tidying and restructuring.
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
mengj@19009
   238
fun const_w_typ thy (c,tp) = 
mengj@19009
   239
    let val tvars = Sign.const_typargs thy (c,tp)
mengj@19009
   240
    in
mengj@19009
   241
	(c,map const_typ_of tvars)
mengj@19009
   242
    end;
mengj@19009
   243
paulson@19208
   244
fun add_term_consts_typs_rm thy ncs (Const(c, tp)) cs =
paulson@19208
   245
      if (c mem ncs) then cs else (const_w_typ thy (c,tp) ins cs)
mengj@19009
   246
  | add_term_consts_typs_rm thy ncs (t $ u) cs =
mengj@19009
   247
      add_term_consts_typs_rm thy ncs  t (add_term_consts_typs_rm thy ncs u cs)
mengj@19009
   248
  | add_term_consts_typs_rm thy ncs (Abs(_,_,t)) cs = add_term_consts_typs_rm thy ncs t cs
mengj@19009
   249
  | add_term_consts_typs_rm thy ncs _ cs = cs;
mengj@19009
   250
mengj@19009
   251
fun term_consts_typs_rm thy ncs t = add_term_consts_typs_rm thy ncs t [];
mengj@19009
   252
paulson@19208
   253
fun consts_typs_of_term thy = term_consts_typs_rm thy standard_consts;
mengj@19009
   254
paulson@19208
   255
fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs)
mengj@19009
   256
mengj@19009
   257
mengj@19009
   258
(******** filter clauses ********)
mengj@19009
   259
mengj@19009
   260
fun find_clause_weight_s_3 gctyps consts_typs wa =
paulson@19208
   261
    let val rel = filter (fn s => uni_mem s gctyps) consts_typs
mengj@19009
   262
    in
paulson@19208
   263
	(real (length rel) / real (length consts_typs)) * wa
mengj@19009
   264
    end;
mengj@19009
   265
mengj@19009
   266
fun relevant_clauses_ax_g_3 _ [] _ (ax,r) = (ax,r)
mengj@19200
   267
  | relevant_clauses_ax_g_3 gctyps ((cls_typ,(clstm,(consts_typs,_)))::y) P (ax,r) =
paulson@19208
   268
      let val weight = find_clause_weight_s_3 gctyps consts_typs 1.0
paulson@19208
   269
          val ccc = (cls_typ, (clstm, (consts_typs,weight)))
paulson@19208
   270
      in
paulson@19208
   271
	if P <= weight 
paulson@19208
   272
	then relevant_clauses_ax_g_3 gctyps y P (ccc::ax, r)
paulson@19208
   273
	else relevant_clauses_ax_g_3 gctyps y P (ax, ccc::r)
paulson@19208
   274
      end;
paulson@19208
   275
paulson@19208
   276
fun find_clause_weight_s_3_alt consts_typs (_,(_,(refconsts_typs,wa))) =
paulson@19208
   277
    find_clause_weight_s_3 refconsts_typs consts_typs wa;
mengj@19009
   278
mengj@19009
   279
fun relevant_clauses_ax_3 rel_axs [] P (addc,tmpc) keep =
paulson@19208
   280
      if null addc orelse null tmpc 
paulson@19208
   281
      then (addc @ rel_axs @ keep, tmpc)   (*termination!*)
paulson@19208
   282
      else relevant_clauses_ax_3 addc tmpc P ([],[]) (rel_axs @ keep)
mengj@19200
   283
  | relevant_clauses_ax_3 rel_axs ((cls_typ,(clstm,(consts_typs,weight)))::e_axs) P (addc,tmpc) keep =
paulson@19208
   284
      let val weights = map (find_clause_weight_s_3_alt consts_typs) rel_axs
paulson@19208
   285
          val weight' = List.foldl Real.max weight weights
paulson@19208
   286
	  val e_ax' = (cls_typ,(clstm,(consts_typs,weight')))
paulson@19208
   287
      in
mengj@19009
   288
	if P <= weight' then relevant_clauses_ax_3 rel_axs e_axs P (e_ax'::addc,tmpc) keep
mengj@19009
   289
	else relevant_clauses_ax_3 rel_axs e_axs P (addc,e_ax'::tmpc) keep
paulson@19208
   290
      end;
mengj@19009
   291
mengj@19009
   292
fun initialize3 thy [] ax_weights = ax_weights
mengj@19200
   293
  | initialize3 thy ((tm,name)::tms_names) ax_weights =
mengj@19200
   294
    let val cls_type = clause_type tm
mengj@19009
   295
	val consts = consts_typs_of_term thy tm
mengj@19009
   296
    in
mengj@19200
   297
	initialize3 thy tms_names ((cls_type,((tm,name),(consts,0.0)))::ax_weights)
mengj@19009
   298
    end;
mengj@19009
   299
mengj@19009
   300
fun add_unit_clauses ax [] = ax
mengj@19009
   301
  | add_unit_clauses ax ((cls_typ,consts_weight)::cs) =
mengj@19009
   302
    case cls_typ of Unit_neq => add_unit_clauses ((cls_typ,consts_weight)::ax) cs
mengj@19009
   303
		  | Unit_geq => add_unit_clauses ((cls_typ,consts_weight)::ax) cs
mengj@19009
   304
		  | Other => add_unit_clauses ax cs;
mengj@19009
   305
mengj@19009
   306
fun relevance_filter3_aux thy axioms goals = 
mengj@19009
   307
    let val pass = !pass_mark
mengj@19009
   308
	val axioms_weights = initialize3 thy axioms []
mengj@19009
   309
	val goals_consts_typs = get_goal_consts_typs thy goals
paulson@19208
   310
	val (rel_clauses,nrel_clauses) =
paulson@19208
   311
	    relevant_clauses_ax_g_3 goals_consts_typs axioms_weights pass ([],[]) 
mengj@19009
   312
	val (ax,r) = relevant_clauses_ax_3 rel_clauses nrel_clauses pass ([],[]) []
mengj@19009
   313
    in
paulson@19208
   314
	if !add_unit then add_unit_clauses ax r else ax
mengj@19009
   315
    end;
mengj@19009
   316
paulson@19208
   317
fun relevance_filter3 thy axioms goals =
paulson@19208
   318
  map (#1 o #2) (relevance_filter3_aux thy axioms goals);
mengj@19009
   319
    
mengj@18791
   320
mengj@18791
   321
(******************************************************************)
mengj@18791
   322
(* Generic functions for relevance filtering                      *)
mengj@18791
   323
(******************************************************************)
mengj@18791
   324
mengj@18791
   325
exception RELEVANCE_FILTER of string;
mengj@18791
   326
mengj@19009
   327
fun relevance_filter thy axioms goals = 
paulson@19208
   328
  case (!strategy) of 1 => relevance_filter1 axioms goals
paulson@19208
   329
		    | 2 => relevance_filter2 axioms goals
paulson@19208
   330
		    | 3 => relevance_filter3 thy axioms goals
paulson@19208
   331
		    | _ => raise RELEVANCE_FILTER("strategy doesn't exist");
mengj@18791
   332
mengj@18791
   333
end;