Add IEEE-754 Floating Point to Bitvector Conversion Fallback

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

@@ -299,12 +299,43 @@ FloatingPointFormula castFrom(
   FloatingPointFormula fromIeeeBitvector(BitvectorFormula number, FloatingPointType pTargetType);
 
   /**
-   * Create a formula that produces a representation of the given floating-point value as a
-   * bitvector conforming to the IEEE 754-2008 FP format. The bit size of the resulting bitvector is
-   * equal to the total size of the {@link FloatingPointNumber}s precision.
+   * Returns a {@link BitvectorFormula} equal to the representation of the given floating-point
+   * value as a bitvector conforming to the IEEE 754-2008 FP format. The bit size of the resulting
+   * bitvector is equal to the {@link FloatingPointType#getTotalSize()} of the {@link
+   * FloatingPointFormula}. This method is not natively supported by all solvers, and SMTLIB2 output
+   * generated containing formulas originating from this method is often not parsable by other
+   * solvers. You can use the method {@link #bitwiseEqual(FloatingPointFormula, BitvectorFormula)}
+   * to avoid both problems.
    */
   BitvectorFormula toIeeeBitvector(FloatingPointFormula number);
 
+  /**
+   * Create a {@link BooleanFormula} representing the equality of the bitvector representation of
+   * the given {@link FloatingPointFormula}s value, conforming to the IEEE 754-2008 floating-point
+   * format, with the given {@link BitvectorFormula}. The size of the given {@link BitvectorFormula}
+   * has to be equal to the size returned by {@link FloatingPointType#getTotalSize()} of the given
+   * {@link FloatingPointFormula}. 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 solver dependent. This method is based on a suggestion in the (<a
+   * href="https://smt-lib.org/theories-FloatingPoint.shtml">SMTLIB2 standard</a>) and is equal to:
+   *
+   * <p>assignment(fromIeeeBitvector(bitvectorValue), floatValue)
+   *
+   * <p>Note: SMTLIB2 output of this method uses the SMTLIB2 function symbol 'to_fp', for example
+   * like this: (assert (= ((_ to_fp eb sb) bitvectorValue) floatValue)) with eb being the bit size
+   * returned by {@link FloatingPointType#getExponentSize()} and sb being the bit size returned by
+   * {@link FloatingPointType#getMantissaSizeWithHiddenBit()} of the {@link FloatingPointType} of
+   * floatValue.
+   *
+   * @param floatValue the {@link FloatingPointFormula} to be converted into an IEEE bitvector.
+   * @param bitvectorValue a {@link BitvectorFormula} that is set to be equal to the IEEE bitvector
+   *     representation of the {@link FloatingPointFormula} parameter.
+   * @return a {@link BooleanFormula} representing the result of the equality of the two parameters,
+   *     i.e. (= ((_ to_fp eb sb) bitvectorValue) floatValue).
+   */
+  BooleanFormula bitwiseEqual(FloatingPointFormula floatValue, BitvectorFormula bitvectorValue);
+
   FloatingPointFormula round(FloatingPointFormula formula, FloatingPointRoundingMode roundingMode);
 
   // ----------------- Arithmetic relations, return type NumeralFormula -----------------

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

@@ -8,13 +8,15 @@
 
 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.basicimpl.AbstractFormulaManager.checkVariableName;
 
-import com.google.common.base.Preconditions;
 import java.math.BigDecimal;
 import java.math.BigInteger;
 import java.util.HashMap;
 import java.util.Map;
+import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.MoreStrings;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.BitvectorFormula;
@@ -48,10 +50,14 @@ public abstract class AbstractFloatingPointFormulaManager<TFormulaInfo, TType, T
 
   private final Map<FloatingPointRoundingMode, TFormulaInfo> roundingModes;
 
+  private final AbstractBitvectorFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> bvMgr;
+
   protected AbstractFloatingPointFormulaManager(
-      FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl> pCreator) {
+      FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl> pCreator,
+      AbstractBitvectorFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> pBvMgr) {
     super(pCreator);
     roundingModes = new HashMap<>();
+    bvMgr = pBvMgr;
   }
 
   protected abstract TFormulaInfo getDefaultRoundingMode();
@@ -75,44 +81,76 @@ public FloatingPointRoundingMode fromRoundingModeFormula(
     return getFormulaCreator().getRoundingMode(extractInfo(pRoundingModeFormula));
   }
 
-  protected FloatingPointFormula wrap(TFormulaInfo pTerm) {
+  /**
+   * Wraps a native floating-point term in a JavaSMT {@link FloatingPointFormula}. If the {@link
+   * FloatingPointType} of the term is not available, please use {@link
+   * AbstractFloatingPointFormulaManager#wrap(Object)}
+   *
+   * @param pTypeForAssertions the {@link FloatingPointType} used to create pTerm. This argument is
+   *     only used to verify the exponent and mantissa sizes of pTerm.
+   */
+  protected FloatingPointFormula wrap(
+      TFormulaInfo pTerm, @Nullable FloatingPointType pTypeForAssertions) {
+    FormulaType<?> type = getFormulaCreator().getFormulaType(pTerm);
+    // The type derived from the term in the creator is usually built from the exponent and
+    // mantissa sizes, hence comparing it to the type used to create the FP term checks that it
+    // was created correctly. (There are other tests checking FP type correctness)
+    if (pTypeForAssertions != null) {
+      assert type.equals(pTypeForAssertions)
+          : "Floating-Point formula %s with type %s is not equal to expected type %s"
+              .formatted(pTerm, type, pTypeForAssertions);
+    } else {
+      assert type.isFloatingPointType()
+          : "Floating-Point formula %s has unexpected type: %s".formatted(pTerm, type);
+    }
+
     return getFormulaCreator().encapsulateFloatingPoint(pTerm);
   }
 
+  /**
+   * Wraps a native floating-point term in a JavaSMT {@link FloatingPointFormula}. Please use {@link
+   * AbstractFloatingPointFormulaManager#wrap(Object, FloatingPointType)} if the {@link
+   * FloatingPointType} of the term is available.
+   */
+  protected FloatingPointFormula wrap(TFormulaInfo pTerm) {
+    return wrap(pTerm, null);
+  }
+
   @Override
   public FloatingPointFormula makeNumber(Rational n, FormulaType.FloatingPointType type) {
-    return wrap(makeNumberImpl(n.toString(), type, getDefaultRoundingMode()));
+    return wrap(makeNumberImpl(n.toString(), type, getDefaultRoundingMode()), type);
   }
 
   @Override
   public FloatingPointFormula makeNumber(
       Rational n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode) {
-    return wrap(makeNumberImpl(n.toString(), type, getRoundingMode(pFloatingPointRoundingMode)));
+    return wrap(
+        makeNumberImpl(n.toString(), type, getRoundingMode(pFloatingPointRoundingMode)), type);
   }
 
   @Override
   public FloatingPointFormula makeNumber(double n, FormulaType.FloatingPointType type) {
-    return wrap(makeNumberImpl(n, type, getDefaultRoundingMode()));
+    return wrap(makeNumberImpl(n, type, getDefaultRoundingMode()), type);
   }
 
   @Override
   public FloatingPointFormula makeNumber(
       double n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode) {
-    return wrap(makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode)));
+    return wrap(makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode)), type);
   }
 
   protected abstract TFormulaInfo makeNumberImpl(
       double n, FormulaType.FloatingPointType type, TFormulaInfo pFloatingPointRoundingMode);
 
   @Override
   public FloatingPointFormula makeNumber(BigDecimal n, FormulaType.FloatingPointType type) {
-    return wrap(makeNumberImpl(n, type, getDefaultRoundingMode()));
+    return wrap(makeNumberImpl(n, type, getDefaultRoundingMode()), type);
   }
 
   @Override
   public FloatingPointFormula makeNumber(
       BigDecimal n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode) {
-    return wrap(makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode)));
+    return wrap(makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode)), type);
   }
 
   protected TFormulaInfo makeNumberImpl(
@@ -122,13 +160,13 @@ protected TFormulaInfo makeNumberImpl(
 
   @Override
   public FloatingPointFormula makeNumber(String n, FormulaType.FloatingPointType type) {
-    return wrap(makeNumberImpl(n, type, getDefaultRoundingMode()));
+    return wrap(makeNumberImpl(n, type, getDefaultRoundingMode()), type);
   }
 
   @Override
   public FloatingPointFormula makeNumber(
       String n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode) {
-    return wrap(makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode)));
+    return wrap(makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode)), type);
   }
 
   /** directly catch the most common special String constants. */
