Posted on Mar 2, 2022

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

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.

Top comments (4)

Ary Borenszweig • Mar 2 '22

Nice post! I'm happy that the API keeps looking better and better.

I'd like that _expr to be somehow exposed only in-package, but not exposed to the public API

You can define it like protected def _expr and it will do exactly that. protected in Crystal works different than in Ruby: only the same type or types in the same namespace (module) have access to them: crystal-lang.org/reference/1.3/syn...

I'm especially unclear on type conversions if left side is an integer-like type

You will have to define overloads on Int32 and so on. In the end if you want to define + for types A and B you will need to define A#+(B) and B#+(A). It's not ideal, but it works. That said, I also noticed that there's a coerce method in Ruby but I never understood how it works. Maybe we could have a similar thing in Crystal, not sure!

chomp

Like in Ruby, when you do puts, if the string ends with a newline it won't show up in the output. And Crystal does the same thing:

$ irb irb(main):001:0> puts "hello" hello => nil irb(main):002:0" puts "hello\n" hello => nil irb(main):003:0" puts "hello\n\n" hello => nil

That said, I don't know why model_to_string returns a newline, it sounds counterintuitive.

Tomasz Wegrzanowski • Mar 2 '22

Like in Ruby, when you do puts, if the string ends with a newline it won't show up in the output. And Crystal does the same thing:

OK, check out this code:

class Foo def as_string "A\nB\n\C\n" end def to_s(io) io << as_string end end a = Foo.new puts "One:" puts a puts "Two:" puts a.to_s puts "Done"

I'd expect puts a and puts a.to_s to do the exact same thing, but they don't, puts a outputs one extra newline. Output of this script is:

One: A B C Two: A B C Done

That's definitely unexpected, and I don't think there's any way for puts a and puts a.to_s to do different thing in Ruby.

That said, I also noticed that there's a coerce method in Ruby but I never understood how it works. Maybe we could have a similar thing in Crystal, not sure!

After I tried it a bit more, I don't think Crystal needs #coerce. Ruby doesn't have methods dispatching on both argument types, and #coerce is a runtime hooks to emulate it for math-like stuff. If you do aFloat * aMatrix or whatnot, Float#* will just see that it has no idea what aMatrix is, and fallback to Matrix#coerce to figure it out (or raises exception if there's no #coerce on its argument).

In Crystal you'd just define new method Float#*(other : Matrix) without having to redefine the original Float#* (and massive performance cost that would imply).

I don't know if there are any scenarios where that's not sufficient.

Ary Borenszweig • Mar 2 '22

Good thing to hear that coerce won't be needed! I think Julia has something similar, mainly to avoid having to do all possible combinations. But maybe not having coerce is simpler to understand.

Regarding the extra newline, the rule about not printing the last newline of a string is exclusive to printing strings. We copied that from Ruby but apparently we didn't think it well. I think Ruby does it like that because if you do puts gets it's a bit ugly to see two newlines. You'd have to call chomp, or pass chomp to gets. But in Crystal we decided that gets (and others) chomp by default o, so this exceptional newline behavior is less needed, or not needed at all. Unfortunately we decided to chomp by default after that exceptional behavior was in place, and with 1.0 it would be hard to change because it's a breaking change. But maybe it's not such a big deal! I'll open a discussion about that.

Tomasz Wegrzanowski • Mar 2 '22

It would be best if puts worked like in Ruby, and never did extra newline, even if something to_ses with a newline at the end.

Basically the algorithm would need to be something like:

def puts(obj) obj.to_s(io) io << "\n" unless io.ends_with?("\n") end

Objects to_sing to something multiline isn't that unusual, and that last \n can't always be avoided.

If that's not really doable, then that's a worse API due to this irregularity, but I guess it's not a huge issue, and every language has some irregularities.