Merge pull request #514 from sosy-lab/use_solver_native_bv_to_ieee-fp_CVC4_CVC5

Use Solver Native Implementation of Bitvector to IEEE FP for CVC4 and CVC5

Author: baierd

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

@@ -15,6 +15,7 @@
 import java.math.BigInteger;
 import java.util.HashMap;
 import java.util.Map;
+import org.sosy_lab.common.MoreStrings;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.BitvectorFormula;
 import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -25,6 +26,7 @@
 import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
+import org.sosy_lab.java_smt.api.FormulaType.BitvectorType;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
 
 /**
@@ -258,6 +260,14 @@ protected abstract TFormulaInfo castFromImpl(
   @Override
   public FloatingPointFormula fromIeeeBitvector(
       BitvectorFormula pNumber, FloatingPointType pTargetType) {
+    BitvectorType bvType = (BitvectorType) formulaCreator.getFormulaType(pNumber);
+    Preconditions.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));
   }
 

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java

@@ -10,13 +10,13 @@
 
 import com.google.common.collect.ImmutableList;
 import edu.stanford.CVC4.BitVector;
-import edu.stanford.CVC4.BitVectorExtract;
 import edu.stanford.CVC4.Expr;
 import edu.stanford.CVC4.ExprManager;
 import edu.stanford.CVC4.FloatingPoint;
 import edu.stanford.CVC4.FloatingPointConvertSort;
 import edu.stanford.CVC4.FloatingPointSize;
 import edu.stanford.CVC4.FloatingPointToFPFloatingPoint;
+import edu.stanford.CVC4.FloatingPointToFPIEEEBitVector;
 import edu.stanford.CVC4.FloatingPointToFPSignedBitVector;
 import edu.stanford.CVC4.FloatingPointToFPUnsignedBitVector;
 import edu.stanford.CVC4.FloatingPointToSBV;
@@ -358,20 +358,10 @@ protected Expr isNegative(Expr pParam) {
 
   @Override
   protected Expr fromIeeeBitvectorImpl(Expr bitvector, FloatingPointType pTargetType) {
-    int mantissaSize = pTargetType.getMantissaSize();
-    int exponentSize = pTargetType.getExponentSize();
-    int size = pTargetType.getTotalSize();
-    assert size == mantissaSize + exponentSize + 1;
-
-    Expr signExtract = exprManager.mkConst(new BitVectorExtract(size - 1, size - 1));
-    Expr exponentExtract = exprManager.mkConst(new BitVectorExtract(size - 2, mantissaSize));
-    Expr mantissaExtract = exprManager.mkConst(new BitVectorExtract(mantissaSize - 1, 0));
-
-    Expr sign = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, signExtract, bitvector);
-    Expr exponent = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, exponentExtract, bitvector);
-    Expr mantissa = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, mantissaExtract, bitvector);
-
-    return exprManager.mkExpr(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa);
+    // This is just named weird, but the CVC4 doc say this is IEEE BV -> FP
+    FloatingPointConvertSort fpConvertSort = new FloatingPointConvertSort(getFPSize(pTargetType));
+    Expr op = exprManager.mkConst(new FloatingPointToFPIEEEBitVector(fpConvertSort));
+    return exprManager.mkExpr(op, bitvector);
   }
 
   @Override

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java

@@ -408,29 +408,20 @@ protected Term isNegative(Term pParam) {
   }
 
   @Override
-  protected Term fromIeeeBitvectorImpl(Term bitvector, FloatingPointType pTargetType) {
-    int mantissaSize = pTargetType.getMantissaSize();
-    int exponentSize = pTargetType.getExponentSize();
-    int size = pTargetType.getTotalSize();
-    assert size == mantissaSize + exponentSize + 1;
-
-    Op signExtract;
-    Op exponentExtract;
-    Op mantissaExtract;
+  protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetType) {
     try {
-      signExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 1, size - 1);
-      exponentExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 2, mantissaSize);
-      mantissaExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, mantissaSize - 1, 0);
-    } catch (CVC5ApiException e) {
-      throw new IllegalArgumentException(
-          "You tried creating a invalid bitvector extract in term " + bitvector + ".", e);
+      return termManager.mkTerm(
+          termManager.mkOp(
+              Kind.FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
+              pTargetType.getExponentSize(),
+              pTargetType.getMantissaSize() + 1), // add sign bit
+          pBitvector);
+    } catch (CVC5ApiException cvc5ApiException) {
+      // This seems to only be thrown for wrong exponent and mantissa sizes (e.g. negative
+      // numbers, size not equal to BV size etc.). We check for this beforehand, so this should
+      // not be thrown.
+      throw new IllegalArgumentException(cvc5ApiException);
     }
-
-    Term sign = termManager.mkTerm(signExtract, bitvector);
-    Term exponent = termManager.mkTerm(exponentExtract, bitvector);
-    Term mantissa = termManager.mkTerm(mantissaExtract, bitvector);
-
-    return termManager.mkTerm(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa);
   }
 
   @Override

src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java

@@ -1098,6 +1098,27 @@ public void checkString2FpConversion64() throws SolverException, InterruptedExce
                 fpmgr.makeNumber(Double.toString(pDouble), doublePrecType)));
   }
 
+  @Test
+  public void checkErrorOnInvalidSize_IeeeBv2FpConversion() {
+    BitvectorFormula bv = bvmgr.makeBitvector(9, 123);
+
+    var exSingle =
+        assertThrows(
+            IllegalArgumentException.class, () -> fpmgr.fromIeeeBitvector(bv, singlePrecType));
+    assertThat(exSingle.getMessage())
+        .contains(
+            "The total size 32 of type FloatingPoint<exp=8,mant=23> "
+                + "has to match the size 9 of type Bitvector<9>.");
+
+    var exDouble =
+        assertThrows(
+            IllegalArgumentException.class, () -> fpmgr.fromIeeeBitvector(bv, doublePrecType));
+    assertThat(exDouble.getMessage())
+        .contains(
+            "The total size 64 of type FloatingPoint<exp=11,mant=52> "
+                + "has to match the size 9 of type Bitvector<9>.");
+  }
+
   @Test
   public void checkIeeeBv2FpConversion32() throws SolverException, InterruptedException {
     proveForAll(