Open Source Adventures: Episode 09: Data Extraction Support for Crystal Z3
Tags: crystal, ruby, z3
Published: 2022-03-05 21:54:41

There's a lot of minor missing functionality I want before I publish the shard. These aren't really related, but I wanted to do them all.

### Get version

`Z3.version` should return version number of the Z3 library (not of the Crystal shard).

It's a simple method, but it has interesting implementation:

```ruby
fun get_version = Z3_get_version(v0 : UInt32*, v1 : UInt32*, v2 : UInt32*, v3 : UInt32*) : Void

def Z3.version
  LibZ3.get_version(out v0, out v1, out v2, out v3)
  [v0, v1, v2, v3].join(".")
end
```

Or is there some kind of `Version` object in Crystal, like [Gem::Version in Ruby](https://ruby-doc.org/stdlib-3.0.0/libdoc/rubygems/rdoc/Gem/Version.html)?

This is quite important, as Z3 changes in small ways between versions, and I had to gate some specs behind version checks.

### `Z3::Exception`

We're throwing a lot of exceptions, so we should wrap them in a nice class. There's no special functionality here, but specs saying `expect{ ... }.to raise_error` without giving error class or message regexp are really fragile.

### Conversion functions

We want these to be available for `Int`s:

```ruby
it "const?" do
  Z3::IntSort[5].const?.should be_true
  Z3::IntSort[-5].const?.should be_true
  (Z3::IntSort[5] + Z3::IntSort[5]).const?.should be_false
  a.const?.should be_false
  (a + b).const?.should be_false
end

it "to_i" do
  Z3::IntSort[5].to_i.should eq(5)
  Z3::IntSort[-10].to_i.should eq(-10)
  (Z3::IntSort[2] + Z3::IntSort[2]).to_i.should eq(4)
  expect_raises(Z3::Exception){ a.to_i }
  expect_raises(Z3::Exception){ (a + b).to_i }
end
```

And these for `Bool`s:

```ruby
it "const?" do
  Z3::BoolSort[true].const?.should be_true
  Z3::BoolSort[false].const?.should be_true
  (Z3::BoolSort[true] | Z3::BoolSort[false]).const?.should be_false
  a.const?.should be_false
  (a | b).const?.should be_false
end

it "to_b" do
  Z3::BoolSort[true].to_b.should eq(true)
  Z3::BoolSort[false].to_b.should eq(false)
  (Z3::BoolSort[true] | Z3::BoolSort[false]).to_b.should eq(true)
  expect_raises(Z3::Exception) { a.to_b }
  expect_raises(Z3::Exception) { (a | b).to_b }
end
```

Notably I want `to_i` and `to_b` to work not just for constants, but also for anything that simplifies to one, as that avoids some stupid edge cases with how Z3 represents negative numbers etc.

### `API.new_from_ast_pointer`

```ruby
def new_from_ast_pointer(_ast)
  _sort = LibZ3.get_sort(Context, _ast)
  sort_kind = LibZ3.get_sort_kind(Context, _sort)
  case sort_kind
  when LibZ3::SortKind::Bool
    BoolExpr.new(_ast)
  when LibZ3::SortKind::Int
    IntExpr.new(_ast)
  else
    raise "Unsupported sort kind #{sort_kind}"
  end
end
```

This probably should go on `AST` or `Expr` abstract class, but there is no such base class yet.

We construct most of our ASTs, and we keep track of what's their sorts, but sometimes we get one from Z3, like Model evaluation results, and then we need to figure out what's its type.

And this means we can get Model to return proper objects, not `String`s.

One problem with this interface is that `Model[]` returns `BoolExpr | IntExpr` (and it will return a much bigger union), even though it's guaranteed to always return something of the same sort as its argument. It's something to sort out eventually.

This change from returning `Strings` to returning `Expr` objects required zero changes in specs, as they `.to_s` everything anyway. One side effect of Z3 overloading `==`, is that specs cannot check for equality of two Z3 objects easily, so they basically do `a.to_s == b.to_s` (wrapped in a custom matcher).

### Integration tests

Unit tests get us only so far, so here's some integration tests:

```ruby
describe "Integration Tests" do
  it "Sudoku" do
    actual = `./examples/sudoku.cr`
    expected = File.read("#{__DIR__}/integration/sudoku.txt")
    actual.should eq(expected)
  end

  it "SEND + MORE = MONEY" do
    actual = `./examples/send_more_money.cr`
    expected = File.read("#{__DIR__}/integration/send_more_money.txt")
    actual.should eq(expected)
  end
end
```

As I wrote a lot of Ruby Z3 solver examples, and I want to port them to Crystal anyway, these are almost free integration tests.

One small problem with my Ruby Z3 integration test set is that many solvers have multiple (often trivially different) solutions, and different versions will change the answer. I'll try to avoid any such solvers for Crystal version.

### Story so far

[All the episode code is in this repo](https://github.com/taw/open-source-adventures).

The library is progressing quite nicely.

### Coming next

In the next episodes we'll see about adding additional sorts. This will require some API changes.