CODEWITHSUNDEEP
z3smt
chansey
chansey

Reputation: 1429

What is `root-object` in z3 with Real theory?

I tried QF_NRA in z3 and it gave me an abstract value about root-obj.

(set-logic QF_NRA)
(declare-const x Real)
(assert (= 2 (* x x)))
(check-sat)
sat
(get-model)
(
  (define-fun x () Real
    (root-obj (+ (^ x 2) (- 2)) 1))
)

I don’t quite understand its meaning.

In addition, the x seems defined in recursion but not by define-fun-rec.

Thanks.

Upvotes: 1

Views: 298

Answers (1)

alias
alias

Reputation: 30525

Algebraic reals

Z3's Real theory supports what's known as algebraic reals. That is, it can express solutions in terms of the roots of polynomials with rational (equivalently, integer) valued coefficients. Note that such a polynomial can have complex roots. Z3 only supports those roots that are real, i.e., those with an imaginary part of 0. An algebraic real is essentially the real-root of a univariate polynomial with integer coefficients.

Dealing with root-obj's

In the example you posted, you're asking z3 to find a satisfying model for x*x == 2. And it's telling you that the solution is "a" zero-of-the polynomial (+ (^ x 2) (- 2)), or written in more familiar notation P(x) = x^2 -2. The index you get is 1 (the second argument to the root-obj), which says it's the "first" real-root of this polynomial. If you ask z3 to give you another solution, it'll give you the next one:

(set-logic QF_NRA)
(declare-const x Real)
(assert (= 2 (* x x)))
(assert (distinct x (root-obj (+ (^ x 2) (- 2)) 1)))
(check-sat)
(get-model)

This prints:

sat
(
  (define-fun x () Real
    (root-obj (+ (^ x 2) (- 2)) 2))
)

As you see, the "next" solution is the second root. What if we assert we want yet another solution?

(set-logic QF_NRA)
(declare-const x Real)
(assert (= 2 (* x x)))
(assert (distinct x (root-obj (+ (^ x 2) (- 2)) 1)))
(assert (distinct x (root-obj (+ (^ x 2) (- 2)) 2)))
(check-sat)

This prints:

unsat

as expected.

Note that algebraic reals do not include numbers such as pi, e, etc., i.e., they do not include transcendentals. Only those real numbers that can be expressed as the root of polynomials with integer coefficients. Leonardo's paper from 2012 explains this in great detail.

Getting approximations

z3 also allows you to get an approximation for such a root-obj solution, with as arbitrary a precision as you like. To do so, use the incantation:

(set-option :pp.decimal true)
(set-option :pp.decimal_precision 20)

where 20 in the second line is how many digits of precision you'd like, and you can change it as you see fit. If you add these two lines to your original script, z3 will respond:

sat
(
  (define-fun x () Real
    (- 1.4142135623730950?))
)

Note the ? at the end of the number. This is z3's way of telling you that the number it printed is an "approximation" to the value, i.e., it isn't the precise result.

A note on "recursion"

Your question suggests maybe x is defined recursively. This isn't the case. It just happens that you picked the variable name to be x and z3 always uses the letter x for the polynomial as well. If you picked y as the variable, you'd still get the exact same answer; the parameter to the polynomial has nothing to the with the variables in your program.

Upvotes: 3

Related Questions