The output contains three algebraic numbers. For example, R
is assigned to the 2nd root/zero of the polynomial x^2 - 130 x - 2000
. This is a precise representation for irrational numbers that are zeros of polynomials. It may be hard to interpret. Thus, we can also ask Z3 to display the result using decimal notation.
(set-option :pp-decimal true)
Z3 will append a ?
to denote that the output is truncated.
Here is the same problem with this option. With this option, we get the following output:
sat
(model
(define-fun R () Real
143.8986691902?)
(define-fun I1 () Real
0.0106497781?)
(define-fun I2 () Real
0.0032488909?)
(define-fun V2 () Real
0.5)
(define-fun V1 () Real
1.0)
(define-fun Vo () Real
(- 2.0))
(define-fun g () Real
(- 2.0))
)