gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-02 09:43:07 26 4
gpt4 key购买 nike

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

最佳答案

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

关于z3 - 使用push命令在Z3中增量求解,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/18269016/

26 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com