Fix Floating-Point Mantissa Not Including Sign Bit

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

@@ -8,7 +8,7 @@
 
 package org.sosy_lab.java_smt.api;
 
-import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointType;
+import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointTypeFromSizesWithoutHiddenBit;
 
 import java.math.BigDecimal;
 import java.math.BigInteger;
@@ -99,7 +99,8 @@ default FloatingPointFormula makeNumber(FloatingPointNumber number) {
         number.getExponent(),
         number.getMantissa(),
         number.getMathSign(),
-        getFloatingPointType(number.getExponentSize(), number.getMantissaSize()));
+        getFloatingPointTypeFromSizesWithoutHiddenBit(
+            number.getExponentSize(), number.getMantissaSizeWithoutHiddenBit()));
   }
 
   /**
@@ -274,8 +275,8 @@ FloatingPointFormula castFrom(
 
   /**
    * Create a formula that interprets the given bitvector as a floating-point value in the IEEE
-   * format, according to the given type. The sum of the sizes of exponent and mantissa of the
-   * target type plus 1 (for the sign bit) needs to be equal to the size of the bitvector.
+   * format, according to the given type. The sum of the sizes of exponent and mantissa (including
+   * the hidden bit) of the target type needs to be equal to the size of the bitvector.
    *
    * <p>Note: This method will return a value that is (numerically) far away from the original
    * value. This method is completely different from {@link #castFrom}, which will produce a
@@ -286,7 +287,7 @@ FloatingPointFormula castFrom(
   /**
    * Create a formula that produces a representation of the given floating-point value as a
    * bitvector conforming to the IEEE format. The size of the resulting bitvector is the sum of the
-   * sizes of the exponent and mantissa of the input formula plus 1 (for the sign bit).
+   * sizes of the exponent and mantissa (including the hidden bit) of the input formula.
    */
   BitvectorFormula toIeeeBitvector(FloatingPointFormula number);
 

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

