Architecture of z3 gem

This post is meant for people who want to dig deep into Z3 gem, or who want to learn from example how to interface with another complex C library. Regular users of Z3 are better off checking out some tutorials I wrote.

Architecture of z3 gem The z3 theorem prover is a C library with quite complex API, and z3 gem needs to take a lot of steps to provide good ruby experience with it.

Z3 C API Overview

The API looks conventional at first - a bunch of black box data types like Z3_context Z3_ast (Abstract Syntax Tree), and a bunch of functions to operate on them. For example to create a node representing equality of two nodes, you call:

Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r);

A huge problem is that so many of those calls claim to accept Z3_ast, but it needs to be particular kind of Z3_ast, otherwise you get a segfault. It's not even static limitation - l and r can be anything, but they must represent the same type. So any kind of thin wrapper is out of the question.

Very Low Level API

The gem uses ffi to setup Z3::VeryLowLevel with direct C calls. For example the aforementioned function is attached like this:

attach_function :Z3_mk_eq, [:ctx_pointer, :ast_pointer, :ast_pointer], :ast_pointer

There's 618 API calls, so it would be tedious to do it manually, so instead a tiny subproject lives in api and generates most of it with some regular expressions. A list of C API calls is extracted from Z3 documentation into api/definitions.h. They look like this:

def_API('Z3_mk_eq', AST, (_in(CONTEXT), _in(AST), _in(AST)))

Then api/gen_api script translates it into proper ruby code. It might seem like it could be handled by ffi library, but there are too many Z3-specific hacks needed. A small number of function calls can't be handled automatically, so they're written manually.

For example Z3_mk_add function creates a node representing addition of any number of nodes, and has signature of:

attach_function :Z3_mk_add, [:ctx_pointer, :int, :pointer], :ast_pointer

Low Level API

There's one intermediate level between raw C calls and ruby code. Z3::LowLevel is also mostly generated by api/gen_api. Here's an example of automatically generated code:

