How to force z3py to show multiple answers if that the case?

Question

from z3 import *

p = Int('p')
q = Int('q')

solve(Or(p==1,p==2,p==3), Or(q==1,q==2), Not(p==q), q==1)

Gives me [p = 2, q = 1], but p could be 2 or 3. So the answer should be {2,3}. How can I tell z3 to inform me about multiple answers?

Answer 1

This question comes up often, and there are a few caveats. Essentially, you have to write a loop to "reject" earlier models and keep querying for satisfiability. For your particular problem, you can code it like this:

from z3 import *

p = Int('p')
q = Int('q')

s = Solver()
s.add(Or(p==1,p==2,p==3), Or(q==1,q==2), Not(p==q), q==1)

res = s.check()
while (res == sat):
  m = s.model()
  print(m)
  block = []
  for var in m:
      block.append(var() != m[var])
  s.add(Or(block))
  res = s.check()

When I run this, I get:

[p = 2, q = 1]
[p = 3, q = 1]

Note that z3 doesn't always produce a "full" model: It'll stop producing assignments once it determines the problem is sat. So, you might have to track your variables and use model-completion explicitly. See Trying to find all solutions to a boolean formula using Z3 in python for details on how to do that.