У меня есть вопрос относительно того, как Z3 постепенно решает проблемы. Прочитав некоторые ответы здесь, я обнаружил следующее:

Существует два способа использования Z3 для пошагового решения: один - режим push / pop (стек), другой - использование предположений.Мягкие / жесткие ограничения в Z3.В режиме стека z3 забудет все выученные леммы вГлобальный (я прав?) размах даже после одного местного "попса"Эффективность усиления ограничений в решателях SMTВ режиме предположений (я не знаю имени, это имя, которое приходит мне в голову), z3 не упростит некоторые формулы, например, распространение значения.Поведение z3 меняется по запросу для несостоявшегося ядра

Я провел некоторое сравнение (вы можете попросить формулы, они слишком велики, чтобы их можно было поднять нарастать по вертикали), но вот мои наблюдения: на некоторых формулах, включая квантификаторы, режим предположений работает быстрее. В некоторых формулах с большим количеством логических переменных (переменных предположений) режим стека работает быстрее, чем режим предположений.

Они реализованы для определенных целей? Как работает пошаговое решение в Z3?