Welcome to my new series! Previously I did Electron Adventures and 100 Languages Speedrun.
Now it's time for something a bit less ambitious. I do a lot of small Open Source things anyway all the time, so in this series I'll just write about the kind of things I do anyway.
I plan it as a more or less daily series of 100 episodes. They'll mostly be much smaller than in my 100 Languages Speedrun series, and any big topic will likely be split into multiple bite-size episodes. Some will be new stuff, some might be flashbacks to old things I made before.
Let's get started!
Z3 and Crystal
Z3 is a theorem prover library, and I maintain a Ruby gem for it. I wrote about it previously in 100 Languages Speedrun: Episode 23: Ruby Z3
.
I want to play with Crystal a bit more, and since I already know Z3, that's a decent start.
Z3 C API
Z3 C API is super unfun to work with. We need to create a Context object (passing a Config), then we need to pass that damn context to every single function call. Due to limitations of C there's some weird calling convention for anything that takes variable number of arguments or returns multiple values. And worst of all, there are so many ways to pass arguments that pass the C type system, but will still hard crash Z3 - like trying to add an integer expression (type Ast) to a boolean expression (also type Ast) for an obvious example, but there are many others.
The way I solved it in Ruby is by layers. First I created the Z3::VeryLowLevel which directly maps to the C API, with functions like these:
module Z3
module VeryLowLevel
attach_function :Z3_mk_gt, [:ctx_pointer, :ast_pointer, :ast_pointer], :ast_pointer
end
end
This means function Z3_mk_gt takes three arguments (Context, Ast, Ast), and returns one argument Ast.
Then there's second layer Z3::LowLevel which handles context, unwraps passed objects, and also handles peculiarities of C APIs like how arrays and multiple return values are handled:
module Z3
module LowLevel
def mk_gt(ast1, ast2) #=> :ast_pointer
VeryLowLevel.Z3_mk_gt(_ctx_pointer, ast1._ast, ast2._ast)
end
end
end
Only on top of that I built the actual API, which did all the crash-prevention checks, automatic coercion, operators, and so on:
module Z3
class Expr < AST
class << self
def Gt(a, b)
a, b = coerce_to_same_sort(a, b)
case a
when ArithExpr
BoolSort.new.new(LowLevel.mk_gt(a, b))
when BitvecExpr
raise Z3::Exception, "Use #signed_gt or #unsigned_gt for Bitvec, not >"
else
raise Z3::Exception, "Can't compare #{a.sort} values"
end
end
end
end
end
module Z3
class ArithExpr < Expr
def >(other)
Expr.Gt(self, other)
end
end
end
The end result is that you can do this:
> Z3.Int("a") > 420
Bool<a > 420>
Which does a lot of Z3 calls behind the scene.
Crystal FFI
OK, let's get started with doing this in Crystal. First, manually doing just enough of the very low level API to get started:
@[Link("z3")]
lib Z3
type Ast = Void*
type Config = Void*
type Context = Void*
type Model = Void*
type Solver = Void*
type Sort = Void*
type Symbol = Void*
# 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_contig = 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) : Int32
fun solver_get_model = Z3_solver_get_model(ctx : Context, solver : Solver) : Model
end
SEND + MORE = MONEY
And let's do a very simple problem, SEND + MORE = MONEY.
First, the global setup:
# Setup library
cfg = Z3.mk_contig()
ctx = Z3.mk_context(cfg)
solver = Z3.mk_solver(ctx)
int_sort = Z3.mk_int_sort(ctx)
There's no automatic conversion of numbers to Z3 objects, so we need to do this manually:
# Integer constants
nums = Hash(Int32, Z3::Ast).new
[0, 1, 9, 10, 100, 1000, 10000].each do |num|
nums[num] = Z3.mk_numeral(ctx, num.to_s, int_sort)
end
And set up variables. They all need to be 0 to 9, but we can't have leading zeroes so M and S must be at least 1:
# Variables, all 0 to 9
vars = Hash(String, Z3::Ast).new
%w[s e n d m o r e m o n e y].uniq.each do |name|
name_sym = Z3.mk_string_symbol(ctx, name)
var = Z3.mk_const(ctx, name_sym, int_sort)
vars[name] = var
Z3.solver_assert(ctx, solver, Z3.mk_ge(ctx, var, nums[0]))
Z3.solver_assert(ctx, solver, Z3.mk_le(ctx, var, nums[9]))
end
# m and s need to be >= 1, no leading zeroes
Z3.solver_assert(ctx, solver, Z3.mk_ge(ctx, vars["m"], nums[1]))
Z3.solver_assert(ctx, solver, Z3.mk_ge(ctx, vars["s"], nums[1]))
They also need to be all different:
# all letters represent different digits
all_distinct = Z3.mk_distinct(ctx, vars.size, vars.values)
Z3.solver_assert(ctx, solver, all_distinct)
Now SEND + MORE = MONEY. This is very verbose, but all the extra arguments like ctx and array sizes get in the way of doing it more concisely:
send_vars = [
Z3.mk_mul(ctx, 2, [vars["s"], nums[1000]]),
Z3.mk_mul(ctx, 2, [vars["e"], nums[100]]),
Z3.mk_mul(ctx, 2, [vars["n"], nums[10]]),
vars["d"],
]
more_vars = [
Z3.mk_mul(ctx, 2, [vars["m"], nums[1000]]),
Z3.mk_mul(ctx, 2, [vars["o"], nums[100]]),
Z3.mk_mul(ctx, 2, [vars["r"], nums[10]]),
vars["e"],
]
money_vars = [
Z3.mk_mul(ctx, 2, [vars["m"], nums[10000]]),
Z3.mk_mul(ctx, 2, [vars["o"], nums[1000]]),
Z3.mk_mul(ctx, 2, [vars["n"], nums[100]]),
Z3.mk_mul(ctx, 2, [vars["e"], nums[10]]),
vars["y"],
]
send_sum = Z3.mk_add(ctx, send_vars.size, send_vars)
more_sum = Z3.mk_add(ctx, more_vars.size, more_vars)
money_sum = Z3.mk_add(ctx, money_vars.size, money_vars)
send_more_sum = Z3.mk_add(ctx, 2, [send_sum, more_sum])
equation = Z3.mk_eq(ctx, send_more_sum, money_sum)
Z3.solver_assert(ctx, solver, equation)
And finally let's print the results. Z3 at least saves us here, as it has some rudimentary model to string conversion, so we don't need to do anything complicated. Eventually we don't want to use that - we'd rather get Hash of results from Z3 Model and handle printing it out ourselves, but that's still far away.
Result code has three possibilities ("definitely no", "definitely yes", and "Z3 couldn't solve it"):
# Get the result
result_code = Z3.solver_check(ctx, solver)
puts "Result code is: #{result_code}"
model = Z3.solver_get_model(ctx, solver)
s = Z3.model_to_string(ctx, model)
puts String.new(s)
Let's run it:
$ ./send_more_money.cr
Result code is: 1
d -> 7
n -> 6
o -> 0
m -> 1
r -> 8
s -> 9
e -> 5
y -> 2
That is: 9567 + 1085 == 10652
Story so far
I put the code in crystal-z3 repo.
We got the point where we can run Z3 from Crystal, but the API is horrendous.
So far Crystal FFI handled everything without any issues, but a lot of complexity is still ahead, and there's also a lot of things I'm ignoring like integrating with Z3 memory management.
Coming next
In the next episode, we'll try to make Crystal handle Z3 Contexts and other very low level concerns for us, so we can make code look less like ass. It will take many iterations before we get something decent. One step at a time.
Latest comments (0)