diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index 694e47b40c..c6b8a6eae9 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/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. * diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 766fbd5c2f..c13e652e77 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/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); + } } diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java index c4b80213bf..a8f503f8a5 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java +++ b/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(); diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java index b90727b8e1..207fc00f0c 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java +++ b/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) { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java index 90b03909c1..b867719194 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -9,6 +9,7 @@ package org.sosy_lab.java_smt.solvers.cvc4; 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; @@ -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 { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java index 692f1a0aa4..1e95a93f2e 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/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 { diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java index b4f01d2449..9bb808be16 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java +++ b/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 { diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java index 4b88885022..14a03e3d55 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java +++ b/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,28 @@ 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 Long signSort = getFormulaCreator().getBitvectorType(1); + final Long expoSort = getFormulaCreator().getBitvectorType(type.getExponentSize()); + final Long mantSort = getFormulaCreator().getBitvectorType(type.getMantissaSize()); + + final Long signBv = Native.mkNumeral(z3context, signBit ? "1" : "0", signSort); + Native.incRef(z3context, signBv); + final Long expoBv = Native.mkNumeral(z3context, exponent.toString(), expoSort); + Native.incRef(z3context, expoBv); + final Long mantBv = Native.mkNumeral(z3context, mantissa.toString(), mantSort); + Native.incRef(z3context, mantBv); + + final Long fp = Native.mkFpaFp(z3context, signBv, expoBv, mantBv); + Native.decRef(z3context, mantBv); + Native.decRef(z3context, expoBv); + Native.decRef(z3context, signBv); + return fp; + } + @Override protected Long makeNumberAndRound(String pN, FloatingPointType pType, Long pRoundingMode) { // Z3 does not allow specifying a rounding mode for numerals, diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index f66699bf47..93e00f8836 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/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; @@ -776,12 +777,16 @@ private List getListOfFloats() { Float.MAX_VALUE, Float.POSITIVE_INFINITY, Float.NEGATIVE_INFINITY, - 0.0f // , -0.0f // MathSat5 fails for NEGATIVE_ZERO - ); + 0.0f, // , -0.0f // MathSat5 fails for NEGATIVE_ZERO + 1f, + -1f, + 2f, + -2f); for (int i = 1; i < 20; i++) { for (int j = 1; j < 20; j++) { flts.add((float) (i * Math.pow(10, j))); + flts.add((float) (-i * Math.pow(10, j))); } } @@ -805,12 +810,16 @@ private List getListOfDoubles() { Double.MAX_VALUE, Double.POSITIVE_INFINITY, Double.NEGATIVE_INFINITY, - 0.0 // , -0.0 // MathSat5 fails for NEGATIVE_ZERO - ); + 0.0, // , -0.0 // MathSat5 fails for NEGATIVE_ZERO + 1d, + -1d, + 2d, + -2d); for (int i = 1; i < 20; i++) { for (int j = 1; j < 20; j++) { dbls.add(i * Math.pow(10, j)); + dbls.add(-i * Math.pow(10, j)); } } @@ -949,4 +958,34 @@ public void failOnInvalidString() { fpmgr.makeNumber("a", singlePrecType); assert_().fail(); } + + @Test + public void fpFrom32BitPattern() throws SolverException, InterruptedException { + for (float f : getListOfFloats()) { + int bits = Float.floatToRawIntBits(f); + int exponent = (bits >>> 23) & 0xFF; + int mantissa = bits & 0x7FFFFF; + boolean sign = bits < 0; // equal to: (bits >>> 31) & 0x1 + final FloatingPointFormula fpFromBv = + fpmgr.makeNumber( + BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, singlePrecType); + final FloatingPointFormula fp = fpmgr.makeNumber(f, singlePrecType); + assertThatFormula(fpmgr.assignment(fpFromBv, fp)).isTautological(); + } + } + + @Test + public void fpFrom64BitPattern() throws SolverException, InterruptedException { + for (double d : getListOfDoubles()) { + long bits = Double.doubleToRawLongBits(d); + long exponent = (bits >>> 52) & 0x7FF; + long mantissa = bits & 0xFFFFFFFFFFFFFL; + boolean sign = bits < 0; // equal to: (doubleBits >>> 63) & 1; + final FloatingPointFormula fpFromBv = + fpmgr.makeNumber( + BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, doublePrecType); + final FloatingPointFormula fp = fpmgr.makeNumber(d, doublePrecType); + assertThatFormula(fpmgr.assignment(fpFromBv, fp)).isTautological(); + } + } }