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.
Top comments (0)