Open Source Adventures: Episode 08: Extending Crystal Z3 for Booleans
Tags: crystal, ruby, z3
Published: 2022-03-05 14:22:34

It's time to extend API supported by Crystal Z3, but first we need to deal with all the copypasta in `z3/api.cr`. It already has so many definitions like this:

```ruby
def mk_power(a, b)
  LibZ3.mk_power(Context, a, b)
end
```

And we really would rather not add 700 more. Booleans are straightforward to add. Reals and BitVectors will need some API changes, so I'll leave them for later.

There's a lot of code changes, so here's just the highlights.

### VSCode Crystal extension isssue

A small annoyance with the extension is that it really thinks that code after `fun` snhould be indented:

```ruby
fun mk_true = Z3_mk_true(ctx : Context) : Ast
```

If you copy and paste it a few times, here's how it's going to format it:

```ruby
fun mk_true = Z3_mk_true(ctx : Context) : Ast
  fun mk_true = Z3_mk_true(ctx : Context) : Ast
    fun mk_true = Z3_mk_true(ctx : Context) : Ast
      fun mk_true = Z3_mk_true(ctx : Context) : Ast
        fun mk_true = Z3_mk_true(ctx : Context) : Ast
          fun mk_true = Z3_mk_true(ctx : Context) : Ast
```

I didn't encounter any other issues, but worth fixing this one.

### Bool types

I tried to do this, Haskell style:

```ruby
module Z3
  class BoolSort
    def self.[](true)
      BoolExpr.new API.mk_true
    end

    def self.[](false)
      BoolExpr.new API.mk_false
    end
```

It feels like it should work, but I'm getting `Error: cannot use 'true' as a parameter name`.

I can't do this either, as there's no `TrueClass` and `FalseClass` in Crystal:

```ruby
module Z3
  class BoolSort
    def self.[](b : TrueClass)
      BoolExpr.new API.mk_true
    end

    def self.[](b : FalseClass)
      BoolExpr.new API.mk_false
    end
```

I can do this, but it looks a lot less elegant:

```ruby
module Z3
  class BoolSort
    def self.[](t : Bool)
      if t
        BoolExpr.new API.mk_true
      else
        BoolExpr.new API.mk_false
      end
    end
```

### ! pseudo-method

Ruby and Crystal both allow redefining operators, but in both cases some are hardcoded. Notably `&&`, `||`, `and`, `or`, `?:` are all hardcoded, as they're really control structures and cannot be implemented as methods using normal semantics of evaluating arguments first.

This makes the Z3 API a bit awkward, as it needs to do `(a >= 0) & (a <= 9)` instead of more natural0 `a >= 0 && a <= 9` - and due to different operator precedence that requires extra parentheses.

Anyway, there's one difference in what's supported. Crystal doesn't support overloading `!`, while Ruby does. Interestingly, Ruby 1.x also did not support overloading `!`.

In principle, there's no reason why it shouldn't be supported. `!` uses standard evaluation order.

Anyway, Crystal Z3 will have to use `~` for boolean negation, not `!`. Ruby Z3 supports both as aliases.

### `.ite` type inference problem

`.ite` (if-then-else) is Z3 equivalent of `?:` operator.

You can pass whatever you want to it, as long as both arguments have the same sort. So `someBoolean.ite(anInt, anotherInt)` is valid, as it `someBoolean.ite(aBool, anotherBool)` etc.

This is fine, but we also want to be able to be able to pass regular constants without explilictly casting them, like `someBoolean.ite(anInt, 0)` or even `someBoolean.ite(10, 20)`.

So here's what I'd like to happen:

```ruby
def ite(a, b) : IntExpr
  IntExpr.new API.mk_ite(@expr, IntSort[a]._expr, IntSort[b]._expr)
end

def ite(a, b) : BoolExpr
  BoolExpr.new API.mk_ite(@expr, BoolSort[a]._expr, BoolSort[b]._expr)
end
```

If `a` and `b` are both of types that can survive `IntSort[]`, then use that definition. If they are of types that survive `BoolSort[]`, use that definition. Otherwise, type error.

I don't think Crystal can quite do this.

So instead I need to do this explicitly:

```ruby
def ite(a : (IntExpr | Int), b : (IntExpr | Int)) : IntExpr
  IntExpr.new API.mk_ite(@expr, IntSort[a]._expr, IntSort[b]._expr)
end

def ite(a : (BoolExpr | Bool), b : (BoolExpr | Bool)) : BoolExpr
  BoolExpr.new API.mk_ite(@expr, BoolSort[a]._expr, BoolSort[b]._expr)
end
```

And I'll need to add support for every new sort here.

There's another reason why what I want doesn't quite work, as in current api both accept `String` to mean a variable of given type, like `IntSort["a"]` and `BoolSort["a"]`, so `aBoolean.ite("a", "b")` would type check both ways in my original definition. This is not really intentional, but I'll need to do some tweaks to the API to support reals and bitvectors anyway, so I'll leave it for now.

### API macros

Here's `api.cr` with some very simple macros. Most methods just add `Context` argument. Some do other things like dealing with passing arrays, allocating strings etc., and that's also somewhat repetitive, but this is a lot less copypasta already.

