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

Question

我在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吗？

谢谢.

Answer 1

是的,如果您使用,Z3可以做到这一点assumptions.这在这里讨论: Z3中的软/硬约束