python - z3 solver Xor issue? - Stack Overflow

admin管理员组

文章数量:1122846

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

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

• python
• xor
• z3py

Share Improve this question Follow asked Nov 22, 2024 at 3:35 Jinhong HuoJinhong Huo 111 silver badge 0

Add a comment  | 

1 Answer 1

Sorted by: Reset to default 1

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.

本文标签： pythonz3 solver Xor issueStack Overflow