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