오픈 소스 모험: 에피소드 71: Crystal Z3 조각 개선

Crystal Z3에서 다양한 퍼즐 게임 해결사를 작성하면서 두 가지 큰 문제를 발견했습니다.

.reduce/+/*/and의 or 체인이 빈 배열

에 대한 특수한 경우에 자주 필요했습니다.

Model#[] 정확한 유형이 정적으로 알려진 경우에도 유형이 지정되지 않은 결과( Expr )를 반환했으므로 모델에서 데이터를 추출하려면 이동해야 합니다#to_s.

Z3.구별

사양 없이 이미 존재했습니다.

  it "Z3.distinct" do
    [
      2 >= a,
      a >= b,
      b >= c,
      c >= 0,
      Z3.distinct([a, b, c]),
    ].should have_solution({
      a => 2,
      b => 1,
      c => 0
    })
  end

Z3.add 및 Z3.mul

구현은 다음과 같습니다.

  def Z3.add(args : Array(IntExpr | Int))
    if args.empty?
      IntSort[0]
    else
      IntExpr.new API.mk_add(args.map{|a| IntSort[a]})
    end
  end

  def Z3.mul(args : Array(IntExpr | Int))
    if args.empty?
      IntSort[1]
    else
      IntExpr.new API.mk_mul(args.map{|a| IntSort[a]})
    end
  end

그리고 사양:

  it "Z3.add" do
    [
      a == 10,
      b == 20,
      c == Z3.add([a, 30, b])
    ].should have_solution({
      c => 60,
    })
    [
      a == Z3.add([] of Z3::IntExpr),
    ].should have_solution({
      a => 0,
    })
    [
      a == Z3.add([b]),
      b == 10,
    ].should have_solution({
      a => 10,
    })
    [
      a == Z3.add([10]),
    ].should have_solution({
      a => 10,
    })
  end

  it "Z3.mul" do
    [
      a == 10,
      b == 20,
      c == Z3.mul([a, 30, b])
    ].should have_solution({
      c => 6000,
    })
    [
      a == Z3.mul([] of Z3::IntExpr),
    ].should have_solution({
      a => 1,
    })
    [
      a == Z3.mul([b]),
      b == 10,
    ].should have_solution({
      a => 10,
    })
    [
      a == Z3.mul([10]),
    ].should have_solution({
      a => 10,
    })
  end

이것들은 또한 비트 벡터와 실수에 대해 정의될 수 있습니다.

Z3.and 및 Z3.or

그리고 Z3.and 및 Z3.or 에 대한 유사한 방법입니다. 이 경우를 제외하고는 빈 배열을 특수한 경우에 사용할 필요가 없으며 Z3 라이브러리가 이를 수행합니다.

  def Z3.and(args : Array(BoolExpr | Bool))
    BoolExpr.new API.mk_and(args.map{|a| BoolSort[a]})
  end

  def Z3.or(args : Array(BoolExpr | Bool))
    BoolExpr.new API.mk_or(args.map{|a| BoolSort[a]})
  end

그리고 사양:

  it "Z3.or" do
    [a == Z3.or([] of Z3::BoolExpr)].should have_solution({a => false})
    [a == Z3.or([true, false])].should have_solution({a => true})
    [a == Z3.or([false, false])].should have_solution({a => false})
    [a == Z3.or([false, b]), b == false].should have_solution({a => false})
    [a == Z3.or([false, b]), b == true].should have_solution({a => true})
    [a == Z3.or([true, false, b]), b == true].should have_solution({a => true})
  end

  it "Z3.and" do
    [a == Z3.and([] of Z3::BoolExpr)].should have_solution({a => true})
    [a == Z3.and([true, false])].should have_solution({a => false})
    [a == Z3.and([true, true])].should have_solution({a => true})
    [a == Z3.and([true, b]), b == false].should have_solution({a => false})
    [a == Z3.and([true, b]), b == true].should have_solution({a => true})
    [a == Z3.and([true, false, b]), b == true].should have_solution({a => false})
  end

비트 벡터에 대해서도 정의할 수 있습니다.

모델#[]

두 번째 문제는 Model#[] 올바르게 입력된 결과를 반환하는 것입니다. Z3 API는 단 한 번의 호출만 가능하며 Ruby에서는 실제로 이 작업을 수행할 필요가 없습니다. 올바른 유형을 반환하는 것이 보장됩니다.

그러나 Crystal에서는 유형 시스템에 이에 대해 알려야 합니다. 이를 위해 다음 매크로를 사용할 수 있습니다.

  {% for type in %w[BoolExpr IntExpr BitvecExpr RealExpr] %}
    def eval(expr : {{type.id}}, complete=false)
      result = API.model_eval(self, expr, complete)
      raise Z3::Exception.new("Incorrect type returned") unless result.is_a?({{type.id}})
      result
    end
  {% end %}

  def [](expr)
    eval(expr, true)
  end

사양은 다음과 같습니다.

require "./spec_helper"

describe Z3::Model do
  a = Z3.bool("a")
  b = Z3.bool("b")
  c = Z3.int("c")
  d = Z3.int("d")
  e = Z3.bitvec("e", 16)
  f = Z3.bitvec("f", 16)
  g = Z3.real("g")
  h = Z3.real("h")

  it "eval boolean" do
    solver = Z3::Solver.new
    solver.assert a == true
    model = solver.model
    model.eval(a).to_s.should eq("true")
    model.eval(b).to_s.should eq("b")
    model.eval(a).to_b.should eq(true)
    expect_raises(Z3::Exception) { model.eval(b).to_b }
  end

  it "[] boolean" do
    solver = Z3::Solver.new
    solver.assert a == true
    model = solver.model
    model[a].to_s.should eq("true")
    model[b].to_s.should eq("false")
    model[a].to_b.should eq(true)
    model[b].to_b.should eq(false)
  end

  it "eval integer" do
    solver = Z3::Solver.new
    solver.assert c == 42
    model = solver.model
    model.eval(c).to_s.should eq("42")
    model.eval(d).to_s.should eq("d")
    model.eval(c).to_i.should eq(42)
    expect_raises(Z3::Exception) { model.eval(d).to_i }
  end

  it "[] integer" do
    solver = Z3::Solver.new
    solver.assert c == 42
    model = solver.model
    model[c].to_s.should eq("42")
    model[d].to_s.should eq("0")
    model[c].to_i.should eq(42)
    model[d].to_i.should eq(0)
  end

  it "eval bit vector" do
    solver = Z3::Solver.new
    solver.assert e == 42
    model = solver.model
    model.eval(e).to_s.should eq("42")
    model.eval(f).to_s.should eq("f")
    model.eval(e).to_i.should eq(42)
    expect_raises(Z3::Exception) { model.eval(f).to_i }
  end

  it "[] bit vector" do
    solver = Z3::Solver.new
    solver.assert e == 42
    model = solver.model
    model[e].to_s.should eq("42")
    model[f].to_s.should eq("0")
    model[e].to_i.should eq(42)
    model[f].to_i.should eq(0)
  end

  it "eval real" do
    solver = Z3::Solver.new
    solver.assert g == 3.5
    model = solver.model
    model.eval(g).to_s.should eq("7/2")
    model.eval(h).to_s.should eq("h")
  end

  it "[] real" do
    solver = Z3::Solver.new
    solver.assert g == 3.5
    model = solver.model
    model[g].to_s.should eq("7/2")
    model[h].to_s.should eq("0")
  end
end

Z3 reals의 경우 #to_f , #to_rat 등을 제공하지 않았습니다. 이는 실제로 매우 복잡하고 매우 일반적인 유형이 아니므로 지금은 #to_s (또는 PR 추가 메서드를 구문 분석해야 합니다. ).

지금까지의 이야기

Updated shard is in .

다음에 온다

다음 몇 개의 에피소드에 걸쳐 Crystal 및 Z3에서 몇 가지 더 많은 퍼즐 게임 해결사를 코딩할 것입니다.