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