Tomasz Wegrzanowski
Posted on March 6, 2022
It's a small change - in addition to Bool and Int sort to also support Reals.
The difficulty is that Z3 Reals are mathematical objects, and don't map to any Crystal number type. Crystal rationals and Crystal floats can represent some of them, but not all. Like square root of 2 for a simple example, is not representable in any way.
So for now it's possible to get numbers into Z3, but no good way to get them out - .to_s will only print rationals nicely. At some point I'd like to figure out some ways to extract real numbers (up to some specific precision) from Z3.
#to_unsafe
The library has a lot of calls to ._expr. It turns out that renaming it to .to_unsafe lets me avoid all most of these conversions.
Before:
def ==(other)
BoolExpr.new API.mk_eq(@expr, sort[other]._expr)
end
After:
def ==(other)
BoolExpr.new API.mk_eq(self, sort[other])
end
RealExpr spec
Nothing too surprising here:
require "./spec_helper"
describe Z3::RealExpr do
a = Z3.real("a")
b = Z3.real("b")
c = Z3.real("c")
x = Z3.bool("x")
it "+" do
[a == 2, b == 4, c == a + b].should have_solution({c => 6})
[a == BigRational.new(1,3), b == BigRational.new(3,2), c == a + b].should have_solution({c => "11/6"})
end
it "-" do
[a == 2, b == 4, c == a - b].should have_solution({c => -2})
end
it "*" do
[a == 2, b == 4, c == a * b].should have_solution({c => 8})
end
it "/" do
[a == 10, b == 3, c == a / b].should have_solution({c => "10/3"})
[a == -10, b == 3, c == a / b].should have_solution({c => "-10/3"})
[a == 10, b == -3, c == a / b].should have_solution({c => "-10/3"})
[a == -10, b == -3, c == a / b].should have_solution({c => "10/3"})
end
it "==" do
[a == 2, b == 2, x == (a == b)].should have_solution({x => true})
[a == 2, b == 3, x == (a == b)].should have_solution({x => false})
end
it "!=" do
[a == 2, b == 2, x == (a != b)].should have_solution({x => false})
[a == 2, b == 3, x == (a != b)].should have_solution({x => true})
end
it ">" do
[a == 3, b == 2, x == (a > b)].should have_solution({x => true})
[a == 2, b == 2, x == (a > b)].should have_solution({x => false})
[a == 1, b == 2, x == (a > b)].should have_solution({x => false})
end
it ">=" do
[a == 3, b == 2, x == (a >= b)].should have_solution({x => true})
[a == 2, b == 2, x == (a >= b)].should have_solution({x => true})
[a == 1, b == 2, x == (a >= b)].should have_solution({x => false})
end
it "<" do
[a == 3, b == 2, x == (a < b)].should have_solution({x => false})
[a == 2, b == 2, x == (a < b)].should have_solution({x => false})
[a == 1, b == 2, x == (a < b)].should have_solution({x => true})
end
it "<=" do
[a == 3, b == 2, x == (a <= b)].should have_solution({x => false})
[a == 2, b == 2, x == (a <= b)].should have_solution({x => true})
[a == 1, b == 2, x == (a <= b)].should have_solution({x => true})
end
it "**" do
[a == 3, b == 4, c == (a ** b)].should have_solution({c => 81})
[a == 81, b == 0.25, c == (a ** b)].should have_solution({c => 3})
end
it "unary -" do
[a == 3, b == -a].should have_solution({b => -3})
[a == 0, b == -a].should have_solution({b => 0})
[a == 3.5, b == -a].should have_solution({b => "-7/2"})
[a == BigRational.new(4, 3), b == -a].should have_solution({b => "-4/3"})
end
# Many expressions will not convert to a rational with .simplify
# Then you get a complex S-expression
# We need to add some way to extract that
it "to_s" do
Z3.real(7).to_s.should eq("7")
Z3.real(-7).to_s.should eq("-7")
(Z3.real(10) / Z3.real(3)).simplify.to_s.should eq("10/3")
(Z3.real(-10) / Z3.real(3)).simplify.to_s.should eq("-10/3")
end
end
Story so far
All the episode code is in this repo.
No new problems this episode, and we even cleaned up some old code.
Coming next
In the next episodes we'll see about adding bit vector sorts. This will require some API changes, as that's a different sort for every bit width.
Posted on March 6, 2022
Join Our Newsletter. No Spam, Only the good stuff.
Sign up to receive the latest update from our blog.