Add IEEE-754 Floating Point to Bitvector Conversion Fallback

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

@@ -13,9 +13,11 @@
 
 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.
@@ -305,6 +307,71 @@ FloatingPointFormula castFrom(
    */
   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))
+   *
+   * <p>Note: SMTLIB2 output of this method uses the SMTLIB2 keyword 'to_fp' as described above and
+   * no keyword variation for floating-point to bitvector conversion like 'fp.as_ieee_bv'.
+   *
+   * @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))
+   *
+   * <p>Note: SMTLIB2 output of this method uses the SMTLIB2 keyword 'to_fp' as described above and
+   * no keyword variation for floating-point to bitvector conversion like 'fp.as_ieee_bv'.
+   *
+   * @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 -----------------
@@ -482,4 +549,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/FormulaType.java

@@ -320,7 +320,6 @@ public boolean isFloatingPointType() {
       return true;
     }
 
-    /** Returns the size of the exponent. */
     public int getExponentSize() {
       return exponentSize;
     }

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

@@ -8,13 +8,19 @@
 
 package org.sosy_lab.java_smt.basicimpl;
 
+import static com.google.common.base.Preconditions.checkArgument;
+import static com.google.common.base.Preconditions.checkNotNull;
+import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointTypeFromSizesWithoutHiddenBit;
 import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName;
 
-import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableMap;
+import com.google.common.collect.ImmutableSet;
 import java.math.BigDecimal;
 import java.math.BigInteger;
 import java.util.HashMap;
 import java.util.Map;
+import java.util.Map.Entry;
+import java.util.Set;
 import org.sosy_lab.common.MoreStrings;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.BitvectorFormula;
@@ -48,10 +54,18 @@ public abstract class AbstractFloatingPointFormulaManager<TFormulaInfo, TType, T
 
   private final Map<FloatingPointRoundingMode, TFormulaInfo> roundingModes;
 
+  private final AbstractBitvectorFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> bvMgr;
+
+  private final AbstractBooleanFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> bMgr;
+
   protected AbstractFloatingPointFormulaManager(
-      FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl> pCreator) {
+      FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl> pCreator,
+      AbstractBitvectorFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> pBvMgr,
+      AbstractBooleanFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> pBMgr) {
     super(pCreator);
     roundingModes = new HashMap<>();
+    bvMgr = pBvMgr;
+    bMgr = pBMgr;
   }
 
   protected abstract TFormulaInfo getDefaultRoundingMode();
@@ -160,7 +174,7 @@ protected abstract TFormulaInfo makeNumberImpl(
       BigInteger exponent, BigInteger mantissa, Sign sign, FloatingPointType type);
 
   protected static boolean isNegativeZero(Double pN) {
-    Preconditions.checkNotNull(pN);
+    checkNotNull(pN);
     return Double.valueOf("-0.0").equals(pN);
   }
 
