使用推送命令在Z3中增量求解

Question

我正在使用Z3的python api來做某種增量求解。我使用solver.push()命令，在迭代中將約束條件推給解算器，同時檢查每個步驟的不可滿足性。我想知道Z3是否會使用從先前的約束中學習的引理或者使用新添加的約束求解時以前獲得的令人滿意的解決方案。我從來沒有使用solver.pop()命令。我在哪裏可以獲得更多關於以前迭代中所做工作的詳細信息？

Answer 1

Z3有多個求解器，但是其中只有一個真正支持先前調用的增量求解和重用工作。默認情況下，只要執行solver.push()，Z3就會自動切換到增量求解器。這個求解器也可以重用以前學過的子句。當執行solver.pop()時，學習的子句將被刪除。 Z3還支持另一種不基於push和pop的增量求解機制。下面是一些相關的帖子：

• Soft/Hard constraints in Z3

• How to use z3 incrementally and model without propositional value ？

• Incremental calls to Z3 on UFBV with and without push calls