Tomasz Węgrzanowski's Blog

Open Source Adventures: Episode 03: Object-Oriented Interface for Crystal Z3

Tomasz Węgrzanowski's photo
Tomasz Węgrzanowski
·

7 min read

In previous two episodes we figured out how to make Crystal work with Z3 using a low level interface, now it's time to wrap it all in objects.

The most important thing is that our objects will NOT map to C types. C has types like Ast, but we want type like Z3::IntExpr or Z3::BoolExpr.

Even worse, at some point we'll also want complex types like Z3::BitVectorExpr(32). And these are not just for our convenience - Z3 will crash if you mix them up, even if C type checks.

In the Ruby Z3 gem I do a lot of runtime type checks and (if semantically safe) type conversions, but hopefully in Crystal we can have compile time type checker do some of that work for us.

I'm not sure if Crystal will be able to figure out rules for bit vectors (appending BV(8) to BV(8) creates BV(16) etc.), so maybe we'll need some runtime type checking, but no bit vectors yet.

LibZ3

Let's start with the lowest level interface. I only added one entry mk_bool_sort, but I moved it to libz3.cr. I'm not entirely sure how to name and organize the whole thing yet. We'll get there when we'll get there.

@[Link("z3")]
lib LibZ3
  type Ast = Void*
  type Config = Void*
  type Context = Void*
  type Model = Void*
  type Solver = Void*
  type Sort = Void*
  type Symbol = Void*

  enum LBool : Int32
    False = -1
    Undefined = 0
    True = 1
  end

  # Just list the ones we need, there's about 700 API calls total
  fun mk_add = Z3_mk_add(ctx : Context, count : UInt32, asts : Ast*) : Ast
  fun mk_const = Z3_mk_const(ctx : Context, name : Symbol, sort : Sort) : Ast
  fun mk_context = Z3_mk_context(cfg : Config) : Context
  fun mk_config = Z3_mk_config() : Config
  fun mk_eq = Z3_mk_eq(ctx : Context, a : Ast, b : Ast) : Ast
  fun mk_ge = Z3_mk_ge(ctx : Context, a : Ast, b : Ast) : Ast
  fun mk_gt = Z3_mk_gt(ctx : Context, a : Ast, b : Ast) : Ast
  fun mk_int_sort = Z3_mk_int_sort(ctx : Context) : Sort
  fun mk_bool_sort = Z3_mk_bool_sort(ctx : Context) : Sort
  fun mk_le = Z3_mk_le(ctx : Context, a : Ast, b : Ast) : Ast
  fun mk_lt = Z3_mk_lt(ctx : Context, a : Ast, b : Ast) : Ast
  fun mk_distinct = Z3_mk_distinct(ctx : Context, count : UInt32, asts : Ast*) : Ast
  fun mk_mul = Z3_mk_mul(ctx : Context, count : UInt32, asts : Ast*) : Ast
  fun mk_numeral = Z3_mk_numeral(ctx : Context, s : UInt8*, sort : Sort) : Ast
  fun mk_solver = Z3_mk_solver(ctx : Context) : Solver
  fun mk_string_symbol = Z3_mk_string_symbol(ctx : Context, s : UInt8*) : Symbol
  fun model_to_string = Z3_model_to_string(ctx : Context, model : Model) : UInt8*
  fun solver_assert = Z3_solver_assert(ctx : Context, solver : Solver, ast : Ast) : Void
  fun solver_check = Z3_solver_check(ctx : Context, solver : Solver) : LBool
  fun solver_get_model = Z3_solver_get_model(ctx : Context, solver : Solver) : Model
end

SEND+MORE=MONEY

And now let's jump to the other end, and see how the program using our library looks like.

#!/usr/bin/env crystal

require "./z3"

# Setup library
solver = Z3::Solver.new

