# HG changeset patch
# User blanchet
# Date 1359651245 -3600
# Node ID cca90dd51e82877d355998ed82e5fe632ef0894a
# Parent  2d07f0fdcb293d99aeb156365894c445f02bf95f
also have SMT solvers alternate fact filter

diff -r 2d07f0fdcb29 -r cca90dd51e82 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -926,6 +926,10 @@
      message_tail = message_tail}
   end
 
+fun rotate_one (x :: xs) = xs @ [x]
+
+fun app_hd f (x :: xs) = f x :: xs
+
 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
    these are sorted out properly in the SMT module, we have to interpret these
    ourselves. *)
@@ -958,11 +962,12 @@
 val smt_max_slices =
   Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
 val smt_slice_fact_frac =
-  Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.5)
+  Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac}
+                           (K 0.667)
 val smt_slice_time_frac =
-  Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.5)
+  Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
 val smt_slice_min_secs =
-  Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 5)
+  Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
 
 fun smt_filter_loop name
                     ({debug, verbose, overlord, max_mono_iters,
@@ -983,7 +988,7 @@
     val ctxt = Proof.context_of state |> repair_context
     val state = state |> Proof.map_context (K ctxt)
     val max_slices = if slice then Config.get ctxt smt_max_slices else 1
-    fun do_slice timeout slice outcome0 time_so_far weighted_facts =
+    fun do_slice timeout slice outcome0 time_so_far weighted_factss =
       let
         val timer = Timer.startRealTimer ()
         val state =
@@ -1002,6 +1007,7 @@
             end
           else
             timeout
+        val weighted_facts = hd weighted_factss
         val num_facts = length weighted_facts
         val _ =
           if debug then
@@ -1061,8 +1067,9 @@
               else
                 ()
           in
-            weighted_facts
-            |> take new_num_facts
+            weighted_factss
+            |> rotate_one
+            |> app_hd (take new_num_facts)
             |> do_slice timeout (slice + 1) outcome0 time_so_far
           end
         else
@@ -1074,16 +1081,17 @@
 
 fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...})
         minimize_command
-        ({state, goal, subgoal, subgoal_count, factss = (_, facts) :: _, (* FIXME *)
-         ...} : prover_problem) =
+        ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
     val ctxt = Proof.context_of state
-    val num_facts = length facts
-    val facts =
-      facts ~~ (0 upto num_facts - 1)
-      |> map (weight_smt_fact ctxt num_facts)
+    fun weight_facts facts =
+      let val num_facts = length facts in
+        facts ~~ (0 upto num_facts - 1)
+        |> map (weight_smt_fact ctxt num_facts)
+      end
+    val weighted_factss = factss |> map (snd #> weight_facts)
     val {outcome, used_facts = used_pairs, used_from, run_time} =
-      smt_filter_loop name params state goal subgoal facts
+      smt_filter_loop name params state goal subgoal weighted_factss
     val used_facts = used_pairs |> map fst
     val outcome = outcome |> Option.map failure_from_smt_failure
     val (preplay, message, message_tail) =