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