如何在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“)。我非常确定应该存在一些方法来做that..but，在网上很难找到示例！

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