Работает ли опция pull_nested_quantifiers с упрощением в Z3? - PullRequest
Новая
       30

Работает ли опция pull_nested_quantifiers с упрощением в Z3?

1 голос
/ 06 марта 2012

Я бы хотел вытащить все вложенные квантификаторы в формуле на самый внешний уровень. Я ожидал, что следующие команды будут работать в 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?

1 Ответ

1 голос
/ 07 марта 2012

В Z3 3.x команда simplify применяет только общие шаги локального упрощения. «Pull-nested-quantifiers» - это этап предварительной обработки. Это будет доступно как тактика / стратегия в будущих выпусках. У Z3 3.2 уже есть много встроенных стратегий / тактик в интерфейсе SMT 2.0. Следующий релиз будет иметь гораздо больший набор тактик. Они будут доступны также в API. Если вам нужна эта функция для какого-то проекта, просто отправьте мне письмо, и я сделаю неофициальный (бета) релиз для вас.

Наконец, у нас есть этот шаг предварительной обработки, потому что модуль MBQI создания экземпляров квантификатора на основе модели работает намного лучше, если универсальные квантификаторы не имеют вложенных (универсальных) квантификаторов. Ваш пример в порядке, так как Z3 устранит экзистенциальность и заменит x новой константой.

...