Changed codes that call relevance filter.
authormengj
Fri Jan 27 05:37:12 2006 +0100 (2006-01-27)
changeset 18792fb427f4a01f2
parent 18791 9b4ae9fa67a4
child 18793 3536d86b5dc1
Changed codes that call relevance filter.
src/HOL/Tools/ATP/res_clasimpset.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jan 27 05:34:20 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jan 27 05:37:12 2006 +0100
     1.3 @@ -3,75 +3,6 @@
     1.4      Copyright   2004  University of Cambridge
     1.5  *)
     1.6  
     1.7 -structure ReduceAxiomsN =
     1.8 -(* Author: Jia Meng, Cambridge University Computer Laboratory
     1.9 -   Remove irrelevant axioms used for a proof of a goal, with with iteration control
    1.10 -   Initial version. Needs elaboration. *)
    1.11 -
    1.12 -struct
    1.13 -
    1.14 -fun add_term_consts_rm ncs (Const(c, _)) cs = if (c mem ncs) then cs else (c ins_string cs)
    1.15 -  | add_term_consts_rm ncs (t $ u) cs =
    1.16 -      add_term_consts_rm ncs t (add_term_consts_rm ncs u cs)
    1.17 -  | add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs
    1.18 -  | add_term_consts_rm ncs _ cs = cs;
    1.19 -
    1.20 -fun term_consts_rm ncs t = add_term_consts_rm ncs t [];
    1.21 -fun thm_consts_rm ncs thm = term_consts_rm ncs (prop_of thm);
    1.22 -fun consts_of_thm (n,thm) = thm_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] thm;
    1.23 -fun consts_of_term term = term_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term;
    1.24 -
    1.25 -fun make_pairs [] _ = []
    1.26 -  | make_pairs (x::xs) y = (x,y)::(make_pairs xs y);
    1.27 -
    1.28 -fun const_thm_list_aux [] cthms = cthms
    1.29 -  | const_thm_list_aux (thm::thms) cthms =
    1.30 -    let val consts = consts_of_thm thm
    1.31 -	val cthms' = make_pairs consts thm 
    1.32 -    in const_thm_list_aux thms (cthms' @ cthms) end;
    1.33 -
    1.34 -fun const_thm_list thms = const_thm_list_aux thms [];
    1.35 -
    1.36 -fun make_thm_table thms = Symtab.make_multi (const_thm_list thms);
    1.37 -
    1.38 -fun consts_in_goal goal = consts_of_term goal;
    1.39 -
    1.40 -fun axioms_having_consts_aux [] tab thms = thms
    1.41 -  | axioms_having_consts_aux (c::cs) tab thms =
    1.42 -    let val thms2 = Option.getOpt (Symtab.lookup tab c, [])
    1.43 -    in axioms_having_consts_aux cs tab (thms2 union thms) end;
    1.44 -
    1.45 -fun axioms_having_consts cs tab = axioms_having_consts_aux cs tab [];
    1.46 -
    1.47 -fun relevant_axioms goal thmTab n =  
    1.48 -    let fun relevant_axioms_aux1 cs k =
    1.49 -	    let val thms1 = axioms_having_consts cs thmTab
    1.50 -		val cs1 = foldl (op union_string) [] (map consts_of_thm thms1)
    1.51 -	    in
    1.52 -		if (cs1 subset cs) orelse n <= k then (k,thms1) 
    1.53 -		else relevant_axioms_aux1 (cs1 union cs) (k+1)
    1.54 -	    end
    1.55 -    in  relevant_axioms_aux1 (consts_in_goal goal) 1  end;
    1.56 -
    1.57 -fun relevant_filter n goal thms = 
    1.58 -    if n<=0 then thms 
    1.59 -    else #2 (relevant_axioms goal (make_thm_table thms) n);
    1.60 -
    1.61 -(* find the thms from thy that contain relevant constants, n is the iteration number *)
    1.62 -fun find_axioms_n thy goal n =
    1.63 -    let val clasetR = ResAxioms.claset_rules_of_thy thy
    1.64 -	val simpsetR = ResAxioms.simpset_rules_of_thy thy	  
    1.65 -	val table = make_thm_table (clasetR @ simpsetR)	
    1.66 -    in relevant_axioms goal table n end;
    1.67 -
    1.68 -fun find_axioms_n_c thy goal n =
    1.69 -    let val current_thms = PureThy.thms_of thy
    1.70 -	val table = make_thm_table current_thms
    1.71 -    in relevant_axioms goal table n end;
    1.72 -
    1.73 -end;
    1.74 -
    1.75 -
    1.76  signature RES_CLASIMP = 
    1.77    sig
    1.78    val blacklist : string list ref (*Theorems forbidden in the output*)
    1.79 @@ -319,28 +250,28 @@
    1.80    To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
    1.81  fun get_clasimp_lemmas ctxt goals = 
    1.82    let val claset_thms =
    1.83 -	    map put_name_pair  (*FIXME: relevance filter should use ALL goals*)
    1.84 -	      (ReduceAxiomsN.relevant_filter (!relevant) (hd goals)
    1.85 -		(ResAxioms.claset_rules_of_ctxt ctxt))
    1.86 +	  map put_name_pair (ResAxioms.claset_rules_of_ctxt ctxt)
    1.87        val simpset_thms = 
    1.88  	    if !use_simpset then 
    1.89 -		  map put_name_pair 
    1.90 -		    (ReduceAxiomsN.relevant_filter (!relevant) (hd goals)
    1.91 -		      (ResAxioms.simpset_rules_of_ctxt ctxt))
    1.92 +		map put_name_pair (ResAxioms.simpset_rules_of_ctxt ctxt)
    1.93  	    else []
    1.94        val banned = make_banned_test (map #1 (claset_thms@simpset_thms))
    1.95        fun ok (a,_) = not (banned a)
    1.96        val claset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok claset_thms)
    1.97        val simpset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok simpset_thms)
    1.98 -      val cls_thms_list = make_unique (mk_clause_table 2200) 
    1.99 + 
   1.100 +
   1.101 +     val cls_thms_list = make_unique (mk_clause_table 2200) 
   1.102                                        (List.concat (simpset_cls_thms@claset_cls_thms))
   1.103 +
   1.104 +     val relevant_cls_thms_list = ReduceAxiomsN.relevance_filter cls_thms_list goals
   1.105        (* Identify the set of clauses to be written out *)
   1.106 -      val clauses = map #1(cls_thms_list);
   1.107 +      val clauses = map #1(relevant_cls_thms_list);
   1.108        val cls_nums = map ResClause.num_of_clauses clauses;
   1.109        (*Note: in every case, cls_num = 1.  I think that only conjecture clauses
   1.110  	can have any other value.*)
   1.111        val whole_list = List.concat 
   1.112 -	    (map clause_numbering (ListPair.zip (cls_thms_list, cls_nums)));
   1.113 +	    (map clause_numbering (ListPair.zip (relevant_cls_thms_list, cls_nums)));
   1.114        
   1.115    in  (* create array of put clausename, number pairs into it *)
   1.116        (Array.fromList whole_list, clauses)