# 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
else
end
end

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

And the spec:

``````  it "Z3.add" do
[
a == 10,
b == 20,
].should have_solution({
c => 60,
})
[
].should have_solution({
a => 0,
})
[
b == 10,
].should have_solution({
a => 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(),
].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).

### Coming next

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