doc-src/Sledgehammer/sledgehammer.tex
author blanchet
Sun Apr 22 14:16:46 2012 +0200 (2012-04-22)
changeset 47672 1bf4fa90cd03
parent 47642 9a9218111085
child 47963 46c73ad5f7c0
permissions -rw-r--r--
fixed typos
blanchet@36926
     1
\documentclass[a4paper,12pt]{article}
blanchet@36926
     2
\usepackage[T1]{fontenc}
blanchet@36926
     3
\usepackage{amsmath}
blanchet@36926
     4
\usepackage{amssymb}
blanchet@36926
     5
\usepackage[english,french]{babel}
blanchet@36926
     6
\usepackage{color}
blanchet@36926
     7
\usepackage{footmisc}
blanchet@36926
     8
\usepackage{graphicx}
blanchet@36926
     9
%\usepackage{mathpazo}
blanchet@36926
    10
\usepackage{multicol}
blanchet@36926
    11
\usepackage{stmaryrd}
blanchet@36926
    12
%\usepackage[scaled=.85]{beramono}
wenzelm@42511
    13
\usepackage{../../lib/texinputs/isabelle,../iman,../pdfsetup}
blanchet@36926
    14
blanchet@46242
    15
\newcommand\download{\url{http://www21.in.tum.de/~blanchet/\#software}}
blanchet@46242
    16
blanchet@43216
    17
\def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}}
blanchet@43216
    18
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$}
blanchet@43216
    19
blanchet@45516
    20
\newcommand\const[1]{\textsf{#1}}
blanchet@45516
    21
blanchet@36926
    22
%\oddsidemargin=4.6mm
blanchet@36926
    23
%\evensidemargin=4.6mm
blanchet@36926
    24
%\textwidth=150mm
blanchet@36926
    25
%\topmargin=4.6mm
blanchet@36926
    26
%\headheight=0mm
blanchet@36926
    27
%\headsep=0mm
blanchet@36926
    28
%\textheight=234mm
blanchet@36926
    29
blanchet@36926
    30
\def\Colon{\mathord{:\mkern-1.5mu:}}
blanchet@36926
    31
%\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
blanchet@36926
    32
%\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
blanchet@36926
    33
\def\lparr{\mathopen{(\mkern-4mu\mid}}
blanchet@36926
    34
\def\rparr{\mathclose{\mid\mkern-4mu)}}
blanchet@36926
    35
blanchet@36926
    36
\def\unk{{?}}
blanchet@36926
    37
\def\undef{(\lambda x.\; \unk)}
blanchet@36926
    38
%\def\unr{\textit{others}}
blanchet@36926
    39
\def\unr{\ldots}
blanchet@36926
    40
\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
blanchet@36926
    41
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
blanchet@36926
    42
blanchet@36926
    43
\urlstyle{tt}
blanchet@36926
    44
blanchet@36926
    45
\begin{document}
blanchet@36926
    46
blanchet@45516
    47
%%% TYPESETTING
blanchet@45516
    48
%\renewcommand\labelitemi{$\bullet$}
blanchet@45516
    49
\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}}
blanchet@45516
    50
blanchet@36926
    51
\selectlanguage{english}
blanchet@36926
    52
blanchet@36926
    53
\title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]
blanchet@36926
    54
Hammering Away \\[\smallskipamount]
blanchet@36926
    55
\Large A User's Guide to Sledgehammer for Isabelle/HOL}
blanchet@36926
    56
\author{\hbox{} \\
blanchet@36926
    57
Jasmin Christian Blanchette \\
blanchet@43002
    58
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\[4\smallskipamount]
blanchet@43002
    59
{\normalsize with contributions from} \\[4\smallskipamount]
blanchet@43002
    60
Lawrence C. Paulson \\
blanchet@43002
    61
{\normalsize Computer Laboratory, University of Cambridge} \\
blanchet@36926
    62
\hbox{}}
blanchet@36926
    63
blanchet@36926
    64
\maketitle
blanchet@36926
    65
blanchet@36926
    66
\tableofcontents
blanchet@36926
    67
blanchet@36926
    68
\setlength{\parskip}{.7em plus .2em minus .1em}
blanchet@36926
    69
\setlength{\parindent}{0pt}
blanchet@36926
    70
\setlength{\abovedisplayskip}{\parskip}
blanchet@36926
    71
\setlength{\abovedisplayshortskip}{.9\parskip}
blanchet@36926
    72
\setlength{\belowdisplayskip}{\parskip}
blanchet@36926
    73
\setlength{\belowdisplayshortskip}{.9\parskip}
blanchet@36926
    74
blanchet@36926
    75
% General-purpose enum environment with correct spacing
blanchet@36926
    76
\newenvironment{enum}%
blanchet@36926
    77
    {\begin{list}{}{%
blanchet@36926
    78
        \setlength{\topsep}{.1\parskip}%
blanchet@36926
    79
        \setlength{\partopsep}{.1\parskip}%
blanchet@36926
    80
        \setlength{\itemsep}{\parskip}%
blanchet@36926
    81
        \advance\itemsep by-\parsep}}
blanchet@36926
    82
    {\end{list}}
blanchet@36926
    83
blanchet@36926
    84
\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
blanchet@36926
    85
\advance\rightskip by\leftmargin}
blanchet@36926
    86
\def\post{\vskip0pt plus1ex\endgroup}
blanchet@36926
    87
blanchet@36926
    88
\def\prew{\pre\advance\rightskip by-\leftmargin}
blanchet@36926
    89
\def\postw{\post}
blanchet@36926
    90
blanchet@36926
    91
\section{Introduction}
blanchet@36926
    92
\label{introduction}
blanchet@36926
    93
blanchet@42964
    94
Sledgehammer is a tool that applies automatic theorem provers (ATPs)
blanchet@47561
    95
and satisfiability-modulo-theories (SMT) solvers on the current goal.%
blanchet@47561
    96
\footnote{The distinction between ATPs and SMT solvers is convenient but mostly
blanchet@47561
    97
historical. The two communities are converging, with more and more ATPs
blanchet@47672
    98
supporting typical SMT features such as arithmetic and sorts, and a few SMT
blanchet@47561
    99
solvers parsing ATP syntaxes. There is also a strong technological connection
blanchet@47561
   100
between instantiation-based ATPs (such as iProver and iProver-Eq) and SMT
blanchet@47561
   101
solvers.}
blanchet@47561
   102
%
blanchet@47561
   103
The supported ATPs are E \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF
blanchet@47561
   104
\cite{tofof}, iProver \cite{korovin-2009}, iProver-Eq
blanchet@47561
   105
\cite{korovin-sticksel-2010}, LEO-II \cite{leo2}, Satallax \cite{satallax},
blanchet@47561
   106
SNARK \cite{snark}, SPASS \cite{weidenbach-et-al-2009}, Vampire
blanchet@47561
   107
\cite{riazanov-voronkov-2002}, and Waldmeister \cite{waldmeister}. The ATPs are
blanchet@47561
   108
run either locally or remotely via the System\-On\-TPTP web service
blanchet@47561
   109
\cite{sutcliffe-2000}. In addition to the ATPs, the SMT solvers Z3 \cite{z3} is
blanchet@47561
   110
used by default, and you can tell Sledgehammer to try Alt-Ergo \cite{alt-ergo},
blanchet@47561
   111
CVC3 \cite{cvc3}, and Yices \cite{yices} as well; these are run either locally
blanchet@47561
   112
or (for CVC3 and Z3) on a server at the TU M\"unchen.
blanchet@36926
   113
blanchet@40073
   114
The problem passed to the automatic provers consists of your current goal
blanchet@40073
   115
together with a heuristic selection of hundreds of facts (theorems) from the
blanchet@40073
   116
current theory context, filtered by relevance. Because jobs are run in the
blanchet@40073
   117
background, you can continue to work on your proof by other means. Provers can
blanchet@40073
   118
be run in parallel. Any reply (which may arrive half a minute later) will appear
blanchet@40073
   119
in the Proof General response buffer.
blanchet@37517
   120
blanchet@40073
   121
The result of a successful proof search is some source text that usually (but
blanchet@40073
   122
not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
blanchet@45380
   123
proof relies on the general-purpose \textit{metis} proof method, which
blanchet@45380
   124
integrates the Metis ATP in Isabelle/HOL with explicit inferences going through
blanchet@45380
   125
the kernel. Thus its results are correct by construction.
blanchet@36926
   126
blanchet@39320
   127
In this manual, we will explicitly invoke the \textbf{sledgehammer} command.
blanchet@44743
   128
Sledgehammer also provides an automatic mode that can be enabled via the ``Auto
blanchet@44743
   129
Sledgehammer'' option in Proof General's ``Isabelle'' menu. In this mode,
blanchet@44743
   130
Sledgehammer is run on every newly entered theorem. The time limit for Auto
blanchet@44743
   131
Sledgehammer and other automatic tools can be set using the ``Auto Tools Time
blanchet@44743
   132
Limit'' option.
blanchet@39320
   133
blanchet@36926
   134
\newbox\boxA
blanchet@46298
   135
\setbox\boxA=\hbox{\texttt{NOSPAM}}
blanchet@36926
   136
blanchet@46298
   137
\newcommand\authoremail{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
blanchet@42763
   138
in.\allowbreak tum.\allowbreak de}}
blanchet@42763
   139
blanchet@40689
   140
To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is
blanchet@40689
   141
imported---this is rarely a problem in practice since it is part of
blanchet@40689
   142
\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's
blanchet@36926
   143
\texttt{src/HOL/Metis\_Examples} directory.
blanchet@36926
   144
Comments and bug reports concerning Sledgehammer or this manual should be
blanchet@42883
   145
directed to the author at \authoremail.
blanchet@36926
   146
blanchet@36926
   147
\vskip2.5\smallskipamount
blanchet@36926
   148
blanchet@36926
   149
%\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
blanchet@36926
   150
%suggesting several textual improvements.
blanchet@36926
   151
blanchet@36926
   152
\section{Installation}
blanchet@36926
   153
\label{installation}
blanchet@36926
   154
blanchet@36926
   155
Sledgehammer is part of Isabelle, so you don't need to install it. However, it
blanchet@46242
   156
relies on third-party automatic provers (ATPs and SMT solvers).
blanchet@42763
   157
blanchet@46242
   158
Among the ATPs, E, LEO-II, Satallax, SPASS, and Vampire can be run locally; in
blanchet@45339
   159
addition, E, E-SInE, E-ToFoF, iProver, iProver-Eq, LEO-II, Satallax, SNARK,
blanchet@47561
   160
Vampire, and Waldmeister are available remotely via System\-On\-TPTP
blanchet@45339
   161
