While writing various puzzle game solvers in Crystal Z3 I discovered two big issues:
- I frequently needed
.reducechains of+/*/and/orwith 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
Coming next
Over the next few episodes I'll code a few more puzzle game solvers in Crystal and Z3.
Top comments (0)