From c6efa1dbfced454d5c950c11906ff45bde62e5d8 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Sat, 23 Mar 2024 14:59:18 +0100 Subject: [PATCH 1/7] Added makeNumberImpl to api --- .../sosy_lab/java_smt/api/FloatingPointFormulaManager.java | 4 ++++ 1 file changed, 4 insertions(+) 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. * From 4a34746260f670e5fbdf56197d84af70d4b09082 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Sat, 23 Mar 2024 14:59:34 +0100 Subject: [PATCH 2/7] Added delegate and basic implementations --- .../AbstractFloatingPointFormulaManager.java | 18 ++++++++++++++++++ .../StatisticsFloatingPointFormulaManager.java | 8 ++++++++ ...ynchronizedFloatingPointFormulaManager.java | 9 +++++++++ 3 files changed, 35 insertions(+) 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) { From c68114ef6a8b059c99112e87ba7b92ec013251fd Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Sat, 23 Mar 2024 15:01:45 +0100 Subject: [PATCH 3/7] Added implementation and tests --- .../cvc4/CVC4FloatingPointFormulaManager.java | 14 +++++++++++++ .../cvc5/CVC5FloatingPointFormulaManager.java | 18 ++++++++++++++++ .../Mathsat5FloatingPointFormulaManager.java | 14 +++++++++++++ .../z3/Z3FloatingPointFormulaManager.java | 21 +++++++++++++++++++ .../test/FloatingPointFormulaManagerTest.java | 10 +++++++++ 5 files changed, 77 insertions(+) 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..87f4a4f889 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/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 { 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..7e097f9eec 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java +++ b/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, diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index f66699bf47..35157cb1d7 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; @@ -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(); + } } From b307c0731ff677d3683c19641ba9c9364809d376 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Sat, 23 Mar 2024 15:02:55 +0100 Subject: [PATCH 4/7] Fixed test --- .../z3/Z3FloatingPointFormulaManager.java | 21 ++++++++----------- .../test/FloatingPointFormulaManagerTest.java | 4 ++-- 2 files changed, 11 insertions(+), 14 deletions(-) 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 7e097f9eec..99b5654101 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java @@ -8,10 +8,8 @@ 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; @@ -75,16 +73,15 @@ protected Long makeNumberImpl(double pN, FloatingPointType pType, Long pRounding @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())); + 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); diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 35157cb1d7..4afafc859c 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -953,10 +953,10 @@ public void failOnInvalidString() { @Test public void fpFromBitPattern() throws SolverException, InterruptedException { - final FloatingPointFormula expr1 = fpmgr.makeNumber(-0.1, doublePrecType); + final FloatingPointFormula expr1 = fpmgr.makeNumber(-0.1, singlePrecType); final FloatingPointFormula expr2 = fpmgr.makeNumber( - BigInteger.valueOf(123), BigInteger.valueOf(5033165), true, doublePrecType); + BigInteger.valueOf(123), BigInteger.valueOf(5033165), true, singlePrecType); assertThatFormula(fpmgr.assignment(expr1, expr2)).isTautological(); } } From 6f5d95cde222bece15b5ca3cb148421502e184e2 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Sat, 23 Mar 2024 15:08:27 +0100 Subject: [PATCH 5/7] Added assertions to uncover potential z3 bug --- .../solvers/z3/Z3FloatingPointFormulaManager.java | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) 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 99b5654101..e0e26c0f5c 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java @@ -83,7 +83,14 @@ protected Long makeNumberImpl( Native.mkNumeral( z3context, mantissa.toString(), Native.mkBvSort(z3context, type.getMantissaSize())); - assert Native.getSort(z3context, signBv) != Native.getSort(z3context, mantBv); + 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); } From 509604b180a323e4dd53c04ab16e3eb60b5e72ed Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Sat, 23 Mar 2024 23:34:24 +0100 Subject: [PATCH 6/7] Added incRef and decRef to z3 ieee number constructor --- .../cvc4/CVC4FloatingPointFormulaManager.java | 2 +- .../z3/Z3FloatingPointFormulaManager.java | 34 +++++++++---------- 2 files changed, 17 insertions(+), 19 deletions(-) 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 87f4a4f889..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,8 +9,8 @@ package org.sosy_lab.java_smt.solvers.cvc4; import com.google.common.collect.ImmutableList; -import edu.stanford.CVC4.BitVectorExtract; 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; 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 e0e26c0f5c..14a03e3d55 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java @@ -75,24 +75,22 @@ protected Long makeNumberImpl(double pN, FloatingPointType pType, Long pRounding 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); + 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 From f682d2a046862e0d6a8d53fb7ed35373eabd9e33 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 24 Mar 2024 01:21:09 +0100 Subject: [PATCH 7/7] add more tests for new FP construction. --- .../test/FloatingPointFormulaManagerTest.java | 49 +++++++++++++++---- 1 file changed, 39 insertions(+), 10 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 4afafc859c..93e00f8836 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -777,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))); } } @@ -806,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)); } } @@ -952,11 +960,32 @@ public void failOnInvalidString() { } @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(); + 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(); + } } }