z3 - 在 Z3 中使用 push 命令进行增量求解

Question

我正在使用 Z3 的 python api 进行某种增量求解。solver.push()我迭代地将约束推送到求解器，同时使用命令检查每个步骤的不可满足性。我想了解 Z3 是否会使用从先前约束中学习到的引理，或者在使用新添加的约束进行求解时先前获得的令人满意的解决方案。我从不使用solver.pop()命令。我在哪里可以获得有关如何使用先前迭代中完成的工作的更多详细信息？

Answer 1

Z3 有多个求解器，但其中只有一个真正支持增量求解和重用以前调用的工作。默认情况下，每当您执行solver.push(). 该求解器还重用以前学习的子句。执行a 时删除学习的子句solver.pop()。Z3 还支持另一种不基于push和的增量求解机制pop。以下是一些相关的帖子：

• Z3 中的软/硬约束

• 如何增量使用z3，没有命题值的建模？</a>

• 在 UFBV 上对 Z3 的增量调用，有和没有推送调用