author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 56380  9bb2856cc845 
child 56725  1ca7fd5f83bb 
permissions  rwrr 
36926  1 
\documentclass[a4paper,12pt]{article} 
2 
\usepackage[T1]{fontenc} 

3 
\usepackage{amsmath} 

4 
\usepackage{amssymb} 

53091  5 
\usepackage[english]{babel} 
36926  6 
\usepackage{color} 
7 
\usepackage{footmisc} 

8 
\usepackage{graphicx} 

9 
%\usepackage{mathpazo} 

10 
\usepackage{multicol} 

11 
\usepackage{stmaryrd} 

12 
%\usepackage[scaled=.85]{beramono} 

48962
a1acc1cb0271
more standard document preparation within session context;
wenzelm
parents:
48803
diff
changeset

13 
\usepackage{isabelle,iman,pdfsetup} 
36926  14 

50929  15 
\newcommand\download{\url{http://isabelle.in.tum.de/components/}} 
46242  16 

43216  17 
\def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}} 
18 
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$} 

19 

45516  20 
\newcommand\const[1]{\textsf{#1}} 
21 

36926  22 
%\oddsidemargin=4.6mm 
23 
%\evensidemargin=4.6mm 

24 
%\textwidth=150mm 

25 
%\topmargin=4.6mm 

26 
%\headheight=0mm 

27 
%\headsep=0mm 

28 
%\textheight=234mm 

29 

30 
\def\Colon{\mathord{:\mkern1.5mu:}} 

31 
%\def\lbrakk{\mathopen{\lbrack\mkern3.25mu\lbrack}} 

32 
%\def\rbrakk{\mathclose{\rbrack\mkern3.255mu\rbrack}} 

33 
\def\lparr{\mathopen{(\mkern4mu\mid}} 

34 
\def\rparr{\mathclose{\mid\mkern4mu)}} 

35 

36 
\def\unk{{?}} 

37 
\def\undef{(\lambda x.\; \unk)} 

38 
%\def\unr{\textit{others}} 

39 
\def\unr{\ldots} 

40 
\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}} 

41 
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}} 

42 

43 
\urlstyle{tt} 

44 

55290  45 
\renewcommand\_{\hbox{\textunderscore\kern.05ex}} 
46 

36926  47 
\begin{document} 
48 

45516  49 
%%% TYPESETTING 
50 
%\renewcommand\labelitemi{$\bullet$} 

51 
\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}} 

52 

36926  53 
\title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex] 
54 
Hammering Away \\[\smallskipamount] 

55 
\Large A User's Guide to Sledgehammer for Isabelle/HOL} 

56 
\author{\hbox{} \\ 

57 
Jasmin Christian Blanchette \\ 

43002
e88fde86e4c2
mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents:
42996
diff
changeset

58 
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\[4\smallskipamount] 
e88fde86e4c2
mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents:
42996
diff
changeset

59 
{\normalsize with contributions from} \\[4\smallskipamount] 
e88fde86e4c2
mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents:
42996
diff
changeset

60 
Lawrence C. Paulson \\ 
e88fde86e4c2
mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents:
42996
diff
changeset

61 
{\normalsize Computer Laboratory, University of Cambridge} \\ 
36926  62 
\hbox{}} 
63 

64 
\maketitle 

65 

66 
\tableofcontents 

67 

68 
\setlength{\parskip}{.7em plus .2em minus .1em} 

69 
\setlength{\parindent}{0pt} 

70 
\setlength{\abovedisplayskip}{\parskip} 

71 
\setlength{\abovedisplayshortskip}{.9\parskip} 

72 
\setlength{\belowdisplayskip}{\parskip} 

73 
\setlength{\belowdisplayshortskip}{.9\parskip} 

74 

52078  75 
% generalpurpose enum environment with correct spacing 
36926  76 
\newenvironment{enum}% 
77 
{\begin{list}{}{% 

78 
\setlength{\topsep}{.1\parskip}% 

79 
\setlength{\partopsep}{.1\parskip}% 

80 
\setlength{\itemsep}{\parskip}% 

81 
\advance\itemsep by\parsep}} 

82 
{\end{list}} 

83 

84 
\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin 

85 
\advance\rightskip by\leftmargin} 

86 
\def\post{\vskip0pt plus1ex\endgroup} 

87 

88 
\def\prew{\pre\advance\rightskip by\leftmargin} 

89 
\def\postw{\post} 

90 

91 
\section{Introduction} 

92 
\label{introduction} 

93 

42964
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

94 
Sledgehammer is a tool that applies automatic theorem provers (ATPs) 
47561
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

95 
and satisfiabilitymodulotheories (SMT) solvers on the current goal.% 
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

96 
\footnote{The distinction between ATPs and SMT solvers is convenient but mostly 
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

97 
historical. The two communities are converging, with more and more ATPs 
47672  98 
supporting typical SMT features such as arithmetic and sorts, and a few SMT 
47561
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

99 
solvers parsing ATP syntaxes. There is also a strong technological connection 
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

100 
between instantiationbased ATPs (such as iProver and iProverEq) and SMT 
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

101 
solvers.} 
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

102 
% 
55334
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset

103 
The supported ATPs are AgsyHOL \cite{agsyHOL}, AltErgo \cite{altergo}, E 
52078  104 
\cite{schulz2002}, ESInE \cite{sine}, EToFoF \cite{tofof}, iProver 
105 
\cite{korovin2009}, iProverEq \cite{korovinsticksel2010}, LEOII 

106 
\cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS 

107 
\cite{weidenbachetal2009}, Vampire \cite{riazanovvoronkov2002}, and 

108 
Waldmeister \cite{waldmeister}. The ATPs are run either locally or remotely via 

109 
the System\On\TPTP web service \cite{sutcliffe2000}. In addition to the ATPs, 

110 
a selection of the SMT solvers CVC3 \cite{cvc3}, Yices \cite{yices}, and Z3 

111 
\cite{z3} are run by default; these are run either locally or (for CVC3 and Z3) 

112 
on a server at the TU M\"unchen. 

36926  113 

40073  114 
The problem passed to the automatic provers consists of your current goal 
115 
together with a heuristic selection of hundreds of facts (theorems) from the 

52078  116 
current theory context, filtered by relevance. 
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset

117 

40073  118 
The result of a successful proof search is some source text that usually (but 
119 
not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed 

55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

120 
proof typically relies on the generalpurpose \textit{metis} proof method, which 
45380  121 
integrates the Metis ATP in Isabelle/HOL with explicit inferences going through 
122 
the kernel. Thus its results are correct by construction. 

36926  123 

53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

124 
For Isabelle/jEdit users, Sledgehammer provides an automatic mode that can be 
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

125 
enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options > 
54114  126 
Isabelle > General.'' In this mode, a reduced version of Sledgehammer is run on 
127 
every newly entered theorem for a few seconds. 

39320  128 

36926  129 
\newbox\boxA 
46298  130 
\setbox\boxA=\hbox{\texttt{NOSPAM}} 
36926  131 

46298  132 
\newcommand\authoremail{\texttt{blan{\color{white}NOSPAM}\kern\wd\boxA{}chette@\allowbreak 
42763  133 
in.\allowbreak tum.\allowbreak de}} 
134 

40689  135 
To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is 
136 
importedthis is rarely a problem in practice since it is part of 

137 
\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's 

36926  138 
\texttt{src/HOL/Metis\_Examples} directory. 
139 
Comments and bug reports concerning Sledgehammer or this manual should be 

42883  140 
directed to the author at \authoremail. 
36926  141 

53759
a198ce71de11
took out Waldmeister from list of default provers  it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents:
53757
diff
changeset

142 
%\vskip2.5\smallskipamount 
a198ce71de11
took out Waldmeister from list of default provers  it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents:
53757
diff
changeset

143 
% 
36926  144 
%\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for 
145 
%suggesting several textual improvements. 

146 

147 
\section{Installation} 

148 
\label{installation} 

149 

48387  150 
Sledgehammer is part of Isabelle, so you do not need to install it. However, it 
46242  151 
relies on thirdparty automatic provers (ATPs and SMT solvers). 
42763  152 

55334
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset

153 
Among the ATPs, AgsyHOL, AltErgo, E, LEOII, Satallax, SPASS, and Vampire can 
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset

154 
be run locally; in addition, AgsyHOL, E, ESInE, EToFoF, iProver, iProverEq, 
52078  155 
LEOII, Satallax, SNARK, Vampire, and Waldmeister are available remotely via 
156 
System\On\TPTP \cite{sutcliffe2000}. If you want better performance, you 

56119
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

157 
should at least install E and SPASS locally. The SMT solvers CVC3, Yices, and Z3 
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

158 
can be run locally. 
36926  159 

46242  160 
There are three main ways to install automatic provers on your machine: 
36926  161 

46242  162 
\begin{sloppy} 
163 
\begin{enum} 

164 
\item[\labelitemi] If you installed an official Isabelle package, it should 

165 
already include properly setup executables for CVC3, E, SPASS, and Z3, ready to use.% 

166 
\footnote{Vampire's and Yices's licenses prevent us from doing the same for 

167 
these otherwise remarkable tools.} 

168 
For Z3, you must additionally set the variable 

169 
\texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a 

56119
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

170 
noncommercial usereither in the environment in which Isabelle is 
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

171 
launched, in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or 
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

172 
via the ``z3\_non\_commercial'' option under ``Plugins > Plugin Options 
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

173 
> Isabelle > General'' in Isabelle/jEdit. 
46242  174 

175 
\item[\labelitemi] Alternatively, you can download the Isabelleaware CVC3, E, 

176 
SPASS, and Z3 binary packages from \download. Extract the archives, then add a 

177 
line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}% 

