Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
authormengj
Tue Mar 07 04:06:02 2006 +0100 (2006-03-07)
changeset 19201294448903a66
parent 19200 1da6b9a1575d
child 19202 0b9eb4b0ad98
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
The hash table (for removing duplicate) now stores clauses as Term.term with names.
src/HOL/Tools/ATP/res_clasimpset.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Mar 07 04:04:21 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Mar 07 04:06:02 2006 +0100
     1.3 @@ -7,15 +7,18 @@
     1.4    sig
     1.5    val blacklist : string list ref (*Theorems forbidden in the output*)
     1.6    val use_simpset: bool ref
     1.7 -  val get_clasimp_lemmas : 
     1.8 -         Proof.context -> term list -> 
     1.9 -         (ResClause.clause * thm) Array.array * ResClause.clause list 
    1.10 +  val get_clasimp_atp_lemmas : 
    1.11 +      Proof.context ->
    1.12 +      Term.term list ->
    1.13 +      (string * Thm.thm) list ->
    1.14 +      (bool * bool * bool) -> bool -> string Array.array * (Term.term * (string * int)) list
    1.15    end;
    1.16 -
    1.17 +  
    1.18  structure ResClasimp : RES_CLASIMP =
    1.19  struct
    1.20  val use_simpset = ref false;   (*Performance is much better without simprules*)
    1.21  
    1.22 +
    1.23  (*In general, these produce clauses that are prolific (match too many equality or
    1.24    membership literals) and relate to seldom-used facts. Some duplicate other rules.
    1.25    FIXME: this blacklist needs to be maintained using theory data and added to using
    1.26 @@ -215,37 +218,95 @@
    1.27        banned
    1.28    end;
    1.29  
    1.30 +
    1.31 +(*** a hash function from Term.term to int, and also a hash table ***)
    1.32 +val xor_words = List.foldl Word.xorb 0w0;
    1.33 +
    1.34 +fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
    1.35 +  | hashw_term ((Free(_,_)), w) = w
    1.36 +  | hashw_term ((Var(_,_)), w) = w
    1.37 +  | hashw_term ((Bound _), w) = w
    1.38 +  | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
    1.39 +  | hashw_term ((P$Q), w) =
    1.40 +    hashw_term (Q, (hashw_term (P, w)));
    1.41 +
    1.42 +fun hashw_pred (P,w) = 
    1.43 +    let val (p,args) = strip_comb P
    1.44 +    in
    1.45 +	List.foldl hashw_term w (p::args)
    1.46 +    end;
    1.47 +
    1.48 +fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_pred(P,0w0))
    1.49 +  | hash_literal P = hashw_pred(P,0w0);
    1.50 +
    1.51 +
    1.52 +fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits
    1.53 +  | get_literals (Const("op |",_)$P$Q) lits =
    1.54 +    get_literals Q (get_literals P lits)
    1.55 +  | get_literals lit lits = (lit::lits);
    1.56 +
    1.57 +
    1.58 +fun hash_term term = Word.toIntX (xor_words (map hash_literal (get_literals term [])));
    1.59 +
    1.60 +
    1.61  (*Create a hash table for clauses, of the given size*)
    1.62  fun mk_clause_table n =
    1.63 -      Polyhash.mkTable (ResClause.hash_clause, ResClause.clause_eq)
    1.64 +      Polyhash.mkTable (hash_term, Term.aconv)
    1.65                         (n, HASH_CLAUSE);
    1.66  
    1.67  (*Use a hash table to eliminate duplicates from xs*)
    1.68  fun make_unique ht xs = 
    1.69        (app (ignore o Polyhash.peekInsert ht) xs;  Polyhash.listItems ht);
    1.70  
    1.71 -(*Write out the claset and simpset rules of the supplied theory.*)
    1.72 -fun get_clasimp_lemmas ctxt goals = 
    1.73 -  let val claset_thms =
    1.74 -	  map put_name_pair (ResAxioms.claset_rules_of_ctxt ctxt)
    1.75 +fun mem_tm tm [] = false
    1.76 +  | mem_tm tm ((tm',name)::tms_names) = Term.aconv (tm,tm') orelse mem_tm tm tms_names;
    1.77 +
    1.78 +fun insert_tms [] tms_names = tms_names
    1.79 +  | insert_tms ((tm,name)::tms_names) tms_names' =
    1.80 +    if mem_tm tm tms_names' then insert_tms tms_names tms_names' else insert_tms tms_names ((tm,name)::tms_names');
    1.81 +
    1.82 +fun warning_thms [] = ()
    1.83 +  | warning_thms ((name,thm)::nthms) = 
    1.84 +    let val nthm = name ^ ": " ^ (string_of_thm thm)
    1.85 +    in
    1.86 +	(warning nthm; warning_thms nthms)
    1.87 +    end;
    1.88 +(*Write out the claset, simpset and atpset rules of the supplied theory.*)
    1.89 +(* also write supplied user rules, they are not relevance filtered *)
    1.90 +fun get_clasimp_atp_lemmas ctxt goals user_thms (use_claset, use_simpset', use_atpset) run_filter =
    1.91 +    let val claset_thms =
    1.92 +	    if use_claset then
    1.93 +		map put_name_pair (ResAxioms.claset_rules_of_ctxt ctxt)
    1.94 +	    else []
    1.95        val simpset_thms = 
    1.96 -	    if !use_simpset then 
    1.97 +	    if (!use_simpset andalso use_simpset') then (* temporary, may merge two use_simpset later *)  
    1.98  		map put_name_pair (ResAxioms.simpset_rules_of_ctxt ctxt)
    1.99  	    else []
   1.100 -      val banned = make_banned_test (map #1 (claset_thms@simpset_thms))
   1.101 -      fun ok (a,_) = not (banned a)
   1.102 -      val claset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok claset_thms)
   1.103 -      val simpset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok simpset_thms)
   1.104 -      val cls_thms_list = make_unique (mk_clause_table 2200) 
   1.105 -                                      (List.concat (simpset_cls_thms@claset_cls_thms))
   1.106 -      val relevant_cls_thms_list =
   1.107 -          ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals
   1.108 -  in  (* create array of put clausename, number pairs into it *)
   1.109 -      (Array.fromList relevant_cls_thms_list, map #1 (relevant_cls_thms_list))
   1.110 -  end;
   1.111 -
   1.112 -
   1.113 +      val atpset_thms =
   1.114 +	  if use_atpset then
   1.115 +	      map put_name_pair (ResAxioms.atpset_rules_of_ctxt ctxt)
   1.116 +	  else []
   1.117 +      val _ = warning_thms atpset_thms
   1.118 +      val user_rules = map put_name_pair user_thms
   1.119 +      val banned = make_banned_test (map #1 (user_rules@atpset_thms@claset_thms@simpset_thms))
   1.120 +      fun ok (a,_) = not (banned a) 	   
   1.121 +      val claset_cls_tms = if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok claset_thms)
   1.122 +			   else ResAxioms.clausify_rules_pairs_abs claset_thms
   1.123 +      val simpset_cls_tms = if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok simpset_thms)
   1.124 +			    else ResAxioms.clausify_rules_pairs_abs simpset_thms
   1.125 +      val atpset_cls_tms = if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok atpset_thms)
   1.126 +			   else ResAxioms.clausify_rules_pairs_abs atpset_thms
   1.127 +      val user_cls_tms = ResAxioms.clausify_rules_pairs_abs user_rules (* no filter here, because user supplied rules *)
   1.128 +      val cls_tms_list = make_unique (mk_clause_table 2200) 
   1.129 +                                      (List.concat (user_cls_tms@atpset_cls_tms@simpset_cls_tms@claset_cls_tms))
   1.130 +      val relevant_cls_tms_list =
   1.131 +	  if run_filter then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_tms_list goals
   1.132 +	  else cls_tms_list
   1.133 +      val all_relevant_cls_tms_list = insert_tms (List.concat user_cls_tms) relevant_cls_tms_list (*ensure all user supplied rules are output*)	  
   1.134 +    in
   1.135 +	(Array.fromList (map fst (map snd all_relevant_cls_tms_list)), all_relevant_cls_tms_list)
   1.136  end;
   1.137  
   1.138  
   1.139  	
   1.140 +end;
   1.141 \ No newline at end of file