Does Z3 v4.3+ support quantifier elimination for NON-linear arithmetic

Question

I could not find out what kind of quantifier elimination Z3 fully supports. What I have is a universally quantified formula over -in general- non-linear terms. I would like to obtain an equivalent quantifier free formula. Is that possible with Z3?

Thanks, Friedrich

Answer 1

Z3 has very limited support for quantifier elimination of nonlinear arithmetic. Moreover, it is not enabled by default. Here is an example on how to enable it, and demonstrating the limitations. It is also available online here.

(set-option :pp-max-depth 20) ;; set option for Z3 pretty printer
(declare-const a Real)
(assert (exists ((x Real)) (= (* x x) a )))
(apply qe)
(echo "enabling nonlinear support...")
(apply (! qe :qe-nonlinear true))
;; It is very limited, it will fail in the following example
(echo "trying a cubic polynomial...")
(assert (exists ((x Real)) (= (* x x x) a)))
(apply (! qe :qe-nonlinear true))