41747
f58d4d202924
fix path to etc/settings and etc/components in doc
blanchet
parents:
41740
diff
changeset

178 
\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at 
46242  179 
startup. Its value can be retrieved by executing \texttt{isabelle} 
41747
f58d4d202924
fix path to etc/settings and etc/components in doc
blanchet
parents:
41740
diff
changeset

180 
\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.} 
46242  181 
file with the absolute path to CVC3, E, SPASS, or Z3. For example, if the 
182 
\texttt{components} file does not exist yet and you extracted SPASS to 

47577  183 
\texttt{/usr/local/spass3.8ds}, create it with the single line 
36926  184 

185 
\prew 

47577  186 
\texttt{/usr/local/spass3.8ds} 
36926  187 
\postw 
188 

47561
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

189 
in it. 
38043  190 

55334
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset

191 
\item[\labelitemi] If you prefer to build AgsyHOL, AltErgo, E, LEOII, 
52078  192 
Satallax, or SPASS manually, or found a Vampire executable somewhere (e.g., 
193 
\url{http://www.vprover.org/}), set the environment variable 

194 
\texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME}, 

195 
\texttt{SATALLAX\_HOME}, \texttt{SPASS\_HOME}, or 

52757  196 
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{agsyHOL}, 
197 
\texttt{eprover} (and/or \texttt{eproof} or \texttt{eproof\_ram}), 

52078  198 
\texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable; 
199 
for AltErgo, set the 

200 
environment variable \texttt{WHY3\_HOME} to the directory that contains the 

201 
\texttt{why3} executable. 

56379
d8ecce5d51cd
use AltErgo 0.95.2, the latest and greatest version
blanchet
parents:
56378
diff
changeset

202 
Sledgehammer has been tested with AgsyHOL 1.0, AltErgo 0.95.2, E 1.0 to 1.8, 
52996  203 
LEOII 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 3.0.% 
38063  204 
\footnote{Following the rewrite of Vampire, the counter for version numbers was 
52996  205 
reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more 
48652  206 
recent than 9.0 or 11.5.}% 
48006  207 
Since the ATPs' output formats are neither documented nor stable, other 
47577  208 
versions might not work well with Sledgehammer. Ideally, 
209 
you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION}, 

46242  210 
\texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or 
56380
9bb2856cc845
don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
blanchet
parents:
56379
diff
changeset

211 
\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``3.0''). 
36926  212 

