src/HOL/Tools/res_atp.ML
changeset 21070 0a898140fea2
parent 20995 51c41f167adc
child 21132 88d1daae0319
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Oct 20 11:03:33 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Oct 20 11:04:15 2006 +0200
     1.3 @@ -55,6 +55,8 @@
     1.4  structure ResAtp =
     1.5  struct
     1.6  
     1.7 +fun timestamp s = Output.debug ("At " ^ Time.toString (Time.now()) ^ ": " ^ s);
     1.8 +
     1.9  (********************************************************************)
    1.10  (* some settings for both background automatic ATP calling procedure*)
    1.11  (* and also explicit ATP invocation methods                         *)
    1.12 @@ -507,21 +509,14 @@
    1.13    | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
    1.14    | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
    1.15  
    1.16 -fun hashw_pred (P,w) = 
    1.17 -    let val (p,args) = strip_comb P
    1.18 -    in
    1.19 -	List.foldl hashw_term w (p::args)
    1.20 -    end;
    1.21 -
    1.22 -fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_pred(P,0w0))
    1.23 -  | hash_literal P = hashw_pred(P,0w0);
    1.24 +fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0))
    1.25 +  | hash_literal P = hashw_term(P,0w0);
    1.26  
    1.27  
    1.28  fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits
    1.29    | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
    1.30    | get_literals lit lits = (lit::lits);
    1.31  
    1.32 -
    1.33  fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
    1.34  
    1.35  (*Versions ONLY for "faking" a theorem name. Here we take variable names into account
    1.36 @@ -556,6 +551,7 @@
    1.37  fun make_unique xs = 
    1.38    let val ht = mk_clause_table 7000
    1.39    in
    1.40 +      Output.debug("make_unique gets " ^ Int.toString (length xs) ^ " clauses");
    1.41        app (ignore o Polyhash.peekInsert ht) xs;  
    1.42        Polyhash.listItems ht
    1.43    end;
    1.44 @@ -621,9 +617,12 @@
    1.45  (*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
    1.46  fun blacklist_filter thms = 
    1.47    if !run_blacklist_filter then 
    1.48 -      let val banned = make_banned_test (map #1 thms)
    1.49 +      let val _ = Output.debug("blacklist filter gets " ^ Int.toString (length thms) ^ " theorems")
    1.50 +          val banned = make_banned_test (map #1 thms)
    1.51  	  fun ok (a,_) = not (banned a)
    1.52 -      in  filter ok thms  end
    1.53 +	  val okthms = filter ok thms
    1.54 +          val _ = Output.debug("...and returns " ^ Int.toString (length okthms))
    1.55 +      in  okthms end
    1.56    else thms;
    1.57  
    1.58  
    1.59 @@ -785,11 +784,13 @@
    1.60        val included_cls = included_thms |> blacklist_filter
    1.61                                         |> ResAxioms.cnf_rules_pairs |> make_unique 
    1.62                                         |> restrict_to_logic logic 
    1.63 +      val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
    1.64        val white_cls = ResAxioms.cnf_rules_pairs white_thms
    1.65        (*clauses relevant to goal gl*)
    1.66        val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl])
    1.67                             goals
    1.68 -      val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
    1.69 +      val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls)))
    1.70 +                  axcls_list
    1.71        val keep_types = if is_fol_logic logic then !ResClause.keep_types 
    1.72                         else is_typed_hol ()
    1.73        val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy