--- a/NEWS Mon Feb 03 19:32:02 2014 +0100
+++ b/NEWS Mon Feb 03 19:32:02 2014 +0100
@@ -116,7 +116,7 @@
* Sledgehammer:
- New option:
- smt
+ smt_proofs
- Renamed options:
isar_compress ~> compress_isar
isar_try0 ~> try0_isar
--- a/src/Doc/Sledgehammer/document/root.tex Mon Feb 03 19:32:02 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Feb 03 19:32:02 2014 +0100
@@ -117,7 +117,7 @@
The result of a successful proof search is some source text that usually (but
not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
-proof relies on the general-purpose \textit{metis} proof method, which
+proof typically relies on the general-purpose \textit{metis} proof method, which
integrates the Metis ATP in Isabelle/HOL with explicit inferences going through
the kernel. Thus its results are correct by construction.
@@ -296,7 +296,7 @@
Waldmeister is run only for unit equational problems, where the goal's
conclusion is a (universally quantified) equation.
-For each successful prover, Sledgehammer gives a one-liner \textit{metis} or
+For each successful prover, Sledgehammer gives a one-line \textit{metis} or
\textit{smt} method call. Rough timings are shown in parentheses, indicating how
fast the call is. You can click the proof to insert it into the theory text.
@@ -308,7 +308,7 @@
\postw
When Isar proof construction is successful, it can yield proofs that are more
-readable and also faster than the \textit{metis} or \textit{smt} one-liners.
+readable and also faster than the \textit{metis} or \textit{smt} one-line proofs.
This feature is experimental and is only available for ATPs.
\section{Hints}
@@ -359,7 +359,7 @@
if that helps.
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
-that Isar proofs should be generated, in addition to one-liner \textit{metis} or
+that Isar proofs should be generated, in addition to one-line \textit{metis} or
\textit{smt} proofs. The length of the Isar proofs can be controlled by setting
\textit{compress\_isar} (\S\ref{output-format}).
@@ -463,9 +463,8 @@
\begin{enum}
\item[\labelitemi] Try the \textit{isar\_proofs} option (\S\ref{output-format}) to
-obtain a step-by-step Isar proof where each step is justified by \textit{metis}.
-Since the steps are fairly small, \textit{metis} is more likely to be able to
-replay them.
+obtain a step-by-step Isar proof. Since the steps are fairly small, \textit{metis}
+and the other Isabelle proof methods are more likely to be able to replay them.
\item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}.
It is usually stronger, but you need to either have Z3 available to replay the
@@ -525,8 +524,8 @@
versions of Metis. It is somewhat slower than \textit{metis}, but the proof
search is fully typed, and it also includes more powerful rules such as the
axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in
-higher-order places (e.g., in set comprehensions). The method kicks in
-automatically as a fallback when \textit{metis} fails, and it is sometimes
+higher-order places (e.g., in set comprehensions). The method is automatically
+tried as a fallback when \textit{metis} fails, and it is sometimes
generated by Sledgehammer instead of \textit{metis} if the proof obviously
requires type information or if \textit{metis} failed when Sledgehammer
preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with
@@ -1069,9 +1068,9 @@
\opdefault{max\_facts}{smart\_int}{smart}
Specifies the maximum number of facts that may be returned by the relevance
-filter. If the option is set to \textit{smart}, it effectively takes a value
-that was empirically found to be appropriate for the prover. Typical values
-range between 50 and 1000.
+filter. If the option is set to \textit{smart} (the default), it effectively
+takes a value that was empirically found to be appropriate for the prover.
+Typical values range between 50 and 1000.
For the MaSh-related commands \textit{learn\_isar}, \textit{learn\_prover},
\textit{relearn\_isar}, and \textit{relearn\_prover}, this option specifies the
@@ -1095,9 +1094,9 @@
Specifies the maximum number of monomorphic instances to generate beyond
\textit{max\_facts}. The higher this limit is, the more monomorphic instances
are potentially generated. Whether monomorphization takes place depends on the
-type encoding used. If the option is set to \textit{smart}, it takes a value
-that was empirically found to be appropriate for the prover. For most provers,
-this value is 100.
+type encoding used. If the option is set to \textit{smart} (the default), it
+takes a value that was empirically found to be appropriate for the prover. For
+most provers, this value is 100.
\nopagebreak
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
@@ -1106,9 +1105,9 @@
Specifies the maximum number of iterations for the monomorphization fixpoint
construction. The higher this limit is, the more monomorphic instances are
potentially generated. Whether monomorphization takes place depends on the
-type encoding used. If the option is set to \textit{smart}, it takes a value
-that was empirically found to be appropriate for the prover. For most provers,
-this value is 3.
+type encoding used. If the option is set to \textit{smart} (the default), it
+takes a value that was empirically found to be appropriate for the prover.
+For most provers, this value is 3.
\nopagebreak
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
@@ -1298,12 +1297,11 @@
\textit{overlord} (\S\ref{mode-of-operation}).}
\opsmart{isar\_proofs}{no\_isar\_proofs}
-Specifies whether Isar proofs should be output in addition to one-liner
-\textit{metis} proofs. The construction of Isar proof is still experimental and
-may sometimes fail; however, when they succeed they are usually faster and more
-intelligible than \textit{metis} proofs. If the option is set to \textit{smart}
-(the default), Isar proofs are only generated when no working one-liner
-\textit{metis} proof is available.
+Specifies whether Isar proofs should be output in addition to one-line proofs.
+The construction of Isar proof is still experimental and may sometimes fail;
+however, when they succeed they are usually faster and more intelligible than
+one-line proofs. If the option is set to \textit{smart} (the default), Isar
+proofs are only generated when no working one-line proof is available.
\opdefault{compress\_isar}{int}{\upshape 10}
Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
@@ -1318,10 +1316,11 @@
\textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs.
The collection of methods is roughly the same as for the \textbf{try0} command.
-\opsmart{smt}{no\_smt}
+\opsmart{smt\_proofs}{no\_smt\_proofs}
Specifies whether the \textit{smt} proof method should be tried as an
-alternative to \textit{metis}. If the option is set to \textit{smart}, the
-\textit{smt} method is used for one-line proofs but not in Isar proofs.
+alternative to \textit{metis}. If the option is set to \textit{smart} (the
+default), the \textit{smt} method is used for one-line proofs but not in Isar
+proofs.
\end{enum}
\subsection{Authentication}
@@ -1357,10 +1356,10 @@
searching for a proof. This excludes problem preparation and is a soft limit.
\opdefault{preplay\_timeout}{float}{\upshape 2}
-Specifies the maximum number of seconds that \textit{metis} or \textit{smt}
-should spend trying to ``preplay'' the found proof. If this option is set to 0,
-no preplaying takes place, and no timing information is displayed next to the
-suggested \textit{metis} calls.
+Specifies the maximum number of seconds that \textit{metis} or other proof
+methods should spend trying to ``preplay'' the found proof. If this option
+is set to 0, no preplaying takes place, and no timing information is displayed
+next to the suggested proof method calls.
\nopagebreak
{\small See also \textit{minimize} (\S\ref{mode-of-operation}).}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Feb 03 19:32:02 2014 +0100
@@ -96,7 +96,7 @@
("isar_proofs", "smart"),
("compress_isar", "10"),
("try0_isar", "true"),
- ("smt", "smart"),
+ ("smt_proofs", "smart"),
("slice", "true"),
("minimize", "smart"),
("preplay_timeout", "2")]
@@ -119,7 +119,7 @@
("dont_slice", "slice"),
("dont_minimize", "minimize"),
("dont_try0_isar", "try0_isar"),
- ("no_smt", "smt")]
+ ("no_smt_proofs", "smt_proofs")]
val params_not_for_minimize =
["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"];
@@ -288,7 +288,7 @@
val isar_proofs = lookup_option lookup_bool "isar_proofs"
val compress_isar = Real.max (1.0, lookup_real "compress_isar")
val try0_isar = lookup_bool "try0_isar"
- val smt = lookup_option lookup_bool "smt"
+ val smt_proofs = lookup_option lookup_bool "smt_proofs"
val slice = mode <> Auto_Try andalso lookup_bool "slice"
val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
val timeout = lookup_time "timeout"
@@ -300,7 +300,7 @@
uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
- compress_isar = compress_isar, try0_isar = try0_isar, smt = smt, slice = slice,
+ compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 19:32:02 2014 +0100
@@ -126,7 +126,7 @@
val skolem_methods =
[Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
-fun isar_proof_text ctxt debug isar_proofs smt isar_params
+fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
fun isar_proof_of () =
@@ -137,7 +137,9 @@
val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
fun massage_meths (meths as meth :: _) =
- if not try0_isar then [meth] else if smt = SOME true then SMT_Method :: meths else meths
+ if not try0_isar then [meth]
+ else if smt_proofs = SOME true then SMT_Method :: meths
+ else meths
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
@@ -355,18 +357,18 @@
if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
in one_line_proof ^ isar_proof end
-fun isar_proof_would_be_a_good_idea smt (meth, play) =
+fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
(case play of
- Played _ => meth = SMT_Method andalso smt <> SOME true
+ Played _ => meth = SMT_Method andalso smt_proofs <> SOME true
| Play_Timed_Out _ => true
| Play_Failed => true
| Not_Played => false)
-fun proof_text ctxt debug isar_proofs smt isar_params num_chained
+fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
(one_line_params as (preplay, _, _, _, _, _)) =
(if isar_proofs = SOME true orelse
- (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt preplay) then
- isar_proof_text ctxt debug isar_proofs smt isar_params
+ (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then
+ isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
else
one_line_proof_text num_chained) one_line_params
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 19:32:02 2014 +0100
@@ -38,7 +38,7 @@
isar_proofs : bool option,
compress_isar : real,
try0_isar : bool,
- smt : bool option,
+ smt_proofs : bool option,
slice : bool,
minimize : bool option,
timeout : Time.time,
@@ -147,7 +147,7 @@
isar_proofs : bool option,
compress_isar : real,
try0_isar : bool,
- smt : bool option,
+ smt_proofs : bool option,
slice : bool,
minimize : bool option,
timeout : Time.time,
@@ -183,7 +183,7 @@
| Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
| _ => "Try this")
-fun bunch_of_proof_methods smt needs_full_types desperate_lam_trans =
+fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
[Metis_Method (SOME full_type_enc, NONE)] @
(if needs_full_types then
[Metis_Method (SOME full_type_enc, NONE),
@@ -193,7 +193,7 @@
[Metis_Method (NONE, NONE),
Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) @
[Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] @
- (if smt then [SMT_Method] else [])
+ (if smt_proofs then [SMT_Method] else [])
fun extract_proof_method ({type_enc, lam_trans, ...} : params)
(Metis_Method (type_enc', lam_trans')) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 19:32:02 2014 +0100
@@ -132,7 +132,7 @@
fun run_atp mode name
(params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
- try0_isar, smt, slice, minimize, timeout, preplay_timeout, ...})
+ try0_isar, smt_proofs, slice, minimize, timeout, preplay_timeout, ...})
minimize_command
({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
@@ -347,7 +347,7 @@
val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
val meths =
- bunch_of_proof_methods (smt <> SOME false) needs_full_types
+ bunch_of_proof_methods (smt_proofs <> SOME false) needs_full_types
(if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)
in
(used_facts,
@@ -380,7 +380,7 @@
subgoal_count)
val num_chained = length (#facts (Proof.goal state))
in
- proof_text ctxt debug isar_proofs smt isar_params num_chained one_line_params
+ proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params
end,
(if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^
(if important_message <> "" then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 03 19:32:02 2014 +0100
@@ -129,8 +129,8 @@
fun print silent f = if silent then () else Output.urgent_message (f ())
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
- type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar, smt,
- preplay_timeout, ...} : params)
+ type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar,
+ smt_proofs, preplay_timeout, ...} : params)
silent (prover : prover) timeout i n state goal facts =
let
val _ =
@@ -144,9 +144,9 @@
uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
- isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar, smt = smt,
- slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
- expect = ""}
+ isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar,
+ smt_proofs = smt_proofs, slice = false, minimize = SOME false, timeout = timeout,
+ preplay_timeout = preplay_timeout, expect = ""}
val problem =
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
factss = [("", facts)]}
@@ -289,8 +289,8 @@
fun adjust_proof_method_params override_params
({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
- max_new_mono_instances, isar_proofs, compress_isar, try0_isar, smt, slice, minimize, timeout,
- preplay_timeout, expect} : params) =
+ max_new_mono_instances, isar_proofs, compress_isar, try0_isar, smt_proofs, slice, minimize,
+ timeout, preplay_timeout, expect} : params) =
let
fun lookup_override name default_value =
(case AList.lookup (op =) override_params name of
@@ -305,7 +305,7 @@
uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
- compress_isar = compress_isar, try0_isar = try0_isar, smt = smt, slice = slice,
+ compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 19:32:02 2014 +0100
@@ -212,7 +212,7 @@
do_slice timeout 1 NONE Time.zeroTime
end
-fun run_smt_solver mode name (params as {debug, verbose, smt, preplay_timeout, ...})
+fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
val thy = Proof.theory_of state
@@ -234,7 +234,7 @@
NONE =>
(Lazy.lazy (fn () =>
play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
- SMT_Method (bunch_of_proof_methods (smt <> SOME false) false liftingN)),
+ SMT_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
fn preplay =>
let
val one_line_params =