问Z3:找到所有令人满意的模型

EN

我正在尝试使用微软研究院开发的Z3来检索一些一阶理论的所有可能的模型。下面是一个最小的工作示例：

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

在这个命题例子中，有两个令人满意的赋值：f->true和f->false。因为Z3 (和一般的SMT求解器)只会尝试找到一个令人满意的模型，所以不可能直接找到所有的解决方案。Here我发现了一个名为(next-sat)的有用命令，但最新版本的Z3似乎不再支持此命令。这对我来说有点不幸，总的来说，我认为这个命令非常有用。有没有其他方法可以做到这一点？