python - 无法在z3py中提取Z3 EnumSort的值

我目前正在尝试将问题编码到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中出现查找错误，似乎在str的结果上我确实获得了调用model.eval()的正确值（即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")时似乎出现此问题。

最佳答案

QF_ABV逻辑不知道代数数据类型。它将把它们视为未解释的。然后返回的模型就好像枚举排序是免费的。