我有一个关于 z3 的部分模型的问题。 我在网上查找了有关它们的信息，但遗憾的是我没有找到太多，除了有时可以在验证失败时检索它们。
如果(check-sat)返回unknown，关于部分模型的保证是什么(如果有的话可以检索(？它能保证永远是健全的吗？
我对与量词相关的不完备性特别感兴趣，尽管我怀疑这有什么不同。
提前谢谢你。
由于据我所知没有官方保证，我希望(不令人满意的(答案是：部分模型在很大程度上取决于具体问题和"手段"(预处理器步骤、启发式、求解器、策略、随机种子、超时......Z3申请解决这个问题。
因此，我希望只有基本上了解整个代码库和您的具体问题的人才能给您一个令人满意的答案......如果有的话。