@@ -261,7 +275,7 @@ protected abstract TFormulaInfo castFromImpl(
   public FloatingPointFormula fromIeeeBitvector(
       BitvectorFormula pNumber, FloatingPointType pTargetType) {
     BitvectorType bvType = (BitvectorType) formulaCreator.getFormulaType(pNumber);
-    Preconditions.checkArgument(
+    checkArgument(
         bvType.getSize() == pTargetType.getTotalSize(),
         MoreStrings.lazyString(
             () ->
@@ -279,7 +293,99 @@ 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(
+        "The chosen solver does not support transforming "
+            + "FloatingPointFormula to IEEE bitvectors. Try using the fallback "
+            + "methods toIeeeBitvector"
+            + "(FloatingPointFormula, String) and/or "
+            + "toIeeeBitvector(FloatingPointFormula, String, Map)");
+  }
+
+  @Override
+  public BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+      FloatingPointFormula f, String bitvectorConstantName) {
+    return toIeeeBitvector(f, bitvectorConstantName, ImmutableMap.of());
+  }
+
+  @Override
+  public BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+      FloatingPointFormula f,
+      String bitvectorConstantName,
+      Map<FloatingPointFormula, BitvectorFormula> specialFPConstantHandling) {
+
+    FormulaType.FloatingPointType fpType =
+        (FloatingPointType) getFormulaCreator().getFormulaType(f);
+    // The BV is sign bit + exponent + mantissa without hidden bit
+    int mantissaSizeWithoutHiddenBit = fpType.getMantissaSizeWithoutHiddenBit();
+    int exponentSize = fpType.getExponentSize();
+    BitvectorFormula bvFormula =
+        bvMgr.makeVariable(1 + exponentSize + mantissaSizeWithoutHiddenBit, bitvectorConstantName);
+
+    // When building new Fp types, we don't include the sign bit
+    FloatingPointFormula fromIeeeBitvector =
+        fromIeeeBitvector(
+            bvFormula,
+            getFloatingPointTypeFromSizesWithoutHiddenBit(
+                exponentSize, mantissaSizeWithoutHiddenBit));
+
+    // assignment() allows a value to be NaN etc.
+    // Note: All fp.to_* functions are unspecified for NaN and infinity input values in the
+    // standard, what solvers return might be distinct.
+    BooleanFormula additionalConstraint = assignment(fromIeeeBitvector, f);
+
+    // Build special numbers so that we can compare them in the map
+    FloatingPointType precision =
+        getFloatingPointTypeFromSizesWithoutHiddenBit(exponentSize, mantissaSizeWithoutHiddenBit);
+    Set<FloatingPointFormula> specialNumbers =
+        ImmutableSet.of(
+            makeNaN(precision), makePlusInfinity(precision), makeMinusInfinity(precision));
+
+    BitvectorFormula toIeeeBv = bvFormula;
+    for (Entry<FloatingPointFormula, BitvectorFormula> entry :
+        specialFPConstantHandling.entrySet()) {
+      FloatingPointFormula fpConst = entry.getKey();
+
+      // We check that FP const special numbers are used (info from SMTLib2-standard)
+      // NaN has multiple possible definitions.
+      // +/- Infinity each has 2; e.g., +infinity for sort (_ FloatingPoint 2 3) is represented
+      //  equivalently by (_ +oo 2 3) and (fp #b0 #b11 #b00).
+      // -0 only has one representation; i.e. (_ -zero 3 2) abbreviates (fp #b1 #b000 #b0), and
+      //  is therefore disallowed.
+      // This automatically checks the correct precision as well!
+      checkArgument(
+          specialNumbers.contains(fpConst),
+          "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. Their precision"
+              + " has to match the precision of the formula to be represented as bitvector.");
+
+      BitvectorFormula bvTerm = entry.getValue();
+      checkArgument(
+          bvMgr.getLength(bvTerm) == bvMgr.getLength(bvFormula),
+          "The size of the bitvector terms used as mapped values needs to be equal to the size of"
+              + " the bitvector returned by this method");
+
+      BooleanFormula assumption = assignment(fpConst, f);
+      toIeeeBv = bMgr.ifThenElse(assumption, bvTerm, toIeeeBv);
+    }
+
+    return BitvectorFormulaAndBooleanFormula.of(toIeeeBv, additionalConstraint);
+  }
+
+  @Override
+  public int getMantissaSizeWithSignBit(FloatingPointFormula f) {
+    return getMantissaSizeWithSignBitImpl(extractInfo(f));
+  }
+
+  protected abstract int getMantissaSizeWithSignBitImpl(TFormulaInfo f);
+
+  @Override
+  public int getExponentSize(FloatingPointFormula f) {
+    return getExponentSizeImpl(extractInfo(f));
+  }
+
+  protected abstract int getExponentSizeImpl(TFormulaInfo f);
 
   @Override
   public FloatingPointFormula negate(FloatingPointFormula pNumber) {
@@ -542,4 +648,28 @@ protected static String getBvRepresentation(BigInteger integer, int size) {
     }
     return String.copyValueOf(values);
   }
+
+  public static final class BitvectorFormulaAndBooleanFormula {
+    private final BitvectorFormula bitvectorFormula;
+    private final BooleanFormula booleanFormula;
+
+    private BitvectorFormulaAndBooleanFormula(
+        BitvectorFormula pBitvectorFormula, BooleanFormula pBooleanFormula) {
+      bitvectorFormula = checkNotNull(pBitvectorFormula);
+      booleanFormula = checkNotNull(pBooleanFormula);
+    }
+
+    private static BitvectorFormulaAndBooleanFormula of(
+        BitvectorFormula pBitvectorFormula, BooleanFormula pBooleanFormula) {
+      return new BitvectorFormulaAndBooleanFormula(pBitvectorFormula, pBooleanFormula);
+    }
+
+    public BitvectorFormula getBitvectorFormula() {
+      return bitvectorFormula;
+    }
+
+    public BooleanFormula getBooleanFormula() {
+      return booleanFormula;
+    }
+  }
 }

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

@@ -412,7 +412,23 @@ private String sanitize(String formulaStr) {
 
   @Override
   public BooleanFormula parse(String formulaStr) throws IllegalArgumentException {
-    return formulaCreator.encapsulateBoolean(parseImpl(sanitize(formulaStr)));
+    try {
+      return formulaCreator.encapsulateBoolean(parseImpl(sanitize(formulaStr)));
+    } catch (IllegalArgumentException illegalArgumentException) {
+      if (illegalArgumentException.getMessage().contains("fp.as_ieee_bv")) {
+        String additionalMessage =
+            "; Note: operation 'fp.as_ieee_bv' is not supported in most SMT solvers. Instead, try"
+                + " utilizing the SMTLIB2 keyword 'to_fp' which is supported in most SMT solvers"
+                + " with Bitvector and Floating-Point support. In case the SMTLIB2 output has been"
+                + " created using JavaSMT, try replacing the FloatingPointFormulaManager method"
+                + " toIeeeBitvector(FloatingPointFormula), with either"
+                + " toIeeeBitvector(FloatingPointFormula, String) or"
+                + " toIeeeBitvector(FloatingPointFormula, String, Map).";
+        throw new IllegalArgumentException(
+            illegalArgumentException.getMessage() + additionalMessage, illegalArgumentException);
+      }
+      throw illegalArgumentException;
+    }
   }
 
   protected abstract String dumpFormulaImpl(TFormulaInfo t) throws IOException;

src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java

@@ -10,6 +10,7 @@
 
 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.BitvectorFormula;
 import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -21,6 +22,7 @@
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
+import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula;
 
 public class DebuggingFloatingPointFormulaManager implements FloatingPointFormulaManager {
   private final FloatingPointFormulaManager delegate;
@@ -224,6 +226,36 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula number) {
     return result;
   }
 
+  @Override
+  public BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+      FloatingPointFormula number, String bitvectorConstantName) {
+    debugging.assertThreadLocal();
+    debugging.assertFormulaInContext(number);
+    BitvectorFormulaAndBooleanFormula res = delegate.toIeeeBitvector(number, bitvectorConstantName);
+    debugging.addFormulaTerm(res.getBitvectorFormula());
+    debugging.addFormulaTerm(res.getBooleanFormula());
+    return res;
+  }
+
+  @Override
+  public BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+      FloatingPointFormula number,
+      String bitvectorConstantName,
+      Map<FloatingPointFormula, BitvectorFormula> specialFPConstantHandling) {
+    debugging.assertThreadLocal();
+    debugging.assertFormulaInContext(number);
+    specialFPConstantHandling.forEach(
+        (key, value) -> {
+          debugging.assertFormulaInContext(key);
+          debugging.assertFormulaInContext(value);
+        });
+    BitvectorFormulaAndBooleanFormula res =
+        delegate.toIeeeBitvector(number, bitvectorConstantName, specialFPConstantHandling);
+    debugging.addFormulaTerm(res.getBitvectorFormula());
+    debugging.addFormulaTerm(res.getBooleanFormula());
+    return res;
+  }
+
   @Override
   public FloatingPointFormula round(
       FloatingPointFormula formula, FloatingPointRoundingMode roundingMode) {
@@ -509,4 +541,18 @@ public BooleanFormula isNegative(FloatingPointFormula number) {
     debugging.addFormulaTerm(result);
     return result;
   }
+
+  @Override
+  public int getMantissaSizeWithSignBit(FloatingPointFormula number) {
+    debugging.assertThreadLocal();
+    debugging.assertFormulaInContext(number);
+    return delegate.getMantissaSizeWithSignBit(number);
+  }
+
+  @Override
+  public int getExponentSize(FloatingPointFormula number) {
+    debugging.assertThreadLocal();
+    debugging.assertFormulaInContext(number);
+    return delegate.getExponentSize(number);
+  }
 }