Tomasz Węgrzanowski's Blog

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

Tomasz Węgrzanowski's photo
Tomasz Węgrzanowski
·

6 min read

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

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

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)

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

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

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

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

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)

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)

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)

$ ./send_more_money2.cr
Result code is: True
d -> 7
n -> 6
o -> 0
m -> 1
r -> 8
s -> 9
e -> 5
y -> 2

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.

Ruby