我正在使用 Z3 的 python api 进行某种增量求解。我迭代地向求解器推送约束，同时使用以下命令检查每个步骤的不满足性solver.push()命令。我想了解 Z3 是否会使用从先前约束中学习到的引理，或者使用新添加的约束进行求解时先前获得的令人满意的解决方案。我从不使用solver.pop()命令。我在哪里可以获得有关如何使用先前迭代中完成的工作的更多详细信息？
Z3 有多个求解器，但只有其中一个真正支持增量求解并重用先前调用的工作。默认情况下，每当您执行一个命令时，Z3都会自动切换到增量求解器solver.push()。该求解器还重用以前学过的子句。当出现以下情况时，学习到的子句将被删除：solver.pop()被执行。 Z3还支持另一种增量求解机制，该机制不基于push and pop。以下是一些相关帖子：
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
