z3 - z3python：没有异或运算符？

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

如果我替换xor为and，则没有问题。所以这意味着不支持异或？

Answer 1

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

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