Skip to content

Commit e7a161a

Browse files
kfriedbergerkfriedberger
authored
Merge pull request #364 from leventeBajczi/ieee-literal
Add new floating point literal constructor using IEEE754 bitpattern
2 parents ce39a12 + f682d2a commit e7a161a

9 files changed

Lines changed: 151 additions & 4 deletions

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
package org.sosy_lab.java_smt.api;
1010

1111
import java.math.BigDecimal;
12+
import java.math.BigInteger;
1213
import org.sosy_lab.common.rationals.Rational;
1314
import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
1415

@@ -41,6 +42,9 @@ FloatingPointFormula makeNumber(
4142
FloatingPointFormula makeNumber(
4243
Rational n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode);
4344

45+
FloatingPointFormula makeNumber(
46+
BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type);
47+
4448
/**
4549
* Creates a variable with exactly the given name.
4650
*

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212

1313
import com.google.common.base.Preconditions;
1414
import java.math.BigDecimal;
15+
import java.math.BigInteger;
1516
import java.util.HashMap;
1617
import java.util.Map;
1718
import org.sosy_lab.common.rationals.Rational;
@@ -133,6 +134,15 @@ protected TFormulaInfo makeNumberImpl(
133134
}
134135
}
135136

137+
@Override
138+
public FloatingPointFormula makeNumber(
139+
BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) {
140+
return wrap(makeNumberImpl(exponent, mantissa, signBit, type));
141+
}
142+
143+
protected abstract TFormulaInfo makeNumberImpl(
144+
BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type);
145+
136146
protected static boolean isNegativeZero(Double pN) {
137147
Preconditions.checkNotNull(pN);
138148
return Double.valueOf("-0.0").equals(pN);
@@ -494,4 +504,12 @@ public FloatingPointFormula round(
494504

495505
protected abstract TFormulaInfo round(
496506
TFormulaInfo pFormula, FloatingPointRoundingMode pRoundingMode);
507+
508+
protected static String getBvRepresentation(BigInteger integer, int size) {
509+
char[] values = new char[size];
510+
for (int i = 0; i < size; i++) {
511+
values[size - 1 - i] = integer.testBit(i) ? '1' : '0';
512+
}
513+
return String.copyValueOf(values);
514+
}
497515
}

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@
1111
import static com.google.common.base.Preconditions.checkNotNull;
1212

1313
import java.math.BigDecimal;
14+
import java.math.BigInteger;
1415
import org.sosy_lab.common.rationals.Rational;
1516
import org.sosy_lab.java_smt.api.BitvectorFormula;
1617
import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -86,6 +87,13 @@ public FloatingPointFormula makeNumber(
8687
return delegate.makeNumber(pN, pType, pFloatingPointRoundingMode);
8788
}
8889

90+
@Override
91+
public FloatingPointFormula makeNumber(
92+
BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) {
93+
stats.fpOperations.getAndIncrement();
94+
return delegate.makeNumber(exponent, mantissa, signBit, type);
95+
}
96+
8997
@Override
9098
public FloatingPointFormula makeVariable(String pVar, FloatingPointType pType) {
9199
stats.fpOperations.getAndIncrement();

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@
1111
import static com.google.common.base.Preconditions.checkNotNull;
1212

1313
import java.math.BigDecimal;
14+
import java.math.BigInteger;
1415
import org.sosy_lab.common.rationals.Rational;
1516
import org.sosy_lab.java_smt.api.BitvectorFormula;
1617
import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -95,6 +96,14 @@ public FloatingPointFormula makeNumber(
9596
}
9697
}
9798

99+
@Override
100+
public FloatingPointFormula makeNumber(
101+
BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) {
102+
synchronized (sync) {
103+
return delegate.makeNumber(exponent, mantissa, signBit, type);
104+
}
105+
}
106+
98107
@Override
99108
public FloatingPointFormula makeVariable(String pVar, FloatingPointType pType) {
100109
synchronized (sync) {

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

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
package org.sosy_lab.java_smt.solvers.cvc4;
1010

1111
import com.google.common.collect.ImmutableList;
12+
import edu.stanford.CVC4.BitVector;
1213
import edu.stanford.CVC4.BitVectorExtract;
1314
import edu.stanford.CVC4.Expr;
1415
import edu.stanford.CVC4.ExprManager;
@@ -82,6 +83,19 @@ protected Expr makeNumberImpl(double pN, FloatingPointType pType, Expr pRounding
8283
return makeNumberImpl(Double.toString(pN), pType, pRoundingMode);
8384
}
8485

86+
@Override
87+
protected Expr makeNumberImpl(
88+
BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) {
89+
final String signStr = signBit ? "1" : "0";
90+
final String exponentStr = getBvRepresentation(exponent, type.getExponentSize());
91+
final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSize());
92+
final String bitvecStr = signStr + exponentStr + mantissaStr;
93+
final BitVector bitVector = new BitVector(bitvecStr, 2);
94+
final FloatingPoint fp =
95+
new FloatingPoint(type.getExponentSize(), type.getMantissaSize() + 1, bitVector);
96+
return exprManager.mkConst(fp);
97+
}
98+
8599
@Override
86100
protected Expr makeNumberAndRound(String pN, FloatingPointType pType, Expr pRoundingMode) {
87101
try {

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@
1717
import io.github.cvc5.Sort;
1818
import io.github.cvc5.Term;
1919
import java.math.BigDecimal;
20+
import java.math.BigInteger;
2021
import org.sosy_lab.common.rationals.Rational;
2122
import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
2223
import org.sosy_lab.java_smt.api.FormulaType;
@@ -66,6 +67,23 @@ protected Term makeNumberImpl(double pN, FloatingPointType pType, Term pRounding
6667
return makeNumberImpl(Double.toString(pN), pType, pRoundingMode);
6768
}
6869

70+
@Override
71+
protected Term makeNumberImpl(
72+
BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) {
73+
try {
74+
final String signStr = signBit ? "1" : "0";
75+
final String exponentStr = getBvRepresentation(exponent, type.getExponentSize());
76+
final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSize());
77+
final String bitvecForm = signStr + exponentStr + mantissaStr;
78+
79+
final Term bv =
80+
solver.mkBitVector(type.getExponentSize() + type.getMantissaSize() + 1, bitvecForm, 2);
81+
return solver.mkFloatingPoint(type.getExponentSize(), type.getMantissaSize() + 1, bv);
82+
} catch (CVC5ApiException e) {
83+
throw new IllegalArgumentException("You tried creating a invalid bitvector", e);
84+
}
85+
}
86+
6987
@Override
7088
protected Term makeNumberAndRound(String pN, FloatingPointType pType, Term pRoundingMode) {
7189
try {

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

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010

1111
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_equal;
1212
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_abs;
13+
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_bits_number;
1314
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_cast;
1415
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_div;
1516
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_equal;
@@ -45,6 +46,7 @@
4546
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_get_type;
4647

4748
import com.google.common.collect.ImmutableList;
49+
import java.math.BigInteger;
4850
import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
4951
import org.sosy_lab.java_smt.api.FormulaType;
5052
import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
@@ -94,6 +96,18 @@ protected Long makeNumberImpl(double pN, FloatingPointType pType, Long pRounding
9496
return makeNumberImpl(Double.toString(pN), pType, pRoundingMode);
9597
}
9698

99+
@Override
100+
protected Long makeNumberImpl(
101+
BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) {
102+
final String signStr = signBit ? "1" : "0";
103+
final String exponentStr = getBvRepresentation(exponent, type.getExponentSize());
104+
final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSize());
105+
final String bitvecForm = signStr + exponentStr + mantissaStr;
106+
final BigInteger bitvecValue = new BigInteger(bitvecForm, 2);
107+
return msat_make_fp_bits_number(
108+
mathsatEnv, bitvecValue.toString(), type.getExponentSize(), type.getMantissaSize());
109+
}
110+
97111
@Override
98112
protected Long makeNumberAndRound(String pN, FloatingPointType pType, Long pRoundingMode) {
99113
try {

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

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010

1111
import com.google.common.collect.ImmutableList;
1212
import com.microsoft.z3.Native;
13+
import java.math.BigInteger;
1314
import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
1415
import org.sosy_lab.java_smt.api.FormulaType;
1516
import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
@@ -70,6 +71,28 @@ protected Long makeNumberImpl(double pN, FloatingPointType pType, Long pRounding
7071
return makeNumberImpl(Double.toString(pN), pType, pRoundingMode);
7172
}
7273

74+
@Override
75+
protected Long makeNumberImpl(
76+
BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) {
77+
78+
final Long signSort = getFormulaCreator().getBitvectorType(1);
79+
final Long expoSort = getFormulaCreator().getBitvectorType(type.getExponentSize());
80+
final Long mantSort = getFormulaCreator().getBitvectorType(type.getMantissaSize());
81+
82+
final Long signBv = Native.mkNumeral(z3context, signBit ? "1" : "0", signSort);
83+
Native.incRef(z3context, signBv);
84+
final Long expoBv = Native.mkNumeral(z3context, exponent.toString(), expoSort);
85+
Native.incRef(z3context, expoBv);
86+
final Long mantBv = Native.mkNumeral(z3context, mantissa.toString(), mantSort);
87+
Native.incRef(z3context, mantBv);
88+
89+
final Long fp = Native.mkFpaFp(z3context, signBv, expoBv, mantBv);
90+
Native.decRef(z3context, mantBv);
91+
Native.decRef(z3context, expoBv);
92+
Native.decRef(z3context, signBv);
93+
return fp;
94+
}
95+
7396
@Override
7497
protected Long makeNumberAndRound(String pN, FloatingPointType pType, Long pRoundingMode) {
7598
// Z3 does not allow specifying a rounding mode for numerals,

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

Lines changed: 43 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@
1818
import com.google.common.collect.ImmutableSet;
1919
import com.google.common.collect.Lists;
2020
import java.math.BigDecimal;
21+
import java.math.BigInteger;
2122
import java.util.List;
2223
import java.util.Random;
2324
import org.junit.Before;
@@ -830,12 +831,16 @@ private List<Float> getListOfFloats() {
830831
Float.MAX_VALUE,
831832
Float.POSITIVE_INFINITY,
832833
Float.NEGATIVE_INFINITY,
833-
0.0f // , -0.0f // MathSat5 fails for NEGATIVE_ZERO
834-
);
834+
0.0f, // , -0.0f // MathSat5 fails for NEGATIVE_ZERO
835+
1f,
836+
-1f,
837+
2f,
838+
-2f);
835839

836840
for (int i = 1; i < 20; i++) {
837841
for (int j = 1; j < 20; j++) {
838842
flts.add((float) (i * Math.pow(10, j)));
843+
flts.add((float) (-i * Math.pow(10, j)));
839844
}
840845
}
841846

@@ -859,12 +864,16 @@ private List<Double> getListOfDoubles() {
859864
Double.MAX_VALUE,
860865
Double.POSITIVE_INFINITY,
861866
Double.NEGATIVE_INFINITY,
862-
0.0 // , -0.0 // MathSat5 fails for NEGATIVE_ZERO
863-
);
867+
0.0, // , -0.0 // MathSat5 fails for NEGATIVE_ZERO
868+
1d,
869+
-1d,
870+
2d,
871+
-2d);
864872

865873
for (int i = 1; i < 20; i++) {
866874
for (int j = 1; j < 20; j++) {
867875
dbls.add(i * Math.pow(10, j));
876+
dbls.add(-i * Math.pow(10, j));
868877
}
869878
}
870879

@@ -1003,4 +1012,34 @@ public void failOnInvalidString() {
10031012
fpmgr.makeNumber("a", singlePrecType);
10041013
assert_().fail();
10051014
}
1015+
1016+
@Test
1017+
public void fpFrom32BitPattern() throws SolverException, InterruptedException {
1018+
for (float f : getListOfFloats()) {
1019+
int bits = Float.floatToRawIntBits(f);
1020+
int exponent = (bits >>> 23) & 0xFF;
1021+
int mantissa = bits & 0x7FFFFF;
1022+
boolean sign = bits < 0; // equal to: (bits >>> 31) & 0x1
1023+
final FloatingPointFormula fpFromBv =
1024+
fpmgr.makeNumber(
1025+
BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, singlePrecType);
1026+
final FloatingPointFormula fp = fpmgr.makeNumber(f, singlePrecType);
1027+
assertThatFormula(fpmgr.assignment(fpFromBv, fp)).isTautological();
1028+
}
1029+
}
1030+
1031+
@Test
1032+
public void fpFrom64BitPattern() throws SolverException, InterruptedException {
1033+
for (double d : getListOfDoubles()) {
1034+
long bits = Double.doubleToRawLongBits(d);
1035+
long exponent = (bits >>> 52) & 0x7FF;
1036+
long mantissa = bits & 0xFFFFFFFFFFFFFL;
1037+
boolean sign = bits < 0; // equal to: (doubleBits >>> 63) & 1;
1038+
final FloatingPointFormula fpFromBv =
1039+
fpmgr.makeNumber(
1040+
BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, doublePrecType);
1041+
final FloatingPointFormula fp = fpmgr.makeNumber(d, doublePrecType);
1042+
assertThatFormula(fpmgr.assignment(fpFromBv, fp)).isTautological();
1043+
}
1044+
}
10061045
}

0 commit comments

Comments
 (0)