\cite{sutcliffe-2000}. If you want better performance, you should at least
blanchet@45339
   162
install E and SPASS locally.
blanchet@36926
   163
blanchet@46643
   164
Among the SMT solvers, Alt-Ergo, CVC3, Yices, and Z3 can be run locally, and
blanchet@46643
   165
CVC3 and Z3 can be run remotely on a TU M\"unchen server. If you want better
blanchet@46643
   166
performance and get the ability to replay proofs that rely on the \emph{smt}
blanchet@46643
   167
proof method without an Internet connection, you should at least install Z3
blanchet@46643
   168
locally.
blanchet@36926
   169
blanchet@46242
   170
There are three main ways to install automatic provers on your machine:
blanchet@36926
   171
blanchet@46242
   172
\begin{sloppy}
blanchet@46242
   173
\begin{enum}
blanchet@46242
   174
\item[\labelitemi] If you installed an official Isabelle package, it should
blanchet@46242
   175
already include properly setup executables for CVC3, E, SPASS, and Z3, ready to use.%
blanchet@46242
   176
\footnote{Vampire's and Yices's licenses prevent us from doing the same for
blanchet@46242
   177
these otherwise remarkable tools.}
blanchet@46242
   178
For Z3, you must additionally set the variable
blanchet@46242
   179
\texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
blanchet@46242
   180
noncommercial user, either in the environment in which Isabelle is
blanchet@46242
   181
launched or in your
blanchet@47561
   182
\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file.
blanchet@46242
   183
blanchet@46242
   184
\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, E,
blanchet@46242
   185
SPASS, and Z3 binary packages from \download. Extract the archives, then add a
blanchet@46242
   186
line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}%
blanchet@41747
   187
\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
blanchet@46242
   188
startup. Its value can be retrieved by executing \texttt{isabelle}
blanchet@41747
   189
\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
blanchet@46242
   190
file with the absolute path to CVC3, E, SPASS, or Z3. For example, if the
blanchet@46242
   191
\texttt{components} file does not exist yet and you extracted SPASS to
blanchet@47577
   192
\texttt{/usr/local/spass-3.8ds}, create it with the single line
blanchet@36926
   193
blanchet@36926
   194
\prew
blanchet@47577
   195
\texttt{/usr/local/spass-3.8ds}
blanchet@36926
   196
\postw
blanchet@36926
   197
blanchet@47561
   198
in it.
blanchet@38043
   199
blanchet@46242
   200
\item[\labelitemi] If you prefer to build E, LEO-II, Satallax, or SPASS
blanchet@46242
   201
manually, or found a Vampire executable somewhere (e.g.,
blanchet@46242
   202
\url{http://www.vprover.org/}), set the environment variable \texttt{E\_HOME},
blanchet@46242
   203
\texttt{LEO2\_HOME}, \texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or
blanchet@38043
   204
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
blanchet@46242
   205
\texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable.
blanchet@47577
   206
Sledgehammer has been tested with E 1.0 to 1.4, LEO-II 1.2.9, Satallax 2.2 and~2.3,
blanchet@47577
   207
SPASS 3.5, 3.7, and 3.8ds, and Vampire 0.6, 1.0, and 1.8%
blanchet@38063
   208
\footnote{Following the rewrite of Vampire, the counter for version numbers was
blanchet@44419
   209
reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent
blanchet@46242
   210
than 9.0 or 11.5.}%
blanchet@38063
   211
. Since the ATPs' output formats are neither documented nor stable, other
blanchet@47577
   212
versions might not work well with Sledgehammer. Ideally,
blanchet@47577
   213
you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
blanchet@46242
   214
\texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
blanchet@46242
   215
\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``1.4'').
blanchet@36926
   216
blanchet@46643
   217
Similarly, if you want to build Alt-Ergo or CVC3, or found a
blanchet@46242
   218
Yices or Z3 executable somewhere (e.g.,
blanchet@46242
   219
\url{http://yices.csl.sri.com/download.shtml} or
blanchet@46242
   220
\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html}),
blanchet@46242
   221
set the environment variable \texttt{CVC3\_\allowbreak SOLVER},
blanchet@46242
   222
\texttt{YICES\_SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of
blanchet@46242
   223
the executable, \emph{including the file name}. Sledgehammer has been tested
blanchet@47530
   224
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@46242
   225
Since the SMT solvers' output formats are somewhat unstable, other
blanchet@46242
   226
versions of the solvers might not work well with Sledgehammer. Ideally,
blanchet@46242
   227
also set \texttt{CVC3\_VERSION}, \texttt{YICES\_VERSION}, or
blanchet@46242
   228
\texttt{Z3\_VERSION} to the solver's version number (e.g., ``3.2'').
blanchet@46242
   229
\end{enum}
blanchet@46242
   230
\end{sloppy}
blanchet@36926
   231
blanchet@46242
   232
To check whether E, SPASS, Vampire, and/or Z3 are successfully installed, try
blanchet@46242
   233
out the example in \S\ref{first-steps}. If the remote versions of any of these
blanchet@46242
   234
provers is used (identified by the prefix ``\emph{remote\_\/}''), or if the
blanchet@46242
   235
local versions fail to solve the easy goal presented there, something must be
blanchet@46242
   236
wrong with the installation.
blanchet@46242
   237
blanchet@46242
   238
Remote prover invocation requires Perl with the World Wide Web Library
blanchet@46242
   239
(\texttt{libwww-perl}) installed. If you must use a proxy server to access the
blanchet@46242
   240
Internet, set the \texttt{http\_proxy} environment variable to the proxy, either
blanchet@46242
   241
in the environment in which Isabelle is launched or in your
blanchet@47561
   242
\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few
blanchet@46242
   243
examples:
blanchet@39152
   244
blanchet@39152
   245
\prew
blanchet@39153
   246
\texttt{http\_proxy=http://proxy.example.org} \\
blanchet@39153
   247
\texttt{http\_proxy=http://proxy.example.org:8080} \\
blanchet@39153
   248
\texttt{http\_proxy=http://joeblow:pAsSwRd@proxy.example.org}
blanchet@39152
   249
\postw
blanchet@37517
   250
blanchet@36926
   251
\section{First Steps}
blanchet@36926
   252
\label{first-steps}
blanchet@36926
   253
blanchet@36926
   254
To illustrate Sledgehammer in context, let us start a theory file and
blanchet@36926
   255
attempt to prove a simple lemma:
blanchet@36926
   256
blanchet@36926
   257
\prew
blanchet@36926
   258
\textbf{theory}~\textit{Scratch} \\
blanchet@36926
   259
\textbf{imports}~\textit{Main} \\
blanchet@36926
   260
\textbf{begin} \\[2\smallskipamount]
blanchet@36926
   261
%
blanchet@42945
   262
\textbf{lemma} ``$[a] = [b] \,\Longrightarrow\, a = b$'' \\
blanchet@36926
   263
\textbf{sledgehammer}
blanchet@36926
   264
\postw
blanchet@36926
   265
blanchet@37517
   266
Instead of issuing the \textbf{sledgehammer} command, you can also find
blanchet@37517
   267
Sledgehammer in the ``Commands'' submenu of the ``Isabelle'' menu in Proof
blanchet@37517
   268
General or press the Emacs key sequence C-c C-a C-s.
blanchet@37517
   269
Either way, Sledgehammer produces the following output after a few seconds:
blanchet@36926
   270
blanchet@36926
   271
\prew
blanchet@36926
   272
\slshape
blanchet@46242
   273
Sledgehammer: ``\textit{e\/}'' on goal \\
blanchet@42945
   274
$[a] = [b] \,\Longrightarrow\, a = b$ \\
blanchet@43054
   275
Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount]
blanchet@42945
   276
%
blanchet@46242
   277
Sledgehammer: ``\textit{z3\/}'' on goal \\
blanchet@46242
   278
$[a] = [b] \,\Longrightarrow\, a = b$ \\
blanchet@46242
   279
Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount]
blanchet@46242
   280
%
blanchet@46242
   281
Sledgehammer: ``\textit{vampire\/}'' on goal \\
blanchet@42945
   282
$[a] = [b] \,\Longrightarrow\, a = b$ \\
blanchet@43054
   283
Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
blanchet@36926
   284
%
blanchet@46242
   285
Sledgehammer: ``\textit{spass\/}'' on goal \\
blanchet@42945
   286
$[a] = [b] \,\Longrightarrow\, a = b$ \\
blanchet@43054
   287
Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
blanchet@36926
   288
%
blanchet@46242
   289
Sledgehammer: ``\textit{remote\_waldmeister\/}'' on goal \\
blanchet@43010
   290
$[a] = [b] \,\Longrightarrow\, a = b$ \\
blanchet@43054
   291
Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
blanchet@40073
   292
%
blanchet@47642
   293
Sledgehammer: ``\textit{remote\_e\_sine\/}'' on goal \\
blanchet@45063
   294
$[a] = [b] \,\Longrightarrow\, a = b$ \\
blanchet@46242
   295
Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms).
blanchet@36926
   296
\postw
blanchet@36926
   297
blanchet@47642
   298
Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel.
blanchet@42945
   299
Depending on which provers are installed and how many processor cores are
blanchet@42945
   300
available, some of the provers might be missing or present with a
blanchet@43010
   301
\textit{remote\_} prefix. Waldmeister is run only for unit equational problems,
blanchet@43010
   302
where the goal's conclusion is a (universally quantified) equation.
blanchet@36926
   303
blanchet@45380
   304
For each successful prover, Sledgehammer gives a one-liner proof that uses
blanchet@45380
   305
the \textit{metis} or \textit{smt} proof method. Approximate timings are shown
blanchet@45380
   306
in parentheses, indicating how fast the call is. You can click the proof to
blanchet@45380
   307
insert it into the theory text.
blanchet@36926
   308
blanchet@43054
   309
In addition, you can ask Sledgehammer for an Isar text proof by passing the
blanchet@42883
   310
\textit{isar\_proof} option (\S\ref{output-format}):
blanchet@36926
   311
blanchet@36926
   312
\prew
blanchet@36926
   313
\textbf{sledgehammer} [\textit{isar\_proof}]
blanchet@36926
   314
\postw
blanchet@36926
   315
blanchet@36926
   316
When Isar proof construction is successful, it can yield proofs that are more
blanchet@45380
   317
readable and also faster than the \textit{metis} or \textit{smt} one-liners.
blanchet@45380
   318
This feature is experimental and is only available for ATPs.
blanchet@36926
   319
blanchet@37517
   320
\section{Hints}
blanchet@37517
   321
\label{hints}
blanchet@37517
   322
blanchet@42884
   323
This section presents a few hints that should help you get the most out of
blanchet@46643
   324
Sledgehammer. Frequently asked questions are answered in
blanchet@45380
   325
\S\ref{frequently-asked-questions}.
blanchet@42884
   326
blanchet@46242
   327
%\newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak}
blanchet@46242
   328
\newcommand\point[1]{\subsection{\emph{#1}}}
blanchet@42763
   329
blanchet@42763
   330
\point{Presimplify the goal}
blanchet@42763
   331
blanchet@37517
   332
For best results, first simplify your problem by calling \textit{auto} or at
blanchet@42945
   333
least \textit{safe} followed by \textit{simp\_all}. The SMT solvers provide
blanchet@42945
   334
arithmetic decision procedures, but the ATPs typically do not (or if they do,
blanchet@42945
   335
Sledgehammer does not use it yet). Apart from Waldmeister, they are not
blanchet@42945
   336
especially good at heavy rewriting, but because they regard equations as
blanchet@42945
   337
undirected, they often prove theorems that require the reverse orientation of a
blanchet@42945
   338
\textit{simp} rule. Higher-order problems can be tackled, but the success rate
blanchet@42945
   339
is better for first-order problems. Hence, you may get better results if you
blanchet@42945
   340
first simplify the problem to remove higher-order features.
blanchet@37517
   341
blanchet@46242
   342
\point{Make sure E, SPASS, Vampire, and Z3 are locally installed}
blanchet@42763
   343
blanchet@42763
   344
Locally installed provers are faster and more reliable than those running on
blanchet@42763
   345
servers. See \S\ref{installation} for details on how to install them.
blanchet@42763
   346
blanchet@42763
   347
\point{Familiarize yourself with the most important options}
blanchet@42763
   348
blanchet@42763
   349
Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of
blanchet@42763
   350
the options are very specialized, but serious users of the tool should at least
blanchet@42763
   351
familiarize themselves with the following options:
blanchet@42763
   352
blanchet@42763
   353
\begin{enum}
blanchet@45516
   354
\item[\labelitemi] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies
blanchet@42884
   355
the automatic provers (ATPs and SMT solvers) that should be run whenever
blanchet@42884
   356
Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{e spass
blanchet@46242
   357
remote\_vampire\/}''). For convenience, you can omit ``\textit{provers}~=''
blanchet@43014
   358
and simply write the prover names as a space-separated list (e.g., ``\textit{e
blanchet@46242
   359
spass remote\_vampire\/}'').
blanchet@42763
   360
blanchet@45516
   361
\item[\labelitemi] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})
blanchet@42884
   362
specifies the maximum number of facts that should be passed to the provers. By
blanchet@42884
   363
default, the value is prover-dependent but varies between about 150 and 1000. If
blanchet@42884
   364
the provers time out, you can try lowering this value to, say, 100 or 50 and see
blanchet@42884
   365
if that helps.
blanchet@42763
   366
blanchet@45516
   367
\item[\labelitemi] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies
blanchet@45380
   368
that Isar proofs should be generated, instead of one-liner \textit{metis} or
blanchet@45380
   369
\textit{smt} proofs. The length of the Isar proofs can be controlled by setting
blanchet@42884
   370
\textit{isar\_shrink\_factor} (\S\ref{output-format}).
blanchet@43038
   371
blanchet@45516
   372
\item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
blanchet@43038
   373
provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
blanchet@43038
   374
asynchronously you should not hesitate to raise this limit to 60 or 120 seconds
blanchet@43038
   375
if you are the kind of user who can think clearly while ATPs are active.
blanchet@42763
   376
\end{enum}
blanchet@42763
   377
blanchet@42884
   378
Options can be set globally using \textbf{sledgehammer\_params}
blanchet@43010
   379
(\S\ref{command-syntax}). The command also prints the list of all available
blanchet@43010
   380
options with their current value. Fact selection can be influenced by specifying
blanchet@43010
   381
``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer} call
blanchet@43010
   382
