technical.tex

\section{Design and implementation}
\label{sec:design-impl}

\texttt{z3.rkt} is currently implemented as a few hundred lines of Racket code
that interface with the Z3 engine via the provided library. Since the system is
still a work in progress, some of these details might change in the future.

\subsubsection{The Z3 wrapper.} We use Racket's foreign interface \cite{racket/foreign}
to map the Z3 library's C functions into Racket. The programmer interface
communicates with Z3 by calling the Racket functions defined by the
wrapper. While it is possible to use the Z3 wrapper directly, we highly
recommend using the programmer interface instead.

\subsubsection{Built-in functions.} Z3 comes with a number of built-in functions that
operate on booleans, numbers, and more complex values. We expose these
functions directly but add a \texttt{/s} suffix to their usual names in the
SMT-LIB standard, because most SMT-LIB names are already defined as functions
by Racket and we want to avoid colliding with them.

\subsubsection{The core commands.} This is a small set of Racket macros and
functions layered on top of the Z3 wrapper. The aim here is to hide the
complexities of the C wrapper (as discussed in \Fref[plain]{sec:usingsmt}) and
stay as close to SMT-LIB version 2 commands \cite{smtlib2:10} as possible. We
prefix commands with \texttt{smt:} to avoid collisions with Racket functions.

\subsection{Derived abstractions}
\label{sec:derived}

Since the full power of Racket is available to us, we can define abstractions
that allow users to simplify their code. For example, SMT-LIB allows users to
define macros via the \texttt{define-fun} command, as demonstrated by
\Fref{fig:smtlib-max}.

\begin{program}
\caption{An SMT-LIB macro, defined with \texttt{define-fun}}
\label{fig:smtlib-max}
\begin{minted}{scheme}
(define-fun max ((a Int) (b Int)) Int
  (ite (> a b) a b)) ; ite is short for if-then-else
...
(assert (= (max 4 7) 7))
\end{minted}
\end{program}

However, Z3's API exposes no such command. Our first attempt was to define a
Racket function to do the same thing, as in \Fref{fig:rkt-max-fn}.

\begin{program}
\caption{A first attempt at ``macros" in \texttt{z3.rkt}}
\label{fig:rkt-max-fn}
\begin{minted}{scheme}
(define (smt-max a b)
  (ite/s (>/s a b) a b))
...
(smt:assert (=/s (smt-max 4 7) 7))
\end{minted}
\end{program}

This works for smaller macros like \texttt{max}, but in our experience this
sort of na\"{i}ve substitution can result in final expressions for deeply
nested functions becoming too large for Z3 to handle\footnote{In theory, we
could merge common parts of expressions to reduce the number of AST nodes
generated. In our experiments, this proved to be effective, yet still
significantly slower than the solution we finally adopted.}.

We note, however, that any macro can also be written as a universally
quantified formula. For example, \texttt{max} can be rewritten as shown in
\Fref{fig:max-forall}.

\begin{program}
\caption{Macros as universally quantified formulas}
\label{fig:max-forall}
\begin{minted}{scheme}
(declare-fun max (Int Int) Int)
(assert (forall ((a Int) (b Int))
                (= (max a b)
                   (ite (> a b) a b))))
\end{minted}
\end{program}

Indeed, Z3 has a \textit{macro finder} component that identifies and
eliminates universal quantifiers that are macros in disguise. We finally
solved the problem by providing a Racket macro, \texttt{smt:define-fun}, that
has the same syntax as the SMT-LIB command and that performs precisely this
transformation.

The definition of \texttt{smt:define-fun} is listed in \Fref{fig:define-fun}.
We use Scheme's \texttt{syntax-rules} macro system \cite[Section~4.3.2]{scheme-r5rs}
to its fullest extent. \texttt{syntax-rules} accepts pairs of input and output
patterns and goes with the output pattern for the first input that can be
matched, somewhat like the \texttt{cond} construct found in many Lisps. We
handle two separate cases: (a) we're defining a plain identifier, in which
case we have no need for the \texttt{forall}, and (b) we're defining a macro
as above, in which case we do. The \texttt{...} as part of the macro
definition is a special form recognized by \texttt{syntax-rules}: wherever it
sees them in the output pattern, it substitutes for them a list of whatever
was present in the input pattern. An example of this substitution is listed in
\Fref{fig:define-fun-example}.

\begin{program}
\caption{A routine for defining macros in \texttt{z3.rkt}}
\label{fig:define-fun}
\begin{minted}{scheme}
(define-syntax smt:define-fun
  (syntax-rules ()
    [(_ id () type body) ; Plain identifiers don't need a forall
     (begin
       (smt:declare-fun id () type)
       (smt:assert (=/s id body)))]
    [(_ id ((argname argtype) ...) type body)
     (begin
       (smt:declare-fun id (argtype ...) type)
       (smt:assert (forall/s ((argname argtype) ...)
                             (=/s (id argname ...) body))))]))
\end{minted}
\end{program}

\begin{program}
\caption{\texttt{smt:define-fun} in action}
\label{fig:define-fun-example}

\begin{minted}{scheme}
(smt:define-fun foo ((x Int) (y Bool)) Int
                    (+/s x (ite/s y 20 0)))
\end{minted}

\begin{center}
{\large $\downarrow$} {\small expands to}
\end{center}

\begin{minted}{scheme}
(smt:declare-fun foo (Int Bool) Int)
(smt:assert (forall/s ((x Int) (y Bool))
                      (=/s (foo x y) (+/s x (ite/s y 20 0)))))
\end{minted}
\end{program}


\subsection{Porting existing SMT-LIB code}
\label{sec:porting-smt-lib}

One of our explicit goals is to enable existing SMT-LIB version 2 code to be
ported with a small number of systematic changes. \Fref{tab:smt-porting}
lists the minimal set of changes that needs to be made to port
existing SMT-LIB code to \texttt{z3.rkt}. We expect many SMT-LIB programs
to become shorter as authors use Racket features wherever appropriate.

\begin{table}[hbt]
\caption{Differences between SMT-LIB and \texttt{z3.rkt}}
\label{tab:smt-porting}
\begin{center}
\begin{tabularx}{0.91\textwidth}{lX}
\hline\noalign{\smallskip}
SMT-LIB code & \texttt{z3.rkt} code \\
\noalign{\smallskip}
\hline
\noalign{\smallskip}
Options: \texttt{(set-option :foo true)} & Keyword arguments: \newline \texttt{(smt:new-context \#:foo \#t)} \\

Logics: \texttt{(set-logic QF\_UF)} & The \texttt{\#:logic} keyword: \newline \texttt{(smt:new-context \#:logic "QF\_UF")} \\

Commands: \texttt{declare-fun}, \texttt{assert}, \ldots & Prefixed with \texttt{smt:} \\

Functions: \texttt{and}, \texttt{or}, \texttt{+}, \texttt{distinct} \ldots & Suffixed with \texttt{/s} \\

Boolean literals: \texttt{true} and \texttt{false} & \texttt{\#t} and \texttt{\#f} \\

% Bit-vector literals: \texttt{\#b101}, \texttt{\#x4d56} & As strings: \texttt{"\#b101"}, \texttt{"\#x4d56"} \\
\hline
\end{tabularx}
\end{center}
\end{table}

\subsection*{Summary}

In this chapter, we introduced our attempt to make a simple and accessible SMT
solver interface. We demonstrated its power with simple programs to solve
logical puzzles, including a web application for an NP-complete logical game.
We saw how the Racket language provides facilities that make the jobs of both
the interface's designer and its users easier.