在 Z3Py 中检索枚举类型的值

【问题标题】：retrieving value of an enumerated type in Z3Py在 Z3Py 中检索枚举类型的值
【发布时间】：2013-01-07 16:33:48
【问题描述】：

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

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

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

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

【问题讨论】：

标签： python z3

【解决方案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)())

【讨论】：