#433: add more documentation and tests for FP numbers.

Author: kfriedberger

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

@@ -8,6 +8,8 @@
 
 package org.sosy_lab.java_smt.api;
 
+import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointType;
+
 import java.math.BigDecimal;
 import java.math.BigInteger;
 import org.sosy_lab.common.rationals.Rational;
@@ -59,12 +61,18 @@ FloatingPointFormula makeNumber(
 
   /**
    * Creates a floating point formula representing the given string value with the specified type.
+   *
+   * <p>The string can be any valid floating-point number, e.g., "1.0", "1.0e-3", but also special
+   * values like "NaN", "Infinity", or "-0.0", etc. A leading "+" sign or "-" sign is allowed.
    */
   FloatingPointFormula makeNumber(String n, FloatingPointType type);
 
   /**
    * Creates a floating point formula representing the given string value with the specified type
    * and rounding mode.
+   *
+   * <p>The string can be any valid floating-point number, e.g., "1.0", "1.0e-3", but also special
+   * values like "NaN", "Infinity", or "-0.0", etc. A leading "+" sign or "-" sign is allowed.
    */
   FloatingPointFormula makeNumber(
       String n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode);
@@ -91,7 +99,7 @@ default FloatingPointFormula makeNumber(FloatingPointNumber number) {
         number.getExponent(),
         number.getMantissa(),
         number.getSign(),
-        FloatingPointType.getFloatingPointType(number.getExponentSize(), number.getMantissaSize()));
+        getFloatingPointType(number.getExponentSize(), number.getMantissaSize()));
   }
 
   /**

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

@@ -149,6 +149,12 @@ protected static boolean isNegativeZero(Double pN) {
     return Double.valueOf("-0.0").equals(pN);
   }
 
+  /**
+   * Parses the provided string and converts it into a floating-point formula.
+   *
+   * <p>The input string must represent a valid finite floating-point number. Values such as NaN,
+   * Infinity, or -Infinity are not allowed and should be handled before calling this method.
+   */
   protected abstract TFormulaInfo makeNumberAndRound(
       String pN, FloatingPointType pType, TFormulaInfo pFloatingPointRoundingMode);
 

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

@@ -105,19 +105,58 @@ public void negative() throws SolverException, InterruptedException {
 
   @Test
   public void parser() throws SolverException, InterruptedException {
-    for (String s : new String[] {"-1", "-Infinity", "-0", "-0.0", "-0.000"}) {
+    for (String s :
+        new String[] {
+          "-1",
+          "-Infinity",
+          "-0",
+          "-0.0",
+          "-0.000",
+          "-0e5",
+          "-0.00e-5",
+          "-12e34",
+          "-12e-34",
+          "-12.34E56",
+          "-12.34e-56"
+        }) {
       FloatingPointFormula formula = fpmgr.makeNumber(s, singlePrecType);
       assertThatFormula(fpmgr.isNegative(formula)).isTautological();
       assertThatFormula(fpmgr.isNegative(fpmgr.negate(formula))).isUnsatisfiable();
       assertEqualsAsFp(fpmgr.negate(formula), fpmgr.abs(formula));
     }
-    for (String s : new String[] {"1", "Infinity", "0", "0.0", "0.000"}) {
+    for (String s :
+        new String[] {
+          "1",
+          "Infinity",
+          "0",
+          "0.0",
+          "0.000",
+          "0e5",
+          "0.00e-5",
+          "12e34",
+          "12e-34",
+          "12.34E56",
+          "12.34e-56"
+        }) {
       FloatingPointFormula formula = fpmgr.makeNumber(s, singlePrecType);
       assertThatFormula(fpmgr.isNegative(formula)).isUnsatisfiable();
       assertThatFormula(fpmgr.isNegative(fpmgr.negate(formula))).isTautological();
       assertEqualsAsFp(formula, fpmgr.abs(formula));
     }
-    for (String s : new String[] {"+1", "+Infinity", "+0", "+0.0", "+0.000"}) {
+    for (String s :
+        new String[] {
+          "+1",
+          "+Infinity",
+          "+0",
+          "+0.0",
+          "+0.000",
+          "+0e5",
+          "+0.00e-5",
+          "+12e34",
+          "+12e-34",
+          "+12.34E56",
+          "+12.34e-56"
+        }) {
       FloatingPointFormula formula = fpmgr.makeNumber(s, singlePrecType);
       assertThatFormula(fpmgr.isNegative(formula)).isUnsatisfiable();
       assertThatFormula(fpmgr.isNegative(fpmgr.negate(formula))).isTautological();
@@ -791,6 +830,26 @@ private <T> void proveForAll(List<T> args, Function<T, BooleanFormula> f)
     }
   }
 
+  @Test
+  public void checkString2FpConversion32() throws SolverException, InterruptedException {
+    proveForAll(
+        getListOfFloats(),
+        pFloat ->
+            fpmgr.equalWithFPSemantics(
+                fpmgr.makeNumber(pFloat, singlePrecType),
+                fpmgr.makeNumber(Float.toString(pFloat), singlePrecType)));
+  }
+
+  @Test
+  public void checkString2FpConversion64() throws SolverException, InterruptedException {
+    proveForAll(
+        getListOfDoubles(),
+        pDouble ->
+            fpmgr.equalWithFPSemantics(
+                fpmgr.makeNumber(pDouble, doublePrecType),
+                fpmgr.makeNumber(Double.toString(pDouble), doublePrecType)));
+  }
+
   @Test
   public void checkIeeeBv2FpConversion32() throws SolverException, InterruptedException {
     proveForAll(