
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}




