在Z3Py中检索枚举类型的值

Question

我该如何检索枚举变量 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)]，但构造方法不返回表达式。

- Vu Nguyen

Answer 1

v.sort().constructor(0) 这个表达式返回一个 Z3 函数声明。在 Z3 中，常量是没有参数的函数。要将声明转换为常量表达式，我们应该使用 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)())

- Leonardo de Moura