Исключение кванторов для перечислимых типов в Z3

Я экспериментирую с тактикой исключения кванторов для формул перечислимых типов. Я хотел бы знать, есть ли способы повысить производительность, как-то настроив решатель. После беглого просмотра исходного кода я пришел к выводу, что, похоже, существуют разные стратегии для исключения кванторов (например, qe_lite.cpp), но они не представлены в качестве параметров тактики qe. В моем случае формулы имеют простую пропозициональную структуру, иногда количественные переменные даже не встречаются в формуле, но процедуру можно вызывать несколько тысяч раз. Итак, я думаю, мои вопросы следующие:

  1. Есть ли в Z3 какое-то кеширование для исключения квантификатора (режим приложения?), Которое позволило бы быстрее обрабатывать кучу похожих или идентичных формул?
  2. Могу ли я научить Z3 использовать разные подходы для исключения кванторов в формулах с конечной областью, чтобы я мог увидеть, какой из них лучше подходит для меня?
  3. Было бы интересно узнать, какой подход обычно используется в Z3 для устранения кванторов для формул над типами конечной области. Выполняется ли это просто заменой + упрощением, или используются какие-то более сложные техники?

Спасибо.


enums z3 quantifiers
person Egbert    schedule 18.04.2013    source источник

Ответы (1)


arrow_upward
1
arrow_downward

  1. «qe-lite» - это отдельная тактика от «qe».
  2. Нет определения сходства формул. Идентичные формулы имеют хэш-консистенцию (представлены уникальным образом), и исключение квантора проходит через это один раз.
  3. Вы можете попробовать «qe» или «qe-lite». «qe-lite» действительно легкий. В основном это устраняет равенство. Это задумано как грубая (более быстрая, неполная) процедура для исключения количественных переменных, когда это необходимо.
  4. Возможности для конечных областей очень просты: Z3 выполняет для бит-вектора, а логические значения, по сути, ALL-SAT для поиска значений, которые можно использовать. Для типов перечисления, заданных как алгебраические типы данных, Z3 просто выполняет разделение регистра (с последующей проверкой выполнимости для сокращения). значения из конечной области, которые
person Nikolaj Bjorner    schedule 18.04.2013
comment
Спасибо за ваш ответ. Включено ли хеширование по умолчанию, если я использую тот же контекст (через C ++ api)? Если нет, как мне его включить? Кроме того, последнее предложение ответа кажется незаконченным, оно просто чрезмерно или вы хотите добавить что-то еще? - person Egbert; 19.04.2013