Display quantified-out formula

Question

how do I display the result of quantifier elimination ?
z3 seems to be happy with the following input

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

but it returns it the same as output.

Thanks

Answer 1

Z3 3.x has a new front-end for the SMT-LIB 2.0 input format. In the new front-end, the command simplify is not an “umbrella” for all simplifications and pre-processing steps available in Z3. The “do-all” approach used in Z3 2.x had several problems. So, in Z3 3.x, we started using a fine-grain approach where the user can specify tactics/strategies for solving and/or simplifying formulas. For example, one can write:

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

This new infrastructure is working in progress. For example, Z3 3.2 does not have commands/tactics for eliminating quantifiers in the new front-end. The commands/tactics for quantifier elimination will be available in Z3 3.3. In the meantime, you can use the old SMT-LIB front-end for eliminating quantifiers. You must provide the command line option -smtc to force Z3 to use the old front-end. Moreover, the old front-end is not fully compliant with SMT-LIB 2.0. So, you must write:

(set-option ELIM_QUANTIFIERS true)
(declare-fun y () Real)
(simplify (exists ((x Real)) (>= x y)))