2

我对 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”）。我很确定应该存在某种方法来做到这一点..但是在网上很难找到例子！

4

1 回答 1

2

我认为混淆可能源于 Store 和 Select 作为具有副作用的方法与表达式之间的差异。

当您这样做时：Store(a, Int(i), Int(i*2))，您正在构建一个表示执行存储结果的表达式。因此，正如@alias 建议的那样，您需要继续构建相同的表达式。

我假设您可能会遇到类似的问题Select。如果你这样做s = Select(a, Int(0))，你正在构建一个表达式，而不是一个值。如果a是 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
于 2019-07-21T15:38:14.643 回答