z3 - Z3配列：Select（）がStore（）によって保存された値を返さないのはなぜですか？

Question

私は以下のような単純なZ3pythonコードを持っています。「print」行は、その上の行に格納されていた「y」を返すことを期待しています。代わりに、結果として「A[x]」が返されました。

I = IntSort()
A = Array('A', I, I)
x = Int('x')
y = Int('y')
Store(A, x, y)
print Select(A,x)

Select()によって保存された値を返さないのはなぜStore()ですか？

ありがとう。

Answer 1

注意すべき点が 2 つあります。

最初：あなたが書くとき

Store(A, x, y)

A、x、y の 3 つの引数を持つ項を作成します。A に副作用はありません。次のように記述して、この用語の名前を作成できます。

B = Store(A,x,y)

2 つ目: Z3 は、必要な場合を除き、用語を単純化しません。Python API は、simplify と呼ばれる単純化関数を公開します。簡略化を呼び出すことにより、簡約された項を取得できます。例は次のとおりです。

I = IntSort()
A = Array('A', I, I)
x = Int('x')
y = Int('y')
B = Store(A, x, y)
print Select(B,x)
print simplify (Select(B,x))