【笔记】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]))