# Variables, all 0 to 9
vars = Hash(Symbol, Z3::IntExpr).new
%i[s e n d m o r e m o n e y].uniq.each do |name|
  var = Z3::IntSort[name]
  vars[name] = var
  solver.assert var >= Z3::IntSort[0]
  solver.assert var <= Z3::IntSort[9]
end

# m and s need to be >= 1, no leading zeroes
solver.assert vars[:m] >= Z3::IntSort[1]
solver.assert vars[:s] >= Z3::IntSort[1]

# all letters represent different digits
solver.assert Z3.distinct(vars.values)

# SEND + MORE = MONEY
send_sum = (
  vars[:s] * Z3::IntSort[1000] +
  vars[:e] * Z3::IntSort[100] +
  vars[:n] * Z3::IntSort[10] +
  vars[:d]
)

more_sum = (
  vars[:m] * Z3::IntSort[1000] +
  vars[:o] * Z3::IntSort[100] +
  vars[:r] * Z3::IntSort[10] +
  vars[:e]
)

money_sum = (
  vars[:m] * Z3::IntSort[10000] +
  vars[:o] * Z3::IntSort[1000] +
  vars[:n] * Z3::IntSort[100] +
  vars[:e] * Z3::IntSort[10] +
  vars[:y]
)

solver.assert send_sum + more_sum == money_sum

# Get the result
result_code = solver.check
puts "Result code is: #{result_code}"
puts solver.model

This is notably improved. I changed the API from using Strings to using Symbols as perhaps better indicating what it's supposed to mean, but I might revert it all back (Ruby gem uses Strings in all examples, but I think it will let you pass Symbols and just convert them to Strings anyway).

There are a few things missing here, compared with the Ruby Z3 gem:

  • we really don't want all those Z3::IntSort[1000] casts. We want a + b, a + 100, and 100 + a etc. work, and for all Integer-like types, not just Int32.
  • the interface around check/model should be automatic - right now the process is "call .check, if it returns True, call .model, otherwise do not call .model as it will crash". We want such concerns to be handled by the library
  • model should return a Hash with results, but a Hash of what? We don't want to expose Hash(Symbol, LibZ3::Ast) as that's crash-prone, so we'd need to somehow figure out which result is which type

Z3 module

Here's the "low level but not very low level" API. I think it should be renamed somehow, to make clear it's not meant to be used directly (in Ruby I use Z3::VeryLowLevel for C API, and Z3::LowLevel for equivalent of this).

This is unchanged from previous episode.

require "./libz3"

module Z3
  extend self

  Context = LibZ3.mk_context(LibZ3.mk_config)

  def mk_solver
    LibZ3.mk_solver(Context)
  end

  def mk_numeral(num, sort)
    LibZ3.mk_numeral(Context, num.to_s, sort)
  end

  def mk_const(name, sort)
    name_sym = LibZ3.mk_string_symbol(Context, name)
    var = LibZ3.mk_const(Context, name_sym, sort)
  end

  def mk_eq(a, b)
    LibZ3.mk_eq(Context, a, b)
  end

  def mk_ge(a, b)
    LibZ3.mk_ge(Context, a, b)
  end

  def mk_gt(a, b)
    LibZ3.mk_gt(Context, a, b)
  end

  def mk_le(a, b)
    LibZ3.mk_le(Context, a, b)
  end

  def mk_lt(a, b)
    LibZ3.mk_lt(Context, a, b)
  end

  def mk_add(asts)
    LibZ3.mk_add(Context, asts.size, asts)
  end

  def mk_mul(asts)
    LibZ3.mk_mul(Context, asts.size, asts)
  end

  def mk_distinct(asts)
    LibZ3.mk_distinct(Context, asts.size, asts)
  end

  def solver_assert(solver, ast)
    LibZ3.solver_assert(Context, solver, ast)
  end

  def solver_check(solver)
    LibZ3.solver_check(Context, solver)
  end

  def solver_get_model(solver)
    LibZ3.solver_get_model(Context, solver)
  end

  def model_to_string(model)
    String.new LibZ3.model_to_string(Context, model)
  end
