Open Source Adventures: Episode 06: How my crystal-z3 compares with bcardiff's crystal-z3
Tags: crystal, ruby, z3
Published: 2022-03-03 21:15:58

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](https://github.com/bcardiff/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:

```ruby
@[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:

```ruby
@[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 `Context`s, while his version puts these methods on the `Context` object.

### Output arguments

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

```ruby
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:

```ruby
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:

```ruby
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:

```ruby
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](https://github.com/taw/crystal-z3), 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.