z3 求解器异或问题？

Question

z3 求解器库是否存在潜在问题。特别是异或运算符？

在 python 中运行以下代码将返回“unsat”，而我相信答案应该是 sat。这是 z3 的潜在问题，还是我的 z3 库已损坏？

from z3 import *

l1 = Bool('l1')
l2 = Bool('l2')
l3 = Bool('l3')

s = Solver()
s.add(Xor(l1, l2, l3))
s.add(l3)
s.add(Not(l1))
s.add(Not(l2))
print(s.check())

Answer 1

Xor 仅接受两个参数。将其重写为

Xor(l1, Xor(l2, l3))

有关详细信息，请参阅 https://z3prover.github.io/api/html/namespacez3py.html#a2c61c680934248373aa85683200a5d91。