You should use Xor(a, b)
. Moreover, to create the Z3 expression that represents the formula a and b
, we must use And(a, b)
. In Python, we can't overload the operators and
and or
.
Here is an example with the 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()