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)))