diff --git a/src/Doc/Sledgehammer/document/root.tex b/src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex +++ b/src/Doc/Sledgehammer/document/root.tex @@ -1,1294 +1,1292 @@ \documentclass[a4paper,12pt]{article} \usepackage{lmodern} \usepackage[T1]{fontenc} \usepackage{amsmath} \usepackage{amssymb} \usepackage[english]{babel} \usepackage{color} \usepackage{footmisc} \usepackage{graphicx} %\usepackage{mathpazo} \usepackage{multicol} \usepackage{stmaryrd} %\usepackage[scaled=.85]{beramono} \usepackage{isabelle,iman,pdfsetup} \newcommand\download{\url{https://isabelle.in.tum.de/components/}} \let\oldS=\S \def\S{\oldS\,} \def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}} \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$} \newcommand\const[1]{\textsf{#1}} %\oddsidemargin=4.6mm %\evensidemargin=4.6mm %\textwidth=150mm %\topmargin=4.6mm %\headheight=0mm %\headsep=0mm %\textheight=234mm \def\Colon{\mathord{:\mkern-1.5mu:}} %\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}} %\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}} \def\lparr{\mathopen{(\mkern-4mu\mid}} \def\rparr{\mathclose{\mid\mkern-4mu)}} \def\unk{{?}} \def\undef{(\lambda x.\; \unk)} %\def\unr{\textit{others}} \def\unr{\ldots} \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}} \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}} \urlstyle{tt} \renewcommand\_{\hbox{\textunderscore\kern-.05ex}} \begin{document} %%% TYPESETTING %\renewcommand\labelitemi{$\bullet$} \renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}} \title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex] Hammering Away \\[\smallskipamount] \Large A User's Guide to Sledgehammer for Isabelle/HOL} \author{\hbox{} \\ Jasmin Blanchette \\ {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\[4\smallskipamount] {\normalsize with contributions from} \\[4\smallskipamount] Lawrence C. Paulson \\ {\normalsize Computer Laboratory, University of Cambridge} \\ \hbox{}} \maketitle \tableofcontents \setlength{\parskip}{.7em plus .2em minus .1em} \setlength{\parindent}{0pt} \setlength{\abovedisplayskip}{\parskip} \setlength{\abovedisplayshortskip}{.9\parskip} \setlength{\belowdisplayskip}{\parskip} \setlength{\belowdisplayshortskip}{.9\parskip} % general-purpose enum environment with correct spacing \newenvironment{enum}% {\begin{list}{}{% \setlength{\topsep}{.1\parskip}% \setlength{\partopsep}{.1\parskip}% \setlength{\itemsep}{\parskip}% \advance\itemsep by-\parsep}} {\end{list}} \def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin \advance\rightskip by\leftmargin} \def\post{\vskip0pt plus1ex\endgroup} \def\prew{\pre\advance\rightskip by-\leftmargin} \def\postw{\post} \section{Introduction} \label{introduction} Sledgehammer is a tool that applies automatic theorem provers (ATPs) and satisfiability-modulo-theories (SMT) solvers on the current goal.% \footnote{The distinction between ATPs and SMT solvers is convenient but mostly historical.} % The supported ATPs are agsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E \cite{schulz-2002}, iProver \cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III \cite{leo3}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, Waldmeister \cite{waldmeister}, and Zipperposition \cite{cruanes-2014}. The ATPs are run either locally or remotely via the System\-On\-TPTP web service \cite{sutcliffe-2000}. The supported SMT solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, veriT \cite{bouton-et-al-2009}, and Z3 \cite{z3}. These are always run locally. The problem passed to the external provers (or solvers) consists of your current goal together with a heuristic selection of hundreds of facts (theorems) from the current theory context, filtered by relevance. 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 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. For Isabelle/jEdit users, Sledgehammer provides an automatic mode that can be enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options > Isabelle > General.'' In this mode, a reduced version of Sledgehammer is run on every newly entered theorem for a few seconds. \newbox\boxA \setbox\boxA=\hbox{\texttt{NOSPAM}} \newcommand\authoremail{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak in.\allowbreak tum.\allowbreak de}} To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is imported---this is rarely a problem in practice since it is part of \textit{Main}. Examples of Sledgehammer use can be found in Isabelle's \texttt{src/HOL/Metis\_Examples} directory. Comments and bug reports concerning Sledgehammer or this manual should be directed to the author at \authoremail. \section{Installation} \label{installation} Sledgehammer is part of Isabelle, so you do not need to install it. However, it relies on third-party automatic provers (ATPs and SMT solvers). Among the ATPs, agsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, and Zipperposition can be run locally; in addition, agsyHOL, Alt-Ergo, E, iProver, LEO-II, Leo-III, Satallax, SNARK, Vampire, Waldmeister, and Zipperposition are available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers CVC3, CVC4, veriT, and Z3 can be run locally. There are three main ways to install automatic provers on your machine: \begin{sloppy} \begin{enum} \item[\labelitemi] If you installed an official Isabelle package, it should already include properly setup executables for CVC4, E, SPASS, Vampire, and Z3, ready to use. To use Vampire, you must confirm that you are a noncommercial user, as indicated by the message that is displayed when Sledgehammer is invoked the first time. \item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, CVC4, E, SPASS, Vampire, and Z3 binary packages from \download. Extract the archives, then add a line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}% \footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at startup. Its value can be retrieved by executing \texttt{isabelle} \texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.} file with the absolute path to CVC3, CVC4, E, SPASS, Vampire, or Z3. For example, if the \texttt{components} file does not exist yet and you extracted SPASS to \texttt{/usr/local/spass-3.8ds}, create it with the single line \prew \texttt{/usr/local/spass-3.8ds} \postw in it. \item[\labelitemi] If you prefer to build agsyHOL, Alt-Ergo, E, LEO-II, Leo-III, or Satallax manually, set the environment variable \texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME}, \texttt{LEO3\_HOME}, or \texttt{SATALLAX\_HOME} to the directory that contains the \texttt{agsyHOL}, \texttt{eprover} (and/or \texttt{eproof} or \texttt{eproof\_ram}), \texttt{leo}, \texttt{leo3}, or \texttt{satallax} executable; for Alt-Ergo, set the environment variable \texttt{WHY3\_HOME} to the directory that contains the \texttt{why3} executable. Sledgehammer has been tested with agsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 2.0, LEO-II 1.3.4, Leo-III 1.1, and Satallax 2.7. Since the ATPs' output formats are neither documented nor stable, other versions might not work well with Sledgehammer. Ideally, you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION}, \texttt{LEO3\_VERSION}, or \texttt{SATALLAX\_VERSION} to the prover's version number (e.g., ``2.7''); this might help Sledgehammer invoke the prover optimally. Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER}, \texttt{VERIT\_\allowbreak SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of the executable, \emph{including the file name}. Sledgehammer has been tested with CVC3 2.2 and 2.4.1, CVC4 1.5-prerelease, veriT smtcomp2019, and Z3 4.3.2. Since Z3's output format is somewhat unstable, other versions of the solver might not work well with Sledgehammer. Ideally, also set \texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, \texttt{VERIT\_VERSION}, or \texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.4.0''). \end{enum} \end{sloppy} To check whether the provers are successfully installed, try out the example in \S\ref{first-steps}. If the remote versions of any of these provers is used (identified by the prefix ``\textit{remote\_\/}''), or if the local versions fail to solve the easy goal presented there, something must be wrong with the installation. Remote prover invocation requires Perl with the World Wide Web Library (\texttt{libwww-perl}) installed. If you must use a proxy server to access the Internet, set the \texttt{http\_proxy} environment variable to the proxy, either in the environment in which Isabelle is launched or in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few examples: \prew \texttt{http\_proxy=http://proxy.example.org} \\ \texttt{http\_proxy=http://proxy.example.org:8080} \\ \texttt{http\_proxy=http://joeblow:pAsSwRd@proxy.example.org} \postw \section{First Steps} \label{first-steps} To illustrate Sledgehammer in context, let us start a theory file and attempt to prove a simple lemma: \prew \textbf{theory}~\textit{Scratch} \\ \textbf{imports}~\textit{Main} \\ \textbf{begin} \\[2\smallskipamount] % \textbf{lemma} ``$[a] = [b] \,\Longrightarrow\, a = b$'' \\ \textbf{sledgehammer} \postw Instead of issuing the \textbf{sledgehammer} command, you can also use the Sledgehammer panel in Isabelle/jEdit. Sledgehammer produces the following output after a few seconds: \prew \slshape Proof found\ldots \\ ``\textit{e\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms) \\ % ``\textit{cvc4\/}'': Try this: \textbf{by} \textit{simp} (0.4 ms) \\ % ``\textit{z3\/}'': Try this: \textbf{by} \textit{simp} (0.5 ms) \\ % ``\textit{spass\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms) % \postw Sledgehammer ran CVC4, E, SPASS, and Z3 in parallel. Depending on which provers are installed and how many processor cores are available, some of the provers might be missing or present with a \textit{remote\_} prefix. 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. In addition, you can ask Sledgehammer for an Isar text proof by enabling the \textit{isar\_proofs} option (\S\ref{output-format}): \prew \textbf{sledgehammer} [\textit{isar\_proofs}] \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-line proofs. This feature is experimental and is only available for ATPs. \section{Hints} \label{hints} This section presents a few hints that should help you get the most out of Sledgehammer. Frequently asked questions are answered in \S\ref{frequently-asked-questions}. %\newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak} \newcommand\point[1]{\subsection{\emph{#1}}} \point{Presimplify the goal} For best results, first simplify your problem by calling \textit{auto} or at least \textit{safe} followed by \textit{simp\_all}. The SMT solvers provide arithmetic decision procedures, but the ATPs typically do not (or if they do, Sledgehammer does not use it yet). Apart from Waldmeister, they are not particularly good at heavy rewriting, but because they regard equations as undirected, they often prove theorems that require the reverse orientation of a \textit{simp} rule. Higher-order problems can be tackled, but the success rate is better for first-order problems. Hence, you may get better results if you first simplify the problem to remove higher-order features. \point{Familiarize yourself with the main options} Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of the options are very specialized, but serious users of the tool should at least familiarize themselves with the following options: \begin{enum} \item[\labelitemi] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies the automatic provers (ATPs and SMT solvers) that should be run whenever Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{cvc4 e spass vampire\/}''). For convenience, you can omit ``\textit{provers}~='' and simply write the prover names as a space-separated list (e.g., ``\textit{cvc4 e spass vampire\/}''). \item[\labelitemi] \textbf{\textit{max\_facts}} (\S\ref{relevance-filter}) specifies the maximum number of facts that should be passed to the provers. By default, the value is prover-dependent but varies between about 50 and 1000. If the provers time out, you can try lowering this value to, say, 25 or 50 and see if that helps. \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies 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} (\S\ref{output-format}). \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the provers' time limit. It is set to 30 seconds by default. \end{enum} Options can be set globally using \textbf{sledgehammer\_params} (\S\ref{command-syntax}). The command also prints the list of all available options with their current value. Fact selection can be influenced by specifying ``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer} call to ensure that certain facts are included, or simply ``$(\textit{my\_facts})$'' to force Sledgehammer to run only with $\textit{my\_facts}$ (and any facts chained into the goal). \section{Frequently Asked Questions} \label{frequently-asked-questions} This sections answers frequently (and infrequently) asked questions about Sledgehammer. It is a good idea to skim over it now even if you do not have any questions at this stage. And if you have any further questions not listed here, send them to the author at \authoremail. \point{Which facts are passed to the automatic provers?} Sledgehammer heuristically selects a few hundred relevant lemmas from the currently loaded libraries. The component that performs this selection is called \emph{relevance filter} (\S\ref{relevance-filter}). \begin{enum} \item[\labelitemi] The traditional relevance filter, called \emph{MePo} (\underline{Me}ng--\underline{Pau}lson), assigns a score to every available fact (lemma, theorem, definition, or axiom) based upon how many constants that fact shares with the conjecture. This process iterates to include facts relevant to those just accepted. The constants are weighted to give unusual ones greater significance. MePo copes best when the conjecture contains some unusual constants; if all the constants are common, it is unable to discriminate among the hundreds of facts that are picked up. The filter is also memoryless: It has no information about how many times a particular fact has been used in a proof, and it cannot learn. \item[\labelitemi] An alternative to MePo is \emph{MaSh} (\underline{Ma}chine Learner for \underline{S}ledge\underline{h}ammer). It applies machine learning to the problem of finding relevant facts. \item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh. This is the default. \end{enum} The number of facts included in a problem varies from prover to prover, since some provers get overwhelmed more easily than others. You can show the number of facts given using the \textit{verbose} option (\S\ref{output-format}) and the actual facts using \textit{debug} (\S\ref{output-format}). Sledgehammer is good at finding short proofs combining a handful of existing lemmas. If you are looking for longer proofs, you must typically restrict the number of facts, by setting the \textit{max\_facts} option (\S\ref{relevance-filter}) to, say, 25 or 50. You can also influence which facts are actually selected in a number of ways. If you simply want to ensure that a fact is included, you can specify it using the ``$(\textit{add}{:}~\textit{my\_facts})$'' syntax. For example: % \prew \textbf{sledgehammer} (\textit{add}: \textit{hd.simps} \textit{tl.simps}) \postw % The specified facts then replace the least relevant facts that would otherwise be included; the other selected facts remain the same. If you want to direct the selection in a particular direction, you can specify the facts via \textbf{using}: % \prew \textbf{using} \textit{hd.simps} \textit{tl.simps} \\ \textbf{sledgehammer} \postw % The facts are then more likely to be selected than otherwise, and if they are selected at iteration $j$ they also influence which facts are selected at iterations $j + 1$, $j + 2$, etc. To give them even more weight, try % \prew \textbf{using} \textit{hd.simps} \textit{tl.simps} \\ \textbf{apply}~\textbf{--} \\ \textbf{sledgehammer} \postw \point{Why does Metis fail to reconstruct the proof?} There are many reasons. If Metis runs seemingly forever, that is a sign that the proof is too difficult for it. Metis's search is complete for first-order logic with equality, so if the proof was found by a superposition-based ATP such as E, SPASS, or Vampire, Metis should eventually find it, but that is little consolation. In some rare cases, \textit{metis} fails fairly quickly, and you get the error message ``One-line proof reconstruction failed.'' This indicates that Sledgehammer determined that the goal is provable, but the proof is, for technical reasons, beyond \textit{metis}'s power. You can then try again with the \textit{strict} option (\S\ref{problem-encoding}). If the goal is actually unprovable and you did not specify an unsound encoding using \textit{type\_enc} (\S\ref{problem-encoding}), this is a bug, and you are strongly encouraged to report this to the author at \authoremail. \point{How can I tell whether a suggested proof is sound?} Earlier versions of Sledgehammer often suggested unsound proofs---either proofs of nontheorems or simply proofs that rely on type-unsound inferences. This is a thing of the past, unless you explicitly specify an unsound encoding using \textit{type\_enc} (\S\ref{problem-encoding}). % Officially, the only form of ``unsoundness'' that lurks in the sound encodings is related to missing characteristic theorems of datatypes. For example, \prew \textbf{lemma}~``$\exists \mathit{xs}.\; \mathit{xs} \neq []$'' \\ \textbf{sledgehammer} () \postw suggests an argumentless \textit{metis} call that fails. However, the conjecture does actually hold, and the \textit{metis} call can be repaired by adding \textit{list.distinct}. % We hope to address this problem in a future version of Isabelle. In the meantime, you can avoid it by passing the \textit{strict} option (\S\ref{problem-encoding}). \point{What are the \textit{full\_types}, \textit{no\_types}, and \textit{mono\_tags} arguments to Metis?} The \textit{metis}~(\textit{full\_types}) proof method and its cousin \textit{metis}~(\textit{mono\_tags}) are fully-typed 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 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 various sets of option for up to 1~second each time to ensure that the generated one-line proofs actually work and to display timing information. This can be configured using the \textit{preplay\_timeout} and \textit{dont\_preplay} options (\S\ref{timeouts}).) % At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types}) uses no type information at all during the proof search, which is more efficient but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally generated by Sledgehammer. % See the \textit{type\_enc} option (\S\ref{problem-encoding}) for details. Incidentally, if you ever see warnings such as \prew \slshape Metis: Falling back on ``\textit{metis} (\textit{full\_types})'' \postw for a successful \textit{metis} proof, you can advantageously pass the \textit{full\_types} option to \textit{metis} directly. \point{And what are the \textit{lifting} and \textit{hide\_lams} arguments to Metis?} Orthogonally to the encoding of types, it is important to choose an appropriate translation of $\lambda$-abstractions. Metis supports three translation schemes, in decreasing order of power: Curry combinators (the default), $\lambda$-lifting, and a ``hiding'' scheme that disables all reasoning under $\lambda$-abstractions. The more powerful schemes also give the automatic provers more rope to hang themselves. See the \textit{lam\_trans} option (\S\ref{problem-encoding}) for details. \point{Are the generated proofs minimal?} Automatic provers frequently use many more facts than are necessary. Sledgehammer includes a minimization tool that takes a set of facts returned by a given prover and repeatedly calls a prover or proof method with subsets of those facts to find a minimal set. Reducing the number of facts typically helps reconstruction, while also removing superfluous clutter from the proof scripts. In earlier versions of Sledgehammer, generated proofs were systematically accompanied by a suggestion to invoke the minimization tool. This step is now performed by default but can be disabled using the \textit{minimize} option (\S\ref{mode-of-operation}). \point{A strange error occurred---what should I do?} Sledgehammer tries to give informative error messages. Please report any strange error to the author at \authoremail. \point{Auto can solve it---why not Sledgehammer?} Problems can be easy for \textit{auto} and difficult for automatic provers, but the reverse is also true, so do not be discouraged if your first attempts fail. Because the system refers to all theorems known to Isabelle, it is particularly suitable when your goal has a short proof but requires lemmas that you do not know about. \point{Why are there so many options?} Sledgehammer's philosophy should work out of the box, without user guidance. Many of the options are meant to be used mostly by the Sledgehammer developers for experiments. Of course, feel free to try them out if you are so inclined. \section{Command Syntax} \label{command-syntax} \subsection{Sledgehammer} \label{sledgehammer} Sledgehammer can be invoked at any point when there is an open goal by entering the \textbf{sledgehammer} command in the theory file. Its general syntax is as follows: \prew \textbf{sledgehammer} \qty{subcommand}$^?$ \qty{options}$^?$ \qty{facts\_override}$^?$ \qty{num}$^?$ \postw In the general syntax, the \qty{subcommand} may be any of the following: \begin{enum} \item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on subgoal number \qty{num} (1 by default), with the given options and facts. \item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of automatic provers supported by Sledgehammer. See \S\ref{installation} and \S\ref{mode-of-operation} for more information on how to install automatic provers. \item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}. \end{enum} In addition, the following subcommands provide finer control over machine learning with MaSh: \begin{enum} \item[\labelitemi] \textbf{\textit{unlearn}:} Resets MaSh, erasing any persistent state. \item[\labelitemi] \textbf{\textit{learn\_isar}:} Invokes MaSh on the current theory to process all the available facts, learning from their Isabelle/Isar proofs. This happens automatically at Sledgehammer invocations if the \textit{learn} option (\S\ref{relevance-filter}) is enabled. \item[\labelitemi] \textbf{\textit{learn\_prover}:} Invokes MaSh on the current theory to process all the available facts, learning from proofs generated by automatic provers. The prover to use and its timeout can be set using the \textit{prover} (\S\ref{mode-of-operation}) and \textit{timeout} (\S\ref{timeouts}) options. It is recommended to perform learning using a first-order ATP (such as E, SPASS, and Vampire) as opposed to a higher-order ATP or an SMT solver. \item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn} followed by \textit{learn\_isar}. \item[\labelitemi] \textbf{\textit{relearn\_prover}:} Same as \textit{unlearn} followed by \textit{learn\_prover}. \end{enum} Sledgehammer's behavior can be influenced by various \qty{options}, which can be specified in brackets after the \textbf{sledgehammer} command. The \qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1, \ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. For example: \prew \textbf{sledgehammer} [\textit{isar\_proofs}, \,\textit{timeout} = 120] \postw Default values can be set using \textbf{sledgehammer\_\allowbreak params}: \prew \textbf{sledgehammer\_params} \qty{options} \postw The supported options are described in \S\ref{option-reference}. The \qty{facts\_override} argument lets you alter the set of facts that go through the relevance filter. It may be of the form ``(\qty{facts})'', where \qty{facts} is a space-separated list of Isabelle facts (theorems, local assumptions, etc.), in which case the relevance filter is bypassed and the given facts are used. It may also be of the form ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}})'', ``(\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', or ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}}\ \textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', where the relevance filter is instructed to proceed as usual except that it should consider \qty{facts\/_{\mathrm{1}}} highly-relevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant. If you use Isabelle/jEdit, Sledgehammer also provides an automatic mode that can be enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options > Isabelle > General.'' For automatic runs, only the first prover set using \textit{provers} (\S\ref{mode-of-operation}) is considered (typically E), \textit{slice} (\S\ref{mode-of-operation}) is disabled, fewer facts are passed to the prover, \textit{fact\_filter} (\S\ref{relevance-filter}) is set to \textit{mepo}, \textit{strict} (\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled, and \textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Time Limit'' option in jEdit. Sledgehammer's output is also more concise. \subsection{Metis} \label{metis} The \textit{metis} proof method has the syntax \prew \textbf{\textit{metis}}~(\qty{options})${}^?$~\qty{facts}${}^?$ \postw where \qty{facts} is a list of arbitrary facts and \qty{options} is a comma-separated list consisting of at most one $\lambda$ translation scheme specification with the same semantics as Sledgehammer's \textit{lam\_trans} option (\S\ref{problem-encoding}) and at most one type encoding specification with the same semantics as Sledgehammer's \textit{type\_enc} option (\S\ref{problem-encoding}). % The supported $\lambda$ translation schemes are \textit{hide\_lams}, \textit{lifting}, and \textit{combs} (the default). % All the untyped type encodings listed in \S\ref{problem-encoding} are supported. For convenience, the following aliases are provided: \begin{enum} \item[\labelitemi] \textbf{\textit{full\_types}:} Alias for \textit{poly\_guards\_query}. \item[\labelitemi] \textbf{\textit{partial\_types}:} Alias for \textit{poly\_args}. \item[\labelitemi] \textbf{\textit{no\_types}:} Alias for \textit{erased}. \end{enum} \section{Option Reference} \label{option-reference} \def\defl{\{} \def\defr{\}} \def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}} \def\optrueonly#1{\flushitem{\textit{#1} $\bigl[$= \textit{true}$\bigr]$\enskip}\nopagebreak\\[\parskip]} \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]} \def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]} \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]} \def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]} \def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} \def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} Sledgehammer's options are categorized as follows:\ mode of operation (\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}), relevance filter (\S\ref{relevance-filter}), output format (\S\ref{output-format}), regression testing (\S\ref{regression-testing}), and timeouts (\S\ref{timeouts}). The descriptions below refer to the following syntactic quantities: \begin{enum} \item[\labelitemi] \qtybf{string}: A string. \item[\labelitemi] \qtybf{bool\/}: \textit{true} or \textit{false}. \item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or \textit{smart}. \item[\labelitemi] \qtybf{int\/}: An integer. \item[\labelitemi] \qtybf{float}: A floating-point number (e.g., 2.5 or 60) expressing a number of seconds. \item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers (e.g., 0.6 0.95). \item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}. \end{enum} Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options have a negative counterpart (e.g., \textit{minimize} vs.\ \textit{dont\_minimize}). When setting Boolean options or their negative counterparts, ``= \textit{true\/}'' may be omitted. \subsection{Mode of Operation} \label{mode-of-operation} \begin{enum} \opnodefaultbrk{provers}{string} Specifies the automatic provers to use as a space-separated list (e.g., ``\textit{cvc4}~\textit{e}~\textit{spass}~\textit{vampire\/}''). Provers can be run locally or remotely; see \S\ref{installation} for installation instructions. The following local provers are supported: \begin{sloppy} \begin{enum} \item[\labelitemi] \textbf{\textit{agsyhol}:} agsyHOL is an automatic higher-order prover developed by Fredrik Lindblad \cite{agsyHOL}. To use agsyHOL, set the environment variable \texttt{AGSYHOL\_HOME} to the directory that contains the \texttt{agsyHOL} executable. Sledgehammer has been tested with version 1.0. \item[\labelitemi] \textbf{\textit{alt\_ergo}:} Alt-Ergo is a polymorphic ATP developed by Bobot et al.\ \cite{alt-ergo}. It supports the TPTP polymorphic typed first-order format (TF1) via Why3 \cite{why3}. To use Alt-Ergo, set the environment variable \texttt{WHY3\_HOME} to the directory that contains the \texttt{why3} executable. Sledgehammer requires Alt-Ergo 0.95.2 and Why3 0.83. \item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3, set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the executable, including the file name, or install the prebuilt CVC3 package from \download. Sledgehammer has been tested with versions 2.2 and 2.4.1. \item[\labelitemi] \textbf{\textit{cvc4}:} CVC4 \cite{cvc4} is the successor to CVC3. To use CVC4, set the environment variable \texttt{CVC4\_SOLVER} to the complete path of the executable, including the file name, or install the prebuilt CVC4 package from \download. Sledgehammer has been tested with version 1.5-prerelease. \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or install the prebuilt E package from \download. Sledgehammer has been tested with versions 1.6 to 1.8. \item[\labelitemi] \textbf{\textit{e\_par}:} E-Par is an experimental metaprover developed by Josef Urban that implements strategy scheduling on top of E. To use E-Par, set the environment variable \texttt{E\_HOME} to the directory that contains the \texttt{runepar.pl} script and the \texttt{eprover} and \texttt{epclextract} executables, or use the prebuilt E package from \download. Be aware that E-Par is experimental software. It has been known to generate zombie processes. Use at your own risks. \item[\labelitemi] \textbf{\textit{ehoh}:} Ehoh is an experimental version of E that supports a $\lambda$-free fragment of higher-order logic. Use at your own risks. \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the directory that contains the \texttt{iproveropt} executable. Sledgehammer has been tested with version 2.8. iProver depends on E to clausify problems, so make sure that E is installed as well. \item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, with support for the TPTP typed higher-order syntax (TH0). To use LEO-II, set the environment variable \texttt{LEO2\_HOME} to the directory that contains the \texttt{leo} executable. Sledgehammer requires version 1.3.4 or above. \item[\labelitemi] \textbf{\textit{leo3}:} Leo-III is an automatic higher-order prover developed by Alexander Steen, Max Wisniewski, Christoph Benzm\"uller et al.\ \cite{leo3}, with support for the TPTP typed higher-order syntax (TH0). To use Leo-III, set the environment variable \texttt{LEO3\_HOME} to the directory that contains the \texttt{leo3} executable. Sledgehammer requires version 1.1 or above. \item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with support for the TPTP typed higher-order syntax (TH0). To use Satallax, set the environment variable \texttt{SATALLAX\_HOME} to the directory that contains the \texttt{satallax} executable. Sledgehammer requires version 2.2 or above. \item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from \download. Sledgehammer requires version 3.8ds or above. \item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution prover developed by Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire} executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``4.2.2''). Sledgehammer has been tested with versions 1.8 to 4.2.2 (in the post-2010 numbering scheme). \item[\labelitemi] \textbf{\textit{verit}:} veriT \cite{bouton-et-al-2009} is an SMT solver developed by David D\'eharbe, Pascal Fontaine, and their colleagues. It is specifically designed to produce detailed proofs for reconstruction in proof assistants. To use veriT, set the environment variable \texttt{VERIT\_SOLVER} to the complete path of the executable, including the file name. Sledgehammer has been tested with version smtcomp2019. \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at Microsoft Research \cite{z3}. To use Z3, set the environment variable \texttt{Z3\_SOLVER} to the complete path of the executable, including the file name. Sledgehammer has been tested with a pre-release version of 4.4.0. \item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be an ATP, exploiting Z3's support for the TPTP typed first-order format (TF0). It is included for experimental purposes. It requires version 4.3.1 of Z3 or above. To use it, set the environment variable \texttt{Z3\_TPTP\_HOME} to the directory that contains the \texttt{z3\_tptp} executable. \item[\labelitemi] \textbf{\textit{zipperposition}:} Zipperposition \cite{cruanes-2014} is a first-order resolution prover developed by Simon Cruanes and colleagues. To use Zipperposition, set the environment variable \texttt{ZIPPERPOSITION\_HOME} to the directory that contains the \texttt{zipperposition} executable. \end{enum} \end{sloppy} Moreover, the following remote provers are supported: \begin{enum} \item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of agsyHOL runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_alt\_ergo}:} The remote version of Alt-Ergo runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_iprover}:} The remote version of iProver runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_pirate}:} Pirate is a highly experimental first-order resolution prover developed by Daniel Wand. The remote version of Pirate run on a private server he generously set up. \item[\labelitemi] \textbf{\textit{remote\_snark}:} SNARK is a first-order resolution prover developed by Stickel et al.\ \cite{snark}. The remote version of SNARK runs on Geoff Sutcliffe's Miami servers. \item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of Vampire runs on Geoff Sutcliffe's Miami servers. \item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be used to prove universally quantified equations using unconditional equations, corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister runs on Geoff Sutcliffe's Miami servers. \item[\labelitemi] \textbf{\textit{remote\_zipperposition}:} The remote version of Zipperposition runs on Geoff Sutcliffe's Miami servers. \end{enum} By default, Sledgehammer runs a subset of CVC4, E, SPASS, Vampire, veriT, and Z3 in parallel, either locally or remotely---depending on the number of processor cores available and on which provers are actually installed. It is generally desirable to run several provers in parallel. \opnodefault{prover}{string} Alias for \textit{provers}. \optrue{slice}{dont\_slice} Specifies whether the time allocated to a prover should be sliced into several segments, each of which has its own set of possibly prover-dependent options. For SPASS and Vampire, the first slice tries the fast but incomplete set-of-support (SOS) strategy, whereas the second slice runs without it. For E, up to three slices are tried, with different weighted search strategies and number of facts. For SMT solvers, several slices are tried with the same options each time but fewer and fewer facts. According to benchmarks with a timeout of 30 seconds, slicing is a valuable optimization, and you should probably leave it enabled unless you are conducting experiments. \nopagebreak {\small See also \textit{verbose} (\S\ref{output-format}).} \optrue{minimize}{dont\_minimize} Specifies whether the minimization tool should be invoked automatically after proof search. \nopagebreak {\small See also \textit{preplay\_timeout} (\S\ref{timeouts}) and \textit{dont\_preplay} (\S\ref{timeouts}).} \opfalse{spy}{dont\_spy} Specifies whether Sledgehammer should record statistics in \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak spy\_\allowbreak sledgehammer}. These statistics can be useful to the developers of Sledgehammer. If you are willing to have your interactions recorded in the name of science, please enable this feature and send the statistics file every now and then to the author of this manual (\authoremail). To change the default value of this option globally, set the environment variable \texttt{SLEDGEHAMMER\_SPY} to \textit{yes}. \nopagebreak {\small See also \textit{debug} (\S\ref{output-format}).} \opfalse{overlord}{no\_overlord} Specifies whether Sledgehammer should put its temporary files in \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for debugging Sledgehammer but also unsafe if several instances of the tool are run simultaneously. The files are identified by the prefixes \texttt{prob\_} and \texttt{mash\_}; you may safely remove them after Sledgehammer has run. \textbf{Warning:} This option is not thread-safe. Use at your own risks. \nopagebreak {\small See also \textit{debug} (\S\ref{output-format}).} \end{enum} \subsection{Relevance Filter} \label{relevance-filter} \begin{enum} \opdefault{fact\_filter}{string}{smart} Specifies the relevance filter to use. The following filters are available: \begin{enum} \item[\labelitemi] \textbf{\textit{mepo}:} The traditional memoryless MePo relevance filter. \item[\labelitemi] \textbf{\textit{mash}:} The MaSh machine learner. Three learning algorithms are provided: \begin{enum} \item[\labelitemi] \textbf{\textit{nb}} is an implementation of naive Bayes. \item[\labelitemi] \textbf{\textit{knn}} is an implementation of $k$-nearest neighbors. \item[\labelitemi] \textbf{\textit{nb\_knn}} (also called \textbf{\textit{yes}} and \textbf{\textit{sml}}) is a combination of naive Bayes and $k$-nearest neighbors. \end{enum} In addition, the special value \textit{none} is used to disable machine learning by default (cf.\ \textit{smart} below). The default algorithm is \textit{nb\_knn}. The algorithm can be selected by setting the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle > General'' in Isabelle/jEdit. Persistent data for both algorithms is stored in the directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak mash}. \item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the rankings from MePo and MaSh. \item[\labelitemi] \textbf{\textit{smart}:} A combination of MePo, MaSh, and MeSh. If the learning algorithm is set to be \textit{none}, \textit{smart} behaves like MePo. \end{enum} \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} (the default), it effectively takes a value that was empirically found to be appropriate for the prover. Typical values lie between 50 and 1000. \opdefault{fact\_thresholds}{float\_pair}{\upshape 0.45~0.85} Specifies the thresholds above which facts are considered relevant by the relevance filter. The first threshold is used for the first iteration of the relevance filter and the second threshold is used for the last iteration (if it is reached). The effective threshold is quadratically interpolated for the other iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems are relevant and 1 only theorems that refer to previously seen constants. \optrue{learn}{dont\_learn} Specifies whether MaSh should be run automatically by Sledgehammer to learn the available theories (and hence provide more accurate results). Learning takes place only if MaSh is enabled. \opdefault{max\_new\_mono\_instances}{int}{smart} 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} (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}).} \opdefault{max\_mono\_iters}{int}{smart} 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} (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}).} \end{enum} \subsection{Problem Encoding} \label{problem-encoding} \newcommand\comb[1]{\const{#1}} \begin{enum} \opdefault{lam\_trans}{string}{smart} Specifies the $\lambda$ translation scheme to use in ATP problems. The supported translation schemes are listed below: \begin{enum} \item[\labelitemi] \textbf{\textit{hide\_lams}:} Hide the $\lambda$-abstractions by replacing them by unspecified fresh constants, effectively disabling all reasoning under $\lambda$-abstractions. \item[\labelitemi] \textbf{\textit{lifting}:} Introduce a new supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions, defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting). \item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators enable the ATPs to synthesize $\lambda$-terms but tend to yield bulkier formulas than $\lambda$-lifting: The translation is quadratic in the worst case, and the equational definitions of the combinators are very prolific in the context of resolution. \item[\labelitemi] \textbf{\textit{combs\_and\_lifting}:} Introduce a new supercombinator \const{c} for each cluster of $\lambda$-abstractions and characterize it both using a lifted equation $\const{c}~x_1~\ldots~x_n = t$ and via Curry combinators. \item[\labelitemi] \textbf{\textit{combs\_or\_lifting}:} For each cluster of $\lambda$-abstractions, heuristically choose between $\lambda$-lifting and Curry combinators. \item[\labelitemi] \textbf{\textit{keep\_lams}:} Keep the $\lambda$-abstractions in the generated problems. This is available only with provers that support the TH0 syntax. \item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used depends on the ATP and should be the most efficient scheme for that ATP. \end{enum} For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting}, irrespective of the value of this option. \opsmartx{uncurried\_aliases}{no\_uncurried\_aliases} Specifies whether fresh function symbols should be generated as aliases for applications of curried functions in ATP problems. \opdefault{type\_enc}{string}{smart} Specifies the type encoding to use in ATP problems. Some of the type encodings are unsound, meaning that they can give rise to spurious proofs (unreconstructible using \textit{metis}). The type encodings are listed below, with an indication of their soundness in parentheses. An asterisk (*) indicates that the encoding is slightly incomplete for reconstruction with \textit{metis}, unless the \textit{strict} option (described below) is enabled. \begin{enum} \item[\labelitemi] \textbf{\textit{erased} (unsound):} No type information is supplied to the ATP, not even to resolve overloading. Types are simply erased. \item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using a predicate \const{g}$(\tau, t)$ that guards bound variables. Constants are annotated with their types, supplied as extra arguments, to resolve overloading. \item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is tagged with its type using a function $\const{t\/}(\tau, t)$. \item[\labelitemi] \textbf{\textit{poly\_args} (unsound):} Like for \textit{poly\_guards} constants are annotated with their types to resolve overloading, but otherwise no type information is encoded. This is the default encoding used by the \textit{metis} proof method. \item[\labelitemi] \textbf{% \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\ \textit{raw\_mono\_args} (unsound):} \\ Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args}, respectively, but the problem is additionally monomorphized, meaning that type variables are instantiated with heuristically chosen ground types. Monomorphization can simplify reasoning but also leads to larger fact bases, which can slow down the ATPs. \item[\labelitemi] \textbf{% \textit{mono\_guards}, \textit{mono\_tags} (sound); \textit{mono\_args} (unsound):} \\ Similar to \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and \textit{raw\_mono\_args}, respectively but types are mangled in constant names instead of being supplied as ground term arguments. The binary predicate $\const{g}(\tau, t)$ becomes a unary predicate $\const{g\_}\tau(t)$, and the binary function $\const{t}(\tau, t)$ becomes a unary function $\const{t\_}\tau(t)$. \item[\labelitemi] \textbf{\textit{mono\_native} (sound):} Exploits native first-order types if the prover supports the TF0, TF1, TH0, or TH1 syntax; otherwise, falls back on \textit{mono\_guards}. The problem is monomorphized. \item[\labelitemi] \textbf{\textit{mono\_native\_higher} (sound):} Exploits native higher-order types if the prover supports the TH0 syntax; otherwise, falls back on \textit{mono\_native} or \textit{mono\_guards}. The problem is monomorphized. \item[\labelitemi] \textbf{\textit{poly\_native} (sound):} Exploits native first-order polymorphic types if the prover supports the TF1 or TH1 syntax; otherwise, falls back on \textit{mono\_native}. \item[\labelitemi] \textbf{% \textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\ \textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\ \textit{mono\_native}? (sound*):} \\ The type encodings \textit{poly\_guards}, \textit{poly\_tags}, \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards}, \textit{mono\_tags}, and \textit{mono\_native} are fully typed and sound. For each of these, Sledgehammer also provides a lighter variant identified by a question mark (`\hbox{?}')\ that detects and erases monotonic types, notably infinite types. (For \textit{mono\_native}, the types are not actually erased but rather replaced by a shared uniform type of individuals.) As argument to the \textit{metis} proof method, the question mark is replaced by a \hbox{``\textit{\_query\/}''} suffix. \item[\labelitemi] \textbf{% \textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\ \textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\ (sound*):} \\ Even lighter versions of the `\hbox{?}' encodings. As argument to the \textit{metis} proof method, the `\hbox{??}' suffix is replaced by \hbox{``\textit{\_query\_query\/}''}. \item[\labelitemi] \textbf{% \textit{poly\_guards}@, \textit{poly\_tags}@, \textit{raw\_mono\_guards}@, \\ \textit{raw\_mono\_tags}@ (sound*):} \\ Alternative versions of the `\hbox{??}' encodings. As argument to the \textit{metis} proof method, the `\hbox{@}' suffix is replaced by \hbox{``\textit{\_at\/}''}. \item[\labelitemi] \textbf{\textit{poly\_args}?, \textit{raw\_mono\_args}? (unsound):} \\ Lighter versions of \textit{poly\_args} and \textit{raw\_mono\_args}. \item[\labelitemi] \textbf{\textit{smart}:} The actual encoding used depends on the ATP and should be the most efficient sound encoding for that ATP. \end{enum} For SMT solvers, the type encoding is always \textit{mono\_native}, irrespective of the value of this option. \nopagebreak {\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter}) and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).} \opfalse{strict}{non\_strict} Specifies whether Sledgehammer should run in its strict mode. In that mode, sound type encodings marked with an asterisk (*) above are made complete for reconstruction with \textit{metis}, at the cost of some clutter in the generated problems. This option has no effect if \textit{type\_enc} is deliberately set to an unsound encoding. \end{enum} \subsection{Output Format} \label{output-format} \begin{enum} \opfalse{verbose}{quiet} Specifies whether the \textbf{sledgehammer} command should explain what it does. \opfalse{debug}{no\_debug} Specifies whether Sledgehammer should display additional debugging information beyond what \textit{verbose} already displays. Enabling \textit{debug} also enables \textit{verbose} behind the scenes. \nopagebreak {\small See also \textit{spy} (\S\ref{mode-of-operation}) and \textit{overlord} (\S\ref{mode-of-operation}).} \opsmart{isar\_proofs}{no\_isar\_proofs} 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}{int}{smart} Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs} is explicitly enabled. A value of $n$ indicates that each Isar proof step should correspond to a group of up to $n$ consecutive proof steps in the ATP proof. If the option is set to \textit{smart} (the default), the compression factor is 10 if the \textit{isar\_proofs} option is explicitly enabled; otherwise, it is $\infty$. \optrueonly{dont\_compress} Alias for ``\textit{compress} = 1''. \optrue{try0}{dont\_try0} Specifies whether standard proof methods such as \textit{auto} and \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\_proofs}{no\_smt\_proofs} +\optrue{smt\_proofs}{no\_smt\_proofs} Specifies whether the \textit{smt} proof method should be tried in addition to -Isabelle's other proof methods. 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. +Isabelle's built-in proof methods. \end{enum} \subsection{Regression Testing} \label{regression-testing} \begin{enum} \opnodefault{expect}{string} Specifies the expected outcome, which must be one of the following: \begin{enum} \item[\labelitemi] \textbf{\textit{some}:} Sledgehammer found a proof. \item[\labelitemi] \textbf{\textit{none}:} Sledgehammer found no proof. \item[\labelitemi] \textbf{\textit{timeout}:} Sledgehammer timed out. \item[\labelitemi] \textbf{\textit{unknown}:} Sledgehammer encountered some problem. \end{enum} Sledgehammer emits an error if the actual outcome differs from the expected outcome. This option is useful for regression testing. \nopagebreak {\small See also \textit{timeout} (\S\ref{timeouts}).} \end{enum} \subsection{Timeouts} \label{timeouts} \begin{enum} \opdefault{timeout}{float}{\upshape 30} Specifies the maximum number of seconds that the automatic provers should spend searching for a proof. This excludes problem preparation and is a soft limit. \opdefault{preplay\_timeout}{float}{\upshape 1} 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}).} \optrueonly{dont\_preplay} Alias for ``\textit{preplay\_timeout} = 0''. \end{enum} \let\em=\sl \bibliography{manual}{} \bibliographystyle{abbrv} \end{document} diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML @@ -1,412 +1,412 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_commands.ML Author: Jasmin Blanchette, TU Muenchen Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax. *) signature SLEDGEHAMMER_COMMANDS = sig type params = Sledgehammer_Prover.params val provers : string Unsynchronized.ref val default_params : theory -> (string * string) list -> params end; structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS = struct open ATP_Util open ATP_Systems open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Prover open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh open Sledgehammer val cvc4N = "cvc4" val veritN = "verit" val z3N = "z3" val runN = "run" val supported_proversN = "supported_provers" val refresh_tptpN = "refresh_tptp" (** Sledgehammer commands **) fun add_fact_override ns : fact_override = {add = ns, del = [], only = false} fun del_fact_override ns : fact_override = {add = [], del = ns, only = false} fun only_fact_override ns : fact_override = {add = ns, del = [], only = true} fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) = {add = #add r1 @ #add r2, del = #del r1 @ #del r2, only = #only r1 andalso #only r2} fun merge_fact_overrides rs = fold merge_fact_override_pairwise rs (only_fact_override []) (*** parameters ***) val provers = Unsynchronized.ref "" type raw_param = string * string list val default_default_params = [("debug", "false"), ("verbose", "false"), ("overlord", "false"), ("spy", "false"), ("type_enc", "smart"), ("strict", "false"), ("lam_trans", "smart"), ("uncurried_aliases", "smart"), ("learn", "true"), ("fact_filter", "smart"), ("max_facts", "smart"), ("fact_thresholds", "0.45 0.85"), ("max_mono_iters", "smart"), ("max_new_mono_instances", "smart"), ("isar_proofs", "smart"), ("compress", "smart"), ("try0", "true"), - ("smt_proofs", "smart"), + ("smt_proofs", "true"), ("slice", "true"), ("minimize", "true"), ("preplay_timeout", "1")] val alias_params = [("prover", ("provers", [])), (* undocumented *) ("dont_preplay", ("preplay_timeout", ["0"])), ("dont_compress", ("compress", ["1"])), ("isar_proof", ("isar_proofs", [])) (* legacy *)] val negated_alias_params = [("no_debug", "debug"), ("quiet", "verbose"), ("no_overlord", "overlord"), ("dont_spy", "spy"), ("non_strict", "strict"), ("no_uncurried_aliases", "uncurried_aliases"), ("dont_learn", "learn"), ("no_isar_proofs", "isar_proofs"), ("dont_slice", "slice"), ("dont_minimize", "minimize"), ("dont_try0", "try0"), ("no_smt_proofs", "smt_proofs")] val property_dependent_params = ["provers", "timeout"] fun is_known_raw_param s = AList.defined (op =) default_default_params s orelse AList.defined (op =) alias_params s orelse AList.defined (op =) negated_alias_params s orelse member (op =) property_dependent_params s orelse s = "expect" fun is_prover_list ctxt s = (case space_explode " " s of ss as _ :: _ => forall (is_prover_supported ctxt) ss | _ => false) fun unalias_raw_param (name, value) = (case AList.lookup (op =) alias_params name of SOME (name', []) => (name', value) | SOME (param' as (name', _)) => if value <> ["false"] then param' else error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ")") | NONE => (case AList.lookup (op =) negated_alias_params name of SOME name' => (name', (case value of ["false"] => ["true"] | ["true"] => ["false"] | [] => ["false"] | _ => value)) | NONE => (name, value))) val any_type_enc = type_enc_of_string Strict "erased" (* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts =" can be omitted. For the last four, this is a secret feature. *) fun normalize_raw_param ctxt = unalias_raw_param #> (fn (name, value) => if is_known_raw_param name then (name, value) else if null value then if is_prover_list ctxt name then ("provers", [name]) else if can (type_enc_of_string Strict) name then ("type_enc", [name]) else if can (trans_lams_of_string ctxt any_type_enc) name then ("lam_trans", [name]) else if member (op =) fact_filters name then ("fact_filter", [name]) else if is_some (Int.fromString name) then ("max_facts", [name]) else error ("Unknown parameter: " ^ quote name) else error ("Unknown parameter: " ^ quote name)) (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are read correctly. *) val implode_param = strip_spaces_except_between_idents o space_implode " " (* FIXME: use "Generic_Data" *) structure Data = Theory_Data ( type T = raw_param list val empty = default_default_params |> map (apsnd single) val extend = I fun merge data : T = AList.merge (op =) (K true) data ) fun remotify_prover_if_supported_and_not_already_remote ctxt name = if String.isPrefix remote_prefix name then SOME name else let val remote_name = remote_prefix ^ name in if is_prover_supported ctxt remote_name then SOME remote_name else NONE end fun remotify_prover_if_not_installed ctxt name = if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name else remotify_prover_if_supported_and_not_already_remote ctxt name (* The first ATP of the list is used by Auto Sledgehammer. *) fun default_provers_param_value mode ctxt = [cvc4N] @ (if is_vampire_noncommercial_license_accepted () = SOME false then [] else [vampireN]) @ [z3N, eN, spassN, veritN] |> map_filter (remotify_prover_if_not_installed ctxt) (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *) |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0)) |> implode_param fun set_default_raw_param param thy = let val ctxt = Proof_Context.init_global thy in thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param)) end fun default_raw_params mode thy = let val ctxt = Proof_Context.init_global thy in Data.get thy |> fold (AList.default (op =)) [("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]), ("timeout", let val timeout = Options.default_int \<^system_option>\sledgehammer_timeout\ in [if timeout <= 0 then "none" else string_of_int timeout] end)] end fun extract_params mode default_params override_params = let val raw_params = rev override_params @ rev default_params val lookup = Option.map implode_param o AList.lookup (op =) raw_params val lookup_string = the_default "" o lookup fun general_lookup_bool option default_value name = (case lookup name of SOME s => parse_bool_option option name s | NONE => default_value) val lookup_bool = the o general_lookup_bool false (SOME false) fun lookup_time name = (case lookup name of SOME s => parse_time name s | NONE => Time.zeroTime) fun lookup_int name = (case lookup name of NONE => 0 | SOME s => (case Int.fromString s of SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value"))) fun lookup_real name = (case lookup name of NONE => 0.0 | SOME s => (case Real.fromString s of SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value"))) fun lookup_real_pair name = (case lookup name of NONE => (0.0, 0.0) | SOME s => (case s |> space_explode " " |> map Real.fromString of [SOME r1, SOME r2] => (r1, r2) | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \ \values (e.g., \"0.6 0.95\")"))) fun lookup_option lookup' name = (case lookup name of SOME "smart" => NONE | _ => SOME (lookup' name)) val debug = mode <> Auto_Try andalso lookup_bool "debug" val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") val overlord = lookup_bool "overlord" val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd val type_enc = if mode = Auto_Try then NONE else (case lookup_string "type_enc" of "smart" => NONE | s => (type_enc_of_string Strict s; SOME s)) val strict = mode = Auto_Try orelse lookup_bool "strict" val lam_trans = lookup_option lookup_string "lam_trans" val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" val learn = lookup_bool "learn" val fact_filter = lookup_option lookup_string "fact_filter" |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf) val max_facts = lookup_option lookup_int "max_facts" val fact_thresholds = lookup_real_pair "fact_thresholds" val max_mono_iters = lookup_option lookup_int "max_mono_iters" val max_new_mono_instances = lookup_option lookup_int "max_new_mono_instances" val isar_proofs = lookup_option lookup_bool "isar_proofs" val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress") val try0 = lookup_bool "try0" - val smt_proofs = lookup_option lookup_bool "smt_proofs" + val smt_proofs = lookup_bool "smt_proofs" val slice = mode <> Auto_Try andalso lookup_bool "slice" val minimize = lookup_bool "minimize" val timeout = lookup_time "timeout" val preplay_timeout = lookup_time "preplay_timeout" val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, 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 = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end fun get_params mode = extract_params mode o default_raw_params mode fun default_params thy = get_params Normal thy o map (apsnd single) val silence_state = Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false) (* Sledgehammer the given subgoal *) val default_learn_prover_timeout = 2.0 fun hammer_away override_params writeln_result subcommand opt_i fact_override state0 = let (* We generally want chained facts to be picked up by the relevance filter, because it can then give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs, verbose output, machine learning). However, if the fact is available by no other means (not even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice but to insert it into the state as an additional hypothesis. *) val {facts = chained0, ...} = Proof.goal state0 val (inserts, keep_chained) = if null chained0 orelse #only fact_override then (chained0, []) else let val ctxt0 = Proof.context_of state0 in List.partition (is_useful_unnamed_local_fact ctxt0) chained0 end val state = state0 |> (if null inserts then I else Proof.refine_insert inserts #> Proof.set_facts keep_chained) |> silence_state val thy = Proof.theory_of state val ctxt = Proof.context_of state val override_params = override_params |> map (normalize_raw_param ctxt) in if subcommand = runN then let val i = the_default 1 opt_i in ignore (run_sledgehammer (get_params Normal thy override_params) Normal writeln_result i fact_override state) end else if subcommand = supported_proversN then supported_provers ctxt else if subcommand = unlearnN then mash_unlearn ctxt else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse subcommand = relearn_isarN orelse subcommand = relearn_proverN then (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt else (); mash_learn ctxt (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *) (get_params Normal thy ([("timeout", [string_of_real default_learn_prover_timeout]), ("slice", ["false"])] @ override_params @ [("preplay_timeout", ["0"])])) fact_override (#facts (Proof.goal state)) (subcommand = learn_proverN orelse subcommand = relearn_proverN)) else if subcommand = refresh_tptpN then refresh_systems_on_tptp () else error ("Unknown subcommand: " ^ quote subcommand) end fun string_of_raw_param (key, values) = key ^ (case implode_param values of "" => "" | value => " = " ^ value) val parse_query_bang = \<^keyword>\?\ || \<^keyword>\!\ || \<^keyword>\!!\ val parse_key = Scan.repeat1 (Parse.embedded || parse_query_bang) >> implode_param val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang) val parse_param = parse_key -- Scan.optional (\<^keyword>\=\ |-- parse_value) [] val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm) val parse_fact_override_chunk = (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override) || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override) || (parse_fact_refs >> only_fact_override) val parse_fact_override = Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides)) no_fact_override val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer\ "search for first-order proof using automatic theorem provers" (Scan.optional Parse.name runN -- parse_params -- parse_fact_override -- Scan.option Parse.nat >> (fn (((subcommand, params), fact_override), opt_i) => Toplevel.keep_proof (hammer_away params NONE subcommand opt_i fact_override o Toplevel.proof_of))) val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer_params\ "set and display the default parameters for Sledgehammer" (parse_params >> (fn params => Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => writeln ("Default parameters for Sledgehammer:\n" ^ (case rev (default_raw_params Normal thy) of [] => "none" | params => params |> map string_of_raw_param |> sort_strings |> cat_lines)))))) fun try_sledgehammer auto state = let val thy = Proof.theory_of state val mode = if auto then Auto_Try else Try val i = 1 in run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state) end val _ = Try.tool_setup (sledgehammerN, (40, \<^system_option>\auto_sledgehammer\, try_sledgehammer)) val _ = Query_Operation.register {name = sledgehammerN, pri = 0} (fn {state = st, args, writeln_result, ...} => (case try Toplevel.proof_of st of SOME state => let val [provers_arg, isar_proofs_arg, try0_arg] = args val override_params = ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @ [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]), ("try0", [try0_arg]), ("debug", ["false"]), ("verbose", ["false"]), ("overlord", ["false"])]); in hammer_away override_params (SOME writeln_result) runN NONE no_fact_override state end | NONE => error "Unknown proof context")) end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML @@ -1,478 +1,478 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_isar.ML Author: Jasmin Blanchette, TU Muenchen Author: Steffen Juilf Smolka, TU Muenchen Isar proof reconstruction from ATP proofs. *) signature SLEDGEHAMMER_ISAR = sig type atp_step_name = ATP_Proof.atp_step_name type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step type 'a atp_proof = 'a ATP_Proof.atp_proof type stature = ATP_Problem_Generate.stature type one_line_params = Sledgehammer_Proof_Methods.one_line_params val trace : bool Config.T type isar_params = bool * (string option * string option) * Time.time * real option * bool * bool * (term, string) atp_step list * thm - val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) -> - int -> one_line_params -> string + val proof_text : Proof.context -> bool -> bool option -> bool -> (unit -> isar_params) -> int -> + one_line_params -> string end; structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = struct open ATP_Util open ATP_Problem open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay open Sledgehammer_Isar_Compress open Sledgehammer_Isar_Minimize structure String_Redirect = ATP_Proof_Redirect( type key = atp_step_name val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') val string_of = fst) open String_Redirect val trace = Attrib.setup_config_bool \<^binding>\sledgehammer_isar_trace\ (K false) val e_definition_rule = "definition" val e_skolemize_rule = "skolemize" val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg" val pirate_datatype_rule = "DT" val satallax_skolemize_rule = "tab_ex" val vampire_skolemisation_rule = "skolemisation" val veriT_la_generic_rule = "la_generic" val veriT_simp_arith_rule = "simp_arith" val veriT_tmp_skolemize_rule = "tmp_skolemize" val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "") val zipperposition_cnf_rule = "cnf" val skolemize_rules = [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule] fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule) val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix val is_skolemize_rule = member (op =) skolemize_rules fun is_arith_rule rule = String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse rule = veriT_la_generic_rule val is_datatype_rule = String.isPrefix pirate_datatype_rule fun raw_label_of_num num = (num, 0) fun label_of_clause [(num, _)] = raw_label_of_num num | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0) fun add_global_fact ss = apsnd (union (op =) ss) fun add_fact_of_dependency [(_, ss as _ :: _)] = add_global_fact ss | add_fact_of_dependency names = apfst (insert (op =) (label_of_clause names)) fun add_line_pass1 (line as (name, role, t, rule, [])) lines = (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or definitions. *) if role = Conjecture orelse role = Negated_Conjecture then line :: lines else if t aconv \<^prop>\True\ then map (replace_dependencies_in_line (name, [])) lines else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines else if role = Axiom then lines (* axioms (facts) need no proof lines *) else map (replace_dependencies_in_line (name, [])) lines | add_line_pass1 line lines = line :: lines fun add_lines_pass2 res [] = rev res | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) = let fun normalize role = role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop) val norm_t = normalize role t val is_duplicate = exists (fn (prev_name, prev_role, prev_t, _, _) => (prev_role = Hypothesis andalso prev_t aconv t) orelse (member (op =) deps prev_name andalso Term.aconv_untyped (normalize prev_role prev_t, norm_t))) res fun looks_boring () = t aconv \<^prop>\False\ orelse length deps < 2 fun is_skolemizing_line (_, _, _, rule', deps') = is_skolemize_rule rule' andalso member (op =) deps' name fun is_before_skolemize_rule () = exists is_skolemizing_line lines in if is_duplicate orelse (role = Plain andalso not (is_skolemize_rule rule) andalso not (is_ext_rule rule) andalso not (is_arith_rule rule) andalso not (is_datatype_rule rule) andalso not (null lines) andalso looks_boring () andalso not (is_before_skolemize_rule ())) then add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines) else add_lines_pass2 (line :: res) lines end type isar_params = bool * (string option * string option) * Time.time * real option * bool * bool * (term, string) atp_step list * thm val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method] val basic_simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method] val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method] val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods val datatype_methods = [Simp_Method, Simp_Size_Method] val systematic_methods = basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @ [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)] val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods val skolem_methods = Moura_Method :: systematic_methods fun isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = let val _ = if debug then writeln "Constructing Isar proof..." else () fun generate_proof_text () = let val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof0, goal) = isar_params () in if null atp_proof0 then one_line_proof_text ctxt 0 one_line_params else let val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods fun massage_methods (meths as meth :: _) = if not try0 then [meth] - else if smt_proofs = SOME true then SMT_Method :: meths + else if smt_proofs 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 val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd val do_preplay = preplay_timeout <> Time.zeroTime val compress = (case compress of NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0 | SOME n => n) fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev fun get_role keep_role ((num, _), role, t, rule, _) = if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE val atp_proof = fold_rev add_line_pass1 atp_proof0 [] |> add_lines_pass2 [] val conjs = map_filter (fn (name, role, _, _, _) => if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE) atp_proof val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof fun add_lemma ((l, t), rule) ctxt = let val (skos, meths) = (if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods) else if is_arith_rule rule then ([], arith_methods) else ([], rewrite_methods)) ||> massage_methods in (Prove ([], skos, l, t, [], ([], []), meths, ""), ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd)) end val (lems, _) = fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt val bot = #1 (List.last atp_proof) val refute_graph = atp_proof |> map (fn (name, _, _, _, from) => (from, name)) |> make_refute_graph bot |> fold (Atom_Graph.default_node o rpair ()) conjs val axioms = axioms_of_refute_graph refute_graph conjs val tainted = tainted_atoms_of_refute_graph refute_graph conjs val is_clause_tainted = exists (member (op =) tainted) val steps = Symtab.empty |> fold (fn (name as (s, _), role, t, rule, _) => Symtab.update_new (s, (rule, t |> (if is_clause_tainted [name] then HOLogic.dest_Trueprop #> role <> Conjecture ? s_not #> fold exists_of (map Var (Term.add_vars t [])) #> HOLogic.mk_Trueprop else I)))) atp_proof fun is_referenced_in_step _ (Let _) = false | is_referenced_in_step l (Prove (_, _, _, _, subs, (ls, _), _, _)) = member (op =) ls l orelse exists (is_referenced_in_proof l) subs and is_referenced_in_proof l (Proof (_, _, steps)) = exists (is_referenced_in_step l) steps fun insert_lemma_in_step lem (step as Prove (qs, fix, l, t, subs, (ls, gs), meths, comment)) = let val l' = the (label_of_isar_step lem) in if member (op =) ls l' then [lem, step] else let val refs = map (is_referenced_in_proof l') subs in if length (filter I refs) = 1 then let val subs' = map2 (fn false => I | true => insert_lemma_in_proof lem) refs subs in [Prove (qs, fix, l, t, subs', (ls, gs), meths, comment)] end else [lem, step] end end and insert_lemma_in_steps lem [] = [lem] | insert_lemma_in_steps lem (step :: steps) = if is_referenced_in_step (the (label_of_isar_step lem)) step then insert_lemma_in_step lem step @ steps else step :: insert_lemma_in_steps lem steps and insert_lemma_in_proof lem (Proof (fix, assms, steps)) = Proof (fix, assms, insert_lemma_in_steps lem steps) val rule_of_clause_id = fst o the o Symtab.lookup steps o fst val finish_off = close_form #> rename_bound_vars fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off | prop_of_clause names = let val lits = map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names) in (case List.partition (can HOLogic.dest_not) lits of (negs as _ :: _, pos as _ :: _) => s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos) | _ => fold (curry s_disj) lits \<^term>\False\) end |> HOLogic.mk_Trueprop |> finish_off fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else [] fun isar_steps outer predecessor accum [] = accum |> (if tainted = [] then (* e.g., trivial, empty proof by Z3 *) cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [], sort_facts (the_list predecessor, []), massage_methods systematic_methods', "")) else I) |> rev | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) = let val l = label_of_clause c val t = prop_of_clause c val rule = rule_of_clause_id id val skolem = is_skolemize_rule rule val deps = ([], []) |> fold add_fact_of_dependency gamma |> is_maybe_ext_rule rule ? add_global_fact [short_thm_name ctxt ext] |> sort_facts val meths = (if skolem then skolem_methods else if is_arith_rule rule then arith_methods else if is_datatype_rule rule then datatype_methods else systematic_methods') |> massage_methods fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "") fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs in if is_clause_tainted c then (case gamma of [g] => if skolem andalso is_clause_tainted g then let val skos = skolems_of ctxt (prop_of_clause g) val subproof = Proof (skos, [], rev accum) in isar_steps outer (SOME l) [prove [subproof] ([], [])] infs end else steps_of_rest (prove [] deps) | _ => steps_of_rest (prove [] deps)) else steps_of_rest (if skolem then (case skolems_of ctxt t of [] => prove [] deps | skos => Prove ([], skos, l, t, [], deps, meths, "")) else prove [] deps) end | isar_steps outer predecessor accum (Cases cases :: infs) = let fun isar_case (c, subinfs) = isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs val c = succedent_of_cases cases val l = label_of_clause c val t = prop_of_clause c val step = Prove (maybe_show outer c, [], l, t, map isar_case (filter_out (null o snd) cases), sort_facts (the_list predecessor, []), massage_methods systematic_methods', "") in isar_steps outer (SOME l) (step :: accum) infs end and isar_proof outer fix assms lems infs = Proof (fix, assms, fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs)) val trace = Config.get ctxt trace val canonical_isar_proof = refute_graph |> trace ? tap (tracing o prefix "Refute graph:\n" o string_of_refute_graph) |> redirect_graph axioms tainted bot |> trace ? tap (tracing o prefix "Direct proof:\n" o string_of_direct_proof) |> isar_proof true params assms lems |> postprocess_isar_proof_remove_show_stuttering |> postprocess_isar_proof_remove_unreferenced_steps I |> relabel_isar_proof_canonically val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty val _ = fold_isar_steps (fn meth => K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth [])) (steps_of_isar_proof canonical_isar_proof) () fun str_of_preplay_outcome outcome = if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?" fun str_of_meth l meth = string_of_proof_method ctxt [] meth ^ " " ^ str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) fun comment_of l = map (str_of_meth l) #> commas fun trace_isar_proof label proof = if trace then tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof ctxt subgoal subgoal_count (comment_isar_proof comment_of proof) ^ "\n") else () fun comment_of l (meth :: _) = (case (verbose, Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of (false, Played _) => "" | (_, outcome) => string_of_play_outcome outcome) val (play_outcome, isar_proof) = canonical_isar_proof |> tap (trace_isar_proof "Original") |> compress_isar_proof ctxt compress preplay_timeout preplay_data |> tap (trace_isar_proof "Compressed") |> postprocess_isar_proof_remove_unreferenced_steps (keep_fastest_method_of_isar_step (!preplay_data) #> minimize ? minimize_isar_step_dependencies ctxt preplay_data) |> tap (trace_isar_proof "Minimized") |> `(preplay_outcome_of_isar_proof (!preplay_data)) ||> (comment_isar_proof comment_of #> chain_isar_proof #> kill_useless_labels_in_isar_proof #> relabel_isar_proof_nicely #> rationalize_obtains_in_isar_proofs ctxt) in (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of (0, 1) => one_line_proof_text ctxt 0 (if is_less (play_outcome_ord (play_outcome, one_line_play)) then (case isar_proof of Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) => let val used_facts' = map_filter (fn s => if exists (fn (s', (sc, _)) => s' = s andalso sc = Chained) used_facts then NONE else SOME (s, (Global, General))) gfs in ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count) end) else one_line_params) ^ (if isar_proofs = SOME true then "\n(No Isar proof available.)" else "") | (_, num_steps) => let val msg = (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] else []) @ (if do_preplay then [string_of_play_outcome play_outcome] else []) in one_line_proof_text ctxt 0 one_line_params ^ "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ Active.sendback_markup_command (string_of_isar_proof ctxt subgoal subgoal_count isar_proof) end) end end in if debug then generate_proof_text () else (case try generate_proof_text () of SOME s => s | NONE => one_line_proof_text ctxt 0 one_line_params ^ (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else "")) end -fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) = +fun isar_proof_would_be_a_good_idea (meth, play) = (case play of - Played _ => meth = SMT_Method andalso smt_proofs <> SOME true + Played _ => false | Play_Timed_Out time => time > Time.zeroTime | Play_Failed => true) 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_proofs preplay) then + (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params else one_line_proof_text ctxt num_chained) one_line_params end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML @@ -1,200 +1,200 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen Generic prover abstraction for Sledgehammer. *) signature SLEDGEHAMMER_PROVER = sig type atp_failure = ATP_Proof.atp_failure type stature = ATP_Problem_Generate.stature type type_enc = ATP_Problem_Generate.type_enc type fact = Sledgehammer_Fact.fact type proof_method = Sledgehammer_Proof_Methods.proof_method type play_outcome = Sledgehammer_Proof_Methods.play_outcome datatype mode = Auto_Try | Try | Normal | Minimize | MaSh type params = {debug : bool, verbose : bool, overlord : bool, spy : bool, provers : string list, type_enc : string option, strict : bool, lam_trans : string option, uncurried_aliases : bool option, learn : bool, fact_filter : string option, max_facts : int option, fact_thresholds : real * real, max_mono_iters : int option, max_new_mono_instances : int option, isar_proofs : bool option, compress : real option, try0 : bool, - smt_proofs : bool option, + smt_proofs : bool, slice : bool, minimize : bool, timeout : Time.time, preplay_timeout : Time.time, expect : string} type prover_problem = {comment : string, state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, factss : (string * fact list) list, found_proof : unit -> unit} type prover_result = {outcome : atp_failure option, used_facts : (string * stature) list, used_from : fact list, preferred_methss : proof_method * proof_method list list, run_time : Time.time, message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string} type prover = params -> prover_problem -> prover_result val SledgehammerN : string val str_of_mode : mode -> string val overlord_file_location_of_prover : string -> string * string val proof_banner : mode -> string -> string val is_atp : theory -> string -> bool val bunches_of_proof_methods : bool -> bool -> bool -> string -> proof_method list list val is_fact_chained : (('a * stature) * 'b) -> bool val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> ((''a * stature) * 'b) list val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> Proof.context val supported_provers : Proof.context -> unit end; structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER = struct open ATP_Proof open ATP_Util open ATP_Systems open ATP_Problem open ATP_Problem_Generate open ATP_Proof_Reconstruct open Metis_Tactic open Sledgehammer_Fact open Sledgehammer_Proof_Methods (* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *) val SledgehammerN = "Sledgehammer" datatype mode = Auto_Try | Try | Normal | Minimize | MaSh fun str_of_mode Auto_Try = "Auto Try" | str_of_mode Try = "Try" | str_of_mode Normal = "Normal" | str_of_mode Minimize = "Minimize" | str_of_mode MaSh = "MaSh" val is_atp = member (op =) o supported_atps type params = {debug : bool, verbose : bool, overlord : bool, spy : bool, provers : string list, type_enc : string option, strict : bool, lam_trans : string option, uncurried_aliases : bool option, learn : bool, fact_filter : string option, max_facts : int option, fact_thresholds : real * real, max_mono_iters : int option, max_new_mono_instances : int option, isar_proofs : bool option, compress : real option, try0 : bool, - smt_proofs : bool option, + smt_proofs : bool, slice : bool, minimize : bool, timeout : Time.time, preplay_timeout : Time.time, expect : string} type prover_problem = {comment : string, state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, factss : (string * fact list) list, found_proof : unit -> unit} type prover_result = {outcome : atp_failure option, used_facts : (string * stature) list, used_from : fact list, preferred_methss : proof_method * proof_method list list, run_time : Time.time, message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string} type prover = params -> prover_problem -> prover_result fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover) fun proof_banner mode name = (case mode of Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof" | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" | _ => "Try this") -fun bunches_of_proof_methods try0 smt_method needs_full_types desperate_lam_trans = +fun bunches_of_proof_methods try0 smt_proofs needs_full_types desperate_lam_trans = (if try0 then [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method], [Meson_Method, Fastforce_Method, Force_Method, Presburger_Method]] else []) @ [[Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE)], (if needs_full_types then [Metis_Method (NONE, NONE), Metis_Method (SOME really_full_type_enc, NONE), Metis_Method (SOME full_typesN, SOME desperate_lam_trans), Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] else [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, SOME desperate_lam_trans), Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)])] @ - (if smt_method then [[SMT_Method]] else []) + (if smt_proofs then [[SMT_Method]] else []) fun is_fact_chained ((_, (sc, _)), _) = sc = Chained fun filter_used_facts keep_chained used = filter ((member (eq_fst (op =)) used o fst) orf (if keep_chained then is_fact_chained else K false)) val max_fact_instances = 10 (* FUDGE *) fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances = Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters) #> Config.put Monomorph.max_new_instances (max_new_instances |> the_default best_max_new_instances) #> Config.put Monomorph.max_thm_instances max_fact_instances fun supported_provers ctxt = let val thy = Proof_Context.theory_of ctxt val (remote_provers, local_provers) = sort_strings (supported_atps thy) @ sort_strings (SMT_Config.available_solvers_of ctxt) |> List.partition (String.isPrefix remote_prefix) in writeln ("Supported provers: " ^ commas (local_provers @ remote_provers)) end end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML @@ -1,407 +1,407 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen ATPs as Sledgehammer provers. *) signature SLEDGEHAMMER_PROVER_ATP = sig type mode = Sledgehammer_Prover.mode type prover = Sledgehammer_Prover.prover val atp_dest_dir : string Config.T val atp_problem_prefix : string Config.T val atp_completish : int Config.T val atp_full_names : bool Config.T val is_ho_atp : Proof.context -> string -> bool val run_atp : mode -> string -> prover end; structure Sledgehammer_Prover_ATP : SLEDGEHAMMER_PROVER_ATP = struct open ATP_Util open ATP_Problem open ATP_Proof open ATP_Problem_Generate open ATP_Proof_Reconstruct open ATP_Satallax open ATP_Systems open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_Prover (* Empty string means create files in Isabelle's temporary files directory. *) val atp_dest_dir = Attrib.setup_config_string \<^binding>\sledgehammer_atp_dest_dir\ (K "") val atp_problem_prefix = Attrib.setup_config_string \<^binding>\sledgehammer_atp_problem_prefix\ (K "prob") val atp_completish = Attrib.setup_config_int \<^binding>\sledgehammer_atp_completish\ (K 0) (* In addition to being easier to read, readable names are often much shorter, especially if types are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short names are enabled by default. *) val atp_full_names = Attrib.setup_config_bool \<^binding>\sledgehammer_atp_full_names\ (K false) fun is_atp_of_format is_format ctxt name = let val thy = Proof_Context.theory_of ctxt in (case try (get_atp thy) name of SOME config => exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt) | NONE => false) end val is_ho_atp = is_atp_of_format is_format_higher_order fun choose_type_enc strictness best_type_enc format = the_default best_type_enc #> type_enc_of_string strictness #> adjust_type_enc format fun has_bound_or_var_of_type pred = exists_subterm (fn Var (_, T as Type _) => pred T | Abs (_, T as Type _, _) => pred T | _ => false) (* Unwanted equalities are those between a (bound or schematic) variable that does not properly occur in the second operand. *) val is_exhaustive_finite = let fun is_bad_equal (Var z) t = not (exists_subterm (fn Var z' => z = z' | _ => false) t) | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) | is_bad_equal _ _ = false fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 fun do_formula pos t = (case (pos, t) of (_, \<^const>\Trueprop\ $ t1) => do_formula pos t1 | (true, Const (\<^const_name>\Pure.all\, _) $ Abs (_, _, t')) => do_formula pos t' | (true, Const (\<^const_name>\All\, _) $ Abs (_, _, t')) => do_formula pos t' | (false, Const (\<^const_name>\Ex\, _) $ Abs (_, _, t')) => do_formula pos t' | (_, \<^const>\Pure.imp\ $ t1 $ t2) => do_formula (not pos) t1 andalso (t2 = \<^prop>\False\ orelse do_formula pos t2) | (_, \<^const>\HOL.implies\ $ t1 $ t2) => do_formula (not pos) t1 andalso (t2 = \<^const>\False\ orelse do_formula pos t2) | (_, \<^const>\Not\ $ t1) => do_formula (not pos) t1 | (true, \<^const>\HOL.disj\ $ t1 $ t2) => forall (do_formula pos) [t1, t2] | (false, \<^const>\HOL.conj\ $ t1 $ t2) => forall (do_formula pos) [t1, t2] | (true, Const (\<^const_name>\HOL.eq\, _) $ t1 $ t2) => do_equals t1 t2 | (true, Const (\<^const_name>\Pure.eq\, _) $ t1 $ t2) => do_equals t1 t2 | _ => false) in do_formula true end (* Facts containing variables of finite types such as "unit" or "bool" or of the form "ALL x. x = A | x = B | x = C" are likely to lead to untypable proofs for unsound type encodings. *) fun is_dangerous_prop ctxt = transform_elim_prop #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite) fun get_slices slice slices = (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single) fun get_facts_of_filter _ [(_, facts)] = facts | get_facts_of_filter fact_filter factss = (case AList.lookup (op =) factss fact_filter of SOME facts => facts | NONE => snd (hd factss)) (* For low values of "max_facts", this fudge value ensures that most slices are invoked with a nontrivial amount of facts. *) val max_fact_factor_fudge = 5 val mono_max_privileged_facts = 10 fun suffix_of_mode Auto_Try = "_try" | suffix_of_mode Try = "_try" | suffix_of_mode Normal = "" | suffix_of_mode MaSh = "" | suffix_of_mode Minimize = "_min" (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on Linux appears to be the only ATP that does not honor its time limit. *) val atp_timeout_slack = seconds 1.0 (* Important messages are important but not so important that users want to see them each time. *) val atp_important_message_keep_quotient = 25 fun run_atp mode name ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, slice, minimize, timeout, preplay_timeout, ...} : params) ({comment, state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) = let val thy = Proof.theory_of state val ctxt = Proof.context_of state val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters, best_max_new_mono_instances, ...} = get_atp thy name () val full_proofs = isar_proofs |> the_default (mode = Minimize) val local_name = perhaps (try (unprefix remote_prefix)) name val spassy = (local_name = pirateN orelse local_name = spassN) val completish = Config.get ctxt atp_completish val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt val (dest_dir, problem_prefix) = if overlord then overlord_file_location_of_prover name else (Config.get ctxt atp_dest_dir, Config.get ctxt atp_problem_prefix) val problem_file_name = Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ suffix_of_mode mode ^ "_" ^ string_of_int subgoal) val prob_path = if dest_dir = "" then File.tmp_path problem_file_name else if File.exists (Path.explode dest_dir) then Path.append (Path.explode dest_dir) problem_file_name else error ("No such directory: " ^ quote dest_dir) val exec = exec full_proofs val command0 = (case find_first (fn var => getenv var <> "") (fst exec) of SOME var => let val pref = getenv var ^ "/" val paths = map (Path.explode o prefix pref) (if ML_System.platform_is_windows then map (suffix ".exe") (snd exec) @ snd exec else snd exec); in (case find_first File.exists paths of SOME path => path | NONE => error ("Bad executable: " ^ Path.print (hd paths))) end | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set")) fun split_time s = let val split = String.tokens (fn c => str c = "\n") val (output, t) = s |> split |> (try split_last #> the_default ([], "0")) |>> cat_lines val num = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int) val digit = Scan.one Symbol.is_ascii_digit val num3 = digit ::: digit ::: (digit >> single) >> (fst o read_int) val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b) val as_time = raw_explode #> Scan.read Symbol.stopper time #> the_default 0 in (output, as_time t |> Time.fromMilliseconds) end fun run () = let (* If slicing is disabled, we expand the last slice to fill the entire time available. *) val all_slices = best_slices ctxt val actual_slices = get_slices slice all_slices fun max_facts_of_slices (slices : (real * (slice_spec * string)) list) = fold (Integer.max o fst o #1 o fst o snd) slices 0 val num_actual_slices = length actual_slices val max_fact_factor = Real.fromInt (case max_facts of NONE => max_facts_of_slices all_slices | SOME max => max) / Real.fromInt (max_facts_of_slices (map snd actual_slices)) fun monomorphize_facts facts = let val ctxt = ctxt |> repair_monomorph_context max_mono_iters best_max_mono_iters max_new_mono_instances best_max_new_mono_instances (* pseudo-theorem involving the same constants as the subgoal *) val subgoal_th = Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy val rths = facts |> chop mono_max_privileged_facts |>> map (pair 1 o snd) ||> map (pair 2 o snd) |> op @ |> cons (0, subgoal_th) in Monomorph.monomorph atp_schematic_consts_of ctxt rths |> tl |> curry ListPair.zip (map fst facts) |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) end fun run_slice time_left (cache_key, cache_value) (slice, (time_frac, (key as ((best_max_facts, best_fact_filter), format, best_type_enc, best_lam_trans, best_uncurried_aliases), extra))) = let val effective_fact_filter = fact_filter |> the_default best_fact_filter val facts = get_facts_of_filter effective_fact_filter factss val num_facts = Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge |> Integer.min (length facts) val generate_info = (case format of DFG _ => true | _ => false) val strictness = if strict then Strict else Non_Strict val type_enc = type_enc |> choose_type_enc strictness best_type_enc format val sound = is_type_enc_sound type_enc val real_ms = Real.fromInt o Time.toMilliseconds val slice_timeout = (real_ms time_left |> (if slice < num_actual_slices - 1 then curry Real.min (time_frac * real_ms timeout) else I)) * 0.001 |> seconds val generous_slice_timeout = if mode = MaSh then one_day else slice_timeout + atp_timeout_slack val _ = if debug then quote name ^ " slice #" ^ string_of_int (slice + 1) ^ " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..." |> writeln else () val readable_names = not (Config.get ctxt atp_full_names) val lam_trans = lam_trans |> the_default best_lam_trans val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases val value as (atp_problem, _, _, _) = if cache_key = SOME key then cache_value else facts |> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) |> take num_facts |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd Thm.prop_of) |> generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode lam_trans uncurried_aliases readable_names true hyp_ts concl_t fun sel_weights () = atp_problem_selection_weights atp_problem fun ord_info () = atp_problem_term_order_info atp_problem val ord = effective_term_order ctxt name val args = arguments ctxt full_proofs extra slice_timeout (File.bash_path prob_path) (ord, ord_info, sel_weights) val command = "(exec 2>&1; " ^ File.bash_path command0 ^ " " ^ args ^ " " ^ ")" |> enclose "TIMEFORMAT='%3R'; { time " " ; }" val _ = atp_problem |> lines_of_atp_problem format ord ord_info |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path val ((output, run_time), (atp_proof, outcome)) = Timeout.apply generous_slice_timeout Isabelle_System.bash_output command |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I) |> fst |> split_time |> (fn accum as (output, _) => (accum, extract_tstplike_proof_and_outcome verbose proof_delims known_failures output |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name) atp_problem handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable))) handle Timeout.TIMEOUT _ => (("", slice_timeout), ([], SOME TimedOut)) val outcome = (case outcome of NONE => (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of SOME facts => let val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts) in if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure end | NONE => (found_proof (); NONE)) | _ => outcome) in ((SOME key, value), (output, run_time, facts, atp_proof, outcome), SOME (format, type_enc)) end val timer = Timer.startRealTimer () fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _), _)) = let val time_left = timeout - Timer.checkRealTimer timer in if time_left <= Time.zeroTime then result else run_slice time_left cache slice |> (fn (cache, (output, run_time, used_from, atp_proof, outcome), format_type_enc) => (cache, (output, run_time0 + run_time, used_from, atp_proof, outcome), format_type_enc)) end | maybe_run_slice _ result = result in ((NONE, ([], Symtab.empty, [], Symtab.empty)), ("", Time.zeroTime, [], [], SOME InternalError), NONE) |> fold maybe_run_slice actual_slices end (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) fun clean_up () = if dest_dir = "" then (try File.rm prob_path; ()) else () fun export (_, (output, _, _, _, _), _) = if dest_dir = "" then () else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output val ((_, (_, pool, lifted, sym_tab)), (output, run_time, used_from, atp_proof, outcome), SOME (format, type_enc)) = with_cleanup clean_up run () |> tap export val important_message = if mode = Normal andalso Random.random_range 0 (atp_important_message_keep_quotient - 1) = 0 then extract_important_message output else "" val (used_facts, preferred_methss, message) = (case outcome of NONE => let val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof) val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof val preferred_methss = (Metis_Method (NONE, NONE), - bunches_of_proof_methods try0 (smt_proofs <> SOME false) needs_full_types - (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)) + bunches_of_proof_methods try0 smt_proofs needs_full_types + (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)) in (used_facts, preferred_methss, fn preplay => let val _ = if verbose then writeln "Generating proof text..." else () fun isar_params () = let val metis_type_enc = if is_typed_helper_used_in_atp_proof atp_proof then SOME full_typesN else NONE val metis_lam_trans = if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE val atp_proof = atp_proof |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab |> spassy ? introduce_spassy_skolems |> factify_atp_proof (map fst used_from) hyp_ts concl_t in (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0, minimize, atp_proof, goal) end val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params ^ (if important_message <> "" then "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message else "") end) end | SOME failure => ([], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) in {outcome = outcome, used_facts = used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} end end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML @@ -1,230 +1,228 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen SMT solvers as Sledgehammer provers. *) signature SLEDGEHAMMER_PROVER_SMT = sig type stature = ATP_Problem_Generate.stature type mode = Sledgehammer_Prover.mode type prover = Sledgehammer_Prover.prover val smt_builtins : bool Config.T val smt_triggers : bool Config.T val smt_max_slices : int Config.T val smt_slice_fact_frac : real Config.T val smt_slice_time_frac : real Config.T val smt_slice_min_secs : int Config.T val is_smt_prover : Proof.context -> string -> bool val run_smt_solver : mode -> string -> prover end; structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT = struct open ATP_Util open ATP_Proof open ATP_Systems open ATP_Problem_Generate open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_Prover val smt_builtins = Attrib.setup_config_bool \<^binding>\sledgehammer_smt_builtins\ (K true) val smt_triggers = Attrib.setup_config_bool \<^binding>\sledgehammer_smt_triggers\ (K true) val is_smt_prover = member (op =) o SMT_Config.available_solvers_of (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out properly in the SMT module, we must interpret these here. *) val z3_failures = [(101, OutOfResources), (103, MalformedInput), (110, MalformedInput), (112, TimedOut)] val unix_failures = [(134, Crashed), (138, Crashed), (139, Crashed)] val smt_failures = z3_failures @ unix_failures fun failure_of_smt_failure (SMT_Failure.Counterexample genuine) = if genuine then Unprovable else GaveUp | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) = (case AList.lookup (op =) smt_failures code of SOME failure => failure | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code)) | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s (* FUDGE *) val smt_max_slices = Attrib.setup_config_int \<^binding>\sledgehammer_smt_max_slices\ (K 8) val smt_slice_fact_frac = Attrib.setup_config_real \<^binding>\sledgehammer_smt_slice_fact_frac\ (K 0.667) val smt_slice_time_frac = Attrib.setup_config_real \<^binding>\sledgehammer_smt_slice_time_frac\ (K 0.333) val smt_slice_min_secs = Attrib.setup_config_int \<^binding>\sledgehammer_smt_slice_min_secs\ (K 3) val is_boring_builtin_typ = not o exists_subtype (member (op =) [\<^typ>\nat\, \<^typ>\int\, HOLogic.realT]) fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice, ...} : params) state goal i = let fun repair_context ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver name) |> Config.put SMT_Config.verbose debug |> (if overlord then Config.put SMT_Config.debug_files (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name)) else I) |> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers) |> not (Config.get ctxt smt_builtins) ? (SMT_Builtin.filter_builtins is_boring_builtin_typ #> Config.put SMT_Systems.z3_extensions false) |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances default_max_new_mono_instances val state = Proof.map_context (repair_context) state val ctxt = Proof.context_of state val max_slices = if slice then Config.get ctxt smt_max_slices else 1 fun do_slice timeout slice outcome0 time_so_far (factss as (fact_filter, facts) :: _) = let val timer = Timer.startRealTimer () val slice_timeout = if slice < max_slices then let val ms = Time.toMilliseconds timeout in Int.min (ms, Int.max (1000 * Config.get ctxt smt_slice_min_secs, Real.ceil (Config.get ctxt smt_slice_time_frac * Real.fromInt ms))) |> Time.fromMilliseconds end else timeout val num_facts = length facts val _ = if debug then quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout |> writeln else () val birth = Timer.checkRealTimer timer val filter_result as {outcome, ...} = SMT_Solver.smt_filter ctxt goal facts i slice_timeout handle exn => if Exn.is_interrupt exn orelse debug then Exn.reraise exn else {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), fact_ids = NONE, atp_proof = K []} val death = Timer.checkRealTimer timer val outcome0 = if is_none outcome0 then SOME outcome else outcome0 val time_so_far = time_so_far + (death - birth) val timeout = timeout - Timer.checkRealTimer timer val too_many_facts_perhaps = (case outcome of NONE => false | SOME (SMT_Failure.Counterexample _) => false | SOME SMT_Failure.Time_Out => slice_timeout <> timeout | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *) | SOME SMT_Failure.Out_Of_Memory => true | SOME (SMT_Failure.Other_Failure _) => true) in if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso timeout > Time.zeroTime then let val new_num_facts = Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts) val factss as (new_fact_filter, _) :: _ = factss |> (fn (x :: xs) => xs @ [x]) |> 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 debug then quote name ^ " invoked with " ^ num_of_facts fact_filter num_facts ^ ": " ^ string_of_atp_failure (failure_of_smt_failure (the outcome)) ^ " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^ "..." |> writeln else () in do_slice timeout (slice + 1) outcome0 time_so_far factss end else {outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result, used_from = facts, run_time = time_so_far} end in do_slice timeout 1 NONE Time.zeroTime end fun run_smt_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs, minimize, preplay_timeout, ...}) ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) = let val thy = Proof.theory_of state val ctxt = Proof.context_of state val factss = map (apsnd (map (apsnd (Thm.transfer thy)))) factss val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} = smt_filter_loop name params state goal subgoal factss val used_facts = (case fact_ids of NONE => map fst used_from | SOME ids => sort_by fst (map (fst o snd) ids)) val outcome = Option.map failure_of_smt_failure outcome val (preferred_methss, message) = (case outcome of NONE => let val _ = found_proof (); - val smt_method = smt_proofs <> SOME false val preferred_methss = - (if smt_method then SMT_Method else Metis_Method (NONE, NONE), - bunches_of_proof_methods try0 smt_method false liftingN) + (if smt_proofs then SMT_Method else Metis_Method (NONE, NONE), + bunches_of_proof_methods try0 smt_proofs false liftingN) in (preferred_methss, fn preplay => let val _ = if verbose then writeln "Generating proof text..." else () fun isar_params () = (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (), goal) val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in - proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained - one_line_params + proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params end) end | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) in {outcome = outcome, used_facts = used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} end end;