无法为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逻辑不知道代数数据类型。它会把它们当作未解释的。你回来的模型就好像枚举类是免费的。