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