Allow users to build new rounding mode formulas

[daniel-raffler]

Hello,
in this PR we add support to explicitly create new rounding mode formulas. So far this has not been possible and rounding-mode formulas were added internally when building new floating-point formulas. This leads to some issues when using visitors on floating-point formulas, as the rounding mode can not be changed when rebuilding the same formula. Let's take the term (fp.sqrt roundTowardPositive a) as an example. Here the rounding mode roundTowardPositive is represented as a FloatingPointRoundingModeFormula in JavaSMT and can in fact be visited. However, since there is no way to instantiate FloatingPointRoundingModeFormula, all the visitor can do is return the same rounding mode again. In the same way there is no way to access the FloatingPointRoundingModeFormula to see which rounding mode is being used by the term.

In this PR we add a new method makeRoundingMode(FloatingPointRoundingMode pRoundingMode) to FloatingPointFormulaManager that allows user to create new rounding mode formulas. We also fixed the visitor code in the backends to properly map solver rounding mode values to JavaSMT rounding modes:

mgr.transformRecursively(t, new FormulaVisitor<Formula>() {
  @Override
  public Formula visitConstant(Formula f, Object value) {
    if(f instanceof FloatingPointRoundingModeFormula && value instanceof FloatingPointRoundingMode) {
      // Switch the rounding mode to "neareast-ties-to-even"
      return fpmgr.makeRoundingMode(FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN);
    } else {
      return f;
    }
  }
}

[kfriedberger]

Thanks for noticing and implementing this long-term issue. Roundingmode was clearly a topic that missed some support.

The changes are fine, except two points:

• we only use the existing tests, and I see no new tests. Could you add some test?
• removing public fields from the enum FormulaDeclarationKind is not backwards-compatible, and there was an API change in one method. This is negligible, as we already prepare several API changes within the next release.

[daniel-raffler]

Thanks! I'll add some test later today

[daniel-raffler]

Should we add a function to get the rounding mode from a rounding mode formula? We currently have to do something like this, which is rather awkward:

private FloatingPointRoundingMode getRoundingMode(
    FloatingPointRoundingModeFormula pRoundingModeFormula) {
  return visit(
      pRoundingModeFormula,
      new DefaultFormulaVisitor<>() {
        @Override
        protected FloatingPointRoundingMode visitDefault(Formula f) {
          throw new IllegalStateException();
        }

        @Override
        public FloatingPointRoundingMode visitConstant(Formula f, Object value) {
          return (FloatingPointRoundingMode) value;
        }
      });
}

Alternatively we could change the API in FloatingPointFormulaManager to require rounding mode formulas, instead of rounding modes as arguments. So, for instance:

FloatingPointFormula sqrt(FloatingPointFormula number, FloatingPointRoundingMode roundingMode);

would become:

FloatingPointFormula sqrt(FloatingPointFormula number, FloatingPointRoundingModeFormula roundingMode);

The original API could then be restored with a default implementation:

default FloatingPointFormula sqrt(FloatingPointFormula number, FloatingPointRoundingMode rm) {
  return sqrt(number, makeRoundingMode(rm));
}

[daniel-raffler]

Another way to implement this is to use indices for the rounding mode. So (fp.sqrt rm f) becomes ((_ fp.sqrt rm) f) and the round mode argument is tucked away from the user. This may be more intuitive as the operations now have the right number of arguments (1 for sqrt, 2 for add, etc) and all arguments are floating point formulas.

The downside is that indices have to be constant, so something like ((_ fp.sqrt (ite c roundTowardNegative roundTowardPositive) f) would not work. On the other hand such cases are rare, and it should always be possible to lift the operation: (ite c ((_ fp.sqrt roundTowardNegative) f) ((_ fp.sqrt roundTowardPositive) f)