我正在使用Z3的python api来做一些增量求解.我迭代地将约束推送到求解器,同时使用solver.push()命令检查每个步骤的不可满足性.我想了解Z3是否会使用先前约束的学习引理或者在使用新添加的约束求解时先前获得的满意解.我从不使用solver.pop()命令.在哪里可以获得有关如何使用先前迭代中完成的工作的更多详细信息？
Z3有多个解算器,但其中只有一个真正支持以前调用的增量求解和重用工作.默认情况下,只要执行a,Z3就会自动切换到增量解算器solver.push().该解算器也会重复使用以前学过的子句.solver.pop()执行a时删除学习的子句.Z3还支持另一种不基于push和的增量求解机制pop.以下是一些相关帖子:
| 归档时间： |
|
| 查看次数： |
1970 次 |
| 最近记录： |