Да, по сути, есть два инкрементальных режима.
На основе стека: с помощью 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 предназначены, по сути, для удобства пользователя. Нет внутренней инкрементальности. Причина в том, что в этих двух режимах используется существенная предварительная обработка, которая не является инкрементальной.
person
Nikolaj Bjorner
schedule
04.11.2016
