【发布时间】：2019-09-28 18:22:45
【问题描述】：
如果一个公式有多个模型，有什么方法可以打印出来吗？
我有一个问题，我知道有很多解决方案。但是，如果我使用以下命令
(check-sat)
(get-model)
(check-sat)
(get-model)
z3 两次打印同一个模型，而不是给我两个不同的模型。
问：有什么方法可以提取公式的多个不同模型？
【问题讨论】：
【发布时间】：2019-09-28 18:22:45
【问题描述】：
没有自动化的方法可以做到这一点。通常的技巧是断言最后一个模型的否定，并要求另一个模型。
详情请看这个答案：how to get multiple solutions for z3 solver in smt2 format example?
【讨论】：