使用 z3 证明 Boolean/Arithmetic 公式的身份

Question

我正在尝试使用 z3 来证明以下身份：

x+y == x^y + 2*(x&y)

也就是说，我们可以用布尔和算术指令的混合来代替任何加法（示例取自第 2.2 章，Hacker's Delight）。

我正在使用以下 z3 python 片段：

from z3 import *

x = BitVec("x", 32)
y = BitVec("y", 32)

lhs = x ^ y + (2*(x&y))
rhs = x + y
s = Solver()
s.add(lhs != rhs)
print s.check()
print s.model()

但是，z3 给了我这个：

sat

[y = 1509949440, x = 1040187384]

所以我想我在某种程度上错误地使用了 API。知道我的错误是什么吗？

Answer 1

显然这是 ^ 运算符的优先级问题。使用

lhs = (x ^ y) + (2*(x&y))

让这个例子对我有用。

使用 z3 证明 Boolean/Arithmetic 公式的身份

Use z3 to Prove Identity of Boolean/Arithmetic Formula

python

z3

z3py