Open Source Adventures: Episode 09: Data Extraction Support for Crystal Z3

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:

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?

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 Ints:

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 Bools:

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

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 Strings.

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:

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.

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.

Comments

[Ary Borenszweig]

Nice post as usual!

For the version, there's a SemanticVersion type in the standard library. For some reason I can't paste links from my cellphone here, no idea why.

[Tomasz Wegrzanowski]

SemanticVersion supports 3 ints, and Z3 uses 4 ints, so that won't work.

[Ary Borenszweig]

It's true. The type in the standard library supports 3 ints plus optional prerelease and build strings. Maybe the last int can be turned into a string and used as prerelease or build. But in any case it's probably a minor thing.