오픈 소스 모험: 에피소드 02: Crystal Z3에 대한 낮은 수준의 우려 숨기기

이전 에피소드에서 우리는 Crystal이 Z3와 함께 작업하는 것을 얻었지만 그것은 직접적으로 낮은 수준의 C API를 따르고 있었습니다.

이 에피소드에서 우리는 문제를 계층화할 것입니다:

먼저 C 함수에 직접 해당하는 매우 낮은 수준의 API를 갖게 됩니다. 일부 유사한 프로젝트에서 본 규칙에 따라 이름을 LibZ3로 변경했습니다.

그런 다음 두 번째 레이어, 낮은 수준의 세부 정보를 많이 숨기는 더 멋진 API가 있습니다. Z3

마지막으로 실제 프로그램

LibZ3와 좋은 API 사이의 거리가 꽤 커서 나중에 이 레이어 케이크에 다른 레이어를 추가하고 싶습니다.

LibZ3

내가 변경한 것은 LibZ3 로 이름을 바꾸고 LBool 열거형을 도입한 두 가지뿐입니다. Z3는 해결할 수 없는 문제를 다루기 때문에 때때로 3가지 값(예, 아니오, 결정할 수 없음)을 반환해야 합니다. 흥미롭게도 이전 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_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

다음 레이어

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

다음 계층은 여러 컨텍스트를 지원하는지 여부에 대한 한 가지 결정을 내려야 하며, 일부 합법적인 용도가 있더라도 그렇게 하지 않을 것입니다. 그렇게 하면 API가 크게 복잡해지며 압도적인 대다수의 응용 프로그램은 이를 필요로 하지 않기 때문입니다. .

이 전체 코드는 매우 복사 및 붙여넣기이며 이러한 호출이 약 700개이므로 결국 매크로 또는 일부 자동화된 생성을 사용해야 합니다. Ruby 버전에서는 자동화된 생성을 사용했는데, 그 코드는 멋진 메타프로그래밍보다 정규 표현식으로 단위 테스트를 하는 것이 더 쉽기 때문입니다.

다음 에피소드에서 단위 테스트 가능한 Crystal 매크로가 어떻게 되는지 확인하고 싶습니다. 기본적으로 expect(somemacro(args)).to expand_to{ some code } ?

여기에 상수 IntSort 를 사용하는 빠른 해킹도 있습니다. Z3에는 N비트 비트 벡터, 다양한 부동 소수점 숫자 및 훨씬 더 특이한 개체와 같은 잠재적으로 무한한 수의 유형이 있으며 이는 많은 복잡성을 추가합니다. 우리는 지금 이것을 무시하고 지금으로서만 정수와 부울을 지원하려고 할 수 있습니다.

수정의 한계

두 가지 Crystal 관련 문제가 있습니다. 먼저 한 줄로 된 메서드 정의를 원합니다. Ruby 3에서 추가한 이 구문과 같은 작업을 수행할 수 있다면 좋을 것입니다.

  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 . 전반적으로 이것은 순전히 구문상의 문제이며, 좋겠지만 다른 구문과 충돌하기 전에 추가할 수 있는 구문이 너무 많습니다.

훨씬 더 큰 문제는 우리가 이것을 해야 하는 이유입니다:

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

Ruby에서 하는 방식 대신:

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

원래는 Ruby 방식으로 시도했지만 Crystal에서는 허용하지 않습니다Z3.mk_distinct(*vars.values). 내가 시도하면 Error: argument to splat must be a tuple, not Array(LibZ3::Ast) .

일부 해결 방법이 없으면 이제 모든 mk_add([...]) 및 mk_mul([...]) 내부에 추가[]가 필요하므로 어색한 API로 이어질 것입니다. 다음 에피소드에서 가능한 해결 방법에 대해 알아보겠습니다.

솔루션 코드

먼저 Solver 및 일부 변수를 설정합니다.

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

컨텍스트를 처리하지 않아도 이 코드는 확실히 정리됩니다.

add 및 muls 및 추가 항목[]이 있는 다음 코드는 놀랍지 않습니다.

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

공정하게 말하면 최종 목표는 다음과 같이 말하므로 큰 문제는 아닙니다.

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)

연산자를 사용하므로 어쨌든 [] 가 없습니다.

그리고 마지막으로 결과를 인쇄합니다. 이제 숫자가 아닌 열거형이므로 아무 것도 하지 않아도 멋지게 인쇄됩니다.

# 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

지금까지의 이야기

All the code is in crystal-z3 repo .

사용할 수 있는 것에 가까워졌지만 API가 불완전하고 불편합니다.

다음에 온다

다음 에피소드에서는 부울과 정수만 사용하여 Z3의 제한된 하위 집합에 대한 멋진 연산자 기반 API를 만들려고 합니다.