Allow users to build new rounding mode formulas

src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java

@@ -34,6 +34,9 @@
  */
 public interface FloatingPointFormulaManager {
 
+  /** Creates a formula for the given floating point rounding mode. */
+  FloatingPointRoundingModeFormula makeRoundingMode(FloatingPointRoundingMode pRoundingMode);
+
   /**
    * Creates a floating point formula representing the given double value with the specified type.
    */

src/org/sosy_lab/java_smt/api/FloatingPointRoundingModeFormula.java

@@ -11,8 +11,11 @@
 import com.google.errorprone.annotations.Immutable;
 
 /**
- * Formula representing a rounding mode for floating-point operations. This is currently unused by
- * the API but necessary for traversal of formulas with such terms.
+ * Formula representing a rounding mode for floating-point operations.
+ *
+ * <p>Rounding mode formulas are used by floating-point formulas to select the rounding mode for the
+ * operation. Use {@link FloatingPointFormulaManager#makeRoundingMode(FloatingPointRoundingMode)} to
+ * wrap a {@link org.sosy_lab.java_smt.api.FloatingPointRoundingMode} value inside a new formula.
  */
 @Immutable
 public interface FloatingPointRoundingModeFormula extends Formula {}

src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java

@@ -252,21 +252,6 @@ public enum FunctionDeclarationKind {
   /** Equal over floating points. */
   FP_EQ,
 
-  /** Rounding over floating points. */
-  FP_ROUND_EVEN,
-
-  /** Rounding over floating points. */
-  FP_ROUND_AWAY,
-
-  /** Rounding over floating points. */
-  FP_ROUND_POSITIVE,
-
-  /** Rounding over floating points. */
-  FP_ROUND_NEGATIVE,
-
-  /** Rounding over floating points. */
-  FP_ROUND_ZERO,
-
   /** Rounding over floating points. */
   FP_ROUND_TO_INTEGRAL,
 

src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java

@@ -22,6 +22,7 @@
 import org.sosy_lab.java_smt.api.FloatingPointFormulaManager;
 import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign;
 import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
+import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
@@ -60,6 +61,12 @@ private TFormulaInfo getRoundingMode(FloatingPointRoundingMode pFloatingPointRou
     return roundingModes.computeIfAbsent(pFloatingPointRoundingMode, this::getRoundingModeImpl);
   }
 
+  @Override
+  public FloatingPointRoundingModeFormula makeRoundingMode(
+      FloatingPointRoundingMode pRoundingMode) {
+    return getFormulaCreator().encapsulateRoundingMode(getRoundingMode(pRoundingMode));
+  }
+
   protected FloatingPointFormula wrap(TFormulaInfo pTerm) {
     return getFormulaCreator().encapsulateFloatingPoint(pTerm);
   }

src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java

@@ -160,6 +160,14 @@ protected FloatingPointFormula encapsulateFloatingPoint(TFormulaInfo pTerm) {
     return new FloatingPointFormulaImpl<>(pTerm);
   }
 
+  protected FloatingPointRoundingModeFormula encapsulateRoundingMode(TFormulaInfo pTerm) {
+    checkArgument(
+        getFormulaType(pTerm).isFloatingPointRoundingModeType(),
+        "Floatingpoint rounding mode formula has unexpected type: %s",
+        getFormulaType(pTerm));
+    return new FloatingPointRoundingModeFormulaImpl<>(pTerm);
+  }
+
   protected <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> encapsulateArray(
       TFormulaInfo pTerm, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
     checkArgument(

src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java

@@ -17,6 +17,7 @@
 import org.sosy_lab.java_smt.api.FloatingPointFormulaManager;
 import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign;
 import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
+import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
@@ -31,6 +32,15 @@ public class DebuggingFloatingPointFormulaManager implements FloatingPointFormul
     debugging = pDebugging;
   }
 
+  @Override
+  public FloatingPointRoundingModeFormula makeRoundingMode(
+      FloatingPointRoundingMode pRoundingMode) {
+    debugging.assertThreadLocal();
+    FloatingPointRoundingModeFormula result = delegate.makeRoundingMode(pRoundingMode);
+    debugging.addFormulaTerm(result);
+    return result;
+  }
+
   @Override
   public FloatingPointFormula makeNumber(double n, FloatingPointType type) {
     debugging.assertThreadLocal();

src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java

@@ -19,6 +19,7 @@
 import org.sosy_lab.java_smt.api.FloatingPointFormulaManager;
 import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign;
 import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
+import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
@@ -34,6 +35,13 @@ class StatisticsFloatingPointFormulaManager implements FloatingPointFormulaManag
     stats = checkNotNull(pStats);
   }
 
+  @Override
+  public FloatingPointRoundingModeFormula makeRoundingMode(
+      FloatingPointRoundingMode pRoundingMode) {
+    stats.fpOperations.getAndIncrement();
+    return delegate.makeRoundingMode(pRoundingMode);
+  }
+
   @Override
   public FloatingPointFormula makeNumber(double pN, FloatingPointType pType) {
     stats.fpOperations.getAndIncrement();

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java

@@ -19,6 +19,7 @@
 import org.sosy_lab.java_smt.api.FloatingPointFormulaManager;
 import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign;
 import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
+import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
@@ -35,6 +36,14 @@ class SynchronizedFloatingPointFormulaManager implements FloatingPointFormulaMan
     sync = checkNotNull(pSync);
   }
 
+  @Override
+  public FloatingPointRoundingModeFormula makeRoundingMode(
+      FloatingPointRoundingMode pRoundingMode) {
+    synchronized (sync) {
+      return delegate.makeRoundingMode(pRoundingMode);
+    }
+  }
+
   @Override
   public FloatingPointFormula makeNumber(double pN, FloatingPointType pType) {
     synchronized (sync) {

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java

@@ -33,6 +33,8 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.FloatingPointFormula;
 import org.sosy_lab.java_smt.api.FloatingPointNumber;
+import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
+import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
@@ -131,6 +133,14 @@ assert getFormulaType(pTerm).isFloatingPointType()
     return new BitwuzlaFloatingPointFormula(pTerm);
   }
 
+  @Override
+  protected FloatingPointRoundingModeFormula encapsulateRoundingMode(Term pTerm) {
+    assert getFormulaType(pTerm).isFloatingPointRoundingModeType()
+        : String.format(
+            "%s is no FP rounding mode, but %s (%s)", pTerm, pTerm.sort(), getFormulaType(pTerm));
+    return new BitwuzlaFloatingPointRoundingModeFormula(pTerm);
+  }
+
   @Override
   @SuppressWarnings("MethodTypeParameterName")
   protected <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> encapsulateArray(
@@ -584,7 +594,19 @@ public Object convertValue(Term term) {
       return term.to_bool();
     }
     if (sort.is_rm()) {
-      return term.to_rm();
+      if (term.is_rm_value_rna()) {
+        return FloatingPointRoundingMode.NEAREST_TIES_AWAY;
+      } else if (term.is_rm_value_rne()) {
+        return FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN;
+      } else if (term.is_rm_value_rtn()) {
+        return FloatingPointRoundingMode.TOWARD_NEGATIVE;
+      } else if (term.is_rm_value_rtp()) {
+        return FloatingPointRoundingMode.TOWARD_POSITIVE;
+      } else if (term.is_rm_value_rtz()) {
+        return FloatingPointRoundingMode.TOWARD_ZERO;
+      } else {
+        throw new IllegalArgumentException(String.format("Unknown rounding mode: %s", term));
+      }
     }
     if (sort.is_bv()) {
       return new BigInteger(term.to_bv(), 2);

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java

@@ -26,6 +26,7 @@
 import edu.stanford.CVC4.Integer;
 import edu.stanford.CVC4.Kind;
 import edu.stanford.CVC4.Rational;
+import edu.stanford.CVC4.RoundingMode;
 import edu.stanford.CVC4.Type;
 import edu.stanford.CVC4.vectorExpr;
 import edu.stanford.CVC4.vectorType;
@@ -41,6 +42,8 @@
 import org.sosy_lab.java_smt.api.FloatingPointFormula;
 import org.sosy_lab.java_smt.api.FloatingPointNumber;
 import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign;
+import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
+import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
@@ -264,6 +267,15 @@ assert getFormulaType(pTerm).isFloatingPointType()
     return new CVC4FloatingPointFormula(pTerm);
   }
 
+  @Override
+  protected FloatingPointRoundingModeFormula encapsulateRoundingMode(Expr pTerm) {
+    assert getFormulaType(pTerm).isFloatingPointRoundingModeType()
+        : String.format(
+            "%s is no FP rounding mode, but %s (%s)",
+            pTerm, pTerm.getType(), getFormulaType(pTerm));
+    return new CVC4FloatingPointRoundingModeFormula(pTerm);
+  }
+
   @Override
   @SuppressWarnings("MethodTypeParameterName")
   protected <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> encapsulateArray(
@@ -323,8 +335,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Expr f) {
       } else if (type.isFloatingPoint()) {
         return visitor.visitConstant(formula, convertFloatingPoint(f));
       } else if (type.isRoundingMode()) {
-        // TODO is this correct?
-        return visitor.visitConstant(formula, f.getConstRoundingMode());
+        return visitor.visitConstant(formula, convertRoundingMode(f));
       } else if (type.isString()) {
         return visitor.visitConstant(formula, f.getConstString());
       } else if (type.isArray()) {
@@ -613,6 +624,9 @@ public Object convertValue(Expr expForType, Expr value) {
     } else if (valueType.isFloatingPoint()) {
       return convertFloatingPoint(value);
 
+    } else if (valueType.isRoundingMode()) {
+      return convertRoundingMode(value);
+
     } else if (valueType.isString()) {
       return unescapeUnicodeForSmtlib(value.getConstString().toString());
 
@@ -648,4 +662,21 @@ private FloatingPointNumber convertFloatingPoint(Expr fpExpr) {
         expWidth,
         mantWidth);
   }
+
+  private FloatingPointRoundingMode convertRoundingMode(Expr pExpr) {
+    RoundingMode rm = pExpr.getConstRoundingMode();
+    if (rm.equals(RoundingMode.roundNearestTiesToAway)) {
+      return FloatingPointRoundingMode.NEAREST_TIES_AWAY;
+    } else if (rm.equals(RoundingMode.roundNearestTiesToEven)) {
+      return FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN;
+    } else if (rm.equals(RoundingMode.roundTowardNegative)) {
+      return FloatingPointRoundingMode.TOWARD_NEGATIVE;
+    } else if (rm.equals(RoundingMode.roundTowardPositive)) {
+      return FloatingPointRoundingMode.TOWARD_POSITIVE;
+    } else if (rm.equals(RoundingMode.roundTowardZero)) {
+      return FloatingPointRoundingMode.TOWARD_ZERO;
+    } else {
+      throw new IllegalArgumentException(String.format("Unknown rounding mode: %s", pExpr));
+    }
+  }
 }

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java

@@ -27,6 +27,7 @@
 import io.github.cvc5.Kind;
 import io.github.cvc5.Op;
 import io.github.cvc5.Pair;
+import io.github.cvc5.RoundingMode;
 import io.github.cvc5.Solver;
 import io.github.cvc5.Sort;
 import io.github.cvc5.Term;
@@ -44,6 +45,8 @@
 import org.sosy_lab.java_smt.api.EnumerationFormula;
 import org.sosy_lab.java_smt.api.FloatingPointFormula;
 import org.sosy_lab.java_smt.api.FloatingPointNumber;
+import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
+import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
@@ -315,6 +318,15 @@ assert getFormulaType(pTerm).isFloatingPointType()
     return new CVC5FloatingPointFormula(pTerm);
   }
 
+  @Override
+  protected FloatingPointRoundingModeFormula encapsulateRoundingMode(Term pTerm) {
+    assert getFormulaType(pTerm).isFloatingPointRoundingModeType()
+        : String.format(
+            "%s is no FP rounding mode, but %s (%s)",
+            pTerm, pTerm.getSort(), getFormulaType(pTerm));
+    return new CVC5FloatingPointRoundingModeFormula(pTerm);
+  }
+
   @Override
   @SuppressWarnings("MethodTypeParameterName")
   protected <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> encapsulateArray(
@@ -399,7 +411,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
         return visitor.visitConstant(formula, convertFloatingPoint(f));
 
       } else if (f.isRoundingModeValue()) {
-        return visitor.visitConstant(formula, f.getRoundingModeValue());
+        return visitor.visitConstant(formula, convertRoundingMode(f));
 
       } else if (f.isConstArray()) {
         Term constant = f.getConstArrayBase();
@@ -816,6 +828,9 @@ public Object convertValue(Term expForType, Term value) {
       } else if (value.isFloatingPointValue()) {
         return convertFloatingPoint(value);
 
+      } else if (value.isRoundingModeValue()) {
+        return convertRoundingMode(value);
+
       } else if (value.isBooleanValue()) {
         return value.getBooleanValue();
 
@@ -845,6 +860,23 @@ private FloatingPointNumber convertFloatingPoint(Term value) throws CVC5ApiExcep
     return FloatingPointNumber.of(bits, expWidth, mantWidth);
   }
 
+  private FloatingPointRoundingMode convertRoundingMode(Term pTerm) throws CVC5ApiException {
+    RoundingMode rm = pTerm.getRoundingModeValue();
+    if (rm.equals(RoundingMode.ROUND_NEAREST_TIES_TO_AWAY)) {
+      return FloatingPointRoundingMode.NEAREST_TIES_AWAY;
+    } else if (rm.equals(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN)) {
+      return FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN;
+    } else if (rm.equals(RoundingMode.ROUND_TOWARD_NEGATIVE)) {
+      return FloatingPointRoundingMode.TOWARD_NEGATIVE;
+    } else if (rm.equals(RoundingMode.ROUND_TOWARD_POSITIVE)) {
+      return FloatingPointRoundingMode.TOWARD_POSITIVE;
+    } else if (rm.equals(RoundingMode.ROUND_TOWARD_ZERO)) {
+      return FloatingPointRoundingMode.TOWARD_ZERO;
+    } else {
+      throw new IllegalArgumentException(String.format("Unknown rounding mode: %s", pTerm));
+    }
+  }
+
   private Term accessVariablesCache(String name, Sort sort) {
     Term existingVar = variablesCache.get(name, sort.toString());
     Preconditions.checkNotNull(