使用 push 命令在 Z3 中增量求解 [英] Incremental solving in Z3 using push command
问题描述
我正在使用 Z3 的 python api 进行某种增量求解.我使用 solver.push() 命令在每一步检查不满足性的同时，迭代地将约束推送到求解器.我想了解 Z3 是否会使用从先前约束中学习到的引理，或者使用新添加的约束求解时先前获得的令人满意的解决方案.我从不使用 solver.pop() 命令.在哪里可以获得有关如何使用先前迭代中完成的工作的更多详细信息?
I am using Z3's python api to do some kind of incremental solving. I push constraints to the solver iteratively while checking for unsatisfiability at each step using solver.push() command. I want to understand whether Z3 would use the learned lemmas from previous constraints or the satisfying solution previously obtained when solving with a newly added constraint. I never use the solver.pop() command. Where can I get more details about how the work done in previous iterations is used?
推荐答案
Z3 有多个求解器，但其中只有一个真正支持增量求解和重用以前调用的工作.默认情况下，每当您执行 solver.push() 时，Z3 都会自动切换到增量求解器.该求解器还重用以前学习的子句.当执行 solver.pop() 时，学习的子句被删除.Z3 还支持另一种不基于push 和pop 的增量求解机制.以下是一些相关帖子:
Z3 has multiple solvers, but only one of them really supports incremental solving and reuse work from previous calls. By default, Z3 will automatically switch to the incremental solver whenever you execute a solver.push(). This solver alsos reuse previously learned clauses. The learned clauses are deleted when a solver.pop() is executed. Z3 also support another mechanism for incremental solving that is not based on push and pop. Here are some related posts:
这篇关于使用 push 命令在 Z3 中增量求解的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
