Open Source Adventures: Episode 10: Real Numbers supports for Crystal Z3
Tags: ruby, crystal, z3
Published: 2022-03-06 17:23:33

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:

```ruby
def ==(other)
  BoolExpr.new API.mk_eq(@expr, sort[other]._expr)
end
```

After:

```ruby
def ==(other)
  BoolExpr.new API.mk_eq(self, sort[other])
end
```

### `RealExpr` spec

Nothing too surprising here:

```ruby
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](https://github.com/taw/open-source-adventures).

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.