z3 - z3python: XOR 演算子はありませんか?

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問題ありません。これは、XOR がサポートされていないことを意味しますか?

Answer 1

を使用する必要がありますXor(a, b)。さらに、式 を表す Z3 式を作成するにはa and b、 を使用する必要がありますAnd(a, b)。andPython では、演算子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()