z3 - Z3可以在增量模式下工作吗？

Question

我在 QFBV 公式上使用 Z3。我想知道 Z3 是否可以像 SAT 求解器那样在 bool 子句上逐步处理这样的公式。基本上我需要一种方法来实现以下循环:

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

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

谢谢。

Answer 1

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