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

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

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

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

Выполняются ли они для определенных целей? Как работает инкрементное решение в Z3?

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

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