feat: Exact precision representable reals

[tiferrei]

⚠️ WORK IN PROGRESS ⚠️

This PR aims to add exact precision real support for the rationals. (#464)
It does so mostly through Value.real = Exact of Q.t | Approx of float

As already mentioned before, this has interesting consequences when it comes to conversions and comparison.

Design Decisions

Here is an (expanding) list of design decisions made that I would like to discuss:

• Approx is sticky, i.e., operations with approximates do not return exacts.
• The point above applies to comparisons: comparisons involving approx(s) are done with floats.
• OfString / ToString are specific to the representation. 1.5 gets parsed to an Approx, 3/2 to an Exact.
• String_to_float does what it says on the tin: gives you a float, i.e., an Approx. We may want to change this to a String_to_real.
• Real.sqrt returns Exact on perfect square num/den, Approx otherwise.
• Real.pow is lossy, and always returns Approx. This can be improved, but requires some care.

TODO

• Tests: Exact reals in binop tests.
• Tests: Exact reals in relop tests.
• Tests: Real tests between approx and exact.
• Tests: Fix smt2 tests.
• Documentation: Real type and its implications.
• Mappings: CVC5.
• Mappings: bitwuzla.
• Mappings: colibri2.
• Mappings: alt-ergo.
• Formatting / Linting.

PS: I am generally not experienced with Smtml, or even OCaml. I would appreciate any and all feedback you have for improving the code. Thanks again for this project! :)

[filipeom]

Thank you for doing this! I'm a bit overwhelmed this week so I will try to review and give more feedback later on the week.

[redianthus]

I am wondering if there is actually a need to keep the Approx of float thing instead of directly removing it and only have | Real of Q.t. What is the use-case for it? To me it seems sufficient to have Q.t if you provide a of_float operation. What do you think?

[tiferrei]

My initial thinking was that, as there are many operations that are not closed over the rationals, such as pow and sqrt, it would be good to have indication of when precision is lost, and the real value is no longer present.

That being said, this is all dependent on the mappings of the solvers providing such information. If at the end of the day the solvers always provide a "forced" Q.t for reals (or a forced float instead) then there is no point in having the distinction.

However I really am not familiar how solvers like CVC5 and Z3 behave in these cases, and the guarantees of the format of their outputs.