Z3 array: why Select() does not return value saved by Store()?

Question

I have simple Z3 python code like below. I expect the "print" line will return me "y" which was stored in the line above it. Instead, I got back "A[x]" as result.

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

Why does not Select() return the value stored by Store()?

Thanks.

Answer 1

There are two things to note:

First: When you write

Store(A, x, y)

You create a term with three arguments , A, x, and y. There is no side-effect to A. You can create a name for this term by writing

B = Store(A,x,y)

Second: Z3 does not simplify terms unless you want it to. The python API exposes a simplification function called simplify. You can obtain the reduced term by calling the simplifier. The example is:

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