Z3：find所有满意的模型
我试图用微软研究所开发的SMT解算器Z3检索一些一阶理论的所有可能的模型。 这是一个最小的工作示例：
(declare-const f Bool) (assert (or (= f true) (= f false))) 在这个命题的情况下，有两个令人满意的分配： f->true和f->false 。 因为Z3（和一般的SMT解算器）只会试图find一个令人满意的模型，所以find所有的解决scheme是不可能的。 在这里，我发现了一个有用的命令(next-sat) ，但是似乎最新版本的Z3不再支持这个命令。 这对我来说有点不幸，总的来说，我认为这个命令是非常有用的。 有没有另外一种方法呢？
一种方法是使用其中的一个API，以及模型生成function。 然后，您可以使用从一个可满足性检查生成的模型添加约束，以防止以前的模型值在随后的可满足性检查中使用，直到没有更令人满意的分配为止。 当然，你必须使用有限的sorting（或者有一些限制来确保这一点），但是如果你不想find所有可能的模型（也就是说，在生成一堆之后停止） 。
这里是一个使用z3py的例子（链接到z3py脚本： http ：//rise4fun.com/Z3Py/a6MC）：
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])) # prevent next model from using the same assignment as a previous model
一般来说，使用所有相关常量的分离都应该起作用（例如，这里的a和b ）。 这列举了a和b （ 1和20之间）满足a >= 2b所有整数赋值。 例如，如果我们将a和b限制在1和5之间，则输出为：
[b = 1, a = 2] [b = 2, a = 4] [b = 1, a = 3] [b = 2, a = 5] [b = 1, a = 4] [b = 1, a = 5]
