为 String -> Z3 中的 String 函数生成和评估模型

Question

我有以下程序将简单的 key = value 约束应用于从 String 到 String 的函数：

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 表达式；但是，我不知道该怎么做。 Eval method from the Python reference docs is nowhere to be found in the namespace. I've done something like this before with the C# bindings 所以我知道这是可能的。

Answer 1

在这一点上，我的 Z3 问题本质上是传统的，再花几分钟的时间表明您可以按如下方式执行此操作：

s.model().eval(expr)

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

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

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

减少意外。

为 String -> Z3 中的 String 函数生成和评估模型

Generating and evaluating models for String -> String functions in Z3

z3

z3py