## DEV Community

Tomasz Wegrzanowski

Posted on

# Open Source Adventures: Episode 10: Real Numbers supports for Crystal Z3

It's a small change - in addition to `Bool` and `Int` sort to also support `Real`s.

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

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.