Add a new method toRational() to NumeralFormulaManager

[daniel-raffler]

Hello everyone,
in this PR we will add a new method toRational() to the NumeralFormulaManager. It is the counterpart to floor (= to_int in SMTLIB) and will turn an integer formula into a rational formula. While we've handled the conversion internally so far, having a way to create to_real terms directly is useful in the visitor

[kfriedberger]

I only find one use-case for an explicit conversion from INT to REAL: The DIV operator will produce an INT for INT, but a fraction (REAL) for REAL.

Could we add a test for that? For example, we could check:

• 5/2 == 2
• toReal(5)/toReal(2) == 2.5

If this conversion is already handled in imgr.divide/rmgr.divide, then I do not yet see any reason to add this casting. we can simply skip the casting operator and visit its child.

[daniel-raffler]

I only find one use-case for an explicit conversion from INT to REAL: The DIV operator will produce an INT for INT, but a fraction (REAL) for REAL.

Could we add a test for that? For example, we could check:

* 5/2 == 2

* toReal(5)/toReal(2) == 2.5

If this conversion is already handled in imgr.divide/rmgr.divide, then I do not yet see any reason to add this casting. we can simply skip the casting operator and visit its child.

I've added the test in 1f747cf, and JavaSMT does add the necessary casts automatically

The reason I wanted the function is that we have to rebuild formulas in #505 that will often use to_real for several solvers. Currently there is no direct counter part for to_real in JavaSMT, and just skipping the conversion also won't work. However, it's should be possible to rebuild most of these formulas in JavaSMT so that the to_real will be added automatically in just the right places. It's just that the bottom-up nature of FormulaTransformationVisitor makes this a bit difficult..

[daniel-raffler]

I'm now replacing (to_real a) with a unary sum (+ a), which will add the necessary conversion automatically