Handling real number formulas

[raner]

I am using JavaSMT in an experimental programming language to detect type constraints and logic errors at compile time. Notably, this language does not use floating point arithmetic but actual real numbers that are implemented by a symbolic math library. This means, for example, that (1/3)*6 == 2 (exactly, no rounding errors) or sqrt(5)*sqrt(125) == 25 (again, exactly). I am planning on using FloatingPointFormulaManager for the constraint validation of real numbers, but if the underlying solvers actually implement this using floating-point numbers, this seems inherently wrong. A lot of the common constraints have to do with zero versus nonzero or negative versus nonnegative numeric validation. For example, when validating the divisor in a division operation, rounding errors might lead to a result of 0.00000017 during compile-time constraint checking (!= 0, hence deemed valid), whereas at runtime the symbolic evaluation yields exactly zero, which would cause a runtime division-by-zero error. Are there any alternatives for validating constraints on "real real" numbers? Or will certain solvers actually employ exact symbolic calculations when implementing FloatingPointFormula?

[kfriedberger]

Hi @raner . it seems as if your question is not about JavaSMT, but rather about the underlying SMT theory of Reals/Rationals and FloatingPoint numbers.

The theory of Reals is based on simple math (like (1/3)*6==2). There is no rounding and no precision (you could also say: infinite precision). The theory of FloatingPoint uses a given precision with only a few bits (like float or double in typical computer architectures). Each operation can round or cut of bits during the computation.

JavaSMT has separate APIs for theories (like RationalFormulaManager and FloatingPointFormulaManager). We do not (directly) allow to combine them in mathematical operations (like sum or multiplication). Each SMT solver only provides its supported features. We do not replace or re-model theories within JavaSMT.

I did not yet understand how you want to include rounding errors into the formula encoding. This needs to be done on user-side, if required.

[raner]

Thanks for your quick response, @kfriedberger :-) I don't want to model rounding errors, I'm only interested in what you've called so aptly "infinite precision." RationalFormulaManager seems to solve my first example ((1/3)*6==2), but I don't think it addresses my second example (sqrt(5)*sqrt(125) == 25), because square roots are not rational numbers. If I model this case using either RationalFormulaManager or FloatingPointFormulaManager I might have rounding errors at compile time, and those rounding errors could possibly allow calculations that would fail at runtime (which works with unlimited precision). For example, I could have an invalid calculation like

        x
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
(√5̅ × √1̅2̅5̅) - 25

or even

        x
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 (√n̅ × √n̅³̅) - n²

If I model these with either RationalFormulaManager or FloatingPointFormulaManager I don't think that the compile-time results (formula is considered valid) would match the runtime results (division by zero error).

Is there something like RealFormulaManager? Are there SMT solvers that actually support the concept of real numbers (ℝ)? If so, could something like RealFormulaManager be created? Or are you saying that RationalFormulaManager would actually behave the way I intend (i.e., it would effectively provide a "Reals" theory)?

[kfriedberger]

Please consider different definitions of and support for "Reals":

• SMT-LIB has a definition of "Reals" (see https://smt-lib.org/theories-Reals.shtml), including a definition of division-by-zero and irrational algebraic number (I have never seen this in the implementation).
• The mathematical concept of "R" (real numbers) inludes irrational algebraic numbers like PI, e, sqrt(2), and such stuff.
• SMT solvers mostly only support rational numbers (all numbers in form n/m where n,m are integers), but call the theory "real".

JavaSMT does provide a RationalNumberManager that supports only Rationals. With the missing support for real numbers in SMT solvers, we do currently not plan to provide a RealNumberManager.

[raner]

Thanks for clarifying, @kfriedberger - if the concept of real (including irrational) numbers is not supported by the underlying solvers, then it obviously doesn't make sense to model this in JavaSMT. I'm therefore closing this issue.

I appreciate the quick response and good discussion! Thank you very much.