to ensure that certain facts are included, or simply ``$(\textit{my\_facts})$''
blanchet@43010
   383
to force Sledgehammer to run only with $\textit{my\_facts}$.
blanchet@42763
   384
blanchet@42763
   385
\section{Frequently Asked Questions}
blanchet@42763
   386
\label{frequently-asked-questions}
blanchet@42763
   387
blanchet@42945
   388
This sections answers frequently (and infrequently) asked questions about
blanchet@42945
   389
Sledgehammer. It is a good idea to skim over it now even if you don't have any
blanchet@42945
   390
questions at this stage. And if you have any further questions not listed here,
blanchet@42945
   391
send them to the author at \authoremail.
blanchet@42945
   392
blanchet@43008
   393
\point{Which facts are passed to the automatic provers?}
blanchet@42883
   394
blanchet@43008
   395
The relevance filter assigns a score to every available fact (lemma, theorem,
blanchet@46300
   396
definition, or axiom) based upon how many constants that fact shares with the
blanchet@43008
   397
conjecture. This process iterates to include facts relevant to those just
blanchet@43008
   398
accepted, but with a decay factor to ensure termination. The constants are
blanchet@42883
   399
weighted to give unusual ones greater significance. The relevance filter copes
blanchet@42883
   400
best when the conjecture contains some unusual constants; if all the constants
blanchet@42883
   401
are common, it is unable to discriminate among the hundreds of facts that are
blanchet@42883
   402
picked up. The relevance filter is also memoryless: It has no information about
blanchet@42883
   403
how many times a particular fact has been used in a proof, and it cannot learn.
blanchet@42763
   404
blanchet@42883
   405
The number of facts included in a problem varies from prover to prover, since
blanchet@43008
   406
some provers get overwhelmed more easily than others. You can show the number of
blanchet@42883
   407
facts given using the \textit{verbose} option (\S\ref{output-format}) and the
blanchet@42883
   408
actual facts using \textit{debug} (\S\ref{output-format}).
blanchet@42883
   409
blanchet@42883
   410
Sledgehammer is good at finding short proofs combining a handful of existing
blanchet@42883
   411
lemmas. If you are looking for longer proofs, you must typically restrict the
blanchet@42884
   412
number of facts, by setting the \textit{max\_relevant} option
blanchet@43574
   413
(\S\ref{relevance-filter}) to, say, 25 or 50.
blanchet@42883
   414
blanchet@42996
   415
You can also influence which facts are actually selected in a number of ways. If
blanchet@42996
   416
you simply want to ensure that a fact is included, you can specify it using the
blanchet@42996
   417
``$(\textit{add}{:}~\textit{my\_facts})$'' syntax. For example:
blanchet@42996
   418
%
blanchet@42996
   419
\prew
blanchet@42996
   420
\textbf{sledgehammer} (\textit{add}: \textit{hd.simps} \textit{tl.simps})
blanchet@42996
   421
\postw
blanchet@42996
   422
%
blanchet@42996
   423
The specified facts then replace the least relevant facts that would otherwise be
blanchet@42996
   424
included; the other selected facts remain the same.
blanchet@42996
   425
If you want to direct the selection in a particular direction, you can specify
blanchet@42996
   426
the facts via \textbf{using}:
blanchet@42996
   427
%
blanchet@42996
   428
\prew
blanchet@42996
   429
\textbf{using} \textit{hd.simps} \textit{tl.simps} \\
blanchet@42996
   430
\textbf{sledgehammer}
blanchet@42996
   431
\postw
blanchet@42996
   432
%
blanchet@42996
   433
The facts are then more likely to be selected than otherwise, and if they are
blanchet@42996
   434
selected at iteration $j$ they also influence which facts are selected at
blanchet@42996
   435
iterations $j + 1$, $j + 2$, etc. To give them even more weight, try
blanchet@42996
   436
%
blanchet@42996
   437
\prew
blanchet@42996
   438
\textbf{using} \textit{hd.simps} \textit{tl.simps} \\
blanchet@42996
   439
\textbf{apply}~\textbf{--} \\
blanchet@42996
   440
\textbf{sledgehammer}
blanchet@42996
   441
\postw
blanchet@42996
   442
blanchet@46300
   443
\point{Why does Metis fail to reconstruct the proof?}
blanchet@46300
   444
blanchet@46300
   445
There are many reasons. If Metis runs seemingly forever, that is a sign that the
blanchet@46300
   446
proof is too difficult for it. Metis's search is complete, so it should
blanchet@46300
   447
eventually find it, but that's little consolation. There are several possible
blanchet@46300
   448
solutions:
blanchet@46300
   449
blanchet@46300
   450
\begin{enum}
blanchet@46300
   451
\item[\labelitemi] Try the \textit{isar\_proof} option (\S\ref{output-format}) to
blanchet@46300
   452
obtain a step-by-step Isar proof where each step is justified by \textit{metis}.
blanchet@46300
   453
Since the steps are fairly small, \textit{metis} is more likely to be able to
blanchet@46300
   454
replay them.
blanchet@46300
   455
blanchet@46300
   456
\item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}. It
blanchet@46300
   457
is usually stronger, but you need to either have Z3 available to replay the
blanchet@46300
   458
proofs, trust the SMT solver, or use certificates. See the documentation in the
blanchet@46300
   459
\emph{SMT} theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}) for details.
blanchet@46300
   460
blanchet@46300
   461
\item[\labelitemi] Try the \textit{blast} or \textit{auto} proof methods, passing
blanchet@46300
   462
the necessary facts via \textbf{unfolding}, \textbf{using}, \textit{intro}{:},
blanchet@46300
   463
\textit{elim}{:}, \textit{dest}{:}, or \textit{simp}{:}, as appropriate.
blanchet@46300
   464
\end{enum}
blanchet@46300
   465
blanchet@46300
   466
In some rare cases, \textit{metis} fails fairly quickly, and you get the error
blanchet@46300
   467
message
blanchet@46300
   468
blanchet@46300
   469
\prew
blanchet@46300
   470
\slshape
blanchet@46300
   471
One-line proof reconstruction failed.
blanchet@46300
   472
\postw
blanchet@46300
   473
blanchet@46300
   474
This message indicates that Sledgehammer determined that the goal is provable,
blanchet@46300
   475
but the proof is, for technical reasons, beyond \textit{metis}'s power. You can
blanchet@46300
   476
then try again with the \textit{strict} option (\S\ref{problem-encoding}).
blanchet@46300
   477
blanchet@46640
   478
If the goal is actually unprovable and you did not specify an unsound encoding
blanchet@46300
   479
using \textit{type\_enc} (\S\ref{problem-encoding}), this is a bug, and you are
blanchet@46300
   480
strongly encouraged to report this to the author at \authoremail.
blanchet@46300
   481
blanchet@46242
   482
\point{Why are the generated Isar proofs so ugly/broken?}
blanchet@42883
   483
