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.
Top comments (3)
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: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:
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 ato_unsafe
method in Array.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)I think overloads would work fine for this specific case, as it's either tuple of
Ast
s or oneArray(Ast)
, so there's no ambiguity. I expect to run into much worse problems soon enough.