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公开了称为简化的简化函数。 您可以通过调用简化器来获得缩短的期限。 示例如下：

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