blanchet@46300
   484
The current implementation of the Isar proof feature,
blanchet@46300
   485
enabled by the \textit{isar\_proof} option (\S\ref{output-format}),
blanchet@46300
   486
is highly experimental. Work on a new implementation has begun. There is a large body of
blanchet@42883
   487
research into transforming resolution proofs into natural deduction proofs (such
blanchet@42883
   488
as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
blanchet@42883
   489
set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
blanchet@42883
   490
value or to try several provers and keep the nicest-looking proof.
blanchet@42883
   491
blanchet@46300
   492
\point{How can I tell whether a suggested proof is sound?}
blanchet@46300
   493
blanchet@46300
   494
Earlier versions of Sledgehammer often suggested unsound proofs---either proofs
blanchet@46300
   495
of nontheorems or simply proofs that rely on type-unsound inferences. This
blanchet@46640
   496
is a thing of the past, unless you explicitly specify an unsound encoding
blanchet@46300
   497
using \textit{type\_enc} (\S\ref{problem-encoding}).
blanchet@46300
   498
%
blanchet@46300
   499
Officially, the only form of ``unsoundness'' that lurks in the sound
blanchet@46300
   500
encodings is related to missing characteristic theorems of datatypes. For
blanchet@46300
   501
example,
blanchet@46300
   502
blanchet@46300
   503
\prew
blanchet@46300
   504
\textbf{lemma}~``$\exists \mathit{xs}.\; \mathit{xs} \neq []$'' \\
blanchet@46300
   505
\textbf{sledgehammer} ()
blanchet@46300
   506
\postw
blanchet@46300
   507
blanchet@46300
   508
suggests an argumentless \textit{metis} call that fails. However, the conjecture
blanchet@46300
   509
does actually hold, and the \textit{metis} call can be repaired by adding
blanchet@46300
   510
\textit{list.distinct}.
blanchet@46300
   511
%
blanchet@46300
   512
We hope to address this problem in a future version of Isabelle. In the
blanchet@46300
   513
meantime, you can avoid it by passing the \textit{strict} option
blanchet@46300
   514
(\S\ref{problem-encoding}).
blanchet@46300
   515
blanchet@46298
   516
\point{What are the \textit{full\_types}, \textit{no\_types}, and
blanchet@46298
   517
\textit{mono\_tags} arguments to Metis?}
blanchet@42883
   518
blanchet@46298
   519
The \textit{metis}~(\textit{full\_types}) proof method
blanchet@46298
   520
and its cousin \textit{metis}~(\textit{mono\_tags}) are fully-typed
blanchet@43228
   521
version of Metis. It is somewhat slower than \textit{metis}, but the proof
blanchet@43228
   522
search is fully typed, and it also includes more powerful rules such as the
blanchet@45516
   523
axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in
blanchet@43228
   524
higher-order places (e.g., in set comprehensions). The method kicks in
blanchet@43228
   525
automatically as a fallback when \textit{metis} fails, and it is sometimes
blanchet@43228
   526
generated by Sledgehammer instead of \textit{metis} if the proof obviously
blanchet@43228
   527
requires type information or if \textit{metis} failed when Sledgehammer
blanchet@43228
   528
preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with
blanchet@46298
   529
various options for up to 3 seconds each time to ensure that the generated
blanchet@46298
   530
one-line proofs actually work and to display timing information. This can be
blanchet@47036
   531
configured using the \textit{preplay\_timeout} and \textit{dont\_preplay}
blanchet@47036
   532
options (\S\ref{timeouts}).)
blanchet@46298
   533
%
blanchet@43229
   534
At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types})
blanchet@43229
   535
uses no type information at all during the proof search, which is more efficient
blanchet@43229
   536
but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally
blanchet@43229
   537
generated by Sledgehammer.
blanchet@46298
   538
%
blanchet@46298
   539
See the \textit{type\_enc} option (\S\ref{problem-encoding}) for details.
blanchet@43229
   540
blanchet@46298
   541
Incidentally, if you ever see warnings such as
blanchet@42883
   542
blanchet@42883
   543
\prew
blanchet@43007
   544
\slshape
blanchet@43228
   545
Metis: Falling back on ``\textit{metis} (\textit{full\_types})''.
blanchet@42883
   546
\postw
blanchet@42883
   547
blanchet@45380
   548
for a successful \textit{metis} proof, you can advantageously pass the
blanchet@43228
   549
\textit{full\_types} option to \textit{metis} directly.
blanchet@43228
   550
blanchet@46366
   551
\point{And what are the \textit{lifting} and \textit{hide\_lams} arguments
blanchet@46298
   552
to Metis?}
blanchet@46298
   553
blanchet@46298
   554
Orthogonally to the encoding of types, it is important to choose an appropriate
blanchet@46298
   555
translation of $\lambda$-abstractions. Metis supports three translation schemes,
blanchet@46298
   556
in decreasing order of power: Curry combinators (the default),
blanchet@46298
   557
$\lambda$-lifting, and a ``hiding'' scheme that disables all reasoning under
blanchet@46298
   558
$\lambda$-abstractions. The more powerful schemes also give the automatic
blanchet@46298
   559
provers more rope to hang themselves. See the \textit{lam\_trans} option (\S\ref{problem-encoding}) for details.
blanchet@46298
   560
blanchet@43054
   561
\point{Are generated proofs minimal?}
blanchet@43036
   562
blanchet@43054
   563
Automatic provers frequently use many more facts than are necessary.
blanchet@43054
   564
Sledgehammer inclues a minimization tool that takes a set of facts returned by a
blanchet@45380
   565
given prover and repeatedly calls the same prover, \textit{metis}, or
blanchet@45380
   566
\textit{smt} with subsets of those axioms in order to find a minimal set.
blanchet@45380
   567
Reducing the number of axioms typically improves Metis's speed and success rate,
blanchet@45380
   568
while also removing superfluous clutter from the proof scripts.
blanchet@43036
   569
blanchet@43229
   570
In earlier versions of Sledgehammer, generated proofs were systematically
blanchet@43229
   571
accompanied by a suggestion to invoke the minimization tool. This step is now
blanchet@43229
   572
performed implicitly if it can be done in a reasonable amount of time (something
blanchet@43229
   573
that can be guessed from the number of facts in the original proof and the time
blanchet@45708
   574
it took to find or preplay it).
blanchet@43036
   575
blanchet@45163
   576
In addition, some provers (e.g., Yices) do not provide proofs or sometimes
blanchet@45163
   577
produce incomplete proofs. The minimizer is then invoked to find out which facts
blanchet@46640
   578
are actually needed from the (large) set of facts that was initially given to
blanchet@45163
   579
the prover. Finally, if a prover returns a proof with lots of facts, the
blanchet@45163
   580
minimizer is invoked automatically since Metis would be unlikely to re-find the
blanchet@45163
   581
proof.
blanchet@45708
   582
%
blanchet@45708
   583
Automatic minimization can be forced or disabled using the \textit{minimize}
blanchet@45708
   584
option (\S\ref{mode-of-operation}).
blanchet@43036
   585
blanchet@43008
   586
\point{A strange error occurred---what should I do?}
blanchet@42763
   587
blanchet@42763
   588
Sledgehammer tries to give informative error messages. Please report any strange
blanchet@42883
   589
error to the author at \authoremail. This applies double if you get the message
blanchet@42763
   590
blanchet@42883
   591
\prew
blanchet@42763
   592
\slshape
blanchet@46242
   593
The prover found a type-unsound proof involving ``\textit{foo\/}'',
blanchet@46242
   594
``\textit{bar\/}'', and ``\textit{baz\/}'' even though a supposedly type-sound
blanchet@43005
   595
encoding was used (or, less likely, your axioms are inconsistent). You might
blanchet@43005
   596
want to report this to the Isabelle developers.
blanchet@42883
   597
\postw
blanchet@42763
   598
blanchet@42763
   599
\point{Auto can solve it---why not Sledgehammer?}
blanchet@42763
   600
blanchet@42763
   601
Problems can be easy for \textit{auto} and difficult for automatic provers, but
blanchet@42763
   602
the reverse is also true, so don't be discouraged if your first attempts fail.
blanchet@39320
   603
Because the system refers to all theorems known to Isabelle, it is particularly
blanchet@39320
   604
suitable when your goal has a short proof from lemmas that you don't know about.
blanchet@37517
   605
blanchet@42883
   606
\point{Why are there so many options?}
blanchet@42883
   607
blanchet@42883
   608
Sledgehammer's philosophy should work out of the box, without user guidance.
blanchet@42883
   609
Many of the options are meant to be used mostly by the Sledgehammer developers
blanchet@42883
   610
for experimentation purposes. Of course, feel free to experiment with them if
blanchet@42883
   611
you are so inclined.
blanchet@42883
   612
blanchet@36926
   613
\section{Command Syntax}
blanchet@36926
   614
\label{command-syntax}
blanchet@36926
   615
blanchet@46242
   616
\subsection{Sledgehammer}
blanchet@46242
   617
blanchet@36926
   618
Sledgehammer can be invoked at any point when there is an open goal by entering
blanchet@36926
   619
the \textbf{sledgehammer} command in the theory file. Its general syntax is as
blanchet@36926
   620
follows:
blanchet@36926
   621
blanchet@36926
   622
\prew
blanchet@43216
   623
\textbf{sledgehammer} \qty{subcommand}$^?$ \qty{options}$^?$ \qty{facts\_override}$^?$ \qty{num}$^?$
blanchet@36926
   624
\postw
blanchet@36926
   625
blanchet@36926
   626
For convenience, Sledgehammer is also available in the ``Commands'' submenu of
blanchet@36926
   627
the ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c
blanchet@36926
   628
C-a C-s. This is equivalent to entering the \textbf{sledgehammer} command with
blanchet@36926
   629
no arguments in the theory text.
blanchet@36926
   630
blanchet@43216
   631
In the general syntax, the \qty{subcommand} may be any of the following:
blanchet@36926
   632
blanchet@36926
   633
\begin{enum}
blanchet@45516
   634
\item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on
blanchet@43216
   635
subgoal number \qty{num} (1 by default), with the given options and facts.
blanchet@36926
   636
blanchet@45516
   637
\item[\labelitemi] \textbf{\textit{min}:} Attempts to minimize the facts
blanchet@43216
   638
specified in the \qty{facts\_override} argument to obtain a simpler proof
blanchet@36926
   639
involving fewer facts. The options and goal number are as for \textit{run}.
blanchet@36926
   640
blanchet@45516
   641
\item[\labelitemi] \textbf{\textit{messages}:} Redisplays recent messages issued
blanchet@40203
   642
