在Z3Py中检索枚举类型的值

Question

如何检索枚举变量的值v ？例如，

vTyp, (val1,val2,val3) = EnumSort('vTyp',['val1','val2','val3'])
v = Const('my variable',vTyp)

现在，由于只是上面的变量v，我将如何检索值的列表 [val1,val2,val3]中v（这里val1,val3,val3是表达如上）？

我试过了，[v.sort().constructor(0), ...(1), ...(2)] 但是构造方法没有返回表达式。

Answer 1

该表达式v.sort().constructor(0)返回 Z3 函数声明。在 Z3 中，常量是带有 0 个参数的函数。要将声明转换为常量表达式，我们应该使用v.sort().constructor(0)().

顺便说一句，该函数is_func_decl可用于测试对象是否是 Z3 函数声明。该函数is_expr与 Z3 表达式等效。

print is_func_decl(v.sort().constructor(0))
print is_expr(v.sort().constructor(0))
print is_expr(v.sort().constructor(0)())