Как использовать массив в PySMT?

Question

У меня проблема с PySMT. Я новичок в этой области и понятия не имею, как использовать массивы.

Это я поняла:

1) Можно объявить массив как:

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

2) Затем, чтобы сохранить значения в массиве:

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

3) Наконец, чтобы получить значение:

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

Я не знаю, есть ли лучший способ сделать это, я также буду признателен за отзывы об этом.

Теперь реальный вопрос: могу ли я добавлять значения в массив внутри цикла for? Например, возможно ли иметь что-то вроде:

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

Проблема здесь в том, что для получения сохраненных значений мне нужно сохранить операцию "Сохранить" внутри переменной (например, "k" выше). Я почти уверен, что должен существовать какой-то способ сделать это... но слишком сложно найти примеры в Интернете!

Answer 1

Я думаю, что путаница может возникнуть из-за разницы между Store и Select как методами с побочными эффектами и выражениями.

Когда вы это сделаете: Store(a, Int(i), Int(i*2)), вы строите выражение, представляющее результат выполнения магазина. Следовательно, как предлагает @alias, вам нужно продолжать использовать одно и то же выражение.

Я предполагаю, что вы можете столкнуться с аналогичной проблемой с Select. Если вы это сделаетеs = Select(a, Int(0)), вы строите выражение, а не значение. Еслиa имеет значение, определенное индексом 0, вы должны иметь возможность s.simplify() и получить значение.

В приведенном выше примере вы сможете заменить шаг 3) просто следующим:

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

Изменить: полный пример после обсуждения ниже

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