Open Source Adventures: Episode 03: Object-Oriented Interface for Crystal Z3

@[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_bool_sort = Z3_mk_bool_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

#!/usr/bin/env crystal

require "./z3"

# Setup library
solver = Z3::Solver.new

# Variables, all 0 to 9
vars = Hash(Symbol, Z3::IntExpr).new
%i[s e n d m o r e m o n e y].uniq.each do |name|
  var = Z3::IntSort[name]
  vars[name] = var
  solver.assert var >= Z3::IntSort[0]
  solver.assert var <= Z3::IntSort[9]
end

# m and s need to be >= 1, no leading zeroes
solver.assert vars[:m] >= Z3::IntSort[1]
solver.assert vars[:s] >= Z3::IntSort[1]

# all letters represent different digits
solver.assert Z3.distinct(vars.values)

# SEND + MORE = MONEY
send_sum = (
  vars[:s] * Z3::IntSort[1000] +
  vars[:e] * Z3::IntSort[100] +
  vars[:n] * Z3::IntSort[10] +
  vars[:d]
)

more_sum = (
  vars[:m] * Z3::IntSort[1000] +
  vars[:o] * Z3::IntSort[100] +
  vars[:r] * Z3::IntSort[10] +
  vars[:e]
)

money_sum = (
  vars[:m] * Z3::IntSort[10000] +
  vars[:o] * Z3::IntSort[1000] +
  vars[:n] * Z3::IntSort[100] +
  vars[:e] * Z3::IntSort[10] +
  vars[:y]
)

solver.assert send_sum + more_sum == money_sum

# Get the result
result_code = solver.check
puts "Result code is: #{result_code}"
puts solver.model

require "./libz3"

module Z3
  extend self

  Context = LibZ3.mk_context(LibZ3.mk_config)

  def mk_solver
    LibZ3.mk_solver(Context)
  end

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

class Z3::Solver
  def initialize
    @solver = Z3.mk_solver
  end

  def assert(expr)
    Z3.solver_assert(@solver, expr._expr)
  end

  def check
    Z3.solver_check(@solver)
  end

  def model
    Z3::Model.new(Z3.solver_get_model(@solver))
  end
end

class Z3::Model
  def initialize(model : LibZ3::Model)
    @model = model
  end

  # This needs to go eventually
  def to_s(io)
    io << Z3.model_to_string(@model).chomp
  end
end

class Z3::IntSort
  @@sort = LibZ3.mk_int_sort(Context)

  def self.[](name : Symbol)
    Z3::IntExpr.new Z3.mk_const(name.to_s, @@sort)
  end

  def self.[](v : Int32)
    Z3::IntExpr.new Z3.mk_numeral(v, @@sort)
  end
end

class Z3::BoolSort
  @@sort = LibZ3.mk_bool_sort(Context)
end

class Z3::IntExpr
  def initialize(expr : LibZ3::Ast)
    @expr = expr
  end

  def sort
    Z3::IntSort
  end

  def ==(other : Z3::IntExpr)
    Z3::BoolExpr.new Z3.mk_eq(@expr, other._expr)
  end

  def >=(other : Z3::IntExpr)
    Z3::BoolExpr.new Z3.mk_ge(@expr, other._expr)
  end

  def >(other : Z3::IntExpr)
    Z3::BoolExpr.new Z3.mk_gt(@expr, other._expr)
  end

  def <=(other : Z3::IntExpr)
    Z3::BoolExpr.new Z3.mk_le(@expr, other._expr)
  end

  def <(other : Z3::IntExpr)
    Z3::BoolExpr.new Z3.mk_lt(@expr, other._expr)
  end

  def *(other : Z3::IntExpr)
    Z3::IntExpr.new Z3.mk_mul([@expr, other._expr])
  end

  def +(other : Z3::IntExpr)
    Z3::IntExpr.new Z3.mk_add([@expr, other._expr])
  end

  def _expr
    @expr
  end
end

class Z3::BoolExpr
  def initialize(expr : LibZ3::Ast)
    @expr = expr
  end

  def sort
    Z3::BoolSort
  end

  def _expr
    @expr
  end
end

# Not sure where to put this
def Z3.distinct(args : Array(Z3::IntExpr))
  Z3::BoolExpr.new Z3.mk_distinct(args.map(&._expr))
end