src/HOL/Tools/ATP/reduce_axiomsN.ML
author haftmann
Fri Feb 10 09:09:07 2006 +0100 (2006-02-10)
changeset 19008 14c1b2f5dda4
parent 18791 9b4ae9fa67a4
child 19009 bb29bf9d3a72
permissions -rw-r--r--
improved code generator devarification
mengj@18791
     1
structure ReduceAxiomsN =
mengj@18791
     2
(* Author: Jia Meng, Cambridge University Computer Laboratory
mengj@18791
     3
   
mengj@18791
     4
   Two filtering strategies *)
mengj@18791
     5
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)
mengj@18791
    15
  | part refs (s::ss) (s1,s2) = if (s mem refs) then (part refs ss (s::s1,s2)) else (part refs ss (s1,s::s2));
mengj@18791
    16
mengj@18791
    17
mengj@18791
    18
fun pol_mem _ [] = false
mengj@18791
    19
  | pol_mem (pol,const) ((p,c)::pcs) = if ((pol = not p) andalso (const = c)) then true else pol_mem (pol,const) pcs;
mengj@18791
    20
mengj@18791
    21
mengj@18791
    22
fun part_w_pol refs [] (s1,s2) = (s1,s2)
mengj@18791
    23
  | part_w_pol refs (s::ss) (s1,s2) = if (pol_mem s refs) then (part_w_pol refs ss (s::s1,s2)) else (part_w_pol refs ss (s1,s::s2));
mengj@18791
    24
mengj@18791
    25
mengj@18791
    26
fun add_term_consts_rm ncs (Const(c, _)) cs = if (c mem ncs) then cs else (c ins_string cs)
mengj@18791
    27
  | add_term_consts_rm ncs (t $ u) cs =
mengj@18791
    28
      add_term_consts_rm ncs t (add_term_consts_rm ncs u cs)
mengj@18791
    29
  | add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs
mengj@18791
    30
  | add_term_consts_rm ncs _ cs = cs;
mengj@18791
    31
mengj@18791
    32
fun term_consts_rm ncs t = add_term_consts_rm ncs t [];
mengj@18791
    33
mengj@18791
    34
fun consts_of_term term = term_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term;
mengj@18791
    35
mengj@18791
    36
mengj@18791
    37
fun add_term_pconsts_rm ncs (Const(c,_)) pol cs = if (c mem ncs) then cs else ((pol,c) ins cs)
mengj@18791
    38
  | add_term_pconsts_rm ncs (Const("Not",_)$P) pol cs = add_term_pconsts_rm ncs P (not pol) cs
mengj@18791
    39
  | add_term_pconsts_rm ncs (P$Q) pol cs = 
mengj@18791
    40
    add_term_pconsts_rm ncs P pol (add_term_pconsts_rm ncs Q pol cs)
mengj@18791
    41
  | add_term_pconsts_rm ncs (Abs(_,_,t)) pol cs = add_term_pconsts_rm ncs t pol cs
mengj@18791
    42
  | add_term_pconsts_rm ncs _ _ cs = cs;
mengj@18791
    43
mengj@18791
    44
mengj@18791
    45
fun term_pconsts_rm ncs t = add_term_pconsts_rm ncs t true [];
mengj@18791
    46
mengj@18791
    47
mengj@18791
    48
fun pconsts_of_term term = term_pconsts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term;
mengj@18791
    49
mengj@18791
    50
fun consts_in_goal goal = consts_of_term goal;
mengj@18791
    51
fun get_goal_consts cs = foldl (op union_string) [] (map consts_in_goal cs);
mengj@18791
    52
mengj@18791
    53
mengj@18791
    54
fun pconsts_in_goal goal = pconsts_of_term goal;
mengj@18791
    55
fun get_goal_pconsts cs = foldl (op union) [] (map pconsts_in_goal cs);
mengj@18791
    56
mengj@18791
    57
mengj@18791
    58
(*************************************************************************)
mengj@18791
    59
(*            the first relevance filtering strategy                     *)
mengj@18791
    60
(*************************************************************************)
mengj@18791
    61
mengj@18791
    62
fun find_clause_weight_s_1 (refconsts : string list) consts wa = 
mengj@18791
    63
    let val (rel,irrel) = part refconsts consts ([],[])
mengj@18791
    64
    in
mengj@18791
    65
	((real (length rel))/(real (length consts))) * wa
mengj@18791
    66
    end;
mengj@18791
    67
mengj@18791
    68
fun find_clause_weight_m_1 [] (_,w) = w 
mengj@18791
    69
  | find_clause_weight_m_1 ((_,(refconsts,wa))::y) (consts,w) =
