Z3 中无法满足的假设？

Question

根据 SMTLib 文档 here，我们可以使用 check-sat-assuming 检查 sat，然后可以使用 get-unsat-assumptions 确定不可满足的假设。

在 JavaAPI 中的 Z3 上反映这一点，我可以看到 checkAssuming API 与check-sat-assuming 做同样的事情，但我似乎找不到任何与get-unsat-assumptions 类似的东西，我能找到的只是getUnsatCore api。

所以我的问题是，我是否可以在 Z3 中使用 JavaAPI 获得不满足的假设？

非常感谢！

Answer 1

看起来像是 Java API 中的一个疏忽。你可能想在他们的 github 网站上提交一张票（或者更好的是一个 pull-request）：https://github.com/Z3Prover/z3/issues