Z3可以在增量模式下工作吗？答案

【问题标题】：Can Z3 work in incremental mode?Z3可以在增量模式下工作吗？
【发布时间】：2012-02-02 22:09:45
【问题描述】：

我在 QFBV 公式上使用 Z3。我想知道 Z3 是否可以在诸如 SAT 求解器之类的公式上逐步处理布尔子句。基本上我需要一种方法来实现以下循环：

F = initial QFBV formula
while(F is unsat) {
    F := F Union {some additional QFBV formula based on unsat core}
}

Z3 是否保留学习到的信息？我可以增量使用 z3 吗？

谢谢。

【问题讨论】：

标签： z3

【解决方案1】：

是的，如果您使用assumptions，Z3 可以做到这一点。这在这里讨论： Soft/Hard constraints in Z3

【讨论】：