在Z3中如何增量求解？
我有一个关于如何Z3逐步解决问题的问题。 在阅读了一些答案之后，我发现了以下内容：
- 有两种方法可以使用Z3进行增量式求解：一种是push / pop（堆栈）模式，另一种是使用假设。 Z3中的软/硬约束 。
- 在堆栈模式下，即使经过一次本地“popup”，z3也会忘记全局 （ 我是对的？ ）范围内的所有学习引理。SMT解算器中约束强化的效率
- 在假设模式（我不知道名字，这是我想到的名字），z3不会简化一些公式，例如价值传播。 z3的行为改变对不可核心的要求
我做了一些比较（欢迎您提出公式，它们太大而不能提高），但这里是我的观察结果：在包括量词在内的一些公式中，假设模式更快。 在有很多布尔variables（假设variables）的一些公式中，堆栈模式比假设模式更快。
他们是为了特定目的而实施的吗 在Z3中如何进行增量式求解？
是的，基本上有两种增量模式。
基于堆栈：使用push（），pop（）创build一个本地上下文，它遵循堆栈规则。 在push（）下添加的断言在匹配pop（）后被删除。 此外，任何在推动下派生的引理都被移除。 使用push（）/ pop（）模拟冻结状态并在冻结状态上添加额外的约束，然后恢复到冻结状态。 它具有的优点是释放了在push（）范围内构build的任何额外的内存开销（例如学习的引理）。 我们的工作假设是，推动下学习的引理不再有用。
基于假设：使用传递给check（）/ check_sat（）的附加假设文字，您可以（1）在假设文字上提取不可满足的核心，（2）获得本地递增，而无需垃圾收集引理， 换句话说，如果Z3学习一个不包含任何假设文字的引理，它就不会垃圾收集它们。 要有效地使用假设文字，您也必须将它们添加到公式中。 所以权衡是假设条款包含了一些膨胀量。 例如，如果你想在局部假定一些公式（<= xy），那么你添加一个子句（=> p（<= xy）），并在调用check_sat（）时假设p。 请注意，最初的假设是一个单位。 Z3有效地传播单位。 通过使用假定文字的公式，它不再是search基本级别的单位。 这会招致一些额外的开销。 单位成为二元条款，二元条款成为三元条款等。
推/拉function之间的区别适用于Z3的默认SMT引擎。 这是大多数公式将要使用的引擎。 Z3包含一些引擎组合。 例如，对于纯粹的位向量问题，Z3最终可能会使用sat引擎。 基于sat的引擎中的增量与默认引擎的实现方式不同。 这里增量是用假设文字来实现的。 您在推送范围内添加的任何断言都被声明为一个含义（=> scope_literals公式）。 这样的范围内的check_sat（）将不得不处理假设文字。 另一方面，任何不依赖于当前范围的结果（引理）都不会在pop（）上被垃圾回收。
在优化模式下，当您声明优化目标时，或者当您使用API上的优化对象时，还可以调用push / pop。 同样的固定点。 对于这两个特性，push / pop基本上是为了用户的方便。 没有内在的渐进性。 原因是这两种模式使用了超级非增量的大量预处理。
