Отображение количественной формулы

как мне отобразить результат исключения квантификатора?
z3, кажется, доволен следующим входом

(set-option :elim-quantifiers true)
(declare-fun y () Real)
(simplify (exists ((x Real)) (>= x y)))

но он возвращает его так же, как вывод.

Спасибо


z3 quantifiers
person bobosoft    schedule 15.11.2011    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Z3 3.x имеет новый интерфейс для входного формата SMT-LIB 2.0. В новом интерфейсе команда simplify не является «зонтиком» для всех упрощений и шагов предварительной обработки, доступных в Z3. Подход «сделай все», использованный в Z3 2.x, имел несколько проблем. Итак, в Z3 3.x мы начали использовать мелкозернистый подход, когда пользователь может указать тактику/стратегию для решения и/или упрощения формул. Например, можно написать:

(declare-const x Int)
(assert (not (or (<= x 0) (<= x 2))))
(apply (and-then simplify propagate-bounds))

Эта новая инфраструктура находится в стадии разработки. Например, в Z3 3.2 нет команд/тактик для устранения квантификаторов в новом интерфейсе. Команды/тактики для исключения квантификаторов будут доступны в Z3 3.3. Тем временем вы можете использовать старый интерфейс SMT-LIB для устранения квантификаторов. Вы должны указать параметр командной строки -smtc, чтобы заставить Z3 использовать старый интерфейс. Более того, старый интерфейс не полностью совместим с SMT-LIB 2.0. Итак, вы должны написать:

(set-option ELIM_QUANTIFIERS true)
(declare-fun y () Real)
(simplify (exists ((x Real)) (>= x y)))
person Leonardo de Moura    schedule 15.11.2011