Open Source Adventures: Episode 07: Specs For Crystal Z3
Tags: crystal, ruby, z3
Published: 2022-03-04 11:41:51

First, I decided to rearrange how code for this series is organized. [All the episode code will go to this repo](https://github.com/taw/open-source-adventures), and [crystal-z3 repo will be the place where the library is going to live once it's a bit more ready](https://github.com/taw/crystal-z3).

Anyway, time to add some specs, and fill in some missing operators.

### Specs in Crystal

In the Ruby gem I'm unit testing Z3 like this:

```ruby
module Z3
  describe IntExpr do
    let(:a) { Z3.Int("a") }
    let(:b) { Z3.Int("b") }
    let(:c) { Z3.Int("c") }
    let(:x) { Z3.Bool("x") }

    it "+" do
      expect([a == 2, b == 4, c == a + b]).to have_solution(c => 6)
    end

    it "-" do
      expect([a == 2, b == 4, c == a - b]).to have_solution(c => -2)
    end

    it "*" do
      expect([a == 2, b == 4, c == a * b]).to have_solution(c => 8)
    end

    ...
```

Crystal comes with builtin rspec-like test runner. I was confused by documentation, especially around two questions - what's equivalent of RSpec's `let`, and how can I do custom matchers?

I can suspend the `let` question for now. For Rails it's common to do very fancy `let` chains - where top of an example group defines a lot of defaults with `let`, then individual scenarios just override some of them. I only really needed to setup some variables.

I checked inside Crystal standard library for some examples, and they were full of macros, and not the most readable. There was [one custom matcher for BigInt](https://github.com/crystal-lang/crystal/blob/master/spec/std/big/big_int_spec.cr), and it was doing some `__FILE__`/`__LINE__` magic.

### `spec/spec_helper.rb`

After some digging in Crystal's source code, I managed to recreate custom expectation, positive case only:

```ruby
require "spec"

class SolutionExpectation(T)
  def initialize(@expected : Hash(T, String))
  end

  def setup_solver(asts)
    solver = Z3::Solver.new
    asts.each do |ast|
      solver.assert(ast)
    end
    solver
  end

  def match(asts)
    solver = setup_solver(asts)
    return false unless solver.satisfiable?
    model = solver.model
    @expected.each do |ast, expected_value|
      return false unless model[ast] == expected_value
    end
    true
  end

  def failure_message(asts)
    solver = setup_solver(asts)
    unless solver.satisfiable?
      return "Expected #{asts.inspect} to have a solution, but no solution was found"
    end
    model = solver.model
    "Solution found, but it does not match expectations:\n" +
    @expected.map do |ast, expected_value|
      "#{asts} (actual #{model[ast]}, expected #{expected_value})"
    end.join("\n")
  end
end

module Spec::Expectations
  def have_solution(solution)
    SolutionExpectation.new solution.transform_values(&.to_s)
  end
end
```

At first I tried to define it as `@expected : Hash(Z3::BoolExpr | Z3::IntExpr, String)`, but Crystal did not like that, saying it conflicts with me passing `@expected : Hash(Z3::IntExpr, String)` to it.

It looks like some subtyping variance issue, which are really infuriating. Notably TypeScript decided to just accept technically invalid types for such cases by default, as there's no sane way to do this fully correctly.

Crystal has more flexible type inference algorithm, so this could be fixable in principle. Anyway, I just avoided the whole problem using generics.

### `spec/int_spec.cr`

It's mostly based on Ruby version, but some functionality is still missing:


```ruby
require "./spec_helper"
require "../src/z3"

describe Z3::IntExpr do
  a = Z3.int("a")
  b = Z3.int("b")
  c = Z3.int("c")
  x = Z3.bool("x")

  it "+" do
    [a == 10, b == 20, c == a + b].should have_solution({c => 30})
    [a == 2, b == 10 + a].should have_solution({b => 12})
    [a == 2, b == a + 10].should have_solution({b => 12})
  end

  it "*" do
    [a == 10, b == 20, c == a * b].should have_solution({c => 200})
    [a == 2, b == 10 * a].should have_solution({b => 20})
    [a == 2, b == a * 10].should have_solution({b => 20})
  end

  it "-" do
    [a == 10, b == 20, c == a - b].should have_solution({c => 30})
    [a == 2, b == 10 - a].should have_solution({b => 12})
    [a == 2, b == a - 10].should have_solution({b => 12})
  end

  it "/" do
    [a ==  10, b ==  3, c == a / b].should have_solution({c =>  3})
    [a == -10, b ==  3, c == a / b].should have_solution({c => -4})
    [a ==  10, b == -3, c == a / b].should have_solution({c => -3})
    [a == -10, b == -3, c == a / b].should have_solution({c =>  4})
  end

  # Can't say these make much sense, but let's document what Z3 actually does
  it "rem" do
    [a ==  10, b ==  3, c == a.rem(b)].should have_solution({c => 10 -  3 *  3})
    [a == -10, b ==  3, c == a.rem(b)].should have_solution({c =>-10 -  3 * -4})
    [a ==  10, b == -3, c == a.rem(b)].should have_solution({c =>-( 10 - -3 * -3)})
    [a == -10, b == -3, c == a.rem(b)].should have_solution({c =>-(-10 - -3 *  4)})
  end

  it "mod" do
    [a ==  10, b ==  3, c == a.mod(b)].should have_solution({c => 1})
    [a ==  10, b == -3, c == a.mod(b)].should have_solution({c => 1})
    [a == -10, b ==  3, c == a.mod(b)].should have_solution({c => 2})
    [a == -10, b == -3, c == a.mod(b)].should have_solution({c => 2})
  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})
  end

  it "unary -" do
    [a == 3, b == -a].should have_solution({b => -3})
  end
end
```

Other than extra `{}`s, the syntax looks just fine.

### Some hacks

At some point we'll need to write `Ast#to_s`. Using one included with Z3 is not really sustainable, as it prints everything as Lisp expression. Most notably it prints negative numbers as Lisp expressions, so `-420` is returned as `(- 420)`, which is definitely not what we want.

For now I just hacked it a bit, here's `IntExpr`:

```ruby
# This is hacky as hell, we need our own printer as these are
# just Lisp-style S-expression and won't even handle negatives in a sensible way
# For example -4 is "(- 4)"
def to_s(io)
  s = API.ast_to_string(@expr)
  if s =~ /\A\(- (\d+)\)\z/
    s = "-#{$1}"
  end
  io << s
end
```

The same code is repeated in `Model` (which now uses `out` argument):

```ruby
def model_eval(model, ast, complete)
  result = LibZ3.model_eval(Context, model, ast, complete, out result_ast)
  raise "Cannot evaluate" unless result == true
  # Full conversion is complicated, this is a good start
  s = ast_to_string result_ast
  if s =~ /\A\(- (\d+)\)\z/
    s = "-#{$1}"
  end
  s
end
```

### Story so far

[All the episode code is in this repo](https://github.com/taw/open-source-adventures).

### Coming next

In the next episode I'll add support for boolean operations, and some integration tests.