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

Question

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

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

спасибо.

Answer 1

1. "qe-lite" - отдельная тактика от "qe".
2. Не найдено обнаружение сходства формул. Идентичные формулы являются хеш-consed (представлены однозначно), а исключение квантификатора проходит один раз.
3. Вы можете попробовать либо «qe», либо «qe-lite». «qe-lite» действительно легкий. Это в основном устраняет равенства. Это подразумевается как грубая (более быстрая, неполная) процедура для исключения количественных переменных, когда это возможно.
4. Возможности для конечных доменов очень просты: Z3 выполняет для вектора бит и Booleans, по существу, ALL-SAT, чтобы найти значения, которые могут использоваться. Для типов перечисления, заданных как алгебраические типы данных, Z3 просто разбивает случай (за которым следует проверка выполнимости для обрезки). значения из конечного домена, которые являются