summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Mon, 03 Feb 2014 19:32:02 +0100 | |

changeset 55297 | 1dfcd49f5dcb |

parent 55296 | 1d3dadda13a1 |

child 55298 | 53569ca831f4 |

renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover

--- 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 =