DEV Community

Tomasz Wegrzanowski
Tomasz Wegrzanowski

Posted on

Open Source Adventures: Episode 02: Hiding Low Level Concerns for Crystal Z3

#ruby #crystal #z3

In the previous episode we got Crystal working with Z3, but it was following low level C API directly.

In this episode we'll layer the problem:

  • first we'll have very low level API that corresponds directly to C functions - following convention I've seen in some similar projects, I renamed it to LibZ3
  • then there's second layer, nicer API that hides a lot of the low level details, Z3
  • and finally the actual program

As the distance between LibZ3 and good API is quite big, I want to add another layer to this layer cake later.

LibZ3

There's just two things I changed - renamed it to LibZ3, and introduced LBool enum. As Z3 deals with problems that are possibly unsolvable, it sometimes needs to return 3-valued answer (yes, no, and can't decide). Interestingly many results that used to be unknown in older Z3 versions then become decidable in newer versions.

@[Link("z3")]
lib LibZ3
  type Ast = Void*
  type Config = Void*
  type Context = Void*
  type Model = Void*
  type Solver = Void*
  type Sort = Void*
  type Symbol = Void*

  enum LBool : Int32
    False = -1
    Undefined = 0
    True = 1
  end

  # Just list the ones we need, there's about 700 API calls total
  fun mk_add = Z3_mk_add(ctx : Context, count : UInt32, asts : Ast*) : Ast
  fun mk_const = Z3_mk_const(ctx : Context, name : Symbol, sort : Sort) : Ast
  fun mk_context = Z3_mk_context(cfg : Config) : Context
  fun mk_config = Z3_mk_config() : Config
  fun mk_eq = Z3_mk_eq(ctx : Context, a : Ast, b : Ast) : Ast
  fun mk_ge = Z3_mk_ge(ctx : Context, a : Ast, b : Ast) : Ast
  fun mk_gt = Z3_mk_gt(ctx : Context, a : Ast, b : Ast) : Ast
  fun mk_int_sort = Z3_mk_int_sort(ctx : Context) : Sort
  fun mk_le = Z3_mk_le(ctx : Context, a : Ast, b : Ast) : Ast
  fun mk_lt = Z3_mk_lt(ctx : Context, a : Ast, b : Ast) : Ast
  fun mk_distinct = Z3_mk_distinct(ctx : Context, count : UInt32, asts : Ast*) : Ast
  fun mk_mul = Z3_mk_mul(ctx : Context, count : UInt32, asts : Ast*) : Ast
  fun mk_numeral = Z3_mk_numeral(ctx : Context, s : UInt8*, sort : Sort) : Ast
  fun mk_solver = Z3_mk_solver(ctx : Context) : Solver
  fun mk_string_symbol = Z3_mk_string_symbol(ctx : Context, s : UInt8*) : Symbol
  fun model_to_string = Z3_model_to_string(ctx : Context, model : Model) : UInt8*
  fun solver_assert = Z3_solver_assert(ctx : Context, solver : Solver, ast : Ast) : Void
  fun solver_check = Z3_solver_check(ctx : Context, solver : Solver) : LBool
  fun solver_get_model = Z3_solver_get_model(ctx : Context, solver : Solver) : Model
end
Enter fullscreen mode Exit fullscreen mode

The Next Layer 

module Z3
  extend self

  Context = LibZ3.mk_context(LibZ3.mk_config)
  IntSort = LibZ3.mk_int_sort(Context)

  def mk_solver
    LibZ3.mk_solver(Context)
  end

  def mk_numeral(num, sort=IntSort)
    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

  def mk_eq(a, b)
    LibZ3.mk_eq(Context, a, b)
  end

  def mk_ge(a, b)
    LibZ3.mk_ge(Context, a, b)
  end

  def mk_gt(a, b)
    LibZ3.mk_gt(Context, a, b)
  end

  def mk_le(a, b)
    LibZ3.mk_le(Context, a, b)
  end

  def mk_lt(a, b)
    LibZ3.mk_lt(Context, a, b)
  end

  def mk_add(asts)
    LibZ3.mk_add(Context, asts.size, asts)
  end

  def mk_mul(asts)
    LibZ3.mk_mul(Context, asts.size, asts)
  end

  def mk_distinct(asts)
    LibZ3.mk_distinct(Context, asts.size, asts)
  end

  def solver_assert(solver, ast)
    LibZ3.solver_assert(Context, solver, ast)
  end

  def solver_check(solver)
    LibZ3.solver_check(Context, solver)
  end

  def solver_get_model(solver)
    LibZ3.solver_get_model(Context, solver)
  end

  def model_to_string(model)
    String.new LibZ3.model_to_string(Context, model)
  end