@@ -148,14 +186,14 @@ protected TFormulaInfo makeNumberImpl(
   @Override
   public FloatingPointFormula makeNumber(
       BigInteger exponent, BigInteger mantissa, Sign sign, FloatingPointType type) {
-    return wrap(makeNumberImpl(exponent, mantissa, sign, type));
+    return wrap(makeNumberImpl(exponent, mantissa, sign, type), type);
   }
 
   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);
   }
 
@@ -171,29 +209,29 @@ protected abstract TFormulaInfo makeNumberAndRound(
   @Override
   public FloatingPointFormula makeVariable(String pVar, FormulaType.FloatingPointType pType) {
     checkVariableName(pVar);
-    return wrap(makeVariableImpl(pVar, pType));
+    return wrap(makeVariableImpl(pVar, pType), pType);
   }
 
   protected abstract TFormulaInfo makeVariableImpl(
       String pVar, FormulaType.FloatingPointType pType);
 
   @Override
   public FloatingPointFormula makePlusInfinity(FormulaType.FloatingPointType pType) {
-    return wrap(makePlusInfinityImpl(pType));
+    return wrap(makePlusInfinityImpl(pType), pType);
   }
 
   protected abstract TFormulaInfo makePlusInfinityImpl(FormulaType.FloatingPointType pType);
 
   @Override
   public FloatingPointFormula makeMinusInfinity(FormulaType.FloatingPointType pType) {
-    return wrap(makeMinusInfinityImpl(pType));
+    return wrap(makeMinusInfinityImpl(pType), pType);
   }
 
   protected abstract TFormulaInfo makeMinusInfinityImpl(FormulaType.FloatingPointType pType);
 
   @Override
   public FloatingPointFormula makeNaN(FormulaType.FloatingPointType pType) {
-    return wrap(makeNaNImpl(pType));
+    return wrap(makeNaNImpl(pType), pType);
   }
 
   protected abstract TFormulaInfo makeNaNImpl(FormulaType.FloatingPointType pType);
@@ -232,7 +270,9 @@ protected abstract TFormulaInfo castToImpl(
   @Override
   public FloatingPointFormula castFrom(
       Formula pNumber, boolean pSigned, FormulaType.FloatingPointType pTargetType) {
-    return wrap(castFromImpl(extractInfo(pNumber), pSigned, pTargetType, getDefaultRoundingMode()));
+    return wrap(
+        castFromImpl(extractInfo(pNumber), pSigned, pTargetType, getDefaultRoundingMode()),
+        pTargetType);
   }
 
   @Override
@@ -243,7 +283,8 @@ public FloatingPointFormula castFrom(
       FloatingPointRoundingMode pFloatingPointRoundingMode) {
     return wrap(
         castFromImpl(
-            extractInfo(number), signed, targetType, getRoundingMode(pFloatingPointRoundingMode)));
+            extractInfo(number), signed, targetType, getRoundingMode(pFloatingPointRoundingMode)),
+        targetType);
   }
 
   protected abstract TFormulaInfo castFromImpl(
@@ -256,7 +297,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(
             () ->
@@ -273,7 +314,34 @@ 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 "
+            + "floating-point formulas to IEEE bitvectors natively");
+  }
+
+  @Override
+  public BooleanFormula bitwiseEqual(
+      FloatingPointFormula floatValue, BitvectorFormula bitvectorValue) {
+    FormulaType.FloatingPointType fpType =
+        (FloatingPointType) getFormulaCreator().getFormulaType(floatValue);
+    checkArgument(
+        fpType.getTotalSize() == bvMgr.getLength(bitvectorValue),
+        "The size of the bitvector term %s is %s, but needs to be equal to the size of"
+            + " the Floating-Point term %s with size %s",
+        bitvectorValue,
+        bvMgr.getLength(bitvectorValue),
+        floatValue,
+        fpType.getTotalSize());
+
+    FloatingPointFormula fromIeeeBitvector = fromIeeeBitvector(bitvectorValue, fpType);
+
+    // We use assignment(), as it allows a fp 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.
+    return assignment(fromIeeeBitvector, floatValue);
+  }
 
   @Override
   public FloatingPointFormula negate(FloatingPointFormula pNumber) {

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

@@ -377,23 +377,28 @@ protected List<TFormulaInfo> parseAllImpl(String formulaStr) throws IllegalArgum
     ImmutableList.Builder<String> declarationTokens = ImmutableList.builder();
     ImmutableList.Builder<String> definitionTokens = ImmutableList.builder();
     ImmutableList.Builder<String> assertTokens = ImmutableList.builder();
-    for (String token : SMTLibTokenizer.of(formulaStr)) {
-      if (SMTLibTokenizer.isDeclarationToken(token)) {
-        declarationTokens.add(token);
-      }
-      if (SMTLibTokenizer.isDefinitionToken(token)) {
-        definitionTokens.add(token);
-      }
-      if (SMTLibTokenizer.isAssertToken(token)) {
-        assertTokens.add(token);
+    try {
+      for (String token : SMTLibTokenizer.of(formulaStr)) {
+        if (SMTLibTokenizer.isDeclarationToken(token)) {
+          declarationTokens.add(token);
+        }
+        if (SMTLibTokenizer.isDefinitionToken(token)) {
+          definitionTokens.add(token);
+        }
+        if (SMTLibTokenizer.isAssertToken(token)) {
+          assertTokens.add(token);
+        }
       }
-    }
-    String definitions =
-        Joiner.on("").join(declarationTokens.build())
-            + Joiner.on("").join(definitionTokens.build());
+      String definitions =
+          Joiner.on("").join(declarationTokens.build())
+              + Joiner.on("").join(definitionTokens.build());
+
+      return Collections3.transformedImmutableListCopy(
+          assertTokens.build(), assertion -> parseImpl(definitions + assertion));
 
-    return Collections3.transformedImmutableListCopy(
-        assertTokens.build(), assertion -> parseImpl(definitions + assertion));
+    } catch (IllegalArgumentException illegalArgumentException) {
+      throw throwIllegalArgumentExceptionWithBetterErrorMessage(illegalArgumentException);
+    }
   }
 
   /**
@@ -1046,4 +1051,29 @@ void applySetLogicCommand() {
       }
     }
   }
+
+  /**
+   * Returns the given {@link IllegalArgumentException} with a potentially improved error message.
+   * For example: the 'as_ieee_bv' and 'to_ieee_bv' operations are not supported by all SMT solvers,
+   * as the standard does not define those. We add an explanation to error messages containing those
+   * operations that explain how to build SMTLIB2 conforming and well accepted SMTLIB2.
+   *
+   * @param illegalArgumentException original {@link IllegalArgumentException} wrapping a solvers or
+   *     our initial error message from parsing SMTLIB2.
+   * @return a {@link IllegalArgumentException} that should be thrown in all cases. Might be the
+   *     original exception.
+   */
+  private IllegalArgumentException throwIllegalArgumentExceptionWithBetterErrorMessage(
+      IllegalArgumentException illegalArgumentException) throws IllegalArgumentException {
+    final String msg = illegalArgumentException.getMessage();
+    if (msg != null && (msg.contains("to_ieee_bv") || msg.contains("as_ieee_bv"))) {
+      // Better error message for certain cases, explaining common problems
+      final String additionalMessage =
+          "; Note: operations 'to_ieee_bv' and 'as_ieee_bv' are not supported in most SMT"
+              + " solvers. You can try using the SMTLIB2 standards preferred way to encode this"
+              + " operation by utilizing the 'to_fp' operation.";
+      return new IllegalArgumentException(msg + additionalMessage, illegalArgumentException);
+    }
+    return illegalArgumentException;
+  }
 }

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

@@ -165,10 +165,6 @@ protected BitvectorFormula encapsulateBitvector(TFormulaInfo pTerm) {
   }
 
   protected FloatingPointFormula encapsulateFloatingPoint(TFormulaInfo pTerm) {
-    checkArgument(
-        getFormulaType(pTerm).isFloatingPointType(),
-        "Floatingpoint formula has unexpected type: %s",
-        getFormulaType(pTerm));
     return new FloatingPointFormulaImpl<>(pTerm);
   }
 

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

@@ -224,6 +224,17 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula number) {
     return result;
   }
 
+  @Override
+  public BooleanFormula bitwiseEqual(
+      FloatingPointFormula floatValue, BitvectorFormula bitvectorValue) {
+    debugging.assertThreadLocal();
+    debugging.assertFormulaInContext(floatValue);
+    debugging.assertFormulaInContext(bitvectorValue);
+    BooleanFormula res = delegate.bitwiseEqual(floatValue, bitvectorValue);
+    debugging.addFormulaTerm(res);
+    return res;
+  }
+
   @Override
   public FloatingPointFormula round(
       FloatingPointFormula formula, FloatingPointRoundingMode roundingMode) {