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

Question

Я использую Z3 по формулам QFBV. Мне было интересно, может ли Z3 поэтапно работать над такими формулами, как SAT solvers can on boolean clauses. В основном мне нужен способ реализовать следующий цикл:

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. Это обсуждается здесь: Soft/Hard constraints in Z3