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 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.