52078  213 
Similarly, if you want to build CVC3, or found a 
46242  214 
Yices or Z3 executable somewhere (e.g., 
215 
\url{http://yices.csl.sri.com/download.shtml} or 

216 
\url{http://research.microsoft.com/enus/um/redmond/projects/z3/download.html}), 

217 
set the environment variable \texttt{CVC3\_\allowbreak SOLVER}, 

218 
\texttt{YICES\_SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of 

52078  219 
the executable, \emph{including the file name}. 
220 
Sledgehammer has been tested with CVC3 2.2 and 2.4.1, 

48405
7682bc885e8a
use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents:
48393
diff
changeset

221 
Yices 1.0.28 and 1.0.33, and Z3 3.0 to 4.0. Since the SMT solvers' output 
7682bc885e8a
use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents:
48393
diff
changeset

222 
formats are somewhat unstable, other versions of the solvers might not work well 
7682bc885e8a
use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents:
48393
diff
changeset

223 
with Sledgehammer. Ideally, also set \texttt{CVC3\_VERSION}, 
7682bc885e8a
use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents:
48393
diff
changeset

224 
\texttt{YICES\_VERSION}, or \texttt{Z3\_VERSION} to the solver's version number 
7682bc885e8a
use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents:
48393
diff
changeset

225 
(e.g., ``4.0''). 
46242  226 
\end{enum} 
227 
\end{sloppy} 

36926  228 

46242  229 
To check whether E, SPASS, Vampire, and/or Z3 are successfully installed, try 
230 
out the example in \S\ref{firststeps}. If the remote versions of any of these 

56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

231 
provers is used (identified by the prefix ``\textit{remote\_\/}''), or if the 
46242  232 
local versions fail to solve the easy goal presented there, something must be 
233 
wrong with the installation. 

234 

235 
Remote prover invocation requires Perl with the World Wide Web Library 

236 
(\texttt{libwwwperl}) installed. If you must use a proxy server to access the 

237 
Internet, set the \texttt{http\_proxy} environment variable to the proxy, either 

238 
in the environment in which Isabelle is launched or in your 

47561
92d88c89efff
update documentation (mostly based on feedback by Makarius)
blanchet
parents:
47530
diff
changeset

239 
\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few 
46242  240 
examples: 
39152
f09b378cb252
make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents:
38997
diff
changeset

241 

f09b378cb252
make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents:
38997
diff
changeset

242 
\prew 
39153  243 
\texttt{http\_proxy=http://proxy.example.org} \\ 
244 
\texttt{http\_proxy=http://proxy.example.org:8080} \\ 

245 
\texttt{http\_proxy=http://joeblow:pAsSwRd@proxy.example.org} 

39152
f09b378cb252
make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents:
38997
diff
changeset

246 
\postw 
37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset

247 

36926  248 
\section{First Steps} 
249 
\label{firststeps} 

250 

251 
To illustrate Sledgehammer in context, let us start a theory file and 

252 
attempt to prove a simple lemma: 

253 

254 
\prew 

255 
\textbf{theory}~\textit{Scratch} \\ 

256 
\textbf{imports}~\textit{Main} \\ 

257 
\textbf{begin} \\[2\smallskipamount] 

258 
% 

42945  259 
\textbf{lemma} ``$[a] = [b] \,\Longrightarrow\, a = b$'' \\ 
36926  260 
\textbf{sledgehammer} 
261 
\postw 

262 

53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

263 
Instead of issuing the \textbf{sledgehammer} command, you can also use the 
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

264 
Sledgehammer panel in Isabelle/jEdit. Sledgehammer produces the following output 
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

265 
after a few seconds: 
36926  266 

267 
\prew 

268 
\slshape 

46242  269 
Sledgehammer: ``\textit{e\/}'' on goal \\ 
42945  270 
$[a] = [b] \,\Longrightarrow\, a = b$ \\ 
43054  271 
Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount] 
42945  272 
% 
46242  273 
Sledgehammer: ``\textit{z3\/}'' on goal \\ 
274 
$[a] = [b] \,\Longrightarrow\, a = b$ \\ 

275 
Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount] 

276 
% 

277 
Sledgehammer: ``\textit{vampire\/}'' on goal \\ 

42945  278 
$[a] = [b] \,\Longrightarrow\, a = b$ \\ 
43054  279 
Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount] 
36926  280 
% 
46242  281 
Sledgehammer: ``\textit{spass\/}'' on goal \\ 
42945  282 
$[a] = [b] \,\Longrightarrow\, a = b$ \\ 
43054  283 
Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount] 
36926  284 
% 
47642
9a9218111085
swap out Satallax, pull in ESInE again  it's not clear yet how useful Satallax is after proof reconstruction, whereas ESInE performed surprisingly well on latest evaluations
blanchet
parents:
47577
diff
changeset

285 
Sledgehammer: ``\textit{remote\_e\_sine\/}'' on goal \\ 
45063
b3b50d8b535a
reintroduced ESInE now that it's unexpectedly working again (thanks to Geoff)
blanchet
parents:
45048
diff
changeset

286 
$[a] = [b] \,\Longrightarrow\, a = b$ \\ 
46242  287 
Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). 
36926  288 
\postw 
289 

53759
a198ce71de11
took out Waldmeister from list of default provers  it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents:
53757
diff
changeset

290 
Sledgehammer ran E, ESInE, SPASS, Vampire, and Z3 in parallel. Depending on 
a198ce71de11
took out Waldmeister from list of default provers  it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents:
53757
diff
changeset

291 
which provers are installed and how many processor cores are available, some of 
a198ce71de11
took out Waldmeister from list of default provers  it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents:
53757
diff
changeset

292 
the provers might be missing or present with a \textit{remote\_} prefix. 
a198ce71de11
took out Waldmeister from list of default provers  it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents:
53757
diff
changeset

293 
Waldmeister is run only for unit equational problems, where the goal's 
a198ce71de11
took out Waldmeister from list of default provers  it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents:
53757
diff
changeset

294 
conclusion is a (universally quantified) equation. 
36926  295 

55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

296 
For each successful prover, Sledgehammer gives a oneline \textit{metis} or 
56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

297 
\textit{smt2} method call. Rough timings are shown in parentheses, indicating how 
48387  298 
fast the call is. You can click the proof to insert it into the theory text. 
36926  299 

51190
2654b3965c8d
made "isar_proofs" a 3way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51189
diff
changeset

300 
In addition, you can ask Sledgehammer for an Isar text proof by enabling the 
49919  301 
\textit{isar\_proofs} option (\S\ref{outputformat}): 
36926  302 

303 
\prew 

49919  304 
\textbf{sledgehammer} [\textit{isar\_proofs}] 
36926  305 
\postw 
306 

307 
When Isar proof construction is successful, it can yield proofs that are more 

56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

308 
readable and also faster than the \textit{metis} or \textit{smt2} oneline 
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

309 
proofs. This feature is experimental and is only available for ATPs. 
36926  310 

37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset

311 
\section{Hints} 
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset

312 
\label{hints} 
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset

313 

42884  314 
This section presents a few hints that should help you get the most out of 
46643
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset

315 
Sledgehammer. Frequently asked questions are answered in 
45380  316 
\S\ref{frequentlyaskedquestions}. 
42884  317 

46242  318 
%\newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak} 
319 
\newcommand\point[1]{\subsection{\emph{#1}}} 

42763  320 

321 
\point{Presimplify the goal} 

322 

37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset

323 
For best results, first simplify your problem by calling \textit{auto} or at 
42945  324 
least \textit{safe} followed by \textit{simp\_all}. The SMT solvers provide 
325 
arithmetic decision procedures, but the ATPs typically do not (or if they do, 

326 
Sledgehammer does not use it yet). Apart from Waldmeister, they are not 

53759
a198ce71de11
took out Waldmeister from list of default provers  it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents:
53757
diff
changeset

327 
particularly good at heavy rewriting, but because they regard equations as 
42945  328 
undirected, they often prove theorems that require the reverse orientation of a 
329 
\textit{simp} rule. Higherorder problems can be tackled, but the success rate 

330 
is better for firstorder problems. Hence, you may get better results if you 

331 
first simplify the problem to remove higherorder features. 

37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset

332 

46242  333 
\point{Make sure E, SPASS, Vampire, and Z3 are locally installed} 
42763  334 

335 
Locally installed provers are faster and more reliable than those running on 

336 
servers. See \S\ref{installation} for details on how to install them. 

337 

53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

338 
\point{Familiarize yourself with the main options} 
42763  339 

340 
Sledgehammer's options are fully documented in \S\ref{commandsyntax}. Many of 

341 
the options are very specialized, but serious users of the tool should at least 

342 
familiarize themselves with the following options: 

343 

344 
\begin{enum} 

45516  345 
\item[\labelitemi] \textbf{\textit{provers}} (\S\ref{modeofoperation}) specifies 
42884  346 
the automatic provers (ATPs and SMT solvers) that should be run whenever 
347 
Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{e spass 

46242  348 
remote\_vampire\/}''). For convenience, you can omit ``\textit{provers}~='' 
43014  349 
and simply write the prover names as a spaceseparated list (e.g., ``\textit{e 
46242  350 
spass remote\_vampire\/}''). 
42763  351 

48294  352 
\item[\labelitemi] \textbf{\textit{max\_facts}} (\S\ref{relevancefilter}) 
42884  353 
specifies the maximum number of facts that should be passed to the provers. By 
48294  354 
default, the value is proverdependent but varies between about 50 and 1000. If 
355 
the provers time out, you can try lowering this value to, say, 25 or 50 and see 

42884  356 
if that helps. 
42763  357 

49919  358 
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{outputformat}) specifies 
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

359 
that Isar proofs should be generated, in addition to oneline \textit{metis} or 
56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

360 
\textit{smt2} proofs. The length of the Isar proofs can be controlled by setting 
55183
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55051
diff
changeset

361 
\textit{compress\_isar} (\S\ref{outputformat}). 
43038  362 

45516  363 
\item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the 
43038  364 
provers' time limit. It is set to 30 seconds, but since Sledgehammer runs 
365 
asynchronously you should not hesitate to raise this limit to 60 or 120 seconds 

366 
if you are the kind of user who can think clearly while ATPs are active. 

42763  367 
\end{enum} 
368 

42884  369 
Options can be set globally using \textbf{sledgehammer\_params} 
43010
a14cf580a5a5
readded Waldmeister as default to the documentation and other minor changes
blanchet
parents:
43008
diff
changeset

370 
(\S\ref{commandsyntax}). The command also prints the list of all available 
a14cf580a5a5
readded Waldmeister as default to the documentation and other minor changes
blanchet
parents:
43008
diff
changeset

371 
options with their current value. Fact selection can be influenced by specifying 
a14cf580a5a5
readded Waldmeister as default to the documentation and other minor changes
blanchet
parents:
43008
diff
changeset

372 
``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer} call 
a14cf580a5a5
readded Waldmeister as default to the documentation and other minor changes
blanchet
parents:
43008
diff
changeset

373 
to ensure that certain facts are included, or simply ``$(\textit{my\_facts})$'' 
a14cf580a5a5
readded Waldmeister as default to the documentation and other minor changes
blanchet
parents:
43008
diff
changeset

374 
to force Sledgehammer to run only with $\textit{my\_facts}$. 
42763  375 

376 
\section{Frequently Asked Questions} 

377 
\label{frequentlyaskedquestions} 

378 

42945  379 
This sections answers frequently (and infrequently) asked questions about 
48387  380 
Sledgehammer. It is a good idea to skim over it now even if you do not have any 
42945  381 
questions at this stage. And if you have any further questions not listed here, 
382 
send them to the author at \authoremail. 

383 

43008
bb212c2ad238
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents:
43007
diff
changeset

384 
\point{Which facts are passed to the automatic provers?} 
42883  385 

48387  386 
Sledgehammer heuristically selects a few hundred relevant lemmas from the 
387 
currently loaded libraries. The component that performs this selection is 

388 
called \emph{relevance filter}. 

389 

390 
\begin{enum} 

391 
\item[\labelitemi] 

48388  392 
The traditional relevance filter, called \emph{MePo} 
393 
(\underline{Me}ng\underline{Pau}lson), assigns a score to every available fact 

394 
(lemma, theorem, definition, or axiom) based upon how many constants that fact 

395 
shares with the conjecture. This process iterates to include facts relevant to 

396 
those just accepted. The constants are weighted to give unusual ones greater 

397 
significance. MePo copes best when the conjecture contains some unusual 

398 
constants; if all the constants are common, it is unable to discriminate among 

399 
the hundreds of facts that are picked up. The filter is also memoryless: It has 

400 
no information about how many times a particular fact has been used in a proof, 

401 
and it cannot learn. 

48387  402 

403 
\item[\labelitemi] 

53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

404 
An experimental alternative to MePo is \emph{MaSh} 
48387  405 
(\underline{Ma}chine Learner for \underline{S}ledge\underline{h}ammer). It 
50221  406 
relies on an external Python tool that applies machine learning to 
48387  407 
the problem of finding relevant facts. 
408 

50459  409 
\item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh. 
48387  410 
\end{enum} 
411 

50459  412 
The default is either MePo or MeSh, depending on whether the environment 
50221  413 
variable \texttt{MASH} is set and what class of provers the target prover 
414 
belongs to (\S\ref{relevancefilter}). 

42763  415 

42883  416 
The number of facts included in a problem varies from prover to prover, since 
43008
bb212c2ad238
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents:
43007
diff
changeset

417 
some provers get overwhelmed more easily than others. You can show the number of 
42883  418 
facts given using the \textit{verbose} option (\S\ref{outputformat}) and the 
419 
actual facts using \textit{debug} (\S\ref{outputformat}). 

420 

421 
Sledgehammer is good at finding short proofs combining a handful of existing 

422 
lemmas. If you are looking for longer proofs, you must typically restrict the 

48294  423 
number of facts, by setting the \textit{max\_facts} option 
43574  424 
(\S\ref{relevancefilter}) to, say, 25 or 50. 
42883  425 

42996  426 
You can also influence which facts are actually selected in a number of ways. If 
427 
you simply want to ensure that a fact is included, you can specify it using the 

428 
``$(\textit{add}{:}~\textit{my\_facts})$'' syntax. For example: 

429 
% 

430 
\prew 

431 
\textbf{sledgehammer} (\textit{add}: \textit{hd.simps} \textit{tl.simps}) 

432 
\postw 

433 
% 

434 
The specified facts then replace the least relevant facts that would otherwise be 

435 
included; the other selected facts remain the same. 

436 
If you want to direct the selection in a particular direction, you can specify 

437 
the facts via \textbf{using}: 

438 
% 

439 
\prew 

440 
\textbf{using} \textit{hd.simps} \textit{tl.simps} \\ 

441 
\textbf{sledgehammer} 

442 
\postw 

443 
% 

444 
The facts are then more likely to be selected than otherwise, and if they are 

445 
selected at iteration $j$ they also influence which facts are selected at 

446 
iterations $j + 1$, $j + 2$, etc. To give them even more weight, try 

447 
% 

448 
\prew 

449 
\textbf{using} \textit{hd.simps} \textit{tl.simps} \\ 

450 
\textbf{apply}~\textbf{} \\ 

451 
\textbf{sledgehammer} 

452 
\postw 

453 

46300  454 
\point{Why does Metis fail to reconstruct the proof?} 
455 

456 
There are many reasons. If Metis runs seemingly forever, that is a sign that the 

457 
proof is too difficult for it. Metis's search is complete, so it should 

458 
eventually find it, but that's little consolation. There are several possible 

459 
solutions: 

460 

461 
\begin{enum} 

49919  462 
\item[\labelitemi] Try the \textit{isar\_proofs} option (\S\ref{outputformat}) to 
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

463 
obtain a stepbystep Isar proof. Since the steps are fairly small, \textit{metis} 
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

464 
and the other Isabelle proof methods are more likely to be able to replay them. 
46300  465 

56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

466 
\item[\labelitemi] Try the \textit{smt2} proof method instead of \textit{metis}. 
48405
7682bc885e8a
use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents:
48393
diff
changeset

467 
It is usually stronger, but you need to either have Z3 available to replay the 
46300  468 
proofs, trust the SMT solver, or use certificates. See the documentation in the 
56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

469 
\textit{SMT2} theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT2.thy}) for details. 
46300  470 

