# HG changeset patch # User blanchet # Date 1283514844 -7200 # Node ID 611e41ef07c31e4f552491c99e77f8d3ad53f0d7 # Parent 2e9bdc6fbedf6ad5c88c67dd55baae8d106b7d0f disable "definitional CNF"; it has a bad impact on "Metis_Examples". Perhaps we should use it more selectively, based on how many clauses we would get using the naive method diff -r 2e9bdc6fbedf -r 611e41ef07c3 src/HOL/Tools/Sledgehammer/clausifier.ML --- a/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Sep 03 13:45:12 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Sep 03 13:54:04 2010 +0200 @@ -241,7 +241,7 @@ let val ctxt0 = Variable.global_thm_context th val (nnf_th, ctxt) = to_nnf th ctxt0 - val def_th = to_definitional_cnf_with_quantifiers thy nnf_th + val def_th = (* FIXME: to_definitional_cnf_with_quantifiers thy *) nnf_th val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs def_th) val (cnf_ths, ctxt) = Meson.make_cnf sko_ths def_th ctxt in diff -r 2e9bdc6fbedf -r 611e41ef07c3 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Sep 03 13:45:12 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Sep 03 13:54:04 2010 +0200 @@ -798,6 +798,7 @@ val thy = ProofContext.theory_of ctxt val _ = trace_msg (fn () => "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) +val timer = Timer.startRealTimer () (*###*) in if exists_type type_has_top_sort (prop_of st0) then (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) @@ -806,6 +807,9 @@ (maps neg_clausify) (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i st0 +|> tap (fn _ => priority (" METIS " ^ +cat_lines (map (Display.string_of_thm ctxt) ths) ^ +string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ " ms")) (*###*) end val metis_tac = generic_metis_tac HO