by Sledgehammer. This allows you to examine results that might have been lost
blanchet@43216
   643
due to Sledgehammer's asynchronous nature. The \qty{num} argument specifies a
blanchet@47530
   644
limit on the number of messages to display (10 by default).
blanchet@36926
   645
blanchet@45516
   646
\item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of
blanchet@41724
   647
automatic provers supported by Sledgehammer. See \S\ref{installation} and
blanchet@41724
   648
\S\ref{mode-of-operation} for more information on how to install automatic
blanchet@41724
   649
provers.
blanchet@36926
   650
blanchet@45516
   651
\item[\labelitemi] \textbf{\textit{running\_provers}:} Prints information about
blanchet@40059
   652
currently running automatic provers, including elapsed runtime and remaining
blanchet@40059
   653
time until timeout.
blanchet@36926
   654
blanchet@45516
   655
\item[\labelitemi] \textbf{\textit{kill\_provers}:} Terminates all running
blanchet@40059
   656
automatic provers.
blanchet@36926
   657
blanchet@45516
   658
\item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
blanchet@36926
   659
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
blanchet@36926
   660
\end{enum}
blanchet@36926
   661
blanchet@43216
   662
Sledgehammer's behavior can be influenced by various \qty{options}, which can be
blanchet@43216
   663
specified in brackets after the \textbf{sledgehammer} command. The
blanchet@43216
   664
\qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
blanchet@46242
   665
\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. For
blanchet@36926
   666
example:
blanchet@36926
   667
blanchet@36926
   668
\prew
blanchet@43216
   669
\textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120]
blanchet@36926
   670
\postw
blanchet@36926
   671
blanchet@36926
   672
Default values can be set using \textbf{sledgehammer\_\allowbreak params}:
blanchet@36926
   673
blanchet@36926
   674
\prew
blanchet@43216
   675
\textbf{sledgehammer\_params} \qty{options}
blanchet@36926
   676
\postw
blanchet@36926
   677
blanchet@36926
   678
The supported options are described in \S\ref{option-reference}.
blanchet@36926
   679
blanchet@43216
   680
The \qty{facts\_override} argument lets you alter the set of facts that go
blanchet@43216
   681
through the relevance filter. It may be of the form ``(\qty{facts})'', where
blanchet@43216
   682
\qty{facts} is a space-separated list of Isabelle facts (theorems, local
blanchet@36926
   683
assumptions, etc.), in which case the relevance filter is bypassed and the given
blanchet@43216
   684
facts are used. It may also be of the form ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}})'',
blanchet@43216
   685
``(\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', or ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}}\
blanchet@43216
   686
\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', where the relevance filter is instructed to
blanchet@43216
   687
proceed as usual except that it should consider \qty{facts\/_{\mathrm{1}}}
blanchet@43216
   688
highly-relevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant.
blanchet@36926
   689
blanchet@39320
   690
You can instruct Sledgehammer to run automatically on newly entered theorems by
blanchet@44743
   691
enabling the ``Auto Sledgehammer'' option in Proof General's ``Isabelle'' menu.
blanchet@44743
   692
For automatic runs, only the first prover set using \textit{provers}
blanchet@42736
   693
(\S\ref{mode-of-operation}) is considered, fewer facts are passed to the prover,
blanchet@46300
   694
\textit{slice} (\S\ref{mode-of-operation}) is disabled, \textit{strict}
blanchet@43574
   695
(\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format})
blanchet@43038
   696
and \textit{debug} (\S\ref{output-format}) are disabled, and \textit{timeout}
blanchet@43038
   697
(\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in Proof
blanchet@43038
   698
General's ``Isabelle'' menu. Sledgehammer's output is also more concise.
blanchet@39320
   699
blanchet@46242
   700
\subsection{Metis}
blanchet@46242
   701
blanchet@43216
   702
The \textit{metis} proof method has the syntax
blanchet@43216
   703
blanchet@43216
   704
\prew
blanchet@45518
   705
\textbf{\textit{metis}}~(\qty{options})${}^?$~\qty{facts}${}^?$
blanchet@43216
   706
\postw
blanchet@43216
   707
blanchet@45518
   708
where \qty{facts} is a list of arbitrary facts and \qty{options} is a
blanchet@45518
   709
comma-separated list consisting of at most one $\lambda$ translation scheme
blanchet@45518
   710
specification with the same semantics as Sledgehammer's \textit{lam\_trans}
blanchet@45518
   711
option (\S\ref{problem-encoding}) and at most one type encoding specification
blanchet@45518
   712
with the same semantics as Sledgehammer's \textit{type\_enc} option
blanchet@45518
   713
(\S\ref{problem-encoding}).
blanchet@45518
   714
%
blanchet@45518
   715
The supported $\lambda$ translation schemes are \textit{hide\_lams},
blanchet@46366
   716
\textit{lifting}, and \textit{combs} (the default).
blanchet@45518
   717
%
blanchet@45518
   718
All the untyped type encodings listed in \S\ref{problem-encoding} are supported.
blanchet@45518
   719
For convenience, the following aliases are provided:
blanchet@45518
   720
\begin{enum}
blanchet@46300
   721
\item[\labelitemi] \textbf{\textit{full\_types}:} Synonym for \textit{poly\_guards\_query}.
blanchet@45518
   722
\item[\labelitemi] \textbf{\textit{partial\_types}:} Synonym for \textit{poly\_args}.
blanchet@45518
   723
\item[\labelitemi] \textbf{\textit{no\_types}:} Synonym for \textit{erased}.
blanchet@45518
   724
\end{enum}
blanchet@43216
   725
blanchet@36926
   726
\section{Option Reference}
blanchet@36926
   727
\label{option-reference}
blanchet@36926
   728
blanchet@43014
   729
\def\defl{\{}
blanchet@43014
   730
\def\defr{\}}
blanchet@43014
   731
blanchet@36926
   732
\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
blanchet@47036
   733
\def\optrueonly#1{\flushitem{\textit{#1} $\bigl[$= \textit{true}$\bigr]$\enskip}\nopagebreak\\[\parskip]}
blanchet@43014
   734
\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
blanchet@43014
   735
\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
blanchet@43014
   736
\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
blanchet@46409
   737
\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@36926
   738
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
blanchet@43014
   739
\def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]}
blanchet@43014
   740
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]}
blanchet@36926
   741
\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
blanchet@36926
   742
\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
blanchet@43014
   743
\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
blanchet@36926
   744
blanchet@36926
   745
Sledgehammer's options are categorized as follows:\ mode of operation
blanchet@38984
   746
(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}),
blanchet@38984
   747
relevance filter (\S\ref{relevance-filter}), output format
blanchet@43038
   748
(\S\ref{output-format}), authentication (\S\ref{authentication}), and timeouts
blanchet@43038
   749
(\S\ref{timeouts}).
blanchet@36926
   750
blanchet@36926
   751
The descriptions below refer to the following syntactic quantities:
blanchet@36926
   752
blanchet@36926
   753
\begin{enum}
blanchet@45516
   754
\item[\labelitemi] \qtybf{string}: A string.
blanchet@45516
   755
\item[\labelitemi] \qtybf{bool\/}: \textit{true} or \textit{false}.
blanchet@45516
   756
\item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or
blanchet@40203
   757
\textit{smart}.
blanchet@45516
   758
\item[\labelitemi] \qtybf{int\/}: An integer.
blanchet@45516
   759
%\item[\labelitemi] \qtybf{float\/}: A floating-point number (e.g., 2.5).
blanchet@45516
   760
\item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers
blanchet@40343
   761
(e.g., 0.6 0.95).
blanchet@45516
   762
\item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}.
blanchet@45516
   763
\item[\labelitemi] \qtybf{float\_or\_none\/}: A floating-point number (e.g., 60 or
blanchet@43036
   764
0.5) expressing a number of seconds, or the keyword \textit{none} ($\infty$
blanchet@43036
   765
seconds).
blanchet@36926
   766
\end{enum}
blanchet@36926
   767
blanchet@43217
   768
Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
blanchet@43217
   769
have a negated counterpart (e.g., \textit{blocking} vs.\
blanchet@46242
   770
\textit{non\_blocking}). When setting them, ``= \textit{true\/}'' may be omitted.
blanchet@36926
   771
blanchet@36926
   772
\subsection{Mode of Operation}
blanchet@36926
   773
\label{mode-of-operation}
blanchet@36926
   774
blanchet@36926
   775
\begin{enum}
blanchet@43014
   776
\opnodefaultbrk{provers}{string}
blanchet@40059
   777
Specifies the automatic provers to use as a space-separated list (e.g.,
blanchet@46299
   778
``\textit{e}~\textit{spass}~\textit{remote\_vampire\/}'').
blanchet@46299
   779
Provers can be run locally or remotely; see \S\ref{installation} for
blanchet@46299
   780
installation instructions.
blanchet@46299
   781
blanchet@46299
   782
The following local provers are supported:
blanchet@36926
   783
blanchet@36926
   784
\begin{enum}
blanchet@46643
   785
\item[\labelitemi] \textbf{\textit{alt\_ergo}:} Alt-Ergo is a polymorphic
blanchet@46643
   786
SMT solver developed by Bobot et al.\ \cite{alt-ergo}.
blanchet@46643
   787
It supports the TPTP polymorphic typed first-order format (TFF1) via Why3
blanchet@46643
   788
\cite{why3}. It is included for experimental purposes. To use Alt-Ergo, set the
blanchet@46643
   789
environment variable \texttt{WHY3\_HOME} to the directory that contains the
blanchet@46643
   790
\texttt{why3} executable. Sledgehammer has been tested with Alt-Ergo 0.93 and an
blanchet@46643
   791
unidentified development version of Why3.
blanchet@46643
   792
blanchet@45516
   793
\item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
blanchet@42945
   794
Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
blanchet@42945
   795
set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
blanchet@46242
   796
executable, including the file name, or install the prebuilt CVC3 package from
blanchet@46299
   797
\download. Sledgehammer has been tested with version 2.2.
blanchet@42945
   798
blanchet@45516
   799
\item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover
blanchet@42964
   800
developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment
blanchet@42964
   801
variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
blanchet@47056
   802
executable and \texttt{E\_VERSION} to the version number (e.g., ``1.4''), or
blanchet@47056
   803
install the prebuilt E package from \download. Sledgehammer has been tested with
blanchet@47056
   804
versions 1.0 to 1.4.
blanchet@36926
   805
blanchet@45516
   806
\item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic
blanchet@44098
   807
higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
blanchet@46242
   808
with support for the TPTP typed higher-order syntax (THF0). To use LEO-II, set
blanchet@46242
   809
the environment variable \texttt{LEO2\_HOME} to the directory that contains the
blanchet@46242
   810
