# HG changeset patch # User blanchet # Date 1360242332 -3600 # Node ID 98fb341d32e332af6fa28c91871733f4d9045f51 # Parent 550f265864e30626af83b11a6a353c7525006cce 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 diff -r 550f265864e3 -r 98fb341d32e3 src/Doc/Sledgehammer/document/root.tex --- 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} diff -r 550f265864e3 -r 98fb341d32e3 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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)] diff -r 550f265864e3 -r 98fb341d32e3 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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