How to use array in PySMT?

Question

I have a problem with PySMT. I'm new in the field and I have no idea how to use arrays.

I've understood that:

1) It's possible to declare an array as:

a = Symbol("a", ArrayType(INT, INT))

2) Then, to store values in the array:

k = Store(a, Int(0), int(5))

3) Finally, to retrieve the value:

print(simplify(k).arg(2))

I don't know if there is a better way to do that, I will appreciate also some feedback about that.

Now, the real question is: Can I append values in the array inside a for loop? For example, is it possible to have something like :

for i in range(10):
    Store(a, Int(i), Int(i*2))

The problem here is that to retrieve the saved values I need to save the "Store" operation inside a variable (like 'k' above). I am pretty sure that should exist some way to do that..but it's too hard to find examples online !

Answer 1

I think the confusion might arise from the difference between Store and Select as methods with side effects vs expressions.

When you do: Store(a, Int(i), Int(i*2)) , you are building an expression in representing the result of performing the store. Therefore, as @alias suggests, you need to keep building on the same expression.

I would assume you might be running into a similar issue with Select. If you do s = Select(a, Int(0)), you are building an expression, not a value. If a is a has a value defined the index 0, you should be able to do s.simplify() and obtain the value.

In the example above, you should be able to replace your step 3) with simply that:

simplify(Select(k, Int(0))) # Int(5)

Edit: Full example following the discussion below

from pysmt.shortcuts import Symbol, Store, Select, Int, get_model
from pysmt.typing import ArrayType, INT

a = Symbol("a", ArrayType(INT, INT))

for i in range(10):
    a = Store(a, Int(i), Int(i*2))

print(a.serialize())
# >>> a[0 := 0][1 := 2][2 := 4][3 := 6][4 := 8][5 := 10][6 := 12][7 := 14][8 := 16][9 := 18]

# x is the expression resulting from reading element 5
# Simplify does not manage to infer that the value should be 10
x = Select(a, Int(5))
print(x.simplify().serialize())
# >>> a[0 := 0][1 := 2][2 := 4][3 := 6][4 := 8][5 := 10][6 := 12][7 := 14][8 := 16][9 := 18][5]

# Ask the solver for a value:
# Note that we can only assert Boolean expressions, and not theory expressions, so we write a trivial expression a = a  
m = get_model(a.Equals(a))

# Evaluate the expression x within the model
print(m[x])
# >>> 10