z3 - Z3Python：配列の例？

Question

Z3 pythonの配列理論を使用したコード例を探していますが、見つかりません。

誰かがいくつかのコード例を提供してもらえますか？

ありがとう！

Answer 1

以下は、配列の宣言と、インデックスhttp://rise4fun.com/Z3Py/7jAjによる項目へのアクセスを示す例です。

x = Int('x')
a = Array('a', IntSort(), BoolSort())
b = Array('b', IntSort(), BoolSort())
c = Array('c', BoolSort(), BoolSort())

e = ForAll(x, Or(Not(a[x]), c[b[x]]))
print e

solver = Solver()
solver.add(e)
c = solver.check()
print c

配列理論を使用Selectした別の例を次に示しますhttp://rise4fun.com/Z3Py/2CAn :Store

x = Int('x')
y = Int('y')
a = Array('a', IntSort(), IntSort())

s = Solver()
s.add(Select(a, x) == x, Store(a, x, y) == a)
print s.check()
print s.model()

とはいえ、StackOverflow にはいくつかの配列の例が浮かんでいます。詳細については、「z3py array」キーワードを使用してサイトを検索してみてください。