Dose z3 find all satifiable models

Question

There are some constraints such as x + y > 5 , x > 3 , y < 4, so the set of models x = 4 y= 3, which is given by z3. Dose z3 can give models incrementally, such as another set of models x=5,y = 2? Thanks. Regards

possible duplicate of [Z3: finding all satisfying models](http://stackoverflow.com/questions/13395391/z3-finding-all-satisfying-models) — Taylor T. Johnson, Jul 23 '13 at 13:05
Here's your example using the method described at that question/answer: http://rise4fun.com/Z3Py/QfFt — Taylor T. Johnson, Jul 23 '13 at 13:07

score 0 · Answer 1 · answered Jul 23 '13 at 14:05

Can you tell me please what happens with this:

x,y = Bools('x y')

s = Solver()
s.add(Or(x,y))


count = 0
while s.check() == sat and count <= 50:
  print s.model()
  s.add(Or(x != s.model()[x], y != s.model()[y])) 
  count = count + 1
print count

the output is:

[y = False, x = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
[y = True]
 51

online here

Dose z3 find all satifiable models

1 Answers1