def mk_eq(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_eq(_ctx_pointer, ast1._ast, ast2._ast)
end

And this one is written manually, with proper helpers:

def mk_and(asts) #=> :ast_pointer
  VeryLowLevel.Z3_mk_and(_ctx_pointer, asts.size, asts_vector(asts))
end

A few things are happening here:

• Z3 API requires Z3_context pointer for almost all of its calls - we automatically provide it with singleton _ctx_pointer.
• We get ruby objects, and extract C pointers from them.
• We return C pointers FFI::Pointer and leave responsibility for wrapping them into ruby objects to the caller, as we actually don't have enough information here to do so.

Another thing Z3::LowLevel API does is setting up error callback, to convert Z3 errors into Ruby exceptions.

Ruby objects

And finally we get to ruby objects like Z3::AST, which is a wrapper for FFI::Pointer representing Z3_ast. Other Z3 C data types get similar treatment.

module Z3
  class AST
    attr_reader :_ast
    def initialize(_ast)
      raise Z3::Exception, "AST expected, got #{_ast.class}" unless _ast.is_a?(FFI::Pointer)
      @_ast = _ast
    end

    # ...

    private_class_method :new
  end
end

First weird thing is this Python-style pseudo-private ._ast. This really shouldn't ever be accessed by user of the gem, but it needs to be accessed by Z3::LowLevel a lot. Ruby doesn't have any concept of C++ style "friend" classes. I've chosen Python pseudo-private convention as opposed to a lot of .instance_eval or similar.

Another weird thing is that Z3::AST class prevents object creation - only its subclasses representing nodes of specific type can be instantiated.

Sorts

Z3 ASTs represent multiple things, mostly sorts and expressions. Z3 automatically interns ASTs, so two identically-shaped ASTs will be the same underlying objects (like two same Ruby Symbols), saving us memory management hassle here.

Sorts are sort of like types. The gem creates a parallel hierarchy so every underlying sort gets an object of its specific class. For example here's whole Z3::BoolSort, which should only have a single object.

module Z3
  class Sort < AST
    def initialize(_ast)
      super(_ast)
      raise Z3::Exception, "Sorts must have AST kind sort" unless ast_kind == :sort
    end
    # ...

module Z3
  class BoolSort < Sort
    def initialize
      super LowLevel.mk_bool_sort
    end

    def expr_class
      BoolExpr
    end

    def from_const(val)
      if val == true
        BoolExpr.new(LowLevel.mk_true, self)
      elsif val == false
        BoolExpr.new(LowLevel.mk_false, self)
      else
        raise Z3::Exception, "Cannot convert #{val.class} to #{self.class}"
      end
    end

    public_class_method :new
  end
end

ast_kind check is for additional segfault prevention.

BoolSort.new creates Ruby object with instance variable _sort pointing to Z3_ast describing Boolean sort.

It seems a bit overkillish to setup so much structure for BoolSort with just two instance values, but some Sort classes have multiple Sort instances. For example Bit Vectors of width n are:

module Z3
  class BitvecSort < Sort
    def initialize(n)
      super LowLevel.mk_bv_sort(n)
    end

    def expr_class
      BitvecExpr
    end    

Expressions

Expressions are also ASTs, but they all carry reference to Ruby instance of their sort.

module Z3
  class Expr < AST
    attr_reader :sort
    def initialize(_ast, sort)
      super(_ast)
      @sort = sort
      unless [:numeral, :app].include?(ast_kind)
        raise Z3::Exception, "Values must have AST kind numeral or app"
      end
    end

This again might seem like an overkill for expressions representing Bool true, but it's extremely important for BitvecExpr to know if it's 8-bit or 24-bit. Because if they get mixed up, segfault.

Building Expressions

Expressions can be built from constants:

IntSort.new.from_const(42)

Declared as variables:

IntSort.new.var("x")

Or created from one or more of existing expression nodes:

module Z3
  class BitvecExpr < Expr
    def rotate_left(num)
      sort.new(LowLevel.mk_rotate_left(num, self))
    end

As you can see, the low level API doesn't know how to turn those C pointers into Ruby objects.

This interface is a bit tedious for the most common case, so there are wrappers with simple interface, which also allow mixing Z3 expressions with Ruby expressions, with a few limitations:

Z3::Int("a") + 2 == Z3::Int("b")

For some advanced use you actually need the whole interface.

Creating Sorts and Expressions from raw pointers

For ASTs we construct we track their sorts. Unfortunately sometimes Z3 gives us raw pointers and we need to guess their types - most obviously when we actually get a solution to our set of constraints.

Z3's introspection API lets us figure this out, and find out proper Ruby objects to connect to.

It has unfortunate limitation that we can only see underlying Z3 sorts. I'd prefer to have SignedBitvectorExpr and UnsignedBitvectorExpr as separate types with nice APIs, unfortunately there's no way to infer if answer Z3 gave came from Ruby SignedBitvectorExpr or UnsignedBitvectorExpr, so that idea can't work.

Printer

Expressions need to be turned into Strings for human consumption. Z3 comes with own printer, but it's some messy Lisp-like syntax, with a lot of weirdness for edge cases.

The gem instead implements its own printer in traditional math notation. Right now it sometimes overdoes explicit parentheses.

Examples

The gem comes with a set of small and intermediate examples in examples/ directory. They're a good starting point to learn common use cases.

There are obvious things like sudoku solvers, but also regular expression crossword solver.

Testing

Testing uses RSpec and has two parts.

Unit tests require a lot of custom matchers, as most objects in the gem override ==.

Some examples:

let(:a) { Z3.Real("a") }
let(:b) { Z3.Real("b") }
let(:c) { Z3.Real("c") }
it "+" do
  expect([a == 2, b == 4, c == a + b]).to have_solution(c => 6)
end

Integration tests run everything in examples and verify that output is exactly as expected. I like reusing other things as test cases like this.