z3 existential theory of the reals

问题:

Does Z3 decide the existential fragment of nonlinear real arithmetic? That is, can I use it as a decision procedure for testing whether a quantifier-free formula with + and x has a solution over the reals?

回答1:

Yes, Z3 has a decision procedure for the existential fragment of nonlinear polynomial real arithmetic. Of course, the procedure is complete modulo available resources. The procedure is quite expensive. This article describes the procedure implemented in Z3.

Here is a small example (also available online here):

(declare-const a Real)
(declare-const b Real)
(assert (= (^ a 5) (+ a 1)))
(assert (= (^ b 3) (+ (^ a 2) 1)))
(check-sat)
(get-model) 
(set-option :pp-decimal true) ;; force Z3 to display the result in decimal notation
(get-model)

Here is a related question:

• Z3 support for nonlinear arithmetic