【笔记】Z3工具默认只能输出一个符合条件的模型，但如果我们想要全部符合条件的模型，可以参考如下代码实现
a = Int('a')
b = Int('b')
s = Solver()
s.add(1 <= a)
s.add(a <= 20)
s.add(1 <= b)
s.add(b <= 20)
s.add(a >= 2*b)
while s.check() == sat:
print (s.model())
s.add(Or(a != s.model()[a], b != s.model()[b]))