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

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Feb 07 11:57:42 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Feb 07 14:05:32 2013 +0100
     2.3 @@ -1123,13 +1123,11 @@
     2.4            end
     2.5          else
     2.6            ()
     2.7 -      val fact_filter =
     2.8 +      val effective_fact_filter =
     2.9          case fact_filter of
    2.10            SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
    2.11          | NONE =>
    2.12 -          if is_smt_prover ctxt prover then
    2.13 -            mepoN
    2.14 -          else if is_mash_enabled () then
    2.15 +          if is_mash_enabled () then
    2.16              (maybe_learn ();
    2.17               if mash_can_suggest_facts ctxt then meshN else mepoN)
    2.18            else
    2.19 @@ -1152,16 +1150,20 @@
    2.20          |>> weight_mash_facts
    2.21        val mess =
    2.22          (* the order is important for the "case" expression below *)
    2.23 -        [] |> (if fact_filter <> mepoN then cons (mash_weight, (mash ()))
    2.24 -               else I)
    2.25 -           |> (if fact_filter <> mashN then cons (mepo_weight, (mepo (), []))
    2.26 -               else I)
    2.27 +        [] |> (if effective_fact_filter <> mepoN then
    2.28 +                 cons (mash_weight, (mash ()))
    2.29 +               else
    2.30 +                 I)
    2.31 +           |> (if effective_fact_filter <> mashN then
    2.32 +                 cons (mepo_weight, (mepo (), []))
    2.33 +               else
    2.34 +                 I)
    2.35        val mesh =
    2.36          mesh_facts (Thm.eq_thm_prop o pairself snd) max_facts mess
    2.37          |> add_and_take
    2.38      in
    2.39 -      case mess of
    2.40 -        [(_, (mepo, _)), (_, (mash, _))] =>
    2.41 +      case (fact_filter, mess) of
    2.42 +        (NONE, [(_, (mepo, _)), (_, (mash, _))]) =>
    2.43          [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take),
    2.44           (mashN, mash |> map fst |> add_and_take)]
    2.45        | _ => [("", mesh)]

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 07 11:57:42 2013 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 07 14:05:32 2013 +0100
     3.3 @@ -634,7 +634,7 @@
     3.4          ({exec, arguments, proof_delims, known_failures, prem_role, best_slices,
     3.5            best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
     3.6          (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
     3.7 -                    uncurried_aliases, max_facts, max_mono_iters,
     3.8 +                    uncurried_aliases, fact_filter, max_facts, max_mono_iters,
     3.9                      max_new_mono_instances, isar_proofs, isar_shrink,
    3.10                      slice, timeout, preplay_timeout, ...})
    3.11          minimize_command
    3.12 @@ -720,7 +720,9 @@
    3.13                                best_uncurried_aliases),
    3.14                        extra))) =
    3.15            let
    3.16 -            val facts = get_facts_for_filter best_fact_filter factss
    3.17 +            val effective_fact_filter =
    3.18 +              fact_filter |> the_default best_fact_filter
    3.19 +            val facts = get_facts_for_filter effective_fact_filter factss
    3.20              val num_facts =
    3.21                length facts |> is_none max_facts ? Integer.min best_max_facts
    3.22              val soundness = if strict then Strict else Non_Strict
    3.23 @@ -988,7 +990,8 @@
    3.24      val ctxt = Proof.context_of state |> repair_context
    3.25      val state = state |> Proof.map_context (K ctxt)
    3.26      val max_slices = if slice then Config.get ctxt smt_max_slices else 1
    3.27 -    fun do_slice timeout slice outcome0 time_so_far weighted_factss =
    3.28 +    fun do_slice timeout slice outcome0 time_so_far
    3.29 +                 (weighted_factss as (fact_filter, weighted_facts) :: _) =
    3.30        let
    3.31          val timer = Timer.startRealTimer ()
    3.32          val state =
    3.33 @@ -1007,7 +1010,6 @@
    3.34              end
    3.35            else
    3.36              timeout
    3.37 -        val weighted_facts = hd weighted_factss
    3.38          val num_facts = length weighted_facts
    3.39          val _ =
    3.40            if debug then
    3.41 @@ -1056,21 +1058,27 @@
    3.42              val new_num_facts =
    3.43                Real.ceil (Config.get ctxt smt_slice_fact_frac
    3.44                           * Real.fromInt num_facts)
    3.45 +            val weighted_factss as (new_fact_filter, _) :: _ =
    3.46 +              weighted_factss
    3.47 +              |> rotate_one
    3.48 +              |> app_hd (apsnd (take new_num_facts))
    3.49 +            val show_filter = fact_filter <> new_fact_filter
    3.50 +            fun num_of_facts fact_filter num_facts =
    3.51 +              string_of_int num_facts ^
    3.52 +              (if show_filter then " " ^ quote fact_filter else "") ^
    3.53 +              " fact" ^ plural_s num_facts
    3.54              val _ =
    3.55                if verbose andalso is_some outcome then
    3.56 -                quote name ^ " invoked with " ^ string_of_int num_facts ^
    3.57 -                " fact" ^ plural_s num_facts ^ ": " ^
    3.58 +                quote name ^ " invoked with " ^
    3.59 +                num_of_facts fact_filter num_facts ^ ": " ^
    3.60                  string_for_failure (failure_from_smt_failure (the outcome)) ^
    3.61 -                " Retrying with " ^ string_of_int new_num_facts ^ " fact" ^
    3.62 -                plural_s new_num_facts ^ "..."
    3.63 +                " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
    3.64 +                "..."
    3.65                  |> Output.urgent_message
    3.66                else
    3.67                  ()
    3.68            in
    3.69 -            weighted_factss
    3.70 -            |> rotate_one
    3.71 -            |> app_hd (take new_num_facts)
    3.72 -            |> do_slice timeout (slice + 1) outcome0 time_so_far
    3.73 +            do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
    3.74            end
    3.75          else
    3.76            {outcome = if is_none outcome then NONE else the outcome0,
    3.77 @@ -1089,7 +1097,7 @@
    3.78          facts ~~ (0 upto num_facts - 1)
    3.79          |> map (weight_smt_fact ctxt num_facts)
    3.80        end
    3.81 -    val weighted_factss = factss |> map (snd #> weight_facts)
    3.82 +    val weighted_factss = factss |> map (apsnd weight_facts)
    3.83      val {outcome, used_facts = used_pairs, used_from, run_time} =
    3.84        smt_filter_loop name params state goal subgoal weighted_factss
    3.85      val used_facts = used_pairs |> map fst