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