z3 - Z3 按位计算？

Question

我编写了以下 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 方程中进行按位算术(在本例中为 &)？

谢谢。

Answer 1

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 下的位向量部分