Added implementation and tests

Author: leventeBajczi

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

@@ -10,6 +10,7 @@
 
 import com.google.common.collect.ImmutableList;
 import edu.stanford.CVC4.BitVectorExtract;
+import edu.stanford.CVC4.BitVector;
 import edu.stanford.CVC4.Expr;
 import edu.stanford.CVC4.ExprManager;
 import edu.stanford.CVC4.FloatingPoint;
@@ -82,6 +83,19 @@ protected Expr makeNumberImpl(double pN, FloatingPointType pType, Expr pRounding
     return makeNumberImpl(Double.toString(pN), pType, pRoundingMode);
   }
 
+  @Override
+  protected Expr makeNumberImpl(
+      BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) {
+    final String signStr = signBit ? "1" : "0";
+    final String exponentStr = getBvRepresentation(exponent, type.getExponentSize());
+    final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSize());
+    final String bitvecStr = signStr + exponentStr + mantissaStr;
+    final BitVector bitVector = new BitVector(bitvecStr, 2);
+    final FloatingPoint fp =
+        new FloatingPoint(type.getExponentSize(), type.getMantissaSize() + 1, bitVector);
+    return exprManager.mkConst(fp);
+  }
+
   @Override
   protected Expr makeNumberAndRound(String pN, FloatingPointType pType, Expr pRoundingMode) {
     try {

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

@@ -17,6 +17,7 @@
 import io.github.cvc5.Sort;
 import io.github.cvc5.Term;
 import java.math.BigDecimal;
+import java.math.BigInteger;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
 import org.sosy_lab.java_smt.api.FormulaType;
@@ -66,6 +67,23 @@ protected Term makeNumberImpl(double pN, FloatingPointType pType, Term pRounding
     return makeNumberImpl(Double.toString(pN), pType, pRoundingMode);
   }
 
+  @Override
+  protected Term makeNumberImpl(
+      BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) {
+    try {
+      final String signStr = signBit ? "1" : "0";
+      final String exponentStr = getBvRepresentation(exponent, type.getExponentSize());
+      final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSize());
+      final String bitvecForm = signStr + exponentStr + mantissaStr;
+
+      final Term bv =
+          solver.mkBitVector(type.getExponentSize() + type.getMantissaSize() + 1, bitvecForm, 2);
+      return solver.mkFloatingPoint(type.getExponentSize(), type.getMantissaSize() + 1, bv);
+    } catch (CVC5ApiException e) {
+      throw new IllegalArgumentException("You tried creating a invalid bitvector", e);
+    }
+  }
+
   @Override
   protected Term makeNumberAndRound(String pN, FloatingPointType pType, Term pRoundingMode) {
     try {

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java

@@ -10,6 +10,7 @@
 
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_equal;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_abs;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_bits_number;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_cast;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_div;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_equal;
@@ -45,6 +46,7 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_get_type;
 
 import com.google.common.collect.ImmutableList;
+import java.math.BigInteger;
 import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
@@ -94,6 +96,18 @@ protected Long makeNumberImpl(double pN, FloatingPointType pType, Long pRounding
     return makeNumberImpl(Double.toString(pN), pType, pRoundingMode);
   }
 
+  @Override
+  protected Long makeNumberImpl(
+      BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) {
+    final String signStr = signBit ? "1" : "0";
+    final String exponentStr = getBvRepresentation(exponent, type.getExponentSize());
+    final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSize());
+    final String bitvecForm = signStr + exponentStr + mantissaStr;
+    final BigInteger bitvecValue = new BigInteger(bitvecForm, 2);
+    return msat_make_fp_bits_number(
+        mathsatEnv, bitvecValue.toString(), type.getExponentSize(), type.getMantissaSize());
+  }
+
   @Override
   protected Long makeNumberAndRound(String pN, FloatingPointType pType, Long pRoundingMode) {
     try {

src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java

@@ -8,8 +8,11 @@
 
 package org.sosy_lab.java_smt.solvers.z3;
 
+import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableList;
 import com.microsoft.z3.Native;
+import com.microsoft.z3.Z3Exception;
+import java.math.BigInteger;
 import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
@@ -70,6 +73,24 @@ protected Long makeNumberImpl(double pN, FloatingPointType pType, Long pRounding
     return makeNumberImpl(Double.toString(pN), pType, pRoundingMode);
   }
 
+  @Override
+  protected Long makeNumberImpl(
+      BigInteger exponent,
+      BigInteger mantissa,
+      boolean signBit,
+      FloatingPointType type) {
+
+    long signBv = Native.mkBvNumeral(z3context, 1, new boolean[]{signBit});
+    long expoBv = Native.mkNumeral(z3context, exponent.toString(), Native.mkBvSort(z3context,
+        type.getExponentSize()));
+    long mantBv = Native.mkNumeral(z3context, mantissa.toString(), Native.mkBvSort(z3context,
+        type.getMantissaSize()));
+
+    assert Native.getSort(z3context, signBv) != Native.getSort(z3context, mantBv);
+
+    return Native.mkFpaFp(z3context, signBv, expoBv, mantBv);
+  }
+
   @Override
   protected Long makeNumberAndRound(String pN, FloatingPointType pType, Long pRoundingMode) {
     // Z3 does not allow specifying a rounding mode for numerals,

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

@@ -18,6 +18,7 @@
 import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Lists;
 import java.math.BigDecimal;
+import java.math.BigInteger;
 import java.util.List;
 import java.util.Random;
 import org.junit.Before;
@@ -949,4 +950,13 @@ public void failOnInvalidString() {
     fpmgr.makeNumber("a", singlePrecType);
     assert_().fail();
   }
+
+  @Test
+  public void fpFromBitPattern() throws SolverException, InterruptedException {
+    final FloatingPointFormula expr1 = fpmgr.makeNumber(-0.1, doublePrecType);
+    final FloatingPointFormula expr2 =
+        fpmgr.makeNumber(
+            BigInteger.valueOf(123), BigInteger.valueOf(5033165), true, doublePrecType);
+    assertThatFormula(fpmgr.assignment(expr1, expr2)).isTautological();
+  }
 }