z3 - Z3 数组：为什么 Select() 不返回 Store() 保存的值？

Question

我有简单的 Z3 python 代码，如下所示。我希望“打印”行将返回存储在其上方行中的“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

有两点需要注意：

第一：当你写

Store(A, x, y)

您创建一个包含三个参数 A、x 和 y的术语。A 没有副作用。您可以通过以下方式为该术语创建名称

B = Store(A,x,y)

第二：除非您愿意，否则 Z3 不会简化术语。python API 公开了一个名为simplified 的简化函数。您可以通过调用简化器来获得缩减项。例子是：

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