Open Source Adventures: Episode 71: Improving Crystal Z3 Shard
Tags: crystal, z3
Published: 2022-07-09 00:00:12

While writing various puzzle game solvers in Crystal Z3 I discovered two big issues:

* I frequently needed `.reduce` chains of `+`/`*`/`and`/`or` with special case for empty arrays
* `Model#[]` returned untyped result (`Expr`) even though its exact type is statically known, so extracting data from the model requires going `#to_s`

### `Z3.distinct`

It was already there, just without a spec:

```crystal
  it "Z3.distinct" do
    [
      2 >= a,
      a >= b,
      b >= c,
      c >= 0,
      Z3.distinct([a, b, c]),
    ].should have_solution({
      a => 2,
      b => 1,
      c => 0
    })
  end
```

### `Z3.add` and `Z3.mul`

Here's implementation:

```crystal
  def Z3.add(args : Array(IntExpr | Int))
    if args.empty?
      IntSort[0]
    else
      IntExpr.new API.mk_add(args.map{|a| IntSort[a]})
    end
  end

  def Z3.mul(args : Array(IntExpr | Int))
    if args.empty?
      IntSort[1]
    else
      IntExpr.new API.mk_mul(args.map{|a| IntSort[a]})
    end
  end
```

And the spec:

```crystal
  it "Z3.add" do
    [
      a == 10,
      b == 20,
      c == Z3.add([a, 30, b])
    ].should have_solution({
      c => 60,
    })
    [
      a == Z3.add([] of Z3::IntExpr),
    ].should have_solution({
      a => 0,
    })
    [
      a == Z3.add([b]),
      b == 10,
    ].should have_solution({
      a => 10,
    })
    [
      a == Z3.add([10]),
    ].should have_solution({
      a => 10,
    })
  end

  it "Z3.mul" do
    [
      a == 10,
      b == 20,
      c == Z3.mul([a, 30, b])
    ].should have_solution({
      c => 6000,
    })
    [
      a == Z3.mul([] of Z3::IntExpr),
    ].should have_solution({
      a => 1,
    })
    [
      a == Z3.mul([b]),
      b == 10,
    ].should have_solution({
      a => 10,
    })
    [
      a == Z3.mul([10]),
    ].should have_solution({
      a => 10,
    })
  end
```

These could also be defined for bitvectors and reals.

### `Z3.and` and `Z3.or`

And similar methods for `Z3.and` and `Z3.or`, except in this case we don't need to special case empty arrays, and Z3 library does it for us.

```crystal
  def Z3.and(args : Array(BoolExpr | Bool))
    BoolExpr.new API.mk_and(args.map{|a| BoolSort[a]})
  end

  def Z3.or(args : Array(BoolExpr | Bool))
    BoolExpr.new API.mk_or(args.map{|a| BoolSort[a]})
  end
```

And the specs:

```crystal
  it "Z3.or" do
    [a == Z3.or([] of Z3::BoolExpr)].should have_solution({a => false})
    [a == Z3.or([true, false])].should have_solution({a => true})
    [a == Z3.or([false, false])].should have_solution({a => false})
    [a == Z3.or([false, b]), b == false].should have_solution({a => false})
    [a == Z3.or([false, b]), b == true].should have_solution({a => true})
    [a == Z3.or([true, false, b]), b == true].should have_solution({a => true})
  end

  it "Z3.and" do
    [a == Z3.and([] of Z3::BoolExpr)].should have_solution({a => true})
    [a == Z3.and([true, false])].should have_solution({a => false})
    [a == Z3.and([true, true])].should have_solution({a => true})
    [a == Z3.and([true, b]), b == false].should have_solution({a => false})
    [a == Z3.and([true, b]), b == true].should have_solution({a => true})
    [a == Z3.and([true, false, b]), b == true].should have_solution({a => false})
  end
```

These could also be defined for bitvectors.

### `Model#[]`

The second issue is having `Model#[]` return correctly typed result. Z3 API has only one call, and in Ruby we really don't need to do this. It's guaranteed to return correct type.

However in Crystal, we need to tell the type system about it. For this we can use this macro:

```crystal
  {% for type in %w[BoolExpr IntExpr BitvecExpr RealExpr] %}
    def eval(expr : {{type.id}}, complete=false)
      result = API.model_eval(self, expr, complete)
      raise Z3::Exception.new("Incorrect type returned") unless result.is_a?({{type.id}})
      result
    end
  {% end %}

  def [](expr)
    eval(expr, true)
  end
```

And here's the spec:

```crystal
require "./spec_helper"

describe Z3::Model do
  a = Z3.bool("a")
  b = Z3.bool("b")
  c = Z3.int("c")
  d = Z3.int("d")
  e = Z3.bitvec("e", 16)
  f = Z3.bitvec("f", 16)
  g = Z3.real("g")
  h = Z3.real("h")

  it "eval boolean" do
    solver = Z3::Solver.new
    solver.assert a == true
    model = solver.model
    model.eval(a).to_s.should eq("true")
    model.eval(b).to_s.should eq("b")
    model.eval(a).to_b.should eq(true)
    expect_raises(Z3::Exception) { model.eval(b).to_b }
  end

  it "[] boolean" do
    solver = Z3::Solver.new
    solver.assert a == true
    model = solver.model
    model[a].to_s.should eq("true")
    model[b].to_s.should eq("false")
    model[a].to_b.should eq(true)
    model[b].to_b.should eq(false)
  end

  it "eval integer" do
    solver = Z3::Solver.new
    solver.assert c == 42
    model = solver.model
    model.eval(c).to_s.should eq("42")
    model.eval(d).to_s.should eq("d")
    model.eval(c).to_i.should eq(42)
    expect_raises(Z3::Exception) { model.eval(d).to_i }
  end

  it "[] integer" do
    solver = Z3::Solver.new
    solver.assert c == 42
    model = solver.model
    model[c].to_s.should eq("42")
    model[d].to_s.should eq("0")
    model[c].to_i.should eq(42)
    model[d].to_i.should eq(0)
  end

  it "eval bit vector" do
    solver = Z3::Solver.new
    solver.assert e == 42
    model = solver.model
    model.eval(e).to_s.should eq("42")
    model.eval(f).to_s.should eq("f")
    model.eval(e).to_i.should eq(42)
    expect_raises(Z3::Exception) { model.eval(f).to_i }
  end

  it "[] bit vector" do
    solver = Z3::Solver.new
    solver.assert e == 42
    model = solver.model
    model[e].to_s.should eq("42")
    model[f].to_s.should eq("0")
    model[e].to_i.should eq(42)
    model[f].to_i.should eq(0)
  end

  it "eval real" do
    solver = Z3::Solver.new
    solver.assert g == 3.5
    model = solver.model
    model.eval(g).to_s.should eq("7/2")
    model.eval(h).to_s.should eq("h")
  end

  it "[] real" do
    solver = Z3::Solver.new
    solver.assert g == 3.5
    model = solver.model
    model[g].to_s.should eq("7/2")
    model[h].to_s.should eq("0")
  end
end
```

For Z3 reals I didn't provide any `#to_f`, `#to_rat` or such, as that's actually quite complicated, and it's not a very common type, so for now you'll need to parse `#to_s` (or PR extra methods).

### Story so far

[Updated shard is in](https://github.com/taw/crystal-z3).

### Coming next

Over the next few episodes I'll code a few more puzzle game solvers in Crystal and Z3.