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