diff --git a/src/Doc/Sledgehammer/document/root.tex b/src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex +++ b/src/Doc/Sledgehammer/document/root.tex @@ -1,1337 +1,1331 @@ \documentclass[a4paper,12pt]{article} \usepackage[T1]{fontenc} \usepackage{amsmath} \usepackage{amssymb} \usepackage{color} \usepackage{footmisc} \usepackage{graphicx} %\usepackage{mathpazo} \usepackage{multicol} \usepackage{stmaryrd} %\usepackage[scaled=.85]{beramono} \usepackage{isabelle,iman,pdfsetup} \newcommand\download{\url{https://isabelle.in.tum.de/components/}} \let\oldS=\S \def\S{\oldS\,} \def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}} \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$} \newcommand\const[1]{\textsf{#1}} %\oddsidemargin=4.6mm %\evensidemargin=4.6mm %\textwidth=150mm %\topmargin=4.6mm %\headheight=0mm %\headsep=0mm %\textheight=234mm \def\Colon{\mathord{:\mkern-1.5mu:}} %\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}} %\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}} \def\lparr{\mathopen{(\mkern-4mu\mid}} \def\rparr{\mathclose{\mid\mkern-4mu)}} \def\unk{{?}} \def\undef{(\lambda x.\; \unk)} %\def\unr{\textit{others}} \def\unr{\ldots} \def\Abs#1{\hbox{\rm{\guillemetleft}}{\,#1\,}\hbox{\rm{\guillemetright}}} \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}} \urlstyle{tt} \renewcommand\_{\hbox{\textunderscore\kern-.05ex}} \hyphenation{Isa-belle super-posi-tion zipper-posi-tion} \begin{document} %%% TYPESETTING %\renewcommand\labelitemi{$\bullet$} \renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}} \title{\includegraphics[scale=0.5]{isabelle_logo} \\[4ex] Hammering Away \\[\smallskipamount] \Large A User's Guide to Sledgehammer for Isabelle/HOL} \author{\hbox{} \\ Jasmin Blanchette \\ {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\[4\smallskipamount] {\normalsize with contributions from} \\[4\smallskipamount] Martin Desharnais \\ {\normalsize Forschungsinstitut CODE, Universit\"at der Bundeswehr M\"unchen} \\[4\smallskipamount] Lawrence C. Paulson \\ {\normalsize Computer Laboratory, University of Cambridge} \\ \hbox{}} \maketitle \tableofcontents \setlength{\parskip}{.7em plus .2em minus .1em} \setlength{\parindent}{0pt} \setlength{\abovedisplayskip}{\parskip} \setlength{\abovedisplayshortskip}{.9\parskip} \setlength{\belowdisplayskip}{\parskip} \setlength{\belowdisplayshortskip}{.9\parskip} % general-purpose enum environment with correct spacing \newenvironment{enum}% {\begin{list}{}{% \setlength{\topsep}{.1\parskip}% \setlength{\partopsep}{.1\parskip}% \setlength{\itemsep}{\parskip}% \advance\itemsep by-\parsep}} {\end{list}} \def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin \advance\rightskip by\leftmargin} \def\post{\vskip0pt plus1ex\endgroup} \def\prew{\pre\advance\rightskip by-\leftmargin} \def\postw{\post} \section{Introduction} \label{introduction} Sledgehammer is a tool that applies automatic theorem provers (ATPs) and satisfiability-modulo-theories (SMT) solvers on the current goal.% \footnote{The distinction between ATPs and SMT solvers is convenient but mostly historical.} % The supported ATPs include agsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E \cite{schulz-2019}, iProver \cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III \cite{leo3}, Satallax \cite{satallax}, SPASS \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, Waldmeister \cite{waldmeister}, and Zipperposition \cite{cruanes-2014}. The ATPs are run either locally or remotely via the System\-On\-TPTP web service \cite{sutcliffe-2000}. The supported SMT solvers are CVC4 \cite{cvc4}, veriT \cite{bouton-et-al-2009}, and Z3 \cite{de-moura-2008}. These are always run locally. The problem passed to the external provers (or solvers) consists of your current goal together with a heuristic selection of hundreds of facts (theorems) from the current theory context, filtered by relevance. The result of a successful proof search is some source text that typically reconstructs the proof within Isabelle. For ATPs, the reconstructed proof typically relies on the general-purpose \textit{metis} proof method, which integrates the Metis ATP in Isabelle/HOL with explicit inferences going through the kernel. Thus its results are correct by construction. For Isabelle/jEdit users, Sledgehammer provides an automatic mode that can be enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options > Isabelle > General.'' In this mode, a reduced version of Sledgehammer is run on every newly entered theorem for a few seconds. \newbox\boxA \setbox\boxA=\hbox{\texttt{NOSPAM}} \newcommand\authoremail{\texttt{jasmin.blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak gmail.\allowbreak com}} To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is imported---this is rarely a problem in practice since it is part of \textit{Main}. Examples of Sledgehammer use can be found in the \texttt{src/HOL/Metis\_Examples} directory. Comments and bug reports concerning Sledgehammer or this manual should be directed to the author at \authoremail. \section{Installation} \label{installation} Sledgehammer is part of Isabelle, so you do not need to install it. However, it relies on third-party automatic provers (ATPs and SMT solvers). Among the ATPs, agsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, and Zipperposition can be run locally; in addition, agsyHOL, Alt-Ergo, E, iProver, LEO-II, Leo-III, Satallax, Vampire, Waldmeister, and Zipperposition are available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers CVC4, veriT, and Z3 can be run locally. There are three main ways to install automatic provers on your machine: \begin{sloppy} \begin{enum} \item[\labelitemi] If you installed an official Isabelle package, it should already include properly set up executables for CVC4, E, SPASS, Vampire, veriT, Z3, and Zipperposition ready to use. \item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC4, E, SPASS, Vampire, veriT, Z3, and Zipperposition binary packages from \download. Extract the archives, then add a line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}% \footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at startup. Its value can be retrieved by executing \texttt{isabelle} \texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.} file with the absolute path to the prover. For example, if the \texttt{components} file does not exist yet and you extracted SPASS to \texttt{/usr/local/spass-3.8ds}, create it with the single line \prew \texttt{/usr/local/spass-3.8ds} \postw in it. \item[\labelitemi] If you prefer to build agsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, or Zipperposition manually, set the environment variable \texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME}, \texttt{LEO3\_HOME}, \texttt{SATALLAX\_HOME}, or \texttt{ZIPPERPOSITION\_HOME} to the directory that contains the \texttt{agsyHOL}, \texttt{eprover} (or \texttt{eprover-ho}), \texttt{leo}, \texttt{leo3}, \texttt{satallax}, or \texttt{zipperposition} executable; for Alt-Ergo, set the environment variable \texttt{WHY3\_HOME} to the directory that contains the \texttt{why3} executable. Ideally, you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION}, \texttt{LEO3\_VERSION}, \texttt{SATALLAX\_VERSION}, or \texttt{ZIPPERPOSITION\_VERSION} to the prover's version number (e.g., ``3.6''). Similarly, if you want to install CVC4, veriT, or Z3, set the environment variable \texttt{CVC4\_\allowbreak SOLVER}, \texttt{ISABELLE\_\allowbreak VERIT}, or \texttt{Z3\_SOLVER} to the complete path of the executable, \emph{including the file name}. Ideally, also set \texttt{CVC4\_VERSION}, \texttt{VERIT\_VERSION}, or \texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.4.0''). \end{enum} \end{sloppy} To check whether the provers are successfully installed, try out the example in \S\ref{first-steps}. If the remote versions of any of these provers is used (identified by the prefix ``\textit{remote\_\/}''), or if the local versions fail to solve the easy goal presented there, something must be wrong with the installation. \section{First Steps} \label{first-steps} To illustrate Sledgehammer in context, let us start a theory file and attempt to prove a simple lemma: \prew \textbf{theory}~\textit{Scratch} \\ \noindent\hbox{}\quad \textbf{imports}~\textit{Main} \\ \textbf{begin} \\[2\smallskipamount] % \textbf{lemma} ``$[a] = [b] \,\Longrightarrow\, a = b$'' \\ \textbf{sledgehammer} \postw Instead of issuing the \textbf{sledgehammer} command, you can also use the Sledgehammer panel in Isabelle/jEdit. Sledgehammer might produce something like the following output after a few seconds: \prew \slshape e found a proof\ldots \\ cvc4 found a proof\ldots \\ z3 found a proof\ldots \\ vampire found a proof\ldots \\ e: Try this: \textbf{by} \textit{simp} (0.3 ms) \\ cvc4: Try this: \textbf{by} \textit{simp} (0.4 ms) \\ z3: Try this: \textbf{by} \textit{simp} (0.5 ms) \\ vampire: Try this: \textbf{by} \textit{simp} (0.3 ms) \\ QED \postw Sledgehammer ran CVC4, E, Vampire, Z3, and possibly other provers in parallel. The list may vary depending on which provers are installed and how many processor cores are available. For each successful prover, Sledgehammer gives a one-line Isabelle proof. Rough timings are shown in parentheses, indicating how fast the call is. You can click the proof to insert it into the theory text. In addition, you can ask Sledgehammer for an Isar text proof by enabling the \textit{isar\_proofs} option (\S\ref{output-format}): \prew \textbf{sledgehammer} [\textit{isar\_proofs}] \postw When Isar proof construction is successful, it can yield proofs that are more readable and also faster than \textit{metis} or \textit{smt} one-line proofs. This feature is experimental. \section{Hints} \label{hints} This section presents a few hints that should help you get the most out of Sledgehammer. Frequently asked questions are answered in \S\ref{frequently-asked-questions}. %\newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak} \newcommand\point[1]{\subsection{\slshape #1}} \point{Presimplify the goal} For best results, first simplify your problem by calling \textit{auto} or at least \textit{safe} followed by \textit{simp\_all}. The SMT solvers provide arithmetic decision procedures, but the ATPs typically do not (or if they do, Sledgehammer does not use it yet). Apart from Waldmeister, they are not particularly good at heavy rewriting, but because they regard equations as undirected, they often prove theorems that require the reverse orientation of a \textit{simp} rule. Higher-order problems can be tackled, but the success rate is better for first-order problems. \point{Familiarize yourself with the main options} Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of the options are very specialized, but serious users of the tool should at least familiarize themselves with the following options: \begin{enum} \item[\labelitemi] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies the automatic provers (ATPs and SMT solvers) that should be run whenever Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{cvc4 e vampire zipperposition\/}''). \item[\labelitemi] \textbf{\textit{max\_facts}} (\S\ref{relevance-filter}) specifies the maximum number of facts that should be passed to the provers. By default, the value is prover-dependent but varies between about 50 and 1000. If the provers time out, you can try lowering this value to, say, 25 or 50 and see if that helps. \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies that Isar proofs should be generated, in addition to one-line proofs. The length of the Isar proofs can be controlled by setting \textit{compress} (\S\ref{output-format}). \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the provers' time limit. It is set to 30 seconds by default. \end{enum} Options can be set globally using \textbf{sledgehammer\_params} (\S\ref{command-syntax}). The command also prints the list of all available options with their current value. Fact selection can be influenced by specifying ``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer} call to ensure that certain facts are included, or simply ``$(\textit{my\_facts})$'' to force Sledgehammer to run only with $\textit{my\_facts}$ (and any facts chained into the goal). \section{Frequently Asked Questions} \label{frequently-asked-questions} This sections answers frequently (and infrequently) asked questions about Sledgehammer. It is a good idea to skim over it now even if you do not have any questions at this stage. \point{Which facts are passed to the automatic provers?} Sledgehammer heuristically selects a subset of lemmas from the currently loaded libraries. The component that performs this selection is called \emph{relevance filter} (\S\ref{relevance-filter}). \begin{enum} \item[\labelitemi] The traditional relevance filter, \emph{MePo} (\underline{Me}ng--\underline{Pau}lson), assigns a score to every available fact (lemma, theorem, definition, or axiom) based upon how many constants that fact shares with the goal. This process iterates to include facts relevant to those just accepted. The constants are weighted to give unusual ones greater significance. MePo copes best when the goal contains some unusual constants; if all the constants are common, it is unable to discriminate among the hundreds of facts that are picked up. The filter is also memoryless: It has no information about how many times a particular fact has been used in a proof, and it cannot learn. \item[\labelitemi] An alternative to MePo is \emph{MaSh} (\underline{Ma}chine Learner for \underline{S}ledge\underline{h}ammer). It applies machine learning to the problem of finding relevant facts. \item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh. This is the default. \end{enum} The number of facts included in a problem varies from prover to prover, since some provers get overwhelmed more easily than others. You can show the number of facts given using the \textit{verbose} option (\S\ref{output-format}) and the actual facts using \textit{debug} (\S\ref{output-format}). Sledgehammer is good at finding short proofs combining a handful of existing lemmas. If you are looking for longer proofs, you must typically restrict the number of facts, by setting the \textit{max\_facts} option (\S\ref{relevance-filter}) to, say, 25 or 50. You can also influence which facts are actually selected in a number of ways. If you simply want to ensure that a fact is included, you can specify it using the syntax ``$(\textit{add}{:}~\textit{my\_facts})$''. For example: % \prew \textbf{sledgehammer} (\textit{add}: \textit{hd.simps} \textit{tl.simps}) \postw % The specified facts then replace the least relevant facts that would otherwise be included; the other selected facts remain the same. If you want to direct the selection in a particular direction, you can specify the facts via \textbf{using}: % \prew \textbf{using} \textit{hd.simps} \textit{tl.simps} \\ \textbf{sledgehammer} \postw % The facts are then more likely to be selected than otherwise, and if they are selected at a given iteration of MePo, they also influence which facts are selected at subsequent iterations. \point{Why does Metis fail to reconstruct the proof?} There are many reasons. If Metis runs seemingly forever, that is a sign that the proof is too difficult for it. Metis's search is complete for first-order logic with equality, so if the proof was found by a superposition-based ATP such as E, SPASS, or Vampire, Metis should \emph{eventually} find it---in principle. In some rare cases, \textit{metis} fails fairly quickly, and you get the error message ``One-line proof reconstruction failed.'' This indicates that Sledgehammer determined that the goal is provable, but the proof is, for technical reasons, beyond \textit{metis}'s power. You can then try again with the \textit{strict} option (\S\ref{problem-encoding}). \point{What are the \textit{full\_types}, \textit{no\_types}, and \\ \textit{mono\_tags} arguments to Metis?} The \textit{metis}~(\textit{full\_types}) proof method and its cousin \textit{metis}~(\textit{mono\_tags}) are fully-typed versions of Metis. It is somewhat slower than \textit{metis}, but the proof search is fully typed, and it also includes more powerful rules such as the axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in higher-order positions (e.g., in set comprehensions). The method is tried as a fallback when \textit{metis} fails, and it is sometimes generated by Sledgehammer instead of \textit{metis} if the proof obviously requires type information or if \textit{metis} failed when Sledgehammer preplayed the proof. % At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types}) uses no type information at all during the proof search, which is more efficient but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally generated by Sledgehammer. % See the \textit{type\_enc} option (\S\ref{problem-encoding}) for details. Incidentally, if you ever see warnings such as \prew \slshape Metis: Falling back on ``\textit{metis} (\textit{full\_types})'' \postw for a successful \textit{metis} proof, you can advantageously pass the \textit{full\_types} option to \textit{metis} directly. \point{And what are the \textit{lifting} and \textit{opaque\_lifting} \\ arguments to Metis?} Orthogonally to the encoding of types, it is important to choose an appropriate translation of $\lambda$-abstractions. Metis supports three translation schemes, in decreasing order of power: Curry combinators (the default), $\lambda$-lifting, and a ``hiding'' scheme that disables all reasoning under $\lambda$-abstractions. See the \textit{lam\_trans} option (\S\ref{problem-encoding}) for details. \point{Are the generated proofs minimal?} Automatic provers frequently use many more facts than are necessary. Sledgehammer includes a proof minimization tool that takes a set of facts returned by a given prover and repeatedly calls a prover or proof method with subsets of those facts to find a minimal set. Reducing the number of facts typically helps reconstruction and declutters the proof documents. \point{A strange error occurred---what should I do?} Sledgehammer tries to give informative error messages. Please report any strange error to the author at \authoremail. \point{Auto can solve it---why not Sledgehammer?} Problems can be easy for \textit{auto} and difficult for automatic provers, but the reverse is also true, so do not be discouraged if your first attempts fail. Because the system refers to all theorems known to Isabelle, it is particularly suitable when your goal has a short proof but requires lemmas that you do not know about. \point{Why are there so many options?} Sledgehammer's philosophy is that it should work out of the box, without user guidance. Most of the options are meant to be used by the Sledgehammer developers for experiments. \section{Command Syntax} \label{command-syntax} \subsection{Sledgehammer} \label{sledgehammer} Sledgehammer can be invoked at any point when there is an open goal by entering the \textbf{sledgehammer} command in the theory file. Its general syntax is as follows: \prew \textbf{sledgehammer} \qty{subcommand}$^?$ \qty{options}$^?$ \qty{facts\_override}$^?$ \qty{num}$^?$ \postw In the general syntax, the \qty{subcommand} may be any of the following: \begin{enum} \item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on subgoal number \qty{num} (1 by default), with the given options and facts. \item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of automatic provers supported by Sledgehammer. See \S\ref{installation} and \S\ref{mode-of-operation} for more information on how to install automatic provers. \item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}. \end{enum} In addition, the following subcommands provide finer control over machine learning with MaSh: \begin{enum} \item[\labelitemi] \textbf{\textit{unlearn}:} Resets MaSh, erasing any persistent state. \item[\labelitemi] \textbf{\textit{learn\_isar}:} Invokes MaSh on the current theory to process all the available facts, learning from their Isabelle/Isar proofs. This happens automatically at Sledgehammer invocations if the \textit{learn} option (\S\ref{relevance-filter}) is enabled. \item[\labelitemi] \textbf{\textit{learn\_prover}:} Invokes MaSh on the current theory to process all the available facts, learning from proofs generated by automatic provers. The prover to use and its timeout can be set using the \textit{prover} (\S\ref{mode-of-operation}) and \textit{timeout} (\S\ref{timeouts}) options. It is recommended to perform learning using a first-order ATP (such as E, SPASS, and Vampire) as opposed to a higher-order ATP or an SMT solver. \item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn} followed by \textit{learn\_isar}. \item[\labelitemi] \textbf{\textit{relearn\_prover}:} Same as \textit{unlearn} followed by \textit{learn\_prover}. \end{enum} Sledgehammer's behavior can be influenced by various \qty{options}, which can be specified in brackets after the \textbf{sledgehammer} command. The \qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1, \ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. For example: \prew \textbf{sledgehammer} [\textit{isar\_proofs}, \,\textit{timeout} = 120] \postw Default values can be set using \textbf{sledgehammer\_\allowbreak params}: \prew \textbf{sledgehammer\_params} \qty{options} \postw The supported options are described in \S\ref{option-reference}. The \qty{facts\_override} argument lets you alter the set of facts that go through the relevance filter. It may be of the form ``(\qty{facts})'', where \qty{facts} is a space-separated list of Isabelle facts (theorems, local assumptions, etc.), in which case the relevance filter is bypassed and the given facts are used. It may also be of the form ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}})'', ``(\textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', or ``(\textit{add}:\ \qty{facts\/_{\mathrm{1}}}\ \textit{del}:\ \qty{facts\/_{\mathrm{2}}})'', where the relevance filter is instructed to proceed as usual except that it should consider \qty{facts\/_{\mathrm{1}}} highly-relevant and \qty{facts\/_{\mathrm{2}}} fully irrelevant. If you use Isabelle/jEdit, Sledgehammer also provides an automatic mode that can be enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options > Isabelle > General.'' For automatic runs, only the first prover set using \textit{provers} (\S\ref{mode-of-operation}) is considered, \textit{dont\_slice} (\S\ref{timeouts}) is set, fewer facts are passed to the prover, \textit{fact\_filter} (\S\ref{relevance-filter}) is set to \textit{mepo}, \textit{strict} (\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled, and \textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Time Limit'' option in jEdit. Sledgehammer's output is also more concise. \subsection{Metis} \label{metis} The \textit{metis} proof method has the syntax \prew \textbf{\textit{metis}}~(\qty{options})${}^?$~\qty{facts}${}^?$ \postw where \qty{facts} is a list of arbitrary facts and \qty{options} is a comma-separated list consisting of at most one $\lambda$ translation scheme specification with the same semantics as Sledgehammer's \textit{lam\_trans} option (\S\ref{problem-encoding}) and at most one type encoding specification with the same semantics as Sledgehammer's \textit{type\_enc} option (\S\ref{problem-encoding}). % The supported $\lambda$ translation schemes are \textit{opaque\_lifting}, \textit{lifting}, and \textit{combs} (the default). % All the untyped type encodings listed in \S\ref{problem-encoding} are supported. For convenience, the following aliases are provided: \begin{enum} \item[\labelitemi] \textbf{\textit{full\_types}:} Alias for \textit{poly\_guards\_query}. \item[\labelitemi] \textbf{\textit{partial\_types}:} Alias for \textit{poly\_args}. \item[\labelitemi] \textbf{\textit{no\_types}:} Alias for \textit{erased}. \end{enum} \section{Option Reference} \label{option-reference} \def\defl{\{} \def\defr{\}} \def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}} \def\optrueonly#1{\flushitem{\textit{#1} $\bigl[$= \textit{true}$\bigr]$\enskip}\nopagebreak\\[\parskip]} \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]} \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]} \def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]} \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]} \def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]} \def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} \def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]} Sledgehammer's options are categorized as follows:\ mode of operation (\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}), relevance filter (\S\ref{relevance-filter}), output format (\S\ref{output-format}), regression testing (\S\ref{regression-testing}), and timeouts (\S\ref{timeouts}). The descriptions below refer to the following syntactic quantities: \begin{enum} \item[\labelitemi] \qtybf{string}: A string. \item[\labelitemi] \qtybf{bool\/}: \textit{true} or \textit{false}. \item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or \textit{smart}. \item[\labelitemi] \qtybf{int\/}: An integer. \item[\labelitemi] \qtybf{float}: A floating-point number (e.g., 2.5 or 60) expressing a number of seconds. \item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers (e.g., 0.6 0.95). \item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}. \end{enum} Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options have a negative counterpart (e.g., \textit{minimize} vs.\ \textit{dont\_minimize}). When setting Boolean options or their negative counterparts, ``= \textit{true\/}'' may be omitted. \subsection{Mode of Operation} \label{mode-of-operation} \begin{enum} \opnodefaultbrk{provers}{string} Specifies the automatic provers to use as a space-separated list (e.g., ``\textit{cvc4}~\textit{e}~\textit{spass}~\textit{vampire\/}''). Provers can be run locally or remotely; see \S\ref{installation} for installation instructions. By default, \textit{provers} is set to the list of all installed local provers. The following local provers are supported: \begin{sloppy} \begin{enum} \item[\labelitemi] \textbf{\textit{agsyhol}:} agsyHOL is an automatic higher-order prover developed by Fredrik Lindblad \cite{agsyHOL}. To use agsyHOL, set the environment variable \texttt{AGSYHOL\_HOME} to the directory that contains the \texttt{agsyHOL} executable. \item[\labelitemi] \textbf{\textit{alt\_ergo}:} Alt-Ergo is a polymorphic ATP developed by Bobot et al.\ \cite{alt-ergo}. It supports the TPTP polymorphic typed first-order format (TF1) via Why3 \cite{why3}. To use Alt-Ergo, set the environment variable \texttt{WHY3\_HOME} to the directory that contains the \texttt{why3} executable. Sledgehammer requires Alt-Ergo 0.95.2 and Why3 0.83. \item[\labelitemi] \textbf{\textit{cvc4}:} CVC4 is an SMT solver developed by Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc4}. To use CVC4, set the environment variable \texttt{CVC4\_SOLVER} to the complete path of the executable, including the file name, or install the prebuilt CVC4 package from \download. \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover developed by Stephan Schulz \cite{schulz-2019}. To use E, set the environment variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or install the prebuilt E package from \download. \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the directory that contains the \texttt{iproveropt} executable. iProver depends on Vampire to clausify problems, so make sure that Vampire is installed as well. \item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, with support for the TPTP typed higher-order syntax (TH0). To use LEO-II, set the environment variable \texttt{LEO2\_HOME} to the directory that contains the \texttt{leo} executable. \item[\labelitemi] \textbf{\textit{leo3}:} Leo-III is an automatic higher-order prover developed by Alexander Steen, Christoph Benzm\"uller, et al.\ \cite{leo3}, with support for the TPTP typed higher-order syntax (TH0). To use Leo-III, set the environment variable \texttt{LEO3\_HOME} to the directory that contains the \texttt{leo3} executable. \item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with support for the TPTP typed higher-order syntax (TH0). To use Satallax, set the environment variable \texttt{SATALLAX\_HOME} to the directory that contains the \texttt{satallax} executable. \item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from \download. \item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution prover developed by Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire} executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``4.2.2''). \item[\labelitemi] \textbf{\textit{verit}:} veriT \cite{bouton-et-al-2009} is an SMT solver developed by David D\'eharbe, Pascal Fontaine, and their colleagues. It is designed to produce detailed proofs for reconstruction in proof assistants. To use veriT, set the environment variable \texttt{ISABELLE\_VERIT} to the complete path of the executable, including the file name. \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at Microsoft Research \cite{de-moura-2008}. To use Z3, set the environment variable \texttt{Z3\_SOLVER} to the complete path of the executable, including the file name. -\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to -be an ATP, exploiting Z3's support for the TPTP typed first-order format (TF0). -It is included for experimental purposes. To use it, set the environment -variable \texttt{Z3\_TPTP\_HOME} to the directory that contains the -\texttt{z3\_tptp} executable. - \item[\labelitemi] \textbf{\textit{zipperposition}:} Zipperposition \cite{cruanes-2014} is a higher-order superposition prover developed by Simon Cruanes, Petar Vukmirovi\'c, and colleagues. To use Zipperposition, set the environment variable \texttt{ZIPPERPOSITION\_HOME} to the directory that contains the \texttt{zipperposition} executable and \texttt{ZIPPERPOSITION\_VERSION} to the version number (e.g., ``2.0.1''). \end{enum} \end{sloppy} Moreover, the following remote provers are supported: \begin{enum} \item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of agsyHOL runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_alt\_ergo}:} The remote version of Alt-Ergo runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_iprover}:} The remote version of iProver runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be used to prove universally quantified equations using unconditional equations, corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister runs on Geoff Sutcliffe's Miami servers. \item[\labelitemi] \textbf{\textit{remote\_zipperposition}:} The remote version of Zipperposition runs on Geoff Sutcliffe's Miami servers. \end{enum} By default, Sledgehammer runs a subset of CVC4, E, SPASS, Vampire, veriT, and Z3 in parallel, either locally or remotely---depending on the number of processor cores available and on which provers are actually installed. It is generally desirable to run several provers in parallel. \opnodefault{prover}{string} Alias for \textit{provers}. \optrue{minimize}{dont\_minimize} Specifies whether the proof minimization tool should be invoked automatically after proof search. \nopagebreak {\small See also \textit{preplay\_timeout} (\S\ref{timeouts}) and \textit{dont\_preplay} (\S\ref{timeouts}).} \opfalse{spy}{dont\_spy} Specifies whether Sledgehammer should record statistics in \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak spy\_\allowbreak sledgehammer}. These statistics can be useful to the developers of Sledgehammer. If you are willing to have your interactions recorded in the name of science, please enable this feature and send the statistics file every now and then to the author of this manual (\authoremail). To change the default value of this option globally, set the environment variable \texttt{SLEDGEHAMMER\_SPY} to \textit{yes}. \nopagebreak {\small See also \textit{debug} (\S\ref{output-format}).} \opfalse{overlord}{no\_overlord} Specifies whether Sledgehammer should put its temporary files in \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for debugging Sledgehammer but also unsafe if several instances of the tool are run simultaneously. The files are identified by the prefixes \texttt{prob\_} and \texttt{mash\_}; you may safely remove them after Sledgehammer has run. \textbf{Warning:} This option is not thread-safe. Use at your own risks. \nopagebreak {\small See also \textit{debug} (\S\ref{output-format}).} \end{enum} \subsection{Relevance Filter} \label{relevance-filter} \begin{enum} \opdefault{fact\_filter}{string}{smart} Specifies the relevance filter to use. The following filters are available: \begin{enum} \item[\labelitemi] \textbf{\textit{mepo}:} The traditional memoryless MePo relevance filter. \item[\labelitemi] \textbf{\textit{mash}:} The MaSh machine learner. Three learning algorithms are provided: \begin{enum} \item[\labelitemi] \textbf{\textit{nb}} is an implementation of naive Bayes. \item[\labelitemi] \textbf{\textit{knn}} is an implementation of $k$-nearest neighbors. \item[\labelitemi] \textbf{\textit{nb\_knn}} (also called \textbf{\textit{yes}} and \textbf{\textit{sml}}) is a combination of naive Bayes and $k$-nearest neighbors. \end{enum} In addition, the special value \textit{none} is used to disable machine learning by default (cf.\ \textit{smart} below). The default algorithm is \textit{nb\_knn}. The algorithm can be selected by setting the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle > General'' in Isabelle/jEdit. Persistent data for both algorithms is stored in the directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak mash}. \item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the rankings from MePo and MaSh. \item[\labelitemi] \textbf{\textit{smart}:} A combination of MePo, MaSh, and MeSh. If the learning algorithm is set to be \textit{none}, \textit{smart} behaves like MePo. \end{enum} \opdefault{max\_facts}{smart\_int}{smart} Specifies the maximum number of facts that may be returned by the relevance filter. If the option is set to \textit{smart} (the default), it effectively takes a value that was empirically found to be appropriate for the prover. Typical values lie between 50 and 1000. \opdefault{fact\_thresholds}{float\_pair}{\upshape 0.45~0.85} Specifies the thresholds above which facts are considered relevant by the relevance filter. The first threshold is used for the first iteration of the relevance filter and the second threshold is used for the last iteration (if it is reached). The effective threshold is quadratically interpolated for the other iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems are relevant and 1 only theorems that refer to previously seen constants. \optrue{learn}{dont\_learn} Specifies whether Sledgehammer invocations should run MaSh to learn the available theories (and hence provide more accurate results). Learning takes place only if MaSh is enabled. \opdefault{max\_new\_mono\_instances}{int}{smart} Specifies the maximum number of monomorphic instances to generate beyond \textit{max\_facts}. The higher this limit is, the more monomorphic instances are potentially generated. Whether monomorphization takes place depends on the type encoding used. If the option is set to \textit{smart} (the default), it takes a value that was empirically found to be appropriate for the prover. For most provers, this value is 100. \nopagebreak {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).} \opdefault{max\_mono\_iters}{int}{smart} Specifies the maximum number of iterations for the monomorphization fixpoint construction. The higher this limit is, the more monomorphic instances are potentially generated. Whether monomorphization takes place depends on the type encoding used. If the option is set to \textit{smart} (the default), it takes a value that was empirically found to be appropriate for the prover. For most provers, this value is 3. \nopagebreak {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).} \opdefault{induction\_rules}{string}{exclude} Specifies whether induction rules should be considered as relevant facts. The following behaviors are available: \begin{enum} \item[\labelitemi] \textbf{\textit{exclude}:} Induction rules are ignored by the relevance filter. \item[\labelitemi] \textbf{\textit{instantiate}:} Induction rules are instantiated based on the goal and then considered by the relevance filter. \item[\labelitemi] \textbf{\textit{include}:} Induction rules are considered by the relevance filter. \end{enum} \end{enum} \subsection{Problem Encoding} \label{problem-encoding} \newcommand\comb[1]{\const{#1}} \begin{enum} \opdefault{lam\_trans}{string}{smart} Specifies the $\lambda$ translation scheme to use in ATP problems. The supported translation schemes are listed below: \begin{enum} \item[\labelitemi] \textbf{\textit{lifting}:} Introduce a new supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions, defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting). \item[\labelitemi] \textbf{\textit{opaque\_lifting}:} Same as \textit{lifting}, except that the supercombinators are kept opaque, i.e. they are unspecified fresh constants. This effectively disables all reasoning under $\lambda$-abstractions. \item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators enable the ATPs to synthesize $\lambda$-terms but tend to yield bulkier formulas than $\lambda$-lifting: The translation is quadratic in the worst case, and the equational definitions of the combinators are very prolific in the context of resolution. \item[\labelitemi] \textbf{\textit{opaque\_combs}:} Same as \textit{combs}, except that the combinators are kept opaque, i.e. without equational definitions. \item[\labelitemi] \textbf{\textit{combs\_and\_lifting}:} Introduce a new supercombinator \const{c} for each cluster of $\lambda$-abstractions and characterize it both using a lifted equation $\const{c}~x_1~\ldots~x_n = t$ and via Curry combinators. \item[\labelitemi] \textbf{\textit{combs\_or\_lifting}:} For each cluster of $\lambda$-abstractions, heuristically choose between $\lambda$-lifting and Curry combinators. \item[\labelitemi] \textbf{\textit{keep\_lams}:} Keep the $\lambda$-abstractions in the generated problems. This is available only with provers that support $\lambda$s. \item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used depends on the ATP and should be the most efficient scheme for that ATP. \end{enum} For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting}, irrespective of the value of this option. \opsmartx{uncurried\_aliases}{no\_uncurried\_aliases} Specifies whether fresh function symbols should be generated as aliases for applications of curried functions in ATP problems. \opdefault{type\_enc}{string}{smart} Specifies the type encoding to use in ATP problems. Some of the type encodings are unsound, meaning that they can give rise to spurious proofs (unreconstructible using \textit{metis}). The type encodings are listed below, with an indication of their soundness in parentheses. An asterisk (*) indicates that the encoding is slightly incomplete for reconstruction with \textit{metis}, unless the \textit{strict} option (described below) is enabled. \begin{enum} \item[\labelitemi] \textbf{\textit{erased} (unsound):} No type information is supplied to the ATP, not even to resolve overloading. Types are simply erased. \item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using a predicate \const{g}$(\tau, t)$ that guards bound variables. Constants are annotated with their types, supplied as extra arguments, to resolve overloading. \item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is tagged with its type using a function $\const{t\/}(\tau, t)$. \item[\labelitemi] \textbf{\textit{poly\_args} (unsound):} Like for \textit{poly\_guards} constants are annotated with their types to resolve overloading, but otherwise no type information is encoded. This is the default encoding used by the \textit{metis} proof method. \item[\labelitemi] \textbf{% \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\ \textit{raw\_mono\_args} (unsound):} \\ Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args}, respectively, but the problem is additionally monomorphized, meaning that type variables are instantiated with heuristically chosen ground types. Monomorphization can simplify reasoning but also leads to larger fact bases, which can slow down the ATPs. \item[\labelitemi] \textbf{% \textit{mono\_guards}, \textit{mono\_tags} (sound); \textit{mono\_args} \\ (unsound):} \\ Similar to \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and \textit{raw\_mono\_\allowbreak args}, respectively but types are mangled in constant names instead of being supplied as ground term arguments. The binary predicate $\const{g}(\tau, t)$ becomes a unary predicate $\const{g\_}\tau(t)$, and the binary function $\const{t}(\tau, t)$ becomes a unary function $\const{t\_}\tau(t)$. \item[\labelitemi] \textbf{\textit{mono\_native} (sound):} Exploits native first-order types if the prover supports the TF0, TF1, TH0, or TH1 syntax; otherwise, falls back on \textit{mono\_guards}. The problem is monomorphized. \item[\labelitemi] \textbf{\textit{mono\_native\_fool} (sound):} Exploits native first-order types, including Booleans, if the prover supports the TFX0, TFX1, TH0, or TH1 syntax; otherwise, falls back on \textit{mono\_native}. The problem is monomorphized. \item[\labelitemi] \textbf{\textit{mono\_native\_higher}, \textit{mono\_native\_higher\_fool} \\ (sound):} Exploits native higher-order types, including Booleans if ending with ``\textit{\_fool}'', if the prover supports the TH0 syntax; otherwise, falls back on \textit{mono\_native} or \textit{mono\_native\_fool}. The problem is monomorphized. \item[\labelitemi] \textbf{\textit{poly\_native}, \textit{poly\_native\_fool}, \textit{poly\_native\_higher}, \\ \textit{poly\_native\_higher\_fool} (sound):} Exploits native first-order polymorphic types if the prover supports the TF1, TFX1, or TH1 syntax; otherwise, falls back on \textit{mono\_native}, \textit{mono\_native\_fool}, \textit{mono\_native\_higher}, or \textit{mono\_native\_higher\_fool}. \item[\labelitemi] \textbf{% \textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\ \textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\ \textit{mono\_native}? (sound*):} \\ The type encodings \textit{poly\_guards}, \textit{poly\_tags}, \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards}, \textit{mono\_tags}, and \textit{mono\_native} are fully typed and sound. For each of these, Sledgehammer also provides a lighter variant identified by a question mark (`\hbox{?}')\ that detects and erases monotonic types, notably infinite types. (For \textit{mono\_native}, the types are not actually erased but rather replaced by a shared uniform type of individuals.) As argument to the \textit{metis} proof method, the question mark is replaced by a \hbox{``\textit{\_query\/}''} suffix. \item[\labelitemi] \textbf{% \textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\ \textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\ (sound*):} \\ Even lighter versions of the `\hbox{?}' encodings. As argument to the \textit{metis} proof method, the `\hbox{??}' suffix is replaced by \hbox{``\textit{\_query\_query\/}''}. \item[\labelitemi] \textbf{% \textit{poly\_guards}@, \textit{poly\_tags}@, \textit{raw\_mono\_guards}@, \\ \textit{raw\_mono\_tags}@ (sound*):} \\ Alternative versions of the `\hbox{??}' encodings. As argument to the \textit{metis} proof method, the `\hbox{@}' suffix is replaced by \hbox{``\textit{\_at\/}''}. \item[\labelitemi] \textbf{\textit{poly\_args}?, \textit{raw\_mono\_args}? (unsound):} \\ Lighter versions of \textit{poly\_args} and \textit{raw\_mono\_args}. \item[\labelitemi] \textbf{\textit{smart}:} The actual encoding used depends on the ATP and should be the most efficient sound encoding for that ATP. \end{enum} For SMT solvers, the type encoding is always \textit{mono\_native}, irrespective of the value of this option. \nopagebreak {\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter}) and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).} \opfalse{strict}{non\_strict} Specifies whether Sledgehammer should run in its strict mode. In that mode, sound type encodings marked with an asterisk (*) above are made complete for reconstruction with \textit{metis}, at the cost of some clutter in the generated problems. This option has no effect if \textit{type\_enc} is deliberately set to an unsound encoding. \end{enum} \subsection{Output Format} \label{output-format} \begin{enum} \opfalse{verbose}{quiet} Specifies whether the \textbf{sledgehammer} command should explain what it does. \opfalse{debug}{no\_debug} Specifies whether Sledgehammer should display additional debugging information beyond what \textit{verbose} already displays. Enabling \textit{debug} also enables \textit{verbose} behind the scenes. \nopagebreak {\small See also \textit{spy} (\S\ref{mode-of-operation}) and \textit{overlord} (\S\ref{mode-of-operation}).} \opdefault{max\_proofs}{int}{\upshape 4} Specifies the maximum number of proofs to display before stopping. This is a soft limit. \opsmart{isar\_proofs}{no\_isar\_proofs} Specifies whether Isar proofs should be output in addition to one-line proofs. The construction of Isar proof is still experimental and may sometimes fail; however, when they succeed they are usually faster and more intelligible than one-line proofs. If the option is set to \textit{smart} (the default), Isar proofs are only generated when no working one-line proof is available. \opdefault{compress}{int}{smart} Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs} is explicitly enabled. A value of $n$ indicates that each Isar proof step should correspond to a group of up to $n$ consecutive proof steps in the ATP proof. If the option is set to \textit{smart} (the default), the compression factor is 10 if the \textit{isar\_proofs} option is explicitly enabled; otherwise, it is $\infty$. \optrueonly{dont\_compress} Alias for ``\textit{compress} = 1''. \optrue{try0}{dont\_try0} Specifies whether standard proof methods such as \textit{auto} and \textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs. The collection of methods is roughly the same as for the \textbf{try0} command. \optrue{smt\_proofs}{no\_smt\_proofs} Specifies whether the \textit{smt} proof method should be tried in addition to Isabelle's built-in proof methods. \end{enum} \subsection{Regression Testing} \label{regression-testing} \begin{enum} \opnodefault{expect}{string} Specifies the expected outcome, which must be one of the following: \begin{enum} \item[\labelitemi] \textbf{\textit{some}:} Sledgehammer found a proof. \item[\labelitemi] \textbf{\textit{none}:} Sledgehammer found no proof. \item[\labelitemi] \textbf{\textit{timeout}:} Sledgehammer timed out. \item[\labelitemi] \textbf{\textit{unknown}:} Sledgehammer encountered some problem. \end{enum} Sledgehammer emits an error if the actual outcome differs from the expected outcome. This option is useful for regression testing. \nopagebreak {\small See also \textit{timeout} (\S\ref{timeouts}).} \end{enum} \subsection{Timeouts} \label{timeouts} \begin{enum} \opdefault{timeout}{float}{\upshape 30} Specifies the maximum number of seconds that the automatic provers should spend searching for a proof. This excludes problem preparation and is a soft limit. \opdefault{slices}{int}{\upshape 6 times the number of cores detected} Specifies the number of time slices. Each time slice corresponds to a prover invocation and has its own set of options. For example, for SPASS, one slice might specify the fast but incomplete set-of-support (SOS) strategy with 100 relevant lemmas, whereas other slices might run without SOS and with 500 lemmas. Slicing (and thereby parallelism) can be disable by setting \textit{slices} to 1. Since slicing is a valuable optimization, you should probably leave it enabled unless you are conducting experiments. \nopagebreak {\small See also \textit{verbose} (\S\ref{output-format}).} \optrueonly{dont\_slice} Alias for ``\textit{slices} = 1''. \opdefault{preplay\_timeout}{float}{\upshape 1} Specifies the maximum number of seconds that \textit{metis} or other proof methods should spend trying to ``preplay'' the found proof. If this option is set to 0, no preplaying takes place, and no timing information is displayed next to the suggested proof method calls. \nopagebreak {\small See also \textit{minimize} (\S\ref{mode-of-operation}).} \optrueonly{dont\_preplay} Alias for ``\textit{preplay\_timeout} = 0''. \end{enum} \section{Mirabelle Testing Tool} \label{mirabelle} The \texttt{isabelle mirabelle} tool executes Sledgehammer or other advisory tools (e.g., Nitpick) or tactics (e.g., \textit{auto}) on all subgoals emerging in a theory. It is typically used to measure the success rate of a proof tool on some benchmark. Its command-line usage is as follows: {\small \begin{verbatim} Usage: isabelle mirabelle [OPTIONS] [SESSIONS ...] Options are: -A ACTION add to list of actions -O DIR output directory for log files (default: "mirabelle") -T THEORY theory restriction: NAME or NAME[FIRST_LINE:LAST_LINE] -m INT max. no. of calls to each action (0: unbounded) (default 0) -s INT run actions on every nth goal (0: uniform distribution) (default 1) -t SECONDS timeout in seconds for each action (default 30) ... Apply the given ACTIONs at all theories and proof steps of the specified sessions. The absence of theory restrictions (option -T) means to check all theories fully. Otherwise only the named theories are checked. \end{verbatim} } Option \texttt{-A ACTION} specifies an action to run on all subgoals. When specified multiple times, all actions are performed in parallel on all selected subgoals. Available actions are \texttt{arith}, \texttt{metis}, \texttt{quickcheck}, \texttt{sledgehammer}, \texttt{sledgehammer\_filter}, and \texttt{try0}. Option \texttt{-O DIR} specifies the output directory, which is created if needed. In this directory, a log file named "mirabelle.log" records the position of each tested subgoal and the result of executing the actions. Option \texttt{-T THEORY} restricts the subgoals to those emerging from this theory. When not provided, all subgoals from are theories are selected. When provided multiple times, the union of all specified theories' subgoals is selected. Option \texttt{-m INT} specifies a maximum number of goals on which the action are run. Option \texttt{-s INT} specifies a stride, effectively running the actions on every $n$th goal. Option \texttt{-t SECONDS} specifies a generic timeout that the actions may interpret differently. More specific documentation about low-level options, the \texttt{ACTION} parameter, and its corresponding options can be found in the Isabelle tool usage by entering \texttt{isabelle mirabelle -?} on the command line. The following subsections assume that the environment variable \texttt{AFP} is defined and points to a release of the Archive of Formal Proofs. \subsection{Example of Benchmarking Sledgehammer} \begin{verbatim} isabelle mirabelle -d '$AFP' -O output \ -A "sledgehammer[provers = e, timeout = 30]" \ VeriComp \end{verbatim} This command specifies to run the Sledgehammer action, using the E prover with a timeout of 30 seconds, on all subgoals emerging from all theory in the AFP session VeriComp. The results are written to \texttt{output/mirabelle.log}. \begin{verbatim} isabelle mirabelle -d '$AFP' -O output \ -T Semantics -T Compiler \ -A "sledgehammer[provers = e, timeout = 30]" \ VeriComp \end{verbatim} This command also specifies to run the Sledgehammer action, but this time only on subgoals emerging from theories Semantics or Compiler. \subsection{Example of Benchmarking Multiple Tools} \begin{verbatim} isabelle mirabelle -d '$AFP' -O output -t 10 \ -A "try0" -A "metis" \ VeriComp \end{verbatim} This command specifies two actions running the \textbf{try0} and \textbf{metis} commands, respectively, each with a timeout of 10 seconds. The results are written to \texttt{output/mirabelle.log}. \subsection{Example of Generating TPTP Files} \begin{verbatim} isabelle mirabelle -d '$AFP' -O output \ -A "sledgehammer[provers = e, timeout = 5, keep_probs = true]" \ VeriComp \end{verbatim} This command generates TPTP files using Sledgehammer. Since the file is generated at the very beginning of every Sledgehammer invocation, a timeout of five seconds making the prover fail faster speeds up processing the subgoals. The results are written in an action-specific subdirectory of the specified output directory (\texttt{output}). A TPTP file is generated for each subgoal. \let\em=\sl \bibliography{manual}{} \bibliographystyle{abbrv} \end{document} diff --git a/src/HOL/TPTP/atp_problem_import.ML b/src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML +++ b/src/HOL/TPTP/atp_problem_import.ML @@ -1,324 +1,323 @@ (* Title: HOL/TPTP/atp_problem_import.ML Author: Jasmin Blanchette, TU Muenchen Copyright 2012 Import TPTP problems as Isabelle terms or goals. *) signature ATP_PROBLEM_IMPORT = sig val read_tptp_file : theory -> (string * term -> 'a) -> string -> 'a list * ('a list * 'a list) * local_theory val nitpick_tptp_file : theory -> int -> string -> unit val refute_tptp_file : theory -> int -> string -> unit val can_tac : Proof.context -> (Proof.context -> tactic) -> term -> bool val SOLVE_TIMEOUT : int -> string -> tactic -> tactic val atp_tac : local_theory -> int -> (string * string) list -> int -> term list -> string -> int -> tactic val smt_solver_tac : string -> local_theory -> int -> tactic val make_conj : term list * term list -> term list -> term val sledgehammer_tptp_file : theory -> int -> string -> unit val isabelle_tptp_file : theory -> int -> string -> unit val isabelle_hot_tptp_file : theory -> int -> string -> unit val translate_tptp_file : theory -> string -> string -> unit end; structure ATP_Problem_Import : ATP_PROBLEM_IMPORT = struct open ATP_Util open ATP_Problem open ATP_Proof open ATP_Problem_Generate val debug = false val overlord = false (** TPTP parsing **) fun exploded_absolute_path file_name = Path.explode file_name |> (fn path => path |> not (Path.is_absolute path) ? Path.append (Path.explode "$PWD")) fun read_tptp_file thy postproc file_name = let fun has_role role (_, role', _, _) = (role' = role) fun get_prop f (name, _, P, _) = P |> f |> close_form |> pair name |> postproc val path = exploded_absolute_path file_name val ((_, _, problem), thy) = TPTP_Interpret.interpret_file true [Path.dir path, Path.explode "$TPTP"] path [] [] thy val (conjs, defs_and_nondefs) = problem |> List.partition (has_role TPTP_Syntax.Role_Conjecture) ||> List.partition (has_role TPTP_Syntax.Role_Definition) in (map (get_prop I) conjs, apply2 (map (get_prop Logic.varify_global)) defs_and_nondefs, Named_Target.theory_init thy) end (** Nitpick **) fun aptrueprop f ((t0 as \<^Const_>\Trueprop\) $ t1) = t0 $ f t1 | aptrueprop f t = f t fun is_legitimate_tptp_def \<^Const_>\Trueprop for t\ = is_legitimate_tptp_def t | is_legitimate_tptp_def \<^Const_>\HOL.eq _ for t u\ = (is_Const t orelse is_Free t) andalso not (exists_subterm (curry (op =) t) u) | is_legitimate_tptp_def _ = false fun nitpick_tptp_file thy timeout file_name = let val (conjs, (defs, nondefs), lthy) = read_tptp_file thy snd file_name val thy = Proof_Context.theory_of lthy val (defs, pseudo_defs) = defs |> map (ATP_Util.abs_extensionalize_term lthy #> aptrueprop (hol_open_form I)) |> List.partition (is_legitimate_tptp_def o perhaps (try HOLogic.dest_Trueprop) o ATP_Util.unextensionalize_def) val nondefs = pseudo_defs @ nondefs val state = Proof.init lthy val params = [("card", "1-100"), ("box", "false"), ("max_threads", "1"), ("batch_size", "5"), ("falsify", if null conjs then "false" else "true"), ("verbose", "true"), ("debug", if debug then "true" else "false"), ("overlord", if overlord then "true" else "false"), ("show_consts", "true"), ("format", "1"), ("max_potential", "0"), ("timeout", string_of_int timeout), ("tac_timeout", string_of_int ((timeout + 49) div 50))] |> Nitpick_Commands.default_params thy val i = 1 val n = 1 val step = 0 val subst = [] in Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst defs nondefs (case conjs of conj :: _ => conj | [] => \<^prop>\True\); () end (** Refute **) fun refute_tptp_file thy timeout file_name = let fun print_szs_of_outcome falsify s = "% SZS status " ^ (if s = "genuine" then if falsify then "CounterSatisfiable" else "Satisfiable" else "GaveUp") |> writeln val (conjs, (defs, nondefs), lthy) = read_tptp_file thy snd file_name val params = [("maxtime", string_of_int timeout), ("maxvars", "100000")] in Refute.refute_term lthy params (defs @ nondefs) (case conjs of conj :: _ => conj | [] => \<^prop>\True\) |> print_szs_of_outcome (not (null conjs)) end (** Sledgehammer and Isabelle (combination of provers) **) fun can_tac ctxt tactic conj = can (Goal.prove_internal ctxt [] (Thm.cterm_of ctxt conj)) (fn [] => tactic ctxt) fun SOLVE_TIMEOUT seconds name tac st = let val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s") val result = Timeout.apply (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) () handle Timeout.TIMEOUT _ => NONE | ERROR _ => NONE in (case result of NONE => (writeln ("FAILURE: " ^ name); Seq.empty) | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st')) end fun nitpick_finite_oracle_tac lthy timeout i th = let fun is_safe (Type (\<^type_name>\fun\, Ts)) = forall is_safe Ts | is_safe \<^typ>\prop\ = true | is_safe \<^typ>\bool\ = true | is_safe _ = false val conj = Thm.term_of (Thm.cprem_of th i) in if exists_type (not o is_safe) conj then Seq.empty else let val thy = Proof_Context.theory_of lthy val state = Proof.init lthy val params = [("box", "false"), ("max_threads", "1"), ("verbose", "true"), ("debug", if debug then "true" else "false"), ("overlord", if overlord then "true" else "false"), ("max_potential", "0"), ("timeout", string_of_int timeout)] |> Nitpick_Commands.default_params thy val i = 1 val n = 1 val step = 0 val subst = [] val (outcome, _) = Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst [] [] conj in if outcome = "none" then ALLGOALS (Skip_Proof.cheat_tac lthy) th else Seq.empty end end fun atp_tac lthy completeness override_params timeout assms prover = let val thy = Proof_Context.theory_of lthy val assm_ths0 = map (Skip_Proof.make_thm thy) assms val ((assm_name, _), lthy) = lthy |> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 3 else 0) |> Local_Theory.note ((\<^binding>\thms\, []), assm_ths0) fun ref_of th = (Facts.named (Thm.derivation_name th), []) val ref_of_assms = (Facts.named assm_name, []) in Sledgehammer_Tactics.sledgehammer_as_oracle_tac lthy ([("debug", if debug then "true" else "false"), ("overlord", if overlord then "true" else "false"), ("provers", prover), ("timeout", string_of_int timeout)] @ (if completeness > 0 then [("type_enc", if completeness = 1 then "mono_native" else "poly_tags")] else []) @ override_params) {add = ref_of_assms :: map ref_of [ext, @{thm someI}], del = [], only = true} [] end fun sledgehammer_tac demo lthy timeout assms i = let val frac = if demo then 16 else 12 fun slice mult completeness prover = SOLVE_TIMEOUT (mult * timeout div frac) (prover ^ (if completeness > 0 then "(" ^ string_of_int completeness ^ ")" else "")) (atp_tac lthy completeness [] (mult * timeout div frac) assms prover i) in slice 2 0 ATP_Proof.spassN ORELSE slice 2 0 ATP_Proof.vampireN ORELSE slice 2 0 ATP_Proof.eN - ORELSE slice 2 0 ATP_Proof.z3_tptpN ORELSE slice 1 1 ATP_Proof.spassN ORELSE slice 1 2 ATP_Proof.eN ORELSE slice 1 1 ATP_Proof.vampireN ORELSE slice 1 2 ATP_Proof.vampireN ORELSE (if demo then slice 2 0 ATP_Proof.satallaxN ORELSE slice 2 0 ATP_Proof.leo2N else no_tac) end fun smt_solver_tac solver lthy = let val lthy = lthy |> Context.proof_map (SMT_Config.select_solver solver) in SMT_Solver.smt_tac lthy [] end fun auto_etc_tac lthy timeout assms i = SOLVE_TIMEOUT (timeout div 20) "nitpick" (nitpick_finite_oracle_tac lthy (timeout div 20) i) ORELSE SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac lthy i) ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac lthy i) ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass" (auto_tac lthy THEN ALLGOALS (atp_tac lthy 0 [] (timeout div 5) assms ATP_Proof.spassN)) ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac lthy i) ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" lthy i) ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc4" (smt_solver_tac "cvc4" lthy i) ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac lthy i) ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac lthy i) ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac lthy [] i) ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac lthy i) fun make_conj (defs, nondefs) conjs = Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => \<^prop>\False\) fun print_szs_of_success conjs success = writeln ("% SZS status " ^ (if success then if null conjs then "Unsatisfiable" else "Theorem" else "GaveUp")) fun sledgehammer_tptp_file thy timeout file_name = let val (conjs, assms, lthy) = read_tptp_file thy snd file_name val conj = make_conj ([], []) conjs val assms = op @ assms in can_tac lthy (fn lthy => sledgehammer_tac true lthy timeout assms 1) conj |> print_szs_of_success conjs end fun generic_isabelle_tptp_file demo thy timeout file_name = let val (conjs, assms, lthy) = read_tptp_file thy snd file_name val conj = make_conj ([], []) conjs val full_conj = make_conj assms conjs val assms = op @ assms val (last_hope_atp, last_hope_completeness) = if demo then (ATP_Proof.satallaxN, 0) else (ATP_Proof.vampireN, 2) in (can_tac lthy (fn lthy => auto_etc_tac lthy (timeout div 2) assms 1) full_conj orelse can_tac lthy (fn lthy => sledgehammer_tac demo lthy (timeout div 2) assms 1) conj orelse can_tac lthy (fn lthy => SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)") (atp_tac lthy last_hope_completeness [] timeout assms last_hope_atp 1)) full_conj) |> print_szs_of_success conjs end val isabelle_tptp_file = generic_isabelle_tptp_file false val isabelle_hot_tptp_file = generic_isabelle_tptp_file true (** Translator between TPTP(-like) file formats **) fun translate_tptp_file thy format_str file_name = let val (conjs, (defs, nondefs), lthy) = read_tptp_file thy I file_name val conj = make_conj ([], []) (map snd conjs) val (format, type_enc, lam_trans) = (case format_str of "FOF" => (FOF, "mono_guards??", liftingN) | "TF0" => (TFF (Monomorphic, Without_FOOL), "mono_native", liftingN) | "TH0" => (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN) | "DFG" => (DFG Monomorphic, "mono_native", liftingN) | _ => error ("Unknown format " ^ quote format_str ^ " (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")")) val generate_info = false val uncurried_aliases = false val readable_names = true val presimp = true val facts = map (apfst (rpair (Global, Non_Rec_Def))) defs @ map (apfst (rpair (Global, General))) nondefs val (atp_problem, _, _, _) = generate_atp_problem lthy generate_info format Hypothesis (type_enc_of_string Strict type_enc) Translator lam_trans uncurried_aliases readable_names presimp [] conj facts val ord = Sledgehammer_ATP_Systems.effective_term_order lthy spassN val ord_info = K [] val lines = lines_of_atp_problem format ord ord_info atp_problem in List.app Output.physical_stdout lines end end; diff --git a/src/HOL/Tools/ATP/atp_proof.ML b/src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML +++ b/src/HOL/Tools/ATP/atp_proof.ML @@ -1,727 +1,717 @@ (* Title: HOL/Tools/ATP/atp_proof.ML Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Claire Quigley, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Author: Mathias Fleury, ENS Rennes Abstract representation of ATP proofs and TSTP/SPASS syntax. *) signature ATP_PROOF = sig type 'a atp_type = 'a ATP_Problem.atp_type type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term type atp_formula_role = ATP_Problem.atp_formula_role type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula type 'a atp_problem = 'a ATP_Problem.atp_problem exception UNRECOGNIZED_ATP_PROOF of unit datatype atp_failure = MaybeUnprovable | Unprovable | GaveUp | ProofMissing | ProofIncomplete | ProofUnparsable | UnsoundProof of bool * string list | TimedOut | Inappropriate | OutOfResources | MalformedInput | MalformedOutput | Interrupted | Crashed | InternalError | UnknownError of string type atp_step_name = string * string list type ('a, 'b) atp_step = atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list val agsyholN : string val alt_ergoN : string val cvc4N : string val eN : string val iproverN : string val leo2N : string val leo3N : string val satallaxN : string val spassN : string val vampireN : string val veritN : string val waldmeisterN : string val z3N : string - val z3_tptpN : string val zipperpositionN : string val remote_prefix : string val dummy_fofN : string val dummy_tfxN : string val dummy_thfN : string val agsyhol_core_rule : string val spass_input_rule : string val spass_pre_skolemize_rule : string val spass_skolemize_rule : string - val z3_tptp_core_rule : string val short_output : bool -> string -> string val string_of_atp_failure : atp_failure -> string val extract_important_message : string -> string val extract_known_atp_failure : (atp_failure * string) list -> string -> atp_failure option val extract_tstplike_proof_and_outcome : bool -> (string * string) list -> (atp_failure * string) list -> string -> string * atp_failure option val is_same_atp_step : atp_step_name -> atp_step_name -> bool val scan_general_id : string list -> string * string list val parse_fol_formula : string list -> (string, string atp_type, (string, string atp_type) atp_term, string) atp_formula * string list val clean_up_atp_proof_dependencies : string atp_proof -> string atp_proof val map_term_names_in_atp_proof : (string -> string) -> string atp_proof -> string atp_proof val nasty_atp_proof : string Symtab.table -> string atp_proof -> string atp_proof val skip_term : string list -> string * string list val parse_hol_formula : string list -> ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, 'c) ATP_Problem.atp_formula * string list val dummy_atype : string ATP_Problem.atp_type val role_of_tptp_string : string -> ATP_Problem.atp_formula_role val parse_line : string -> ('a * string ATP_Problem.atp_problem_line list) list -> string list -> ((string * string list) * ATP_Problem.atp_formula_role * (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, 'c) ATP_Problem.atp_formula * string * (string * 'd list) list) list * string list val core_inference : 'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role * ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list val vampire_step_name_ord : (string * 'a) ord val core_of_agsyhol_proof : string -> string list option val string_of_atp_step : ('a -> string) -> ('b -> string) -> ('a, 'b) atp_step -> string val atp_proof_of_tstplike_proof : string -> string atp_problem -> string -> string atp_proof end; structure ATP_Proof : ATP_PROOF = struct open ATP_Util open ATP_Problem val agsyholN = "agsyhol" val alt_ergoN = "alt_ergo" val cvc4N = "cvc4" val eN = "e" val iproverN = "iprover" val leo2N = "leo2" val leo3N = "leo3" val satallaxN = "satallax" val spassN = "spass" val vampireN = "vampire" val veritN = "verit" val waldmeisterN = "waldmeister" val z3N = "z3" -val z3_tptpN = "z3_tptp" val zipperpositionN = "zipperposition" val remote_prefix = "remote_" val dummy_fofN = "dummy_fof" val dummy_tfxN = "dummy_tfx" val dummy_thfN = "dummy_thf" val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *) val spass_input_rule = "Inp" val spass_pre_skolemize_rule = "__Sko0" (* arbitrary *) val spass_skolemize_rule = "__Sko" (* arbitrary *) -val z3_tptp_core_rule = "__z3_tptp_core" (* arbitrary *) exception UNRECOGNIZED_ATP_PROOF of unit datatype atp_failure = MaybeUnprovable | Unprovable | GaveUp | ProofMissing | ProofIncomplete | ProofUnparsable | UnsoundProof of bool * string list | TimedOut | Inappropriate | OutOfResources | MalformedInput | MalformedOutput | Interrupted | Crashed | InternalError | UnknownError of string fun short_output verbose output = if verbose then if output = "" then "No details available" else elide_string 1000 output else "" fun from_lemmas [] = "" | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) fun string_of_atp_failure MaybeUnprovable = "Problem maybe unprovable" | string_of_atp_failure Unprovable = "Unprovable problem" | string_of_atp_failure GaveUp = "Gave up" | string_of_atp_failure ProofMissing = "Claims the conjecture is a theorem but did not provide a proof" | string_of_atp_failure ProofIncomplete = "Claims the conjecture is a theorem but provided an incomplete proof" | string_of_atp_failure ProofUnparsable = "Claims the conjecture is a theorem but provided an unparsable proof" | string_of_atp_failure (UnsoundProof (false, ss)) = "Derived the lemma \"False\"" ^ from_lemmas ss ^ ", probably due to the use of an unsound type encoding" | string_of_atp_failure (UnsoundProof (true, ss)) = "Derived the lemma \"False\"" ^ from_lemmas ss ^ ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)" | string_of_atp_failure TimedOut = "Timed out" | string_of_atp_failure Inappropriate = "Problem outside the prover's scope" | string_of_atp_failure OutOfResources = "Ran out of resources" | string_of_atp_failure MalformedInput = "Malformed problem" | string_of_atp_failure MalformedOutput = "Malformed output" | string_of_atp_failure Interrupted = "Interrupted" | string_of_atp_failure Crashed = "Crashed" | string_of_atp_failure InternalError = "Internal prover error" | string_of_atp_failure (UnknownError s) = "Prover error" ^ (if s = "" then " (pass the \"verbose\" option for details)" else ":\n" ^ s) fun extract_delimited (begin_delim, end_delim) output = (case first_field begin_delim output of SOME (_, tail) => (case first_field "\n" tail of SOME (_, tail') => if end_delim = "" then tail' else (case first_field end_delim tail' of SOME (body, _) => body | NONE => "") | NONE => "") | NONE => "") val tstp_important_message_delims = ("% SZS start RequiredInformation", "% SZS end RequiredInformation") fun extract_important_message output = (case extract_delimited tstp_important_message_delims output of "" => "" | s => s |> space_explode "\n" |> filter_out (curry (op =) "") |> map (perhaps (try (unprefix "%"))) |> map (perhaps (try (unprefix " "))) |> space_implode "\n " |> quote) (* Splits by the first possible of a list of delimiters. *) fun extract_tstplike_proof delims output = (case apply2 (find_first (fn s => String.isSubstring s output)) (ListPair.unzip delims) of (SOME begin_delim, SOME end_delim) => extract_delimited (begin_delim, end_delim) output | _ => "") fun extract_known_atp_failure known_failures output = known_failures |> find_first (fn (_, pattern) => String.isSubstring pattern output) |> Option.map fst fun extract_tstplike_proof_and_outcome verbose proof_delims known_failures output = let val known_atp_failure = extract_known_atp_failure known_failures output val tstplike_proof = extract_tstplike_proof proof_delims output in (case (tstplike_proof, known_atp_failure) of (_, SOME ProofIncomplete) => ("", NONE) | (_, SOME ProofUnparsable) => ("", NONE) | ("", SOME ProofMissing) => ("", NONE) | ("", NONE) => ("", SOME (UnknownError (short_output verbose output))) | res as ("", _) => res | (tstplike_proof, _) => (tstplike_proof, NONE)) end type atp_step_name = string * string list fun is_same_atp_step (s1, _) (s2, _) = s1 = s2 val vampire_fact_prefix = "f" fun vampire_step_name_ord p = let val q = apply2 fst p in (* The "unprefix" part is to cope with Vampire's output. *) (case apply2 (Int.fromString o perhaps (try (unprefix vampire_fact_prefix))) q of (SOME i, SOME j) => int_ord (i, j) | _ => raise Fail "not Vampire") end type ('a, 'b) atp_step = atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list (**** PARSING OF TSTP FORMAT ****) (* Strings enclosed in single quotes (e.g., file names), identifiers possibly starting - with "$" and possibly with "!" in them (for "z3_tptp"). *) + with "$" and possibly with "!" in them. *) val scan_general_id = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode || (Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode)) -- Scan.optional (Scan.repeat ($$ "!") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode)) "" >> op ^ fun skip_term x = let fun skip _ accum [] = (accum, []) | skip n accum (ss as s :: ss') = if (s = "," orelse s = ".") andalso n = 0 then (accum, ss) else if member (op =) [")", "]"] s then if n = 0 then (accum, ss) else skip (n - 1) (s :: accum) ss' else if member (op =) ["(", "["] s then skip (n + 1) (s :: accum) ss' else skip n (s :: accum) ss' in (skip 0 [] #>> (rev #> implode)) x end and skip_terms x = (skip_term ::: Scan.repeat ($$ "," |-- skip_term)) x datatype source = File_Source of string * string option | Inference_Source of string * string list | Introduced_Source of string val dummy_phi = AAtom (ATerm (("", []), [])) val dummy_atype = AType (("", []), []) (* "skip_term" is there to cope with Waldmeister nonsense such as "theory(equality)". *) fun parse_dependency x = (parse_inference_source >> snd || scan_general_id --| skip_term >> single) x and parse_dependencies x = (Scan.repeats (Scan.option ($$ ",") |-- parse_dependency) >> (filter_out (curry (op =) "theory"))) x and parse_file_source x = (Scan.this_string "file" |-- $$ "(" |-- scan_general_id -- Scan.option ($$ "," |-- scan_general_id --| Scan.option ($$ "," |-- $$ "[" -- Scan.option scan_general_id --| $$ "]")) --| $$ ")") x and parse_inference_source x = (Scan.this_string "inference" |-- $$ "(" |-- scan_general_id --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]" --| $$ ")") x and parse_introduced_source x = (Scan.this_string "introduced" |-- $$ "(" |-- scan_general_id --| Scan.option ($$ "," |-- skip_term) --| $$ ")") x and parse_source x = (parse_file_source >> File_Source >> SOME || parse_inference_source >> Inference_Source >> SOME || parse_introduced_source >> Introduced_Source >> SOME || scan_general_id >> (fn s => SOME (Inference_Source ("", [s]))) (* for E *) || skip_term >> K NONE) x fun list_app (f, args) = fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f fun parse_class x = scan_general_id x and parse_classes x = (parse_class ::: Scan.repeat ($$ "&" |-- parse_class)) x fun parse_type x = (($$ "(" |-- parse_type --| $$ ")" || Scan.this_string tptp_pi_binder |-- $$ "[" |-- skip_terms --| $$ "]" --| $$ ":" -- parse_type >> (fn (_, ty) => ty (* currently ignoring type constructor declarations anyway *)) || (scan_general_id -- Scan.optional ($$ "{" |-- parse_classes --| $$ "}") []) -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") [] >> AType) -- Scan.option (($$ tptp_app || $$ tptp_fun_type || $$ tptp_product_type) -- parse_type) >> (fn (a, NONE) => a | (a, SOME (bin_op, b)) => if bin_op = tptp_app then (case a of AType (s_clss, tys) => AType (s_clss, tys @ [b]) | _ => raise UNRECOGNIZED_ATP_PROOF ()) else if bin_op = tptp_fun_type then AFun (a, b) else if bin_op = tptp_product_type then AType ((tptp_product_type, []), [a, b]) else raise Fail "impossible case")) x and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x (* We currently half ignore types. *) fun parse_fol_optional_type_signature x = (Scan.option ($$ tptp_has_type |-- parse_type) >> (fn some as SOME (AType ((s, []), [])) => if s = dfg_individual_type then NONE else some | res => res)) x and parse_fol_arg x = ($$ "(" |-- parse_fol_term --| $$ ")" --| parse_fol_optional_type_signature || scan_general_id -- parse_fol_optional_type_signature -- Scan.optional ($$ "<" |-- parse_types --| $$ ">") [] -- Scan.optional ($$ "(" |-- parse_fol_terms --| $$ ")") [] >> (fn (((s, ty_opt), tyargs), args) => if is_tptp_variable s andalso null tyargs andalso null args andalso is_some ty_opt then ATerm ((s, the_list ty_opt), []) else ATerm ((s, tyargs), args))) x and parse_fol_term x = (parse_fol_arg -- Scan.repeat ($$ tptp_app |-- parse_fol_arg) --| parse_fol_optional_type_signature >> list_app) x and parse_fol_terms x = (parse_fol_term ::: Scan.repeat ($$ "," |-- parse_fol_term)) x fun parse_fol_atom x = (parse_fol_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal -- parse_fol_term) >> (fn (u1, NONE) => AAtom u1 | (u1, SOME (neg, u2)) => AAtom (ATerm (("equal", []), [u1, u2])) |> is_some neg ? mk_anot)) x (* TPTP formulas are fully parenthesized, so we don't need to worry about operator precedence. *) fun parse_fol_literal x = ((Scan.repeat ($$ tptp_not) >> length) -- ($$ "(" |-- parse_fol_formula --| $$ ")" || parse_fol_quantified_formula || parse_fol_atom) >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_anot)) x and parse_fol_formula x = (parse_fol_literal -- Scan.option ((Scan.this_string tptp_implies || Scan.this_string tptp_iff || Scan.this_string tptp_not_iff || Scan.this_string tptp_if || $$ tptp_or || $$ tptp_and) -- parse_fol_formula) >> (fn (phi1, NONE) => phi1 | (phi1, SOME (c, phi2)) => if c = tptp_implies then mk_aconn AImplies phi1 phi2 else if c = tptp_iff then mk_aconn AIff phi1 phi2 else if c = tptp_not_iff then mk_anot (mk_aconn AIff phi1 phi2) else if c = tptp_if then mk_aconn AImplies phi2 phi1 else if c = tptp_or then mk_aconn AOr phi1 phi2 else if c = tptp_and then mk_aconn AAnd phi1 phi2 else raise Fail ("impossible connective " ^ quote c))) x and parse_fol_quantified_formula x = (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists) --| $$ "[" -- parse_fol_terms --| $$ "]" --| $$ ":" -- parse_fol_literal >> (fn ((q, ts), phi) => AQuant (q, map (fn ATerm ((s, _), _) => (s, NONE)) ts, phi))) x val parse_tstp_extra_arguments = Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term)) NONE val waldmeister_conjecture_name = "conjecture_1" fun is_same_term subst tm1 tm2 = let fun do_term_pair (AAbs (((var1, typ1), body1), args1)) (AAbs (((var2, typ2), body2), args2)) (SOME subst) = if typ1 <> typ2 andalso length args1 = length args2 then NONE else let val ls = length subst in SOME ((var1, var2) :: subst) |> do_term_pair body1 body2 |> (fn SOME subst => SOME (nth_drop (length subst - ls - 1) subst) | NONE => NONE) |> (if length args1 = length args2 then fold2 do_term_pair args1 args2 else K NONE) end | do_term_pair (ATerm ((s1, _), args1)) (ATerm ((s2, _), args2)) (SOME subst) = (case apply2 is_tptp_variable (s1, s2) of (true, true) => (case AList.lookup (op =) subst s1 of SOME s2' => if s2' = s2 then SOME subst else NONE | NONE => if null (AList.find (op =) subst s2) then SOME ((s1, s2) :: subst) else NONE) | (false, false) => if s1 = s2 then SOME subst else NONE | _ => NONE) |> (if length args1 = length args2 then fold2 do_term_pair args1 args2 else K NONE) | do_term_pair _ _ _ = NONE in SOME subst |> do_term_pair tm1 tm2 |> is_some end fun is_same_formula comm subst (AQuant (q1, xs1, phi1)) (AQuant (q2, xs2, phi2)) = q1 = q2 andalso length xs1 = length xs2 andalso is_same_formula comm ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2 | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) = c1 = c2 andalso length phis1 = length phis2 andalso forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2) | is_same_formula comm subst (AAtom (tm1 as ATerm (("equal", tys), [tm11, tm12]))) (AAtom tm2) = is_same_term subst tm1 tm2 orelse (comm andalso is_same_term subst (ATerm (("equal", tys), [tm12, tm11])) tm2) | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2 | is_same_formula _ _ _ _ = false fun matching_formula_line_identifier phi (Formula ((ident, _), _, phi', _, _)) = if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE | matching_formula_line_identifier _ _ = NONE fun find_formula_in_problem phi = maps snd #> map_filter (matching_formula_line_identifier phi) #> try (single o hd) #> the_default [] fun commute_eq (AAtom (ATerm ((s, tys), tms))) = AAtom (ATerm ((s, tys), rev tms)) | commute_eq _ = raise Fail "expected equation" fun role_of_tptp_string "axiom" = Axiom | role_of_tptp_string "definition" = Definition | role_of_tptp_string "lemma" = Lemma | role_of_tptp_string "hypothesis" = Hypothesis | role_of_tptp_string "conjecture" = Conjecture | role_of_tptp_string "negated_conjecture" = Negated_Conjecture | role_of_tptp_string "plain" = Plain | role_of_tptp_string "type" = Type_Role | role_of_tptp_string _ = Unknown val tptp_binary_ops = [tptp_and, tptp_or, tptp_implies, tptp_iff, tptp_if, tptp_equal, tptp_not_equal, tptp_not_and, tptp_not_or, tptp_not_iff, tptp_app] fun parse_one_in_list xs = foldl1 (op ||) (map Scan.this_string xs) fun parse_binary_op x = (parse_one_in_list tptp_binary_ops >> (fn c => if c = tptp_equal then "equal" else c)) x val parse_fol_quantifier = parse_one_in_list [tptp_forall, tptp_exists, tptp_lambda, tptp_hilbert_choice, tptp_hilbert_the] val parse_hol_quantifier = parse_one_in_list [tptp_ho_forall, tptp_ho_exists, tptp_hilbert_choice, tptp_hilbert_the] fun mk_ho_of_fo_quant q = if q = tptp_forall then tptp_ho_forall else if q = tptp_exists then tptp_ho_exists else if q = tptp_hilbert_choice then tptp_hilbert_choice else if q = tptp_hilbert_the then tptp_hilbert_the else raise Fail ("unrecognized quantification: " ^ q) fun remove_hol_app (ATerm ((s, ty), args)) = if s = tptp_app then (case args of ATerm (f, xs) :: ys => remove_hol_app (ATerm (f, xs @ ys)) | AAbs ((var, phi), xs) :: ys => remove_hol_app (AAbs ((var, phi), xs @ ys))) else ATerm ((s, ty), map remove_hol_app args) | remove_hol_app (AAbs ((var, phi), args)) = AAbs ((var, remove_hol_app phi), map remove_hol_app args) fun parse_hol_typed_var x = (Scan.repeat (scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type) --| Scan.option (Scan.this_string ",")) || $$ "(" |-- parse_hol_typed_var --| $$ ")") x fun parse_simple_hol_term x = (parse_fol_quantifier -- ($$ "[" |-- parse_hol_typed_var --| $$ "]" --| $$ ":") -- parse_hol_term >> (fn ((q, ys), t) => fold_rev (fn (var, ty) => fn r => AAbs (((var, the_default dummy_atype ty), r), []) |> (if tptp_lambda <> q then mk_app (q |> mk_ho_of_fo_quant |> mk_simple_aterm) else I)) ys t) || Scan.this_string tptp_not |-- parse_hol_term >> mk_app (mk_simple_aterm tptp_not) || scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type) >> (fn (var, typ_opt) => ATerm ((var, the_list typ_opt), [])) || parse_hol_quantifier >> mk_simple_aterm || $$ "(" |-- parse_hol_term --| $$ ")" || parse_binary_op >> mk_simple_aterm) x and parse_hol_term x = (parse_simple_hol_term -- Scan.repeat (parse_binary_op -- parse_simple_hol_term) >> (fn (t1, c_ti_s) => fold (fn (c, ti) => fn left => if c = tptp_app then mk_app left ti else mk_apps (mk_simple_aterm c) [left, ti]) c_ti_s t1)) x fun parse_hol_formula x = (parse_hol_term #>> remove_hol_app #>> AAtom) x fun parse_tstp_hol_line problem = (Scan.this_string tptp_thf -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ "," -- (parse_hol_formula || skip_term >> K dummy_phi) -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." >> (fn (((num, role), phi), src) => let val role' = role_of_tptp_string role val ((name, phi), rule, deps) = (case src of SOME (File_Source (_, SOME s)) => if role' = Definition then (((num, map fst (find_formula_in_problem phi problem)), phi), "", []) else (((num, [s]), phi), "", []) | SOME (Inference_Source (rule, deps)) => (((num, []), phi), rule, deps) | SOME (Introduced_Source rule) => (((num, []), phi), rule, []) | _ => (((num, [num]), phi), "", [])) in [(name, role', phi, rule, map (rpair []) deps)] end) fun parse_tstp_fol_line problem = ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tff) -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ "," -- (parse_fol_formula || skip_term >> K dummy_phi) -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." >> (fn (((num, role0), phi), src) => let val role = role_of_tptp_string role0 val ((name, phi), role', rule, deps) = (* Waldmeister isn't exactly helping. *) (case src of SOME (File_Source (_, SOME s)) => (if s = waldmeister_conjecture_name then (case find_formula_in_problem (mk_anot phi) problem of (* Waldmeister hack: Get the original orientation of the equation to avoid confusing Isar. *) [(s, phi')] => ((num, [s]), phi |> not (is_same_formula false [] (mk_anot phi) phi') ? commute_eq) | _ => ((num, []), phi)) else ((num, [s]), phi), role, "", []) | SOME (File_Source _) => (((num, map fst (find_formula_in_problem phi problem)), phi), role, "", []) | SOME (Inference_Source (rule, deps)) => (((num, []), phi), role, rule, deps) | SOME (Introduced_Source rule) => (((num, []), phi), Lemma, rule, []) | _ => (((num, [num]), phi), role, "", [])) fun mk_step () = (name, role', phi, rule, map (rpair []) deps) in [(case role' of Definition => (case phi of AAtom (ATerm (("equal", _), _)) => (* Vampire's equality proxy axiom *) (name, Definition, phi, rule, map (rpair []) deps) | _ => mk_step ()) | _ => mk_step ())] end) fun parse_tstp_line problem = parse_tstp_fol_line problem || parse_tstp_hol_line problem (**** PARSING OF SPASS OUTPUT ****) (* SPASS returns clause references of the form "x.y". We ignore "y". *) val parse_dot_name = scan_general_id --| $$ "." --| scan_general_id val parse_spass_annotations = Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name --| Scan.option ($$ ","))) [] (* We ignore the stars and the pluses that follow literals. *) fun parse_decorated_atom x = (parse_fol_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x fun mk_horn ([], []) = AAtom (ATerm (("c_False", []), [])) | mk_horn (neg_lits, pos_lits) = foldr1 (uncurry (mk_aconn AOr)) (map mk_anot neg_lits @ pos_lits) fun parse_horn_clause x = (Scan.repeat parse_decorated_atom --| $$ "|" --| $$ "|" -- Scan.repeat parse_decorated_atom --| $$ "-" --| $$ ">" -- Scan.repeat parse_decorated_atom >> (mk_horn o apfst (op @))) x val parse_spass_debug = Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) --| $$ ")") (* Syntax: [0:] || -> . derived from formulae * *) fun parse_spass_line x = (parse_spass_debug |-- scan_general_id --| $$ "[" --| Scan.many1 Symbol.is_digit --| $$ ":" -- Symbol.scan_ascii_id -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "." -- Scan.option (Scan.this_string "derived from formulae " |-- Scan.repeat (scan_general_id --| Scan.option ($$ " "))) >> (fn ((((num, rule), deps), u), names) => [((num, these names), Unknown, u, rule, map (rpair []) deps)])) x fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, []) -(* Syntax: SZS core ... *) -fun parse_z3_tptp_core_line x = - (Scan.this_string "SZS core" |-- Scan.repeat ($$ " " |-- scan_general_id) - >> map (core_inference z3_tptp_core_rule)) x - fun parse_line local_name problem = (* Satallax is handled separately, in "atp_satallax.ML". *) if local_name = spassN then parse_spass_line - else if local_name = z3_tptpN then parse_z3_tptp_core_line else parse_tstp_line problem fun core_of_agsyhol_proof s = (case split_lines s of "The transformed problem consists of the following conjectures:" :: conj :: _ :: proof_term :: _ => SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term) | _ => NONE) fun clean_up_dependencies _ [] = [] | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) = (name, role, u, rule, map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) :: clean_up_dependencies (name :: seen) steps fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof fun map_term_names_in_atp_proof f = let fun map_type (AType ((s, clss), tys)) = AType ((f s, map f clss), map map_type tys) | map_type (AFun (ty, ty')) = AFun (map_type ty, map_type ty') | map_type (APi (ss, ty)) = APi (map f ss, map_type ty) fun map_term (ATerm ((s, tys), ts)) = ATerm ((f s, map map_type tys), map map_term ts) | map_term (AAbs (((s, ty), tm), args)) = AAbs (((f s, map_type ty), map_term tm), map map_term args) fun map_formula (AQuant (q, xs, phi)) = AQuant (q, map (apfst f) xs, map_formula phi) | map_formula (AConn (c, phis)) = AConn (c, map map_formula phis) | map_formula (AAtom t) = AAtom (map_term t) fun map_step (name, role, phi, rule, deps) = (name, role, map_formula phi, rule, deps) in map map_step end fun nasty_name pool s = Symtab.lookup pool s |> the_default s fun nasty_atp_proof pool = not (Symtab.is_empty pool) ? map_term_names_in_atp_proof (nasty_name pool) fun string_of_list f xs = enclose "[" "]" (commas (map f xs)) fun string_of_atp_step_name (s, ss) = "(" ^ s ^ ", " ^ string_of_list I ss ^ ")" fun string_of_atp_step f g (name, role, x, y, names) = let val name' = string_of_atp_step_name name val role' = ATP_Problem.tptp_string_of_role role val x' = f x val y' = g y val names' = string_of_list string_of_atp_step_name names in "(" ^ name' ^ ", " ^ role' ^ ", " ^ x' ^ ", " ^ y' ^ ", " ^ names' ^ ")" end fun parse_proof local_name problem = strip_spaces_except_between_idents #> raw_explode #> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) (Scan.finite Symbol.stopper (Scan.repeats1 (parse_line local_name problem)))) #> fst fun atp_proof_of_tstplike_proof _ _ "" = [] | atp_proof_of_tstplike_proof local_prover problem tstp = (case core_of_agsyhol_proof tstp of SOME facts => facts |> map (core_inference agsyhol_core_rule) | NONE => tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |> parse_proof local_prover problem |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o apply2 #1)))) end; diff --git a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML @@ -1,482 +1,481 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Author: Jasmin Blanchette, TU Munich Author: Sascha Boehme, TU Munich Author: Tobias Nipkow, TU Munich Author: Makarius Author: Martin Desharnais, UniBw Munich, MPI-INF Saarbruecken Mirabelle action: "sledgehammer". *) structure Mirabelle_Sledgehammer: MIRABELLE_ACTION = struct (*To facilitate synching the description of Mirabelle Sledgehammer parameters (in ../lib/Tools/mirabelle) with the parameters actually used by this interface, the former extracts PARAMETER and DESCRIPTION from code below which has this pattern (provided it appears in a single line): val .*K = "PARAMETER" (*DESCRIPTION*) *) (* NOTE: Do not forget to update the Sledgehammer documentation to reflect changes here. *) val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) val keep_probsK = "keep_probs" (*=BOOL: keep temporary problem files created by sledgehammer*) val keep_proofsK = "keep_proofs" (*=BOOL: keep temporary proof files created by ATPs*) val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (e.g. using metis)*) val term_orderK = "term_order" (*=STRING: term order (in E)*) (*defaults used in this Mirabelle action*) val check_trivial_default = false val keep_probs_default = false val keep_proofs_default = false datatype sh_data = ShData of { calls: int, success: int, nontriv_calls: int, nontriv_success: int, lemmas: int, max_lems: int, time_isa: int, time_prover: int} datatype re_data = ReData of { calls: int, success: int, nontriv_calls: int, nontriv_success: int, proofs: int, time: int, timeout: int, lemmas: int * int * int, posns: (Position.T * bool) list } fun make_sh_data (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, time_prover) = ShData{calls=calls, success=success, nontriv_calls=nontriv_calls, nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, time_isa=time_isa, time_prover=time_prover} fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time, timeout,lemmas,posns) = ReData{calls=calls, success=success, nontriv_calls=nontriv_calls, nontriv_success=nontriv_success, proofs=proofs, time=time, timeout=timeout, lemmas=lemmas, posns=posns} val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0) val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), []) fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover}) = (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns) datatype data = Data of { sh: sh_data, re_u: re_data (* proof method with unminimized set of lemmas *) } type change_data = (data -> data) -> unit fun make_data (sh, re_u) = Data {sh=sh, re_u=re_u} val empty_data = make_data (empty_sh_data, empty_re_data) fun map_sh_data f (Data {sh, re_u}) = let val sh' = make_sh_data (f (tuple_of_sh_data sh)) in make_data (sh', re_u) end fun map_re_data f (Data {sh, re_u}) = let val f' = make_re_data o f o tuple_of_re_data val re_u' = f' re_u in make_data (sh, re_u') end fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); val inc_sh_calls = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover)) val inc_sh_success = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover)) val inc_sh_nontriv_calls = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover)) val inc_sh_nontriv_success = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover)) fun inc_sh_lemmas n = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => (calls, success, nontriv_calls, nontriv_success, lemmas+n, max_lems, time_isa, time_prover)) fun inc_sh_max_lems n = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => (calls, success,nontriv_calls, nontriv_success, lemmas, Int.max (max_lems, n), time_isa, time_prover)) fun inc_sh_time_isa t = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa + t, time_prover)) fun inc_sh_time_prover t = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover + t)) val inc_proof_method_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) val inc_proof_method_success = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) val inc_proof_method_nontriv_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns)) val inc_proof_method_nontriv_success = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns)) val inc_proof_method_proofs = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns)) fun inc_proof_method_time t = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) val inc_proof_method_timeout = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns)) fun inc_proof_method_lemmas n = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) fun inc_proof_method_posns pos = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) val str0 = string_of_int o the_default 0 local val str = string_of_int val str3 = Real.fmt (StringCvt.FIX (SOME 3)) fun percentage a b = string_of_int (a * 100 div b) fun ms t = Real.fromInt t / 1000.0 fun avg_time t n = if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 fun log_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover}) = "\nTotal number of sledgehammer calls: " ^ str calls ^ "\nNumber of successful sledgehammer calls: " ^ str success ^ "\nNumber of sledgehammer lemmas: " ^ str lemmas ^ "\nMax number of sledgehammer lemmas: " ^ str max_lems ^ "\nSuccess rate: " ^ percentage success calls ^ "%" ^ "\nTotal number of nontrivial sledgehammer calls: " ^ str nontriv_calls ^ "\nNumber of successful nontrivial sledgehammer calls: " ^ str nontriv_success ^ "\nTotal time for sledgehammer calls (Isabelle): " ^ str3 (ms time_isa) ^ "\nTotal time for successful sledgehammer calls (ATP): " ^ str3 (ms time_prover) ^ "\nAverage time for sledgehammer calls (Isabelle): " ^ str3 (avg_time time_isa calls) ^ "\nAverage time for successful sledgehammer calls (ATP): " ^ str3 (avg_time time_prover success) fun log_re_data sh_calls (ReData {calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas = (lemmas, lems_sos, lems_max), posns}) = let val proved = posns |> map (fn (pos, triv) => str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^ (if triv then "[T]" else "")) in "\nTotal number of proof method calls: " ^ str calls ^ "\nNumber of successful proof method calls: " ^ str success ^ " (proof: " ^ str proofs ^ ")" ^ "\nNumber of proof method timeouts: " ^ str timeout ^ "\nSuccess rate: " ^ percentage success sh_calls ^ "%" ^ "\nTotal number of nontrivial proof method calls: " ^ str nontriv_calls ^ "\nNumber of successful nontrivial proof method calls: " ^ str nontriv_success ^ " (proof: " ^ str proofs ^ ")" ^ "\nNumber of successful proof method lemmas: " ^ str lemmas ^ "\nSOS of successful proof method lemmas: " ^ str lems_sos ^ "\nMax number of successful proof method lemmas: " ^ str lems_max ^ "\nTotal time for successful proof method calls: " ^ str3 (ms time) ^ "\nAverage time for successful proof method calls: " ^ str3 (avg_time time success) ^ "\nProved: " ^ space_implode " " proved end in fun log_data (Data {sh, re_u}) = let val ShData {calls=sh_calls, ...} = sh val ReData {calls=re_calls, ...} = re_u in if sh_calls > 0 then let val text1 = log_sh_data sh in if re_calls > 0 then text1 ^ "\n" ^ log_re_data sh_calls re_u else text1 end else "" end end type stature = ATP_Problem_Generate.stature fun is_good_line s = (String.isSubstring " ms)" s orelse String.isSubstring " s)" s) andalso not (String.isSubstring "(> " s) andalso not (String.isSubstring ", > " s) andalso not (String.isSubstring "may fail" s) (* Fragile hack *) fun proof_method_from_msg args msg = (case AList.lookup (op =) args proof_methodK of SOME name => if name = "smart" then if exists is_good_line (split_lines msg) then "none" else "fail" else name | NONE => if exists is_good_line (split_lines msg) then "none" (* trust the preplayed proof *) else if String.isSubstring "metis (" msg then msg |> Substring.full |> Substring.position "metis (" |> snd |> Substring.position ")" |> fst |> Substring.string |> suffix ")" else if String.isSubstring "metis" msg then "metis" else "smt") local fun run_sh params term_order keep pos state = let fun set_file_name (SOME (dir, keep_probs, keep_proofs)) = let val filename = "prob_" ^ StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^ StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos)) in Config.put Sledgehammer_Prover_ATP.atp_problem_prefix (filename ^ "__") #> (keep_probs ? Config.put Sledgehammer_Prover_ATP.atp_problem_dest_dir dir) #> (keep_proofs ? Config.put Sledgehammer_Prover_ATP.atp_proof_dest_dir dir) #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ()) end | set_file_name NONE = I val state' = state |> Proof.map_context (set_file_name keep #> (Option.map (Config.put Sledgehammer_ATP_Systems.term_order) term_order |> the_default I)) val ((_, (sledgehammer_outcome, msg)), cpu_time) = Mirabelle.cpu_time (fn () => Sledgehammer.run_sledgehammer params Sledgehammer_Prover.Normal NONE 1 Sledgehammer_Fact.no_fact_override state') () in (sledgehammer_outcome, msg, cpu_time) end handle ERROR msg => (Sledgehammer.SH_Unknown, " error: " ^ msg, 0) | _ => (Sledgehammer.SH_Unknown, " error: unexpected error", 0) in fun run_sledgehammer (params as {provers, ...}) output_dir term_order keep_probs keep_proofs proof_method_from_msg thy_index trivial pos st = let val thy = Proof.theory_of st val thy_name = Context.theory_name thy val triv_str = if trivial then "[T] " else "" val keep = if keep_probs orelse keep_proofs then let val subdir = StringCvt.padLeft #"0" 4 (string_of_int thy_index) ^ "_" ^ thy_name in Path.append output_dir (Path.basic subdir) |> Isabelle_System.make_directory |> Path.implode |> (fn dir => SOME (dir, keep_probs, keep_proofs)) end else NONE val prover_name = hd provers val (sledgehamer_outcome, msg, cpu_time) = run_sh params term_order keep pos st val (time_prover, change_data, proof_method_and_used_thms) = (case sledgehamer_outcome of Sledgehammer.SH_Some {used_facts, run_time, ...} => let val num_used_facts = length used_facts val time_prover = Time.toMilliseconds run_time fun get_thms (name, stature) = try (Sledgehammer_Util.thms_of_name (Proof.context_of st)) name |> Option.map (pair (name, stature)) val change_data = inc_sh_success #> not trivial ? inc_sh_nontriv_success #> inc_sh_lemmas num_used_facts #> inc_sh_max_lems num_used_facts #> inc_sh_time_prover time_prover in (SOME time_prover, change_data, SOME (proof_method_from_msg msg, map_filter get_thms used_facts)) end | _ => (NONE, I, NONE)) val outcome_msg = "(SH " ^ string_of_int cpu_time ^ "ms" ^ (case time_prover of NONE => "" | SOME ms => ", ATP " ^ string_of_int ms ^ "ms") ^ ") [" ^ prover_name ^ "]: " in (sledgehamer_outcome, triv_str ^ outcome_msg ^ msg, change_data #> inc_sh_time_isa cpu_time, proof_method_and_used_thms) end end fun override_params prover type_enc timeout = [("provers", prover), ("max_facts", "0"), ("type_enc", type_enc), ("strict", "true"), ("slice", "false"), ("timeout", timeout |> Time.toSeconds |> string_of_int)] fun run_proof_method trivial full name meth named_thms timeout pos st = let fun do_method named_thms ctxt = let val ref_of_str = (* FIXME proper wrapper for parser combinators *) suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none #> Parse.thm #> fst val thms = named_thms |> maps snd val facts = named_thms |> map (ref_of_str o fst o fst) val fact_override = {add = facts, del = [], only = true} fun my_timeout time_slice = timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal fun sledge_tac time_slice prover type_enc = Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt (override_params prover type_enc (my_timeout time_slice)) fact_override [] in if meth = "sledgehammer_tac" then - sledge_tac 0.2 ATP_Proof.vampireN "mono_native" - ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??" - ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native" - ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??" + sledge_tac 0.25 ATP_Proof.vampireN "mono_native" + ORELSE' sledge_tac 0.25 ATP_Proof.eN "poly_guards??" + ORELSE' sledge_tac 0.25 ATP_Proof.spassN "mono_native" ORELSE' SMT_Solver.smt_tac ctxt thms else if meth = "smt" then SMT_Solver.smt_tac ctxt thms else if full then Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms else if String.isPrefix "metis (" meth then let val (type_encs, lam_trans) = meth |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start |> filter Token.is_proper |> tl |> Metis_Tactic.parse_metis_options |> fst |>> the_default [ATP_Proof_Reconstruct.partial_typesN] ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end else if meth = "metis" then Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms else if meth = "none" then K all_tac else if meth = "fail" then K no_tac else (warning ("Unknown method " ^ quote meth); K no_tac) end fun apply_method named_thms = Mirabelle.can_apply timeout (do_method named_thms) st fun with_time (false, t) = ("failed (" ^ string_of_int t ^ ")", I) | with_time (true, t) = ("succeeded (" ^ string_of_int t ^ ")", inc_proof_method_success #> not trivial ? inc_proof_method_nontriv_success #> inc_proof_method_lemmas (length named_thms) #> inc_proof_method_time t #> inc_proof_method_posns (pos, trivial) #> name = "proof" ? inc_proof_method_proofs) fun timed_method named_thms = with_time (Mirabelle.cpu_time apply_method named_thms) handle Timeout.TIMEOUT _ => ("timeout", inc_proof_method_timeout) | ERROR msg => ("error: " ^ msg, I) in timed_method named_thms |> apsnd (fn change_data => change_data #> inc_proof_method_calls #> not trivial ? inc_proof_method_nontriv_calls) end val try0 = Try0.try0 (SOME (Time.fromSeconds 5)) ([], [], [], []) fun make_action ({arguments, timeout, output_dir, ...} : Mirabelle.action_context) = let (* Parse Mirabelle-specific parameters *) val check_trivial = Mirabelle.get_bool_argument arguments (check_trivialK, check_trivial_default) val keep_probs = Mirabelle.get_bool_argument arguments (keep_probsK, keep_probs_default) val keep_proofs = Mirabelle.get_bool_argument arguments (keep_proofsK, keep_proofs_default) val term_order = AList.lookup (op =) arguments term_orderK val proof_method_from_msg = proof_method_from_msg arguments val params = Sledgehammer_Commands.default_params \<^theory> arguments val data = Synchronized.var "Mirabelle_Sledgehammer.data" empty_data val init_msg = "Params for sledgehammer: " ^ Sledgehammer_Prover.string_of_params params fun run ({theory_index, name, pos, pre, ...} : Mirabelle.command) = let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then "" else let val trivial = check_trivial andalso try0 pre handle Timeout.TIMEOUT _ => false val (outcome, log1, change_data1, proof_method_and_used_thms) = run_sledgehammer params output_dir term_order keep_probs keep_proofs proof_method_from_msg theory_index trivial pos pre val (log2, change_data2) = (case proof_method_and_used_thms of SOME (proof_method, used_thms) => run_proof_method trivial false name proof_method used_thms timeout pos pre |> apfst (prefix (proof_method ^ " (sledgehammer): ")) | NONE => ("", I)) val () = Synchronized.change data (change_data1 #> change_data2 #> inc_sh_calls #> not trivial ? inc_sh_nontriv_calls) in log1 ^ "\n" ^ log2 |> Symbol.trim_blanks |> prefix_lines (Sledgehammer.short_string_of_sledgehammer_outcome outcome ^ " ") end end fun finalize () = log_data (Synchronized.value data) in (init_msg, {run = run, finalize = finalize}) end val () = Mirabelle.register_action "sledgehammer" make_action end diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML @@ -1,719 +1,698 @@ (* Title: HOL/Tools/ATP/atp_systems.ML Author: Fabian Immler, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Setup for supported ATPs. *) signature SLEDGEHAMMER_ATP_SYSTEMS = sig type term_order = ATP_Problem.term_order type atp_format = ATP_Problem.atp_format type atp_formula_role = ATP_Problem.atp_formula_role type atp_failure = ATP_Proof.atp_failure type base_slice = int * string type atp_slice = atp_format * string * string * bool * string type atp_config = {exec : string list * string list, arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string list, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, good_slices : Proof.context -> (base_slice * atp_slice) list, good_max_mono_iters : int, good_max_new_mono_instances : int} val default_max_mono_iters : int val default_max_new_mono_instances : int val term_order : string Config.T val e_smartN : string val e_autoN : string val e_fun_weightN : string val e_sym_offset_weightN : string val e_default_fun_weight : real Config.T val e_fun_weight_base : real Config.T val e_fun_weight_span : real Config.T val e_default_sym_offs_weight : real Config.T val e_sym_offs_weight_base : real Config.T val e_sym_offs_weight_span : real Config.T val spass_H1SOS : string val spass_H2 : string val spass_H2LR0LT0 : string val spass_H2NuVS0 : string val spass_H2NuVS0Red2 : string val spass_H2SOS : string val isabelle_scala_function: string list * string list val remote_atp : string -> string -> string list -> (string * string) list -> (atp_failure * string) list -> atp_formula_role -> (Proof.context -> base_slice * atp_slice) -> string * (unit -> atp_config) val add_atp : string * (unit -> atp_config) -> theory -> theory val get_atp : theory -> string -> (unit -> atp_config) val is_atp_installed : theory -> string -> bool val refresh_systems_on_tptp : unit -> unit val effective_term_order : Proof.context -> string -> term_order val local_atps : string list val remote_atps : string list val atps : string list end; structure Sledgehammer_ATP_Systems : SLEDGEHAMMER_ATP_SYSTEMS = struct open ATP_Problem open ATP_Proof open ATP_Problem_Generate (* ATP configuration *) val TF0 = TFF (Monomorphic, Without_FOOL) val TF1 = TFF (Polymorphic, Without_FOOL) val TX0 = TFF (Monomorphic, With_FOOL {with_ite = true, with_let = true}) val TX1 = TFF (Polymorphic, With_FOOL {with_ite = true, with_let = true}) val TH0 = THF (Monomorphic, {with_ite = true, with_let = true}, THF_With_Choice) val TH1 = THF (Polymorphic, {with_ite = true, with_let = true}, THF_With_Choice) val default_max_mono_iters = 3 (* FUDGE *) val default_max_new_mono_instances = 100 (* FUDGE *) type base_slice = int * string type atp_slice = atp_format * string * string * bool * string type atp_config = {exec : string list * string list, arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string list, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, good_slices : Proof.context -> (base_slice * atp_slice) list, good_max_mono_iters : int, good_max_new_mono_instances : int} (* "good_slices" must be found empirically, taking a holistic approach since the ATPs are run in parallel. Each slice has the format (time_frac, ((max_facts, fact_filter), format, type_enc, lam_trans, uncurried_aliases), extra) where time_frac = faction of the time available given to the slice (which should add up to 1.0) extra = extra information to the prover (e.g., SOS or no SOS). The last slice should be the most "normal" one, because it will get all the time available if the other slices fail early and also because it is used if slicing is disabled (e.g., by the minimizer). *) val mepoN = "mepo" val mashN = "mash" val meshN = "mesh" val tstp_proof_delims = [("% SZS output start CNFRefutation", "% SZS output end CNFRefutation"), ("% SZS output start Refutation", "% SZS output end Refutation"), ("% SZS output start Proof", "% SZS output end Proof")] fun known_szs_failures wrap = [(Unprovable, wrap "CounterSatisfiable"), (Unprovable, wrap "Satisfiable"), (GaveUp, wrap "GaveUp"), (GaveUp, wrap "Unknown"), (GaveUp, wrap "Incomplete"), (ProofMissing, wrap "Theorem"), (ProofMissing, wrap "Unsatisfiable"), (TimedOut, wrap "Timeout"), (Inappropriate, wrap "Inappropriate"), (OutOfResources, wrap "ResourceOut"), (OutOfResources, wrap "MemoryOut"), (Interrupted, wrap "Forced"), (Interrupted, wrap "User")] val known_szs_status_failures = known_szs_failures (prefix "SZS status ") val known_says_failures = known_szs_failures (prefix " says ") structure Data = Theory_Data ( type T = ((unit -> atp_config) * stamp) Symtab.table val empty = Symtab.empty fun merge data : T = Symtab.merge (eq_snd (op =)) data handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name) ) fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000) val sosN = "sos" val no_sosN = "no_sos" val smartN = "smart" (* val kboN = "kbo" *) val lpoN = "lpo" val xweightsN = "_weights" val xprecN = "_prec" val xsimpN = "_simp" (* SPASS-specific *) (* Possible values for "atp_term_order": "smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *) val term_order = Attrib.setup_config_string \<^binding>\atp_term_order\ (K smartN) (* agsyHOL *) val agsyhol_config : atp_config = {exec = (["AGSYHOL_HOME"], ["agsyHOL"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => ["--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem], proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, prem_role = Hypothesis, good_slices = (* FUDGE *) K [((60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_max_new_mono_instances = default_max_new_mono_instances} val agsyhol = (agsyholN, fn () => agsyhol_config) (* Alt-Ergo *) val alt_ergo_config : atp_config = {exec = (["WHY3_HOME"], ["why3"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => ["--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem], proof_delims = [], known_failures = [(ProofMissing, ": Valid"), (TimedOut, ": Timeout"), (GaveUp, ": Unknown")], prem_role = Hypothesis, good_slices = (* FUDGE *) K [((100, meshN), (TF1, "poly_native", liftingN, false, ""))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} val alt_ergo = (alt_ergoN, fn () => alt_ergo_config) (* E *) val e_smartN = "smart" val e_autoN = "auto" val e_fun_weightN = "fun_weight" val e_sym_offset_weightN = "sym_offset_weight" (* FUDGE *) val e_default_fun_weight = Attrib.setup_config_real \<^binding>\atp_e_default_fun_weight\ (K 20.0) val e_fun_weight_base = Attrib.setup_config_real \<^binding>\atp_e_fun_weight_base\ (K 0.0) val e_fun_weight_span = Attrib.setup_config_real \<^binding>\atp_e_fun_weight_span\ (K 40.0) val e_default_sym_offs_weight = Attrib.setup_config_real \<^binding>\atp_e_default_sym_offs_weight\ (K 1.0) val e_sym_offs_weight_base = Attrib.setup_config_real \<^binding>\atp_e_sym_offs_weight_base\ (K ~20.0) val e_sym_offs_weight_span = Attrib.setup_config_real \<^binding>\atp_e_sym_offs_weight_span\ (K 60.0) fun e_selection_heuristic_case heuristic fw sow = if heuristic = e_fun_weightN then fw else if heuristic = e_sym_offset_weightN then sow else raise Fail ("unexpected " ^ quote heuristic) fun scaled_e_selection_weight ctxt heuristic w = w * Config.get ctxt (e_selection_heuristic_case heuristic e_fun_weight_span e_sym_offs_weight_span) + Config.get ctxt (e_selection_heuristic_case heuristic e_fun_weight_base e_sym_offs_weight_base) |> Real.ceil |> signed_string_of_int fun e_selection_weight_arguments ctxt heuristic sel_weights = if heuristic = e_fun_weightN orelse heuristic = e_sym_offset_weightN then (* supplied by Stephan Schulz *) "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ \--destructive-er-aggressive --destructive-er --presat-simplify \ \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^ e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^ "(SimulateSOS," ^ (e_selection_heuristic_case heuristic e_default_fun_weight e_default_sym_offs_weight |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^ ",20,1.5,1.5,1" ^ (sel_weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_selection_weight ctxt heuristic w) |> implode) ^ "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\ \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\ \FIFOWeight(PreferProcessed))' " else "-xAuto " val e_ord_weights = map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode "," fun e_ord_precedence [_] = "" | e_ord_precedence info = info |> map fst |> space_implode "<" fun e_term_order_info_arguments false false _ = "" | e_term_order_info_arguments gen_weights gen_prec ord_info = let val ord_info = ord_info () in (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^ (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "") end val e_config : atp_config = {exec = (["E_HOME"], ["eprover-ho", "eprover"]), arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn problem => fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => ["--auto-schedule --tstp-in --tstp-out --silent " ^ e_selection_weight_arguments ctxt heuristic sel_weights ^ e_term_order_info_arguments gen_weights gen_prec ord_info ^ "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^ "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ File.bash_path problem], proof_delims = [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @ tstp_proof_delims, known_failures = [(TimedOut, "Failure: Resource limit exceeded (time)"), (TimedOut, "time limit exceeded")] @ known_szs_status_failures, prem_role = Conjecture, good_slices = let val (format, type_enc, lam_trans) = if string_ord (getenv "E_VERSION", "2.7") <> LESS then (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN) else if string_ord (getenv "E_VERSION", "2.6") <> LESS then (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN) else (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN) in (* FUDGE *) K [((512, meshN), (format, type_enc, lam_trans, false, e_fun_weightN)), ((1024, meshN), (format, type_enc, lam_trans, false, e_sym_offset_weightN)), ((128, mepoN), (format, type_enc, lam_trans, false, e_autoN)), ((724, meshN), (format, "poly_guards??", lam_trans, false, e_sym_offset_weightN)), ((256, mepoN), (format, type_enc, liftingN, false, e_fun_weightN)), ((64, mashN), (format, type_enc, combsN, false, e_fun_weightN))] end, good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} val e = (eN, fn () => e_config) (* iProver *) val iprover_config : atp_config = {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => ["--clausifier \"$VAMPIRE_HOME\"/vampire " ^ "--clausifier_options \"--mode clausify\" " ^ "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem], proof_delims = tstp_proof_delims, known_failures = [(ProofIncomplete, "% SZS output start CNFRefutation")] @ known_szs_status_failures, prem_role = Hypothesis, good_slices = (* FUDGE *) K [((32, meshN), (TF0, "mono_native", liftingN, false, "")), ((512, meshN), (TX0, "mono_native", liftingN, false, "")), ((128, mashN), (TF0, "mono_native", combsN, false, "")), ((1024, meshN), (TF0, "mono_native", liftingN, false, "")), ((256, mepoN), (TF0, "mono_native", combsN, false, ""))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} val iprover = (iproverN, fn () => iprover_config) (* LEO-II *) val leo2_config : atp_config = {exec = (["LEO2_HOME"], ["leo.opt", "leo"]), arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => fn _ => ["--foatp e --atp e=\"$E_HOME\"/eprover \ \--atp epclextract=\"$E_HOME\"/epclextract \ \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ (if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^ File.bash_path problem], proof_delims = tstp_proof_delims, known_failures = [(TimedOut, "CPU time limit exceeded, terminating"), (GaveUp, "No.of.Axioms")] @ known_szs_status_failures, prem_role = Hypothesis, good_slices = (* FUDGE *) K [((40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_max_new_mono_instances = default_max_new_mono_instances} val leo2 = (leo2N, fn () => leo2_config) (* Leo-III *) (* Include choice? Disabled now since it's disabled for Satallax as well. *) val leo3_config : atp_config = {exec = (["LEO3_HOME"], ["leo3"]), arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem => fn _ => [File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC4_SOLVER\" --atp e=\"$E_HOME\"/eprover \ \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ (if full_proofs then "--nleq --naeq " else "")], proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, prem_role = Hypothesis, good_slices = (* FUDGE *) K [((512, meshN), (TH0, "mono_native_higher", keep_lamsN, false, "")), ((512, meshN), (TF0, "mono_native", liftingN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_max_new_mono_instances = default_max_new_mono_instances} val leo3 = (leo3N, fn () => leo3_config) (* Satallax *) (* Choice is disabled until there is proper reconstruction for it. *) val satallax_config : atp_config = {exec = (["SATALLAX_HOME"], ["satallax.opt", "satallax"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => [(case getenv "E_HOME" of "" => "" | home => "-E " ^ home ^ "/eprover ") ^ "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem], proof_delims = [("% SZS output start Proof", "% SZS output end Proof")], known_failures = known_szs_status_failures, prem_role = Hypothesis, good_slices = (* FUDGE *) K [((256, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_max_new_mono_instances = default_max_new_mono_instances} val satallax = (satallaxN, fn () => satallax_config) (* SPASS *) val spass_H1SOS = "-Heuristic=1 -SOS" val spass_H2 = "-Heuristic=2" val spass_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0" val spass_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0" val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2" val spass_H2SOS = "-Heuristic=2 -SOS" val spass_config : atp_config = let val format = DFG Monomorphic in {exec = (["SPASS_HOME"], ["SPASS"]), arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn problem => fn _ => ["-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^ "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem |> extra_options <> "" ? prefix (extra_options ^ " ")], proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = [(GaveUp, "SPASS beiseite: Completion found"), (TimedOut, "SPASS beiseite: Ran out of time"), (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), (MalformedInput, "Undefined symbol"), (MalformedInput, "Free Variable"), (Unprovable, "No formulae and clauses found in input file"), (InternalError, "Please report this error")], prem_role = Conjecture, good_slices = (* FUDGE *) K [((150, meshN), (format, "mono_native", combsN, true, "")), ((500, meshN), (format, "mono_native", liftingN, true, spass_H2SOS)), ((50, meshN), (format, "mono_native", liftingN, true, spass_H2LR0LT0)), ((250, meshN), (format, "mono_native", combsN, true, spass_H2NuVS0)), ((1000, mepoN), (format, "mono_native", liftingN, true, spass_H1SOS)), ((150, meshN), (format, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)), ((300, meshN), (format, "mono_native", combsN, true, spass_H2SOS)), ((100, meshN), (format, "mono_native", combs_and_liftingN, true, spass_H2))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} end val spass = (spassN, fn () => spass_config) (* Vampire *) val vampire_basic_options = "--proof tptp --output_axiom_names on" ^ (if ML_System.platform_is_windows then "" (*time slicing is not support in the Windows version of Vampire*) else " --mode casc") val vampire_full_proof_options = " --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0" val vampire_config : atp_config = {exec = (["VAMPIRE_HOME"], ["vampire"]), arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ => [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^ " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem |> sos = sosN ? prefix "--sos on "], proof_delims = [("=========== Refutation ==========", "======= End of refutation =======")] @ tstp_proof_delims, known_failures = [(GaveUp, "UNPROVABLE"), (GaveUp, "CANNOT PROVE"), (Unprovable, "Satisfiability detected"), (Unprovable, "Termination reason: Satisfiable"), (Interrupted, "Aborted by signal SIGINT")] @ known_szs_status_failures, prem_role = Hypothesis, good_slices = (* FUDGE *) K [((512, meshN), (TX1, "mono_native_fool", combsN, false, sosN)), ((1024, meshN), (TX1, "mono_native_fool", liftingN, false, sosN)), ((256, mashN), (TX1, "mono_native_fool", liftingN, false, no_sosN)), ((512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)), ((16, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN)), ((32, meshN), (TX1, "mono_native_fool", combsN, false, no_sosN)), ((64, meshN), (TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN)), ((128, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} val vampire = (vampireN, fn () => vampire_config) -(* Z3 with TPTP syntax (half experimental, half legacy) *) - -val z3_tptp_config : atp_config = - {exec = (["Z3_TPTP_HOME"], ["z3_tptp"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ => - ["-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ File.bash_path problem], - proof_delims = [("SZS status Theorem", "")], - known_failures = known_szs_status_failures, - prem_role = Hypothesis, - good_slices = - (* FUDGE *) - K [((250, meshN), (TF0, "mono_native", combsN, false, "")), - ((125, mepoN), (TF0, "mono_native", combsN, false, "")), - ((62, mashN), (TF0, "mono_native", combsN, false, "")), - ((31, meshN), (TF0, "mono_native", combsN, false, ""))], - good_max_mono_iters = default_max_mono_iters, - good_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} - -val z3_tptp = (z3_tptpN, fn () => z3_tptp_config) - - (* Zipperposition *) val zipperposition_config : atp_config = let val format = THF (Polymorphic, {with_ite = true, with_let = false}, THF_Without_Choice) in {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]), arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ => ["--input tptp", "--output tptp", "--timeout " ^ Time.toString timeout, extra_options, File.bash_path problem], proof_delims = tstp_proof_delims, known_failures = [(TimedOut, "SZS status ResourceOut")] @ (* odd way of timing out *) known_szs_status_failures, prem_role = Hypothesis, good_slices = K [((1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" -q \"6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|fifo\" -q \"4|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-struct(1,5,2,3)\" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1")), ((128, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=off --ho-prim-enum=full --ho-prim-max=1 --avatar=off --recognize-injectivity=true --ho-elim-leibniz=4 --ho-unif-level=full-framework --no-max-vars -q \"2|prefer-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1)\" -q \"4|const|conjecture-relative-e(0.1,1,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1.5)\" -q \"4|prefer-sos|pnrefined(1,1,1,1,2,1.5,2)\" --select=ho-selection5 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=5 --e-call-point=0.25 --e-auto=true --sine=50 --sine-tolerance=2 --sine-depth-max=4 --sine-depth-min=1 --e-max-derived=96 --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=arity0 --prec-gen-fun=invfreq_conj")), ((512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=2 --ho-unif-max-depth=1 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection16 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true --ho-unif-level=pragmatic-framework --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=lambda-def-invfreqrank --e-call-point=0.1")), ((32, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic -nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=3 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=7 --sine=50 --sine-tolerance=1 --sine-depth-max=2 --sine-depth-min=1 --e-max-derived=64 --sine-ignore-k-most-common-syms=2 --sine-trim-implications=true --e-encode-lambdas=lift --scan-clause-ac=false --lambdasup=0 --kbo-weight-fun=lambda-def-invfreqrank --demod-in-var-args=true --bool-demod=true --lambda-demod=true --e-call-point=0.1")), ((64, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-comb-complete --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-sqarity --ho-prim-enum=none --tptp-def-as-rewrite -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --select=NoSelection --solve-formulas=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=8 --sine=60 --sine-tolerance=2 --sine-depth-max=5 --sine-depth-min=1 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --e-max-derived=50 --e-encode-lambdas=ignore --scan-clause-ac=false --presaturate=true --comb-b-penalty=3 --comb-c-penalty=3 --comb-k-penalty=1 --comb-s-penalty=5 --subvarsup=false --e-call-point=0.15")), ((256, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=0 --ho-prim-enum=none -q \"2|prefer-ho-steps|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|default\" -q \"2|prefer-empty-trail|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" --select=bb+e-selection7 --ho-pattern-decider=false --ho-fixpoint-decider=true --ho-solid-decider=false --sine=150 --sine-tolerance=2 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=2 --fluid-log-hoist=false --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-prim-enum=eq --ho-prim-enum-add-var=true --ho-prim-max=1 --ho-prim-enum-early-bird=true -o tptp --avatar=eager --split-only-ground=true"))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} end val zipperposition = (zipperpositionN, fn () => zipperposition_config) (* Remote ATP invocation via SystemOnTPTP *) val no_remote_systems = {url = "", systems = [] : string list} val remote_systems = Synchronized.var "atp_remote_systems" no_remote_systems fun get_remote_systems () = Timeout.apply (seconds 10.0) SystemOnTPTP.list_systems () handle ERROR msg => (warning msg; no_remote_systems) | Timeout.TIMEOUT _ => no_remote_systems fun find_remote_system name [] systems = find_first (String.isPrefix (name ^ "---")) systems | find_remote_system name (version :: versions) systems = case find_first (String.isPrefix (name ^ "---" ^ version)) systems of NONE => find_remote_system name versions systems | res => res fun get_remote_system name versions = Synchronized.change_result remote_systems (fn remote => (if #url remote <> SystemOnTPTP.get_url () orelse null (#systems remote) then get_remote_systems () else remote) |> ` #systems) |> `(find_remote_system name versions) fun the_remote_system name versions = (case get_remote_system name versions of (SOME sys, _) => sys | (NONE, []) => error "SystemOnTPTP is currently not available" | (NONE, syss) => (case syss |> filter_out (String.isPrefix "%") |> filter_out (curry (op =) "") of [] => error "SystemOnTPTP is currently not available" | [msg] => error ("SystemOnTPTP is currently not available: " ^ msg) | syss => error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^ commas_quote syss ^ ".)"))) val max_remote_secs = 1000 (* give Geoff Sutcliffe's servers a break *) val isabelle_scala_function = (["SCALA_HOME"], ["bin/scala"]) fun remote_config system_name system_versions proof_delims known_failures prem_role good_slice = {exec = isabelle_scala_function, arguments = fn _ => fn _ => fn command => fn timeout => fn problem => fn _ => [the_remote_system system_name system_versions, Isabelle_System.absolute_path problem, command, string_of_int (Int.min (max_remote_secs, to_secs 1 timeout) * 1000)], proof_delims = union (op =) tstp_proof_delims proof_delims, known_failures = known_failures @ known_says_failures, prem_role = prem_role, good_slices = fn ctxt => [good_slice ctxt], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} : atp_config fun remotify_config system_name system_versions good_slice ({proof_delims, known_failures, prem_role, ...} : atp_config) = remote_config system_name system_versions proof_delims known_failures prem_role good_slice fun remote_atp name system_name system_versions proof_delims known_failures prem_role good_slice = (remote_prefix ^ name, fn () => remote_config system_name system_versions proof_delims known_failures prem_role good_slice) fun remotify_atp (name, config) system_name system_versions good_slice = (remote_prefix ^ name, remotify_config system_name system_versions good_slice o config) fun gen_remote_waldmeister name type_enc = remote_atp name "Waldmeister" ["710"] tstp_proof_delims ([(OutOfResources, "Too many function symbols"), (Inappropriate, "**** Unexpected end of file."), (Crashed, "Unrecoverable Segmentation Fault")] @ known_szs_status_failures) Hypothesis (K ((50, meshN), (CNF_UEQ, type_enc, combsN, false, "")) (* FUDGE *)) val remote_agsyhol = remotify_atp agsyhol "agsyHOL" ["1.0", "1"] (K ((60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *)) val remote_alt_ergo = remotify_atp alt_ergo "Alt-Ergo" ["0.95.2"] (K ((250, meshN), (TF1, "poly_native", keep_lamsN, false, "")) (* FUDGE *)) val remote_e = remotify_atp e "E" ["2.0", "1.9.1", "1.8"] (K ((750, meshN), (TF0, "mono_native", combsN, false, "")) (* FUDGE *)) val remote_iprover = remotify_atp iprover "iProver" ["0.99"] (K ((150, meshN), (FOF, "mono_guards??", liftingN, false, "")) (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"] (K ((40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", liftingN, false, "")) (* FUDGE *)) val remote_leo3 = remotify_atp leo3 "Leo-III" ["1.1"] (K ((150, meshN), (THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "poly_native_higher", keep_lamsN, false, "")) (* FUDGE *)) val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" val remote_zipperposition = remotify_atp zipperposition "Zipperpin" ["2.1", "2.0"] (K ((512, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *)) (* Dummy prover *) fun dummy_config prem_role format type_enc uncurried_aliases : atp_config = {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]), arguments = K (K (K (K (K (K []))))), proof_delims = [], known_failures = known_szs_status_failures, prem_role = prem_role, good_slices = K [((200, "mepo"), (format, type_enc, if is_format_higher_order format then keep_lamsN else combsN, uncurried_aliases, ""))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} val dummy_fof = (dummy_fofN, fn () => dummy_config Hypothesis FOF "mono_guards??" false) val dummy_tfx = (dummy_tfxN, fn () => dummy_config Hypothesis TX1 "poly_native_fool" false) val dummy_thf = (dummy_thfN, fn () => dummy_config Hypothesis TH1 "poly_native_higher" false) val dummy_thf_reduced = let val format = THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice) val config = dummy_config Hypothesis format "poly_native_higher" false in (dummy_thfN ^ "_reduced", fn () => config) end (* Setup *) fun add_atp (name, config) thy = Data.map (Symtab.update_new (name, (config, stamp ()))) thy handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name) fun get_atp thy name = fst (the (Symtab.lookup (Data.get thy) name)) handle Option.Option => error ("Unknown ATP: " ^ name) fun is_atp_installed thy name = let val {exec, ...} = get_atp thy name () in exists (fn var => getenv var <> "") (fst exec) end fun refresh_systems_on_tptp () = Synchronized.change remote_systems (fn _ => get_remote_systems ()) fun effective_term_order ctxt atp = let val ord = Config.get ctxt term_order in if ord = smartN then {is_lpo = false, gen_weights = (atp = spassN), gen_prec = (atp = spassN), gen_simp = false} else let val is_lpo = String.isSubstring lpoN ord in {is_lpo = is_lpo, gen_weights = not is_lpo andalso String.isSubstring xweightsN ord, gen_prec = String.isSubstring xprecN ord, gen_simp = String.isSubstring xsimpN ord} end end val local_atps = - [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition] + [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, zipperposition] val remote_atps = [remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3, remote_waldmeister, remote_zipperposition, dummy_fof, dummy_tfx, dummy_thf, dummy_thf_reduced] val atps = local_atps @ remote_atps val _ = Theory.setup (fold add_atp atps) val local_atps = map fst local_atps val remote_atps = map fst remote_atps val atps = map fst atps end;