Z3 3.x имеет «язык спецификации стратегии», основанный на тактике и тактике. Я пока что не "рекламирую", потому что он работает.
Основная идея описана в этой слайд-колоде .
У нас есть разные встроенные стратегии для каждой логики. Стратегии обычно не поддерживают постепенное решение, потому что они могут применять преобразования, использующие допущение «замкнутого мира». Например, у нас есть преобразования, которые отображают 0-1 линейную целочисленную арифметику в SAT. Всякий раз, когда Z3 обнаруживает, что пользователь «хочет» инкрементного решения (например, несколько команд check-sat, push и pop), он переключается на решатель общего назначения. В будущих версиях мы предоставим больше возможностей для управления поведением Z3.
Кстати, если у вас есть две последовательные команды (check-sat) (check-sat), Z3 не обязательно входит в инкрементный режим. Он будет введен, только если между двумя вызовами есть команда assert или push.
Теперь предположим, что ваш запрос имеет форму: (check-sat) <assertions> (check-sat), а ваш второй запрос имеет форму (check-sat) <assertions> (push) (check-sat). В обоих случаях Z3 будет в инкрементном режиме во втором (check-sat). Тем не менее, поведение по-прежнему не то же самое. Инкрементный решатель «компилирует» утвержденные формулы во внутренний формат, и его поведение зависит от выполнения команды push. Например, он будет использовать более эффективную кодировку бинарных предложений только в том случае, если отсутствует область действия пользователя. Под областью пользователя я подразумеваю количество push команд - количество pop команд. Это происходит потому, что структура данных, используемая в более эффективном кодировании, не имеет эффективной операции отмены / обращения.