Z3：找到满足所有车型(Z3: finding all satisfying models)

我想检索所有可能的模型使用Z3，微软研究院开发的SMT求解一些一阶理论。 下面是一个最小的工作示例：

(declare-const f Bool)
(assert (or (= f true) (= f false)))

在这种情况下，命题有两个令人满意的作业： f->true和f->false 。 由于Z3（一般和SMT求解器）将只尝试找到一个满意的模型，发现所有的解决方案是不能直接。 在这里我找到了一个叫有用的命令(next-sat)但似乎Z3的最新版本不再支持这一点。 这对我来说有点可惜，一般我认为该命令是非常有用的。 是否有这样做的另一种方式？

Answer 1:

一种方法来完成，这是使用API​​中的一个，与模型生成能力一起。 然后，您可以使用生成的模型从一个满足性检查，添加约束，以防止在随后的满足性检查正在使用以前的模型值，直到没有更令人满意的分配。 当然，你必须使用有限的种类（或有一定的限制，确保这一点），但你可以有无限种使用，以及如果你不希望找出所有可能的模型（即阻止你产生了一堆后） 。

下面是使用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]

文章来源: Z3: finding all satisfying models