无法在 z3py 中提取 Z3 EnumSort 的值

Question

我目前正在尝试将一个问题编码到 Z3 中，并且我希望建模一个“三态”布尔值（即具有 true、false 和 unknown 的布尔值）。

这是我的建模方式：

#!/usr/bin/env python

import z3
from collections import OrderedDict

TristateValues = ["True", "False", "Unknown"]
Tristate, consts = z3.EnumSort("Tristate", TristateValues)
TristateValues = OrderedDict(zip(TristateValues, consts))

s = z3.Solver()
x = z3.Const("x", Tristate)
s.add(x != TristateValues["Unknown"])
value = s.check()
if value == z3.sat:
    m = s.model()
    print str(m.eval(x))
else:
    print str(value)

# EOF

在这个小例子中，一切正常，我得到了诸如True 或False 之类的值。

但是，在更大的示例中，我得到的结果如下：

• Tristate!val!0
• Tristate!val!1
• Tristate!val!2

显然，这些“三态”字符串和实际值之间似乎会有一个映射，所以我写了这样的东西：

ModelToTristate = {}

as_list = list(TristateValues.keys())
for idx in range(0, len(as_list)):
    ModelToTristate["Tristate!val!{:d}".format(idx)] = as_list[idx]

尝试在值之间进行映射（这就是为什么使用OrderedDict 对保持顺序很重要）。

而且，最初，这似乎奏效了。然而，我又遇到了一些更奇怪的错误：

• 我最终会在ModelToTristate 中找到查找错误，似乎我确实在model.eval() 的结果上获得了调用str 的正确值（即，Z3 将给出True、False、等等而不是Tristate!val!*)
• 我会在模型中发现不一致（例如，即使在断言 x == Tristate["False"] 时，检查查找也会导致 model.eval(x) == Tristate!val!1，其中 Tristate!val!1 映射到 True）

对于最后一个问题，我认为存在查找问题，而不是 Z3 给出的值不正确。

所以，我的问题是：是什么导致 Z3 使用这些 Tristate!val!* 字符串，我可以“强制”Z3 使用正确的值（即True、False、Unknown）吗？

我使用的是 Z3 4.5.0。

更新检查后，好像是我用SolverFor("QF_ABV")的时候出现这个问题。

Answer 1

QF_ABV 逻辑不知道代数数据类型。它会将它们视为未解释的。你当时得到的模型就好像枚举排序是免费的一样。