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