```crystal
module Z3
  module API
    extend self

    Context = LibZ3.mk_context(LibZ3.mk_config)

    {% for name in %w[
      mk_div
      mk_eq
      mk_false
      mk_ge
      mk_gt
      mk_iff
      mk_implies
      mk_ite
      mk_le
      mk_lt
      mk_mod
      mk_not
      mk_power
      mk_rem
      mk_solver
      mk_true
      mk_unary_minus
      mk_xor
      simplify
      solver_assert
      solver_check
      solver_get_model
    ] %}
      def {{name.id}}(*args)
        LibZ3.{{name.id}}(Context, *args)
      end
    {% end %}

    {% for name in %w[
      mk_add
      mk_and
      mk_distinct
      mk_mul
      mk_or
      mk_sub
    ] %}
      def {{name.id}}(asts)
        LibZ3.{{name.id}}(Context, asts.size, asts)
      end
    {% end %}

    def mk_numeral(num : Int, sort)
      LibZ3.mk_numeral(Context, num.to_s, sort)
    end

    def mk_const(name, sort)
      name_sym = LibZ3.mk_string_symbol(Context, name)
      var = LibZ3.mk_const(Context, name_sym, sort)
    end

    # Not a real Z3 function
    def mk_ne(a, b)
      LibZ3.mk_distinct(Context, 2, [a, b])
    end

    def model_to_string(model)
      String.new LibZ3.model_to_string(Context, model)
    end

    def ast_to_string(ast)
      String.new LibZ3.ast_to_string(Context, ast)
    end

    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
  end
end
```

### New Int Functionality

I added one extra method `#simplify`. It's currently copy&pasted for every type:

```ruby
  it "simplify" do
    a = Z3::IntSort[5]
    b = Z3::IntSort[3]
    ((a+b).to_s).should eq("(+ 5 3)")
    ((a+b).simplify.to_s).should eq("8")
  end
```

### Bool Spec

Here's the spec for all the new Bool functionality:

```ruby
require "./spec_helper"

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

  it "&" do
    [a ==  true, b ==  true, c == (a & b)].should have_solution({c =>  true})
    [a ==  true, b == false, c == (a & b)].should have_solution({c => false})
    [a == false, b ==  true, c == (a & b)].should have_solution({c => false})
    [a == false, b == false, c == (a & b)].should have_solution({c => false})
  end

  it "|" do
    [a ==  true, b ==  true, c == (a | b)].should have_solution({c =>  true})
    [a ==  true, b == false, c == (a | b)].should have_solution({c =>  true})
    [a == false, b ==  true, c == (a | b)].should have_solution({c =>  true})
    [a == false, b == false, c == (a | b)].should have_solution({c => false})
  end

  it "^" do
    [a ==  true, b ==  true, c == (a ^ b)].should have_solution({c => false})
    [a ==  true, b == false, c == (a ^ b)].should have_solution({c =>  true})
    [a == false, b ==  true, c == (a ^ b)].should have_solution({c =>  true})
    [a == false, b == false, c == (a ^ b)].should have_solution({c => false})
  end

  it "!=" do
    [a ==  true, b ==  true, c == (a != b)].should have_solution({c => false})
    [a ==  true, b == false, c == (a != b)].should have_solution({c =>  true})
    [a == false, b ==  true, c == (a != b)].should have_solution({c =>  true})
    [a == false, b == false, c == (a != b)].should have_solution({c => false})
  end

  it "implies" do
    [a ==  true, b ==  true, c == a.implies(b)].should have_solution({c =>  true})
    [a ==  true, b == false, c == a.implies(b)].should have_solution({c => false})
    [a == false, b ==  true, c == a.implies(b)].should have_solution({c =>  true})
    [a == false, b == false, c == a.implies(b)].should have_solution({c =>  true})
  end

  it "iff" do
    [a ==  true, b ==  true, c == a.iff(b)].should have_solution({c =>  true})
    [a ==  true, b == false, c == a.iff(b)].should have_solution({c => false})
    [a == false, b ==  true, c == a.iff(b)].should have_solution({c => false})
    [a == false, b == false, c == a.iff(b)].should have_solution({c =>  true})
  end

  it "==" do
    [a ==  true, b ==  true, c == (a == b)].should have_solution({c =>  true})
    [a ==  true, b == false, c == (a == b)].should have_solution({c => false})
    [a == false, b ==  true, c == (a == b)].should have_solution({c => false})
    [a == false, b == false, c == (a == b)].should have_solution({c =>  true})
  end

  # ! not possible
  it "~" do
    [a ==  true, b == ~a].should have_solution({b => false})
    [a == false, b == ~a].should have_solution({b =>  true})
  end

  it "if then else" do
    [a ==  true, x == a.ite(2, 3)].should have_solution({x => 2})
    [a == false, x == a.ite(2, 3)].should have_solution({x => 3})
    [a == true,  b == a.ite(true, false)].should have_solution({b => true})
    [a == false, b == a.ite(true, false)].should have_solution({b => false})
    [a == true,  b == a.ite(false, true)].should have_solution({b => false})
    [a == false, b == a.ite(false, true)].should have_solution({b => true})
  end

  it "simplify" do
    a = Z3::BoolSort[true]
    b = Z3::BoolSort[false]
    ((a&b).to_s).should eq("(and true false)")
    ((a&b).simplify.to_s).should eq("false")
  end
end
```

### Story so far

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

We reached the point where abuot 80% of examples from my Ruby Z3 library could be ported to Crystal. The biggest missing piece is some way to extract data from the model better than stringifying the ASTs. Additional sorts like reals and bitvectors would be nice as well, and now that we can do it with less copy&pasting it should be easy enough.

### Coming next

In the next episodes we'll see about adding additional sorts, better ways to extract data from the model, and some integration tests. Then I'll turn this into a proper shard you'll be able to use.