src/HOL/Tools/ATP/res_clasimpset.ML
changeset 18449 e314fb38307d
parent 18420 9470061ab283
child 18509 d2d96f12a1fc
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Dec 21 12:05:47 2005 +0100
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Dec 21 12:06:08 2005 +0100
     1.3 @@ -143,27 +143,30 @@
     1.4      
     1.5  (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute
     1.6  Some primes from http://primes.utm.edu/:
     1.7 -   1823   1831   1847   1861   1867   1871   1873   1877   1879   1889 
     1.8 -   1901   1907   1913   1931   1933   1949   1951   1973   1979   1987 
     1.9 -   1993   1997   1999   2003   2011   2017   2027   2029   2039   2053 
    1.10 -   2063   2069   2081   2083   2087   2089   2099   2111   2113   2129 
    1.11  *)
    1.12  
    1.13 -exception HASH_CLAUSE;
    1.14 +exception HASH_CLAUSE and HASH_STRING;
    1.15 +
    1.16 +(*Catches (for deletion) theorems automatically generated from other theorems*)
    1.17 +fun insert_suffixed_names ht x = 
    1.18 +     (Polyhash.insert ht (x^"_iff1", ()); 
    1.19 +      Polyhash.insert ht (x^"_iff2", ()); 
    1.20 +      Polyhash.insert ht (x^"_dest", ())); 
    1.21 +
    1.22 +fun make_suffix_test xs = 
    1.23 +  let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
    1.24 +                                (6000, HASH_STRING)
    1.25 +      fun suffixed s = isSome (Polyhash.peek ht s)
    1.26 +  in  app (insert_suffixed_names ht) xs; suffixed  end;
    1.27  
    1.28  (*Create a hash table for clauses, of the given size*)
    1.29 -fun mk_clause_table size =
    1.30 -      Hashtable.create{hash = ResClause.hash1_clause, 
    1.31 -		       exn = HASH_CLAUSE,
    1.32 -		       == = ResClause.clause_eq, 
    1.33 -		       size = size};
    1.34 -
    1.35 -(*Insert x only if fresh*)
    1.36 -fun insert_new ht (x,y) = ignore (Hashtable.lookup ht x)
    1.37 -            handle HASH_CLAUSE => Hashtable.insert ht (x,y); 
    1.38 +fun mk_clause_table n =
    1.39 +      Polyhash.mkTable (ResClause.hash_clause, ResClause.clause_eq)
    1.40 +                       (n, HASH_CLAUSE);
    1.41  
    1.42  (*Use a hash table to eliminate duplicates from xs*)
    1.43 -fun make_unique ht xs = (app (insert_new ht) xs;  Hashtable.map Library.I ht);
    1.44 +fun make_unique ht xs = 
    1.45 +      (app (ignore o Polyhash.peekInsert ht) xs;  Polyhash.listItems ht);
    1.46  
    1.47  (*Write out the claset and simpset rules of the supplied theory.
    1.48    FIXME: argument "goal" is a hack to allow relevance filtering.
    1.49 @@ -173,15 +176,17 @@
    1.50  	    map put_name_pair
    1.51  	      (ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.52  		(ResAxioms.claset_rules_of_ctxt ctxt))
    1.53 -      val claset_cls_thms = ResAxioms.clausify_rules_pairs claset_thms
    1.54 -      val simpset_cls_thms = 
    1.55 +      val simpset_thms = 
    1.56  	    if !use_simpset then 
    1.57 -	       ResAxioms.clausify_rules_pairs 
    1.58 -		  (map put_name_pair 
    1.59 +		  map put_name_pair 
    1.60  		    (ReduceAxiomsN.relevant_filter (!relevant) goal
    1.61 -		      (ResAxioms.simpset_rules_of_ctxt ctxt)))
    1.62 +		      (ResAxioms.simpset_rules_of_ctxt ctxt))
    1.63  	    else []
    1.64 -      val cls_thms_list = make_unique (mk_clause_table 2129) 
    1.65 +      val suffixed = make_suffix_test (map #1 (claset_thms@simpset_thms))
    1.66 +      fun ok (a,_) = not (suffixed a)
    1.67 +      val claset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok claset_thms)
    1.68 +      val simpset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok simpset_thms)
    1.69 +      val cls_thms_list = make_unique (mk_clause_table 2200) 
    1.70                                        (List.concat (simpset_cls_thms@claset_cls_thms))
    1.71        (* Identify the set of clauses to be written out *)
    1.72        val clauses = map #1(cls_thms_list);