Decidable sqrt function in Z3

Question

Since disabling unsound simplification of root objects, Z3 will now fail on this simple model involving a square root:

(define-fun sqrt ((x Real)) Real (^ x 0.5))
(declare-fun y () Real)
(declare-fun x () Real)
(assert (= y (sqrt x)))
(check-sat)

This returns sat with Z3 4.4.1, but unknown with master. If I change the problem definition to use is_sqrt as defined by Nikolaj in this question, then Z3 master will return sat. The approach using is_sqrt shows that all real roots can be pushed into QF_NRA by introducing auxiliary variables, so I think Z3 should be able to solve all problems involving roots over the reals.

How can I define a square-root function in the reals that will result in a decidable theory, assuming the rest of the model is in QF_NRA?

Answer 1

There is a subtle difference between (assert (= y (^ x 0.5))) and (assert (and (= x (* y y)) (> y 0.0))). The difference comes from the requirement that all functions in Z3 (and SMT-LIB) are total. This means, for example, that y=1/x, x=0 is considered satisfiable. Given that ^ is total in Z3, (assert (and (= y (^ x 0.5)) (< x 0.0))) is considered satisfiable. We can't convert (= y (^ x 0.5)) to (and (= x (* y y)) (> y 0.0)), because if x < 0 then the former is considered satisfiable but the latter is unsatisfiable. Similarly, any sqrt function defined within SMT-LIB would also be total, so we cannot define a sqrt function by any other means such that (assert (= y (sqrt x))) is equivalent to (assert (and (= x (* y y)) (> y 0.0))). In addition to the above difference as to whether or not y = sqrt(x), x < 0 (pseudocode) is considered satisfiable, it is also the case that (assert (and (= x (* y y)) (> y 0.0))) is decidable (it is in QF_NRA), while (assert (= y (^ x 0.5))) is not.

The solution for my purpose is to not use a Z3 or SMT-LIB function definition for the square-root. Instead, I will use statements of the form (assert (and (= x (* y y)) (> y 0.0))) to indicate that y is the square-root of x. Such assertions are within QF_NRA, so models built in this way will be decidable. Furthermore, this has the advantage that y = sqrt(x), x < 0 (pseudocode) will return unsat if it is represented in SMT-LIB via the statements (assert (and (= x (* y y)) (> y 0.0))) and (assert (< x 0.0)). To return unsat for this example is more in-line with my use case.