pp.decimal for cos, sin, acos, asin, and pi

[dstaple]

I'm wondering if/how we could add pretty-printing with pp.decimal for cos, sin, acos, asin, and pi. Z3 will leave expressions such as (cos 0.1) unevaluated when returning a model from get-model or get-value, because they cannot be evaluated exactly. However, if we have (set-option :pp.decimal true), then we should be able to evaluate these expressions.

Currently this input:

(set-option :pp.decimal true)
(declare-const my_cos Real)
(declare-const my_sin Real)
(declare-const my_acos Real)
(declare-const my_asin Real)
(declare-const my_pi Real)
(assert (= my_cos (cos 0.1)))
(assert (= my_sin (sin 0.1)))
(assert (= 0.1 (cos my_acos)))
(assert (= 0.1 (sin my_asin)))
(assert (= my_pi pi))
(check-sat-using qfnra-nlsat)
(get-value (my_cos my_sin my_acos my_asin my_pi))
(get-model)

produces this output:

sat
((my_cos (cos 0.1))
 (my_sin (sin 0.1))
 (my_acos (+ (acos (- 0.1)) pi))
 (my_asin (acos (- 0.9949874371?)))
 (my_pi pi))

Ideally, the output would be something like:

sat
((my_cos 0.9950041652?)
 (my_sin 0.0998334166?)
 (my_acos 1.4706289056?)
 (my_asin 0.1001674211?)
 (my_pi 3.1415926535?))

[dstaple]

For rationals, the relevant method is mpq_manager::display_decimal located in src/util/mpq.cpp. For algebraic numbers, the display_decimal method is defined in src/math/polynomial/algebraic_numbers.cpp. There are similar methods defined for floating-point numbers, and other sorts. So, it seems to me that I need to implement or modify a display_decimal method. I'm going to trace through and see which display_decimal method is hit when I give the above example involving trig, and see if it can be modified to accomplish the above.

[dstaple]

I'm surprised to find that there are already methods not only for pretty-printing pi, but also for computing increasingly narrow bounds for pi. This can be seen by building the unit tests shipped with the Z3 source, and running ./test-z3 interval and ./test-z3 rcf from the build directory. Relevant source and test files include:

    src/math/realclosure/realclosure.cpp
    src/test/rcf.cpp
    src/test/trigo.cpp
    src/test/interval.cpp

Computing increasingly narrow bounds like this makes a lot of sense not only for pretty-printing, but also for proving inequalities mixing rational, algebraic, and transcendental numbers. This raises a few questions: 1) Why doesn't pp.decimal work for printing an approximate value of pi from the SMT-LIB interface, given that methods are already implemented to do this? This seems like a bug. 2) Why can't Z3 prove e.g. pi < 4 using this mechanism? Currently (assert (< 4 pi)) (check-sat) returns unknown. 3) It seems that I could define similar interval-refinement methods that would permit not only pretty-printing trig values, e.g. cos(0.1), but also prove statements such as cos(0.1) > 0.995.

[NikolajBjorner]

There are several goodies for real-closure operations. There is also a paper at CADE 2013, http://research.microsoft.com/en-us/um/people/leonardo/files/CADE2013.pdf, by Leo and Grant describing background. As you point out there is potential to leverage these features for many things that are not available. Possibly, improving evaluation over transcendental numerals could be one thing. Currently, the algebraic numerals (roots of polynomials whose coefficients may be other algebraic numerals), stand alone. The sine function (interval.h) can be evaluated up to some prescribed precision over abstract numeral classes (very likely, algebraic numerals will work, but I am not sure if this was done before). For interval reasoning, the infinite precision symbolic representation would likely be super slow. AFAIK tools such as iSAT and DReal use floating points when they do interval reasoning. Done properly it is a non-trivial extension (but as noted first, many goodies are already in place and makes the overall task much more bearable than a cold bootstrap).

[pcarbonn]

The ksmt solver supports transcendental functions. See their paper. It would be great if Z3 supported them too.