diff -r cf1c19eee826 -r b218cc3d1bb4 src/HOL/Tools/ATP/reduce_axiomsN.ML --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML Wed Mar 22 11:54:54 2006 +0100 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML Wed Mar 22 12:30:29 2006 +0100 @@ -5,197 +5,24 @@ structure ReduceAxiomsN = struct -val pass_mark = ref 0.5; -val strategy = ref 3; -val max_filtered = ref 2000; - -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; +val pass_mark = ref 0.6; +val reduction_factor = ref 1.0; - -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); - +(*Whether all "simple" unit clauses should be included*) +val add_unit = ref false; +val unit_pass_mark = ref 0.0; -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 []; (*Including equality in this list might be expected to stop rules like subset_antisym from being chosen, but for some reason filtering works better with them listed.*) 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; + ["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->", + "op =","==","True","False"]; -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_kind = 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) = @@ -239,20 +66,23 @@ | const_typ_of (TVar _) = CTVar -fun const_w_typ thy (c,typ) = +fun const_with_typ thy (c,typ) = let val tvars = Sign.const_typargs thy (c,typ) - in (c, map const_typ_of tvars) end; + in (c, map const_typ_of tvars) end + handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*) -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; +(*Free variables are counted, as well as constants, to handle locales*) +fun add_term_consts_typs_rm thy (Const(c, typ)) cs = + if (c mem standard_consts) then cs + else const_with_typ thy (c,typ) ins cs + | add_term_consts_typs_rm thy (Free(c, typ)) cs = + const_with_typ thy (c,typ) ins cs + | add_term_consts_typs_rm thy (t $ u) cs = + add_term_consts_typs_rm thy t (add_term_consts_typs_rm thy u cs) + | add_term_consts_typs_rm thy (Abs(_,_,t)) cs = add_term_consts_typs_rm thy t cs + | add_term_consts_typs_rm thy _ 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 consts_typs_of_term thy t = add_term_consts_typs_rm thy t []; fun get_goal_consts_typs thy cs = foldl (op union) [] (map (consts_typs_of_term thy) cs) @@ -276,19 +106,21 @@ structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord); -fun count_axiom_consts thy ((tm,_), tab) = - let fun count_term_consts (Const cT, tab) = - let val (c, cts) = const_w_typ thy cT - val cttab = Option.getOpt (Symtab.lookup tab c, CTtab.empty) - val n = Option.getOpt (CTtab.lookup cttab cts, 0) - in - Symtab.update (c, CTtab.update (cts, n+1) cttab) tab - end +fun count_axiom_consts thy ((t,_), tab) = + let fun count_const (a, T, tab) = + let val (c, cts) = const_with_typ thy (a,T) + val cttab = Option.getOpt (Symtab.lookup tab c, CTtab.empty) + val n = Option.getOpt (CTtab.lookup cttab cts, 0) + in + Symtab.update (c, CTtab.update (cts, n+1) cttab) tab + end + fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab) + | count_term_consts (Free(a,T), tab) = count_const(a,T,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 - in count_term_consts (tm, tab) end; + in count_term_consts (t, tab) end; (******** filter clauses ********) @@ -310,36 +142,39 @@ (*Relevant constants are weighted according to frequency, but irrelevant constants are simply counted. Otherwise, Skolem functions, which are rare, would harm a clause's chances of being picked.*) -fun clause_weight_s_3 ctab gctyps consts_typs = +fun clause_weight ctab gctyps consts_typs = let val rel = filter (fn s => uni_mem s gctyps) consts_typs val rel_weight = consts_typs_weight ctab rel in rel_weight / (rel_weight + real (length consts_typs - length rel)) end; - -fun relevant_clauses_ax_3 ctab rel_axs [] P (addc,tmpc) keep = + +fun relevant_clauses ctab rel_axs [] (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 = + else relevant_clauses ctab addc tmpc ([],[]) (rel_axs @ keep) + | relevant_clauses ctab rel_axs ((clstm,(consts_typs,w))::e_axs) (addc,tmpc) keep = let fun clause_weight_ax (_,(refconsts_typs,wa)) = - wa * clause_weight_s_3 ctab refconsts_typs consts_typs; - val weight' = List.foldl Real.max weight (map clause_weight_ax rel_axs) + wa * clause_weight ctab refconsts_typs consts_typs; + val weight' = List.foldl Real.max w (map clause_weight_ax rel_axs) 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 + if !pass_mark <= weight' + then relevant_clauses ctab rel_axs e_axs (e_ax'::addc, tmpc) keep + else relevant_clauses ctab rel_axs e_axs (addc, e_ax'::tmpc) keep end; fun pair_consts_typs_axiom thy (tm,name) = ((tm,name), (consts_typs_of_term thy tm)); -fun safe_unit_clause ((t,_), _) = - case clause_kind t of +(*Unit clauses other than non-trivial equations can be included subject to + a separate (presumably lower) mark. *) +fun good_unit_clause ((t,_), (_,w)) = + !unit_pass_mark <= w andalso + (case clause_kind t of Unit_neq => true | Unit_geq => true - | Other => false; + | Other => false); fun axiom_ord ((_,(_,w1)), (_,(_,w2))) = Real.compare (w2,w1); @@ -352,46 +187,34 @@ fun showax ((_,cname), (_,w)) = Output.debug ("Axiom " ^ show_cname cname ^ " has weight " ^ Real.toString w) - fun relevance_filter3_aux thy axioms goals = - let val pass = !pass_mark - val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms +fun relevance_filter_aux thy axioms goals = + let val const_tab = List.foldl (count_axiom_consts thy) 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 + let val weight = clause_weight const_tab goals_consts_typs consts_typs val ccc = (clstm, (consts_typs,weight)) in - if pass <= weight + if !pass_mark <= weight then relevant y (ccc::ax, r) else relevant y (ax, ccc::r) end val (rel_clauses,nrel_clauses) = relevant (map (pair_consts_typs_axiom thy) axioms) ([],[]) - val (ax,r) = relevant_clauses_ax_3 const_tab rel_clauses nrel_clauses pass ([],[]) [] - val ax' = Library.take(!max_filtered, Library.sort axiom_ord ax) + val (ax,r) = relevant_clauses const_tab rel_clauses nrel_clauses ([],[]) [] + val max_filtered = floor (!reduction_factor * real (length ax)) + val ax' = Library.take(max_filtered, Library.sort axiom_ord ax) in if !Output.show_debug_msgs then (List.app showconst (Symtab.dest const_tab); List.app showax ax) else (); - if !add_unit then (filter safe_unit_clause r) @ ax' + if !add_unit then (filter good_unit_clause r) @ ax' else ax' end; -fun relevance_filter3 thy axioms goals = - map #1 (relevance_filter3_aux thy axioms goals); +fun relevance_filter thy axioms goals = + map #1 (relevance_filter_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; \ No newline at end of file