z3 UNSAT，如何检索多个核心

Question

很抱歉重新发布这个问题， How to get z3 to return multiple unsat cores, multiple satisfying assignments

为了完整起见，上面链接中的原始问题是：

我有兴趣检索（用于 QF_LRA）

-多个（最小或其他）UNSAT核心和 - 多项 SAT 作业

我查看了论坛上有关此主题的早期讨论，例如， 在逻辑 QF_LRA 上使用 z3 时如何获得不同的未饱和内核。这些 请参阅 z3 Python 教程，例如， http://rise4fun.com/Z3Py/tutorial/musmss 似乎离线 现在。我尝试了 github 等的其他建议来找到 提到教程，但没有运气。

感谢 Nikolaj Bjorner 为我之前的问题发布了答案。 但是，我不确定答案中发布的代码片段是否完整？有人可以对此发表评论吗？

我查看了在我最初问题的答案中提到的参考论文和 Mark Liffiton 的网页。如果可以重新发布或澄清完整的代码片段，那将是最有帮助的。

非常感谢

Answer 1

这是一个格式问题：HTML 格式裁剪了一些字符。现在已经修复了。您现在应该可以看到整个示例。