471 
\item[\labelitemi] Try the \textit{blast} or \textit{auto} proof methods, passing 

472 
the necessary facts via \textbf{unfolding}, \textbf{using}, \textit{intro}{:}, 

473 
\textit{elim}{:}, \textit{dest}{:}, or \textit{simp}{:}, as appropriate. 

474 
\end{enum} 

475 

476 
In some rare cases, \textit{metis} fails fairly quickly, and you get the error 

477 
message 

478 

479 
\prew 

480 
\slshape 

481 
Oneline proof reconstruction failed. 

482 
\postw 

483 

484 
This message indicates that Sledgehammer determined that the goal is provable, 

485 
but the proof is, for technical reasons, beyond \textit{metis}'s power. You can 

486 
then try again with the \textit{strict} option (\S\ref{problemencoding}). 

487 

46640  488 
If the goal is actually unprovable and you did not specify an unsound encoding 
46300  489 
using \textit{type\_enc} (\S\ref{problemencoding}), this is a bug, and you are 
490 
strongly encouraged to report this to the author at \authoremail. 

491 

492 
\point{How can I tell whether a suggested proof is sound?} 

493 

494 
Earlier versions of Sledgehammer often suggested unsound proofseither proofs 

495 
of nontheorems or simply proofs that rely on typeunsound inferences. This 

46640  496 
is a thing of the past, unless you explicitly specify an unsound encoding 
46300  497 
using \textit{type\_enc} (\S\ref{problemencoding}). 
498 
% 

499 
Officially, the only form of ``unsoundness'' that lurks in the sound 

500 
encodings is related to missing characteristic theorems of datatypes. For 

501 
example, 

502 

503 
\prew 

504 
\textbf{lemma}~``$\exists \mathit{xs}.\; \mathit{xs} \neq []$'' \\ 

505 
\textbf{sledgehammer} () 

506 
\postw 

507 

508 
suggests an argumentless \textit{metis} call that fails. However, the conjecture 

509 
does actually hold, and the \textit{metis} call can be repaired by adding 

510 
\textit{list.distinct}. 

511 
% 

512 
We hope to address this problem in a future version of Isabelle. In the 

513 
meantime, you can avoid it by passing the \textit{strict} option 

514 
(\S\ref{problemencoding}). 

515 

46298  516 
\point{What are the \textit{full\_types}, \textit{no\_types}, and 
517 
\textit{mono\_tags} arguments to Metis?} 

42883  518 

46298  519 
The \textit{metis}~(\textit{full\_types}) proof method 
520 
and its cousin \textit{metis}~(\textit{mono\_tags}) are fullytyped 

53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

521 
versions of Metis. It is somewhat slower than \textit{metis}, but the proof 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43217
diff
changeset

522 
search is fully typed, and it also includes more powerful rules such as the 
45516  523 
axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in 
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

524 
higherorder places (e.g., in set comprehensions). The method is automatically 
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

525 
tried as a fallback when \textit{metis} fails, and it is sometimes 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43217
diff
changeset

526 
generated by Sledgehammer instead of \textit{metis} if the proof obviously 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43217
diff
changeset

527 
requires type information or if \textit{metis} failed when Sledgehammer 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43217
diff
changeset

528 
preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with 
55277
93c7fcfbe6f5
reduced preplaying timeout, since (1) Isar proofs are getting better and better as alternatives; (2) the same timeout is used for each step in an Isar proof, where a lower timeout makes more sense
blanchet
parents:
55183
diff
changeset

529 
various sets of option for up to 2~seconds each time to ensure that the generated 
46298  530 
oneline proofs actually work and to display timing information. This can be 
47036  531 
configured using the \textit{preplay\_timeout} and \textit{dont\_preplay} 
532 
options (\S\ref{timeouts}).) 

46298  533 
% 
43229  534 
At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types}) 
535 
uses no type information at all during the proof search, which is more efficient 

536 
but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally 

537 
generated by Sledgehammer. 

46298  538 
% 
539 
See the \textit{type\_enc} option (\S\ref{problemencoding}) for details. 

43229  540 

46298  541 
Incidentally, if you ever see warnings such as 
42883  542 

543 
\prew 

43007  544 
\slshape 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43217
diff
changeset

545 
Metis: Falling back on ``\textit{metis} (\textit{full\_types})''. 
42883  546 
\postw 
547 

45380  548 
for a successful \textit{metis} proof, you can advantageously pass the 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43217
diff
changeset

549 
\textit{full\_types} option to \textit{metis} directly. 
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43217
diff
changeset

550 

46366  551 
\point{And what are the \textit{lifting} and \textit{hide\_lams} arguments 
46298  552 
to Metis?} 
553 

554 
Orthogonally to the encoding of types, it is important to choose an appropriate 

555 
translation of $\lambda$abstractions. Metis supports three translation schemes, 

556 
in decreasing order of power: Curry combinators (the default), 

557 
$\lambda$lifting, and a ``hiding'' scheme that disables all reasoning under 

558 
$\lambda$abstractions. The more powerful schemes also give the automatic 

559 
provers more rope to hang themselves. See the \textit{lam\_trans} option (\S\ref{problemencoding}) for details. 

560 

43054  561 
\point{Are generated proofs minimal?} 
43036  562 

43054  563 
Automatic provers frequently use many more facts than are necessary. 
564 
Sledgehammer inclues a minimization tool that takes a set of facts returned by a 

45380  565 
given prover and repeatedly calls the same prover, \textit{metis}, or 
56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

566 
\textit{smt2} with subsets of those axioms in order to find a minimal set. 
45380  567 
Reducing the number of axioms typically improves Metis's speed and success rate, 
568 
while also removing superfluous clutter from the proof scripts. 

43036  569 

43229  570 
In earlier versions of Sledgehammer, generated proofs were systematically 
571 
accompanied by a suggestion to invoke the minimization tool. This step is now 

572 
performed implicitly if it can be done in a reasonable amount of time (something 

573 
that can be guessed from the number of facts in the original proof and the time 

45708
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

574 
it took to find or preplay it). 
43036  575 

45163  576 
In addition, some provers (e.g., Yices) do not provide proofs or sometimes 
577 
produce incomplete proofs. The minimizer is then invoked to find out which facts 

46640  578 
are actually needed from the (large) set of facts that was initially given to 
45163  579 
the prover. Finally, if a prover returns a proof with lots of facts, the 
580 
minimizer is invoked automatically since Metis would be unlikely to refind the 

581 
proof. 

45708
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

582 
% 
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

583 
Automatic minimization can be forced or disabled using the \textit{minimize} 
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

584 
option (\S\ref{modeofoperation}). 
43036  585 

43008
bb212c2ad238
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents:
43007
diff
changeset

586 
\point{A strange error occurredwhat should I do?} 
42763  587 

588 
Sledgehammer tries to give informative error messages. Please report any strange 

53224  589 
error to the author at \authoremail. This applies doubly if you get the message 
42763  590 

42883  591 
\prew 
42763  592 
\slshape 
53224  593 
The prover derived ``\textit{False}'' using ``\textit{foo\/}'', 
594 
``\textit{bar\/}'', and ``\textit{baz\/}''. 

595 
This could be due to inconsistent axioms (including ``\textbf{sorry}''s) or to 

596 
a bug in Sledgehammer. If the problem persists, please contact the 

597 
Isabelle developers. 

42883  598 
\postw 
42763  599 

600 
\point{Auto can solve itwhy not Sledgehammer?} 

601 

602 
Problems can be easy for \textit{auto} and difficult for automatic provers, but 

48387  603 
the reverse is also true, so do not be discouraged if your first attempts fail. 
39320  604 
Because the system refers to all theorems known to Isabelle, it is particularly 
48387  605 
suitable when your goal has a short proof from lemmas that you do not know 
606 
about. 

37517
19ba7ec5f1e3
steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
blanchet
parents:
37498
diff
changeset

607 

42883  608 
\point{Why are there so many options?} 
609 

610 
Sledgehammer's philosophy should work out of the box, without user guidance. 

611 
Many of the options are meant to be used mostly by the Sledgehammer developers 

53102  612 
for experiments. Of course, feel free to try them out if you are so inclined. 
42883  613 

36926  614 
\section{Command Syntax} 
615 
\label{commandsyntax} 

616 

46242  617 
\subsection{Sledgehammer} 
618 

36926  619 
Sledgehammer can be invoked at any point when there is an open goal by entering 
620 
the \textbf{sledgehammer} command in the theory file. Its general syntax is as 

621 
follows: 

622 

623 
\prew 

43216  624 
\textbf{sledgehammer} \qty{subcommand}$^?$ \qty{options}$^?$ \qty{facts\_override}$^?$ \qty{num}$^?$ 
36926  625 
\postw 
626 

43216  627 
In the general syntax, the \qty{subcommand} may be any of the following: 
36926  628 

629 
\begin{enum} 

45516  630 
\item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on 
43216  631 
subgoal number \qty{num} (1 by default), with the given options and facts. 
36926  632 

45516  633 
\item[\labelitemi] \textbf{\textit{min}:} Attempts to minimize the facts 
43216  634 
specified in the \qty{facts\_override} argument to obtain a simpler proof 
36926  635 
involving fewer facts. The options and goal number are as for \textit{run}. 
636 

