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,1293 +1,1383 @@ \documentclass[a4paper,12pt]{article} \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] +Martin Desharnais \\ +{\normalsize Forschungsinstitut CODE, Universit\"at der Bundeswehr M\"unchen} \\[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 higher-order superposition 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 and \texttt{ZIPPERPOSITION\_VERSION} to the version number (e.g., ``2.0.1''). Sledgehammer has been tested with version 2.0.1. \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. \optrue{smt\_proofs}{no\_smt\_proofs} Specifies whether the \textit{smt} proof method should be tried in addition to 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} +\section{Mirabelle Testing Tool} +\label{mirabelle} + +% using Sledgehammer or other advisory tools +% proof tools or counterexample generator +The \texttt{isabelle mirabelle} tool executes Sledgehammer, or other advisory +tools (e.g. proof tools, counterexample generators) on most subgoals in a theory. +It is typically used to quantify the success rate of a proof tool on a +representative benchmark. Its command-line usage is: + +{\small +\begin{verbatim} +isabelle mirabelle [OPTIONS] ACTIONS FILES + + Options are: + -L LOGIC parent logic to use (default HOL) + -O DIR output directory for test data (default None) + -S FILE user-provided setup file (no actions required) + -T THEORY parent theory to use (default Main) + -d DIR include session directory + -q be quiet (suppress output of Isabelle process) + -t TIMEOUT timeout for each action in seconds (default 30) + + Apply the given actions at all proof steps in the given theory + files. +\end{verbatim} +} + +Option \texttt{-L LOGIC} specifies the parent session to use. This is often a +logic (e.g. Pure, HOL) but may be any session (e.g. from the AFP). Using +multiple sessions is not supported at the moment. If a theory A needs to import +from multiple sessions, this limitation can be overcome by + +\begin{enumerate} + \item defining a custom session S with a single theory B; + \item moving all imports from A to B; + \item building the heap image of S; + \item importing S.B from theory A; + \item executing Mirabelle with C as parent logic, i.e. with \texttt{-L S}. +\end{enumerate} + +Option \texttt{-O DIR} specifies the output directory, which is created if not +already existing, where the log will be written. In this directory, one log +file per theory records the position of each tested subgoal and the result of +executing the proof tool. + +Option \texttt{-t TIMEOUT} specifies a generic timeout that different actions +may interpret in different ways. + +More specific documentation about parameters \texttt{ACTIONS}, \texttt{FILES}, +and their corresponding options may be found in the isabelle tool usage by +entering \texttt{isabelle mirabelle -?} on the command line. + +\subsection{Example of Benchmarking Sledgehammer} + +\begin{verbatim} +isabelle mirabelle -O output \ + sledgehammer[prover=e,prover_timeout=10] Huffman.thy +\end{verbatim} + +This command benchmarks sledgehammer when using \textbf{\textit{e}} as prover +with a timeout of 10 seconds. The results are written to the file +\texttt{output/Huffman.log}. + +\subsection{Example of Benchmarking Other Tools} + +\begin{verbatim} +isabelle mirabelle -O output -t 10 \ + try0 Huffman.thy +\end{verbatim} + +This command benchmarks the \texttt{try0} tactic with a timeout of 10 seconds. +The results are written to the file \texttt{output/Huffman.log}. + +\subsection{Example of Generating TPTP Files} + +\begin{verbatim} +isabelle mirabelle -O output \ + sledgehammer[prover_timeout=1,keep=tptp-files] Huffman.thy +\end{verbatim} + +This command generates TPTP files with sledgehammer. Since the file is +generated at the very beginning of every sledgehammer invocation, a timeout of +1 second making the prover fail faster speeds handling the theory up. The +results are written in the \texttt{tptp-files} directory, which has to exist +prior to the command invocation. A distinct TPTP file is generated for each +subgoal with a file name ending with \texttt{.smt\_in}. + \let\em=\sl \bibliography{manual}{} \bibliographystyle{abbrv} \end{document} diff --git a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML @@ -1,643 +1,644 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich *) structure Mirabelle_Sledgehammer : MIRABELLE_ACTION = struct (*To facilitate synching the description of Mirabelle Sledgehammer parameters (in ../lib/Tools/mirabelle) with the parameters actually used by this interface, the former extracts PARAMETER and DESCRIPTION from code below which has this pattern (provided it appears in a single line): val .*K = "PARAMETER" (*DESCRIPTION*) *) +(* NOTE: Do not forget to update the Sledgehammer documentation to reflect changes here. *) val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*) val fact_filterK = "fact_filter" (*=STRING: fact filter*) val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*) val isar_proofsK = "isar_proofs" (*=SMART_BOOL: enable Isar proof generation*) val keepK = "keep" (*=PATH: path where to keep temporary files created by sledgehammer*) val lam_transK = "lam_trans" (*=STRING: lambda translation scheme*) val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*) val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*) val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*) val max_new_mono_instancesK = "max_new_mono_instances" (*=NUM: max. new monomorphic instances*) val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*) val minimizeK = "minimize" (*=BOOL: instruct sledgehammer to run its minimizer*) val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*) val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (ie. using metis/smt)*) val proverK = "prover" (*=STRING: name of the external prover to call*) val prover_timeoutK = "prover_timeout" (*=TIME: timeout for invoked ATP (seconds of process time)*) val sliceK = "slice" (*=BOOL: allow sledgehammer-level strategy-scheduling*) val smt_proofsK = "smt_proofs" (*=BOOL: enable SMT proof generation*) val strictK = "strict" (*=BOOL: run in strict mode*) val term_orderK = "term_order" (*=STRING: term order (in E)*) val type_encK = "type_enc" (*=STRING: type encoding scheme*) val uncurried_aliasesK = "uncurried_aliases" (*=SMART_BOOL: use fresh function names to alias curried applications*) fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " fun proof_method_tag meth id = "#" ^ string_of_int id ^ " " ^ (!meth) ^ " (sledgehammer): " val separator = "-----" (*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*) (*defaults used in this Mirabelle action*) val preplay_timeout_default = "1" val lam_trans_default = "smart" val uncurried_aliases_default = "smart" val fact_filter_default = "smart" val type_enc_default = "smart" val strict_default = "false" val max_facts_default = "smart" val slice_default = "true" val max_calls_default = "10000000" val trivial_default = "false" (*If a key is present in args then augment a list with its pair*) (*This is used to avoid fixing default values at the Mirabelle level, and instead use the default values of the tool (Sledgehammer in this case).*) fun available_parameter args key label list = let val value = AList.lookup (op =) args key in if is_some value then (label, the value) :: list else list end datatype sh_data = ShData of { calls: int, success: int, nontriv_calls: int, nontriv_success: int, lemmas: int, max_lems: int, time_isa: int, time_prover: int, time_prover_fail: int} datatype re_data = ReData of { calls: int, success: int, nontriv_calls: int, nontriv_success: int, proofs: int, time: int, timeout: int, lemmas: int * int * int, posns: (Position.T * bool) list } fun make_sh_data (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, time_prover,time_prover_fail) = ShData{calls=calls, success=success, nontriv_calls=nontriv_calls, nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, time_isa=time_isa, time_prover=time_prover, time_prover_fail=time_prover_fail} fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time, timeout,lemmas,posns) = ReData{calls=calls, success=success, nontriv_calls=nontriv_calls, nontriv_success=nontriv_success, proofs=proofs, time=time, timeout=timeout, lemmas=lemmas, posns=posns} val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0) val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), []) fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail}) = (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns) datatype data = Data of { sh: sh_data, re_u: re_data (* proof method with unminimized set of lemmas *) } fun make_data (sh, re_u) = Data {sh=sh, re_u=re_u} val empty_data = make_data (empty_sh_data, empty_re_data) fun map_sh_data f (Data {sh, re_u}) = let val sh' = make_sh_data (f (tuple_of_sh_data sh)) in make_data (sh', re_u) end fun map_re_data f (Data {sh, re_u}) = let val f' = make_re_data o f o tuple_of_re_data val re_u' = f' re_u in make_data (sh, re_u') end fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); val inc_sh_calls = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) val inc_sh_success = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) val inc_sh_nontriv_calls = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) val inc_sh_nontriv_success = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) fun inc_sh_lemmas n = map_sh_data (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail)) fun inc_sh_max_lems n = map_sh_data (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail)) fun inc_sh_time_isa t = map_sh_data (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail)) fun inc_sh_time_prover t = map_sh_data (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail)) fun inc_sh_time_prover_fail t = map_sh_data (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t)) val inc_proof_method_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) val inc_proof_method_success = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) val inc_proof_method_nontriv_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns)) val inc_proof_method_nontriv_success = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns)) val inc_proof_method_proofs = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns)) fun inc_proof_method_time t = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) val inc_proof_method_timeout = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns)) fun inc_proof_method_lemmas n = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) fun inc_proof_method_posns pos = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) val str0 = string_of_int o the_default 0 local val str = string_of_int val str3 = Real.fmt (StringCvt.FIX (SOME 3)) fun percentage a b = string_of_int (a * 100 div b) fun time t = Real.fromInt t / 1000.0 fun avg_time t n = if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 fun log_sh_data log (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) = (log ("Total number of sledgehammer calls: " ^ str calls); log ("Number of successful sledgehammer calls: " ^ str success); log ("Number of sledgehammer lemmas: " ^ str lemmas); log ("Max number of sledgehammer lemmas: " ^ str max_lems); log ("Success rate: " ^ percentage success calls ^ "%"); log ("Total number of nontrivial sledgehammer calls: " ^ str nontriv_calls); log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success); log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa)); log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover)); log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail)); log ("Average time for sledgehammer calls (Isabelle): " ^ str3 (avg_time time_isa calls)); log ("Average time for successful sledgehammer calls (ATP): " ^ str3 (avg_time time_prover success)); log ("Average time for failed sledgehammer calls (ATP): " ^ str3 (avg_time time_prover_fail (calls - success))) ) fun str_of_pos (pos, triv) = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^ (if triv then "[T]" else "") fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls, re_nontriv_success, re_proofs, re_time, re_timeout, (lemmas, lems_sos, lems_max), re_posns) = (log ("Total number of " ^ tag ^ "proof method calls: " ^ str re_calls); log ("Number of successful " ^ tag ^ "proof method calls: " ^ str re_success ^ " (proof: " ^ str re_proofs ^ ")"); log ("Number of " ^ tag ^ "proof method timeouts: " ^ str re_timeout); log ("Success rate: " ^ percentage re_success sh_calls ^ "%"); log ("Total number of nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_calls); log ("Number of successful nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_success ^ " (proof: " ^ str re_proofs ^ ")"); log ("Number of successful " ^ tag ^ "proof method lemmas: " ^ str lemmas); log ("SOS of successful " ^ tag ^ "proof method lemmas: " ^ str lems_sos); log ("Max number of successful " ^ tag ^ "proof method lemmas: " ^ str lems_max); log ("Total time for successful " ^ tag ^ "proof method calls: " ^ str3 (time re_time)); log ("Average time for successful " ^ tag ^ "proof method calls: " ^ str3 (avg_time re_time re_success)); if tag="" then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns)) else () ) in fun log_data id log (Data {sh, re_u}) = let val ShData {calls=sh_calls, ...} = sh fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else () fun log_re tag m = log_re_data log tag sh_calls (tuple_of_re_data m) fun log_proof_method (tag1, m1) = app_if m1 (fn () => (log_re tag1 m1; log "")) in if sh_calls > 0 then (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n"); log_sh_data log (tuple_of_sh_data sh); log ""; log_proof_method ("", re_u)) else () end end (* Warning: we implicitly assume single-threaded execution here *) val data = Unsynchronized.ref ([] : (int * data) list) fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy) fun done id ({log, ...}: Mirabelle.done_args) = AList.lookup (op =) (!data) id |> Option.map (log_data id log) |> K () fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ()) fun get_prover_name thy args = let fun default_prover_name () = hd (#provers (Sledgehammer_Commands.default_params thy [])) handle List.Empty => error "No ATP available" in (case AList.lookup (op =) args proverK of SOME name => name | NONE => default_prover_name ()) end fun get_prover ctxt name params goal = let val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (Thm.prop_of goal) in Sledgehammer_Prover_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal learn name end type stature = ATP_Problem_Generate.stature fun is_good_line s = (String.isSubstring " ms)" s orelse String.isSubstring " s)" s) andalso not (String.isSubstring "(> " s) andalso not (String.isSubstring ", > " s) andalso not (String.isSubstring "may fail" s) (* Fragile hack *) fun proof_method_from_msg args msg = (case AList.lookup (op =) args proof_methodK of SOME name => if name = "smart" then if exists is_good_line (split_lines msg) then "none" else "fail" else name | NONE => if exists is_good_line (split_lines msg) then "none" (* trust the preplayed proof *) else if String.isSubstring "metis (" msg then msg |> Substring.full |> Substring.position "metis (" |> snd |> Substring.position ")" |> fst |> Substring.string |> suffix ")" else if String.isSubstring "metis" msg then "metis" else "smt") local datatype sh_result = SH_OK of int * int * (string * stature) list | SH_FAIL of int * int | SH_ERROR fun run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans uncurried_aliases e_selection_heuristic term_order force_sos hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st = let val thy = Proof.theory_of st val {context = ctxt, facts = chained_ths, goal} = Proof.goal st val i = 1 fun set_file_name (SOME dir) = Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix ("prob_" ^ str0 (Position.line_of pos) ^ "__") #> Config.put SMT_Config.debug_files (dir ^ "/" ^ Name.desymbolize (SOME false) (ATP_Util.timestamp ()) ^ "_" ^ serial_string ()) | set_file_name NONE = I val st' = st |> Proof.map_context (set_file_name dir #> (Option.map (Config.put ATP_Systems.e_selection_heuristic) e_selection_heuristic |> the_default I) #> (Option.map (Config.put ATP_Systems.term_order) term_order |> the_default I) #> (Option.map (Config.put ATP_Systems.force_sos) force_sos |> the_default I)) val params as {max_facts, minimize, preplay_timeout, ...} = Sledgehammer_Commands.default_params thy ([(* ("verbose", "true"), *) ("fact_filter", fact_filter), ("type_enc", type_enc), ("strict", strict), ("lam_trans", lam_trans |> the_default lam_trans_default), ("uncurried_aliases", uncurried_aliases |> the_default uncurried_aliases_default), ("max_facts", max_facts), ("slice", slice), ("timeout", string_of_int timeout), ("preplay_timeout", preplay_timeout)] |> isar_proofsLST |> smt_proofsLST |> minimizeLST (*don't confuse the two minimization flags*) |> max_new_mono_instancesLST |> max_mono_itersLST) val default_max_facts = Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt val time_limit = (case hard_timeout of NONE => I | SOME secs => Timeout.apply (Time.fromSeconds secs)) fun failed failure = ({outcome = SOME failure, used_facts = [], used_from = [], preferred_methss = (Sledgehammer_Proof_Methods.Auto_Method, []), run_time = Time.zeroTime, message = K ""}, ~1) val ({outcome, used_facts, preferred_methss, run_time, message, ...} : Sledgehammer_Prover.prover_result, time_isa) = time_limit (Mirabelle.cpu_time (fn () => let val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover_name val keywords = Thy_Header.get_keywords' ctxt val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val facts = Sledgehammer_Fact.nearly_all_facts ctxt ho_atp Sledgehammer_Fact.no_fact_override keywords css_table chained_ths hyp_ts concl_t val factss = facts |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name (the_default default_max_facts max_facts) Sledgehammer_Fact.no_fact_override hyp_ts concl_t |> tap (fn factss => "Line " ^ str0 (Position.line_of pos) ^ ": " ^ Sledgehammer.string_of_factss factss |> writeln) val prover = get_prover ctxt prover_name params goal val problem = {comment = "", state = st', goal = goal, subgoal = i, subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss, found_proof = I} in prover params problem end)) () handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut | Fail "inappropriate" => failed ATP_Proof.Inappropriate val time_prover = run_time |> Time.toMilliseconds val msg = message (fn () => Sledgehammer.play_one_line_proof minimize preplay_timeout used_facts st' i preferred_methss) in (case outcome of NONE => (msg, SH_OK (time_isa, time_prover, used_facts)) | SOME _ => (msg, SH_FAIL (time_isa, time_prover))) end handle ERROR msg => ("error: " ^ msg, SH_ERROR) in fun run_sledgehammer trivial args proof_method named_thms id ({pre=st, log, pos, ...}: Mirabelle.run_args) = let val thy = Proof.theory_of st val triv_str = if trivial then "[T] " else "" val _ = change_data id inc_sh_calls val _ = if trivial then () else change_data id inc_sh_nontriv_calls val prover_name = get_prover_name thy args val fact_filter = AList.lookup (op =) args fact_filterK |> the_default fact_filter_default val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default val strict = AList.lookup (op =) args strictK |> the_default strict_default val max_facts = (case AList.lookup (op =) args max_factsK of SOME max => max | NONE => (case AList.lookup (op =) args max_relevantK of SOME max => max | NONE => max_facts_default)) val slice = AList.lookup (op =) args sliceK |> the_default slice_default val lam_trans = AList.lookup (op =) args lam_transK val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK val term_order = AList.lookup (op =) args term_orderK val force_sos = AList.lookup (op =) args force_sosK |> Option.map (curry (op <>) "false") val dir = AList.lookup (op =) args keepK val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) (* always use a hard timeout, but give some slack so that the automatic minimizer has a chance to do its magic *) val preplay_timeout = AList.lookup (op =) args preplay_timeoutK |> the_default preplay_timeout_default val isar_proofsLST = available_parameter args isar_proofsK "isar_proofs" val smt_proofsLST = available_parameter args smt_proofsK "smt_proofs" val minimizeLST = available_parameter args minimizeK "minimize" val max_new_mono_instancesLST = available_parameter args max_new_mono_instancesK max_new_mono_instancesK val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK val hard_timeout = SOME (4 * timeout) val (msg, result) = run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans uncurried_aliases e_selection_heuristic term_order force_sos hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st in (case result of SH_OK (time_isa, time_prover, names) => let fun get_thms (name, stature) = try (Sledgehammer_Util.thms_of_name (Proof.context_of st)) name |> Option.map (pair (name, stature)) in change_data id inc_sh_success; if trivial then () else change_data id inc_sh_nontriv_success; change_data id (inc_sh_lemmas (length names)); change_data id (inc_sh_max_lems (length names)); change_data id (inc_sh_time_isa time_isa); change_data id (inc_sh_time_prover time_prover); proof_method := proof_method_from_msg args msg; named_thms := SOME (map_filter get_thms names); log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg) end | SH_FAIL (time_isa, time_prover) => let val _ = change_data id (inc_sh_time_isa time_isa) val _ = change_data id (inc_sh_time_prover_fail time_prover) in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)) end end fun override_params prover type_enc timeout = [("provers", prover), ("max_facts", "0"), ("type_enc", type_enc), ("strict", "true"), ("slice", "false"), ("timeout", timeout |> Time.toSeconds |> string_of_int)] fun run_proof_method trivial full name meth named_thms id ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = let fun do_method named_thms ctxt = let val ref_of_str = (* FIXME proper wrapper for parser combinators *) suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none #> Parse.thm #> fst val thms = named_thms |> maps snd val facts = named_thms |> map (ref_of_str o fst o fst) val fact_override = {add = facts, del = [], only = true} fun my_timeout time_slice = timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal fun sledge_tac time_slice prover type_enc = Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt (override_params prover type_enc (my_timeout time_slice)) fact_override [] in if !meth = "sledgehammer_tac" then sledge_tac 0.2 ATP_Proof.vampireN "mono_native" ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??" ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native" ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??" ORELSE' SMT_Solver.smt_tac ctxt thms else if !meth = "smt" then SMT_Solver.smt_tac ctxt thms else if full then Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms else if String.isPrefix "metis (" (!meth) then let val (type_encs, lam_trans) = !meth |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start |> filter Token.is_proper |> tl |> Metis_Tactic.parse_metis_options |> fst |>> the_default [ATP_Proof_Reconstruct.partial_typesN] ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end else if !meth = "metis" then Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms else if !meth = "none" then K all_tac else if !meth = "fail" then K no_tac else (warning ("Unknown method " ^ quote (!meth)); K no_tac) end fun apply_method named_thms = Mirabelle.can_apply timeout (do_method named_thms) st fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" | with_time (true, t) = (change_data id inc_proof_method_success; if trivial then () else change_data id inc_proof_method_nontriv_success; change_data id (inc_proof_method_lemmas (length named_thms)); change_data id (inc_proof_method_time t); change_data id (inc_proof_method_posns (pos, trivial)); if name = "proof" then change_data id inc_proof_method_proofs else (); "succeeded (" ^ string_of_int t ^ ")") fun timed_method named_thms = (with_time (Mirabelle.cpu_time apply_method named_thms), true) handle Timeout.TIMEOUT _ => (change_data id inc_proof_method_timeout; ("timeout", false)) | ERROR msg => ("error: " ^ msg, false) val _ = log separator val _ = change_data id inc_proof_method_calls val _ = if trivial then () else change_data id inc_proof_method_nontriv_calls in named_thms |> timed_method |>> log o prefix (proof_method_tag meth id) |> snd end val try_timeout = seconds 5.0 (* crude hack *) val num_sledgehammer_calls = Unsynchronized.ref 0 fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) = let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then () else let val max_calls = AList.lookup (op =) args max_callsK |> the_default max_calls_default |> Int.fromString |> the val _ = num_sledgehammer_calls := !num_sledgehammer_calls + 1; in if !num_sledgehammer_calls > max_calls then () else let val meth = Unsynchronized.ref "" val named_thms = Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) val trivial = if AList.lookup (op =) args check_trivialK |> the_default trivial_default |> Value.parse_bool then Try0.try0 (SOME try_timeout) ([], [], [], []) pre handle Timeout.TIMEOUT _ => false else false fun apply_method () = (Mirabelle.catch_result (proof_method_tag meth) false (run_proof_method trivial false name meth (these (!named_thms))) id st; ()) in Mirabelle.catch sh_tag (run_sledgehammer trivial args meth named_thms) id st; if is_some (!named_thms) then apply_method () else () end end end fun invoke args = Mirabelle.register (init, sledgehammer_action args, done) end diff --git a/src/HOL/Mirabelle/lib/Tools/mirabelle b/src/HOL/Mirabelle/lib/Tools/mirabelle --- a/src/HOL/Mirabelle/lib/Tools/mirabelle +++ b/src/HOL/Mirabelle/lib/Tools/mirabelle @@ -1,136 +1,136 @@ #!/usr/bin/env bash # # Author: Sascha Boehme # # DESCRIPTION: testing tool for automated proof tools PRG="$(basename "$0")" function print_action_names() { for TOOL in "$MIRABELLE_HOME/Tools"/mirabelle_*.ML do echo "$TOOL" | perl -w -p -e 's/.*mirabelle_(.*)\.ML/ $1/' done } function print_sledgehammer_options() { grep -e "^val .*K =" "$MIRABELLE_HOME/Tools/mirabelle_sledgehammer.ML" | \ perl -w -p -e 's/val .*K *= *"(.*)" *\(\*(.*)\*\)/ $1$2/' } function usage() { + # Do not forget to update the Sledgehammer documentation to reflect changes here. [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None" timeout="$MIRABELLE_TIMEOUT" echo echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES" echo echo " Options are:" echo " -L LOGIC parent logic to use (default $MIRABELLE_LOGIC)" echo " -O DIR output directory for test data (default $out)" echo " -S FILE user-provided setup file (no actions required)" echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)" echo " -d DIR include session directory" echo " -q be quiet (suppress output of Isabelle process)" echo " -t TIMEOUT timeout for each action in seconds (default $timeout)" echo - echo " Apply the given actions (i.e., automated proof tools)" - echo " at all proof steps in the given theory files." + echo " Apply the given actions at all proof steps in the given theory files." echo echo " ACTIONS is a colon-separated list of actions, where each action is" echo " either NAME or NAME[OPTION,...,OPTION]. Available actions are:" print_action_names echo echo " Available OPTIONs for the ACTION sledgehammer:" print_sledgehammer_options echo echo " FILES is a list of theory files, where each file is either NAME.thy" echo " or NAME.thy[START:END] and START and END are numbers indicating the" echo " range the given actions are to be applied." echo exit 1 } function fail() { echo "$1" >&2 exit 2 } ## process command line # options [ $# -eq 0 ] && usage MIRABELLE_DIR= MIRABELLE_SETUP_FILE= while getopts "L:T:O:d:t:S:q?" OPT do case "$OPT" in L) MIRABELLE_LOGIC="$OPTARG" ;; T) MIRABELLE_THEORY="$OPTARG" ;; O) MIRABELLE_OUTPUT_PATH="$OPTARG" ;; d) MIRABELLE_DIR="$OPTARG" ;; t) MIRABELLE_TIMEOUT="$OPTARG" ;; S) MIRABELLE_SETUP_FILE="$OPTARG" ;; q) MIRABELLE_QUIET="true" ;; \?) usage ;; esac done export MIRABELLE_DIR export MIRABELLE_SETUP_FILE export MIRABELLE_QUIET shift $(($OPTIND - 1)) export MIRABELLE_ACTIONS="$1" shift # setup if [ -z "$MIRABELLE_OUTPUT_PATH" ]; then MIRABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mirabelle$$" PURGE_OUTPUT="true" fi mkdir -p "$MIRABELLE_OUTPUT_PATH" export MIRABELLE_OUTPUT_PATH ## main for FILE in "$@" do perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" || fail "Mirabelle failed." done ## cleanup if [ -n "$PURGE_OUTPUT" ]; then rm -rf "$MIRABELLE_OUTPUT_PATH" fi diff --git a/src/HOL/Sledgehammer.thy b/src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy +++ b/src/HOL/Sledgehammer.thy @@ -1,39 +1,39 @@ (* Title: HOL/Sledgehammer.thy Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Jia Meng, Cambridge University Computer Laboratory and NICTA Author: Jasmin Blanchette, TU Muenchen *) section \Sledgehammer: Isabelle--ATP Linkup\ theory Sledgehammer imports Presburger SMT keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl begin lemma size_ne_size_imp_ne: "size x \ size y \ x \ y" by (erule contrapos_nn) (rule arg_cong) -ML_file \Tools/ATP/atp_systems.ML\ +ML_file \Tools/ATP/atp_systems.ML\ (* TODO: rename and move to Tools/Sledgehammer *) ML_file \Tools/Sledgehammer/async_manager_legacy.ML\ ML_file \Tools/Sledgehammer/sledgehammer_util.ML\ ML_file \Tools/Sledgehammer/sledgehammer_fact.ML\ ML_file \Tools/Sledgehammer/sledgehammer_proof_methods.ML\ ML_file \Tools/Sledgehammer/sledgehammer_isar_annotate.ML\ ML_file \Tools/Sledgehammer/sledgehammer_isar_proof.ML\ ML_file \Tools/Sledgehammer/sledgehammer_isar_preplay.ML\ ML_file \Tools/Sledgehammer/sledgehammer_isar_compress.ML\ ML_file \Tools/Sledgehammer/sledgehammer_isar_minimize.ML\ ML_file \Tools/Sledgehammer/sledgehammer_isar.ML\ ML_file \Tools/Sledgehammer/sledgehammer_prover.ML\ ML_file \Tools/Sledgehammer/sledgehammer_prover_atp.ML\ ML_file \Tools/Sledgehammer/sledgehammer_prover_smt.ML\ ML_file \Tools/Sledgehammer/sledgehammer_prover_minimize.ML\ ML_file \Tools/Sledgehammer/sledgehammer_mepo.ML\ ML_file \Tools/Sledgehammer/sledgehammer_mash.ML\ ML_file \Tools/Sledgehammer/sledgehammer.ML\ ML_file \Tools/Sledgehammer/sledgehammer_commands.ML\ end diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML @@ -1,567 +1,567 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_fact.ML Author: Jia Meng, Cambridge University Computer Laboratory and NICTA Author: Jasmin Blanchette, TU Muenchen Sledgehammer fact handling. *) signature SLEDGEHAMMER_FACT = sig type status = ATP_Problem_Generate.status type stature = ATP_Problem_Generate.stature - type raw_fact = ((unit -> string) * stature) * thm + type raw_fact = ((unit -> string) * stature) * thm (* TODO: rename to lazy_fact *) type fact = (string * stature) * thm type fact_override = {add : (Facts.ref * Token.src list) list, del : (Facts.ref * Token.src list) list, only : bool} val instantiate_inducts : bool Config.T val no_fact_override : fact_override val fact_of_ref : Proof.context -> Keyword.keywords -> thm list -> status Termtab.table -> Facts.ref * Token.src list -> ((string * stature) * thm) list val cartouche_thm : Proof.context -> thm -> string val is_blacklisted_or_something : Proof.context -> bool -> string -> bool val clasimpset_rule_table_of : Proof.context -> status Termtab.table val build_name_tables : (thm -> string) -> ('a * thm) list -> string Symtab.table * string Symtab.table val fact_distinct : (term * term -> bool) -> ('a * thm) list -> ('a * thm) list val maybe_instantiate_inducts : Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list -> (((unit -> string) * 'a) * thm) list val fact_of_raw_fact : raw_fact -> fact val is_useful_unnamed_local_fact : Proof.context -> thm -> bool val all_facts : Proof.context -> bool -> bool -> Keyword.keywords -> thm list -> thm list -> status Termtab.table -> raw_fact list val nearly_all_facts : Proof.context -> bool -> fact_override -> Keyword.keywords -> status Termtab.table -> thm list -> term list -> term -> raw_fact list val drop_duplicate_facts : raw_fact list -> raw_fact list end; structure Sledgehammer_Fact : SLEDGEHAMMER_FACT = struct open ATP_Util open ATP_Problem_Generate open Sledgehammer_Util type raw_fact = ((unit -> string) * stature) * thm type fact = (string * stature) * thm type fact_override = {add : (Facts.ref * Token.src list) list, del : (Facts.ref * Token.src list) list, only : bool} val local_thisN = Long_Name.localN ^ Long_Name.separator ^ Auto_Bind.thisN (* gracefully handle huge background theories *) val max_facts_for_duplicates = 50000 val max_facts_for_complex_check = 25000 val max_simps_for_clasimpset = 10000 (* experimental feature *) val instantiate_inducts = Attrib.setup_config_bool \<^binding>\sledgehammer_instantiate_inducts\ (K false) val no_fact_override = {add = [], del = [], only = false} fun needs_quoting keywords s = Keyword.is_literal keywords s orelse exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s) fun make_name keywords multi j name = (name |> needs_quoting keywords name ? quote) ^ (if multi then "(" ^ string_of_int j ^ ")" else "") fun explode_interval _ (Facts.FromTo (i, j)) = i upto j | explode_interval max (Facts.From i) = i upto i + max - 1 | explode_interval _ (Facts.Single i) = [i] fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs)) fun is_rec_def (\<^const>\Trueprop\ $ t) = is_rec_def t | is_rec_def (\<^const>\Pure.imp\ $ _ $ t2) = is_rec_def t2 | is_rec_def (Const (\<^const_name>\Pure.eq\, _) $ t1 $ t2) = is_rec_eq t1 t2 | is_rec_def (Const (\<^const_name>\HOL.eq\, _) $ t1 $ t2) = is_rec_eq t1 t2 | is_rec_def _ = false fun is_assum assms th = exists (fn ct => Thm.prop_of th aconv Thm.term_of ct) assms fun is_chained chained = member Thm.eq_thm_prop chained fun scope_of_thm global assms chained th = if is_chained chained th then Chained else if global then Global else if is_assum assms th then Assum else Local val may_be_induction = exists_subterm (fn Var (_, Type (\<^type_name>\fun\, [_, T])) => body_type T = \<^typ>\bool\ | _ => false) (* TODO: get rid of *) fun normalize_vars t = let fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s | normT (TVar (z as (_, S))) = (fn ((knownT, nT), accum) => (case find_index (equal z) knownT of ~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum)) | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum)))) | normT (T as TFree _) = pair T fun norm (t $ u) = norm t ##>> norm u #>> op $ | norm (Const (s, T)) = normT T #>> curry Const s | norm (Var (z as (_, T))) = normT T #> (fn (T, (accumT, (known, n))) => (case find_index (equal z) known of ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1))) | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n))))) | norm (Abs (_, T, t)) = norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t)) | norm (Bound j) = pair (Bound j) | norm (Free (s, T)) = normT T #>> curry Free s in fst (norm t (([], 0), ([], 0))) end fun status_of_thm css name th = if Termtab.is_empty css then General else let val t = Thm.prop_of th in (* FIXME: use structured name *) if String.isSubstring ".induct" name andalso may_be_induction t then Induction else let val t = normalize_vars t in (case Termtab.lookup css t of SOME status => status | NONE => let val concl = Logic.strip_imp_concl t in (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of SOME lrhss => let val prems = Logic.strip_imp_prems t val t' = Logic.list_implies (prems, Logic.mk_equals lrhss) in Termtab.lookup css t' |> the_default General end | NONE => General) end) end end fun stature_of_thm global assms chained css name th = (scope_of_thm global assms chained th, status_of_thm css name th) fun fact_of_ref ctxt keywords chained css (xthm as (xref, args)) = let val ths = Attrib.eval_thms ctxt [xthm] val bracket = implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src ctxt) args) fun nth_name j = (case xref of Facts.Fact s => cartouche (simplify_spaces (YXML.content_of s)) ^ bracket | Facts.Named (("", _), _) => "[" ^ bracket ^ "]" | Facts.Named ((name, _), NONE) => make_name keywords (length ths > 1) (j + 1) name ^ bracket | Facts.Named ((name, _), SOME intervals) => make_name keywords true (nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket) fun add_nth th (j, rest) = let val name = nth_name j in (j + 1, ((name, stature_of_thm false [] chained css name th), th) :: rest) end in (0, []) |> fold add_nth ths |> snd end (* Reject theorems with names like "List.filter.filter_list_def" or "Accessible_Part.acc.defs", as these are definitions arising from packages. *) fun is_package_def s = let val ss = Long_Name.explode s in length ss > 2 andalso not (hd ss = "local") andalso exists (fn suf => String.isSuffix suf s) ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"] end (* FIXME: put other record thms here, or declare as "no_atp" *) fun multi_base_blacklist ctxt ho_atp = ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", "case_cong_weak", "nat_of_char_simps", "nibble.simps", "nibble.distinct"] |> not (ho_atp orelse Config.get ctxt instantiate_inducts) ? append ["induct", "inducts"] |> map (prefix Long_Name.separator) (* The maximum apply depth of any "metis" call in "Metis_Examples" (back in 2007) was 11. *) val max_apply_depth = 18 fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1) | apply_depth (Abs (_, _, t)) = apply_depth t | apply_depth _ = 0 fun is_too_complex t = apply_depth t > max_apply_depth (* FIXME: Ad hoc list *) val technical_prefixes = ["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence", "Limited_Sequence", "Meson", "Metis", "Nitpick", "Quickcheck_Random", "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "Sledgehammer", "SMT"] |> map (suffix Long_Name.separator) fun is_technical_const s = exists (fn pref => String.isPrefix pref s) technical_prefixes (* FIXME: make more reliable *) val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator fun is_low_level_class_const s = s = \<^const_name>\equal_class.equal\ orelse String.isSubstring sep_class_sep s val sep_that = Long_Name.separator ^ Auto_Bind.thatN val skolem_thesis = Name.skolem Auto_Bind.thesisN fun is_that_fact th = exists_subterm (fn Free (s, _) => s = skolem_thesis | _ => false) (Thm.prop_of th) andalso String.isSuffix sep_that (Thm.get_name_hint th) datatype interest = Deal_Breaker | Interesting | Boring fun combine_interests Deal_Breaker _ = Deal_Breaker | combine_interests _ Deal_Breaker = Deal_Breaker | combine_interests Interesting _ = Interesting | combine_interests _ Interesting = Interesting | combine_interests Boring Boring = Boring val type_has_top_sort = exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) fun is_likely_tautology_too_meta_or_too_technical th = let fun is_interesting_subterm (Const (s, _)) = not (member (op =) atp_widely_irrelevant_consts s) | is_interesting_subterm (Free _) = true | is_interesting_subterm _ = false fun interest_of_bool t = if exists_Const ((is_technical_const o fst) orf (is_low_level_class_const o fst) orf type_has_top_sort o snd) t then Deal_Breaker else if exists_type (exists_subtype (curry (op =) \<^typ>\prop\)) t orelse not (exists_subterm is_interesting_subterm t) then Boring else Interesting fun interest_of_prop _ (\<^const>\Trueprop\ $ t) = interest_of_bool t | interest_of_prop Ts (\<^const>\Pure.imp\ $ t $ u) = combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u) | interest_of_prop Ts (Const (\<^const_name>\Pure.all\, _) $ Abs (_, T, t)) = if type_has_top_sort T then Deal_Breaker else interest_of_prop (T :: Ts) t | interest_of_prop Ts ((t as Const (\<^const_name>\Pure.all\, _)) $ u) = interest_of_prop Ts (t $ eta_expand Ts u 1) | interest_of_prop _ (Const (\<^const_name>\Pure.eq\, _) $ t $ u) = combine_interests (interest_of_bool t) (interest_of_bool u) | interest_of_prop _ _ = Deal_Breaker val t = Thm.prop_of th in (interest_of_prop [] t <> Interesting andalso not (Thm.eq_thm_prop (@{thm ext}, th))) orelse is_that_fact th end fun is_blacklisted_or_something ctxt ho_atp = let val blist = multi_base_blacklist ctxt ho_atp in fn name => is_package_def name orelse exists (fn s => String.isSuffix s name) blist end (* This is a terrible hack. Free variables are sometimes coded as "M__" when they are displayed as "M" and we want to avoid clashes with these. But sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all prefixes of all free variables. In the worse case scenario, where the fact won't be resolved correctly, the user can fix it manually, e.g., by giving a name to the offending fact. *) fun all_prefixes_of s = map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1) fun close_form t = (t, [] |> Term.add_free_names t |> maps all_prefixes_of) |> fold (fn ((s, i), T) => fn (t', taken) => let val s' = singleton (Name.variant_list taken) s in ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const else Logic.all_const) T $ Abs (s', T, abstract_over (Var ((s, i), T), t')), s' :: taken) end) (Term.add_vars t [] |> sort_by (fst o fst)) |> fst fun cartouche_term ctxt = close_form #> hackish_string_of_term ctxt #> cartouche fun cartouche_thm ctxt = cartouche_term ctxt o Thm.prop_of (* TODO: rewrite to use nets and/or to reuse existing data structures *) fun clasimpset_rule_table_of ctxt = let val simps = ctxt |> simpset_of |> dest_ss |> #simps in if length simps >= max_simps_for_clasimpset then Termtab.empty else let fun add stature th = Termtab.update (normalize_vars (Thm.prop_of th), stature) val {safeIs, (* safeEs, *) unsafeIs, (* unsafeEs, *) ...} = ctxt |> claset_of |> Classical.rep_cs val intros = map #1 (Item_Net.content safeIs @ Item_Net.content unsafeIs) (* Add once it is used: val elims = Item_Net.content safeEs @ Item_Net.content unsafeEs |> map Classical.classical_rule *) val specs = Spec_Rules.get ctxt val (rec_defs, nonrec_defs) = specs |> filter (Spec_Rules.is_equational o #rough_classification) |> maps #rules |> List.partition (is_rec_def o Thm.prop_of) val spec_intros = specs |> filter (Spec_Rules.is_relational o #rough_classification) |> maps #rules in Termtab.empty |> fold (add Simp o snd) simps |> fold (add Rec_Def) rec_defs |> fold (add Non_Rec_Def) nonrec_defs (* Add once it is used: |> fold (add Elim) elims *) |> fold (add Intro) intros |> fold (add Inductive) spec_intros end end fun normalize_eq (\<^const>\Trueprop\ $ (t as (t0 as Const (\<^const_name>\HOL.eq\, _)) $ t1 $ t2)) = if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else t0 $ t2 $ t1 | normalize_eq (\<^const>\Trueprop\ $ (t as \<^const>\Not\ $ ((t0 as Const (\<^const_name>\HOL.eq\, _)) $ t1 $ t2))) = if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else HOLogic.mk_not (t0 $ t2 $ t1) | normalize_eq (Const (\<^const_name>\Pure.eq\, Type (_, [T, _])) $ t1 $ t2) = (if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then (t1, t2) else (t2, t1)) |> (fn (t1, t2) => HOLogic.eq_const T $ t1 $ t2) | normalize_eq t = t fun if_thm_before th th' = if Context.subthy_id (apply2 Thm.theory_id (th, th')) then th else th' (* Hack: Conflate the facts about a class as seen from the outside with the corresponding low-level facts, so that MaSh can learn from the low-level proofs. *) fun un_class_ify s = (case first_field "_class" s of SOME (pref, suf) => [s, pref ^ suf] | NONE => [s]) fun build_name_tables name_of facts = let fun cons_thm (_, th) = Termtab.cons_list (normalize_vars (normalize_eq (Thm.prop_of th)), th) fun add_plain canon alias = Symtab.update (Thm.get_name_hint alias, name_of (if_thm_before canon alias)) fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases fun add_inclass (name, target) = fold (fn s => Symtab.update (s, target)) (un_class_ify name) val prop_tab = fold cons_thm facts Termtab.empty val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty in (plain_name_tab, inclass_name_tab) end fun fact_distinct eq facts = fold (fn (i, fact as (_, th)) => Net.insert_term_safe (eq o apply2 (normalize_eq o Thm.prop_of o snd o snd)) (normalize_eq (Thm.prop_of th), (i, fact))) (tag_list 0 facts) Net.empty |> Net.entries |> sort (int_ord o apply2 fst) |> map snd fun struct_induct_rule_on th = (case Logic.strip_horn (Thm.prop_of th) of (prems, \<^const>\Trueprop\ $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) => if not (is_TVar ind_T) andalso length prems > 1 andalso exists (exists_subterm (curry (op aconv) p)) prems andalso not (exists (exists_subterm (curry (op aconv) a)) prems) then SOME (p_name, ind_T) else NONE | _ => NONE) val instantiate_induct_timeout = seconds 0.01 fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x = let fun varify_noninducts (t as Free (s, T)) = if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T) | varify_noninducts t = t val p_inst = concl_prop |> map_aterms varify_noninducts |> close_form |> lambda (Free ind_x) |> hackish_string_of_term ctxt in ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", stature), th |> Rule_Insts.read_instantiate ctxt [(((p_name, 0), Position.none), p_inst)] []) end fun type_match thy (T1, T2) = (Sign.typ_match thy (T2, T1) Vartab.empty; true) handle Type.TYPE_MATCH => false fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) = (case struct_induct_rule_on th of SOME (p_name, ind_T) => let val thy = Proof_Context.theory_of ctxt in stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T)) |> map_filter (try (Timeout.apply instantiate_induct_timeout (instantiate_induct_rule ctxt stmt p_name ax))) end | NONE => [ax]) fun external_frees t = [] |> Term.add_frees t |> filter_out (Name.is_internal o fst) fun maybe_instantiate_inducts ctxt hyp_ts concl_t = if Config.get ctxt instantiate_inducts then let val ind_stmt = (hyp_ts |> filter_out (null o external_frees), concl_t) |> Logic.list_implies |> Object_Logic.atomize_term ctxt val ind_stmt_xs = external_frees ind_stmt in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end else I fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th) fun fact_count facts = Facts.fold_static (K (Integer.add 1)) facts 0 fun is_useful_unnamed_local_fact ctxt = let val thy = Proof_Context.theory_of ctxt val global_facts = Global_Theory.facts_of thy val local_facts = Proof_Context.facts_of ctxt val named_locals = Facts.dest_static true [global_facts] local_facts |> maps (map (normalize_eq o Thm.prop_of) o snd) in fn th => not (Thm.has_name_hint th) andalso not (member (op aconv) named_locals (normalize_eq (Thm.prop_of th))) end fun all_facts ctxt generous ho_atp keywords add_ths chained css = let val thy = Proof_Context.theory_of ctxt val transfer = Global_Theory.transfer_theories thy val global_facts = Global_Theory.facts_of thy val is_too_complex = if generous orelse fact_count global_facts >= max_facts_for_complex_check then K false else is_too_complex val local_facts = Proof_Context.facts_of ctxt val assms = Assumption.all_assms_of ctxt val named_locals = Facts.dest_static true [global_facts] local_facts val unnamed_locals = Facts.props local_facts |> map #1 |> filter (is_useful_unnamed_local_fact ctxt) |> map (pair "" o single) val full_space = Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp fun add_facts global foldx facts = foldx (fn (name0, ths) => fn accum => if name0 <> "" andalso (Long_Name.is_hidden (Facts.intern facts name0) orelse ((Facts.is_concealed facts name0 orelse (not generous andalso is_blacklisted_or_something name0)) andalso forall (not o member Thm.eq_thm_prop add_ths) ths)) then accum else let val n = length ths val multi = n > 1 fun check_thms a = (case try (Proof_Context.get_thms ctxt) a of NONE => false | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')) in snd (fold_rev (fn th0 => fn (j, accum) => let val th = transfer th0 in (j - 1, if not (member Thm.eq_thm_prop add_ths th) andalso (is_likely_tautology_too_meta_or_too_technical th orelse is_too_complex (Thm.prop_of th)) then accum else let fun get_name () = if name0 = "" orelse name0 = local_thisN then cartouche_thm ctxt th else let val short_name = Facts.extern ctxt facts name0 in if check_thms short_name then short_name else let val long_name = Name_Space.extern ctxt full_space name0 in if check_thms long_name then long_name else name0 end end |> make_name keywords multi j val stature = stature_of_thm global assms chained css name0 th val new = ((get_name, stature), th) in (if multi then apsnd else apfst) (cons new) accum end) end) ths (n, accum)) end) in (* The single-theorem names go before the multiple-theorem ones (e.g., "xxx" vs. "xxx(3)"), so that single names are preferred when both are available. *) ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals) |> add_facts true Facts.fold_static global_facts global_facts |> op @ end fun nearly_all_facts ctxt ho_atp {add, del, only} keywords css chained hyp_ts concl_t = if only andalso null add then [] else let val chained = chained |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th]) in (if only then maps (map (fn ((name, stature), th) => ((K name, stature), th)) o fact_of_ref ctxt keywords chained css) add else let val (add, del) = apply2 (Attrib.eval_thms ctxt) (add, del) val facts = all_facts ctxt false ho_atp keywords add chained css |> filter_out ((member Thm.eq_thm_prop del orf (Named_Theorems.member ctxt \<^named_theorems>\no_atp\ andf not o member Thm.eq_thm_prop add)) o snd) in facts end) |> maybe_instantiate_inducts ctxt hyp_ts concl_t end fun drop_duplicate_facts facts = let val num_facts = length facts in facts |> num_facts <= max_facts_for_duplicates ? fact_distinct (op aconv) end end;