@@ -23,11 +23,31 @@
 @AutoValue
 public abstract class FloatingPointNumber {
 
+  // TODO: remove deprecated constants from public API after 6.0 release (and delete the unused).
+  @Deprecated(since = "6.0", forRemoval = true)
   public static final int SINGLE_PRECISION_EXPONENT_SIZE = 8;
+
+  /**
+   * @deprecated this constant can be confusing, as the SMTLIB2 standard expects the mantissa to
+   *     include the hidden bit, but this constant does not.
+   */
+  @Deprecated(since = "6.0", forRemoval = true)
   public static final int SINGLE_PRECISION_MANTISSA_SIZE = 23;
+
+  protected static final int SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT = 23;
+
+  @Deprecated(since = "6.0", forRemoval = true)
   public static final int DOUBLE_PRECISION_EXPONENT_SIZE = 11;
+
+  /**
+   * @deprecated this constant can be confusing, as the SMTLIB2 standard expects the mantissa to
+   *     include the hidden bit, but this constant does not.
+   */
+  @Deprecated(since = "6.0", forRemoval = true)
   public static final int DOUBLE_PRECISION_MANTISSA_SIZE = 52;
 
+  protected static final int DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT = 52;
+
   public enum Sign {
     POSITIVE,
     NEGATIVE;
@@ -80,7 +100,42 @@ public final boolean getSign() {
 
   public abstract int getExponentSize();
 
-  public abstract int getMantissaSize();
+  /**
+   * Returns the size of the mantissa (also called a coefficient or significant), excluding the sign
+   * bit.
+   *
+   * @deprecated this method can be confusing, as the SMTLIB2 standard expects the mantissa to
+   *     include the hidden bit, but this does not. Use {@link #getMantissaSizeWithoutHiddenBit()}
+   *     instead if you want the mantissa without the hidden bit, and {@link
+   *     #getMantissaSizeWithHiddenBit()} if you want it to include the hidden bit.
+   */
+  @Deprecated(since = "6.0", forRemoval = true)
+  @SuppressWarnings("InlineMeSuggester")
+  public final int getMantissaSize() {
+    return getMantissaSizeWithoutHiddenBit();
+  }
+
+  /**
+   * Returns the size of the mantissa (also called a coefficient or significant), excluding the
+   * hidden bit.
+   */
+  public abstract int getMantissaSizeWithoutHiddenBit();
+
+  /**
+   * Returns the size of the mantissa (also called a coefficient or significant), including the
+   * hidden bit.
+   */
+  public int getMantissaSizeWithHiddenBit() {
+    return getMantissaSizeWithoutHiddenBit() + 1;
+  }
+
+  /**
+   * Returns the size of the precision, i.e. the single sign bit + the size of the exponent + the
+   * size of the mantissa (excluding the hidden bit).
+   */
+  public int getTotalSize() {
+    return getMantissaSizeWithoutHiddenBit() + getExponentSize() + 1;
+  }
 
   /**
    * Get a floating-point number with the given sign, exponent, and mantissa.
@@ -92,22 +147,28 @@ public final boolean getSign() {
    * @param mantissa the mantissa of the floating-point number, given as unsigned (not negative)
    *     number without hidden bit
    * @param exponentSize the (maximum) size of the exponent in bits
-   * @param mantissaSize the (maximum) size of the mantissa in bits
+   * @param mantissaSizeWithoutHiddenBit the (maximum) size of the mantissa in bits (excluding the
+   *     hidden bit)
    * @see #of(Sign, BigInteger, BigInteger, int, int)
    */
   @Deprecated(
       since = "2025.01, because using a boolean flag as signBit is misleading",
       forRemoval = true)
   @InlineMe(
       replacement =
-          "FloatingPointNumber.of(Sign.of(sign), exponent, mantissa, exponentSize, mantissaSize)",
+          "FloatingPointNumber.of(Sign.of(sign), exponent, mantissa, exponentSize,"
+              + " mantissaSizeWithoutHiddenBit)",
       imports = {
         "org.sosy_lab.java_smt.api.FloatingPointNumber",
         "org.sosy_lab.java_smt.api.FloatingPointNumber.Sign"
       })
   public static FloatingPointNumber of(
-      boolean sign, BigInteger exponent, BigInteger mantissa, int exponentSize, int mantissaSize) {
-    return of(Sign.of(sign), exponent, mantissa, exponentSize, mantissaSize);
+      boolean sign,
+      BigInteger exponent,
+      BigInteger mantissa,
+      int exponentSize,
+      int mantissaSizeWithoutHiddenBit) {
+    return of(Sign.of(sign), exponent, mantissa, exponentSize, mantissaSizeWithoutHiddenBit);
   }
 
   /**
@@ -119,15 +180,21 @@ public static FloatingPointNumber of(
    * @param mantissa the mantissa of the floating-point number, given as unsigned (not negative)
    *     number without hidden bit
    * @param exponentSize the (maximum) size of the exponent in bits
-   * @param mantissaSize the (maximum) size of the mantissa in bits
+   * @param mantissaSizeWithoutHiddenBit the (maximum) size of the mantissa in bits (excluding the
+   *     hidden bit)
    */
   public static FloatingPointNumber of(
-      Sign sign, BigInteger exponent, BigInteger mantissa, int exponentSize, int mantissaSize) {
+      Sign sign,
+      BigInteger exponent,
+      BigInteger mantissa,
+      int exponentSize,
+      int mantissaSizeWithoutHiddenBit) {
     Preconditions.checkArgument(exponent.bitLength() <= exponentSize);
-    Preconditions.checkArgument(mantissa.bitLength() <= mantissaSize);
+    Preconditions.checkArgument(mantissa.bitLength() <= mantissaSizeWithoutHiddenBit);
     Preconditions.checkArgument(exponent.compareTo(BigInteger.ZERO) >= 0);
     Preconditions.checkArgument(mantissa.compareTo(BigInteger.ZERO) >= 0);
-    return new AutoValue_FloatingPointNumber(sign, exponent, mantissa, exponentSize, mantissaSize);
+    return new AutoValue_FloatingPointNumber(
+        sign, exponent, mantissa, exponentSize, mantissaSizeWithoutHiddenBit);
   }
 
   /**
@@ -136,47 +203,59 @@ public static FloatingPointNumber of(
    * @param bits the bit-representation of the floating-point number, consisting of sign bit,
    *     exponent (without bias) and mantissa (without hidden bit) in this exact ordering
    * @param exponentSize the size of the exponent in bits
-   * @param mantissaSize the size of the mantissa in bits
+   * @param mantissaSizeWithoutHiddenBit the size of the mantissa in bits (excluding the hidden bit)
    */
-  public static FloatingPointNumber of(String bits, int exponentSize, int mantissaSize) {
+  public static FloatingPointNumber of(
+      String bits, int exponentSize, int mantissaSizeWithoutHiddenBit) {
     Preconditions.checkArgument(0 < exponentSize);
-    Preconditions.checkArgument(0 < mantissaSize);
+    Preconditions.checkArgument(0 < mantissaSizeWithoutHiddenBit);
     Preconditions.checkArgument(
-        bits.length() == 1 + exponentSize + mantissaSize,
+        bits.length() == 1 + exponentSize + mantissaSizeWithoutHiddenBit,
         "Bitsize (%s) of floating point numeral does not match the size of sign, exponent and "
             + "mantissa (%s + %s + %s).",
         bits.length(),
         1,
         exponentSize,
-        mantissaSize);
+        mantissaSizeWithoutHiddenBit);
     Preconditions.checkArgument(bits.chars().allMatch(c -> c == '0' || c == '1'));
     Sign sign = Sign.of(bits.charAt(0) == '1');
     BigInteger exponent = new BigInteger(bits.substring(1, 1 + exponentSize), 2);
     BigInteger mantissa =
-        new BigInteger(bits.substring(1 + exponentSize, 1 + exponentSize + mantissaSize), 2);
-    return of(sign, exponent, mantissa, exponentSize, mantissaSize);
+        new BigInteger(
+            bits.substring(1 + exponentSize, 1 + exponentSize + mantissaSizeWithoutHiddenBit), 2);
+    return of(sign, exponent, mantissa, exponentSize, mantissaSizeWithoutHiddenBit);
   }
 
   /**
    * Returns true if this floating-point number is an IEEE-754-2008 single precision type with 32
-   * bits length consisting of an 8 bit exponent, a 23 bit mantissa and a single sign bit.
+   * bits length consisting of an 8 bit exponent, a 24 bit mantissa (including the hidden bit).
    *
    * @return true for IEEE-754 single precision type, false otherwise.
    */
   public boolean isIEEE754SinglePrecision() {
-    return getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE
-        && getMantissaSize() == SINGLE_PRECISION_MANTISSA_SIZE;
+    // Mantissa does not include the hidden bit internally
+    return getTotalSize()
+            == SINGLE_PRECISION_EXPONENT_SIZE
+                + SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT
+                + 1
+        && getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE
+        && getMantissaSizeWithoutHiddenBit() == SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT;
   }
 
   /**
    * Returns true if this floating-point number is an IEEE-754-2008 double precision type with 64
-   * bits length consisting of an 11 bit exponent, a 52 bit mantissa and a single sign bit.
+   * bits length consisting of an 11 bit exponent, a 53 bit mantissa (including the hidden bit).
    *
    * @return true for IEEE-754 double precision type, false otherwise.
    */
   public boolean isIEEE754DoublePrecision() {
-    return getExponentSize() == DOUBLE_PRECISION_EXPONENT_SIZE
-        && getMantissaSize() == DOUBLE_PRECISION_MANTISSA_SIZE;
+    // Mantissa does not include the hidden bit internally
+    return getTotalSize()
+            == DOUBLE_PRECISION_EXPONENT_SIZE
+                + DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT
+                + 1
+        && getExponentSize() == DOUBLE_PRECISION_EXPONENT_SIZE
+        && getMantissaSizeWithoutHiddenBit() == DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT;
   }
 
   /** compute a representation as Java-based float value, if possible. */
@@ -204,18 +283,18 @@ public double doubleValue() {
   }
 
   private BitSet getBits() {
-    var mantissaSize = getMantissaSize();
+    var mantissaSizeWithoutSign = getMantissaSizeWithoutHiddenBit();
     var exponentSize = getExponentSize();
     var mantissa = getMantissa();
     var exponent = getExponent();
-    var bits = new BitSet(1 + exponentSize + mantissaSize);
+    var bits = new BitSet(getTotalSize());
     if (getMathSign().isNegative()) {
-      bits.set(exponentSize + mantissaSize); // if negative, set first bit to 1
+      bits.set(exponentSize + mantissaSizeWithoutSign); // if negative, set first bit to 1
     }
     for (int i = 0; i < exponentSize; i++) {
-      bits.set(mantissaSize + i, exponent.testBit(i));
+      bits.set(mantissaSizeWithoutSign + i, exponent.testBit(i));
     }
-    for (int i = 0; i < mantissaSize; i++) {
+    for (int i = 0; i < mantissaSizeWithoutSign; i++) {
       bits.set(i, mantissa.testBit(i));
     }
     return bits;
@@ -227,7 +306,7 @@ private BitSet getBits() {
    */
   @Override
   public final String toString() {
-    var length = 1 + getExponentSize() + getMantissaSize();
+    var length = getTotalSize();
     var str = new StringBuilder(length);
     var bits = getBits();
     for (int i = 0; i < length; i++) {