\texttt{leo} executable. Sledgehammer requires version 1.2.9 or above.
blanchet@44098
   811
blanchet@45516
   812
\item[\labelitemi] \textbf{\textit{metis}:} Although it is much less powerful than
blanchet@44098
   813
the external provers, Metis itself can be used for proof search.
blanchet@44098
   814
blanchet@45516
   815
\item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic
blanchet@44098
   816
higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
blanchet@46242
   817
support for the TPTP typed higher-order syntax (THF0). To use Satallax, set the
blanchet@46242
   818
environment variable \texttt{SATALLAX\_HOME} to the directory that contains the
blanchet@46242
   819
\texttt{satallax} executable. Sledgehammer requires version 2.2 or above.
blanchet@44098
   820
blanchet@45516
   821
\item[\labelitemi] \textbf{\textit{smt}:} The \textit{smt} proof method with the
blanchet@45555
   822
current settings (usually:\ Z3 with proof reconstruction).
blanchet@45380
   823
blanchet@45516
   824
\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution
blanchet@42964
   825
prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
blanchet@42964
   826
To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
blanchet@47056
   827
that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the
blanchet@47577
   828
version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from
blanchet@47056
   829
\download. Sledgehammer requires version 3.5 or above.
blanchet@36926
   830
blanchet@45516
   831
\item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution
blanchet@42964
   832
prover developed by Andrei Voronkov and his colleagues
blanchet@42964
   833
\cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
blanchet@42964
   834
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
blanchet@44419
   835
executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``1.8'').
blanchet@46242
   836
Sledgehammer has been tested with versions 0.6, 1.0, and 1.8.
blanchet@46643
   837
Versions above 1.8 support the TPTP typed first-order format (TFF0).
blanchet@40942
   838
blanchet@45516
   839
\item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at
blanchet@44098
   840
SRI \cite{yices}. To use Yices, set the environment variable
blanchet@44098
   841
\texttt{YICES\_SOLVER} to the complete path of the executable, including the
blanchet@45864
   842
file name. Sledgehammer has been tested with version 1.0.28.
blanchet@44098
   843
blanchet@45516
   844
\item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
blanchet@41740
   845
Microsoft Research \cite{z3}. To use Z3, set the environment variable
blanchet@41740
   846
\texttt{Z3\_SOLVER} to the complete path of the executable, including the file
blanchet@44421
   847
name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
blanchet@45864
   848
noncommercial user. Sledgehammer has been tested with versions 3.0 to 3.2.
blanchet@41740
   849
blanchet@45516
   850
\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
blanchet@45516
   851
an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
blanchet@45864
   852
formats (FOF and TFF0). It is included for experimental purposes. It
blanchet@45864
   853
requires version 3.0 or above. To use it, set the environment variable
blanchet@45864
   854
\texttt{Z3\_HOME} to the directory that contains the \texttt{z3}
blanchet@45864
   855
executable.
blanchet@42945
   856
\end{enum}
blanchet@42945
   857
blanchet@46299
   858
The following remote provers are supported:
blanchet@42945
   859
blanchet@42945
   860
\begin{enum}
blanchet@45516
   861
\item[\labelitemi] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
blanchet@42945
   862
on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
blanchet@42945
   863
point).
blanchet@40073
   864
blanchet@45516
   865
\item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs
blanchet@36926
   866
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
blanchet@36926
   867
blanchet@45516
   868
\item[\labelitemi] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover
blanchet@47075
   869
developed by Kry\v stof Hoder \cite{sine} based on E. It runs on Geoff
blanchet@47075
   870
Sutcliffe's Miami servers.
blanchet@44091
   871
blanchet@45516
   872
\item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
blanchet@44091
   873
developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
blanchet@45516
   874
servers. This ATP supports the TPTP typed first-order format (TFF0). The
blanchet@44091
   875
remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
blanchet@44091
   876
blanchet@45516
   877
\item[\labelitemi] \textbf{\textit{remote\_iprover}:} iProver is a pure
blanchet@45339
   878
instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. The
blanchet@45339
   879
remote version of iProver runs on Geoff Sutcliffe's Miami servers
blanchet@45339
   880
\cite{sutcliffe-2000}.
blanchet@45339
   881
blanchet@45516
   882
\item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} iProver-Eq is an
blanchet@45339
   883
instantiation-based prover with native support for equality developed by
blanchet@45339
   884
Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. The
blanchet@45339
   885
remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers
blanchet@45339
   886
\cite{sutcliffe-2000}.
blanchet@45339
   887
blanchet@45516
   888
\item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
blanchet@44098
   889
runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
blanchet@42964
   890
blanchet@45516
   891
\item[\labelitemi] \textbf{\textit{remote\_satallax}:} The remote version of
blanchet@44098
   892
Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
blanchet@42964
   893
blanchet@45516
   894
\item[\labelitemi] \textbf{\textit{remote\_snark}:} SNARK is a first-order
blanchet@43625
   895
resolution prover developed by Stickel et al.\ \cite{snark}. It supports the
blanchet@45516
   896
TPTP typed first-order format (TFF0). The remote version of SNARK runs on
blanchet@43625
   897
Geoff Sutcliffe's Miami servers.
blanchet@40073
   898
blanchet@45516
   899
\item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of
blanchet@44419
   900
Vampire runs on Geoff Sutcliffe's Miami servers. Version 1.8 is used.
blanchet@42945
   901
blanchet@45516
   902
\item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
blanchet@42945
   903
equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be
blanchet@43625
   904
used to prove universally quantified equations using unconditional equations,
blanchet@43625
   905
corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister
blanchet@43625
   906
runs on Geoff Sutcliffe's Miami servers.
blanchet@41738
   907
blanchet@45516
   908
\item[\labelitemi] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
blanchet@40942
   909
servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
blanchet@40942
   910
point).
blanchet@40073
   911
blanchet@45516
   912
\item[\labelitemi] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3
blanchet@44423
   913
with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
blanchet@36926
   914
\end{enum}
blanchet@36926
   915
blanchet@47642
   916
By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever
blanchet@44091
   917
the SMT module's \textit{smt\_solver} configuration option is set to), and (if
blanchet@44091
   918
appropriate) Waldmeister in parallel---either locally or remotely, depending on
blanchet@44091
   919
the number of processor cores available. For historical reasons, the default
blanchet@44091
   920
value of this option can be overridden using the option ``Sledgehammer:
blanchet@44743
   921
Provers'' in Proof General's ``Isabelle'' menu.
blanchet@36926
   922
blanchet@44743
   923
It is generally a good idea to run several provers in parallel. Running E,
blanchet@44743
   924
SPASS, and Vampire for 5~seconds yields a similar success rate to running the
blanchet@44743
   925
most effective of these for 120~seconds \cite{boehme-nipkow-2010}.
blanchet@40059
   926
blanchet@43053
   927
For the \textit{min} subcommand, the default prover is \textit{metis}. If
blanchet@43053
   928
several provers are set, the first one is used.
blanchet@43053
   929
blanchet@40059
   930
\opnodefault{prover}{string}
blanchet@40059
   931
Alias for \textit{provers}.
blanchet@40059
   932
blanchet@38983
   933
\opfalse{blocking}{non\_blocking}
blanchet@38983
   934
Specifies whether the \textbf{sledgehammer} command should operate
blanchet@38983
   935
synchronously. The asynchronous (non-blocking) mode lets the user start proving
blanchet@38983
   936
the putative theorem manually while Sledgehammer looks for a proof, but it can
blanchet@42995
   937
also be more confusing. Irrespective of the value of this option, Sledgehammer
blanchet@42995
   938
is always run synchronously for the new jEdit-based user interface or if
blanchet@42995
   939
\textit{debug} (\S\ref{output-format}) is enabled.
blanchet@38983
   940
blanchet@45708
   941
\optrue{slice}{dont\_slice}
blanchet@42443
   942
Specifies whether the time allocated to a prover should be sliced into several
blanchet@42443
   943
segments, each of which has its own set of possibly prover-dependent options.
blanchet@42446
   944
For SPASS and Vampire, the first slice tries the fast but incomplete
blanchet@42443
   945
set-of-support (SOS) strategy, whereas the second slice runs without it. For E,
blanchet@42446
   946
up to three slices are tried, with different weighted search strategies and
blanchet@42443
   947
number of facts. For SMT solvers, several slices are tried with the same options
blanchet@42446
   948
each time but fewer and fewer facts. According to benchmarks with a timeout of
blanchet@42446
   949
30 seconds, slicing is a valuable optimization, and you should probably leave it
blanchet@42446
   950
enabled unless you are conducting experiments. This option is implicitly
blanchet@42443
   951
disabled for (short) automatic runs.
blanchet@42443
   952
blanchet@42443
   953
\nopagebreak
blanchet@42443
   954
{\small See also \textit{verbose} (\S\ref{output-format}).}
blanchet@42443
   955
blanchet@45708
   956
\opsmart{minimize}{dont\_minimize}
blanchet@45708
   957
Specifies whether the minimization tool should be invoked automatically after
blanchet@45708
   958
proof search. By default, automatic minimization takes place only if
blanchet@45708
   959
it can be done in a reasonable amount of time (as determined by
blanchet@45708
   960
the number of facts in the original proof and the time it took to find or
blanchet@45708
   961
preplay it) or the proof involves an unreasonably large number of facts.
blanchet@45708
   962
blanchet@45708
   963
\nopagebreak
blanchet@47036
   964
{\small See also \textit{preplay\_timeout} (\S\ref{timeouts})
blanchet@47036
   965
and \textit{dont\_preplay} (\S\ref{timeouts}).}
blanchet@45708
   966
blanchet@36926
   967
\opfalse{overlord}{no\_overlord}
blanchet@36926
   968
Specifies whether Sledgehammer should put its temporary files in
blanchet@36926
   969
\texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
blanchet@36926
   970
debugging Sledgehammer but also unsafe if several instances of the tool are run
blanchet@36926
   971
simultaneously. The files are identified by the prefix \texttt{prob\_}; you may
blanchet@36926
   972
safely remove them after Sledgehammer has run.
blanchet@36926
   973
blanchet@36926
   974
\nopagebreak
blanchet@36926
   975
{\small See also \textit{debug} (\S\ref{output-format}).}
blanchet@36926
   976
\end{enum}
blanchet@36926
   977
blanchet@36926
   978
\subsection{Problem Encoding}
blanchet@36926
   979
\label{problem-encoding}
blanchet@36926
   980
blanchet@45516
   981
