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