关于Z3如何逐步解决问题,我有一个问题.在阅读了一些答案后,我发现了以下内容:
- 有两种方法可以使用Z3进行增量求解:一种是推/弹(堆栈)模式,另一种是使用假设.Z3中的软/硬约束.
- 在堆栈模式下,z3会忘记全局(我是对吗？)范围内所有学习的引理,即使在SMT求解器中有一个局部"弹出" 约束强化效率之后
- 在假设模式中(我不知道名称,这是我想到的名称),z3不会简化一些公式,例如值传播.z3行为根据不满核心的要求而变化
我做了一些比较(欢迎你问一下这些公式,它们太大而无法放在rise4fun上),但这里是我的观察:在一些公式中,包括量词,假设模式更快.在一些包含大量布尔变量(假设变量)的公式中,堆栈模式比假设模式更快.
它们是否针对特定目的实施？增量求解如何在Z3中起作用？