45516  637 
\item[\labelitemi] \textbf{\textit{messages}:} Redisplays recent messages issued 
40203  638 
by Sledgehammer. This allows you to examine results that might have been lost 
43216  639 
due to Sledgehammer's asynchronous nature. The \qty{num} argument specifies a 
47530  640 
limit on the number of messages to display (10 by default). 
36926  641 

45516  642 
\item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of 
41724  643 
automatic provers supported by Sledgehammer. See \S\ref{installation} and 
644 
\S\ref{modeofoperation} for more information on how to install automatic 

645 
provers. 

36926  646 

45516  647 
\item[\labelitemi] \textbf{\textit{running\_provers}:} Prints information about 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

648 
currently running automatic provers, including elapsed runtime and remaining 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

649 
time until timeout. 
36926  650 

50720  651 
\item[\labelitemi] \textbf{\textit{kill\_all}:} Terminates all running 
49365  652 
threads (automatic provers and machine learners). 
36926  653 

48393  654 
\item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote 
655 
ATPs available at System\On\TPTP \cite{sutcliffe2000}. 

656 
\end{enum} 

657 

49365  658 
In addition, the following subcommands provide finer control over machine 
48393  659 
learning with MaSh: 
660 

661 
\begin{enum} 

662 
\item[\labelitemi] \textbf{\textit{unlearn}:} Resets MaSh, erasing any 

663 
persistent state. 

48387  664 

48393  665 
\item[\labelitemi] \textbf{\textit{learn\_isar}:} Invokes MaSh on the current 
666 
theory to process all the available facts, learning from their Isabelle/Isar 

667 
proofs. This happens automatically at Sledgehammer invocations if the 

668 
\textit{learn} option (\S\ref{relevancefilter}) is enabled. 

48387  669 

50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50459
diff
changeset

670 
\item[\labelitemi] \textbf{\textit{learn\_prover}:} Invokes MaSh on the current 
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50459
diff
changeset

671 
theory to process all the available facts, learning from proofs generated by 
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50459
diff
changeset

672 
automatic provers. The prover to use and its timeout can be set using the 
48393  673 
\textit{prover} (\S\ref{modeofoperation}) and \textit{timeout} 
674 
(\S\ref{timeouts}) options. It is recommended to perform learning using an 

675 
efficient firstorder ATP (such as E, SPASS, and Vampire) as opposed to a 

676 
higherorder ATP or an SMT solver. 

677 

678 
\item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn} 

679 
followed by \textit{learn\_isar}. 

680 

50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50459
diff
changeset

681 
\item[\labelitemi] \textbf{\textit{relearn\_prover}:} Same as \textit{unlearn} 
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50459
diff
changeset

682 
followed by \textit{learn\_prover}. 
48387  683 

684 
\item[\labelitemi] \textbf{\textit{running\_learners}:} Prints information about 

685 
currently running machine learners, including elapsed runtime and remaining 

686 
time until timeout. 

36926  687 
\end{enum} 
688 

43216  689 
Sledgehammer's behavior can be influenced by various \qty{options}, which can be 
690 
specified in brackets after the \textbf{sledgehammer} command. The 

691 
\qty{options} are a list of keyvalue pairs of the form ``[$k_1 = v_1, 

50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50459
diff
changeset

692 
\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. 
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50459
diff
changeset

693 
For example: 
36926  694 

695 
\prew 

49919  696 
\textbf{sledgehammer} [\textit{isar\_proofs}, \,\textit{timeout} = 120] 
36926  697 
\postw 
698 

699 
Default values can be set using \textbf{sledgehammer\_\allowbreak params}: 

700 

701 
\prew 

43216  702 
\textbf{sledgehammer\_params} \qty{options} 
36926  703 
\postw 
704 

705 
The supported options are described in \S\ref{optionreference}. 

706 

43216  707 
The \qty{facts\_override} argument lets you alter the set of facts that go 
708 
through the relevance filter. It may be of the form ``(\qty{facts})'', where 

709 
\qty{facts} is a spaceseparated list of Isabelle facts (theorems, local 

36926  710 
assumptions, etc.), in which case the relevance filter is bypassed and the given 
43216  711 
facts are used. It may also be of the form ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}})'', 
712 
``(\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', or ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}}\ 

713 
\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', where the relevance filter is instructed to 

714 
proceed as usual except that it should consider \qty{facts\/_{\mathrm{1}}} 

715 
highlyrelevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant. 

36926  716 

53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

717 
If you use Isabelle/jEdit, Sledgehammer also provides an automatic mode that can 
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

718 
be enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options 
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

719 
> Isabelle > General.'' For automatic runs, only the first prover set using 
54114  720 
\textit{provers} (\S\ref{modeofoperation}) is considered (typically E), 
721 
\textit{slice} (\S\ref{modeofoperation}) is disabled, 

722 
\textit{minimize} (\S\ref{modeofoperation}) is disabled, fewer facts are 

723 
passed to the prover, \textit{fact\_filter} (\S\ref{relevancefilter}) is set to 

724 
\textit{mepo}, \textit{strict} (\S\ref{problemencoding}) is enabled, 

725 
\textit{verbose} (\S\ref{outputformat}) and \textit{debug} 

726 
(\S\ref{outputformat}) are disabled, \textit{preplay\_timeout} 

727 
(\S\ref{timeouts}) is set to 0, and \textit{timeout} (\S\ref{timeouts}) is 

728 
superseded by the ``Auto Time Limit'' option in jEdit. Sledgehammer's output is 

729 
also more concise. 

39320  730 

46242  731 
\subsection{Metis} 
732 

43216  733 
The \textit{metis} proof method has the syntax 
734 

735 
\prew 

45518  736 
\textbf{\textit{metis}}~(\qty{options})${}^?$~\qty{facts}${}^?$ 
43216  737 
\postw 
738 

45518  739 
where \qty{facts} is a list of arbitrary facts and \qty{options} is a 
740 
commaseparated list consisting of at most one $\lambda$ translation scheme 

741 
specification with the same semantics as Sledgehammer's \textit{lam\_trans} 

742 
option (\S\ref{problemencoding}) and at most one type encoding specification 

743 
with the same semantics as Sledgehammer's \textit{type\_enc} option 

744 
(\S\ref{problemencoding}). 

745 
% 

746 
The supported $\lambda$ translation schemes are \textit{hide\_lams}, 

46366  747 
\textit{lifting}, and \textit{combs} (the default). 
45518  748 
% 
749 
All the untyped type encodings listed in \S\ref{problemencoding} are supported. 

750 
For convenience, the following aliases are provided: 

751 
\begin{enum} 

48393  752 
\item[\labelitemi] \textbf{\textit{full\_types}:} Alias for \textit{poly\_guards\_query}. 
753 
\item[\labelitemi] \textbf{\textit{partial\_types}:} Alias for \textit{poly\_args}. 

754 
\item[\labelitemi] \textbf{\textit{no\_types}:} Alias for \textit{erased}. 

45518  755 
\end{enum} 
43216  756 

36926  757 
\section{Option Reference} 
758 
\label{optionreference} 

759 

43014  760 
\def\defl{\{} 
761 
\def\defr{\}} 

762 

36926  763 
\def\flushitem#1{\item[]\noindent\kern\leftmargin \textbf{#1}} 
47036  764 
\def\optrueonly#1{\flushitem{\textit{#1} $\bigl[$= \textit{true}$\bigr]$\enskip}\nopagebreak\\[\parskip]} 
43014  765 
\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} 
766 
\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} 

767 
\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} 

46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46366
diff
changeset

768 
\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} 
36926  769 
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]} 
43014  770 
\def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]} 
771 
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]} 

36926  772 
\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]} 
773 
\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} 

43014  774 
\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} 
36926  775 

776 
Sledgehammer's options are categorized as follows:\ mode of operation 

38984  777 
(\S\ref{modeofoperation}), problem encoding (\S\ref{problemencoding}), 
778 
relevance filter (\S\ref{relevancefilter}), output format 

43038  779 
(\S\ref{outputformat}), authentication (\S\ref{authentication}), and timeouts 
780 
(\S\ref{timeouts}). 

36926  781 

782 
The descriptions below refer to the following syntactic quantities: 

783 

784 
\begin{enum} 

45516  785 
\item[\labelitemi] \qtybf{string}: A string. 
786 
\item[\labelitemi] \qtybf{bool\/}: \textit{true} or \textit{false}. 

787 
\item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or 

40203  788 
\textit{smart}. 
45516  789 
\item[\labelitemi] \qtybf{int\/}: An integer. 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54788
diff
changeset

790 
\item[\labelitemi] \qtybf{float}: A floatingpoint number (e.g., 2.5 or 60) 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54788
diff
changeset

791 
expressing a number of seconds. 
45516  792 
\item[\labelitemi] \qtybf{float\_pair\/}: A pair of floatingpoint numbers 
40343
4521d56aef63
use floatingpoint numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset

793 
(e.g., 0.6 0.95). 
45516  794 
\item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}. 
36926  795 
\end{enum} 
796 

43217  797 
Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options 
47963  798 
have a negative counterpart (e.g., \textit{blocking} vs.\ 
799 
\textit{non\_blocking}). When setting Boolean options or their negative 

800 
counterparts, ``= \textit{true\/}'' may be omitted. 

36926  801 

802 
\subsection{Mode of Operation} 

803 
\label{modeofoperation} 

804 

805 
\begin{enum} 

