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

Question

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

Answer 1

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

• Soft/Hard constraints in Z3

• How to use z3 incrementally and model without propositional value ？

• Incremental calls to Z3 on UFBV with and without push calls