\newcommand\comb[1]{\const{#1}}
blanchet@45516
   982
blanchet@36926
   983
\begin{enum}
blanchet@45516
   984
\opdefault{lam\_trans}{string}{smart}
blanchet@45516
   985
Specifies the $\lambda$ translation scheme to use in ATP problems. The supported
blanchet@45516
   986
translation schemes are listed below:
blanchet@45516
   987
blanchet@45516
   988
\begin{enum}
blanchet@45516
   989
\item[\labelitemi] \textbf{\textit{hide\_lams}:} Hide the $\lambda$-abstractions
blanchet@45516
   990
by replacing them by unspecified fresh constants, effectively disabling all
blanchet@45516
   991
reasoning under $\lambda$-abstractions.
blanchet@45516
   992
blanchet@46366
   993
\item[\labelitemi] \textbf{\textit{lifting}:} Introduce a new
blanchet@45516
   994
supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions,
blanchet@45516
   995
defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting).
blanchet@45516
   996
blanchet@46366
   997
\item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry
blanchet@45516
   998
combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators
blanchet@45516
   999
enable the ATPs to synthesize $\lambda$-terms but tend to yield bulkier formulas
blanchet@45516
  1000
than $\lambda$-lifting: The translation is quadratic in the worst case, and the
blanchet@45516
  1001
equational definitions of the combinators are very prolific in the context of
blanchet@45516
  1002
resolution.
blanchet@45516
  1003
blanchet@46366
  1004
\item[\labelitemi] \textbf{\textit{combs\_and\_lifting}:} Introduce a new
blanchet@45516
  1005
supercombinator \const{c} for each cluster of $\lambda$-abstractions and characterize it both using a
blanchet@45516
  1006
lifted equation $\const{c}~x_1~\ldots~x_n = t$ and via Curry combinators.
blanchet@45516
  1007
blanchet@46366
  1008
\item[\labelitemi] \textbf{\textit{combs\_or\_lifting}:} For each cluster of
blanchet@46366
  1009
$\lambda$-abstractions, heuristically choose between $\lambda$-lifting and Curry
blanchet@46366
  1010
combinators.
blanchet@46366
  1011
blanchet@45516
  1012
\item[\labelitemi] \textbf{\textit{keep\_lams}:}
blanchet@45516
  1013
Keep the $\lambda$-abstractions in the generated problems. This is available
blanchet@45516
  1014
only with provers that support the THF0 syntax.
blanchet@45516
  1015
blanchet@45516
  1016
\item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used
blanchet@45516
  1017
depends on the ATP and should be the most efficient scheme for that ATP.
blanchet@45516
  1018
\end{enum}
blanchet@45516
  1019
blanchet@46366
  1020
For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting},
blanchet@46366
  1021
irrespective of the value of this option.
blanchet@45516
  1022
blanchet@46409
  1023
\opsmartx{uncurried\_aliases}{no\_uncurried\_aliases}
blanchet@46411
  1024
Specifies whether fresh function symbols should be generated as aliases for
blanchet@46411
  1025
applications of curried functions in ATP problems.
blanchet@46409
  1026
blanchet@43627
  1027
\opdefault{type\_enc}{string}{smart}
blanchet@43627
  1028
Specifies the type encoding to use in ATP problems. Some of the type encodings
blanchet@43627
  1029
are unsound, meaning that they can give rise to spurious proofs
blanchet@45380
  1030
(unreconstructible using \textit{metis}). The supported type encodings are
blanchet@46300
  1031
listed below, with an indication of their soundness in parentheses.
blanchet@46302
  1032
An asterisk (*) means that the encoding is slightly incomplete for
blanchet@46302
  1033
reconstruction with \textit{metis}, unless the \emph{strict} option (described
blanchet@46302
  1034
below) is enabled.
blanchet@42228
  1035
blanchet@42228
  1036
\begin{enum}
blanchet@45516
  1037
\item[\labelitemi] \textbf{\textit{erased} (very unsound):} No type information is
blanchet@46300
  1038
supplied to the ATP, not even to resolve overloading. Types are simply erased.
blanchet@42582
  1039
blanchet@45516
  1040
\item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using
blanchet@46300
  1041
a predicate \const{g}$(\tau, t)$ that guards bound
blanchet@43990
  1042
variables. Constants are annotated with their types, supplied as additional
blanchet@42887
  1043
arguments, to resolve overloading.
blanchet@42685
  1044
blanchet@45516
  1045
\item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
blanchet@46300
  1046
tagged with its type using a function $\const{t\/}(\tau, t)$.
blanchet@42887
  1047
blanchet@45516
  1048
\item[\labelitemi] \textbf{\textit{poly\_args} (unsound):}
blanchet@43990
  1049
Like for \textit{poly\_guards} constants are annotated with their types to
blanchet@43002
  1050
resolve overloading, but otherwise no type information is encoded. This
blanchet@43228
  1051
coincides with the default encoding used by the \textit{metis} command.
blanchet@42685
  1052
blanchet@45516
  1053
\item[\labelitemi]
blanchet@42722
  1054
\textbf{%
blanchet@44494
  1055
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\
blanchet@44494
  1056
\textit{raw\_mono\_args} (unsound):} \\
blanchet@43990
  1057
Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args},
blanchet@42722
  1058
respectively, but the problem is additionally monomorphized, meaning that type
blanchet@42722
  1059
variables are instantiated with heuristically chosen ground types.
blanchet@42722
  1060
Monomorphization can simplify reasoning but also leads to larger fact bases,
blanchet@42722
  1061
which can slow down the ATPs.
blanchet@42582
  1062
blanchet@45516
  1063
\item[\labelitemi]
blanchet@42722
  1064
\textbf{%
blanchet@44494
  1065
\textit{mono\_guards}, \textit{mono\_tags} (sound);
blanchet@44494
  1066
\textit{mono\_args} (unsound):} \\
blanchet@42722
  1067
Similar to
blanchet@44494
  1068
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and
blanchet@44494
  1069
\textit{raw\_mono\_args}, respectively but types are mangled in constant names
blanchet@44494
  1070
instead of being supplied as ground term arguments. The binary predicate
blanchet@46300
  1071
$\const{g}(\tau, t)$ becomes a unary predicate
blanchet@46300
  1072
$\const{g\_}\tau(t)$, and the binary function
blanchet@46300
  1073
$\const{t}(\tau, t)$ becomes a unary function
blanchet@46300
  1074
$\const{t\_}\tau(t)$.
blanchet@42589
  1075
blanchet@46435
  1076
\item[\labelitemi] \textbf{\textit{mono\_native} (sound):} Exploits native
blanchet@46643
  1077
first-order types if the prover supports the TFF0, TFF1, or THF0 syntax;
blanchet@46643
  1078
otherwise, falls back on \textit{mono\_guards}. The problem is monomorphized.
blanchet@43625
  1079
blanchet@46435
  1080
\item[\labelitemi] \textbf{\textit{mono\_native\_higher} (sound):} Exploits
blanchet@46435
  1081
native higher-order types if the prover supports the THF0 syntax; otherwise,
blanchet@46435
  1082
falls back on \textit{mono\_native} or \textit{mono\_guards}. The problem is
blanchet@46435
  1083
monomorphized.
blanchet@42681
  1084
blanchet@46643
  1085
\item[\labelitemi] \textbf{\textit{poly\_native} (sound):} Exploits native
blanchet@46643
  1086
polymorphic first-order types if the prover supports the TFF1 syntax; otherwise,
blanchet@46643
  1087
falls back on \textit{mono\_native}.
blanchet@46643
  1088
blanchet@45516
  1089
\item[\labelitemi]
blanchet@42681
  1090
\textbf{%
blanchet@44494
  1091
\textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\
blanchet@44494
  1092
\textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
blanchet@46435
  1093
\textit{mono\_native}? (sound*):} \\
blanchet@43990
  1094
The type encodings \textit{poly\_guards}, \textit{poly\_tags},
blanchet@44494
  1095
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
blanchet@47036
  1096
\textit{mono\_tags}, and \textit{mono\_native} are fully typed and sound. For
blanchet@47036
  1097
each of these, Sledgehammer also provides a lighter variant identified by a
blanchet@47036
  1098
question mark (`\hbox{?}')\ that detects and erases monotonic types, notably
blanchet@47036
  1099
infinite types. (For \textit{mono\_native}, the types are not actually erased
blanchet@47036
  1100
but rather replaced by a shared uniform type of individuals.) As argument to the
blanchet@47036
  1101
\textit{metis} proof method, the question mark is replaced by a
blanchet@47036
  1102
\hbox{``\textit{\_query\/}''} suffix.
blanchet@42582
  1103
blanchet@45516
  1104
\item[\labelitemi]
blanchet@42887
  1105
\textbf{%
blanchet@44769
  1106
\textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\
blanchet@44769
  1107
\textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\
blanchet@46300
  1108
(sound*):} \\
blanchet@44816
  1109
Even lighter versions of the `\hbox{?}' encodings. As argument to the
blanchet@44816
  1110
\textit{metis} proof method, the `\hbox{??}' suffix is replaced by
blanchet@46242
  1111
\hbox{``\textit{\_query\_query\/}''}.
blanchet@44816
  1112
blanchet@45516
  1113
\item[\labelitemi]
blanchet@44816
  1114
\textbf{%
blanchet@46300
  1115
\textit{poly\_guards}@?, \textit{raw\_mono\_guards}@? (sound*):} \\
blanchet@44816
  1116
Alternative versions of the `\hbox{??}' encodings. As argument to the
blanchet@44816
  1117
\textit{metis} proof method, the `\hbox{@?}' suffix is replaced by
blanchet@46242
  1118
\hbox{``\textit{\_at\_query\/}''}.
blanchet@44769
  1119
blanchet@45516
  1120
\item[\labelitemi]
blanchet@44769
  1121
\textbf{%
blanchet@44494
  1122
\textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\
blanchet@44743
  1123
\textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
blanchet@46435
  1124
\textit{mono\_native}!, \textit{mono\_native\_higher}! (mildly unsound):} \\
blanchet@43990
  1125
The type encodings \textit{poly\_guards}, \textit{poly\_tags},
blanchet@44494
  1126
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
blanchet@46435
  1127
\textit{mono\_tags}, \textit{mono\_native}, and \textit{mono\_native\_higher}
blanchet@44743
  1128
also admit a mildly unsound (but very efficient) variant identified by an
blanchet@44816
  1129
exclamation mark (`\hbox{!}') that detects and erases erases all types except
blanchet@46435
  1130
those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_native}
blanchet@46435
  1131
and \textit{mono\_native\_higher}, the types are not actually erased but rather
blanchet@44743
  1132
replaced by a shared uniform type of individuals.) As argument to the
blanchet@44743
  1133
