\index{HolSmtLib|(} \index{SMT solvers|see {HolSmtLib}} \index{decision procedures!SMT} \setcounter{sessioncount}{0} The purpose of \ml{HolSmtLib} is to provide a platform for experimenting with combinations of interactive theorem proving and Satisfiability Modulo Theories~(SMT) solvers. \ml{HolSmtLib} was developed as part of a research project on {\it Expressive Multi-theory Reasoning for Interactive Verification} (EPSRC grant EP/F067909/1) from 2008 to~2011. It is loosely inspired by \ml{HolSatLib} (Section~\ref{sec:HolSatLib}), and has been described in parts in the following publications: \begin{itemize} \item Tjark Weber: {\it SMT Solvers: New Oracles for the HOL Theorem Prover}. To appear in International Journal on Software Tools for Technology Transfer (STTT), 2011. \item Sascha B{\"o}hme, Tjark Weber: {\it Fast LCF-Style Proof Reconstruction for Z3}. In Matt Kaufmann and Lawrence C.\ Paulson, editors, Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11--14, 2010. Proceedings, volume 6172 of Lecture Notes in Computer Science, pages 179--194. Springer, 2010. \end{itemize} \ml{HolSmtLib} uses external SMT solvers to prove instances of SMT tautologies, \ie, formulas that are provable using (a combination of) propositional logic, equality reasoning, linear arithmetic on integers and reals, and decision procedures for bit vectors and arrays. The supported fragment of higher-order logic varies with the SMT solver used, and is discussed in more detail below. At least for Yices, it is a superset of the fragment supported by \ml{bossLib.DECIDE} (and the performance of \ml{HolSmtLib}, especially on big problems, should be much better). \subsection{Interface} The library currently provides three tactics to invoke different SMT solvers, namely \ml{YICES\_TAC}, \ml{Z3\_ORACLE\_TAC}, and \ml{Z3\_TAC}. These tactics are defined in the \ml{HolSmtLib} structure, which is the library's main entry point. Given a goal~$(\Gamma, \varphi)$ (where $\Gamma$ is a list of assumptions, and $\varphi$ is the goal's conclusion), each tactic returns (i)~an empty list of new goals, and (ii)~a validation function that returns a theorem~$\Gamma' \vdash \varphi$ (with $\Gamma' \subseteq \Gamma$). These tactics fail if the SMT solver cannot prove the goal.\footnote{Internally, the goal's assumptions and the \emph{negated} conclusion are passed to the SMT solver. If the SMT solver determines that these formulas are unsatisfiable, then the (unnegated) conclusion must be provable from the assumptions.} In other words, these tactics solve the goal (or fail). As with other tactics, \ml{Tactical.TAC\_PROOF} can be used to derive functions of type \ml{goal -> thm}. For each tactic, the \ml{HolSmtLib} structure additionally provides a corresponding function of type \ml{term -> thm}. These functions are called \ml{YICES\_PROVE}, \ml{Z3\_ORACLE\_PROVE}, and \ml{Z3\_PROVE}, respectively. Applied to a formula $\varphi$, they return the theorem $\emptyset \vdash \varphi$ (or fail). \paragraph{Oracles vs.\ proof reconstruction} \ml{YICES\_TAC} and \ml{Z3\_ORACLE\_TAC} use the SMT solver (Yices and Z3, respectively) as an oracle: the solver's result is trusted. Bugs in the SMT solver or in \ml{HolSmtLib} could potentially lead to inconsistent theorems. Accordingly, the derived theorem is tagged with an oracle tag. \ml{Z3\_TAC}, on the other hand, performs proof reconstruction. It requests a detailed proof from Z3, which is then checked in \HOL{}. One obtains a proper \HOL{} theorem; no (additional) oracle tags are introduced. However, Z3's proofs do not always contain enough information to allow efficient checking in \HOL{}; therefore, proof reconstruction may be slow or fail. \paragraph{Supported subsets of higher-order logic} \ml{YICES\_TAC} employs a translation into Yices's native input format. The interface supports types \holtxt{bool}, \holtxt{num}, \holtxt{int}, \holtxt{real}, \holtxt{->} (\ie, function types), \holtxt{prod} (\ie, tuples), fixed-width word types, inductive data types, records, and the following terms: equality, Boolean connectives (\holtxt{T}, \holtxt{F}, \holtxt{==>}, \holtxt{/\bs}, \holtxt{\bs /}, negation, \holtxt{if-then-else}, \holtxt{bool-case}), quantifiers (\holtxt{!}, \holtxt{?}), numeric literals, arithmetic operators (\holtxt{SUC}, \holtxt{+}, \holtxt{-}, \holtxt{*}, \holtxt{/}, unary minus, \holtxt{DIV}, \holtxt{MOD}, \holtxt{ABS}, \holtxt{MIN}, \holtxt{MAX}), comparison operators (\holtxt{<}, \holtxt{<=}, \holtxt{>}, \holtxt{>=}, both on \holtxt{num}, \holtxt{int}, and \holtxt{real}), function application, lambda abstraction, tuple selectors \holtxt{FST} and \holtxt{SND}, and various word operations. Z3 is integrated via a more restrictive translation into SMT-LIB~2 format, described below. Therefore, Yices is typically the solver of choice at the moment (unless you need proof reconstruction, which is available for Z3 only). However, there are a few operations (\eg, specific word operations) that are supported by the SMT-LIB format, but not by Yices. See \ml{selftest.sml} for further details. Terms of higher-order logic that are not supported by the respective target solver/\allowbreak translation are typically treated in one of three ways: \begin{enumerate} \item Some unsupported terms are replaced by equivalent suppported terms during a pre-processing step. For instance, all tactics first generalize the goal's conclusion by stripping outermost universal quantifiers, and attempt to eliminate certain set expressions by rewriting them into predicate applications: \eg, \holtxt{y IN \{x | P x\}} is replaced by \holtxt{P y}. The resulting term is $\beta$-normalized. Depending on the target solver, further simplifications are performed. \item Remaining unsupported constants are treated as uninterpreted, \ie, replaced by fresh variables. This should not affect soundness, but it may render goals unprovable and lead to spurious counterexamples. To see all fresh variables introduced by the translation, you can set \ml{HolSmtLib}'s tracing variable (see below) to a sufficiently high value. \item Various syntactic side conditions are currently not enforced by the translation and may result in invalid input to the SMT solver. For instance, Yices only allows \emph{linear} arithmetic (\ie, multiplication by constants) and word-shifts by numeric literals (constants). If the goal is outside the allowed syntactic fragment, the SMT solver will typically fail to decide the problem. \ml{HolSmtLib} at present only provides a generic error message in this case. Inspecting the SMT solver's output might provide further hints. \end{enumerate} \begin{session} \begin{verbatim} - load "HolSmtLib"; open HolSmtLib; (* output omitted *) > val it = () : unit - show_tags := true; > val it = () : unit - YICES_PROVE ``(a ==> b) /\ (b ==> a) = (a=b)``; > val it = [oracles: DISK_THM, HolSmtLib] [axioms: ] [] |- (a ==> b) /\ (b ==> a) = (a = b) : thm - Z3_ORACLE_PROVE ``(a ==> b) /\ (b ==> a) = (a=b)``; > val it = [oracles: DISK_THM, HolSmtLib] [axioms: ] [] |- (a ==> b) /\ (b ==> a) = (a = b) : thm - Z3_PROVE ``(a ==> b) /\ (b ==> a) = (a=b)``; > val it = [oracles: DISK_THM] [axioms: ] [] |- (a ==> b) /\ (b ==> a) = (a = b) : thm \end{verbatim} \end{session} \paragraph{Support for the SMT-LIB 2 file format} SMT-LIB (see \url{http://combination.cs.uiowa.edu/smtlib/}) is the standard input format for SMT solvers. \ml{HolSmtLib} supports (a subset of) version~2.0 of this format. A translation of \HOL{} terms into SMT-LIB~2 format is available in \ml{SmtLib.sml}, and a parser for SMT-LIB~2 files (translating them into \HOL{} types, terms, and formulas) can be found in \ml{SmtLib\_Parser.sml}, with auxiliary functions in \ml{SmtLib\_\{Logics,Theories\}.sml}. The SMT-LIB~2 translation supports types \holtxt{bool}, \holtxt{int} and \holtxt{real}, fixed-width word types, and the following terms: equality, Boolean connectives, quantifiers, numeric literals, arithmetic operators, comparison operators, function application, and various word operations. Notably, the SMT-LIB interface does \emph{not} support type \holtxt{num}, data types or records, and higher-order formulas. See the files mentioned above and the examples in \ml{selftest.sml} for further details. \paragraph{Tracing} Tracing output can be controlled via \ml{Feedback.set\_trace "HolSmtLib"}. See the source code in \ml{Library.sml} for possible values. Communication between \HOL{} and external SMT solvers is via temporary files. These files are located in the standard temporary directory, typically {\tt /tmp} on Unix machines. The actual file names are generated at run-time, and can be shown by setting the above tracing variable to a sufficiently high value. The default behavior of \ml{HolSmtLib} is to delete temporary files after successful invocation of the SMT solver. This also can be changed via the above tracing variable. If there is an error, files are retained in any case (but note that the operating system may delete temporary files automatically, \eg, when \HOL{} exits). \subsection{Installing SMT solvers} \ml{HolSmtLib} has been tested with Yices~1.0.29 and Z3~2.19. Later versions may or may not work. (Yices~2 is not supported.) To use \ml{HolSmtLib}, you need to install at least one of these SMT solvers on your machine. As mentioned before, Yices supports a larger fragment of higher-order logic than Z3, but proof reconstruction has been implemented only for Z3. Yices is available for various platforms from \url{http://yices.csl.sri.com/}. After installation, you must set the environment variable {\tt \$HOL4\_YICES\_EXECUTABLE} to the name of the Yices executable, \eg, {\tt /bin/yices}, before you invoke \HOL. The Z3 website, \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}, provides Windows and Linux versions of the solver. Alternatively, the Windows version can be installed on Linux and Mac OS~X---see the instructions at \url{http://www4.in.tum.de/~boehmes/z3.html}.\footnote{Later versions of Z3 than 2.19 are available for Mac OS~X directly, but not supported by \HOL.} After installation, you must set the environment variable {\tt \$HOL4\_Z3\_EXECUTABLE} to the name of the Z3 executable, \eg, {\tt /bin/z3}, before you invoke \HOL. It should be relatively straightforward to integrate other SMT solvers that support the SMT-LIB~2 input format as oracles. However, this will involve a (typically small) amount of Standard ML programming, \eg, to interpret the solver's output. See \ml{Z3.sml} for some relevant code. \subsection{Wishlist} The following features have not been implemented yet. Please submit additional feature requests (or code contributions) via \url{http://github.com/HOL-Theorem-Prover/HOL}. \paragraph{Counterexamples} For satisfiable input formulas, SMT solvers typically return a satisfying assignment. This assignment could be displayed to the \HOL{} user as a counterexample. It could also be turned into a theorem, similar to the way \ml{HolSatLib} treats satisfying assignments. \paragraph{Proof reconstruction for other SMT solvers} Proof reconstruction has been implemented only for Z3. Several other SMT solvers can produce proofs, and it would be nice to offer \HOL{} users more choice. However, in the absence of a standard proof format for SMT solvers, it is perhaps not worth the implementation effort. \paragraph{Support for Z3's SMT-LIB extensions} Z3 supports extensions of the SMT-LIB language, \eg, data types. \ml{HolSmtLib} does not utilize these extensions yet when calling Z3. This would require the translation for Z3 to be distinct from the generic SMT-LIB translation. \paragraph{SMT solvers as a web service} The need to install an SMT solver locally poses an entry barrier. It would be much more convenient to have a web server running one (or several) SMT solvers, roughly similar to the ``System on TPTP'' interface that G.~Sutcliffe provides for first-order theorem provers (\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}). For Isabelle/HOL, such a web service has been installed by S.~B{\"o}hme in Munich, but unfortunately it is not publicly available. Perhaps the SMT-EXEC initiative (\url{http://www.smtexec.org/}) could offer hardware or implementation support. \index{HolSmtLib|)} %%% Local Variables: %%% mode: latex %%% TeX-master: "description" %%% End: