Tomasz Węgrzanowski's Blog

Open Source Adventures: Episode 06: How my crystal-z3 compares with bcardiff's crystal-z3

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

3 min read

I was about to work on specs, but I need to interrupt this for something really interesting.

Back in 2019 bcardiff (Brian J. Cardiff) created his own crystal-z3. I had no idea about it back when I started, so these are completely independent.

LibZ3

So here's how his libz3.cr starts:

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

  enum LBool
    False = -1
    Undef
    True
  end

And here's mine:

@[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

It is basically identical. He added alias String = UInt8* (I didn't even know about alias, and it seems a bit ambiguous this way), while I made the enum a bit more explicit, but it is all nearly identical.

The list of functions in it is 80% overlapping, and even the formatting is nearly the same. Like some random examples:

fun mk_bool_sort = Z3_mk_bool_sort(c : Context) : Sort
fun mk_add = Z3_mk_add(c : Context, num_args : UInt32, args : Ast*) : Ast
fun ast_to_string = Z3_ast_to_string(c : Context, a : Ast) : String

fun mk_bool_sort = Z3_mk_bool_sort(ctx : Context) : Sort
fun mk_add = Z3_mk_add(ctx : Context, count : UInt32, asts : Ast*) : Ast
fun ast_to_string = Z3_ast_to_string(ctx : Context, ast : Ast) : UInt8*

The only real difference between our libz3.cr files is that I put it inside Z3 namespace and he didn't.

Putting everything in same namespace seemed pretty natural to me, but double checking things, apparently that's not the convention. Would that conflict with how I use protected, or not really?

Context

The biggest difference between our approaches is that his Z3 uses one Context per Solver, while mine use sone global Context.

I also have the whole layer just to avoid dealing with Contexts, while his version puts these methods on the Context object.

Output arguments

Interesting thing I discovered are out arguments. Here's his version:

res = LibZ3.model_eval(@context, self, t, model_completion, out v)
raise "fail to eval" unless res
v

Here's what I've been doing:

result_ptr = Pointer(LibZ3::Ast).malloc
result = LibZ3.model_eval(Context, model, ast, complete, result_ptr)
raise "Cannot evaluate" unless result == true
result_ptr[0]

Yeah, I'm definitely going to be using this out thing.

Operations

One place where our approaches really differ is how we represent expressions. In his version, all of them are Z3::Ast, and if you add an int to a bool, and get a segfault, tough luck.

I always keep track of what's the type of which expression.

Access to C pointers

In his version, he does this:

def to_unsafe
  @raw
end

Which he then uses like this:

protected def unsafe_ast_args(a : Ast, b : Ast)
  [a.to_unsafe, b.to_unsafe] of LibZ3::Ast
end

In mine it's this, without any further wrappers:

protected def _expr
  @expr
end

Should I be using protected def to_unsafe? I'm not sure about conventions here.

Story so far

All the code is in crystal-z3 repo, but there's no new code for this episode.

Overall our approaches were very similar considering we did it completely independently. Especially with libz3.cr.

One thing I definitely need to do is the out argument. I guess I could try to move LibZ3 out of Z3 namespace if it doesn't cause any issues. I'm not sure about to_unsafe.

I definitely want to keep track of everything's sorts at all times. It looks like supporting multiple contexts might be less of a problem than I expected, but I'm not terribly keen to do this, at least for now.

Coming next

In the next episode I'll get back to adding the tests.

Ruby