add cutoff beyond which facts are handled using definitional CNF

--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Thu Sep 09 12:28:00 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Thu Sep 09 14:47:06 2010 +0200
@@ -7,6 +7,7 @@
 
 signature CLAUSIFIER =
 sig
+  val min_clauses_for_definitional_cnf : int
   val extensionalize_theorem : thm -> thm
   val introduce_combinators_in_cterm : cterm -> thm
   val introduce_combinators_in_theorem : thm -> thm
@@ -17,6 +18,11 @@
 structure Clausifier : CLAUSIFIER =
 struct
 
+(* Cutoff beyond which definitional CNF is used. Definitional CNF has a certain
+   overhead, but it prevents the exponential explosion of the number of
+   clauses. *)
+val min_clauses_for_definitional_cnf = 30
+
 (**** Transformation of Elimination Rules into First-Order Formulas****)
 
 val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
@@ -241,9 +247,17 @@
   let
     val ctxt0 = Variable.global_thm_context th
     val (nnf_th, ctxt) = to_nnf th ctxt0
-    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
+    fun aux th =
+      Meson.make_cnf (map (skolem_theorem_of_def thy) (assume_skolem_funs th))
+                     th ctxt
+    val (cnf_ths, ctxt) =
+      aux nnf_th
+      |> (fn (cnf_ths, ctxt) =>
+             if null cnf_ths orelse
+                length cnf_ths >= min_clauses_for_definitional_cnf then
+               aux (to_definitional_cnf_with_quantifiers thy nnf_th)
+             else
+               (cnf_ths, ctxt))
   in
     cnf_ths |> map introduce_combinators_in_theorem
             |> Variable.export ctxt ctxt0

--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 09 12:28:00 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 09 14:47:06 2010 +0200
@@ -447,7 +447,7 @@
       end
   in
     aux tha thb
-    handle TERM z =>
+    handle TERM _ =>
            (* We could do it right the first time but this error occurs seldom
               and we don't want to break existing proofs in subtle ways or slow
               them down needlessly. *)
@@ -827,8 +827,7 @@
     if exists_type type_has_top_sort (prop_of st0) then
       (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
     else
-      Meson.MESON (K all_tac) (* TODO: Try (cnf.cnfx_rewrite_tac ctxt) *)
-                  (maps neg_clausify)
+      Meson.MESON (K all_tac) (maps neg_clausify)
                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
                   ctxt i st0
   end