Add IEEE-754 Floating Point to Bitvector Conversion Fallback

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

@@ -299,12 +299,49 @@ 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 total size of the {@link FloatingPointFormula}s {@link
+   * FloatingPointType}. 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 #toIeeeBitvector(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 with the given {@link BitvectorFormula},
+   * conforming to the IEEE 754-2008 floating-point format. The size m of the given {@link
+   * BitvectorFormula} has to be equal to the sum of the sizes of the exponent eb and mantissa sb
+   * (including the hidden bit) 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>), with eb
+   * being the {@link FloatingPointFormula}s exponent bit size, sb being its mantissa with the
+   * hidden bit, and eb + sb equal to the bit size of the used {@link BitvectorFormula} parameter,
+   * illustrated in SMTLIB2 as:
+   *
+   * <p>(= ((_ to_fp eb sb) bitvectorFormulaSetToBeEqualToFpNumber) fpNumber)
+   *
+   * <p>Example usage in SMTLIB2, asserting the equality of the 2 parameters:
+   *
+   * <p>(declare-fun bitvectorFormulaSetToBeEqualToFpNumber () (_ BitVec m))
+   *
+   * <p>(assert (= ((_ to_fp eb sb) bitvectorFormulaSetToBeEqualToFpNumber) fpNumber))
+   *
+   * <p>Note: SMTLIB2 output of this method uses the SMTLIB2 keyword 'to_fp' as described above.
+   *
+   * @param fpNumber the {@link FloatingPointFormula} to be converted into an IEEE bitvector.
+   * @param bitvectorFormulaSetToBeEqualToFpNumber 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) bitvectorFormulaSetToBeEqualToFpNumber) fpNumber).
+   */
+  BooleanFormula toIeeeBitvector(
+      FloatingPointFormula fpNumber, BitvectorFormula bitvectorFormulaSetToBeEqualToFpNumber);
+
   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,82 @@ 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) {
+      checkArgument(
+          type.equals(pTypeForAssertions),
+          "Floating-Point formula %s type %s is not equal to expected type %s",
+          pTerm,
+          type,
+          pTypeForAssertions);
+    } else {
+      checkArgument(
+          type.isFloatingPointType(),
+          "Floating-Point formula %s has unexpected type: %s",
+          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 +166,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. */
@@ -153,14 +197,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);
   }
 
@@ -176,29 +220,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);
@@ -237,7 +281,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
@@ -248,7 +294,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(
@@ -261,14 +308,14 @@ 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(
             () ->
                 String.format(
                     "The total size %s of type %s has to match the size %s of type %s.",
                     pTargetType.getTotalSize(), pTargetType, bvType.getSize(), bvType)));
-    return wrap(fromIeeeBitvectorImpl(extractInfo(pNumber), pTargetType));
+    return wrap(fromIeeeBitvectorImpl(extractInfo(pNumber), pTargetType), pTargetType);
   }
 
   protected abstract TFormulaInfo fromIeeeBitvectorImpl(
@@ -279,7 +326,35 @@ 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 toIeeeBitvector(
+      FloatingPointFormula fpNumber, BitvectorFormula bitvectorFormulaSetToBeEqualToFpNumber) {
+    FormulaType.FloatingPointType fpType =
+        (FloatingPointType) getFormulaCreator().getFormulaType(fpNumber);
+    checkArgument(
+        fpType.getTotalSize() == bvMgr.getLength(bitvectorFormulaSetToBeEqualToFpNumber),
+        "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",
+        bitvectorFormulaSetToBeEqualToFpNumber,
+        bvMgr.getLength(bitvectorFormulaSetToBeEqualToFpNumber),
+        fpNumber,
+        fpType.getTotalSize());
+
+    FloatingPointFormula fromIeeeBitvector =
+        fromIeeeBitvector(bitvectorFormulaSetToBeEqualToFpNumber, 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, fpNumber);
+  }
 
   @Override
   public FloatingPointFormula negate(FloatingPointFormula pNumber) {

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

@@ -366,22 +366,27 @@ protected TFormulaInfo parseImpl(String formulaStr) throws IllegalArgumentExcept
 
   @ForOverride
   protected List<TFormulaInfo> parseAllImpl(String formulaStr) throws IllegalArgumentException {
-    // The fallback implementation splits the input into declarations and assertions,
-    // and parses each assertion separately,
-    // which is not very efficient, but it works for simple cases and is better than nothing
-    List<String> tokens = Tokenizer.tokenize(formulaStr);
-
-    List<String> declarationTokens =
-        tokens.stream().filter(Tokenizer::isDeclarationToken).collect(Collectors.toList());
-    List<String> definitionTokens =
-        tokens.stream().filter(Tokenizer::isDefinitionToken).collect(Collectors.toList());
-    List<String> assertTokens =
-        tokens.stream().filter(Tokenizer::isAssertToken).collect(Collectors.toList());
-    String definitions =
-        Joiner.on("").join(declarationTokens) + Joiner.on("").join(definitionTokens);
-
-    return Collections3.transformedImmutableListCopy(
-        assertTokens, assertion -> parseImpl(definitions + assertion));
+    try {
+      // The fallback implementation splits the input into declarations and assertions,
+      // and parses each assertion separately,
+      // which is not very efficient, but it works for simple cases and is better than nothing
+      List<String> tokens = Tokenizer.tokenize(formulaStr);
+
+      List<String> declarationTokens =
+          tokens.stream().filter(Tokenizer::isDeclarationToken).collect(Collectors.toList());
+      List<String> definitionTokens =
+          tokens.stream().filter(Tokenizer::isDefinitionToken).collect(Collectors.toList());
+      List<String> assertTokens =
+          tokens.stream().filter(Tokenizer::isAssertToken).collect(Collectors.toList());
+      String definitions =
+          Joiner.on("").join(declarationTokens) + Joiner.on("").join(definitionTokens);
+
+      return Collections3.transformedImmutableListCopy(
+          assertTokens, assertion -> parseImpl(definitions + assertion));
+
+    } catch (IllegalArgumentException illegalArgumentException) {
+      throw throwIllegalArgumentExceptionWithBetterErrorMessage(illegalArgumentException);
+    }
   }
 
   /**
@@ -811,4 +816,29 @@ public final String unescape(String pVar) {
     }
     return pVar; // unchanged
   }
+
+  /**
+   * 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;
+  }
 }