mengj@18791
    70
    let val w' = find_clause_weight_s_1 refconsts consts wa
mengj@18791
    71
    in
mengj@18791
    72
	if (w < w') then find_clause_weight_m_1 y (consts,w')
mengj@18791
    73
	else find_clause_weight_m_1 y (consts,w)
mengj@18791
    74
    end;
mengj@18791
    75
mengj@18791
    76
mengj@18791
    77
fun relevant_clauses_ax_g_1 _ []  _ (ax,r) = (ax,r)
mengj@18791
    78
  | relevant_clauses_ax_g_1 gconsts  ((clsthm,(consts,_))::y) P (ax,r) =
mengj@18791
    79
    let val weight = find_clause_weight_s_1 gconsts consts 1.0
mengj@18791
    80
    in
mengj@18791
    81
	if  P <= weight then relevant_clauses_ax_g_1 gconsts y P ((clsthm,(consts,weight))::ax,r)
mengj@18791
    82
	else relevant_clauses_ax_g_1 gconsts y P (ax,(clsthm,(consts,weight))::r)
mengj@18791
    83
    end;
mengj@18791
    84
mengj@18791
    85
mengj@18791
    86
fun relevant_clauses_ax_1 rel_axs  [] P (addc,tmpc) keep = 
mengj@18791
    87
    (case addc of [] => rel_axs @ keep
mengj@18791
    88
		| _ => case tmpc of [] => addc @ rel_axs @ keep
mengj@18791
    89
				  | _ => relevant_clauses_ax_1 addc tmpc P ([],[]) (rel_axs @ keep))
mengj@18791
    90
  | relevant_clauses_ax_1 rel_axs ((clsthm,(consts,weight))::e_axs) P (addc,tmpc) keep = 
mengj@18791
    91
    let val weight' = find_clause_weight_m_1 rel_axs (consts,weight) 
mengj@18791
    92
	val e_ax' = (clsthm,(consts, weight'))
mengj@18791
    93
    in
mengj@18791
    94
	
mengj@18791
    95
	if P <= weight' then relevant_clauses_ax_1 rel_axs e_axs P ((clsthm,(consts,weight'))::addc,tmpc) keep
mengj@18791
    96
	else relevant_clauses_ax_1 rel_axs e_axs P (addc,(clsthm,(consts,weight'))::tmpc) keep 
mengj@18791
    97
    end;
mengj@18791
    98
mengj@18791
    99
mengj@18791
   100
fun initialize [] ax_weights = ax_weights
mengj@18791
   101
  | initialize ((cls,thm)::clss_thms) ax_weights =
mengj@18791
   102
    let val tm = prop_of thm
mengj@18791
   103
	val consts = consts_of_term tm
mengj@18791
   104
    in
mengj@18791
   105
	initialize clss_thms (((cls,thm),(consts,0.0))::ax_weights)
mengj@18791
   106
    end;
mengj@18791
   107
mengj@18791
   108
fun relevance_filter1_aux axioms goals = 
mengj@18791
   109
    let val pass = !pass_mark
mengj@18791
   110
	val axioms_weights = initialize axioms []
mengj@18791
   111
	val goals_consts = get_goal_consts goals
mengj@18791
   112
	val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_1 goals_consts axioms_weights pass ([],[]) 
mengj@18791
   113
    in
mengj@18791
   114
	relevant_clauses_ax_1 rel_clauses nrel_clauses pass ([],[]) []
mengj@18791
   115
    end;
mengj@18791
   116
mengj@18791
   117
fun relevance_filter1 axioms goals = map fst (relevance_filter1_aux axioms goals);
mengj@18791
   118
mengj@18791
   119
mengj@18791
   120
mengj@18791
   121
mengj@18791
   122
(*************************************************************************)
mengj@18791
   123
(*            the second relevance filtering strategy                    *)
mengj@18791
   124
(*************************************************************************)
mengj@18791
   125
mengj@18791
   126
fun find_clause_weight_s_2 (refpconsts : (bool * string) list) pconsts wa = 
mengj@18791
   127
    let val (rel,irrel) = part_w_pol refpconsts pconsts ([],[])
mengj@18791
   128
    in
mengj@18791
   129
	((real (length rel))/(real (length pconsts))) * wa
mengj@18791
   130
    end;
mengj@18791
   131
mengj@18791
   132
fun find_clause_weight_m_2 [] (_,w) = w 
mengj@18791
   133
  | find_clause_weight_m_2 ((_,(refpconsts,wa))::y) (pconsts,w) =
mengj@18791
   134
    let val w' = find_clause_weight_s_2 refpconsts pconsts wa
mengj@18791
   135
    in
mengj@18791
   136
	if (w < w') then find_clause_weight_m_2 y (pconsts,w')
mengj@18791
   137
	else find_clause_weight_m_2 y (pconsts,w)
mengj@18791
   138
    end;
mengj@18791
   139
mengj@18791
   140
mengj@18791
   141
fun relevant_clauses_ax_g_2 _ []  _ (ax,r) = (ax,r)
mengj@18791
   142
  | relevant_clauses_ax_g_2 gpconsts  ((clsthm,(pconsts,_))::y) P (ax,r) =
mengj@18791
   143
    let val weight = find_clause_weight_s_2 gpconsts pconsts 1.0
mengj@18791
   144
    in
mengj@18791
   145
	if  P <= weight then relevant_clauses_ax_g_2 gpconsts y P ((clsthm,(pconsts,weight))::ax,r)
mengj@18791
   146
	else relevant_clauses_ax_g_2 gpconsts y P (ax,(clsthm,(pconsts,weight))::r)
mengj@18791
   147
    end;
mengj@18791
   148
mengj@18791
   149
mengj@18791
   150
fun relevant_clauses_ax_2 rel_axs  [] P (addc,tmpc) keep = 
mengj@18791
   151
    (case addc of [] => rel_axs @ keep
mengj@18791
   152
		| _ => case tmpc of [] => addc @ rel_axs @ keep
mengj@18791
   153
				  | _ => relevant_clauses_ax_2 addc tmpc P ([],[]) (rel_axs @ keep))
mengj@18791
   154
  | relevant_clauses_ax_2 rel_axs ((clsthm,(pconsts,weight))::e_axs) P (addc,tmpc) keep = 
mengj@18791
   155
    let val weight' = find_clause_weight_m_2 rel_axs (pconsts,weight) 
mengj@18791
   156
	val e_ax' = (clsthm,(pconsts, weight'))
mengj@18791
   157
    in
mengj@18791
   158
	
mengj@18791
   159
	if P <= weight' then relevant_clauses_ax_2 rel_axs e_axs P ((clsthm,(pconsts,weight'))::addc,tmpc) keep
