在 Z3 中生成和评估字符串 -> 字符串函数的模型

Question

我有以下程序，它将简单的key=value约束应用于从字符串到字符串的函数：

from z3 import *
map = Function('map', StringSort(), StringSort())
c1 = map(StringVal('key1')) == 'value1'
c2 = map(StringVal('key2')) == 'value2'
c3 = map(StringVal('key3')) == 'value3'
c4 = map(StringVal('key4')) == 'value4'
s = Solver()
s.add(And(c1, c2, c3, c4))
print(s.check())
print(s.model())

该模型的输出如下：

[map = [Concat(Unit(Char),
Concat(Unit(Char),
Concat(Unit(Char), Unit(Char)))) ->
"value1",
Concat(Unit(Char),
Concat(Unit(Char),
Concat(Unit(Char), Unit(Char)))) ->
"value2",
Concat(Unit(Char),
Concat(Unit(Char),
Concat(Unit(Char), Unit(Char)))) ->
"value3",
Concat(Unit(Char),
Concat(Unit(Char),
Concat(Unit(Char), Unit(Char)))) ->
"value4",
else -> "value1"]]

这有点奇怪，但据推测，这只是Z3对函数域元素表示的限制。

希望我能在模型中函数的具体常数值上评估Z3表达式；然而，我不知道该怎么做。Python参考文档中的Eval方法在命名空间中找不到。我以前用C#绑定做过类似的事情，所以我知道这是可能的。

Answer 1

在这一点上，我的Z3问题基本上是传统的，再折腾几分钟就会发现你可以这样做：

s.model().eval(expr)

python文档中的Eval函数实际上被列为Model的成员函数，很容易被遗漏

根据@alias的评论，使用实际上是最佳实践

s.model().evaluate(expr, model_completion = True)

以减少意外。