\textit{metis} proof method, the exclamation mark is replaced by the suffix
blanchet@46242
  1134
\hbox{``\textit{\_bang\/}''}.
blanchet@42887
  1135
blanchet@45516
  1136
\item[\labelitemi]
blanchet@44769
  1137
\textbf{%
blanchet@44769
  1138
\textit{poly\_guards}!!, \textit{poly\_tags}!!, \textit{raw\_mono\_guards}!!, \\
blanchet@44769
  1139
\textit{raw\_mono\_tags}!!, \textit{mono\_guards}!!, \textit{mono\_tags}!! \\
blanchet@44769
  1140
(mildly unsound):} \\
blanchet@44816
  1141
Even lighter versions of the `\hbox{!}' encodings. As argument to the
blanchet@44816
  1142
\textit{metis} proof method, the `\hbox{!!}' suffix is replaced by
blanchet@46242
  1143
\hbox{``\textit{\_bang\_bang\/}''}.
blanchet@44816
  1144
blanchet@45516
  1145
\item[\labelitemi]
blanchet@44816
  1146
\textbf{%
blanchet@45950
  1147
\textit{poly\_guards}@!, \textit{raw\_mono\_guards}@! (mildly unsound):} \\
blanchet@44816
  1148
Alternative versions of the `\hbox{!!}' encodings. As argument to the
blanchet@44816
  1149
\textit{metis} proof method, the `\hbox{@!}' suffix is replaced by
blanchet@46242
  1150
\hbox{``\textit{\_at\_bang\/}''}.
blanchet@44769
  1151
blanchet@45516
  1152
\item[\labelitemi] \textbf{\textit{smart}:} The actual encoding used depends on
blanchet@47036
  1153
the ATP and should be the most efficient sound encoding for that ATP.
blanchet@42228
  1154
\end{enum}
blanchet@42228
  1155
blanchet@46435
  1156
For SMT solvers, the type encoding is always \textit{mono\_native}, irrespective
blanchet@44743
  1157
of the value of this option.
blanchet@42888
  1158
blanchet@42888
  1159
\nopagebreak
blanchet@42888
  1160
{\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
blanchet@42888
  1161
and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).}
blanchet@43574
  1162
blanchet@46302
  1163
\opfalse{strict}{non\_strict}
blanchet@46300
  1164
Specifies whether Sledgehammer should run in its strict mode. In that mode,
blanchet@46302
  1165
sound type encodings marked with an asterisk (*) above are made complete
blanchet@46300
  1166
for reconstruction with \textit{metis}, at the cost of some clutter in the
blanchet@46300
  1167
generated problems. This option has no effect if \textit{type\_enc} is
blanchet@46300
  1168
deliberately set to an unsound encoding.
blanchet@38591
  1169
\end{enum}
blanchet@36926
  1170
blanchet@38591
  1171
\subsection{Relevance Filter}
blanchet@38591
  1172
\label{relevance-filter}
blanchet@38591
  1173
blanchet@38591
  1174
\begin{enum}
blanchet@40343
  1175
\opdefault{relevance\_thresholds}{float\_pair}{\upshape 0.45~0.85}
blanchet@38746
  1176
Specifies the thresholds above which facts are considered relevant by the
blanchet@38746
  1177
relevance filter. The first threshold is used for the first iteration of the
blanchet@38746
  1178
relevance filter and the second threshold is used for the last iteration (if it
blanchet@38746
  1179
is reached). The effective threshold is quadratically interpolated for the other
blanchet@40343
  1180
iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems
blanchet@40343
  1181
are relevant and 1 only theorems that refer to previously seen constants.
blanchet@36926
  1182
blanchet@43065
  1183
\opdefault{max\_relevant}{smart\_int}{smart}
blanchet@38746
  1184
Specifies the maximum number of facts that may be returned by the relevance
blanchet@38746
  1185
filter. If the option is set to \textit{smart}, it is set to a value that was
blanchet@40059
  1186
empirically found to be appropriate for the prover. A typical value would be
blanchet@43065
  1187
250.
blanchet@42180
  1188
blanchet@43352
  1189
\opdefault{max\_new\_mono\_instances}{int}{\upshape 200}
blanchet@42884
  1190
Specifies the maximum number of monomorphic instances to generate beyond
blanchet@42884
  1191
\textit{max\_relevant}. The higher this limit is, the more monomorphic instances
blanchet@42884
  1192
are potentially generated. Whether monomorphization takes place depends on the
blanchet@43627
  1193
type encoding used.
blanchet@42884
  1194
blanchet@42884
  1195
\nopagebreak
blanchet@43627
  1196
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
blanchet@42884
  1197
blanchet@42884
  1198
\opdefault{max\_mono\_iters}{int}{\upshape 3}
blanchet@42884
  1199
Specifies the maximum number of iterations for the monomorphization fixpoint
blanchet@42884
  1200
construction. The higher this limit is, the more monomorphic instances are
blanchet@42884
  1201
potentially generated. Whether monomorphization takes place depends on the
blanchet@43627
  1202
type encoding used.
blanchet@42884
  1203
blanchet@42884
  1204
\nopagebreak
blanchet@43627
  1205
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
blanchet@36926
  1206
\end{enum}
blanchet@36926
  1207
blanchet@36926
  1208
\subsection{Output Format}
blanchet@36926
  1209
\label{output-format}
blanchet@36926
  1210
blanchet@36926
  1211
\begin{enum}
blanchet@36926
  1212
blanchet@36926
  1213
\opfalse{verbose}{quiet}
blanchet@36926
  1214
Specifies whether the \textbf{sledgehammer} command should explain what it does.
blanchet@41208
  1215
This option is implicitly disabled for automatic runs.
blanchet@36926
  1216
blanchet@36926
  1217
\opfalse{debug}{no\_debug}
blanchet@40203
  1218
Specifies whether Sledgehammer should display additional debugging information
blanchet@40203
  1219
beyond what \textit{verbose} already displays. Enabling \textit{debug} also
blanchet@41208
  1220
enables \textit{verbose} and \textit{blocking} (\S\ref{mode-of-operation})
blanchet@41208
  1221
behind the scenes. The \textit{debug} option is implicitly disabled for
blanchet@41208
  1222
automatic runs.
blanchet@36926
  1223
blanchet@36926
  1224
\nopagebreak
blanchet@36926
  1225
{\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
blanchet@36926
  1226
blanchet@36926
  1227
\opfalse{isar\_proof}{no\_isar\_proof}
blanchet@36926
  1228
Specifies whether Isar proofs should be output in addition to one-liner
blanchet@36926
  1229
\textit{metis} proofs. Isar proof construction is still experimental and often
blanchet@36926
  1230
fails; however, they are usually faster and sometimes more robust than
blanchet@36926
  1231
\textit{metis} proofs.
blanchet@36926
  1232
blanchet@40343
  1233
\opdefault{isar\_shrink\_factor}{int}{\upshape 1}
blanchet@36926
  1234
Specifies the granularity of the Isar proof. A value of $n$ indicates that each
blanchet@36926
  1235
Isar proof step should correspond to a group of up to $n$ consecutive proof
blanchet@36926
  1236
steps in the ATP proof.
blanchet@36926
  1237
\end{enum}
blanchet@36926
  1238
blanchet@38984
  1239
\subsection{Authentication}
blanchet@38984
  1240
\label{authentication}
blanchet@38984
  1241
blanchet@38984
  1242
\begin{enum}
blanchet@38984
  1243
\opnodefault{expect}{string}
blanchet@38984
  1244
Specifies the expected outcome, which must be one of the following:
blanchet@36926
  1245
blanchet@36926
  1246
\begin{enum}
blanchet@46300
  1247
\item[\labelitemi] \textbf{\textit{some}:} Sledgehammer found a proof.
blanchet@45516
  1248
\item[\labelitemi] \textbf{\textit{none}:} Sledgehammer found no proof.
blanchet@45516
  1249
\item[\labelitemi] \textbf{\textit{timeout}:} Sledgehammer timed out.
blanchet@45516
  1250
\item[\labelitemi] \textbf{\textit{unknown}:} Sledgehammer encountered some
blanchet@40203
  1251
problem.
blanchet@38984
  1252
\end{enum}
blanchet@38984
  1253
blanchet@38984
  1254
Sledgehammer emits an error (if \textit{blocking} is enabled) or a warning
blanchet@38984
  1255
(otherwise) if the actual outcome differs from the expected outcome. This option
blanchet@38984
  1256
is useful for regression testing.
blanchet@38984
  1257
blanchet@38984
  1258
\nopagebreak
blanchet@43038
  1259
{\small See also \textit{blocking} (\S\ref{mode-of-operation}) and
blanchet@43038
  1260
\textit{timeout} (\S\ref{timeouts}).}
blanchet@43038
  1261
\end{enum}
blanchet@43038
  1262
blanchet@43038
  1263
\subsection{Timeouts}
blanchet@43038
  1264
\label{timeouts}
blanchet@43038
  1265
blanchet@43038
  1266
\begin{enum}
blanchet@43038
  1267
\opdefault{timeout}{float\_or\_none}{\upshape 30}
blanchet@43038
  1268
Specifies the maximum number of seconds that the automatic provers should spend
blanchet@43038
  1269
searching for a proof. This excludes problem preparation and is a soft limit.
blanchet@43038
  1270
For historical reasons, the default value of this option can be overridden using
blanchet@44743
  1271
the option ``Sledgehammer: Time Limit'' in Proof General's ``Isabelle'' menu.
blanchet@43038
  1272
blanchet@46298
  1273
\opdefault{preplay\_timeout}{float\_or\_none}{\upshape 3}
blanchet@45380
  1274
Specifies the maximum number of seconds that \textit{metis} or \textit{smt}
blanchet@45380
  1275
should spend trying to ``preplay'' the found proof. If this option is set to 0,
blanchet@45380
  1276
no preplaying takes place, and no timing information is displayed next to the
blanchet@45380
  1277
suggested \textit{metis} calls.
blanchet@45708
  1278
blanchet@45708
  1279
\nopagebreak
blanchet@45708
  1280
{\small See also \textit{minimize} (\S\ref{mode-of-operation}).}
blanchet@47036
  1281
blanchet@47036
  1282
\optrueonly{dont\_preplay}
blanchet@47036
  1283
Alias for ``\textit{preplay\_timeout} = 0''.
blanchet@47036
  1284
blanchet@36926
  1285
\end{enum}
blanchet@36926
  1286
blanchet@36926
  1287
\let\em=\sl
blanchet@36926
  1288
\bibliography{../manual}{}
blanchet@36926
  1289
\bibliographystyle{abbrv}
blanchet@36926
  1290
blanchet@36926
  1291
\end{document}