5

列挙変数の値を取得するにはどうすればよいですv か? 例えば、

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

さて、上記の variableだけが与えられた場合、 (where are expressions as above) の値のvリストを取得するにはどうすればよいでしょう か?[val1,val2,val3]vval1,val3,val3

試し[v.sort().constructor(0), ...(1), ...(2)] ましたが、コンストラクター メソッドが式を返しません。

4

1 に答える 1

4

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)())
于 2013-01-07T16:58:17.943 に答える