Integrating Z3 Into Your Tool

April 23, 2014 · 5 minute read

In my research, I make heavy use of SMT solvers to build software verification tools (specificially, Microsoft’s Z3). Anyone who’s tried writing this sort of software eventually runs into a fundamental question: what interface should I use between my tool and the solver?

In general, there are two strategies for implementing this integration:

  1. Use the z3 standalone executable, and pass it queries through its command line interface. This strategy requires that you first output queries in a file format such as SMT-LIB2. I call this strategy “lightweight” integration.

  2. Integrate with Z3 at the API level by using or writing FFI bindings with the underlying C API. Rather than encoding queries as text files and sending them in batch to Z3, you use relevant API calls to construct and dispatch queries in memory. I call this strategy “heavyweight” integration.

Advantages of lightweight integration

  1. Significantly eases the burden of debugging queries. You have a text file that you can examine, edit, and debug as you please. These queries files also serve as persisted “proofs”.

  2. Does not require the existence of a binding library between your language and Z3.

  3. Isolates errors in your tool from those in Z3. If your program crashes, you can be sure it wasn’t because of something like a segfault in Z3 (so long as you have adequate checks for z3 abnormal termination).

  4. Compatibility with other SMT solvers. The SMT-LIB2 format is a standard that is mostly compatible with other solvers as long as you don’t make use of Z3-specific constructs.

Advantages of heavyweight integration

  1. Faster. Lightweight integration is comparatively slow due to the overhead of writing files and invoking an external process for each dispatch to z3. Some verification tools can dispatch hundreds of thousands of small queries, and IO+process overhead can be quite significant.

  2. Allows incremental computation. Rather than sending an entire query at once, you can make use of features like push and pop all within a single Z3 process. This also makes use of Z3’s internal ability to cache incremental results.

Regardless of your integration strategy, it’s a good idea to isolate the low-level Z3 interface from a higher-level interface for constructing queries at a higher level of abstraction.

For instance, I encapsulate my low-level lightweight Z3 interface in a Scala module called Z3 that defines types corresponding to entities at the logic level. These types essentially map one-to-one to language entities in SMT-LIB2. Here’s a skeleton of Z3, although I’ve omitted a lot for brevity:

object Z3 {

    // binary operations
    sealed trait Bop
    case object Add extends Bop
    case object Sub extends Bop

    // expressions
    sealed trait Expr
    case class EBin(b: Bop, e1: Expr, e2: Expr) extends Expr
    case class EVar(s: String) extends Expr

    // predicates
    sealed trait Pred
    case object PTrue extends Pred
    case object PFalse extends Pred
    case object PAnd(ps: Seq[Pred]) extends Pred
    case object PAtom(b: Brel, e1: Expr, e2: Expr) extends Pred

    // relations
    sealed trait Brel
    case object Eq extends Brel
    case object Ne extends Brel

    // types
    sealed trait Ty
    case class BoolTy extends Ty
    case class IntTy extends Ty

    // declarations
    sealed trait Declaration
    case class ConstDeclaration(name: String, ty: Ty) extends Declaration

    // assertions
    case class Assertion(p: Pred)

    // commands
    sealed trait Command
    case object CheckSat extends Command

    def toQuery(decls: Seq[Declaration], assns: Seq[Assertion]): String = { ... }
    def executeRaw(q: String): String = { ... }

    def isSat(decls: Seq[Declaration], assns: Seq[Assertion]): Boolean = {
        executeRaw(toQuery(decls, assns)) match {
            case "unsat" => false
            case "sat"   => true
            case _       => // ... error

The function toQuery constructs a query string from a set of declarations and assertions by recursive construction. executeRaw then simply emits the query string to a file, invokes z3, waits for it to terminate, then returns the output of z3. isSat, as its name suggests, just returns true if the supplied system of constraints (assertions) is satisfiable by using toQuery and executeRaw under the hood.

I then have a higher level module called Check that translates verification obligations from the source language being verified down to types from the Z3 module. To check those obligations, it invokes isSat with a properly crafted set of assertions:

object Check {
    def check(pre: SExpr, path: SPath, post: SExpr): Boolean = { ... }

In particular, the function check verifies that any program state satisfying the precondition pre entails the postcondition post after executing path, so long as path terminates. In more formal terms, it checks that the strongest postcondition of pre with respect to path implies post. I’ve elided the contents of check because its implementation depends greatly on the source language, but the general idea is to translate path into a sequence of assertions where each assertion encodes the effect of a statement in that path. We then check the validity of the encoded formula $pre \land path \rightarrow post$ by checking that the formula $pre \land path \land \lnot post$ is unsatisfiable.1

What makes Check high-level? Well, the module’s public interface makes no reference to the low-level types from Z3, but rather types corresponding to elements of the source language being verified: SExpr is the type of expressions in the source language, and SPath encodes a sequence of statements along an execution path. Thus, one can use Check without ever having to worry about the underlying logic or constraint solving engine.

  1. This is due to the equivalence $p \rightarrow q \equiv \lnot p \lor q$. [return]