Может ли Z3 работать в инкрементном режиме?

Question

Я использую Z3 в формулах QFBV.Мне было интересно, может ли 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