如果有多个解决方案，我最多可以打印2个？ [处于保留状态]

Question

如果一个公式具有多个模型，是否有某种方法可以打印它们？

我有一个问题，我知道有很多解决方案。但是，如果我使用以下命令

(check-sat)
(get-model)
(check-sat)
(get-model)

[z3打印两次相同的模型，而不是给我两个不同的模型。

Q：有什么方法可以提取公式的多个不同模型？

Answer 1

没有自动的方法可以做到这一点。通常的技巧是断言最后一个模型的取反，然后要求另一个模型。