model - 剂量 z3 找到所有可满足的模型

Question

有一些约束，例如 x + y > 5 , x > 3 , y < 4，所以模型集合 x = 4 y= 3，由 z3 给出。剂量z3可以增量给模型，比如另外一组模型x=5,y=2？谢谢。问候

Answer 1

你能告诉我这会发生什么吗：

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

输出是：

[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

在线这里