如何在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))

这里的问题是，要检索保存的值，我需要将“Store”操作保存在一个变量中（如上面的“k”）。 我很肯定，应该有一些方法可以做到这一点…但这是太难找到网上的例子！你知道吗

Answer 1

我认为混淆可能是由于Store和Select as方法与表达式之间的差异造成的。你知道吗

当您这样做：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