Как работает пошаговое решение в Z3?

Question

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

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

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

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

Answer 1

Да, по сути, есть два дополнительных режима.

На основе стека: используя push(), pop() вы создаете локальный контекст, который следует дисциплине стека. Утверждения, добавленные в push (), удаляются после соответствующего pop(). Кроме того, любые леммы, которые получены при толчке, удаляются. Используйте push()/pop(), чтобы эмулировать замораживание состояния и добавление дополнительных ограничений над замороженным состоянием, затем вернитесь в замороженное состояние. Преимущество состоит в том, что освобождаются любые дополнительные накладные расходы памяти (такие как изученные леммы), созданные в рамках push (). Рабочее предположение состоит в том, что выученные леммы под толчком больше не будут полезны.

Основанный на предположениях: используя дополнительные литералы предположений, переданные в check()/check_sat(), вы можете (1) извлечь неудовлетворительные ядра поверх литералов предположений, (2) получить локальную инкрементальность без лемм сбора мусора, которые получаются независимо от предположений. Другими словами, если Z3 узнает лемму, которая не содержит никаких литералов предположений, она ожидает, что они не будут собирать мусор. Чтобы эффективно использовать предполагаемые литералы, вам также необходимо добавить их в формулы. Таким образом, компромисс заключается в том, что предложения, используемые с допущениями, содержат некоторое количество раздувания. Например, если вы хотите локально принять некоторую формулу (<= x y), то вы добавляете предложение (=> p (<= x y)) и принимаете p при вызове check_sat(). Обратите внимание, что исходное предположение было единицей. Z3 размножает единицы эффективно. С формулировкой, которая использует предположительные литералы, она больше не является единицей на базовом уровне поиска. Это влечет за собой дополнительные накладные расходы. Единицы становятся бинарными предложениями, бинарные предложения становятся троичными предложениями и т. Д.

Различия между функциями push/pop сохраняются для стандартного движка SMT Z3. Это двигатель, который будет использовать большинство формул. Z3 содержит некоторое портфолио двигателей. Например, для задач с чисто битовым вектором, Z3 может в конечном итоге использовать основанный на спутнике движок. Инкрементальность в движке на основе спутника реализована иначе, чем движок по умолчанию. Здесь инкрементальность реализуется с использованием литералов предположения. Любое утверждение, которое вы добавляете в область действия push, утверждается как импликация (=> scope_literals формула). check_sat() в такой области будет иметь дело с литералами предположений. С другой стороны, любое последствие (лемма), которое не зависит от текущей области, не является сборщиком мусора в pop().

В режиме оптимизации, когда вы устанавливаете цели оптимизации или когда вы используете объекты оптимизации через API, вы также можете вызывать push/pop. Аналогично с фиксированными точками. Для этих двух функций push/pop в основном для удобства пользователя. Там нет внутренней приращения. Причина в том, что эти два режима используют существенную предварительную обработку, которая является суперинкрементной.