python - 在 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)] ，但构造函数方法不返回表达式。

score 4 · Accepted Answer

该表达式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)())

1 回答 1