43014  806 
\opnodefaultbrk{provers}{string} 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

807 
Specifies the automatic provers to use as a spaceseparated list (e.g., 
46299  808 
``\textit{e}~\textit{spass}~\textit{remote\_vampire\/}''). 
809 
Provers can be run locally or remotely; see \S\ref{installation} for 

810 
installation instructions. 

811 

812 
The following local provers are supported: 

36926  813 

48701  814 
\begin{sloppy} 
36926  815 
\begin{enum} 
55334
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset

816 
\item[\labelitemi] \textbf{\textit{agsyhol}:} AgsyHOL is an automatic 
52078  817 
higherorder prover developed by Fredrik Lindblad \cite{agsyHOL}, 
55334
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset

818 
with support for the TPTP typed higherorder syntax (THF0). To use AgsyHOL, set 
52078  819 
the environment variable \texttt{AGSYHOL\_HOME} to the directory that contains 
820 
the \texttt{agsyHOL} executable. Sledgehammer has been tested with version 1.0. 

821 

46643
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset

822 
\item[\labelitemi] \textbf{\textit{alt\_ergo}:} AltErgo is a polymorphic 
52078  823 
ATP developed by Bobot et al.\ \cite{altergo}. 
46643
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset

824 
It supports the TPTP polymorphic typed firstorder format (TFF1) via Why3 
53102  825 
\cite{why3}. To use AltErgo, set the environment variable \texttt{WHY3\_HOME} 
56379
d8ecce5d51cd
use AltErgo 0.95.2, the latest and greatest version
blanchet
parents:
56378
diff
changeset

826 
to the directory that contains the \texttt{why3} executable. Sledgehammer 
d8ecce5d51cd
use AltErgo 0.95.2, the latest and greatest version
blanchet
parents:
56378
diff
changeset

827 
requires AltErgo 0.95.2 and Why3 0.83. 
46643
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46640
diff
changeset

828 

45516  829 
\item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by 
42945  830 
Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3, 
831 
set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the 

46242  832 
executable, including the file name, or install the prebuilt CVC3 package from 
48006  833 
\download. Sledgehammer has been tested with version 2.2 and 2.4.1. 
42945  834 

45516  835 
\item[\labelitemi] \textbf{\textit{e}:} E is a firstorder resolution prover 
42964
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

836 
developed by Stephan Schulz \cite{schulz2002}. To use E, set the environment 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

837 
variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof} 
52757  838 
executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or 
47056  839 
install the prebuilt E package from \download. Sledgehammer has been tested with 
52757  840 
versions 1.0 to 1.8. 
48652  841 

842 
\item[\labelitemi] \textbf{\textit{e\_males}:} EMaLeS is a metaprover developed 

843 
by Daniel K\"uhlwein that implements strategy scheduling on top of E. To use 

844 
EMaLeS, set the environment variable \texttt{E\_MALES\_HOME} to the directory 

845 
that contains the \texttt{emales.py} script. Sledgehammer has been tested with 

846 
version 1.1. 

36926  847 

54694
af9cdb4989c7
added warning to documentation, based on isabelleusers thread
blanchet
parents:
54139
diff
changeset

848 
\item[\labelitemi] \textbf{\textit{e\_par}:} EPar is an experimental metaprover 
af9cdb4989c7
added warning to documentation, based on isabelleusers thread
blanchet
parents:
54139
diff
changeset

849 
developed by Josef Urban that implements strategy scheduling on top of E. To use 
af9cdb4989c7
added warning to documentation, based on isabelleusers thread
blanchet
parents:
54139
diff
changeset

850 
EPar, set the environment variable \texttt{E\_HOME} to the directory that 
af9cdb4989c7
added warning to documentation, based on isabelleusers thread
blanchet
parents:
54139
diff
changeset

851 
contains the \texttt{runepar.pl} script and the \texttt{eprover} and 
50929  852 
\texttt{epclextract} executables, or use the prebuilt E package from \download. 
54694
af9cdb4989c7
added warning to documentation, based on isabelleusers thread
blanchet
parents:
54139
diff
changeset

853 
Be aware that EPar is experimental software. It has been known to generate 
af9cdb4989c7
added warning to documentation, based on isabelleusers thread
blanchet
parents:
54139
diff
changeset

854 
zombie processes. Use at your own risks. 
50929  855 

48701  856 
\item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure 
857 
instantiationbased prover developed by Konstantin Korovin \cite{korovin2009}. 

858 
To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the 

48714  859 
directory that contains the \texttt{iprover} and \texttt{vclausify\_rel} 
860 
executables. Sledgehammer has been tested with version 0.99. 

48701  861 

862 
\item[\labelitemi] \textbf{\textit{iprover\_eq}:} iProverEq is an 

863 
instantiationbased prover with native support for equality developed by 

864 
Konstantin Korovin and Christoph Sticksel \cite{korovinsticksel2010}. To use 

865 
iProverEq, set the environment variable \texttt{IPROVER\_EQ\_HOME} to the 

48714  866 
directory that contains the \texttt{iprovereq} and \texttt{vclausify\_rel} 
867 
executables. Sledgehammer has been tested with version 0.8. 

48701  868 

45516  869 
\item[\labelitemi] \textbf{\textit{leo2}:} LEOII is an automatic 
44098  870 
higherorder prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, 
46242  871 
with support for the TPTP typed higherorder syntax (THF0). To use LEOII, set 
872 
the environment variable \texttt{LEO2\_HOME} to the directory that contains the 

52757  873 
\texttt{leo} executable. Sledgehammer requires version 1.3.4 or above. 
44098  874 

48652  875 
\item[\labelitemi] \textbf{\textit{metis}:} Although it is less powerful than 
44098  876 
the external provers, Metis itself can be used for proof search. 
877 

45516  878 
\item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic 
44098  879 
higherorder prover developed by Chad Brown et al.\ \cite{satallax}, with 
46242  880 
support for the TPTP typed higherorder syntax (THF0). To use Satallax, set the 
881 
environment variable \texttt{SATALLAX\_HOME} to the directory that contains the 

882 
\texttt{satallax} executable. Sledgehammer requires version 2.2 or above. 

44098  883 

56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

884 
\item[\labelitemi] \textbf{\textit{smt}:} The \textit{smt2} proof method with the 
48652  885 
current settings (usually:\ Z3 with proof reconstruction) can be used for proof 
886 
search. 

45380  887 

45516  888 
\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a firstorder resolution 
42964
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

889 
prover developed by Christoph Weidenbach et al.\ \cite{weidenbachetal2009}. 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

890 
To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory 
47056  891 
that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the 
47577  892 
version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from 
48006  893 
\download. Sledgehammer requires version 3.8ds or above. 
36926  894 

48652  895 
\item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a firstorder 
896 
resolution prover developed by Andrei Voronkov and his colleagues 

42964
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

897 
\cite{riazanovvoronkov2002}. To use Vampire, set the environment variable 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

898 
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire} 
48006  899 
executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., 
56380
9bb2856cc845
don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
blanchet
parents:
56379
diff
changeset

900 
``3.0''). Sledgehammer has been tested with versions 0.6 to 3.0. 
52996  901 
Versions strictly above 1.8 support the TPTP typed firstorder format (TFF0). 
40942  902 

45516  903 
\item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at 
44098  904 
SRI \cite{yices}. To use Yices, set the environment variable 
905 
\texttt{YICES\_SOLVER} to the complete path of the executable, including the 

45864  906 
file name. Sledgehammer has been tested with version 1.0.28. 
44098  907 

45516  908 
\item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at 
41740
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

909 
Microsoft Research \cite{z3}. To use Z3, set the environment variable 
4b09f8b9e012
added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents:
41738
diff
changeset

910 
\texttt{Z3\_SOLVER} to the complete path of the executable, including the file 
44421  911 
name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a 
56119
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

912 
noncommercial usereither in the environment in which Isabelle is 
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

913 
launched, in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or 
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

914 
via the ``z3\_non\_commercial'' option under ``Plugins > Plugin Options 
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

915 
> Isabelle > General'' in Isabelle/jEdit. Sledgehammer has been tested with 
2e44053fee87
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
blanchet
parents:
55334
diff
changeset

916 
versions 3.0, 3.1, 3.2, and 4.0. 
56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

917 

04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

918 
\item[\labelitemi] \textbf{\textit{z3\_new}:} Newer versions of Z3 (e.g., 4.3) 
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

919 
are treated as a different prover by Isabelle. To use these, set the environment 
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

920 
variable \texttt{Z3\_NEW\_SOLVER} to the complete path of the executable, 
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

921 
including the file name. You also need to set \texttt{Z3\_NON\_COMMERCIAL} to 
56378  922 
``yes'', as described above. Sledgehammer has been tested with versions 4.3.0 
923 
and 4.3.1. 

42945  924 
\end{enum} 
56378  925 

926 
\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be 

927 
an ATP, exploiting Z3's support for the TPTP untyped and typed firstorder 

928 
formats (FOF and TFF0). It is included for experimental purposes. It requires 

929 
version 4.3.1 of Z3 above. To use it, set the environment variable 

930 
\texttt{Z3\_TPTP\_HOME} to the directory that contains the \texttt{z3\_tptp} 

931 
executable. 

932 

48701  933 
\end{sloppy} 
42945  934 

56378  935 
In addition to the local provers, the following remote provers are supported: 
42945  936 

937 
\begin{enum} 

52078  938 
\item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of 
55334
5f5104069b33
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
blanchet
parents:
55297
diff
changeset

