Add IEEE-754 Floating Point to Bitvector Conversion Fallback

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

@@ -8,13 +8,15 @@
 
 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.getFloatingPointTypeWithoutSignBit;
 
 import java.math.BigDecimal;
 import java.math.BigInteger;
+import java.util.Map;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
+import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula;
 
 /**
  * Floating point operations.
@@ -99,7 +101,8 @@ default FloatingPointFormula makeNumber(FloatingPointNumber number) {
         number.getExponent(),
         number.getMantissa(),
         number.getMathSign(),
-        getFloatingPointType(number.getExponentSize(), number.getMantissaSize()));
+        getFloatingPointTypeWithoutSignBit(
+            number.getExponentSize(), number.getMantissaSizeWithoutSignBit()));
   }
 
   /**
@@ -285,11 +288,70 @@ 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).
+   * bitvector conforming to the IEEE 754-2008 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).
    */
   BitvectorFormula toIeeeBitvector(FloatingPointFormula number);
 
+  /**
+   * Create a formula that produces a representation of the given floating-point value as a
+   * bitvector conforming to the IEEE 754-2008 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).
+   * This implementation can be used independently of {@link
+   * #toIeeeBitvector(FloatingPointFormula)}, as it does not rely on an SMT solvers support for
+   * {@link #toIeeeBitvector(FloatingPointFormula)}. Behavior for special FP values (NaN, Inf, etc.)
+   * is not defined, and returned values are solver dependent. In case you want to define how to
+   * handle those values, please use {@link #toIeeeBitvector(FloatingPointFormula, String, Map)}.
+   * This method is based on a suggestion in the SMTLib2 standard ( <a
+   * href="https://smt-lib.org/theories-FloatingPoint.shtml">source</a>) implementation:
+   *
+   * <p>(declare-fun b () (_ BitVec m))
+   *
+   * <p>(assert (= ((_ to_fp eb sb) b) f))
+   *
+   * @param number the {@link FloatingPointFormula} to be converted into an IEEE bitvector.
+   * @param bitvectorConstantName the name of the returned {@link BitvectorFormula}.
+   * @return {@link BitvectorFormulaAndBooleanFormula} consisting of the transformed input
+   *     floating-point as a {@link BitvectorFormula} and the additional constraint as {@link
+   *     BooleanFormula}.
+   */
+  BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+      FloatingPointFormula number, String bitvectorConstantName);
+
+  /**
+   * Create a formula that produces a representation of the given floating-point value as a
+   * bitvector conforming to the IEEE 754-2008 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).
+   * This implementation can be used independently of {@link
+   * #toIeeeBitvector(FloatingPointFormula)}, as it does not rely on an SMT solvers support for
+   * {@link #toIeeeBitvector(FloatingPointFormula)}. Behavior for special FP values (NaN, Inf, etc.)
+   * can be defined using the specialFPConstantHandling parameter. This method is based on a
+   * suggestion in the SMTLib2 standard ( <a
+   * href="https://smt-lib.org/theories-FloatingPoint.shtml">source</a>) implementation:
+   *
+   * <p>(declare-fun b () (_ BitVec m))
+   *
+   * <p>(assert (= ((_ to_fp eb sb) b) f))
+   *
+   * @param number the {@link FloatingPointFormula} to be converted into an IEEE bitvector.
+   * @param bitvectorConstantName the name of the returned {@link BitvectorFormula}.
+   * @param specialFPConstantHandling a {@link Map} defining the returned {@link BitvectorFormula}
+   *     for special {@link FloatingPointFormula} constant numbers. You are only allowed to specify
+   *     a mapping for special FP numbers with more than one well-defined bitvector representation,
+   *     i.e. NaN and +/- Infinity. The width of the mapped bitvector values has to match the
+   *     expected width of the bitvector return value. The {@link FloatingPointType}, i.e.
+   *     precision, of the key FP numbers has to match the {@link FloatingPointType} of the
+   *     parameter {@code number}. For an empty {@link Map}, or missing mappings, this method
+   *     behaves like {@link #toIeeeBitvector(FloatingPointFormula, String)}.
+   * @return {@link BitvectorFormulaAndBooleanFormula} consisting of the transformed input
+   *     floating-point as a {@link BitvectorFormula} and the additional constraint as {@link
+   *     BooleanFormula}.
+   */
+  BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+      FloatingPointFormula number,
+      String bitvectorConstantName,
+      Map<FloatingPointFormula, BitvectorFormula> specialFPConstantHandling);
+
   FloatingPointFormula round(FloatingPointFormula formula, FloatingPointRoundingMode roundingMode);
 
   // ----------------- Arithmetic relations, return type NumeralFormula -----------------
@@ -467,4 +529,13 @@ FloatingPointFormula multiply(
    * </ul>
    */
   BooleanFormula isNegative(FloatingPointFormula number);
+
+  /**
+   * Returns the size of the mantissa (also called a coefficient or significant), including the sign
+   * bit, for the given {@link FloatingPointFormula}.
+   */
+  int getMantissaSizeWithSignBit(FloatingPointFormula number);
+
+  /** Returns the size of the exponent for the given {@link FloatingPointFormula}. */
+  int getExponentSize(FloatingPointFormula number);
 }

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>