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.
Top comments (3)
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.
SemanticVersion supports 3 ints, and Z3 uses 4 ints, so that won't work.
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.