end

Object Oriented API

OK, and let's finally get to the interesting part.

class Z3::Solver
  def initialize
    @solver = Z3.mk_solver
  end

  def assert(expr)
    Z3.solver_assert(@solver, expr._expr)
  end

  def check
    Z3.solver_check(@solver)
  end

  def model
    Z3::Model.new(Z3.solver_get_model(@solver))
  end
end

class Z3::Model
  def initialize(model : LibZ3::Model)
    @model = model
  end

  # This needs to go eventually
  def to_s(io)
    io << Z3.model_to_string(@model).chomp
  end
end

class Z3::IntSort
  @@sort = LibZ3.mk_int_sort(Context)

  def self.[](name : Symbol)
    Z3::IntExpr.new Z3.mk_const(name.to_s, @@sort)
  end

  def self.[](v : Int32)
    Z3::IntExpr.new Z3.mk_numeral(v, @@sort)
  end
end

class Z3::BoolSort
  @@sort = LibZ3.mk_bool_sort(Context)
end

class Z3::IntExpr
  def initialize(expr : LibZ3::Ast)
    @expr = expr
  end

  def sort
    Z3::IntSort
  end

  def ==(other : Z3::IntExpr)
    Z3::BoolExpr.new Z3.mk_eq(@expr, other._expr)
  end

  def >=(other : Z3::IntExpr)
    Z3::BoolExpr.new Z3.mk_ge(@expr, other._expr)
  end

  def >(other : Z3::IntExpr)
    Z3::BoolExpr.new Z3.mk_gt(@expr, other._expr)
  end

  def <=(other : Z3::IntExpr)
    Z3::BoolExpr.new Z3.mk_le(@expr, other._expr)
  end

  def <(other : Z3::IntExpr)
    Z3::BoolExpr.new Z3.mk_lt(@expr, other._expr)
  end

  def *(other : Z3::IntExpr)
    Z3::IntExpr.new Z3.mk_mul([@expr, other._expr])
  end

  def +(other : Z3::IntExpr)
    Z3::IntExpr.new Z3.mk_add([@expr, other._expr])
  end

  def _expr
    @expr
  end
end

class Z3::BoolExpr
  def initialize(expr : LibZ3::Ast)
    @expr = expr
  end

  def sort
    Z3::BoolSort
  end

  def _expr
    @expr
  end
end

# Not sure where to put this
def Z3.distinct(args : Array(Z3::IntExpr))
  Z3::BoolExpr.new Z3.mk_distinct(args.map(&._expr))
end

It's good enough to support our current use case, however we face quite a few issues:

  • I'd like that _expr to be somehow exposed only in-package, but not exposed to the public API, as using is extremely crash-prone. I put '_' in front in Python-style convention (also in Ruby), but maybe there's some better solution?
  • it all needs type conversions, and from all builtin integer-like types, not just Int32
  • I'm especially unclear on type conversions if left side is an integer-like type, and right side is a Z3::IntExpr, Ruby has runtime #coerce system for it
  • it's not really clear why now I need to add .chomp inside Z3::Model.to_s - before I could puts Z3.model_to_string(@model) and it would not do a double-newline
  • these are all singleton classes like Z3::IntSort, but this interface wouldn't work so great on non-singleton classes like Z3::BitVectorSort(32)
  • Z3.distinct doesn't fit anywhere right now, and I'll need to add a few more such methods later - I did the same thing and threw them into Z3 module in Ruby too

Story so far

All the code is in crystal-z3 repo.

The API is incomplete, both for trivial reasons (+ but no -, no boolean operators etc.), and for more fundamental reasons (especially no way to extract result from Z3::Model just to dump it to string), but it's quite close to the point of being usable.

Coming next

In the next episode we'll see if we can avoid explicit casting of integers.

Ruby