improve documentation for FP operations and rounding.

Author: kfriedberger

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

@@ -19,29 +19,75 @@
  * <p>Most operations are overloaded: there is an option of either using the default rounding mode
  * (set via the option {@code solver.floatingPointRoundingMode}), or providing the rounding mode
  * explicitly.
+ *
+ * <p>If the result of an operation can not be exactly represented by the available floating-point
+ * type, i.e., the given precision is insufficient, the result is rounded to the nearest possible
+ * floating-point representation, depending on the given rounding mode.
+ *
+ * <p>Example: If the input number is too large to be represented as a floating point with the given
+ * type, it will be converted to positive infinity (+inf) or negative infinity (-inf). If the input
+ * number is too small to be represented with the given type (closer to zero than the smallest
+ * possible floating-point number), it will be converted to zero, with the sign preserved.
  */
 public interface FloatingPointFormulaManager {
 
+  /**
+   * Creates a floating point formula representing the given double value with the specified type.
+   */
   FloatingPointFormula makeNumber(double n, FloatingPointType type);
 
+  /**
+   * Creates a floating point formula representing the given double value with the specified type
+   * and rounding mode.
+   */
   FloatingPointFormula makeNumber(
       double n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode);
 
+  /**
+   * Creates a floating point formula representing the given BigDecimal value with the specified
+   * type.
+   */
   FloatingPointFormula makeNumber(BigDecimal n, FloatingPointType type);
 
+  /**
+   * Creates a floating point formula representing the given BigDecimal value with the specified
+   * type and rounding mode.
+   */
   FloatingPointFormula makeNumber(
       BigDecimal n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode);
 
+  /**
+   * Creates a floating point formula representing the given string value with the specified type.
+   */
   FloatingPointFormula makeNumber(String n, FloatingPointType type);
 
+  /**
+   * Creates a floating point formula representing the given string value with the specified type
+   * and rounding mode.
+   */
   FloatingPointFormula makeNumber(
       String n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode);
 
+  /**
+   * Creates a floating point formula representing the given Rational value with the specified type.
+   */
   FloatingPointFormula makeNumber(Rational n, FloatingPointType type);
 
+  /**
+   * Creates a floating point formula representing the given Rational value with the specified type
+   * and rounding mode.
+   */
   FloatingPointFormula makeNumber(
       Rational n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode);
 
+  /**
+   * Creates a floating point formula from the given exponent, mantissa, and sign bit with the
+   * specified type.
+   *
+   * @param exponent the exponent part of the floating point number
+   * @param mantissa the mantissa part of the floating point number
+   * @param signBit the sign bit of the floating point number, e.g., true for negative numbers
+   */
   FloatingPointFormula makeNumber(
       BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type);
 

src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java

@@ -55,6 +55,7 @@ public class FloatingPointFormulaManagerTest
   private FloatingPointFormula negInf;
   private FloatingPointFormula zero;
   private FloatingPointFormula one;
+  private FloatingPointFormula negZero;
 
   @Before
   public void init() {
@@ -66,6 +67,7 @@ public void init() {
     posInf = fpmgr.makePlusInfinity(singlePrecType);
     negInf = fpmgr.makeMinusInfinity(singlePrecType);
     zero = fpmgr.makeNumber(0.0, singlePrecType);
+    negZero = fpmgr.makeNumber(-0.0, singlePrecType);
     one = fpmgr.makeNumber(1.0, singlePrecType);
   }
 
@@ -131,8 +133,7 @@ public void parser() throws SolverException, InterruptedException {
   public void negativeZeroDivision() throws SolverException, InterruptedException {
     BooleanFormula formula =
         fpmgr.equalWithFPSemantics(
-            fpmgr.divide(
-                one, fpmgr.makeNumber(-0.0, singlePrecType), FloatingPointRoundingMode.TOWARD_ZERO),
+            fpmgr.divide(one, negZero, FloatingPointRoundingMode.TOWARD_ZERO),
             fpmgr.makeMinusInfinity(singlePrecType));
     assertThatFormula(formula).isSatisfiable();
     assertThatFormula(bmgr.not(formula)).isUnsatisfiable();
@@ -267,8 +268,8 @@ public void specialValueFunctions() throws SolverException, InterruptedException
     assertThatFormula(fpmgr.isSubnormal(zero)).isUnsatisfiable();
     assertThatFormula(fpmgr.isSubnormal(zero)).isUnsatisfiable();
 
-    FloatingPointFormula negZero = fpmgr.makeNumber(-0.0, singlePrecType);
     assertThatFormula(fpmgr.isZero(negZero)).isTautological();
+    assertThatFormula(fpmgr.equalWithFPSemantics(zero, negZero)).isTautological();
     assertThatFormula(fpmgr.isSubnormal(negZero)).isUnsatisfiable();
     assertThatFormula(fpmgr.isSubnormal(negZero)).isUnsatisfiable();
 
@@ -1056,4 +1057,27 @@ public void fpFrom64BitPattern() throws SolverException, InterruptedException {
       assertEqualsAsFormula(fpFromBv, fp);
     }
   }
+
+  @Test
+  public void fpFromNumberIntoTooNarrowType() throws SolverException, InterruptedException {
+    // near zero rounds to zero, if precision is too narrow
+    for (double nearZero : new double[] {Double.MIN_VALUE, Float.MIN_VALUE / 2d}) {
+      assertThatFormula(
+              fpmgr.equalWithFPSemantics(zero, fpmgr.makeNumber(nearZero, singlePrecType)))
+          .isTautological();
+      assertThatFormula(
+              fpmgr.equalWithFPSemantics(negZero, fpmgr.makeNumber(-nearZero, singlePrecType)))
+          .isTautological();
+    }
+
+    // near infinity rounds to infinity, if precision is too narrow
+    for (double nearInf : new double[] {Double.MAX_VALUE, Float.MAX_VALUE * 2d}) {
+      assertThatFormula(
+              fpmgr.equalWithFPSemantics(posInf, fpmgr.makeNumber(nearInf, singlePrecType)))
+          .isTautological();
+      assertThatFormula(
+              fpmgr.equalWithFPSemantics(negInf, fpmgr.makeNumber(-nearInf, singlePrecType)))
+          .isTautological();
+    }
+  }
 }