¿Puede Z3 funcionar en modo incremental?

Question

Estoy usando Z3 en fórmulas QFBV. Me preguntaba si Z3 puede trabajar de forma incremental en tales fórmulas, como los solucionadores de SAT pueden en cláusulas booleanas. Básicamente, necesito una forma de implementar el siguiente ciclo:

F = initial QFBV formula 
while(F is unsat) { 
    F := F Union {some additional QFBV formula based on unsat core} 
} 

¿Mantiene Z3 la información aprendida? ¿Puedo usar z3 incrementalmente?

Gracias.

Answer 1

Sí, Z3 puede hacerlo si usa assumptions. Esto se discute aquí: Soft/Hard constraints in Z3