939 
AgsyHOL runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe2000}. 
52078  940 

45516  941 
\item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs 
36926  942 
on Geoff Sutcliffe's Miami servers \cite{sutcliffe2000}. 
943 

45516  944 
\item[\labelitemi] \textbf{\textit{remote\_e\_sine}:} ESInE is a metaprover 
47075  945 
developed by Kry\v stof Hoder \cite{sine} based on E. It runs on Geoff 
946 
Sutcliffe's Miami servers. 

44091  947 

45516  948 
\item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} EToFoF is a metaprover 
44091  949 
developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami 
45516  950 
servers. This ATP supports the TPTP typed firstorder format (TFF0). The 
44091  951 
remote version of EToFoF runs on Geoff Sutcliffe's Miami servers. 
952 

48701  953 
\item[\labelitemi] \textbf{\textit{remote\_iprover}:} The 
45339  954 
remote version of iProver runs on Geoff Sutcliffe's Miami servers 
955 
\cite{sutcliffe2000}. 

956 

48701  957 
\item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} The 
45339  958 
remote version of iProverEq runs on Geoff Sutcliffe's Miami servers 
959 
\cite{sutcliffe2000}. 

960 

45516  961 
\item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEOII 
44098  962 
runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe2000}. 
42964
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

963 

45516  964 
\item[\labelitemi] \textbf{\textit{remote\_satallax}:} The remote version of 
44098  965 
Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe2000}. 
42964
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42945
diff
changeset

966 

45516  967 
\item[\labelitemi] \textbf{\textit{remote\_snark}:} SNARK is a firstorder 
43625  968 
resolution prover developed by Stickel et al.\ \cite{snark}. It supports the 
45516  969 
TPTP typed firstorder format (TFF0). The remote version of SNARK runs on 
43625  970 
Geoff Sutcliffe's Miami servers. 
40073  971 

54788
a898e15b522a
primitive support for SPASSPirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54694
diff
changeset

972 
\item[\labelitemi] \textbf{\textit{remote\_spass\_pirate}:} SPASSPirate is a 
a898e15b522a
primitive support for SPASSPirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54694
diff
changeset

973 
highly experimental firstorder resolution prover developed by Daniel Wand. 
a898e15b522a
primitive support for SPASSPirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54694
diff
changeset

974 
The remote version of SPASSPirate run on a private server set up by Daniel 
a898e15b522a
primitive support for SPASSPirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54694
diff
changeset

