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

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.

Comments

[Ary Borenszweig]

Hi! The reason Brian used to_unsafe is because that method is implicitly called when you pass something to C and the type doesn't match: crystal-lang.org/reference/1.3/syn...

So in your case if you define a to_unsafe for Z3::IntExpr that returns @expr, you could replace this:

    def ==(other)
      BoolExpr.new API.mk_eq(@expr, sort[other]._expr)
    end

with this:

    def ==(other)
      BoolExpr.new API.mk_eq(self, sort[other])
    end

which might be nicer to read/write, depending on personal taste.

[Tomasz Wegrzanowski]

Is it true even if I mark to_unsafe as protected?

To be honest if users call something called to_unsafe they only have themselves to blame. I just didn't want it to be called expr as that might encourage segfault-prone code.

[Ary Borenszweig]

Hm, good point. Apparently it doesn't work if to_unsafe is protected or private, but I think it should. I'll ask to change that.

[Brian J. Cardiff]

Wow. I didn't think mine deserves that attention. I am happy it helped you learn some bit of Crystal.

I didn't put a lot of thought on the organization. I was more eager to make some experiments with Z3.

Definitely +1 for namespaces and your approach of safer expressions.

Mapping two different worlds it definitely deserves attention and design. I have experimented on bring together Tcl/Tk, Cocoa, Prolog, Z3 with Crystal. All of them has some notion of types or ast that are usually represented by an opaque pointer yet not everything can be combined together. Since these experiments were not aimed to be consumed they lack some attention to the design.

I am very happy there is another person willing to play with Z3 and Crystal. This series made my week 💙

Your repo is more about a log of this series. Let me know if you are interested in maintaining a shard of this. If not, maybe in the future I could grab some of the ideas you present here. But I am happy to collaborate in this regard and make Z3/SMT more approachable for Crystallers.

[Tomasz Wegrzanowski]

Yeah, the repo is just a log right now, I wasn't really sure if it's going to work out, or crash and burn. I think I'll move the per-episode code to another repo, and use crystal-z3 for a proper shard.