# HG changeset patch
# User mengj
# Date 1138336632 -3600
# Node ID fb427f4a01f256a112d0d338be5ac886a1675678
# Parent  9b4ae9fa67a43c3ed508feeaf93a8cacf4b0189e
Changed codes that call relevance filter.

diff -r 9b4ae9fa67a4 -r fb427f4a01f2 src/HOL/Tools/ATP/res_clasimpset.ML
--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jan 27 05:34:20 2006 +0100
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jan 27 05:37:12 2006 +0100
@@ -3,75 +3,6 @@
     Copyright   2004  University of Cambridge
 *)
 
-structure ReduceAxiomsN =
-(* Author: Jia Meng, Cambridge University Computer Laboratory
-   Remove irrelevant axioms used for a proof of a goal, with with iteration control
-   Initial version. Needs elaboration. *)
-
-struct
-
-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 [];
-fun thm_consts_rm ncs thm = term_consts_rm ncs (prop_of thm);
-fun consts_of_thm (n,thm) = thm_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] thm;
-fun consts_of_term term = term_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term;
-
-fun make_pairs [] _ = []
-  | make_pairs (x::xs) y = (x,y)::(make_pairs xs y);
-
-fun const_thm_list_aux [] cthms = cthms
-  | const_thm_list_aux (thm::thms) cthms =
-    let val consts = consts_of_thm thm
-	val cthms' = make_pairs consts thm 
-    in const_thm_list_aux thms (cthms' @ cthms) end;
-
-fun const_thm_list thms = const_thm_list_aux thms [];
-
-fun make_thm_table thms = Symtab.make_multi (const_thm_list thms);
-
-fun consts_in_goal goal = consts_of_term goal;
-
-fun axioms_having_consts_aux [] tab thms = thms
-  | axioms_having_consts_aux (c::cs) tab thms =
-    let val thms2 = Option.getOpt (Symtab.lookup tab c, [])
-    in axioms_having_consts_aux cs tab (thms2 union thms) end;
-
-fun axioms_having_consts cs tab = axioms_having_consts_aux cs tab [];
-
-fun relevant_axioms goal thmTab n =  
-    let fun relevant_axioms_aux1 cs k =
-	    let val thms1 = axioms_having_consts cs thmTab
-		val cs1 = foldl (op union_string) [] (map consts_of_thm thms1)
-	    in
-		if (cs1 subset cs) orelse n <= k then (k,thms1) 
-		else relevant_axioms_aux1 (cs1 union cs) (k+1)
-	    end
-    in  relevant_axioms_aux1 (consts_in_goal goal) 1  end;
-
-fun relevant_filter n goal thms = 
-    if n<=0 then thms 
-    else #2 (relevant_axioms goal (make_thm_table thms) n);
-
-(* find the thms from thy that contain relevant constants, n is the iteration number *)
-fun find_axioms_n thy goal n =
-    let val clasetR = ResAxioms.claset_rules_of_thy thy
-	val simpsetR = ResAxioms.simpset_rules_of_thy thy	  
-	val table = make_thm_table (clasetR @ simpsetR)	
-    in relevant_axioms goal table n end;
-
-fun find_axioms_n_c thy goal n =
-    let val current_thms = PureThy.thms_of thy
-	val table = make_thm_table current_thms
-    in relevant_axioms goal table n end;
-
-end;
-
-
 signature RES_CLASIMP = 
   sig
   val blacklist : string list ref (*Theorems forbidden in the output*)
@@ -319,28 +250,28 @@
   To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
 fun get_clasimp_lemmas ctxt goals = 
   let val claset_thms =
-	    map put_name_pair  (*FIXME: relevance filter should use ALL goals*)
-	      (ReduceAxiomsN.relevant_filter (!relevant) (hd goals)
-		(ResAxioms.claset_rules_of_ctxt ctxt))
+	  map put_name_pair (ResAxioms.claset_rules_of_ctxt ctxt)
       val simpset_thms = 
 	    if !use_simpset then 
-		  map put_name_pair 
-		    (ReduceAxiomsN.relevant_filter (!relevant) (hd goals)
-		      (ResAxioms.simpset_rules_of_ctxt ctxt))
+		map put_name_pair (ResAxioms.simpset_rules_of_ctxt ctxt)
 	    else []
       val banned = make_banned_test (map #1 (claset_thms@simpset_thms))
       fun ok (a,_) = not (banned a)
       val claset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok claset_thms)
       val simpset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok simpset_thms)
-      val cls_thms_list = make_unique (mk_clause_table 2200) 
+ 
+
+     val cls_thms_list = make_unique (mk_clause_table 2200) 
                                       (List.concat (simpset_cls_thms@claset_cls_thms))
+
+     val relevant_cls_thms_list = ReduceAxiomsN.relevance_filter cls_thms_list goals
       (* Identify the set of clauses to be written out *)
-      val clauses = map #1(cls_thms_list);
+      val clauses = map #1(relevant_cls_thms_list);
       val cls_nums = map ResClause.num_of_clauses clauses;
       (*Note: in every case, cls_num = 1.  I think that only conjecture clauses
 	can have any other value.*)
       val whole_list = List.concat 
-	    (map clause_numbering (ListPair.zip (cls_thms_list, cls_nums)));
+	    (map clause_numbering (ListPair.zip (relevant_cls_thms_list, cls_nums)));
       
   in  (* create array of put clausename, number pairs into it *)
       (Array.fromList whole_list, clauses)