src/HOL/Tools/ATP/res_clasimpset.ML
changeset 18420 9470061ab283
parent 18144 4edcb5fdc3b0
child 18449 e314fb38307d
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Dec 16 11:51:24 2005 +0100
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Dec 16 12:15:54 2005 +0100
     1.3 @@ -141,36 +141,56 @@
     1.4  	multi (clause, theorem) num_of_cls []
     1.5      end;
     1.6      
     1.7 -fun get_simpset_thms ctxt goal clas =
     1.8 -  let val ctab = fold_rev Symtab.update clas Symtab.empty
     1.9 -      fun unused (s,_) = not (Symtab.defined ctab s)
    1.10 -  in  ResAxioms.clausify_rules_pairs 
    1.11 -	(filter unused
    1.12 -	  (map put_name_pair 
    1.13 -	    (ReduceAxiomsN.relevant_filter (!relevant) goal
    1.14 -	      (ResAxioms.simpset_rules_of_ctxt ctxt))))
    1.15 -  end;
    1.16 -		  
    1.17 +(*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute
    1.18 +Some primes from http://primes.utm.edu/:
    1.19 +   1823   1831   1847   1861   1867   1871   1873   1877   1879   1889 
    1.20 +   1901   1907   1913   1931   1933   1949   1951   1973   1979   1987 
    1.21 +   1993   1997   1999   2003   2011   2017   2027   2029   2039   2053 
    1.22 +   2063   2069   2081   2083   2087   2089   2099   2111   2113   2129 
    1.23 +*)
    1.24 +
    1.25 +exception HASH_CLAUSE;
    1.26 +
    1.27 +(*Create a hash table for clauses, of the given size*)
    1.28 +fun mk_clause_table size =
    1.29 +      Hashtable.create{hash = ResClause.hash1_clause, 
    1.30 +		       exn = HASH_CLAUSE,
    1.31 +		       == = ResClause.clause_eq, 
    1.32 +		       size = size};
    1.33 +
    1.34 +(*Insert x only if fresh*)
    1.35 +fun insert_new ht (x,y) = ignore (Hashtable.lookup ht x)
    1.36 +            handle HASH_CLAUSE => Hashtable.insert ht (x,y); 
    1.37 +
    1.38 +(*Use a hash table to eliminate duplicates from xs*)
    1.39 +fun make_unique ht xs = (app (insert_new ht) xs;  Hashtable.map Library.I ht);
    1.40  
    1.41  (*Write out the claset and simpset rules of the supplied theory.
    1.42    FIXME: argument "goal" is a hack to allow relevance filtering.
    1.43    To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
    1.44  fun get_clasimp_lemmas ctxt goal = 
    1.45 -    let val claset_thms =
    1.46 -		map put_name_pair
    1.47 -		  (ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.48 -		    (ResAxioms.claset_rules_of_ctxt ctxt))
    1.49 -	val claset_cls_thms = ResAxioms.clausify_rules_pairs claset_thms
    1.50 -	val simpset_cls_thms = 
    1.51 -	      if !use_simpset then get_simpset_thms ctxt goal claset_thms
    1.52 -	      else []
    1.53 -	val cls_thms_list = List.concat (claset_cls_thms@simpset_cls_thms)
    1.54 -	(* Identify the set of clauses to be written out *)
    1.55 -	val clauses = map #1(cls_thms_list);
    1.56 -	val cls_nums = map ResClause.num_of_clauses clauses;
    1.57 -        val whole_list = List.concat 
    1.58 -              (map clause_numbering (ListPair.zip (cls_thms_list, cls_nums)));
    1.59 - 	
    1.60 +  let val claset_thms =
    1.61 +	    map put_name_pair
    1.62 +	      (ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.63 +		(ResAxioms.claset_rules_of_ctxt ctxt))
    1.64 +      val claset_cls_thms = ResAxioms.clausify_rules_pairs claset_thms
    1.65 +      val simpset_cls_thms = 
    1.66 +	    if !use_simpset then 
    1.67 +	       ResAxioms.clausify_rules_pairs 
    1.68 +		  (map put_name_pair 
    1.69 +		    (ReduceAxiomsN.relevant_filter (!relevant) goal
    1.70 +		      (ResAxioms.simpset_rules_of_ctxt ctxt)))
    1.71 +	    else []
    1.72 +      val cls_thms_list = make_unique (mk_clause_table 2129) 
    1.73 +                                      (List.concat (simpset_cls_thms@claset_cls_thms))
    1.74 +      (* Identify the set of clauses to be written out *)
    1.75 +      val clauses = map #1(cls_thms_list);
    1.76 +      val cls_nums = map ResClause.num_of_clauses clauses;
    1.77 +      (*Note: in every case, cls_num = 1.  I think that only conjecture clauses
    1.78 +	can have any other value.*)
    1.79 +      val whole_list = List.concat 
    1.80 +	    (map clause_numbering (ListPair.zip (cls_thms_list, cls_nums)));
    1.81 +      
    1.82    in  (* create array of put clausename, number pairs into it *)
    1.83        (Array.fromList whole_list, clauses)
    1.84    end;