当check-sat返回未知时保证部分模型

Question

我对z3的部分模型有疑问。我在网上查看了有关它们的信息，但遗憾的是我没有找到太多，除了在验证失败时有时可以检索它们。

如果(check-sat)返回unknown，对部分模型有什么保证（如果有任何可以检索的话）？是否保证始终是健全的？

我特别感兴趣的是与量词相关的不完整性，尽管我怀疑这有什么不同。

先感谢您。

Answer 1

由于 - 据我所知 - 没有官方保证，我希望（不满意）答案是：部分模型在很大程度上取决于具体问题和“手段”（预处理器步骤，启发式，求解器，策略，随机种子） ，超时，...）Z3适用于解决问题。

因此，我希望只有那些基本上知道整个代码库和你的具体问题的人才能给你一个满意的答案......如果有的话。