Eu tenho uma pergunta sobre como Z3 incrementalmente resolve problemas. Depois de ler algumas respostas aqui, encontrei o seguinte:

Existem duas maneiras de usar o Z3 para solução incremental: um é o modo push / pop (pilha), o outro está usando as suposições.Restrições Soft / Hard no Z3.No modo de pilha, o z3 esquecerá todos os lemas aprendidos emglobal (Estou certo?) alcance mesmo após um "pop" localEficiência de fortalecimento de restrições em solucionadores de SMTNo modo de suposições (não sei o nome, esse é o nome que me vem à mente), o z3 não simplifica algumas fórmulas, por ex. propagação de valor.Comportamento do z3 mudando a pedido do núcleo insaturado

Eu fiz alguma comparação (você está convidado a pedir as fórmulas, elas são grandes demais para serem colocadas no rise4fun), mas aqui estão minhas observações: Em algumas fórmulas, incluindo quantificadores, o modo de suposições é mais rápido. Em algumas fórmulas com muitas variáveis ​​booleanas (variáveis ​​de suposições), o modo de pilha é mais rápido que o modo de suposições.

Eles são implementados para propósitos específicos? Como a resolução incremental funciona no Z3?