end
Enter fullscreen mode Exit fullscreen mode

The next layer needs to make one decision - to support multiple contexts or not, and I won't do it, even though that has some legitimate uses, as that would drastically overcomplicate the API, and overwhelming majority of applications don't need that.

This whole code is very copy and paste, and there's about 700 such calls, so we'll eventually have to use macros, or some automated generation. In Ruby version I used automated generation, as that code is easier to unit tests with regexps than fancy metaprogramming.

I want to check how unit-testable Crystal macros are in some future episode, basically is there some kind of expect(somemacro(args)).to expand_to{ some code }?

There's also one quick hack here, with constant IntSort. Z3 has potentially infinite number of types, like N-bit bitvectors, various floating point numbers, and some much more exotic objects, and that adds a lot of complexity. We could just ignore this for now, and try to support integers and booleans only for now.

Crystal Limitations

There ary two Crystal-specific issues. First I'd really want some kind of one-line method definitions. It would be great if we could do something like this syntax Ruby 3 added:

  def mk_eq(a, b) = LibZ3.mk_eq(Context, a, b)
  def mk_ge(a, b) = LibZ3.mk_ge(Context, a, b)
  def mk_gt(a, b) = LibZ3.mk_gt(Context, a, b)
  def mk_le(a, b) = LibZ3.mk_le(Context, a, b)
  def mk_lt(a, b) = LibZ3.mk_lt(Context, a, b)
Enter fullscreen mode Exit fullscreen mode

There's been some discussion about adding that to Crystal too. Overall it's a purely syntactic issue, and while it would be nice, there's only so much syntax you can add before it conflicts with other syntax.

A much bigger issue is why we have to do this:

  def mk_distinct(asts)
    LibZ3.mk_distinct(Context, asts.size, asts)
  end
Enter fullscreen mode Exit fullscreen mode

Instead of the way we'd do it in Ruby:

  def mk_distinct(*asts)
    LibZ3.mk_distinct(Context, asts.size, asts)
  end
Enter fullscreen mode Exit fullscreen mode

I originally tried it the Ruby way, but Crystal just plain won't allow Z3.mk_distinct(*vars.values). If I try I get Error: argument to splat must be a tuple, not Array(LibZ3::Ast).

Without some workarounds, this will lead to an awkward APIs, as now every mk_add([...]) and mk_mul([...]) need extra [] inside. We'll get to possible workarounds in a future episode.

Solution Code

First we setup Solver and some variables:

# Setup library
solver = Z3.mk_solver

# Integer constants
nums = Hash(Int32, LibZ3::Ast).new
[0, 1, 9, 10, 100, 1000, 10000].each do |num|
  nums[num] = Z3.mk_numeral(num)
end

# Variables, all 0 to 9
vars = Hash(String, LibZ3::Ast).new
%w[s e n d m o r e m o n e y].uniq.each do |name|
  var = Z3.mk_const(name, Z3::IntSort)
  vars[name] = var
  Z3.solver_assert(solver, Z3.mk_ge(var, nums[0]))
  Z3.solver_assert(solver, Z3.mk_le(var, nums[9]))
end

# m and s need to be >= 1, no leading zeroes
Z3.solver_assert(solver, Z3.mk_ge(vars["m"], nums[1]))
Z3.solver_assert(solver, Z3.mk_ge(vars["s"], nums[1]))

# all letters represent different digits
Z3.solver_assert(solver, Z3.mk_distinct(vars.values))
Enter fullscreen mode Exit fullscreen mode

Not having to deal with the contex deinitely cleans up this code.

The following code with adds and muls and their extra [] is not amazing:

# SEND + MORE = MONEY
send_sum = Z3.mk_add([
  Z3.mk_mul([vars["s"], nums[1000]]),
  Z3.mk_mul([vars["e"], nums[100]]),
  Z3.mk_mul([vars["n"], nums[10]]),
  vars["d"],
])

more_sum = Z3.mk_add([
  Z3.mk_mul([vars["m"], nums[1000]]),
  Z3.mk_mul([vars["o"], nums[100]]),
  Z3.mk_mul([vars["r"], nums[10]]),
  vars["e"],
])

money_sum = Z3.mk_add([
  Z3.mk_mul([vars["m"], nums[10000]]),
  Z3.mk_mul([vars["o"], nums[1000]]),
  Z3.mk_mul([vars["n"], nums[100]]),
  Z3.mk_mul([vars["e"], nums[10]]),
  vars["y"],
])

equation = Z3.mk_eq(Z3.mk_add([send_sum, more_sum]), money_sum)
Z3.solver_assert(solver, equation)
Enter fullscreen mode Exit fullscreen mode

To be fair, it's no big deal, as the end goal is saying something more like this:

send_sum = Z3.Int("s") * 1000 + Z3.Int("e") * 100 + Z3.Int("n") * 10 + Z3.Int("d")
more_sum = Z3.Int("m") * 1000 + Z3.Int("o") * 100 + Z3.Int("r") * 10 + Z3.Int("e")
money_sum = Z3.Int("m") * 10000 +  Z3.Int("o") * 1000 + Z3.Int("n") * 100 + Z3.Int("e") * 10 + Z3.Int("y")
solver.assert(send_sum + more_sum == money_sum)
Enter fullscreen mode Exit fullscreen mode

Which won't have any []s anyway, as it will be using operators.

And finally we print the result. As it's enum now not a number, it prints nicely without us doing anything:

# Get the result
result_code = Z3.solver_check(solver)
puts "Result code is: #{result_code}"

model = Z3.solver_get_model(solver)
puts Z3.model_to_string(model)
Enter fullscreen mode Exit fullscreen mode 
$ ./send_more_money2.cr
Result code is: True
d -> 7
n -> 6
o -> 0
m -> 1
r -> 8
s -> 9
e -> 5
y -> 2
Enter fullscreen mode Exit fullscreen mode

Story so far

All the code is in crystal-z3 repo.

We got closer to something usable, but the API is both incomplete and inconvenient.

Coming next

In the next episode we'll try to create nice operator-based API for limited subset of Z3 with just booleans and integers.

Latest comments (3)

Collapse
 
asterite profile image
Ary Borenszweig •

Thank you for these posts! Having someone use Crystal and document their experience and things we need to improve is always welcome.

Regarding the tuple to array thing... I was wondering if you could define a method mk_distinct(*asts) like in Ruby, and then turn that into an Array before passing it to C:

def mk_distinct(*asts)
  LibZ3.mk_distinct(Context, asts.size, asts.to_a)
end
Enter fullscreen mode Exit fullscreen mode

I think that should work. And if you wanted to support arrays too you would need to add another overload, which isn't ideal but it works too:

def mk_distinct(asts : Array)
  LibZ3.mk_distinct(Context, asts.size, asts)
end

# Then the other overload could be:
def mk_distinct(*asts)
  mk_distinct(asts.to_a)
end
Enter fullscreen mode Exit fullscreen mode

That said, I'm now thinking that maybe tuples should be implicitly convertible to C. That's done with the to_unsafe method, similar to how there's a to_unsafe method in Array.

Collapse
 
asterite profile image
Ary Borenszweig •

Nevermind, there's no way to implement Tuple#to_unsafe, but maybe the approach above is acceptable (especially because you will also be able to generate these definitions using macros)

Collapse
 
taw profile image
Tomasz Wegrzanowski •

I think overloads would work fine for this specific case, as it's either tuple of Asts or one Array(Ast), so there's no ambiguity. I expect to run into much worse problems soon enough.

Read next

kavindukarunasena profile image

ngFor in Angular

Kavindu Karunasena -

paulike profile image

Programming languages

Paul Ngugi -

zaidbari profile image

Maximizing Web Performance: A Comprehensive Guide

Zaid Bari -

paulike profile image

Computer Basics

Paul Ngugi -