DEV Community

Tomasz Wegrzanowski
Tomasz Wegrzanowski

Posted on

Open Source Adventures: Episode 08: Extending Crystal Z3 for Booleans

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:

def mk_power(a, b)
  LibZ3.mk_power(Context, a, b)
end
Enter fullscreen mode Exit fullscreen mode

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:

fun mk_true = Z3_mk_true(ctx : Context) : Ast
Enter fullscreen mode Exit fullscreen mode

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

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
Enter fullscreen mode Exit fullscreen mode

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

Bool types

I tried to do this, Haskell style:

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

    def self.[](false)
      BoolExpr.new API.mk_false
    end
Enter fullscreen mode Exit fullscreen mode

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:

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

    def self.[](b : FalseClass)
      BoolExpr.new API.mk_false
    end
Enter fullscreen mode Exit fullscreen mode

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

module Z3
  class BoolSort
    def self.[](t : Bool)
      if t
        BoolExpr.new API.mk_true
      else
        BoolExpr.new API.mk_false
      end
    end
Enter fullscreen mode Exit fullscreen mode

! 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:

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
Enter fullscreen mode Exit fullscreen mode

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:

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
Enter fullscreen mode Exit fullscreen mode

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.

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
Enter fullscreen mode Exit fullscreen mode

New Int Functionality

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

  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
Enter fullscreen mode Exit fullscreen mode

Bool Spec

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

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
Enter fullscreen mode Exit fullscreen mode

Story so far

All the episode code is in this repo.

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.

Top comments (0)