975 
Wand. 
a898e15b522a
primitive support for SPASSPirate (Daniel Wand's polymorphic SPASS prototype)
blanchet
parents:
54694
diff
changeset

976 

45516  977 
\item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of 
48006  978 
Vampire runs on Geoff Sutcliffe's Miami servers. 
42945  979 

45516  980 
\item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit 
42945  981 
equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be 
43625  982 
used to prove universally quantified equations using unconditional equations, 
983 
corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister 

984 
runs on Geoff Sutcliffe's Miami servers. 

36926  985 
\end{enum} 
986 

48405
7682bc885e8a
use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents:
48393
diff
changeset

987 
By default, Sledgehammer runs a selection of CVC3, E, ESInE, SPASS, Vampire, 
53759
a198ce71de11
took out Waldmeister from list of default provers  it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
blanchet
parents:
53757
diff
changeset

988 
Yices, and Z3 in paralleleither locally or remotely, depending on the number 
53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

989 
of processor cores available. 
36926  990 

44743  991 
It is generally a good idea to run several provers in parallel. Running E, 
992 
SPASS, and Vampire for 5~seconds yields a similar success rate to running the 

993 
most effective of these for 120~seconds \cite{boehmenipkow2010}. 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

994 

43053  995 
For the \textit{min} subcommand, the default prover is \textit{metis}. If 
996 
several provers are set, the first one is used. 

997 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

998 
\opnodefault{prover}{string} 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

999 
Alias for \textit{provers}. 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

1000 

38983  1001 
\opfalse{blocking}{non\_blocking} 
1002 
Specifies whether the \textbf{sledgehammer} command should operate 

1003 
synchronously. The asynchronous (nonblocking) mode lets the user start proving 

1004 
the putative theorem manually while Sledgehammer looks for a proof, but it can 

42995
e23f61546cf0
always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
blanchet
parents:
42964
diff
changeset

1005 
also be more confusing. Irrespective of the value of this option, Sledgehammer 
53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

1006 
is always run synchronously if \textit{debug} (\S\ref{outputformat}) is 
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

1007 
enabled. 
38983  1008 

45708
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

1009 
\optrue{slice}{dont\_slice} 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset

1010 
Specifies whether the time allocated to a prover should be sliced into several 
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset

1011 
segments, each of which has its own set of possibly proverdependent options. 
42446  1012 
For SPASS and Vampire, the first slice tries the fast but incomplete 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset

1013 
setofsupport (SOS) strategy, whereas the second slice runs without it. For E, 
42446  1014 
up to three slices are tried, with different weighted search strategies and 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset

1015 
number of facts. For SMT solvers, several slices are tried with the same options 
42446  1016 
each time but fewer and fewer facts. According to benchmarks with a timeout of 
1017 
30 seconds, slicing is a valuable optimization, and you should probably leave it 

54114  1018 
enabled unless you are conducting experiments. 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset

1019 

724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset

1020 
\nopagebreak 
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset

1021 
{\small See also \textit{verbose} (\S\ref{outputformat}).} 
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42442
diff
changeset

1022 

45708
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

1023 
\opsmart{minimize}{dont\_minimize} 
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

1024 
Specifies whether the minimization tool should be invoked automatically after 
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

1025 
proof search. By default, automatic minimization takes place only if 
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

1026 
it can be done in a reasonable amount of time (as determined by 
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

1027 
the number of facts in the original proof and the time it took to find or 
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

1028 
preplay it) or the proof involves an unreasonably large number of facts. 
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

1029 

7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

1030 
\nopagebreak 
47036  1031 
{\small See also \textit{preplay\_timeout} (\S\ref{timeouts}) 
1032 
and \textit{dont\_preplay} (\S\ref{timeouts}).} 

45708
7c8bed80301f
updated Sledgehammer docs with new/renamed options
blanchet
parents:
45555
diff
changeset

1033 

53801  1034 
\opfalse{spy}{dont\_spy} 
1035 
Specifies whether Sledgehammer should record statistics in 

1036 
\texttt{\$ISA\BELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak spy\_\allowbreak sledgehammer}. 

1037 
These statistics can be useful to the developers of Sledgehammer. If you are willing to have your 

1038 
interactions recorded in the name of science, please enable this feature and send the statistics 

1039 
file every now and then to the author of this manual (\authoremail). 

1040 
To change the default value of this option globally, set the environment variable 

1041 
\texttt{SLEDGEHAMMER\_SPY} to \texttt{yes}. 

1042 

1043 
\nopagebreak 

1044 
{\small See also \textit{debug} (\S\ref{outputformat}).} 

1045 

36926  1046 
\opfalse{overlord}{no\_overlord} 
1047 
Specifies whether Sledgehammer should put its temporary files in 

1048 
\texttt{\$ISA\BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for 

1049 
debugging Sledgehammer but also unsafe if several instances of the tool are run 

48390
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48388
diff
changeset

1050 
simultaneously. The files are identified by the prefixes \texttt{prob\_} and 
4147f2bc4442
add versioning to MaSh state + cleanup dead code
blanchet
parents:
48388
diff
changeset

1051 
\texttt{mash\_}; you may safely remove them after Sledgehammer has run. 
36926  1052 

54139  1053 
\textbf{Warning:} This option is not threadsafe. Use at your own risks. 
1054 

36926  1055 
\nopagebreak 
1056 
{\small See also \textit{debug} (\S\ref{outputformat}).} 

1057 
\end{enum} 

1058 

48387  1059 
\subsection{Relevance Filter} 
1060 
\label{relevancefilter} 

1061 

1062 
\begin{enum} 

48388  1063 
\opdefault{fact\_filter}{string}{smart} 
1064 
Specifies the relevance filter to use. The following filters are available: 

1065 

1066 
\begin{enum} 

1067 
\item[\labelitemi] \textbf{\textit{mepo}:} 

1068 
The traditional memoryless MePo relevance filter. 

1069 

1070 
\item[\labelitemi] \textbf{\textit{mash}:} 

53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

1071 
The experimental MaSh machine learner. MaSh relies on the external Python 
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

1072 
program \texttt{mash.py}, which is part of Isabelle. To enable MaSh, set the 
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

1073 
environment variable \texttt{MASH} to \texttt{yes}. Persistent data is stored in 
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

1074 
the directory \texttt{\$ISABELLE\_HOME\_USER/mash}. 
48388  1075 

51024
98fb341d32e3
distinguish MeSh and smart  with smart, allow combinations of MaSh, MeSh, and MePo in different slices  and use MaSh also with SMT solvers, based on evaluation
blanchet
parents:
50929
diff
changeset

1076 
\item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the 
98fb341d32e3
distinguish MeSh and smart  with smart, allow combinations of MaSh, MeSh, and MePo in different slices  and use MaSh also with SMT solvers, based on evaluation
blanchet
parents:
50929
diff
changeset

1077 
rankings from MePo and MaSh. 
48388  1078 

51024
98fb341d32e3
distinguish MeSh and smart  with smart, allow combinations of MaSh, MeSh, and MePo in different slices  and use MaSh also with SMT solvers, based on evaluation
blanchet
parents:
50929
diff
changeset

1079 
\item[\labelitemi] \textbf{\textit{smart}:} A mixture of MePo, MaSh, and MeSh if 
98fb341d32e3
distinguish MeSh and smart  with smart, allow combinations of MaSh, MeSh, and MePo in different slices  and use MaSh also with SMT solvers, based on evaluation
blanchet
parents:
50929
diff
changeset

1080 
MaSh is enabled; otherwise, MePo. 
48388  1081 
\end{enum} 
1082 

48387  1083 
\opdefault{max\_facts}{smart\_int}{smart} 
1084 
Specifies the maximum number of facts that may be returned by the relevance 

55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

1085 
filter. If the option is set to \textit{smart} (the default), it effectively 
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

1086 
takes a value that was empirically found to be appropriate for the prover. 
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

1087 
Typical values range between 50 and 1000. 
48387  1088 

53757
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53518
diff
changeset

1089 
For the MaShrelated commands \textit{learn\_isar}, \textit{learn\_prover}, 
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53518
diff
changeset

1090 
\textit{relearn\_isar}, and \textit{relearn\_prover}, this option specifies the 
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53518
diff
changeset

1091 
maximum number of facts from the background library that should be learned 
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53518
diff
changeset

1092 
($\infty$ by default). 
8d1a059ebcdb
reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents:
53518
diff
changeset

1093 

48387  1094 
\opdefault{fact\_thresholds}{float\_pair}{\upshape 0.45~0.85} 
1095 
Specifies the thresholds above which facts are considered relevant by the 

1096 
relevance filter. The first threshold is used for the first iteration of the 

1097 
relevance filter and the second threshold is used for the last iteration (if it 

1098 
is reached). The effective threshold is quadratically interpolated for the other 

1099 
iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems 

1100 
are relevant and 1 only theorems that refer to previously seen constants. 

1101 

48388  1102 
\optrue{learn}{dont\_learn} 
1103 
Specifies whether MaSh should be run automatically by Sledgehammer to learn the 

53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

1104 
available theories (and hence provide more accurate results). Learning takes 
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53759
diff
changeset

1105 
place only if MaSh is enabled. 
48388  1106 

48387  1107 
\opdefault{max\_new\_mono\_instances}{int}{smart} 
1108 
Specifies the maximum number of monomorphic instances to generate beyond 

1109 
\textit{max\_facts}. The higher this limit is, the more monomorphic instances 

1110 
are potentially generated. Whether monomorphization takes place depends on the 

55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

1111 
type encoding used. If the option is set to \textit{smart} (the default), it 
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

1112 
takes a value that was empirically found to be appropriate for the prover. For 
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

1113 
most provers, this value is 100. 
48387  1114 

1115 
\nopagebreak 

1116 
{\small See also \textit{type\_enc} (\S\ref{problemencoding}).} 

1117 

1118 
\opdefault{max\_mono\_iters}{int}{smart} 

1119 
Specifies the maximum number of iterations for the monomorphization fixpoint 

1120 
construction. The higher this limit is, the more monomorphic instances are 

1121 
potentially generated. Whether monomorphization takes place depends on the 

55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

1122 
type encoding used. If the option is set to \textit{smart} (the default), it 
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

1123 
takes a value that was empirically found to be appropriate for the prover. 
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55290
diff
changeset

1124 
For most provers, this value is 3. 
48387  1125 

1126 
\nopagebreak 

1127 
{\small See also \textit{type\_enc} (\S\ref{problemencoding}).} 

1128 
\end{enum} 

1129 

36926  1130 
\subsection{Problem Encoding} 
1131 
\label{problemencoding} 

1132 

45516  1133 
\newcommand\comb[1]{\const{#1}} 
1134 

36926  1135 
\begin{enum} 
45516  1136 
\opdefault{lam\_trans}{string}{smart} 
1137 
Specifies the $\lambda$ translation scheme to use in ATP problems. The supported 

1138 
translation schemes are listed below: 

1139 

1140 
\begin{enum} 

1141 
\item[\labelitemi] \textbf{\textit{hide\_lams}:} Hide the $\lambda$abstractions 

1142 
by replacing them by unspecified fresh constants, effectively disabling all 

1143 
reasoning under $\lambda$abstractions. 

1144 

46366  1145 
\item[\labelitemi] \textbf{\textit{lifting}:} Introduce a new 
45516  1146 
supercombinator \const{c} for each cluster of $n$~$\lambda$abstractions, 
1147 
defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$lifting). 

1148 

46366  1149 
\item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry 
45516  1150 
combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators 
1151 
enable the ATPs to synthesize $\lambda$terms but tend to yield bulkier formulas 

1152 
than $\lambda$lifting: The translation is quadratic in the worst case, and the 

1153 
equational definitions of the combinators are very prolific in the context of 

1154 
resolution. 

1155 

46366  1156 
\item[\labelitemi] \textbf{\textit{combs\_and\_lifting}:} Introduce a new 
45516  1157 
supercombinator \const{c} for each cluster of $\lambda$abstractions and characterize it both using a 
1158 
lifted equation $\const{c}~x_1~\ldots~x_n = t$ and via Curry combinators. 

1159 

46366  1160 
\item[\labelitemi] \textbf{\textit{combs\_or\_lifting}:} For each cluster of 
1161 
$\lambda$abstractions, heuristically choose between $\lambda$lifting and Curry 

1162 
combinators. 

1163 

45516  1164 
\item[\labelitemi] \textbf{\textit{keep\_lams}:} 
1165 
Keep the $\lambda$abstractions in the generated problems. This is available 

1166 
only with provers that support the THF0 syntax. 

1167 

1168 
\item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used 

1169 
depends on the ATP and should be the most efficient scheme for that ATP. 

1170 
\end{enum} 

1171 

46366  1172 
For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting}, 
1173 
irrespective of the value of this option. 

45516  1174 

46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46366
diff
changeset

1175 
\opsmartx{uncurried\_aliases}{no\_uncurried\_aliases} 
46411  1176 
Specifies whether fresh function symbols should be generated as aliases for 
1177 
applications of curried functions in ATP problems. 

46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46366
diff
changeset

1178 

43627
ecd4bb7a8bc0
update documentation after "type_enc" renaming + fixed a few other outofdate factlets
blanchet
parents:
43625
diff
changeset

1179 
\opdefault{type\_enc}{string}{smart} 
ecd4bb7a8bc0
update documentation after "type_enc" renaming + fixed a few other outofdate factlets
blanchet
parents:
43625
diff
changeset

1180 
Specifies the type encoding to use in ATP problems. Some of the type encodings 
ecd4bb7a8bc0
update documentation after "type_enc" renaming + fixed a few other outofdate factlets
blanchet
parents:
43625
diff
changeset

1181 
are unsound, meaning that they can give rise to spurious proofs 
48093  1182 
(unreconstructible using \textit{metis}). The type encodings are 
46300  1183 
listed below, with an indication of their soundness in parentheses. 
48093  1184 
An asterisk (*) indicates that the encoding is slightly incomplete for 
56120
04c37dfef684
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
blanchet
parents:
56119
diff
changeset

1185 
reconstruction with \textit{metis}, unless the \textit{strict} option (described 
46302  1186 
below) is enabled. 
42228  1187 

1188 
\begin{enum} 

48090  1189 
\item[\labelitemi] \textbf{\textit{erased} (unsound):} No type information is 
46300  1190 
supplied to the ATP, not even to resolve overloading. Types are simply erased. 
42582  1191 

45516  1192 
\item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using 
46300  1193 
a predicate \const{g}$(\tau, t)$ that guards bound 
48090  1194 
variables. Constants are annotated with their types, supplied as extra 
42887
771be1dcfef6
document new type system and soundness properties of the different systems
blanchet
parents:
42884
diff
changeset

1195 
arguments, to resolve overloading. 
42685  1196 

45516  1197 
\item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is 
46300  1198 
tagged with its type using a function $\const{t\/}(\tau, t)$. 
42887
771be1dcfef6
document new type system and soundness properties of the different systems
blanchet
parents:
42884
diff
changeset

1199 

45516  1200 
\item[\labelitemi] \textbf{\textit{poly\_args} (unsound):} 
43990  1201 
Like for \textit{poly\_guards} constants are annotated with their types to 
43002
e88fde86e4c2
mention contributions from LCP and explain metis and metisFT encodings
blanchet
parents:
42996
diff
changeset

1202 
resolve overloading, but otherwise no type information is encoded. This 
48090  1203 
is the default encoding used by the \textit{metis} command. 
42685  1204 

45516  1205 
\item[\labelitemi] 
42722  1206 
\textbf{% 
44494
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset

1207 
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\ 
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset

1208 
\textit{raw\_mono\_args} (unsound):} \\ 
43990  1209 
Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args}, 
42722  1210 
respectively, but the problem is additionally monomorphized, meaning that type 
1211 
variables are instantiated with heuristically chosen ground types. 

1212 
Monomorphization can simplify reasoning but also leads to larger fact bases, 

1213 
which can slow down the ATPs. 

42582  1214 

45516  1215 
\item[\labelitemi] 
42722  1216 
\textbf{% 
44494
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset

1217 
\textit{mono\_guards}, \textit{mono\_tags} (sound); 
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset

1218 
\textit{mono\_args} (unsound):} \\ 
42722  1219 
Similar to 
44494
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44423
diff
changeset

1220 
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and 
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44 