z3python : no XOR operator?

Question

我在 Z3 python 中有这段代码:

x = Bool('x')
y = Bool('y')
z = Bool('z')
z == (x xor y)
s = Solver()
s.add(z == True)
print s.check()

但是这段代码运行时报如下错误:

c.py(4): error: invalid syntax

如果我用and替换xor，就没有问题。那么这意味着不支持 XOR？

Answer 1

你应该使用Xor(a, b)。此外，要创建表示公式 a 和 b 的 Z3 表达式，我们必须使用 And(a, b)。在 Python 中，我们不能重载运算符 and 和 or。这是一个使用 Xor ( available online at rise4fun ) 的示例。

x = Bool('x')
y = Bool('y')
z = Xor(x, y)
s = Solver()
s.add(z)
print s.check()
print s.model()