Frequency strategy. Revised indentation, etc.
(* Authors: Jia Meng, NICTA and Lawrence C Paulson, Cambridge University Computer Laboratory
ID: $Id$
Filtering strategies *)
structure ReduceAxiomsN =
struct
val pass_mark = ref 0.5;
val strategy = ref 1;
fun pol_to_int true = 1
| pol_to_int false = ~1;
fun part refs [] (s1,s2) = (s1,s2)
| part refs (s::ss) (s1,s2) =
if (s mem refs) then part refs ss (s::s1,s2) else part refs ss (s1,s::s2);
fun pol_mem _ [] = false
| pol_mem (pol,const) ((p,c)::pcs) =
(pol = not p andalso const = c) orelse pol_mem (pol,const) pcs;
fun part_w_pol refs [] (s1,s2) = (s1,s2)
| 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);
fun add_term_consts_rm ncs (Const(c, _)) cs =
if (c mem ncs) then cs else (c ins_string cs)
| add_term_consts_rm ncs (t $ u) cs =
add_term_consts_rm ncs t (add_term_consts_rm ncs u cs)
| add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs
| add_term_consts_rm ncs _ cs = cs;
fun term_consts_rm ncs t = add_term_consts_rm ncs t [];
val standard_consts =
["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->","op =","==","True","False"];
val consts_of_term = term_consts_rm standard_consts;
fun add_term_pconsts_rm ncs (Const(c,_)) pol cs = if c mem ncs then cs else ((pol,c) ins cs)
| add_term_pconsts_rm ncs (Const("Not",_)$P) pol cs = add_term_pconsts_rm ncs P (not pol) cs
| add_term_pconsts_rm ncs (P$Q) pol cs =
add_term_pconsts_rm ncs P pol (add_term_pconsts_rm ncs Q pol cs)
| add_term_pconsts_rm ncs (Abs(_,_,t)) pol cs = add_term_pconsts_rm ncs t pol cs
| add_term_pconsts_rm ncs _ _ cs = cs;
fun term_pconsts_rm ncs t = add_term_pconsts_rm ncs t true [];
val pconsts_of_term = term_pconsts_rm standard_consts;
fun consts_in_goal goal = consts_of_term goal;
fun get_goal_consts cs = foldl (op union_string) [] (map consts_in_goal cs);
fun pconsts_in_goal goal = pconsts_of_term goal;
fun get_goal_pconsts cs = foldl (op union) [] (map pconsts_in_goal cs);
(*************************************************************************)
(* the first relevance filtering strategy *)
(*************************************************************************)
fun find_clause_weight_s_1 (refconsts : string list) consts wa =
let val (rel,irrel) = part refconsts consts ([],[])
in
(real (length rel) / real (length consts)) * wa
end;
fun find_clause_weight_m_1 [] (_,w) = w
| find_clause_weight_m_1 ((_,(refconsts,wa))::y) (consts,w) =
let val w' = find_clause_weight_s_1 refconsts consts wa
in
if w < w' then find_clause_weight_m_1 y (consts,w')
else find_clause_weight_m_1 y (consts,w)
end;
fun relevant_clauses_ax_g_1 _ [] _ (ax,r) = (ax,r)
| relevant_clauses_ax_g_1 gconsts ((clstm,(consts,_))::y) P (ax,r) =
let val weight = find_clause_weight_s_1 gconsts consts 1.0
in
if P <= weight
then relevant_clauses_ax_g_1 gconsts y P ((clstm,(consts,weight))::ax,r)
else relevant_clauses_ax_g_1 gconsts y P (ax,(clstm,(consts,weight))::r)
end;
fun relevant_clauses_ax_1 rel_axs [] P (addc,tmpc) keep =
(case addc of [] => rel_axs @ keep
| _ => case tmpc of [] => addc @ rel_axs @ keep
| _ => relevant_clauses_ax_1 addc tmpc P ([],[]) (rel_axs @ keep))
| relevant_clauses_ax_1 rel_axs ((clstm,(consts,weight))::e_axs) P (addc,tmpc) keep =
let val weight' = find_clause_weight_m_1 rel_axs (consts,weight)
val e_ax' = (clstm,(consts, weight'))
in
if P <= weight'
then relevant_clauses_ax_1 rel_axs e_axs P ((clstm,(consts,weight'))::addc,tmpc) keep
else relevant_clauses_ax_1 rel_axs e_axs P (addc,(clstm,(consts,weight'))::tmpc) keep
end;
fun initialize [] ax_weights = ax_weights
| initialize ((tm,name)::tms_names) ax_weights =
let val consts = consts_of_term tm
in
initialize tms_names (((tm,name),(consts,0.0))::ax_weights)
end;
fun relevance_filter1_aux axioms goals =
let val pass = !pass_mark
val axioms_weights = initialize axioms []
val goals_consts = get_goal_consts goals
val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_1 goals_consts axioms_weights pass ([],[])
in
relevant_clauses_ax_1 rel_clauses nrel_clauses pass ([],[]) []
end;
fun relevance_filter1 axioms goals = map fst (relevance_filter1_aux axioms goals);
(*************************************************************************)
(* the second relevance filtering strategy *)
(*************************************************************************)
fun find_clause_weight_s_2 (refpconsts : (bool * string) list) pconsts wa =
let val (rel,irrel) = part_w_pol refpconsts pconsts ([],[])
in
((real (length rel))/(real (length pconsts))) * wa
end;
fun find_clause_weight_m_2 [] (_,w) = w
| find_clause_weight_m_2 ((_,(refpconsts,wa))::y) (pconsts,w) =
let val w' = find_clause_weight_s_2 refpconsts pconsts wa
in
if (w < w') then find_clause_weight_m_2 y (pconsts,w')
else find_clause_weight_m_2 y (pconsts,w)
end;
fun relevant_clauses_ax_g_2 _ [] _ (ax,r) = (ax,r)
| relevant_clauses_ax_g_2 gpconsts ((clstm,(pconsts,_))::y) P (ax,r) =
let val weight = find_clause_weight_s_2 gpconsts pconsts 1.0
in
if P <= weight then relevant_clauses_ax_g_2 gpconsts y P ((clstm,(pconsts,weight))::ax,r)
else relevant_clauses_ax_g_2 gpconsts y P (ax,(clstm,(pconsts,weight))::r)
end;
fun relevant_clauses_ax_2 rel_axs [] P (addc,tmpc) keep =
(case addc of [] => rel_axs @ keep
| _ => case tmpc of [] => addc @ rel_axs @ keep
| _ => relevant_clauses_ax_2 addc tmpc P ([],[]) (rel_axs @ keep))
| relevant_clauses_ax_2 rel_axs ((clstm,(pconsts,weight))::e_axs) P (addc,tmpc) keep =
let val weight' = find_clause_weight_m_2 rel_axs (pconsts,weight)
val e_ax' = (clstm,(pconsts, weight'))
in
if P <= weight' then relevant_clauses_ax_2 rel_axs e_axs P ((clstm,(pconsts,weight'))::addc,tmpc) keep
else relevant_clauses_ax_2 rel_axs e_axs P (addc,(clstm,(pconsts,weight'))::tmpc) keep
end;
fun initialize_w_pol [] ax_weights = ax_weights
| initialize_w_pol ((tm,name)::tms_names) ax_weights =
let val consts = pconsts_of_term tm
in
initialize_w_pol tms_names (((tm,name),(consts,0.0))::ax_weights)
end;
fun relevance_filter2_aux axioms goals =
let val pass = !pass_mark
val axioms_weights = initialize_w_pol axioms []
val goals_consts = get_goal_pconsts goals
val (rel_clauses,nrel_clauses) = relevant_clauses_ax_g_2 goals_consts axioms_weights pass ([],[])
in
relevant_clauses_ax_2 rel_clauses nrel_clauses pass ([],[]) []
end;
fun relevance_filter2 axioms goals = map fst (relevance_filter2_aux axioms goals);
(******************************************************************)
(* the third relevance filtering strategy *)
(******************************************************************)
(*** unit clauses ***)
datatype clause_type = Unit_neq | Unit_geq | Other
(*Whether all "simple" unit clauses should be included*)
val add_unit = ref true;
fun literals_of_term args (Const ("Trueprop",_) $ P) = literals_of_term args P
| literals_of_term args (Const ("op |",_) $ P $ Q) =
literals_of_term (literals_of_term args P) Q
| literals_of_term args P = P::args;
fun is_ground t = (term_vars t = []) andalso (term_frees t = []);
fun eq_clause_type (P,Q) =
if ((is_ground P) orelse (is_ground Q)) then Unit_geq else Other;
fun unit_clause_type (Const ("op =",_) $ P $ Q) = eq_clause_type (P,Q)
| unit_clause_type _ = Unit_neq;
fun clause_type tm =
case literals_of_term [] tm of
[lit] => unit_clause_type lit
| _ => Other;
(*** constants with types ***)
datatype const_typ = CTVar | CType of string * const_typ list
fun uni_type (CType(con1,args1)) (CType(con2,args2)) = con1=con2 andalso uni_types args1 args2
| uni_type (CType _) CTVar = true
| uni_type CTVar CTVar = true
| uni_type CTVar _ = false
and uni_types [] [] = true
| uni_types (a1::as1) (a2::as2) = uni_type a1 a2 andalso uni_types as1 as2;
fun uni_constants (c1,ctp1) (c2,ctp2) = (c1 = c2) andalso (uni_types ctp1 ctp2);
fun uni_mem _ [] = false
| uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) =
uni_constants (c1,c_typ1) (c,c_typ) orelse uni_mem (c,c_typ) ctyps;
fun const_typ_of (Type (c,typs)) = CType (c,map const_typ_of typs)
| const_typ_of (TFree(_,_)) = CTVar
| const_typ_of (TVar(_,_)) = CTVar
fun const_w_typ thy (c,typ) =
let val tvars = Sign.const_typargs thy (c,typ)
in (c, map const_typ_of tvars) end;
fun add_term_consts_typs_rm thy ncs (Const(c, typ)) cs =
if (c mem ncs) then cs else (const_w_typ thy (c,typ) ins cs)
| add_term_consts_typs_rm thy ncs (t $ u) cs =
add_term_consts_typs_rm thy ncs t (add_term_consts_typs_rm thy ncs u cs)
| add_term_consts_typs_rm thy ncs (Abs(_,_,t)) cs = add_term_consts_typs_rm thy ncs t cs
| add_term_consts_typs_rm thy ncs _ cs = cs;
fun term_consts_typs_rm thy ncs t = add_term_consts_typs_rm thy ncs t [];
fun consts_typs_of_term thy = term_consts_typs_rm thy standard_consts;
fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs)
fun lookup_or_zero (c,tab) =
case Symtab.lookup tab c of
NONE => 0
| SOME n => n
fun count_term_consts (Const(c,_), tab) =
Symtab.update (c, 1 + lookup_or_zero (c,tab)) tab
| count_term_consts (t $ u, tab) =
count_term_consts (t, count_term_consts (u, tab))
| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
| count_term_consts (_, tab) = tab;
fun count_axiom_consts ((tm,_), tab) = count_term_consts (tm, tab);
(******** filter clauses ********)
(*The default ignores the constant-count and gives the old Strategy 3*)
val weight_fn = ref (fn x : real => 1.0);
fun add_ct_weight ctab ((c,_), w) =
w + !weight_fn (100.0 / real (Option.valOf (Symtab.lookup ctab c)));
fun consts_typs_weight ctab =
List.foldl (add_ct_weight ctab) 0.0;
fun clause_weight_s_3 ctab gctyps consts_typs =
let val rel = filter (fn s => uni_mem s gctyps) consts_typs
in
(consts_typs_weight ctab rel) / (consts_typs_weight ctab consts_typs)
end;
fun find_clause_weight_s_3_alt ctab consts_typs (_,(refconsts_typs,wa)) =
wa * clause_weight_s_3 ctab refconsts_typs consts_typs;
fun relevant_clauses_ax_3 ctab rel_axs [] P (addc,tmpc) keep =
if null addc orelse null tmpc
then (addc @ rel_axs @ keep, tmpc) (*termination!*)
else relevant_clauses_ax_3 ctab addc tmpc P ([],[]) (rel_axs @ keep)
| relevant_clauses_ax_3 ctab rel_axs ((clstm,(consts_typs,weight))::e_axs) P (addc,tmpc) keep =
let val weights = map (find_clause_weight_s_3_alt ctab consts_typs) rel_axs
val weight' = List.foldl Real.max weight weights
val e_ax' = (clstm, (consts_typs,weight'))
in
if P <= weight'
then relevant_clauses_ax_3 ctab rel_axs e_axs P (e_ax'::addc, tmpc) keep
else relevant_clauses_ax_3 ctab rel_axs e_axs P (addc, e_ax'::tmpc) keep
end;
fun weight_of_axiom thy (tm,name) =
((tm,name), (consts_typs_of_term thy tm));
fun safe_unit_clause ((clstm,_), _) =
case clause_type clstm of
Unit_neq => true
| Unit_geq => true
| Other => false;
fun relevance_filter3_aux thy axioms goals =
let val pass = !pass_mark
val const_tab = List.foldl count_axiom_consts Symtab.empty axioms
val goals_consts_typs = get_goal_consts_typs thy goals
fun relevant [] (ax,r) = (ax,r)
| relevant ((clstm,consts_typs)::y) (ax,r) =
let val weight = clause_weight_s_3 const_tab goals_consts_typs consts_typs
val ccc = (clstm, (consts_typs,weight))
in
if pass <= weight
then relevant y (ccc::ax, r)
else relevant y (ax, ccc::r)
end
val (rel_clauses,nrel_clauses) =
relevant (map (weight_of_axiom thy) axioms) ([],[])
val (ax,r) = relevant_clauses_ax_3 const_tab rel_clauses nrel_clauses pass ([],[]) []
in
if !add_unit then (filter safe_unit_clause r) @ ax
else ax
end;
fun relevance_filter3 thy axioms goals =
map #1 (relevance_filter3_aux thy axioms goals);
(******************************************************************)
(* Generic functions for relevance filtering *)
(******************************************************************)
exception RELEVANCE_FILTER of string;
fun relevance_filter thy axioms goals =
case (!strategy) of 1 => relevance_filter1 axioms goals
| 2 => relevance_filter2 axioms goals
| 3 => relevance_filter3 thy axioms goals
| _ => raise RELEVANCE_FILTER("strategy doesn't exist");
end;