Allow users to build new rounding mode formulas

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

@@ -2,12 +2,13 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
 package org.sosy_lab.java_smt.api;
 
+import static org.sosy_lab.java_smt.api.FormulaManager.API_METHOD_NOT_IMPLEMENTED;
 import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointType;
 
 import java.math.BigDecimal;
@@ -34,6 +35,19 @@
  */
 public interface FloatingPointFormulaManager {
 
+  /** Creates a formula for the given floating point rounding mode. */
+  FloatingPointRoundingModeFormula makeRoundingMode(FloatingPointRoundingMode pRoundingMode);
+
+  /**
+   * Converts a rounding mode formula to the corresponding enum value. This method is the inverse of
+   * {@link #makeRoundingMode(FloatingPointRoundingMode)}.
+   */
+  @SuppressWarnings("unused")
+  default FloatingPointRoundingMode fromRoundingModeFormula(
+      FloatingPointRoundingModeFormula pRoundingModeFormula) {
+    throw new UnsupportedOperationException(API_METHOD_NOT_IMPLEMENTED);
+  }
+
   /**
    * Creates a floating point formula representing the given double value with the specified type.
    */

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

@@ -2,13 +2,17 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
 package org.sosy_lab.java_smt.api;
 
-/** Possible floating point rounding modes. */
+/**
+ * Represents the various rounding modes that can be applied when converting or manipulating
+ * floating-point values and formulas. These modes define how results are rounded when an exact
+ * representation is not possible due to precision limits of the target format.
+ */
 public enum FloatingPointRoundingMode {
   NEAREST_TIES_TO_EVEN,
   NEAREST_TIES_AWAY,

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

@@ -11,8 +11,15 @@
 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.
+ *
+ * <p>This class is rarely used in the API but necessary to support visitor traversal of formulas
+ * with certain floating-point operations, where JavaSMT provides the rounding mode as Formula-based
+ * argument.
  */
 @Immutable
 public interface FloatingPointRoundingModeFormula extends Formula {}

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

@@ -20,6 +20,16 @@
 /** FormulaManager class contains all operations which can be performed on formulas. */
 public interface FormulaManager {
 
+  /**
+   * Standardized message for not implemented API methods.
+   *
+   * <p>This constant can be used in {@link UnsupportedOperationException} to indicate that a
+   * certain method is not implemented by some subclass. We recommend using this constant in API
+   * extensions where the default implementation throws an exception.
+   */
+  String API_METHOD_NOT_IMPLEMENTED =
+      "The requested method is not implemented in the current implementation of this interface.";
+
   /**
    * Returns the Integer-Theory. Because most SAT-solvers support automatic casting between Integer-
    * and Rational-Theory, the Integer- and the RationalFormulaManager both return the same Formulas

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

@@ -261,21 +261,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,18 @@ private TFormulaInfo getRoundingMode(FloatingPointRoundingMode pFloatingPointRou
     return roundingModes.computeIfAbsent(pFloatingPointRoundingMode, this::getRoundingModeImpl);
   }
 
+  @Override
+  public FloatingPointRoundingModeFormula makeRoundingMode(
+      FloatingPointRoundingMode pRoundingMode) {
+    return getFormulaCreator().encapsulateRoundingMode(getRoundingMode(pRoundingMode));
+  }
+
+  @Override
+  public FloatingPointRoundingMode fromRoundingModeFormula(
+      FloatingPointRoundingModeFormula pRoundingModeFormula) {
+    return getFormulaCreator().getRoundingMode(extractInfo(pRoundingModeFormula));
+  }
+
   protected FloatingPointFormula wrap(TFormulaInfo pTerm) {
     return getFormulaCreator().encapsulateFloatingPoint(pTerm);
   }

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

@@ -31,6 +31,7 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.EnumerationFormula;
 import org.sosy_lab.java_smt.api.FloatingPointFormula;
+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;
@@ -134,6 +135,16 @@ public final TType getRegexType() {
     return regexType;
   }
 
+  public FloatingPointRoundingMode getRoundingMode(FloatingPointRoundingModeFormula f) {
+    return getRoundingMode(extractInfo(f));
+  }
+
+  @SuppressWarnings("unused")
+  protected FloatingPointRoundingMode getRoundingMode(TFormulaInfo f) {
+    throw new UnsupportedOperationException(
+        "Floating point rounding modes are not supported by this solver.");
+  }
+
   public abstract TFormulaInfo makeVariable(TType type, String varName);
 
   public BooleanFormula encapsulateBoolean(TFormulaInfo pTerm) {
@@ -160,6 +171,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,23 @@ 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 FloatingPointRoundingMode fromRoundingModeFormula(
+      FloatingPointRoundingModeFormula pRoundingModeFormula) {
+    debugging.assertThreadLocal();
+    debugging.assertFormulaInContext(pRoundingModeFormula);
+    return delegate.fromRoundingModeFormula(pRoundingModeFormula);
+  }
+
   @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,20 @@ class StatisticsFloatingPointFormulaManager implements FloatingPointFormulaManag
     stats = checkNotNull(pStats);
   }
 
+  @Override
+  public FloatingPointRoundingModeFormula makeRoundingMode(
+      FloatingPointRoundingMode pRoundingMode) {
+    stats.fpOperations.getAndIncrement();
+    return delegate.makeRoundingMode(pRoundingMode);
+  }
+
+  @Override
+  public FloatingPointRoundingMode fromRoundingModeFormula(
+      FloatingPointRoundingModeFormula pRoundingModeFormula) {
+    stats.fpOperations.getAndIncrement();
+    return delegate.fromRoundingModeFormula(pRoundingModeFormula);
+  }
+
   @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,22 @@ class SynchronizedFloatingPointFormulaManager implements FloatingPointFormulaMan
     sync = checkNotNull(pSync);
   }
 
+  @Override
+  public FloatingPointRoundingModeFormula makeRoundingMode(
+      FloatingPointRoundingMode pRoundingMode) {
+    synchronized (sync) {
+      return delegate.makeRoundingMode(pRoundingMode);
+    }
+  }
+
+  @Override
+  public FloatingPointRoundingMode fromRoundingModeFormula(
+      FloatingPointRoundingModeFormula pRoundingModeFormula) {
+    synchronized (sync) {
+      return delegate.fromRoundingModeFormula(pRoundingModeFormula);
+    }
+  }
+
   @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,7 @@ public Object convertValue(Term term) {
       return term.to_bool();
     }
     if (sort.is_rm()) {
-      return term.to_rm();
+      return getRoundingMode(term);
     }
     if (sort.is_bv()) {
       return new BigInteger(term.to_bv(), 2);
@@ -627,4 +637,23 @@ public Collection<Term> getConstraintsForTerm(Term pTerm) {
 
     return transformedImmutableSetCopy(usedConstraintVariables, constraintsForVariables::get);
   }
+
+  @Override
+  protected FloatingPointRoundingMode getRoundingMode(Term term) {
+    checkArgument(term.sort().is_rm(), "Term '%s' is not of rounding mode sort.", term);
+    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 in Term '%s'.", term));
+    }
+  }
 }