次のZ3 pythonコードを書きます
x, y = Ints('x y')
F = (x == y & 16) # x has the value of (y & 16)
print F
しかし、次のエラーが発生します。
TypeError: unsupported operand type(s) for &: 'instance' and 'int'
Z3方程式でビット単位の算術演算(この場合は&)を行う方法は?
ありがとう。
次のZ3 pythonコードを書きます
x, y = Ints('x y')
F = (x == y & 16) # x has the value of (y & 16)
print F
しかし、次のエラーが発生します。
TypeError: unsupported operand type(s) for &: 'instance' and 'int'
Z3方程式でビット単位の算術演算(この場合は&)を行う方法は?
ありがとう。
x
y
ビットベクトルでなければなりません:
x, y = BitVecs('x y', 32)
F = (x == y & 16) # x has the value of (y & 16)
print F
http://rise4fun.com/Z3/tutorial/guideの Bitvectors セクションを参照してください。