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