mengj@18791
   160
	else relevant_clauses_ax_2 rel_axs e_axs P (addc,(clsthm,(pconsts,weight'))::tmpc) keep 
mengj@18791
   161
    end;
mengj@18791
   162
mengj@18791
   163
mengj@18791
   164
fun initialize_w_pol [] ax_weights = ax_weights
mengj@18791
   165
  | initialize_w_pol ((cls,thm)::clss_thms) ax_weights =
mengj@18791
   166
    let val tm = prop_of thm
mengj@18791
   167
	val consts = pconsts_of_term tm
mengj@18791
   168
    in
mengj@18791
   169
	initialize_w_pol clss_thms (((cls,thm),(consts,0.0))::ax_weights)
mengj@18791
   170
    end;
mengj@18791
   171
mengj@18791
   172
mengj@18791
   173
fun relevance_filter2_aux axioms goals = 
mengj@18791
   174
    let val pass = !pass_mark
mengj@18791
   175
	val axioms_weights = initialize_w_pol axioms []
mengj@18791
   176
	val goals_consts = get_goal_pconsts goals
mengj@18791
   177
	val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_2 goals_consts axioms_weights pass ([],[]) 
mengj@18791
   178
    in
mengj@18791
   179
	relevant_clauses_ax_2 rel_clauses nrel_clauses pass ([],[]) []
mengj@18791
   180
    end;
mengj@18791
   181
mengj@18791
   182
fun relevance_filter2 axioms goals = map fst (relevance_filter2_aux axioms goals);
mengj@18791
   183
mengj@18791
   184
mengj@18791
   185
mengj@18791
   186
mengj@18791
   187
(******************************************************************)
mengj@18791
   188
(* Generic functions for relevance filtering                      *)
mengj@18791
   189
(******************************************************************)
mengj@18791
   190
mengj@18791
   191
exception RELEVANCE_FILTER of string;
mengj@18791
   192
mengj@18791
   193
fun relevance_filter axioms goals = 
mengj@18791
   194
    let val cls = (case (!strategy) of 1 => relevance_filter1 axioms goals
mengj@18791
   195
				     | 2 => relevance_filter2 axioms goals
mengj@18791
   196
				     | _ => raise RELEVANCE_FILTER("strategy doesn't exists"))
mengj@18791
   197
    in
mengj@18791
   198
	cls
mengj@18791
   199
    end;
mengj@18791
   200
mengj@18791
   201
mengj@18791
   202
end;