# HG changeset patch
# User blanchet
# Date 1306767638 -7200
# Node ID 8f1f80a40498be5e8c3e4d577a321ef79ceb62ed
# Parent  2834548a7a480e7a072328bdc97307067eacc0d7
don't slice if there are too few facts

diff -r 2834548a7a48 -r 8f1f80a40498 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 30 17:00:38 2011 +0200
@@ -33,7 +33,7 @@
      max_relevant: int option,
      max_mono_iters: int,
      max_new_mono_instances: int,
-     explicit_apply: bool,
+     explicit_apply: bool option,
      isar_proof: bool,
      isar_shrink_factor: int,
      slicing: bool,
@@ -155,8 +155,14 @@
   is_metis_prover orf is_smt_prover ctxt orf
   is_atp_installed (Proof_Context.theory_of ctxt)
 
-fun get_slices slicing slices =
-  (0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)
+fun get_slices num_facts slicing slices =
+  (0 upto length slices - 1) ~~ slices
+  |> (if slicing andalso
+         exists (fn (_, (_, (max_facts, _))) => max_facts < num_facts)
+                slices then
+        I
+      else
+        List.last #> single)
 
 val metis_default_max_relevant = 20
 
@@ -166,7 +172,8 @@
       metis_default_max_relevant
     else if is_atp thy name then
       fold (Integer.max o fst o snd o snd o snd)
-           (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0
+           (get_slices 16384 (* large number *) slicing
+                       (#best_slices (get_atp thy name) ctxt)) 0
     else (* is_smt_prover ctxt name *)
       SMT_Solver.default_max_relevant ctxt name
   end
@@ -295,7 +302,7 @@
    max_relevant: int option,
    max_mono_iters: int,
    max_new_mono_instances: int,
-   explicit_apply: bool,
+   explicit_apply: bool option,
    isar_proof: bool,
    isar_shrink_factor: int,
    slicing: bool,
@@ -592,7 +599,8 @@
           let
             (* If slicing is disabled, we expand the last slice to fill the
                entire time available. *)
-            val actual_slices = get_slices slicing (best_slices ctxt)
+            val actual_slices =
+              get_slices (length facts) slicing (best_slices ctxt)
             val num_actual_slices = length actual_slices
             fun monomorphize_facts facts =
               let
@@ -787,12 +795,9 @@
                 val used_ths =
                   facts |> map untranslated_fact |> filter_used_facts used_facts
                         |> map snd
-                val reconstructors =
-                  [Metis, MetisFT]
-                  |> uses_typed_helpers typed_helpers atp_proof ? rev
               in
                 play_one_line_proof debug preplay_timeout used_ths state subgoal
-                                    reconstructors
+                                    [Metis, MetisFT]
               end,
            fn preplay =>
               let