1\index{HolSmtLib|(} 2\index{SMT solvers|see {HolSmtLib}} 3\index{decision procedures!SMT} 4 5\setcounter{sessioncount}{0} 6 7The purpose of \ml{HolSmtLib} is to provide a platform for 8experimenting with combinations of interactive theorem proving and 9Satisfiability Modulo Theories~(SMT) solvers. \ml{HolSmtLib} was 10developed as part of a research project on {\it Expressive 11 Multi-theory Reasoning for Interactive Verification} (EPSRC grant 12EP/F067909/1) from 2008 to~2011. It is loosely inspired by 13\ml{HolSatLib} (Section~\ref{sec:HolSatLib}), and has been described 14in parts in the following publications: 15\begin{itemize} 16\item Tjark Weber: {\it SMT Solvers: New Oracles for the HOL Theorem 17 Prover}. To appear in International Journal on Software Tools for 18 Technology Transfer (STTT), 2011. 19\item Sascha B{\"o}hme, Tjark Weber: {\it Fast LCF-Style Proof 20 Reconstruction for Z3}. In Matt Kaufmann and Lawrence C.\ Paulson, 21 editors, Interactive Theorem Proving, First International 22 Conference, ITP 2010, Edinburgh, UK, July 11--14, 2010. 23 Proceedings, volume 6172 of Lecture Notes in Computer Science, pages 24 179--194. Springer, 2010. 25\end{itemize} 26\ml{HolSmtLib} uses external SMT solvers to prove instances of SMT 27tautologies, \ie, formulas that are provable using (a combination of) 28propositional logic, equality reasoning, linear arithmetic on integers 29and reals, and decision procedures for bit vectors and arrays. The 30supported fragment of higher-order logic varies with the SMT solver 31used, and is discussed in more detail below. At least for Yices, it 32is a superset of the fragment supported by \ml{bossLib.DECIDE} (and 33the performance of \ml{HolSmtLib}, especially on big problems, should 34be much better). 35 36\subsection{Interface} 37 38The library currently provides three tactics to invoke different SMT 39solvers, namely \ml{YICES\_TAC}, \ml{Z3\_ORACLE\_TAC}, and 40\ml{Z3\_TAC}. These tactics are defined in the \ml{HolSmtLib} 41structure, which is the library's main entry point. Given a 42goal~$(\Gamma, \varphi)$ (where $\Gamma$ is a list of assumptions, and 43$\varphi$ is the goal's conclusion), each tactic returns (i)~an empty 44list of new goals, and (ii)~a validation function that returns a 45theorem~$\Gamma' \vdash \varphi$ (with $\Gamma' \subseteq \Gamma$). 46These tactics fail if the SMT solver cannot prove the 47goal.\footnote{Internally, the goal's assumptions and the 48 \emph{negated} conclusion are passed to the SMT solver. If the SMT 49 solver determines that these formulas are unsatisfiable, then the 50 (unnegated) conclusion must be provable from the assumptions.} In 51other words, these tactics solve the goal (or fail). As with other 52tactics, \ml{Tactical.TAC\_PROOF} can be used to derive functions of 53type \ml{goal -> thm}. 54 55For each tactic, the \ml{HolSmtLib} structure additionally provides a 56corresponding function of type \ml{term -> thm}. These functions are 57called \ml{YICES\_PROVE}, \ml{Z3\_ORACLE\_PROVE}, and \ml{Z3\_PROVE}, 58respectively. Applied to a formula $\varphi$, they return the theorem 59$\emptyset \vdash \varphi$ (or fail). 60 61\paragraph{Oracles vs.\ proof reconstruction} 62 63\ml{YICES\_TAC} and \ml{Z3\_ORACLE\_TAC} use the SMT solver (Yices and 64Z3, respectively) as an oracle: the solver's result is trusted. Bugs 65in the SMT solver or in \ml{HolSmtLib} could potentially lead to 66inconsistent theorems. Accordingly, the derived theorem is tagged 67with an oracle tag. 68 69\ml{Z3\_TAC}, on the other hand, performs proof reconstruction. It 70requests a detailed proof from Z3, which is then checked in \HOL{}. 71One obtains a proper \HOL{} theorem; no (additional) oracle tags are 72introduced. However, Z3's proofs do not always contain enough 73information to allow efficient checking in \HOL{}; therefore, proof 74reconstruction may be slow or fail. 75 76\paragraph{Supported subsets of higher-order logic} 77 78\ml{YICES\_TAC} employs a translation into Yices's native input 79format. The interface supports types \holtxt{bool}, \holtxt{num}, 80\holtxt{int}, \holtxt{real}, \holtxt{->} (\ie, function types), 81\holtxt{prod} (\ie, tuples), fixed-width word types, inductive data 82types, records, and the following terms: equality, Boolean connectives 83(\holtxt{T}, \holtxt{F}, \holtxt{==>}, \holtxt{/\bs}, \holtxt{\bs /}, 84negation, \holtxt{if-then-else}, \holtxt{bool-case}), quantifiers 85(\holtxt{!}, \holtxt{?}), numeric literals, arithmetic operators 86(\holtxt{SUC}, \holtxt{+}, \holtxt{-}, \holtxt{*}, \holtxt{/}, unary 87minus, \holtxt{DIV}, \holtxt{MOD}, \holtxt{ABS}, \holtxt{MIN}, 88\holtxt{MAX}), comparison operators (\holtxt{<}, \holtxt{<=}, 89\holtxt{>}, \holtxt{>=}, both on \holtxt{num}, \holtxt{int}, and 90\holtxt{real}), function application, lambda abstraction, tuple 91selectors \holtxt{FST} and \holtxt{SND}, and various word operations. 92 93Z3 is integrated via a more restrictive translation into SMT-LIB~2 94format, described below. Therefore, Yices is typically the solver of 95choice at the moment (unless you need proof reconstruction, which is 96available for Z3 only). However, there are a few operations (\eg, 97specific word operations) that are supported by the SMT-LIB format, 98but not by Yices. See \ml{selftest.sml} for further details. 99 100Terms of higher-order logic that are not supported by the respective 101target solver/\allowbreak translation are typically treated in one of 102three ways: 103\begin{enumerate} 104\item Some unsupported terms are replaced by equivalent suppported 105 terms during a pre-processing step. For instance, all tactics first 106 generalize the goal's conclusion by stripping outermost universal 107 quantifiers, and attempt to eliminate certain set expressions by 108 rewriting them into predicate applications: \eg, \holtxt{y IN \{x | 109 P x\}} is replaced by \holtxt{P y}. The resulting term is 110 $\beta$-normalized. Depending on the target solver, further 111 simplifications are performed. 112\item Remaining unsupported constants are treated as uninterpreted, 113 \ie, replaced by fresh variables. This should not affect soundness, 114 but it may render goals unprovable and lead to spurious 115 counterexamples. To see all fresh variables introduced by the 116 translation, you can set \ml{HolSmtLib}'s tracing variable (see 117 below) to a sufficiently high value. 118\item Various syntactic side conditions are currently not enforced by 119 the translation and may result in invalid input to the SMT solver. 120 For instance, Yices only allows \emph{linear} arithmetic (\ie, 121 multiplication by constants) and word-shifts by numeric literals 122 (constants). If the goal is outside the allowed syntactic fragment, 123 the SMT solver will typically fail to decide the problem. 124 \ml{HolSmtLib} at present only provides a generic error message in 125 this case. Inspecting the SMT solver's output might provide further 126 hints. 127\end{enumerate} 128 129\begin{session} 130\begin{verbatim} 131- load "HolSmtLib"; open HolSmtLib; 132(* output omitted *) 133> val it = () : unit 134 135- show_tags := true; 136> val it = () : unit 137 138- YICES_PROVE ``(a ==> b) /\ (b ==> a) = (a=b)``; 139> val it = [oracles: DISK_THM, HolSmtLib] [axioms: ] [] 140 |- (a ==> b) /\ (b ==> a) = (a = b) : thm 141 142- Z3_ORACLE_PROVE ``(a ==> b) /\ (b ==> a) = (a=b)``; 143> val it = [oracles: DISK_THM, HolSmtLib] [axioms: ] [] 144 |- (a ==> b) /\ (b ==> a) = (a = b) : thm 145 146- Z3_PROVE ``(a ==> b) /\ (b ==> a) = (a=b)``; 147> val it = [oracles: DISK_THM] [axioms: ] [] 148 |- (a ==> b) /\ (b ==> a) = (a = b) : thm 149\end{verbatim} 150\end{session} 151 152\paragraph{Support for the SMT-LIB 2 file format} 153 154SMT-LIB (see \url{http://combination.cs.uiowa.edu/smtlib/}) is the 155standard input format for SMT solvers. \ml{HolSmtLib} supports (a 156subset of) version~2.0 of this format. A translation of \HOL{} terms 157into SMT-LIB~2 format is available in \ml{SmtLib.sml}, and a parser 158for SMT-LIB~2 files (translating them into \HOL{} types, terms, and 159formulas) can be found in \ml{SmtLib\_Parser.sml}, with auxiliary 160functions in \ml{SmtLib\_\{Logics,Theories\}.sml}. 161 162The SMT-LIB~2 translation supports types \holtxt{bool}, \holtxt{int} 163and \holtxt{real}, fixed-width word types, and the following terms: 164equality, Boolean connectives, quantifiers, numeric literals, 165arithmetic operators, comparison operators, function application, and 166various word operations. Notably, the SMT-LIB interface does 167\emph{not} support type \holtxt{num}, data types or records, and 168higher-order formulas. See the files mentioned above and the examples 169in \ml{selftest.sml} for further details. 170 171\paragraph{Tracing} 172 173Tracing output can be controlled via \ml{Feedback.set\_trace 174 "HolSmtLib"}. See the source code in \ml{Library.sml} for 175possible values. 176 177Communication between \HOL{} and external SMT solvers is via temporary 178files. These files are located in the standard temporary directory, 179typically {\tt /tmp} on Unix machines. The actual file names are 180generated at run-time, and can be shown by setting the above tracing 181variable to a sufficiently high value. 182 183The default behavior of \ml{HolSmtLib} is to delete temporary files 184after successful invocation of the SMT solver. This also can be 185changed via the above tracing variable. If there is an error, files 186are retained in any case (but note that the operating system may 187delete temporary files automatically, \eg, when \HOL{} exits). 188 189\subsection{Installing SMT solvers} 190 191\ml{HolSmtLib} has been tested with Yices~1.0.29 and Z3~2.19. Later 192versions may or may not work. (Yices~2 is not supported.) To use 193\ml{HolSmtLib}, you need to install at least one of these SMT solvers 194on your machine. As mentioned before, Yices supports a larger 195fragment of higher-order logic than Z3, but proof reconstruction has 196been implemented only for Z3. 197 198Yices is available for various platforms from 199\url{http://yices.csl.sri.com/}. After installation, you must set the 200environment variable {\tt \$HOL4\_YICES\_EXECUTABLE} to the name of 201the Yices executable, \eg, {\tt /bin/yices}, before you invoke \HOL. 202 203The Z3 website, 204\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}, 205provides Windows and Linux versions of the solver. Alternatively, the 206Windows version can be installed on Linux and Mac OS~X---see the 207instructions at 208\url{http://www4.in.tum.de/~boehmes/z3.html}.\footnote{Later versions 209 of Z3 than 2.19 are available for Mac OS~X directly, but not 210 supported by \HOL.} After installation, you must set the 211environment variable {\tt \$HOL4\_Z3\_EXECUTABLE} to the name of the 212Z3 executable, \eg, {\tt /bin/z3}, before you invoke \HOL. 213 214It should be relatively straightforward to integrate other SMT solvers 215that support the SMT-LIB~2 input format as oracles. However, this 216will involve a (typically small) amount of Standard ML programming, 217\eg, to interpret the solver's output. See \ml{Z3.sml} for some 218relevant code. 219 220\subsection{Wishlist} 221 222The following features have not been implemented yet. Please submit 223additional feature requests (or code contributions) via 224\url{http://github.com/mn200/HOL}. 225 226\paragraph{Counterexamples} 227 228For satisfiable input formulas, SMT solvers typically return a 229satisfying assignment. This assignment could be displayed to the 230\HOL{} user as a counterexample. It could also be turned into a 231theorem, similar to the way \ml{HolSatLib} treats satisfying 232assignments. 233 234\paragraph{Proof reconstruction for other SMT solvers} 235 236Proof reconstruction has been implemented only for Z3. Several other 237SMT solvers can produce proofs, and it would be nice to offer \HOL{} 238users more choice. However, in the absence of a standard proof format 239for SMT solvers, it is perhaps not worth the implementation effort. 240 241\paragraph{Support for Z3's SMT-LIB extensions} 242 243Z3 supports extensions of the SMT-LIB language, \eg, data types. 244\ml{HolSmtLib} does not utilize these extensions yet when calling Z3. 245This would require the translation for Z3 to be distinct from the 246generic SMT-LIB translation. 247 248\paragraph{SMT solvers as a web service} 249 250The need to install an SMT solver locally poses an entry barrier. It 251would be much more convenient to have a web server running one (or 252several) SMT solvers, roughly similar to the ``System on TPTP'' 253interface that G.~Sutcliffe provides for first-order theorem provers 254(\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}). For 255Isabelle/HOL, such a web service has been installed by S.~B{\"o}hme in 256Munich, but unfortunately it is not publicly available. Perhaps the 257SMT-EXEC initiative (\url{http://www.smtexec.org/}) could offer 258hardware or implementation support. 259 260\index{HolSmtLib|)} 261 262%%% Local Variables: 263%%% mode: latex 264%%% TeX-master: "description" 265%%% End: 266