# HG changeset patch # User paulson # Date 1161335055 -7200 # Node ID 0a898140fea2eed06cf2f11c61d843d3c666a84c # Parent e55b507d0c619af2a83d2fb2bef3428d77fff2bb Added more debugging info diff -r e55b507d0c61 -r 0a898140fea2 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Fri Oct 20 11:03:33 2006 +0200 +++ b/src/HOL/Tools/res_atp.ML Fri Oct 20 11:04:15 2006 +0200 @@ -55,6 +55,8 @@ structure ResAtp = struct +fun timestamp s = Output.debug ("At " ^ Time.toString (Time.now()) ^ ": " ^ s); + (********************************************************************) (* some settings for both background automatic ATP calling procedure*) (* and also explicit ATP invocation methods *) @@ -507,21 +509,14 @@ | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w) | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w))); -fun hashw_pred (P,w) = - let val (p,args) = strip_comb P - in - List.foldl hashw_term w (p::args) - end; - -fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_pred(P,0w0)) - | hash_literal P = hashw_pred(P,0w0); +fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0)) + | hash_literal P = hashw_term(P,0w0); fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits) | get_literals lit lits = (lit::lits); - fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t []))); (*Versions ONLY for "faking" a theorem name. Here we take variable names into account @@ -556,6 +551,7 @@ fun make_unique xs = let val ht = mk_clause_table 7000 in + Output.debug("make_unique gets " ^ Int.toString (length xs) ^ " clauses"); app (ignore o Polyhash.peekInsert ht) xs; Polyhash.listItems ht end; @@ -621,9 +617,12 @@ (*Remove lemmas that are banned from the backlist. Also remove duplicates. *) fun blacklist_filter thms = if !run_blacklist_filter then - let val banned = make_banned_test (map #1 thms) + let val _ = Output.debug("blacklist filter gets " ^ Int.toString (length thms) ^ " theorems") + val banned = make_banned_test (map #1 thms) fun ok (a,_) = not (banned a) - in filter ok thms end + val okthms = filter ok thms + val _ = Output.debug("...and returns " ^ Int.toString (length okthms)) + in okthms end else thms; @@ -785,11 +784,13 @@ val included_cls = included_thms |> blacklist_filter |> ResAxioms.cnf_rules_pairs |> make_unique |> restrict_to_logic logic + val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls)) val white_cls = ResAxioms.cnf_rules_pairs white_thms (*clauses relevant to goal gl*) val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl]) goals - val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls)) + val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls))) + axcls_list val keep_types = if is_fol_logic logic then !ResClause.keep_types else is_typed_hol () val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy