python - 我们如何使用 python 对 z3 中的整数使用 xor 操作？

Question

from z3 import *
x = Int('x') #declaration
y = Int('y') #declaration
solve((x ^ y)==2) #solving

我无法使用python在z3中执行异或运算。如果我做错了，请帮助告诉我正确的写作方式是什么，否则建议其他一些方式。请尽快回复。

score 3 · Accepted Answer

您可以^在 Python 中使用整数：

>>> 2^3
1

但是，z3 不使用整数，而是使用自己的 Int 对象，并且不支持异或。你必须使用BitVec类型。

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

solve(x^y==2, show=True)

1 回答 1