Fix Floating-Point Mantissa Not Including Sign Bit

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

@@ -23,6 +23,7 @@
 @AutoValue
 public abstract class FloatingPointNumber {
 
+  // Mantissas do not include the sign bit
   public static final int SINGLE_PRECISION_EXPONENT_SIZE = 8;
   public static final int SINGLE_PRECISION_MANTISSA_SIZE = 23;
   public static final int DOUBLE_PRECISION_EXPONENT_SIZE = 11;
@@ -80,8 +81,29 @@ public final boolean getSign() {
 
   public abstract int getExponentSize();
 
+  /**
+   * Returns the size of the mantissa (also called a coefficient or significant), excluding the sign
+   * bit.
+   */
+  // TODO: mark as soon to be deprecated
   public abstract int getMantissaSize();
 
+  /**
+   * Returns the size of the mantissa (also called a coefficient or significant), excluding the sign
+   * bit.
+   */
+  public int getMantissaSizeWithoutSignBit() {
+    return getMantissaSize();
+  }
+
+  /**
+   * Returns the size of the mantissa (also called a coefficient or significant), including the sign
+   * bit.
+   */
+  public int getMantissaSizeWithSignBit() {
+    return getMantissaSize() + 1;
+  }
+
   /**
    * Get a floating-point number with the given sign, exponent, and mantissa.
    *
@@ -92,7 +114,7 @@ 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 mantissaSize the (maximum) size of the mantissa in bits (excluding the sign bit)
    * @see #of(Sign, BigInteger, BigInteger, int, int)
    */
   @Deprecated(
@@ -119,7 +141,7 @@ 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 mantissaSize the (maximum) size of the mantissa in bits (excluding the sign bit)
    */
   public static FloatingPointNumber of(
       Sign sign, BigInteger exponent, BigInteger mantissa, int exponentSize, int mantissaSize) {
@@ -136,7 +158,7 @@ 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 mantissaSize the size of the mantissa in bits (excluding the sign bit)
    */
   public static FloatingPointNumber of(String bits, int exponentSize, int mantissaSize) {
     Preconditions.checkArgument(0 < exponentSize);
@@ -159,24 +181,26 @@ public static FloatingPointNumber of(String bits, int exponentSize, int mantissa
 
   /**
    * 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 sign bit).
    *
    * @return true for IEEE-754 single precision type, false otherwise.
    */
   public boolean isIEEE754SinglePrecision() {
+    // Mantissa does not include the sign bit
     return getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE
-        && getMantissaSize() == SINGLE_PRECISION_MANTISSA_SIZE;
+        && getMantissaSizeWithoutSignBit() == SINGLE_PRECISION_MANTISSA_SIZE;
   }
 
   /**
    * 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 sign bit).
    *
    * @return true for IEEE-754 double precision type, false otherwise.
    */
   public boolean isIEEE754DoublePrecision() {
+    // Mantissa does not include the sign bit
     return getExponentSize() == DOUBLE_PRECISION_EXPONENT_SIZE
-        && getMantissaSize() == DOUBLE_PRECISION_MANTISSA_SIZE;
+        && getMantissaSizeWithoutSignBit() == DOUBLE_PRECISION_MANTISSA_SIZE;
   }
 
   /** compute a representation as Java-based float value, if possible. */
@@ -204,18 +228,18 @@ public double doubleValue() {
   }
 
   private BitSet getBits() {
-    var mantissaSize = getMantissaSize();
+    var mantissaSizeWithoutSign = getMantissaSizeWithoutSignBit();
     var exponentSize = getExponentSize();
     var mantissa = getMantissa();
     var exponent = getExponent();
-    var bits = new BitSet(1 + exponentSize + mantissaSize);
+    var bits = new BitSet(exponentSize + mantissaSizeWithoutSign + 1);
     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 +251,7 @@ private BitSet getBits() {
    */
   @Override
   public final String toString() {
-    var length = 1 + getExponentSize() + getMantissaSize();
+    var length = getExponentSize() + getMantissaSizeWithSignBit();
     var str = new StringBuilder(length);
     var bits = getBits();
     for (int i = 0; i < length; i++) {

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

@@ -205,14 +205,61 @@ public String toSMTLIBString() {
     }
   }
 
-  public static FloatingPointType getFloatingPointType(int exponentSize, int mantissaSize) {
-    return new FloatingPointType(exponentSize, mantissaSize);
+  /**
+   * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes.
+   * The mantissa size is expected to not include the sign bit.
+   *
+   * @param exponentSize size of the exponent for the base of the floating-point
+   * @param mantissaSizeWithoutSignBit size of the mantissa (also called a coefficient or
+   *     significant), excluding the sign bit.
+   * @return the newly constructed {@link FloatingPointType}.
+   */
+  // TODO: mark as soon to be deprecated
+  public static FloatingPointType getFloatingPointType(
+      int exponentSize, int mantissaSizeWithoutSignBit) {
+    return new FloatingPointType(exponentSize, mantissaSizeWithoutSignBit);
+  }
+
+  /**
+   * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes.
+   * The mantissa size is expected to not include the sign bit.
+   *
+   * @param exponentSize size of the exponent for the base of the floating-point
+   * @param mantissaSizeWithoutSignBit size of the mantissa (also called a coefficient or
+   *     significant), excluding the sign bit.
+   * @return the newly constructed {@link FloatingPointType}.
+   */
+  public static FloatingPointType getFloatingPointTypeWithoutSignBit(
+      int exponentSize, int mantissaSizeWithoutSignBit) {
+    return new FloatingPointType(exponentSize, mantissaSizeWithoutSignBit);
+  }
+
+  /**
+   * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes.
+   * The mantissa size is expected to not include the sign bit.
+   *
+   * @param exponentSize size of the exponent for the base of the floating-point
+   * @param mantissaSizeWithSignBit size of the mantissa (also called a coefficient or significant),
+   *     including the sign bit.
+   * @return the newly constructed {@link FloatingPointType}.
+   */
+  public static FloatingPointType getFloatingPointTypeWithSignBit(
+      int exponentSize, int mantissaSizeWithSignBit) {
+    return new FloatingPointType(exponentSize, mantissaSizeWithSignBit);
   }
 
+  /**
+   * @return single precision {@link FloatingPointType} with exponent sized 8, and mantissa sized 24
+   *     (including the sign bit).
+   */
   public static FloatingPointType getSinglePrecisionFloatingPointType() {
     return FloatingPointType.SINGLE_PRECISION_FP_TYPE;
   }
 
+  /**
+   * @return double precision {@link FloatingPointType} with exponent sized 11, and mantissa sized
+   *     53 (including the sign bit).
+   */
   public static FloatingPointType getDoublePrecisionFloatingPointType() {
     return FloatingPointType.DOUBLE_PRECISION_FP_TYPE;
   }
@@ -226,6 +273,8 @@ public static final class FloatingPointType extends FormulaType<FloatingPointFor
         new FloatingPointType(DOUBLE_PRECISION_EXPONENT_SIZE, DOUBLE_PRECISION_MANTISSA_SIZE);
 
     private final int exponentSize;
+    // The SMTLib2 standard defines the mantissa size as including the sign bit. We do not include
+    // it here though.
     private final int mantissaSize;
 
     private FloatingPointType(int pExponentSize, int pMantissaSize) {
@@ -238,15 +287,40 @@ public boolean isFloatingPointType() {
       return true;
     }
 
+    /** Returns the size of the exponent */
     public int getExponentSize() {
       return exponentSize;
     }
 
+    /**
+     * Returns the size of the mantissa (also called a coefficient or significant), excluding the
+     * sign bit.
+     */
+    // TODO: mark as soon to be deprecated
     public int getMantissaSize() {
       return mantissaSize;
     }
 
-    /** Return the total size of a value of this type in bits. */
+    /**
+     * Returns the size of the mantissa (also called a coefficient or significant), excluding the
+     * sign bit.
+     */
+    public int getMantissaSizeWithoutSignBit() {
+      return mantissaSize;
+    }
+
+    /**
+     * Returns the size of the mantissa (also called a coefficient or significant), including the
+     * sign bit.
+     */
+    public int getMantissaSizeWithSignBit() {
+      return mantissaSize + 1;
+    }
+
+    /**
+     * Return the total size of a value of this type in bits. Equal to exponent + mantissa
+     * (including the sign bit).
+     */
     public int getTotalSize() {
       return exponentSize + mantissaSize + 1;
     }
@@ -270,12 +344,12 @@ public boolean equals(Object obj) {
 
     @Override
     public String toString() {
-      return "FloatingPoint<exp=" + exponentSize + ",mant=" + mantissaSize + ">";
+      return "FloatingPoint<exp=" + exponentSize + ",mant=" + getMantissaSizeWithSignBit() + ">";
     }
 
     @Override
     public String toSMTLIBString() {
-      return "(_ FloatingPoint " + exponentSize + " " + mantissaSize + ")";
+      return "(_ FloatingPoint " + exponentSize + " " + getMantissaSizeWithSignBit() + ")";
     }
   }
 
@@ -478,7 +552,7 @@ public static FormulaType<?> fromString(String t) {
     } else if (t.startsWith("FloatingPoint<")) {
       // FloatingPoint<exp=11,mant=52>
       List<String> exman = Splitter.on(',').limit(2).splitToList(t.substring(14, t.length() - 1));
-      return FormulaType.getFloatingPointType(
+      return FormulaType.getFloatingPointTypeWithoutSignBit(
           Integer.parseInt(exman.get(0).substring(4)), Integer.parseInt(exman.get(1).substring(5)));
     } else if (t.startsWith("Bitvector<")) {
       // Bitvector<32>

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

@@ -256,7 +256,12 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula pNumber) {
     return getFormulaCreator().encapsulateBitvector(toIeeeBitvectorImpl(extractInfo(pNumber)));
   }
 
-  protected abstract TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber);
+  @SuppressWarnings("unused")
+  protected TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber) {
+    throw new UnsupportedOperationException(
+        "Solver does not support transformation from "
+            + "floating-point numbers to IEEE bitvector");
+  }
 
   @Override
   public FloatingPointFormula negate(FloatingPointFormula pNumber) {

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

@@ -94,7 +94,7 @@ protected Term makeNumberImpl(
     Sort expSort = termManager.mk_bv_sort(type.getExponentSize());
     Term expTerm = termManager.mk_bv_value(expSort, exponent.toString(2));
 
-    Sort mantissaSort = termManager.mk_bv_sort(type.getMantissaSize());
+    Sort mantissaSort = termManager.mk_bv_sort(type.getMantissaSizeWithoutSignBit());
     Term mantissaTerm = termManager.mk_bv_value(mantissaSort, mantissa.toString(2));
 
     return termManager.mk_fp_value(signTerm, expTerm, mantissaTerm);
@@ -144,7 +144,7 @@ protected Term castToImpl(
           pRoundingMode,
           pNumber,
           targetType.getExponentSize(),
-          targetType.getMantissaSize() + 1);
+          targetType.getMantissaSizeWithSignBit());
     } else if (pTargetType.isBitvectorType()) {
       FormulaType.BitvectorType targetType = (FormulaType.BitvectorType) pTargetType;
       if (pSigned) {
@@ -171,14 +171,14 @@ protected Term castFromImpl(
             roundingMode,
             pNumber,
             pTargetType.getExponentSize(),
-            pTargetType.getMantissaSize() + 1);
+            pTargetType.getMantissaSizeWithSignBit());
       } else {
         return termManager.mk_term(
             Kind.FP_TO_FP_FROM_UBV,
             roundingMode,
             pNumber,
             pTargetType.getExponentSize(),
-            pTargetType.getMantissaSize() + 1);
+            pTargetType.getMantissaSizeWithSignBit());
       }
 
     } else {
@@ -193,7 +193,7 @@ protected Term fromIeeeBitvectorImpl(Term pNumber, FloatingPointType pTargetType
         Kind.FP_TO_FP_FROM_BV,
         pNumber,
         pTargetType.getExponentSize(),
-        pTargetType.getMantissaSize() + 1);
+        pTargetType.getMantissaSizeWithSignBit());
   }
 
   @Override

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

@@ -102,7 +102,7 @@ assert getFormulaType(pTerm).isBitvectorType()
   // system instead use bitwuzla_mk_fp_value_from_real somehow or convert myself
   @Override
   public Sort getFloatingPointType(FloatingPointType type) {
-    return termManager.mk_fp_sort(type.getExponentSize(), type.getMantissaSize() + 1);
+    return termManager.mk_fp_sort(type.getExponentSize(), type.getMantissaSizeWithSignBit());
   }
 
   @Override
@@ -171,7 +171,7 @@ public FormulaType<?> bitwuzlaSortToType(Sort pSort) {
     if (pSort.is_fp()) {
       int exponent = pSort.fp_exp_size();
       int mantissa = pSort.fp_sig_size() - 1;
-      return FormulaType.getFloatingPointType(exponent, mantissa);
+      return FormulaType.getFloatingPointTypeWithoutSignBit(exponent, mantissa);
     } else if (pSort.is_bv()) {
       return FormulaType.getBitvectorTypeWithSize(pSort.bv_size());
     } else if (pSort.is_array()) {
@@ -380,7 +380,7 @@ public <T extends Formula> FormulaType<T> getFormulaType(T pFormula) {
       }
       int exp = sort.fp_exp_size();
       int man = sort.fp_sig_size() - 1;
-      return (FormulaType<T>) FormulaType.getFloatingPointType(exp, man);
+      return (FormulaType<T>) FormulaType.getFloatingPointTypeWithoutSignBit(exp, man);
     } else if (sort.is_rm()) {
       return (FormulaType<T>) FormulaType.FloatingPointRoundingModeType;
     }