从 Z3Py 中的模型中检索数组答案

【问题标题】：Retrieving array from model in Z3Py从 Z3Py 中的模型中检索数组
【发布时间】：2016-05-18 03:22:44
【问题描述】：

我知道有一个similar question for Z3 C++ API，但我找不到 Z3Py 的相应信息。我正在尝试从 Z3 找到的模型中检索数组，以便我可以使用索引访问数组的值。例如，如果我有

>>> b = Array('b', IntSort(), BitVecSort(8))
>>> s = Solver()
>>> s.add(b[0] == 0)
>>> s.check()
sat

那么我想做类似的事情

>>> s.model()[b][0]
0

但我目前得到：

>>> s.model()[b][0]
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: 'FuncInterp' object does not support indexing

从 C++ 的答案来看，似乎我必须使用从模型中获得的一些值来声明一个新函数，但我对它的理解不够好，无法自己适应 Z3Py。

【问题讨论】：

标签： arrays z3 z3py

【解决方案1】：

您可以通过构造对关联数组模型函数的调用，让模型在特定点评估 (eval(...)) 数组。这是一个例子：

b = Array('b', IntSort(), BitVecSort(8))
s = Solver()
s.add(b[0] == 21)
s.add(b[1] == 47)
s.check()

m = s.model()
print(m[b])

print(m.eval(b[0]))
print(m.eval(b[1]))

产生

[1 -> 47, 0 -> 21, else -> 47]
21
47

【讨论】：