Add new floating point literal constructor using IEEE754 bitpattern

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

@@ -9,6 +9,7 @@
 package org.sosy_lab.java_smt.api;
 
 import java.math.BigDecimal;
+import java.math.BigInteger;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
 
@@ -41,6 +42,9 @@ FloatingPointFormula makeNumber(
   FloatingPointFormula makeNumber(
       Rational n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode);
 
+  FloatingPointFormula makeNumber(
+      BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type);
+
   /**
    * Creates a variable with exactly the given name.
    *

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

@@ -12,6 +12,7 @@
 
 import com.google.common.base.Preconditions;
 import java.math.BigDecimal;
+import java.math.BigInteger;
 import java.util.HashMap;
 import java.util.Map;
 import org.sosy_lab.common.rationals.Rational;
@@ -133,6 +134,15 @@ protected TFormulaInfo makeNumberImpl(
     }
   }
 
+  @Override
+  public FloatingPointFormula makeNumber(
+      BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) {
+    return wrap(makeNumberImpl(exponent, mantissa, signBit, type));
+  }
+
+  protected abstract TFormulaInfo makeNumberImpl(
+      BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type);
+
   protected static boolean isNegativeZero(Double pN) {
     Preconditions.checkNotNull(pN);
     return Double.valueOf("-0.0").equals(pN);
@@ -486,4 +496,12 @@ public FloatingPointFormula round(
 
   protected abstract TFormulaInfo round(
       TFormulaInfo pFormula, FloatingPointRoundingMode pRoundingMode);
+
+  protected static String getBvRepresentation(BigInteger integer, int size) {
+    char[] values = new char[size];
+    for (int i = 0; i < size; i++) {
+      values[size - 1 - i] = integer.testBit(i) ? '1' : '0';
+    }
+    return String.copyValueOf(values);
+  }
 }

src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java

@@ -11,6 +11,7 @@
 import static com.google.common.base.Preconditions.checkNotNull;
 
 import java.math.BigDecimal;
+import java.math.BigInteger;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.BitvectorFormula;
 import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -86,6 +87,13 @@ public FloatingPointFormula makeNumber(
     return delegate.makeNumber(pN, pType, pFloatingPointRoundingMode);
   }
 
+  @Override
+  public FloatingPointFormula makeNumber(
+      BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) {
+    stats.fpOperations.getAndIncrement();
+    return delegate.makeNumber(exponent, mantissa, signBit, type);
+  }
+
   @Override
   public FloatingPointFormula makeVariable(String pVar, FloatingPointType pType) {
     stats.fpOperations.getAndIncrement();

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java

@@ -11,6 +11,7 @@
 import static com.google.common.base.Preconditions.checkNotNull;
 
 import java.math.BigDecimal;
+import java.math.BigInteger;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.BitvectorFormula;
 import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -95,6 +96,14 @@ public FloatingPointFormula makeNumber(
     }
   }
 
+  @Override
+  public FloatingPointFormula makeNumber(
+      BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) {
+    synchronized (sync) {
+      return delegate.makeNumber(exponent, mantissa, signBit, type);
+    }
+  }
+
   @Override
   public FloatingPointFormula makeVariable(String pVar, FloatingPointType pType) {
     synchronized (sync) {

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

@@ -10,6 +10,7 @@
 
 import com.google.common.collect.ImmutableList;
 import com.microsoft.z3.Native;
+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 +71,30 @@ 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.getBvSortSize(z3context, Native.getSort(z3context, signBv)) == 1
+        : "SignBV should be 1 bit long";
+    assert Native.getBvSortSize(z3context, Native.getSort(z3context, expoBv))
+            == type.getExponentSize()
+        : "ExpoBV should be " + type.getExponentSize() + " bits long";
+    assert Native.getBvSortSize(z3context, Native.getSort(z3context, mantBv))
+            == type.getMantissaSize()
+        : "MantBV should be " + type.getMantissaSize() + " bits long";
+
+    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, singlePrecType);
+    final FloatingPointFormula expr2 =
+        fpmgr.makeNumber(
+            BigInteger.valueOf(123), BigInteger.valueOf(5033165), true, singlePrecType);
+    assertThatFormula(fpmgr.assignment(expr1, expr2)).isTautological();
+  }
 }