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

Я использую 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 постепенно?

Спасибо.


z3
person mahesh prabhu    schedule 02.02.2012    source источник

Ответы (1)


arrow_upward
6
arrow_downward

Да, Z3 может это сделать, если вы используете assumptions. Это обсуждается здесь: Мягкие/жесткие ограничения в Z3

person Leonardo de Moura    schedule 03.02.2012