blanchet@36918: \documentclass[a4paper,12pt]{article} blanchet@36918: \usepackage[T1]{fontenc} blanchet@36918: \usepackage{amsmath} blanchet@36918: \usepackage{amssymb} blanchet@36918: \usepackage[english,french]{babel} blanchet@36918: \usepackage{color} blanchet@36918: \usepackage{footmisc} blanchet@36918: \usepackage{graphicx} blanchet@36918: %\usepackage{mathpazo} blanchet@36918: \usepackage{multicol} blanchet@36918: \usepackage{stmaryrd} blanchet@36918: %\usepackage[scaled=.85]{beramono} wenzelm@43382: \usepackage{../../lib/texinputs/isabelle,../iman,../pdfsetup} blanchet@36918: blanchet@47113: \newcommand\download{\url{http://www21.in.tum.de/~blanchet/\#software}} blanchet@47113: blanchet@44057: \def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}} blanchet@44057: \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$} blanchet@44057: blanchet@46387: \newcommand\const[1]{\textsf{#1}} blanchet@46387: blanchet@36918: %\oddsidemargin=4.6mm blanchet@36918: %\evensidemargin=4.6mm blanchet@36918: %\textwidth=150mm blanchet@36918: %\topmargin=4.6mm blanchet@36918: %\headheight=0mm blanchet@36918: %\headsep=0mm blanchet@36918: %\textheight=234mm blanchet@36918: blanchet@36918: \def\Colon{\mathord{:\mkern-1.5mu:}} blanchet@36918: %\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}} blanchet@36918: %\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}} blanchet@36918: \def\lparr{\mathopen{(\mkern-4mu\mid}} blanchet@36918: \def\rparr{\mathclose{\mid\mkern-4mu)}} blanchet@36918: blanchet@36918: \def\unk{{?}} blanchet@36918: \def\undef{(\lambda x.\; \unk)} blanchet@36918: %\def\unr{\textit{others}} blanchet@36918: \def\unr{\ldots} blanchet@36918: \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}} blanchet@36918: \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}} blanchet@36918: blanchet@36918: \urlstyle{tt} blanchet@36918: blanchet@36918: \begin{document} blanchet@36918: blanchet@46387: %%% TYPESETTING blanchet@46387: %\renewcommand\labelitemi{$\bullet$} blanchet@46387: \renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}} blanchet@46387: blanchet@36918: \selectlanguage{english} blanchet@36918: blanchet@36918: \title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex] blanchet@36918: Hammering Away \\[\smallskipamount] blanchet@36918: \Large A User's Guide to Sledgehammer for Isabelle/HOL} blanchet@36918: \author{\hbox{} \\ blanchet@36918: Jasmin Christian Blanchette \\ blanchet@43843: {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\[4\smallskipamount] blanchet@43843: {\normalsize with contributions from} \\[4\smallskipamount] blanchet@43843: Lawrence C. Paulson \\ blanchet@43843: {\normalsize Computer Laboratory, University of Cambridge} \\ blanchet@36918: \hbox{}} blanchet@36918: blanchet@36918: \maketitle blanchet@36918: blanchet@36918: \tableofcontents blanchet@36918: blanchet@36918: \setlength{\parskip}{.7em plus .2em minus .1em} blanchet@36918: \setlength{\parindent}{0pt} blanchet@36918: \setlength{\abovedisplayskip}{\parskip} blanchet@36918: \setlength{\abovedisplayshortskip}{.9\parskip} blanchet@36918: \setlength{\belowdisplayskip}{\parskip} blanchet@36918: \setlength{\belowdisplayshortskip}{.9\parskip} blanchet@36918: blanchet@36918: % General-purpose enum environment with correct spacing blanchet@36918: \newenvironment{enum}% blanchet@36918: {\begin{list}{}{% blanchet@36918: \setlength{\topsep}{.1\parskip}% blanchet@36918: \setlength{\partopsep}{.1\parskip}% blanchet@36918: \setlength{\itemsep}{\parskip}% blanchet@36918: \advance\itemsep by-\parsep}} blanchet@36918: {\end{list}} blanchet@36918: blanchet@36918: \def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin blanchet@36918: \advance\rightskip by\leftmargin} blanchet@36918: \def\post{\vskip0pt plus1ex\endgroup} blanchet@36918: blanchet@36918: \def\prew{\pre\advance\rightskip by-\leftmargin} blanchet@36918: \def\postw{\post} blanchet@36918: blanchet@36918: \section{Introduction} blanchet@36918: \label{introduction} blanchet@36918: blanchet@43805: Sledgehammer is a tool that applies automatic theorem provers (ATPs) blanchet@48432: and satisfiability-modulo-theories (SMT) solvers on the current goal.% blanchet@48432: \footnote{The distinction between ATPs and SMT solvers is convenient but mostly blanchet@48432: historical. The two communities are converging, with more and more ATPs blanchet@48432: supporting typical SMT features such as arithemtic and sorts, and a few SMT blanchet@48432: solvers parsing ATP syntaxes. There is also a strong technological connection blanchet@48432: between instantiation-based ATPs (such as iProver and iProver-Eq) and SMT blanchet@48432: solvers.} blanchet@48432: % blanchet@48432: The supported ATPs are E \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF blanchet@48432: \cite{tofof}, iProver \cite{korovin-2009}, iProver-Eq blanchet@48432: \cite{korovin-sticksel-2010}, LEO-II \cite{leo2}, Satallax \cite{satallax}, blanchet@48432: SNARK \cite{snark}, SPASS \cite{weidenbach-et-al-2009}, Vampire blanchet@48432: \cite{riazanov-voronkov-2002}, and Waldmeister \cite{waldmeister}. The ATPs are blanchet@48432: run either locally or remotely via the System\-On\-TPTP web service blanchet@48432: \cite{sutcliffe-2000}. In addition to the ATPs, the SMT solvers Z3 \cite{z3} is blanchet@48432: used by default, and you can tell Sledgehammer to try Alt-Ergo \cite{alt-ergo}, blanchet@48432: CVC3 \cite{cvc3}, and Yices \cite{yices} as well; these are run either locally blanchet@48432: or (for CVC3 and Z3) on a server at the TU M\"unchen. blanchet@36918: blanchet@40254: The problem passed to the automatic provers consists of your current goal blanchet@40254: together with a heuristic selection of hundreds of facts (theorems) from the blanchet@40254: current theory context, filtered by relevance. Because jobs are run in the blanchet@40254: background, you can continue to work on your proof by other means. Provers can blanchet@40254: be run in parallel. Any reply (which may arrive half a minute later) will appear blanchet@40254: in the Proof General response buffer. blanchet@37517: blanchet@40254: The result of a successful proof search is some source text that usually (but blanchet@40254: not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed blanchet@46251: proof relies on the general-purpose \textit{metis} proof method, which blanchet@46251: integrates the Metis ATP in Isabelle/HOL with explicit inferences going through blanchet@46251: the kernel. Thus its results are correct by construction. blanchet@36918: blanchet@39566: In this manual, we will explicitly invoke the \textbf{sledgehammer} command. blanchet@45607: Sledgehammer also provides an automatic mode that can be enabled via the ``Auto blanchet@45607: Sledgehammer'' option in Proof General's ``Isabelle'' menu. In this mode, blanchet@45607: Sledgehammer is run on every newly entered theorem. The time limit for Auto blanchet@45607: Sledgehammer and other automatic tools can be set using the ``Auto Tools Time blanchet@45607: Limit'' option. blanchet@39566: blanchet@36918: \newbox\boxA blanchet@47126: \setbox\boxA=\hbox{\texttt{NOSPAM}} blanchet@36918: blanchet@47126: \newcommand\authoremail{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak blanchet@43628: in.\allowbreak tum.\allowbreak de}} blanchet@43628: blanchet@40937: To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is blanchet@40937: imported---this is rarely a problem in practice since it is part of blanchet@40937: \textit{Main}. Examples of Sledgehammer use can be found in Isabelle's blanchet@36918: \texttt{src/HOL/Metis\_Examples} directory. blanchet@36918: Comments and bug reports concerning Sledgehammer or this manual should be blanchet@43752: directed to the author at \authoremail. blanchet@36918: blanchet@36918: \vskip2.5\smallskipamount blanchet@36918: blanchet@36918: %\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for blanchet@36918: %suggesting several textual improvements. blanchet@36918: blanchet@36918: \section{Installation} blanchet@36918: \label{installation} blanchet@36918: blanchet@36918: Sledgehammer is part of Isabelle, so you don't need to install it. However, it blanchet@47113: relies on third-party automatic provers (ATPs and SMT solvers). blanchet@43628: blanchet@47113: Among the ATPs, E, LEO-II, Satallax, SPASS, and Vampire can be run locally; in blanchet@46210: addition, E, E-SInE, E-ToFoF, iProver, iProver-Eq, LEO-II, Satallax, SNARK, blanchet@48432: Vampire, and Waldmeister are available remotely via System\-On\-TPTP blanchet@46210: \cite{sutcliffe-2000}. If you want better performance, you should at least blanchet@46210: install E and SPASS locally. blanchet@36918: blanchet@47514: Among the SMT solvers, Alt-Ergo, CVC3, Yices, and Z3 can be run locally, and blanchet@47514: CVC3 and Z3 can be run remotely on a TU M\"unchen server. If you want better blanchet@47514: performance and get the ability to replay proofs that rely on the \emph{smt} blanchet@47514: proof method without an Internet connection, you should at least install Z3 blanchet@47514: locally. blanchet@36918: blanchet@47113: There are three main ways to install automatic provers on your machine: blanchet@47113: blanchet@47113: \begin{sloppy} blanchet@36918: \begin{enum} blanchet@47113: \item[\labelitemi] If you installed an official Isabelle package, it should blanchet@47113: already include properly setup executables for CVC3, E, SPASS, and Z3, ready to use.% blanchet@47113: \footnote{Vampire's and Yices's licenses prevent us from doing the same for blanchet@47113: these otherwise remarkable tools.} blanchet@47113: For Z3, you must additionally set the variable blanchet@47113: \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a blanchet@47113: noncommercial user, either in the environment in which Isabelle is blanchet@47113: launched or in your blanchet@48432: \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file. blanchet@36918: blanchet@47113: \item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, E, blanchet@47113: SPASS, and Z3 binary packages from \download. Extract the archives, then add a blanchet@47113: line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}% blanchet@42618: \footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at blanchet@47113: startup. Its value can be retrieved by executing \texttt{isabelle} blanchet@42618: \texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.} blanchet@47113: file with the absolute path to CVC3, E, SPASS, or Z3. For example, if the blanchet@47113: \texttt{components} file does not exist yet and you extracted SPASS to blanchet@48448: \texttt{/usr/local/spass-3.8ds}, create it with the single line blanchet@36918: blanchet@36918: \prew blanchet@48448: \texttt{/usr/local/spass-3.8ds} blanchet@36918: \postw blanchet@36918: blanchet@48432: in it. blanchet@38289: blanchet@47113: \item[\labelitemi] If you prefer to build E, LEO-II, Satallax, or SPASS blanchet@47113: manually, or found a Vampire executable somewhere (e.g., blanchet@47113: \url{http://www.vprover.org/}), set the environment variable \texttt{E\_HOME}, blanchet@47113: \texttt{LEO2\_HOME}, \texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or blanchet@38289: \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof}, blanchet@47113: \texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable. blanchet@48448: Sledgehammer has been tested with E 1.0 to 1.4, LEO-II 1.2.9, Satallax 2.2 and~2.3, blanchet@48448: SPASS 3.5, 3.7, and 3.8ds, and Vampire 0.6, 1.0, and 1.8% blanchet@38309: \footnote{Following the rewrite of Vampire, the counter for version numbers was blanchet@45278: reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent blanchet@47113: than 9.0 or 11.5.}% blanchet@38309: . Since the ATPs' output formats are neither documented nor stable, other blanchet@48448: versions might not work well with Sledgehammer. Ideally, blanchet@48448: you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION}, blanchet@47113: \texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or blanchet@47113: \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``1.4''). blanchet@47113: blanchet@47514: Similarly, if you want to build Alt-Ergo or CVC3, or found a blanchet@47113: Yices or Z3 executable somewhere (e.g., blanchet@47113: \url{http://yices.csl.sri.com/download.shtml} or blanchet@47113: \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html}), blanchet@47113: set the environment variable \texttt{CVC3\_\allowbreak SOLVER}, blanchet@47113: \texttt{YICES\_SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of blanchet@47113: the executable, \emph{including the file name}. Sledgehammer has been tested blanchet@48401: with Alt-Ergo 0.93, CVC3 2.2 and 2.4.1, Yices 1.0.28 and 1.0.33, and Z3 3.0 to 3.2. blanchet@47113: Since the SMT solvers' output formats are somewhat unstable, other blanchet@47113: versions of the solvers might not work well with Sledgehammer. Ideally, blanchet@47113: also set \texttt{CVC3\_VERSION}, \texttt{YICES\_VERSION}, or blanchet@47113: \texttt{Z3\_VERSION} to the solver's version number (e.g., ``3.2''). blanchet@36918: \end{enum} blanchet@47113: \end{sloppy} blanchet@36918: blanchet@47113: To check whether E, SPASS, Vampire, and/or Z3 are successfully installed, try blanchet@47113: out the example in \S\ref{first-steps}. If the remote versions of any of these blanchet@47113: provers is used (identified by the prefix ``\emph{remote\_\/}''), or if the blanchet@47113: local versions fail to solve the easy goal presented there, something must be blanchet@47113: wrong with the installation. blanchet@36918: blanchet@47113: Remote prover invocation requires Perl with the World Wide Web Library blanchet@47113: (\texttt{libwww-perl}) installed. If you must use a proxy server to access the blanchet@47113: Internet, set the \texttt{http\_proxy} environment variable to the proxy, either blanchet@47113: in the environment in which Isabelle is launched or in your blanchet@48432: \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few blanchet@47113: examples: blanchet@39388: blanchet@39388: \prew blanchet@39389: \texttt{http\_proxy=http://proxy.example.org} \\ blanchet@39389: \texttt{http\_proxy=http://proxy.example.org:8080} \\ blanchet@39389: \texttt{http\_proxy=http://joeblow:pAsSwRd@proxy.example.org} blanchet@39388: \postw blanchet@37517: blanchet@36918: \section{First Steps} blanchet@36918: \label{first-steps} blanchet@36918: blanchet@36918: To illustrate Sledgehammer in context, let us start a theory file and blanchet@36918: attempt to prove a simple lemma: blanchet@36918: blanchet@36918: \prew blanchet@36918: \textbf{theory}~\textit{Scratch} \\ blanchet@36918: \textbf{imports}~\textit{Main} \\ blanchet@36918: \textbf{begin} \\[2\smallskipamount] blanchet@36918: % blanchet@43786: \textbf{lemma} ``$[a] = [b] \,\Longrightarrow\, a = b$'' \\ blanchet@36918: \textbf{sledgehammer} blanchet@36918: \postw blanchet@36918: blanchet@37517: Instead of issuing the \textbf{sledgehammer} command, you can also find blanchet@37517: Sledgehammer in the ``Commands'' submenu of the ``Isabelle'' menu in Proof blanchet@37517: General or press the Emacs key sequence C-c C-a C-s. blanchet@37517: Either way, Sledgehammer produces the following output after a few seconds: blanchet@36918: blanchet@36918: \prew blanchet@36918: \slshape blanchet@47113: Sledgehammer: ``\textit{e\/}'' on goal \\ blanchet@43786: $[a] = [b] \,\Longrightarrow\, a = b$ \\ blanchet@43895: Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount] blanchet@43786: % blanchet@47113: Sledgehammer: ``\textit{z3\/}'' on goal \\ blanchet@47113: $[a] = [b] \,\Longrightarrow\, a = b$ \\ blanchet@47113: Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount] blanchet@47113: % blanchet@47113: Sledgehammer: ``\textit{vampire\/}'' on goal \\ blanchet@43786: $[a] = [b] \,\Longrightarrow\, a = b$ \\ blanchet@43895: Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount] blanchet@36918: % blanchet@47113: Sledgehammer: ``\textit{spass\/}'' on goal \\ blanchet@43786: $[a] = [b] \,\Longrightarrow\, a = b$ \\ blanchet@43895: Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount] blanchet@36918: % blanchet@47113: Sledgehammer: ``\textit{remote\_waldmeister\/}'' on goal \\ blanchet@43851: $[a] = [b] \,\Longrightarrow\, a = b$ \\ blanchet@43895: Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount] blanchet@40254: % blanchet@47935: Sledgehammer: ``\textit{remote\_satallax\/}'' on goal \\ blanchet@45929: $[a] = [b] \,\Longrightarrow\, a = b$ \\ blanchet@47113: Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). blanchet@36918: \postw blanchet@36918: blanchet@47935: Sledgehammer ran E, Satallax, SPASS, Vampire, Waldmeister, and Z3 in parallel. blanchet@43786: Depending on which provers are installed and how many processor cores are blanchet@43786: available, some of the provers might be missing or present with a blanchet@43851: \textit{remote\_} prefix. Waldmeister is run only for unit equational problems, blanchet@43851: where the goal's conclusion is a (universally quantified) equation. blanchet@36918: blanchet@46251: For each successful prover, Sledgehammer gives a one-liner proof that uses blanchet@46251: the \textit{metis} or \textit{smt} proof method. Approximate timings are shown blanchet@46251: in parentheses, indicating how fast the call is. You can click the proof to blanchet@46251: insert it into the theory text. blanchet@36918: blanchet@43895: In addition, you can ask Sledgehammer for an Isar text proof by passing the blanchet@43752: \textit{isar\_proof} option (\S\ref{output-format}): blanchet@36918: blanchet@36918: \prew blanchet@36918: \textbf{sledgehammer} [\textit{isar\_proof}] blanchet@36918: \postw blanchet@36918: blanchet@36918: When Isar proof construction is successful, it can yield proofs that are more blanchet@46251: readable and also faster than the \textit{metis} or \textit{smt} one-liners. blanchet@46251: This feature is experimental and is only available for ATPs. blanchet@36918: blanchet@37517: \section{Hints} blanchet@37517: \label{hints} blanchet@37517: blanchet@43753: This section presents a few hints that should help you get the most out of blanchet@47514: Sledgehammer. Frequently asked questions are answered in blanchet@46251: \S\ref{frequently-asked-questions}. blanchet@43753: blanchet@47113: %\newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak} blanchet@47113: \newcommand\point[1]{\subsection{\emph{#1}}} blanchet@43628: blanchet@43628: \point{Presimplify the goal} blanchet@43628: blanchet@37517: For best results, first simplify your problem by calling \textit{auto} or at blanchet@43786: least \textit{safe} followed by \textit{simp\_all}. The SMT solvers provide blanchet@43786: arithmetic decision procedures, but the ATPs typically do not (or if they do, blanchet@43786: Sledgehammer does not use it yet). Apart from Waldmeister, they are not blanchet@43786: especially good at heavy rewriting, but because they regard equations as blanchet@43786: undirected, they often prove theorems that require the reverse orientation of a blanchet@43786: \textit{simp} rule. Higher-order problems can be tackled, but the success rate blanchet@43786: is better for first-order problems. Hence, you may get better results if you blanchet@43786: first simplify the problem to remove higher-order features. blanchet@37517: blanchet@47113: \point{Make sure E, SPASS, Vampire, and Z3 are locally installed} blanchet@43628: blanchet@43628: Locally installed provers are faster and more reliable than those running on blanchet@43628: servers. See \S\ref{installation} for details on how to install them. blanchet@43628: blanchet@43628: \point{Familiarize yourself with the most important options} blanchet@43628: blanchet@43628: Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of blanchet@43628: the options are very specialized, but serious users of the tool should at least blanchet@43628: familiarize themselves with the following options: blanchet@43628: blanchet@43628: \begin{enum} blanchet@46387: \item[\labelitemi] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies blanchet@43753: the automatic provers (ATPs and SMT solvers) that should be run whenever blanchet@43753: Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{e spass blanchet@47113: remote\_vampire\/}''). For convenience, you can omit ``\textit{provers}~='' blanchet@43855: and simply write the prover names as a space-separated list (e.g., ``\textit{e blanchet@47113: spass remote\_vampire\/}''). blanchet@43628: blanchet@46387: \item[\labelitemi] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter}) blanchet@43753: specifies the maximum number of facts that should be passed to the provers. By blanchet@43753: default, the value is prover-dependent but varies between about 150 and 1000. If blanchet@43753: the provers time out, you can try lowering this value to, say, 100 or 50 and see blanchet@43753: if that helps. blanchet@43628: blanchet@46387: \item[\labelitemi] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies blanchet@46251: that Isar proofs should be generated, instead of one-liner \textit{metis} or blanchet@46251: \textit{smt} proofs. The length of the Isar proofs can be controlled by setting blanchet@43753: \textit{isar\_shrink\_factor} (\S\ref{output-format}). blanchet@43879: blanchet@46387: \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the blanchet@43879: provers' time limit. It is set to 30 seconds, but since Sledgehammer runs blanchet@43879: asynchronously you should not hesitate to raise this limit to 60 or 120 seconds blanchet@43879: if you are the kind of user who can think clearly while ATPs are active. blanchet@43628: \end{enum} blanchet@43628: blanchet@43753: Options can be set globally using \textbf{sledgehammer\_params} blanchet@43851: (\S\ref{command-syntax}). The command also prints the list of all available blanchet@43851: options with their current value. Fact selection can be influenced by specifying blanchet@43851: ``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer} call blanchet@43851: to ensure that certain facts are included, or simply ``$(\textit{my\_facts})$'' blanchet@43851: to force Sledgehammer to run only with $\textit{my\_facts}$. blanchet@43628: blanchet@43628: \section{Frequently Asked Questions} blanchet@43628: \label{frequently-asked-questions} blanchet@43628: blanchet@43786: This sections answers frequently (and infrequently) asked questions about blanchet@43786: Sledgehammer. It is a good idea to skim over it now even if you don't have any blanchet@43786: questions at this stage. And if you have any further questions not listed here, blanchet@43786: send them to the author at \authoremail. blanchet@43786: blanchet@43849: \point{Which facts are passed to the automatic provers?} blanchet@43752: blanchet@43849: The relevance filter assigns a score to every available fact (lemma, theorem, blanchet@47128: definition, or axiom) based upon how many constants that fact shares with the blanchet@43849: conjecture. This process iterates to include facts relevant to those just blanchet@43849: accepted, but with a decay factor to ensure termination. The constants are blanchet@43752: weighted to give unusual ones greater significance. The relevance filter copes blanchet@43752: best when the conjecture contains some unusual constants; if all the constants blanchet@43752: are common, it is unable to discriminate among the hundreds of facts that are blanchet@43752: picked up. The relevance filter is also memoryless: It has no information about blanchet@43752: how many times a particular fact has been used in a proof, and it cannot learn. blanchet@43752: blanchet@43752: The number of facts included in a problem varies from prover to prover, since blanchet@43849: some provers get overwhelmed more easily than others. You can show the number of blanchet@43752: facts given using the \textit{verbose} option (\S\ref{output-format}) and the blanchet@43752: actual facts using \textit{debug} (\S\ref{output-format}). blanchet@43752: blanchet@43752: Sledgehammer is good at finding short proofs combining a handful of existing blanchet@43752: lemmas. If you are looking for longer proofs, you must typically restrict the blanchet@43753: number of facts, by setting the \textit{max\_relevant} option blanchet@44436: (\S\ref{relevance-filter}) to, say, 25 or 50. blanchet@43752: blanchet@43837: You can also influence which facts are actually selected in a number of ways. If blanchet@43837: you simply want to ensure that a fact is included, you can specify it using the blanchet@43837: ``$(\textit{add}{:}~\textit{my\_facts})$'' syntax. For example: blanchet@43837: % blanchet@43837: \prew blanchet@43837: \textbf{sledgehammer} (\textit{add}: \textit{hd.simps} \textit{tl.simps}) blanchet@43837: \postw blanchet@43837: % blanchet@43837: The specified facts then replace the least relevant facts that would otherwise be blanchet@43837: included; the other selected facts remain the same. blanchet@43837: If you want to direct the selection in a particular direction, you can specify blanchet@43837: the facts via \textbf{using}: blanchet@43837: % blanchet@43837: \prew blanchet@43837: \textbf{using} \textit{hd.simps} \textit{tl.simps} \\ blanchet@43837: \textbf{sledgehammer} blanchet@43837: \postw blanchet@43837: % blanchet@43837: The facts are then more likely to be selected than otherwise, and if they are blanchet@43837: selected at iteration $j$ they also influence which facts are selected at blanchet@43837: iterations $j + 1$, $j + 2$, etc. To give them even more weight, try blanchet@43837: % blanchet@43837: \prew blanchet@43837: \textbf{using} \textit{hd.simps} \textit{tl.simps} \\ blanchet@43837: \textbf{apply}~\textbf{--} \\ blanchet@43837: \textbf{sledgehammer} blanchet@43837: \postw blanchet@43837: blanchet@47128: \point{Why does Metis fail to reconstruct the proof?} blanchet@47128: blanchet@47128: There are many reasons. If Metis runs seemingly forever, that is a sign that the blanchet@47128: proof is too difficult for it. Metis's search is complete, so it should blanchet@47128: eventually find it, but that's little consolation. There are several possible blanchet@47128: solutions: blanchet@47128: blanchet@47128: \begin{enum} blanchet@47128: \item[\labelitemi] Try the \textit{isar\_proof} option (\S\ref{output-format}) to blanchet@47128: obtain a step-by-step Isar proof where each step is justified by \textit{metis}. blanchet@47128: Since the steps are fairly small, \textit{metis} is more likely to be able to blanchet@47128: replay them. blanchet@47128: blanchet@47128: \item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}. It blanchet@47128: is usually stronger, but you need to either have Z3 available to replay the blanchet@47128: proofs, trust the SMT solver, or use certificates. See the documentation in the blanchet@47128: \emph{SMT} theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}) for details. blanchet@47128: blanchet@47128: \item[\labelitemi] Try the \textit{blast} or \textit{auto} proof methods, passing blanchet@47128: the necessary facts via \textbf{unfolding}, \textbf{using}, \textit{intro}{:}, blanchet@47128: \textit{elim}{:}, \textit{dest}{:}, or \textit{simp}{:}, as appropriate. blanchet@47128: \end{enum} blanchet@47128: blanchet@47128: In some rare cases, \textit{metis} fails fairly quickly, and you get the error blanchet@47128: message blanchet@47128: blanchet@47128: \prew blanchet@47128: \slshape blanchet@47128: One-line proof reconstruction failed. blanchet@47128: \postw blanchet@47128: blanchet@47128: This message indicates that Sledgehammer determined that the goal is provable, blanchet@47128: but the proof is, for technical reasons, beyond \textit{metis}'s power. You can blanchet@47128: then try again with the \textit{strict} option (\S\ref{problem-encoding}). blanchet@47128: blanchet@47511: If the goal is actually unprovable and you did not specify an unsound encoding blanchet@47128: using \textit{type\_enc} (\S\ref{problem-encoding}), this is a bug, and you are blanchet@47128: strongly encouraged to report this to the author at \authoremail. blanchet@47128: blanchet@47113: \point{Why are the generated Isar proofs so ugly/broken?} blanchet@43752: blanchet@47128: The current implementation of the Isar proof feature, blanchet@47128: enabled by the \textit{isar\_proof} option (\S\ref{output-format}), blanchet@47128: is highly experimental. Work on a new implementation has begun. There is a large body of blanchet@43752: research into transforming resolution proofs into natural deduction proofs (such blanchet@43752: as Isar proofs), which we hope to leverage. In the meantime, a workaround is to blanchet@43752: set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger blanchet@43752: value or to try several provers and keep the nicest-looking proof. blanchet@43752: blanchet@47128: \point{How can I tell whether a suggested proof is sound?} blanchet@47128: blanchet@47128: Earlier versions of Sledgehammer often suggested unsound proofs---either proofs blanchet@47128: of nontheorems or simply proofs that rely on type-unsound inferences. This blanchet@47511: is a thing of the past, unless you explicitly specify an unsound encoding blanchet@47128: using \textit{type\_enc} (\S\ref{problem-encoding}). blanchet@47128: % blanchet@47128: Officially, the only form of ``unsoundness'' that lurks in the sound blanchet@47128: encodings is related to missing characteristic theorems of datatypes. For blanchet@47128: example, blanchet@47128: blanchet@47128: \prew blanchet@47128: \textbf{lemma}~``$\exists \mathit{xs}.\; \mathit{xs} \neq []$'' \\ blanchet@47128: \textbf{sledgehammer} () blanchet@47128: \postw blanchet@47128: blanchet@47128: suggests an argumentless \textit{metis} call that fails. However, the conjecture blanchet@47128: does actually hold, and the \textit{metis} call can be repaired by adding blanchet@47128: \textit{list.distinct}. blanchet@47128: % blanchet@47128: We hope to address this problem in a future version of Isabelle. In the blanchet@47128: meantime, you can avoid it by passing the \textit{strict} option blanchet@47128: (\S\ref{problem-encoding}). blanchet@47128: blanchet@47126: \point{What are the \textit{full\_types}, \textit{no\_types}, and blanchet@47126: \textit{mono\_tags} arguments to Metis?} blanchet@43752: blanchet@47126: The \textit{metis}~(\textit{full\_types}) proof method blanchet@47126: and its cousin \textit{metis}~(\textit{mono\_tags}) are fully-typed blanchet@44069: version of Metis. It is somewhat slower than \textit{metis}, but the proof blanchet@44069: search is fully typed, and it also includes more powerful rules such as the blanchet@46387: axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in blanchet@44069: higher-order places (e.g., in set comprehensions). The method kicks in blanchet@44069: automatically as a fallback when \textit{metis} fails, and it is sometimes blanchet@44069: generated by Sledgehammer instead of \textit{metis} if the proof obviously blanchet@44069: requires type information or if \textit{metis} failed when Sledgehammer blanchet@44069: preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with blanchet@47126: various options for up to 3 seconds each time to ensure that the generated blanchet@47126: one-line proofs actually work and to display timing information. This can be blanchet@47907: configured using the \textit{preplay\_timeout} and \textit{dont\_preplay} blanchet@47907: options (\S\ref{timeouts}).) blanchet@47126: % blanchet@44070: At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types}) blanchet@44070: uses no type information at all during the proof search, which is more efficient blanchet@44070: but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally blanchet@44070: generated by Sledgehammer. blanchet@47126: % blanchet@47126: See the \textit{type\_enc} option (\S\ref{problem-encoding}) for details. blanchet@44070: blanchet@47126: Incidentally, if you ever see warnings such as blanchet@43752: blanchet@43752: \prew blanchet@43848: \slshape blanchet@44069: Metis: Falling back on ``\textit{metis} (\textit{full\_types})''. blanchet@43752: \postw blanchet@43752: blanchet@46251: for a successful \textit{metis} proof, you can advantageously pass the blanchet@44069: \textit{full\_types} option to \textit{metis} directly. blanchet@44069: blanchet@47194: \point{And what are the \textit{lifting} and \textit{hide\_lams} arguments blanchet@47126: to Metis?} blanchet@47126: blanchet@47126: Orthogonally to the encoding of types, it is important to choose an appropriate blanchet@47126: translation of $\lambda$-abstractions. Metis supports three translation schemes, blanchet@47126: in decreasing order of power: Curry combinators (the default), blanchet@47126: $\lambda$-lifting, and a ``hiding'' scheme that disables all reasoning under blanchet@47126: $\lambda$-abstractions. The more powerful schemes also give the automatic blanchet@47126: provers more rope to hang themselves. See the \textit{lam\_trans} option (\S\ref{problem-encoding}) for details. blanchet@47126: blanchet@43895: \point{Are generated proofs minimal?} blanchet@43877: blanchet@43895: Automatic provers frequently use many more facts than are necessary. blanchet@43895: Sledgehammer inclues a minimization tool that takes a set of facts returned by a blanchet@46251: given prover and repeatedly calls the same prover, \textit{metis}, or blanchet@46251: \textit{smt} with subsets of those axioms in order to find a minimal set. blanchet@46251: Reducing the number of axioms typically improves Metis's speed and success rate, blanchet@46251: while also removing superfluous clutter from the proof scripts. blanchet@43877: blanchet@44070: In earlier versions of Sledgehammer, generated proofs were systematically blanchet@44070: accompanied by a suggestion to invoke the minimization tool. This step is now blanchet@44070: performed implicitly if it can be done in a reasonable amount of time (something blanchet@44070: that can be guessed from the number of facts in the original proof and the time blanchet@46579: it took to find or preplay it). blanchet@43877: blanchet@46034: In addition, some provers (e.g., Yices) do not provide proofs or sometimes blanchet@46034: produce incomplete proofs. The minimizer is then invoked to find out which facts blanchet@47511: are actually needed from the (large) set of facts that was initially given to blanchet@46034: the prover. Finally, if a prover returns a proof with lots of facts, the blanchet@46034: minimizer is invoked automatically since Metis would be unlikely to re-find the blanchet@46034: proof. blanchet@46579: % blanchet@46579: Automatic minimization can be forced or disabled using the \textit{minimize} blanchet@46579: option (\S\ref{mode-of-operation}). blanchet@43877: blanchet@43849: \point{A strange error occurred---what should I do?} blanchet@43628: blanchet@43628: Sledgehammer tries to give informative error messages. Please report any strange blanchet@43752: error to the author at \authoremail. This applies double if you get the message blanchet@43628: blanchet@43752: \prew blanchet@43628: \slshape blanchet@47113: The prover found a type-unsound proof involving ``\textit{foo\/}'', blanchet@47113: ``\textit{bar\/}'', and ``\textit{baz\/}'' even though a supposedly type-sound blanchet@43846: encoding was used (or, less likely, your axioms are inconsistent). You might blanchet@43846: want to report this to the Isabelle developers. blanchet@43752: \postw blanchet@43628: blanchet@43628: \point{Auto can solve it---why not Sledgehammer?} blanchet@43628: blanchet@43628: Problems can be easy for \textit{auto} and difficult for automatic provers, but blanchet@43628: the reverse is also true, so don't be discouraged if your first attempts fail. blanchet@39566: Because the system refers to all theorems known to Isabelle, it is particularly blanchet@39566: suitable when your goal has a short proof from lemmas that you don't know about. blanchet@37517: blanchet@43752: \point{Why are there so many options?} blanchet@43752: blanchet@43752: Sledgehammer's philosophy should work out of the box, without user guidance. blanchet@43752: Many of the options are meant to be used mostly by the Sledgehammer developers blanchet@43752: for experimentation purposes. Of course, feel free to experiment with them if blanchet@43752: you are so inclined. blanchet@43752: blanchet@36918: \section{Command Syntax} blanchet@36918: \label{command-syntax} blanchet@36918: blanchet@47113: \subsection{Sledgehammer} blanchet@47113: blanchet@36918: Sledgehammer can be invoked at any point when there is an open goal by entering blanchet@36918: the \textbf{sledgehammer} command in the theory file. Its general syntax is as blanchet@36918: follows: blanchet@36918: blanchet@36918: \prew blanchet@44057: \textbf{sledgehammer} \qty{subcommand}$^?$ \qty{options}$^?$ \qty{facts\_override}$^?$ \qty{num}$^?$ blanchet@36918: \postw blanchet@36918: blanchet@36918: For convenience, Sledgehammer is also available in the ``Commands'' submenu of blanchet@36918: the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c blanchet@36918: C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with blanchet@36918: no arguments in the theory text. blanchet@36918: blanchet@44057: In the general syntax, the \qty{subcommand} may be any of the following: blanchet@36918: blanchet@36918: \begin{enum} blanchet@46387: \item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on blanchet@44057: subgoal number \qty{num} (1 by default), with the given options and facts. blanchet@36918: blanchet@46387: \item[\labelitemi] \textbf{\textit{min}:} Attempts to minimize the facts blanchet@44057: specified in the \qty{facts\_override} argument to obtain a simpler proof blanchet@36918: involving fewer facts. The options and goal number are as for \textit{run}. blanchet@36918: blanchet@46387: \item[\labelitemi] \textbf{\textit{messages}:} Redisplays recent messages issued blanchet@40444: by Sledgehammer. This allows you to examine results that might have been lost blanchet@44057: due to Sledgehammer's asynchronous nature. The \qty{num} argument specifies a blanchet@48401: limit on the number of messages to display (10 by default). blanchet@36918: blanchet@46387: \item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of blanchet@42588: automatic provers supported by Sledgehammer. See \S\ref{installation} and blanchet@42588: \S\ref{mode-of-operation} for more information on how to install automatic blanchet@42588: provers. blanchet@36918: blanchet@46387: \item[\labelitemi] \textbf{\textit{running\_provers}:} Prints information about blanchet@40240: currently running automatic provers, including elapsed runtime and remaining blanchet@40240: time until timeout. blanchet@36918: blanchet@46387: \item[\labelitemi] \textbf{\textit{kill\_provers}:} Terminates all running blanchet@40240: automatic provers. blanchet@36918: blanchet@46387: \item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote blanchet@36918: ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}. blanchet@36918: \end{enum} blanchet@36918: blanchet@44057: Sledgehammer's behavior can be influenced by various \qty{options}, which can be blanchet@44057: specified in brackets after the \textbf{sledgehammer} command. The blanchet@44057: \qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1, blanchet@47113: \ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. For blanchet@36918: example: blanchet@36918: blanchet@36918: \prew blanchet@44057: \textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120] blanchet@36918: \postw blanchet@36918: blanchet@36918: Default values can be set using \textbf{sledgehammer\_\allowbreak params}: blanchet@36918: blanchet@36918: \prew blanchet@44057: \textbf{sledgehammer\_params} \qty{options} blanchet@36918: \postw blanchet@36918: blanchet@36918: The supported options are described in \S\ref{option-reference}. blanchet@36918: blanchet@44057: The \qty{facts\_override} argument lets you alter the set of facts that go blanchet@44057: through the relevance filter. It may be of the form ``(\qty{facts})'', where blanchet@44057: \qty{facts} is a space-separated list of Isabelle facts (theorems, local blanchet@36918: assumptions, etc.), in which case the relevance filter is bypassed and the given blanchet@44057: facts are used. It may also be of the form ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}})'', blanchet@44057: ``(\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', or ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}}\ blanchet@44057: \textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', where the relevance filter is instructed to blanchet@44057: proceed as usual except that it should consider \qty{facts\/_{\mathrm{1}}} blanchet@44057: highly-relevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant. blanchet@36918: blanchet@39566: You can instruct Sledgehammer to run automatically on newly entered theorems by blanchet@45607: enabling the ``Auto Sledgehammer'' option in Proof General's ``Isabelle'' menu. blanchet@45607: For automatic runs, only the first prover set using \textit{provers} blanchet@43601: (\S\ref{mode-of-operation}) is considered, fewer facts are passed to the prover, blanchet@47128: \textit{slice} (\S\ref{mode-of-operation}) is disabled, \textit{strict} blanchet@44436: (\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format}) blanchet@43879: and \textit{debug} (\S\ref{output-format}) are disabled, and \textit{timeout} blanchet@43879: (\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in Proof blanchet@43879: General's ``Isabelle'' menu. Sledgehammer's output is also more concise. blanchet@39566: blanchet@47113: \subsection{Metis} blanchet@47113: blanchet@44057: The \textit{metis} proof method has the syntax blanchet@44057: blanchet@44057: \prew blanchet@46389: \textbf{\textit{metis}}~(\qty{options})${}^?$~\qty{facts}${}^?$ blanchet@44057: \postw blanchet@44057: blanchet@46389: where \qty{facts} is a list of arbitrary facts and \qty{options} is a blanchet@46389: comma-separated list consisting of at most one $\lambda$ translation scheme blanchet@46389: specification with the same semantics as Sledgehammer's \textit{lam\_trans} blanchet@46389: option (\S\ref{problem-encoding}) and at most one type encoding specification blanchet@46389: with the same semantics as Sledgehammer's \textit{type\_enc} option blanchet@46389: (\S\ref{problem-encoding}). blanchet@46389: % blanchet@46389: The supported $\lambda$ translation schemes are \textit{hide\_lams}, blanchet@47194: \textit{lifting}, and \textit{combs} (the default). blanchet@46389: % blanchet@46389: All the untyped type encodings listed in \S\ref{problem-encoding} are supported. blanchet@46389: For convenience, the following aliases are provided: blanchet@46389: \begin{enum} blanchet@47128: \item[\labelitemi] \textbf{\textit{full\_types}:} Synonym for \textit{poly\_guards\_query}. blanchet@46389: \item[\labelitemi] \textbf{\textit{partial\_types}:} Synonym for \textit{poly\_args}. blanchet@46389: \item[\labelitemi] \textbf{\textit{no\_types}:} Synonym for \textit{erased}. blanchet@46389: \end{enum} blanchet@44057: blanchet@36918: \section{Option Reference} blanchet@36918: \label{option-reference} blanchet@36918: blanchet@43855: \def\defl{\{} blanchet@43855: \def\defr{\}} blanchet@43855: blanchet@36918: \def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}} blanchet@47907: \def\optrueonly#1{\flushitem{\textit{#1} $\bigl[$= \textit{true}$\bigr]$\enskip}\nopagebreak\\[\parskip]} blanchet@43855: \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} blanchet@43855: \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} blanchet@43855: \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} blanchet@47237: \def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} blanchet@36918: \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]} blanchet@43855: \def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]} blanchet@43855: \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]} blanchet@36918: \def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]} blanchet@36918: \def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} blanchet@43855: \def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} blanchet@36918: blanchet@36918: Sledgehammer's options are categorized as follows:\ mode of operation blanchet@39228: (\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}), blanchet@39228: relevance filter (\S\ref{relevance-filter}), output format blanchet@43879: (\S\ref{output-format}), authentication (\S\ref{authentication}), and timeouts blanchet@43879: (\S\ref{timeouts}). blanchet@36918: blanchet@36918: The descriptions below refer to the following syntactic quantities: blanchet@36918: blanchet@36918: \begin{enum} blanchet@46387: \item[\labelitemi] \qtybf{string}: A string. blanchet@46387: \item[\labelitemi] \qtybf{bool\/}: \textit{true} or \textit{false}. blanchet@46387: \item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or blanchet@40444: \textit{smart}. blanchet@46387: \item[\labelitemi] \qtybf{int\/}: An integer. blanchet@46387: %\item[\labelitemi] \qtybf{float\/}: A floating-point number (e.g., 2.5). blanchet@46387: \item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers blanchet@40584: (e.g., 0.6 0.95). blanchet@46387: \item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}. blanchet@46387: \item[\labelitemi] \qtybf{float\_or\_none\/}: A floating-point number (e.g., 60 or blanchet@43877: 0.5) expressing a number of seconds, or the keyword \textit{none} ($\infty$ blanchet@43877: seconds). blanchet@36918: \end{enum} blanchet@36918: blanchet@44058: Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options blanchet@44058: have a negated counterpart (e.g., \textit{blocking} vs.\ blanchet@47113: \textit{non\_blocking}). When setting them, ``= \textit{true\/}'' may be omitted. blanchet@36918: blanchet@36918: \subsection{Mode of Operation} blanchet@36918: \label{mode-of-operation} blanchet@36918: blanchet@36918: \begin{enum} blanchet@43855: \opnodefaultbrk{provers}{string} blanchet@40240: Specifies the automatic provers to use as a space-separated list (e.g., blanchet@47127: ``\textit{e}~\textit{spass}~\textit{remote\_vampire\/}''). blanchet@47127: Provers can be run locally or remotely; see \S\ref{installation} for blanchet@47127: installation instructions. blanchet@47127: blanchet@47127: The following local provers are supported: blanchet@36918: blanchet@36918: \begin{enum} blanchet@47514: \item[\labelitemi] \textbf{\textit{alt\_ergo}:} Alt-Ergo is a polymorphic blanchet@47514: SMT solver developed by Bobot et al.\ \cite{alt-ergo}. blanchet@47514: It supports the TPTP polymorphic typed first-order format (TFF1) via Why3 blanchet@47514: \cite{why3}. It is included for experimental purposes. To use Alt-Ergo, set the blanchet@47514: environment variable \texttt{WHY3\_HOME} to the directory that contains the blanchet@47514: \texttt{why3} executable. Sledgehammer has been tested with Alt-Ergo 0.93 and an blanchet@47514: unidentified development version of Why3. blanchet@47514: blanchet@46387: \item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by blanchet@43786: Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3, blanchet@43786: set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the blanchet@47113: executable, including the file name, or install the prebuilt CVC3 package from blanchet@47127: \download. Sledgehammer has been tested with version 2.2. blanchet@43786: blanchet@46387: \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover blanchet@43805: developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment blanchet@43805: variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof} blanchet@47926: executable and \texttt{E\_VERSION} to the version number (e.g., ``1.4''), or blanchet@47926: install the prebuilt E package from \download. Sledgehammer has been tested with blanchet@47926: versions 1.0 to 1.4. blanchet@36918: blanchet@46387: \item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic blanchet@44969: higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, blanchet@47113: with support for the TPTP typed higher-order syntax (THF0). To use LEO-II, set blanchet@47113: the environment variable \texttt{LEO2\_HOME} to the directory that contains the blanchet@47113: \texttt{leo} executable. Sledgehammer requires version 1.2.9 or above. blanchet@44969: blanchet@46387: \item[\labelitemi] \textbf{\textit{metis}:} Although it is much less powerful than blanchet@44969: the external provers, Metis itself can be used for proof search. blanchet@44969: blanchet@46387: \item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic blanchet@44969: higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with blanchet@47113: support for the TPTP typed higher-order syntax (THF0). To use Satallax, set the blanchet@47113: environment variable \texttt{SATALLAX\_HOME} to the directory that contains the blanchet@47113: \texttt{satallax} executable. Sledgehammer requires version 2.2 or above. blanchet@44969: blanchet@46387: \item[\labelitemi] \textbf{\textit{smt}:} The \textit{smt} proof method with the blanchet@46426: current settings (usually:\ Z3 with proof reconstruction). blanchet@46251: blanchet@46387: \item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution blanchet@43805: prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}. blanchet@43805: To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory blanchet@47926: that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the blanchet@48448: version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from blanchet@47926: \download. Sledgehammer requires version 3.5 or above. blanchet@36918: blanchet@46387: \item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution blanchet@43805: prover developed by Andrei Voronkov and his colleagues blanchet@43805: \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable blanchet@43805: \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire} blanchet@45278: executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``1.8''). blanchet@47113: Sledgehammer has been tested with versions 0.6, 1.0, and 1.8. blanchet@47514: Versions above 1.8 support the TPTP typed first-order format (TFF0). blanchet@36918: blanchet@46387: \item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at blanchet@44969: SRI \cite{yices}. To use Yices, set the environment variable blanchet@44969: \texttt{YICES\_SOLVER} to the complete path of the executable, including the blanchet@46731: file name. Sledgehammer has been tested with version 1.0.28. blanchet@44969: blanchet@46387: \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at blanchet@42611: Microsoft Research \cite{z3}. To use Z3, set the environment variable blanchet@42611: \texttt{Z3\_SOLVER} to the complete path of the executable, including the file blanchet@45280: name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a blanchet@46731: noncommercial user. Sledgehammer has been tested with versions 3.0 to 3.2. blanchet@42611: blanchet@46387: \item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be blanchet@46387: an ATP, exploiting Z3's support for the TPTP untyped and typed first-order blanchet@46731: formats (FOF and TFF0). It is included for experimental purposes. It blanchet@46731: requires version 3.0 or above. To use it, set the environment variable blanchet@46731: \texttt{Z3\_HOME} to the directory that contains the \texttt{z3} blanchet@46731: executable. blanchet@43786: \end{enum} blanchet@43786: blanchet@47127: The following remote provers are supported: blanchet@43786: blanchet@43786: \begin{enum} blanchet@46387: \item[\labelitemi] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs blanchet@43786: on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to blanchet@43786: point). blanchet@40254: blanchet@46387: \item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs blanchet@36918: on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. blanchet@36918: blanchet@46387: \item[\labelitemi] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover blanchet@47935: developed by Kry\v stof Hoder \cite{sine} based on E. It runs on Geoff blanchet@47935: Sutcliffe's Miami servers. blanchet@44962: blanchet@46387: \item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover blanchet@44962: developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami blanchet@46387: servers. This ATP supports the TPTP typed first-order format (TFF0). The blanchet@44962: remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers. blanchet@44962: blanchet@46387: \item[\labelitemi] \textbf{\textit{remote\_iprover}:} iProver is a pure blanchet@46210: instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. The blanchet@46210: remote version of iProver runs on Geoff Sutcliffe's Miami servers blanchet@46210: \cite{sutcliffe-2000}. blanchet@46210: blanchet@46387: \item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} iProver-Eq is an blanchet@46210: instantiation-based prover with native support for equality developed by blanchet@46210: Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. The blanchet@46210: remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers blanchet@46210: \cite{sutcliffe-2000}. blanchet@46210: blanchet@46387: \item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II blanchet@44969: runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. blanchet@43805: blanchet@46387: \item[\labelitemi] \textbf{\textit{remote\_satallax}:} The remote version of blanchet@44969: Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. blanchet@43805: blanchet@46387: \item[\labelitemi] \textbf{\textit{remote\_snark}:} SNARK is a first-order blanchet@44492: resolution prover developed by Stickel et al.\ \cite{snark}. It supports the blanchet@46387: TPTP typed first-order format (TFF0). The remote version of SNARK runs on blanchet@44492: Geoff Sutcliffe's Miami servers. blanchet@40254: blanchet@46387: \item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of blanchet@45278: Vampire runs on Geoff Sutcliffe's Miami servers. Version 1.8 is used. blanchet@43786: blanchet@46387: \item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit blanchet@43786: equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be blanchet@44492: used to prove universally quantified equations using unconditional equations, blanchet@44492: corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister blanchet@44492: runs on Geoff Sutcliffe's Miami servers. blanchet@42609: blanchet@46387: \item[\labelitemi] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on blanchet@41190: servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to blanchet@41190: point). blanchet@40254: blanchet@46387: \item[\labelitemi] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3 blanchet@45282: with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers. blanchet@36918: \end{enum} blanchet@36918: blanchet@47935: By default, Sledgehammer runs E, Satallax, SPASS, Vampire, Z3 (or whatever blanchet@44962: the SMT module's \textit{smt\_solver} configuration option is set to), and (if blanchet@44962: appropriate) Waldmeister in parallel---either locally or remotely, depending on blanchet@44962: the number of processor cores available. For historical reasons, the default blanchet@44962: value of this option can be overridden using the option ``Sledgehammer: blanchet@45607: Provers'' in Proof General's ``Isabelle'' menu. blanchet@36918: blanchet@45607: It is generally a good idea to run several provers in parallel. Running E, blanchet@45607: SPASS, and Vampire for 5~seconds yields a similar success rate to running the blanchet@45607: most effective of these for 120~seconds \cite{boehme-nipkow-2010}. blanchet@40240: blanchet@43894: For the \textit{min} subcommand, the default prover is \textit{metis}. If blanchet@43894: several provers are set, the first one is used. blanchet@43894: blanchet@40240: \opnodefault{prover}{string} blanchet@40240: Alias for \textit{provers}. blanchet@40240: blanchet@39227: \opfalse{blocking}{non\_blocking} blanchet@39227: Specifies whether the \textbf{sledgehammer} command should operate blanchet@39227: synchronously. The asynchronous (non-blocking) mode lets the user start proving blanchet@39227: the putative theorem manually while Sledgehammer looks for a proof, but it can blanchet@43836: also be more confusing. Irrespective of the value of this option, Sledgehammer blanchet@43836: is always run synchronously for the new jEdit-based user interface or if blanchet@43836: \textit{debug} (\S\ref{output-format}) is enabled. blanchet@39227: blanchet@46579: \optrue{slice}{dont\_slice} blanchet@43314: Specifies whether the time allocated to a prover should be sliced into several blanchet@43314: segments, each of which has its own set of possibly prover-dependent options. blanchet@43317: For SPASS and Vampire, the first slice tries the fast but incomplete blanchet@43314: set-of-support (SOS) strategy, whereas the second slice runs without it. For E, blanchet@43317: up to three slices are tried, with different weighted search strategies and blanchet@43314: number of facts. For SMT solvers, several slices are tried with the same options blanchet@43317: each time but fewer and fewer facts. According to benchmarks with a timeout of blanchet@43317: 30 seconds, slicing is a valuable optimization, and you should probably leave it blanchet@43317: enabled unless you are conducting experiments. This option is implicitly blanchet@43314: disabled for (short) automatic runs. blanchet@43314: blanchet@43314: \nopagebreak blanchet@43314: {\small See also \textit{verbose} (\S\ref{output-format}).} blanchet@43314: blanchet@46579: \opsmart{minimize}{dont\_minimize} blanchet@46579: Specifies whether the minimization tool should be invoked automatically after blanchet@46579: proof search. By default, automatic minimization takes place only if blanchet@46579: it can be done in a reasonable amount of time (as determined by blanchet@46579: the number of facts in the original proof and the time it took to find or blanchet@46579: preplay it) or the proof involves an unreasonably large number of facts. blanchet@46579: blanchet@46579: \nopagebreak blanchet@47907: {\small See also \textit{preplay\_timeout} (\S\ref{timeouts}) blanchet@47907: and \textit{dont\_preplay} (\S\ref{timeouts}).} blanchet@46579: blanchet@36918: \opfalse{overlord}{no\_overlord} blanchet@36918: Specifies whether Sledgehammer should put its temporary files in blanchet@36918: \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for blanchet@36918: debugging Sledgehammer but also unsafe if several instances of the tool are run blanchet@36918: simultaneously. The files are identified by the prefix \texttt{prob\_}; you may blanchet@36918: safely remove them after Sledgehammer has run. blanchet@36918: blanchet@36918: \nopagebreak blanchet@36918: {\small See also \textit{debug} (\S\ref{output-format}).} blanchet@36918: \end{enum} blanchet@36918: blanchet@36918: \subsection{Problem Encoding} blanchet@36918: \label{problem-encoding} blanchet@36918: blanchet@46387: \newcommand\comb[1]{\const{#1}} blanchet@46387: blanchet@36918: \begin{enum} blanchet@46387: \opdefault{lam\_trans}{string}{smart} blanchet@46387: Specifies the $\lambda$ translation scheme to use in ATP problems. The supported blanchet@46387: translation schemes are listed below: blanchet@46387: blanchet@46387: \begin{enum} blanchet@46387: \item[\labelitemi] \textbf{\textit{hide\_lams}:} Hide the $\lambda$-abstractions blanchet@46387: by replacing them by unspecified fresh constants, effectively disabling all blanchet@46387: reasoning under $\lambda$-abstractions. blanchet@46387: blanchet@47194: \item[\labelitemi] \textbf{\textit{lifting}:} Introduce a new blanchet@46387: supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions, blanchet@46387: defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting). blanchet@46387: blanchet@47194: \item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry blanchet@46387: combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators blanchet@46387: enable the ATPs to synthesize $\lambda$-terms but tend to yield bulkier formulas blanchet@46387: than $\lambda$-lifting: The translation is quadratic in the worst case, and the blanchet@46387: equational definitions of the combinators are very prolific in the context of blanchet@46387: resolution. blanchet@46387: blanchet@47194: \item[\labelitemi] \textbf{\textit{combs\_and\_lifting}:} Introduce a new blanchet@46387: supercombinator \const{c} for each cluster of $\lambda$-abstractions and characterize it both using a blanchet@46387: lifted equation $\const{c}~x_1~\ldots~x_n = t$ and via Curry combinators. blanchet@46387: blanchet@47194: \item[\labelitemi] \textbf{\textit{combs\_or\_lifting}:} For each cluster of blanchet@47194: $\lambda$-abstractions, heuristically choose between $\lambda$-lifting and Curry blanchet@47194: combinators. blanchet@47194: blanchet@46387: \item[\labelitemi] \textbf{\textit{keep\_lams}:} blanchet@46387: Keep the $\lambda$-abstractions in the generated problems. This is available blanchet@46387: only with provers that support the THF0 syntax. blanchet@46387: blanchet@46387: \item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used blanchet@46387: depends on the ATP and should be the most efficient scheme for that ATP. blanchet@46387: \end{enum} blanchet@46387: blanchet@47194: For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting}, blanchet@47194: irrespective of the value of this option. blanchet@46387: blanchet@47237: \opsmartx{uncurried\_aliases}{no\_uncurried\_aliases} blanchet@47239: Specifies whether fresh function symbols should be generated as aliases for blanchet@47239: applications of curried functions in ATP problems. blanchet@47237: blanchet@44494: \opdefault{type\_enc}{string}{smart} blanchet@44494: Specifies the type encoding to use in ATP problems. Some of the type encodings blanchet@44494: are unsound, meaning that they can give rise to spurious proofs blanchet@46251: (unreconstructible using \textit{metis}). The supported type encodings are blanchet@47128: listed below, with an indication of their soundness in parentheses. blanchet@47130: An asterisk (*) means that the encoding is slightly incomplete for blanchet@47130: reconstruction with \textit{metis}, unless the \emph{strict} option (described blanchet@47130: below) is enabled. blanchet@43089: blanchet@43089: \begin{enum} blanchet@46387: \item[\labelitemi] \textbf{\textit{erased} (very unsound):} No type information is blanchet@47128: supplied to the ATP, not even to resolve overloading. Types are simply erased. blanchet@43453: blanchet@46387: \item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using blanchet@47128: a predicate \const{g}$(\tau, t)$ that guards bound blanchet@44861: variables. Constants are annotated with their types, supplied as additional blanchet@43756: arguments, to resolve overloading. blanchet@43555: blanchet@46387: \item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is blanchet@47128: tagged with its type using a function $\const{t\/}(\tau, t)$. blanchet@43756: blanchet@46387: \item[\labelitemi] \textbf{\textit{poly\_args} (unsound):} blanchet@44861: Like for \textit{poly\_guards} constants are annotated with their types to blanchet@43843: resolve overloading, but otherwise no type information is encoded. This blanchet@44069: coincides with the default encoding used by the \textit{metis} command. blanchet@43555: blanchet@46387: \item[\labelitemi] blanchet@43587: \textbf{% blanchet@45349: \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\ blanchet@45349: \textit{raw\_mono\_args} (unsound):} \\ blanchet@44861: Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args}, blanchet@43587: respectively, but the problem is additionally monomorphized, meaning that type blanchet@43587: variables are instantiated with heuristically chosen ground types. blanchet@43587: Monomorphization can simplify reasoning but also leads to larger fact bases, blanchet@43587: which can slow down the ATPs. blanchet@43453: blanchet@46387: \item[\labelitemi] blanchet@43587: \textbf{% blanchet@45349: \textit{mono\_guards}, \textit{mono\_tags} (sound); blanchet@45349: \textit{mono\_args} (unsound):} \\ blanchet@43587: Similar to blanchet@45349: \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and blanchet@45349: \textit{raw\_mono\_args}, respectively but types are mangled in constant names blanchet@45349: instead of being supplied as ground term arguments. The binary predicate blanchet@47128: $\const{g}(\tau, t)$ becomes a unary predicate blanchet@47128: $\const{g\_}\tau(t)$, and the binary function blanchet@47128: $\const{t}(\tau, t)$ becomes a unary function blanchet@47128: $\const{t\_}\tau(t)$. blanchet@43453: blanchet@47263: \item[\labelitemi] \textbf{\textit{mono\_native} (sound):} Exploits native blanchet@47514: first-order types if the prover supports the TFF0, TFF1, or THF0 syntax; blanchet@47514: otherwise, falls back on \textit{mono\_guards}. The problem is monomorphized. blanchet@44492: blanchet@47263: \item[\labelitemi] \textbf{\textit{mono\_native\_higher} (sound):} Exploits blanchet@47263: native higher-order types if the prover supports the THF0 syntax; otherwise, blanchet@47263: falls back on \textit{mono\_native} or \textit{mono\_guards}. The problem is blanchet@47263: monomorphized. blanchet@43551: blanchet@47514: \item[\labelitemi] \textbf{\textit{poly\_native} (sound):} Exploits native blanchet@47514: polymorphic first-order types if the prover supports the TFF1 syntax; otherwise, blanchet@47514: falls back on \textit{mono\_native}. blanchet@47514: blanchet@46387: \item[\labelitemi] blanchet@43551: \textbf{% blanchet@45349: \textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\ blanchet@45349: \textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\ blanchet@47263: \textit{mono\_native}? (sound*):} \\ blanchet@44861: The type encodings \textit{poly\_guards}, \textit{poly\_tags}, blanchet@45349: \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards}, blanchet@47907: \textit{mono\_tags}, and \textit{mono\_native} are fully typed and sound. For blanchet@47907: each of these, Sledgehammer also provides a lighter variant identified by a blanchet@47907: question mark (`\hbox{?}')\ that detects and erases monotonic types, notably blanchet@47907: infinite types. (For \textit{mono\_native}, the types are not actually erased blanchet@47907: but rather replaced by a shared uniform type of individuals.) As argument to the blanchet@47907: \textit{metis} proof method, the question mark is replaced by a blanchet@47907: \hbox{``\textit{\_query\/}''} suffix. blanchet@43460: blanchet@46387: \item[\labelitemi] blanchet@43756: \textbf{% blanchet@45640: \textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\ blanchet@45640: \textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\ blanchet@47128: (sound*):} \\ blanchet@45678: Even lighter versions of the `\hbox{?}' encodings. As argument to the blanchet@45678: \textit{metis} proof method, the `\hbox{??}' suffix is replaced by blanchet@47113: \hbox{``\textit{\_query\_query\/}''}. blanchet@45678: blanchet@46387: \item[\labelitemi] blanchet@45678: \textbf{% blanchet@47128: \textit{poly\_guards}@?, \textit{raw\_mono\_guards}@? (sound*):} \\ blanchet@45678: Alternative versions of the `\hbox{??}' encodings. As argument to the blanchet@45678: \textit{metis} proof method, the `\hbox{@?}' suffix is replaced by blanchet@47113: \hbox{``\textit{\_at\_query\/}''}. blanchet@45640: blanchet@46387: \item[\labelitemi] blanchet@45640: \textbf{% blanchet@45349: \textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\ blanchet@45607: \textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\ blanchet@47263: \textit{mono\_native}!, \textit{mono\_native\_higher}! (mildly unsound):} \\ blanchet@44861: The type encodings \textit{poly\_guards}, \textit{poly\_tags}, blanchet@45349: \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards}, blanchet@47263: \textit{mono\_tags}, \textit{mono\_native}, and \textit{mono\_native\_higher} blanchet@45607: also admit a mildly unsound (but very efficient) variant identified by an blanchet@45678: exclamation mark (`\hbox{!}') that detects and erases erases all types except blanchet@47263: those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_native} blanchet@47263: and \textit{mono\_native\_higher}, the types are not actually erased but rather blanchet@45607: replaced by a shared uniform type of individuals.) As argument to the blanchet@45607: \textit{metis} proof method, the exclamation mark is replaced by the suffix blanchet@47113: \hbox{``\textit{\_bang\/}''}. blanchet@43756: blanchet@46387: \item[\labelitemi] blanchet@45640: \textbf{% blanchet@45640: \textit{poly\_guards}!!, \textit{poly\_tags}!!, \textit{raw\_mono\_guards}!!, \\ blanchet@45640: \textit{raw\_mono\_tags}!!, \textit{mono\_guards}!!, \textit{mono\_tags}!! \\ blanchet@45640: (mildly unsound):} \\ blanchet@45678: Even lighter versions of the `\hbox{!}' encodings. As argument to the blanchet@45678: \textit{metis} proof method, the `\hbox{!!}' suffix is replaced by blanchet@47113: \hbox{``\textit{\_bang\_bang\/}''}. blanchet@45678: blanchet@46387: \item[\labelitemi] blanchet@45678: \textbf{% blanchet@46821: \textit{poly\_guards}@!, \textit{raw\_mono\_guards}@! (mildly unsound):} \\ blanchet@45678: Alternative versions of the `\hbox{!!}' encodings. As argument to the blanchet@45678: \textit{metis} proof method, the `\hbox{@!}' suffix is replaced by blanchet@47113: \hbox{``\textit{\_at\_bang\/}''}. blanchet@45640: blanchet@46387: \item[\labelitemi] \textbf{\textit{smart}:} The actual encoding used depends on blanchet@47907: the ATP and should be the most efficient sound encoding for that ATP. blanchet@43089: \end{enum} blanchet@43089: blanchet@47263: For SMT solvers, the type encoding is always \textit{mono\_native}, irrespective blanchet@45607: of the value of this option. blanchet@43757: blanchet@43757: \nopagebreak blanchet@43757: {\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter}) blanchet@43757: and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).} blanchet@44436: blanchet@47130: \opfalse{strict}{non\_strict} blanchet@47128: Specifies whether Sledgehammer should run in its strict mode. In that mode, blanchet@47130: sound type encodings marked with an asterisk (*) above are made complete blanchet@47128: for reconstruction with \textit{metis}, at the cost of some clutter in the blanchet@47128: generated problems. This option has no effect if \textit{type\_enc} is blanchet@47128: deliberately set to an unsound encoding. blanchet@38814: \end{enum} blanchet@36918: blanchet@38814: \subsection{Relevance Filter} blanchet@38814: \label{relevance-filter} blanchet@38814: blanchet@38814: \begin{enum} blanchet@40584: \opdefault{relevance\_thresholds}{float\_pair}{\upshape 0.45~0.85} blanchet@38985: Specifies the thresholds above which facts are considered relevant by the blanchet@38985: relevance filter. The first threshold is used for the first iteration of the blanchet@38985: relevance filter and the second threshold is used for the last iteration (if it blanchet@38985: is reached). The effective threshold is quadratically interpolated for the other blanchet@40584: iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems blanchet@40584: are relevant and 1 only theorems that refer to previously seen constants. blanchet@36918: blanchet@43906: \opdefault{max\_relevant}{smart\_int}{smart} blanchet@38985: Specifies the maximum number of facts that may be returned by the relevance blanchet@38985: filter. If the option is set to \textit{smart}, it is set to a value that was blanchet@40240: empirically found to be appropriate for the prover. A typical value would be blanchet@43906: 250. blanchet@43051: blanchet@44218: \opdefault{max\_new\_mono\_instances}{int}{\upshape 200} blanchet@43753: Specifies the maximum number of monomorphic instances to generate beyond blanchet@43753: \textit{max\_relevant}. The higher this limit is, the more monomorphic instances blanchet@43753: are potentially generated. Whether monomorphization takes place depends on the blanchet@44494: type encoding used. blanchet@43753: blanchet@43753: \nopagebreak blanchet@44494: {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).} blanchet@43753: blanchet@43753: \opdefault{max\_mono\_iters}{int}{\upshape 3} blanchet@43753: Specifies the maximum number of iterations for the monomorphization fixpoint blanchet@43753: construction. The higher this limit is, the more monomorphic instances are blanchet@43753: potentially generated. Whether monomorphization takes place depends on the blanchet@44494: type encoding used. blanchet@43753: blanchet@43753: \nopagebreak blanchet@44494: {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).} blanchet@36918: \end{enum} blanchet@36918: blanchet@36918: \subsection{Output Format} blanchet@36918: \label{output-format} blanchet@36918: blanchet@36918: \begin{enum} blanchet@36918: blanchet@36918: \opfalse{verbose}{quiet} blanchet@36918: Specifies whether the \textbf{sledgehammer} command should explain what it does. blanchet@41456: This option is implicitly disabled for automatic runs. blanchet@36918: blanchet@36918: \opfalse{debug}{no\_debug} blanchet@40444: Specifies whether Sledgehammer should display additional debugging information blanchet@40444: beyond what \textit{verbose} already displays. Enabling \textit{debug} also blanchet@41456: enables \textit{verbose} and \textit{blocking} (\S\ref{mode-of-operation}) blanchet@41456: behind the scenes. The \textit{debug} option is implicitly disabled for blanchet@41456: automatic runs. blanchet@36918: blanchet@36918: \nopagebreak blanchet@36918: {\small See also \textit{overlord} (\S\ref{mode-of-operation}).} blanchet@36918: blanchet@36918: \opfalse{isar\_proof}{no\_isar\_proof} blanchet@36918: Specifies whether Isar proofs should be output in addition to one-liner blanchet@36918: \textit{metis} proofs. Isar proof construction is still experimental and often blanchet@36918: fails; however, they are usually faster and sometimes more robust than blanchet@36918: \textit{metis} proofs. blanchet@36918: blanchet@40584: \opdefault{isar\_shrink\_factor}{int}{\upshape 1} blanchet@36918: Specifies the granularity of the Isar proof. A value of $n$ indicates that each blanchet@36918: Isar proof step should correspond to a group of up to $n$ consecutive proof blanchet@36918: steps in the ATP proof. blanchet@36918: \end{enum} blanchet@36918: blanchet@39228: \subsection{Authentication} blanchet@39228: \label{authentication} blanchet@36918: blanchet@36918: \begin{enum} blanchet@39228: \opnodefault{expect}{string} blanchet@39228: Specifies the expected outcome, which must be one of the following: blanchet@39228: blanchet@39228: \begin{enum} blanchet@47128: \item[\labelitemi] \textbf{\textit{some}:} Sledgehammer found a proof. blanchet@46387: \item[\labelitemi] \textbf{\textit{none}:} Sledgehammer found no proof. blanchet@46387: \item[\labelitemi] \textbf{\textit{timeout}:} Sledgehammer timed out. blanchet@46387: \item[\labelitemi] \textbf{\textit{unknown}:} Sledgehammer encountered some blanchet@40444: problem. blanchet@39228: \end{enum} blanchet@39228: blanchet@39228: Sledgehammer emits an error (if \textit{blocking} is enabled) or a warning blanchet@39228: (otherwise) if the actual outcome differs from the expected outcome. This option blanchet@39228: is useful for regression testing. blanchet@39228: blanchet@39228: \nopagebreak blanchet@43879: {\small See also \textit{blocking} (\S\ref{mode-of-operation}) and blanchet@43879: \textit{timeout} (\S\ref{timeouts}).} blanchet@43879: \end{enum} blanchet@43879: blanchet@43879: \subsection{Timeouts} blanchet@43879: \label{timeouts} blanchet@43879: blanchet@43879: \begin{enum} blanchet@43879: \opdefault{timeout}{float\_or\_none}{\upshape 30} blanchet@43879: Specifies the maximum number of seconds that the automatic provers should spend blanchet@43879: searching for a proof. This excludes problem preparation and is a soft limit. blanchet@43879: For historical reasons, the default value of this option can be overridden using blanchet@45607: the option ``Sledgehammer: Time Limit'' in Proof General's ``Isabelle'' menu. blanchet@43879: blanchet@47126: \opdefault{preplay\_timeout}{float\_or\_none}{\upshape 3} blanchet@46251: Specifies the maximum number of seconds that \textit{metis} or \textit{smt} blanchet@46251: should spend trying to ``preplay'' the found proof. If this option is set to 0, blanchet@46251: no preplaying takes place, and no timing information is displayed next to the blanchet@46251: suggested \textit{metis} calls. blanchet@46579: blanchet@46579: \nopagebreak blanchet@46579: {\small See also \textit{minimize} (\S\ref{mode-of-operation}).} blanchet@47907: blanchet@47907: \optrueonly{dont\_preplay} blanchet@47907: Alias for ``\textit{preplay\_timeout} = 0''. blanchet@47907: blanchet@36918: \end{enum} blanchet@36918: blanchet@36918: \let\em=\sl blanchet@36918: \bibliography{../manual}{} blanchet@36918: \bibliographystyle{abbrv} blanchet@36918: blanchet@36918: \end{document}