檢索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)]但構造函數方法不返回表達式。

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)())