Tengo una pregunta sobre cómo Z3 soluciona problemas de manera incremental. Después de leer algunas respuestas aquí, encontré lo siguiente:

Hay dos formas de usar Z3 para la resolución incremental: una es el modo push / pop (pila), la otra está usando suposiciones.Restricciones suaves / duras en Z3.En el modo de pila, z3 olvidará todos los lemas aprendidos englobal (estoy en lo cierto?) alcance incluso después de un "pop" localEficiencia del fortalecimiento de restricciones en los solucionadores de SMT.En el modo de suposiciones (no sé el nombre, ese es el nombre que me viene a la mente), z3 no simplificará algunas fórmulas, por ejemplo. propagación de valores.Cambio de comportamiento de z3 a petición de unsat core

Hice algunas comparaciones (puede pedir las fórmulas, son demasiado grandes para ponerlas en el rise4fun), pero aquí están mis observaciones: en algunas fórmulas, incluidos los cuantificadores, el modo de suposiciones es más rápido. En algunas fórmulas con muchas variables booleanas (variables de suposiciones), el modo de pila es más rápido que el modo de suposiciones.

¿Se implementan para fines específicos? ¿Cómo funciona la resolución incremental en Z3?