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