Open Source Adventures: Episode 71: Improving Crystal Z3 Shard

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:

  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:

  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:

  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.

  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:

  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:

  {% 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:

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.

Coming next

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