distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation

--- a/src/Doc/Sledgehammer/document/root.tex	Thu Feb 07 11:57:42 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Feb 07 14:05:32 2013 +0100
@@ -1063,10 +1063,11 @@
 variable \texttt{MASH} to \texttt{yes}. Persistent data is stored in the
 directory \texttt{\$ISABELLE\_HOME\_USER/mash}.
 
-\item[\labelitemi] \textbf{\textit{mesh}:} A combination of MePo and MaSh.
+\item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
+rankings from MePo and MaSh.
 
-\item[\labelitemi] \textbf{\textit{smart}:} Use MeSh if MaSh is
-enabled and the target prover is an ATP; otherwise, use MePo.
+\item[\labelitemi] \textbf{\textit{smart}:} A mixture of MePo, MaSh, and MeSh if
+MaSh is enabled; otherwise, MePo.
 \end{enum}
 
 \opdefault{max\_facts}{smart\_int}{smart}

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Feb 07 11:57:42 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Feb 07 14:05:32 2013 +0100
@@ -1123,13 +1123,11 @@
           end
         else
           ()
-      val fact_filter =
+      val effective_fact_filter =
         case fact_filter of
           SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
         | NONE =>
-          if is_smt_prover ctxt prover then
-            mepoN
-          else if is_mash_enabled () then
+          if is_mash_enabled () then
             (maybe_learn ();
              if mash_can_suggest_facts ctxt then meshN else mepoN)
           else
@@ -1152,16 +1150,20 @@
         |>> weight_mash_facts
       val mess =
         (* the order is important for the "case" expression below *)
-        [] |> (if fact_filter <> mepoN then cons (mash_weight, (mash ()))
-               else I)
-           |> (if fact_filter <> mashN then cons (mepo_weight, (mepo (), []))
-               else I)
+        [] |> (if effective_fact_filter <> mepoN then
+                 cons (mash_weight, (mash ()))
+               else
+                 I)
+           |> (if effective_fact_filter <> mashN then
+                 cons (mepo_weight, (mepo (), []))
+               else
+                 I)
       val mesh =
         mesh_facts (Thm.eq_thm_prop o pairself snd) max_facts mess
         |> add_and_take
     in
-      case mess of
-        [(_, (mepo, _)), (_, (mash, _))] =>
+      case (fact_filter, mess) of
+        (NONE, [(_, (mepo, _)), (_, (mash, _))]) =>
         [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take),
          (mashN, mash |> map fst |> add_and_take)]
       | _ => [("", mesh)]

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 07 11:57:42 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 07 14:05:32 2013 +0100
@@ -634,7 +634,7 @@
         ({exec, arguments, proof_delims, known_failures, prem_role, best_slices,
           best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
         (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
-                    uncurried_aliases, max_facts, max_mono_iters,
+                    uncurried_aliases, fact_filter, max_facts, max_mono_iters,
                     max_new_mono_instances, isar_proofs, isar_shrink,
                     slice, timeout, preplay_timeout, ...})
         minimize_command
@@ -720,7 +720,9 @@
                               best_uncurried_aliases),
                       extra))) =
           let
-            val facts = get_facts_for_filter best_fact_filter factss
+            val effective_fact_filter =
+              fact_filter |> the_default best_fact_filter
+            val facts = get_facts_for_filter effective_fact_filter factss
             val num_facts =
               length facts |> is_none max_facts ? Integer.min best_max_facts
             val soundness = if strict then Strict else Non_Strict
@@ -988,7 +990,8 @@
     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_factss =
+    fun do_slice timeout slice outcome0 time_so_far
+                 (weighted_factss as (fact_filter, weighted_facts) :: _) =
       let
         val timer = Timer.startRealTimer ()
         val state =
@@ -1007,7 +1010,6 @@
             end
           else
             timeout
-        val weighted_facts = hd weighted_factss
         val num_facts = length weighted_facts
         val _ =
           if debug then
@@ -1056,21 +1058,27 @@
             val new_num_facts =
               Real.ceil (Config.get ctxt smt_slice_fact_frac
                          * Real.fromInt num_facts)
+            val weighted_factss as (new_fact_filter, _) :: _ =
+              weighted_factss
+              |> rotate_one
+              |> app_hd (apsnd (take new_num_facts))
+            val show_filter = fact_filter <> new_fact_filter
+            fun num_of_facts fact_filter num_facts =
+              string_of_int num_facts ^
+              (if show_filter then " " ^ quote fact_filter else "") ^
+              " fact" ^ plural_s num_facts
             val _ =
               if verbose andalso is_some outcome then
-                quote name ^ " invoked with " ^ string_of_int num_facts ^
-                " fact" ^ plural_s num_facts ^ ": " ^
+                quote name ^ " invoked with " ^
+                num_of_facts fact_filter num_facts ^ ": " ^
                 string_for_failure (failure_from_smt_failure (the outcome)) ^
-                " Retrying with " ^ string_of_int new_num_facts ^ " fact" ^
-                plural_s new_num_facts ^ "..."
+                " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
+                "..."
                 |> Output.urgent_message
               else
                 ()
           in
-            weighted_factss
-            |> rotate_one
-            |> app_hd (take new_num_facts)
-            |> do_slice timeout (slice + 1) outcome0 time_so_far
+            do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
           end
         else
           {outcome = if is_none outcome then NONE else the outcome0,
@@ -1089,7 +1097,7 @@
         facts ~~ (0 upto num_facts - 1)
         |> map (weight_smt_fact ctxt num_facts)
       end
-    val weighted_factss = factss |> map (snd #> weight_facts)
+    val weighted_factss = factss |> map (apsnd weight_facts)
     val {outcome, used_facts = used_pairs, used_from, run_time} =
       smt_filter_loop name params state goal subgoal weighted_factss
     val used_facts = used_pairs |> map fst