CODEWITHSUNDEEP
pythonxorz3py
Jinhong Huo
Jinhong Huo

Reputation: 1

z3 solver Xor issue?

Is there a potential issue with z3 solver library. Sprecifically on Xor operator?

Running the following code in python would return 'unsat' while I believe the answer should be sat. Is this a potential issue with z3, or is my z3 library corrupted?


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())

Upvotes: 0

Views: 37

Answers (1)

alias
alias

Reputation: 30525

Xor takes only two arguments. Rewrite it as

Xor(l1, Xor(l2, l3))

See https://z3prover.github.io/api/html/namespacez3py.html#a2c61c680934248373aa85683200a5d91 for details.

Note that the API for Xor does take 3 arguments, but the last argument is the "context", not another boolean. (Context is something you can ignore for most practical purposes. It dictates which solver-context the expression should be created in. For most users the default one is sufficient.)

Strictly speaking this is a short-coming of the z3py API. It should've warned you that the argument you passed is not a context, and stopped processing. Alas, the z3py API is forgoes most such checks, and the outcome is typically unpredictable when you use it in a way it's not intended. A good way to debug such problems is to add the line:

print(s)

to your program before you call s.check(). If you do so, you'll see it prints:

[Xor(l1, l2), l3, Not(l1), Not(l2)]

That is, it also asserted l3 as a constraint, which is not what you intended. And this is the reason why you got unsat as the answer.

Long story short, only pass two arguments to Xor; and it'll work as intended.

Upvotes: 1

Related Questions