Я хотел бы вывести все вложенные квантификаторы в формулу на самый внешний уровень. Я ожидал, что следующие команды будут работать в Z3, но они не работают:
(set-option :pull-nested-quantifiers true)
(simplify (exists ((x Int)) (and (>= x 0)
(forall ((y Int)) (and (>= y 1) (> x y))))))
Какова цель :pull-nested-quantifiers? Как получить вложенные квантификаторы с помощью SMT-LIB или Z3 API?
В Z3 3.x команда simplify применяет только шаги локального упрощения общего назначения. «Вытягивающие вложенные квантификаторы» — это этап предварительной обработки. Он будет доступен как тактика/стратегия в будущих выпусках. Z3 3.2 уже имеет множество встроенных стратегий/тактик во внешнем интерфейсе SMT 2.0. В следующем выпуске будет гораздо больший набор тактик. Они будут доступны также в API. Если вам нужна эта функция для какого-то проекта, просто отправьте мне письмо по электронной почте, и я сделаю для вас неофициальную (бета-версию).
Наконец, у нас есть этот этап предварительной обработки, потому что модуль MBQI создания экземпляров квантификатора на основе модели работает намного лучше, если универсальные квантификаторы не имеют вложенных (универсальных) квантификаторов. Ваш пример в порядке, так как Z3 устранит экзистенциальное и заменит x новой константой.
