DEV Community

Tomasz Wegrzanowski
Tomasz Wegrzanowski

Posted on

3 1

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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.

Billboard image

The Next Generation Developer Platform

Coherence is the first Platform-as-a-Service you can control. Unlike "black-box" platforms that are opinionated about the infra you can deploy, Coherence is powered by CNC, the open-source IaC framework, which offers limitless customization.

Learn more

Top comments (0)

A Workflow Copilot. Tailored to You.

Pieces.app image

Our desktop app, with its intelligent copilot, streamlines coding by generating snippets, extracting code from screenshots, and accelerating problem-solving.

Read the docs

👋 Kindness is contagious

Discover a treasure trove of wisdom within this insightful piece, highly respected in the nurturing DEV Community enviroment. Developers, whether novice or expert, are encouraged to participate and add to our shared knowledge basin.

A simple "thank you" can illuminate someone's day. Express your appreciation in the comments section!

On DEV, sharing ideas smoothens our journey and strengthens our community ties. Learn something useful? Offering a quick thanks to the author is deeply appreciated.

Okay