From f99f39c527af8fff5a915cb0bd41fb5f5d821d0d Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 17:21:58 +0200 Subject: [PATCH 01/67] Add native Mathsat test for mantissa not including the sign bit with BV transformation and width comparison --- .../Mathsat5AbstractNativeApiTest.java | 39 +++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java index bd277cf91a..129b2669a8 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java @@ -35,6 +35,7 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_repr; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_to_smtlib2_ext; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_to_smtlib2_term; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_type_equals; import org.junit.After; import org.junit.Ignore; @@ -79,6 +80,44 @@ public void fpMantWidth() { assertThat(msat_get_fp_type_mant_width(env, type)).isEqualTo(23); } + /* + * MathSAT5, compared to all other solvers and the standard, does not expect the sign bit to be + * included in the mantissa! + */ + @Test + public void fpMantissaDoesNotIncludeSignBit() { + int totalBVSize = 32; + long bvNumber = msat_make_bv_number(env, "42", totalBVSize, 10); + long bvType = msat_term_get_type(bvNumber); + assertThat(msat_get_bv_type_size(env, bvType)).isEqualTo(totalBVSize); + assertThat(msat_get_bv_type_size(env, msat_term_get_type(bvNumber))).isEqualTo(totalBVSize); + + int exponent = 8; + int mantissaWithoutSign = 23; // excluding sign bit + long fpSinglePrecType = msat_get_fp_type(env, exponent, mantissaWithoutSign); + assertThat(msat_get_fp_type_mant_width(env, fpSinglePrecType)).isEqualTo(mantissaWithoutSign); + assertThat(msat_get_fp_type_exp_width(env, fpSinglePrecType)).isEqualTo(exponent); + // total size is exp + man + 1 + assertThat( + msat_get_fp_type_mant_width(env, fpSinglePrecType) + + msat_get_fp_type_exp_width(env, fpSinglePrecType) + + 1) + .isEqualTo(totalBVSize); + + long bvToFpSinglePrec = + Mathsat5NativeApi.msat_make_fp_from_ieeebv(env, exponent, mantissaWithoutSign, bvNumber); + assertThat(msat_type_equals(msat_term_get_type(bvToFpSinglePrec), fpSinglePrecType)).isTrue(); + assertThat(msat_get_fp_type_mant_width(env, msat_term_get_type(bvToFpSinglePrec))) + .isEqualTo(mantissaWithoutSign); + assertThat(msat_get_fp_type_exp_width(env, msat_term_get_type(bvToFpSinglePrec))) + .isEqualTo(exponent); + + long bvToFpSinglePrecToBv = Mathsat5NativeApi.msat_make_fp_as_ieeebv(env, bvToFpSinglePrec); + assertThat(msat_type_equals(msat_term_get_type(bvToFpSinglePrecToBv), bvType)).isTrue(); + assertThat(msat_get_bv_type_size(env, msat_term_get_type(bvToFpSinglePrecToBv))) + .isEqualTo(totalBVSize); + } + @Test public void fpExpWidthIllegal() { long type = msat_get_integer_type(env); From 737718c51f6c516386580cb5c1ad97495a6780f6 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 18:12:09 +0200 Subject: [PATCH 02/67] Add note about mantissa und sign bit in FloatingPointNumber.java --- src/org/sosy_lab/java_smt/api/FloatingPointNumber.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index fe3c14b1ca..a9b2513aad 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -23,6 +23,7 @@ @AutoValue public abstract class FloatingPointNumber { + // Mantissas do not include the sign bit public static final int SINGLE_PRECISION_EXPONENT_SIZE = 8; public static final int SINGLE_PRECISION_MANTISSA_SIZE = 23; public static final int DOUBLE_PRECISION_EXPONENT_SIZE = 11; From d50ad4c825cefba8fa05292c2244798e0c4b42a7 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:37:43 +0200 Subject: [PATCH 03/67] Add JavaDoc to FormulaType.FloatingPointType and add methods to get the type/mantissa with/without sign bit and add sign bit to toString and toSMTLIBString representations --- .../sosy_lab/java_smt/api/FormulaType.java | 86 +++++++++++++++++-- 1 file changed, 80 insertions(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index d5beea79cc..a6a705a8f6 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -205,14 +205,61 @@ public String toSMTLIBString() { } } - public static FloatingPointType getFloatingPointType(int exponentSize, int mantissaSize) { - return new FloatingPointType(exponentSize, mantissaSize); + /** + * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes. + * The mantissa size is expected to not include the sign bit. + * + * @param exponentSize size of the exponent for the base of the floating-point + * @param mantissaSizeWithoutSignBit size of the mantissa (also called a coefficient or + * significant), excluding the sign bit. + * @return the newly constructed {@link FloatingPointType}. + */ + // TODO: mark as soon to be deprecated + public static FloatingPointType getFloatingPointType( + int exponentSize, int mantissaSizeWithoutSignBit) { + return new FloatingPointType(exponentSize, mantissaSizeWithoutSignBit); + } + + /** + * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes. + * The mantissa size is expected to not include the sign bit. + * + * @param exponentSize size of the exponent for the base of the floating-point + * @param mantissaSizeWithoutSignBit size of the mantissa (also called a coefficient or + * significant), excluding the sign bit. + * @return the newly constructed {@link FloatingPointType}. + */ + public static FloatingPointType getFloatingPointTypeWithoutSignBit( + int exponentSize, int mantissaSizeWithoutSignBit) { + return new FloatingPointType(exponentSize, mantissaSizeWithoutSignBit); + } + + /** + * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes. + * The mantissa size is expected to not include the sign bit. + * + * @param exponentSize size of the exponent for the base of the floating-point + * @param mantissaSizeWithSignBit size of the mantissa (also called a coefficient or significant), + * including the sign bit. + * @return the newly constructed {@link FloatingPointType}. + */ + public static FloatingPointType getFloatingPointTypeWithSignBit( + int exponentSize, int mantissaSizeWithSignBit) { + return new FloatingPointType(exponentSize, mantissaSizeWithSignBit); } + /** + * @return single precision {@link FloatingPointType} with exponent sized 8, and mantissa sized 24 + * (including the sign bit). + */ public static FloatingPointType getSinglePrecisionFloatingPointType() { return FloatingPointType.SINGLE_PRECISION_FP_TYPE; } + /** + * @return double precision {@link FloatingPointType} with exponent sized 11, and mantissa sized + * 53 (including the sign bit). + */ public static FloatingPointType getDoublePrecisionFloatingPointType() { return FloatingPointType.DOUBLE_PRECISION_FP_TYPE; } @@ -226,6 +273,8 @@ public static final class FloatingPointType extends FormulaType"; + return "FloatingPoint"; } @Override public String toSMTLIBString() { - return "(_ FloatingPoint " + exponentSize + " " + mantissaSize + ")"; + return "(_ FloatingPoint " + exponentSize + " " + getMantissaSizeWithSignBit() + ")"; } } @@ -478,7 +552,7 @@ public static FormulaType fromString(String t) { } else if (t.startsWith("FloatingPoint<")) { // FloatingPoint List exman = Splitter.on(',').limit(2).splitToList(t.substring(14, t.length() - 1)); - return FormulaType.getFloatingPointType( + return FormulaType.getFloatingPointTypeWithoutSignBit( Integer.parseInt(exman.get(0).substring(4)), Integer.parseInt(exman.get(1).substring(5))); } else if (t.startsWith("Bitvector<")) { // Bitvector<32> From a4240e696684deac32584475038d2c663fa8287a Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:39:27 +0200 Subject: [PATCH 04/67] Add JavaDoc to FloatingPointNumber and add methods to get the mantissa with/without sign bit and use those as far as possible to make the code unambiguous for mantissas --- .../java_smt/api/FloatingPointNumber.java | 49 ++++++++++++++----- 1 file changed, 36 insertions(+), 13 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index a9b2513aad..6c750e3701 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -81,8 +81,29 @@ public final boolean getSign() { public abstract int getExponentSize(); + /** + * Returns the size of the mantissa (also called a coefficient or significant), excluding the sign + * bit. + */ + // TODO: mark as soon to be deprecated public abstract int getMantissaSize(); + /** + * Returns the size of the mantissa (also called a coefficient or significant), excluding the sign + * bit. + */ + public int getMantissaSizeWithoutSignBit() { + return getMantissaSize(); + } + + /** + * Returns the size of the mantissa (also called a coefficient or significant), including the sign + * bit. + */ + public int getMantissaSizeWithSignBit() { + return getMantissaSize() + 1; + } + /** * Get a floating-point number with the given sign, exponent, and mantissa. * @@ -93,7 +114,7 @@ public final boolean getSign() { * @param mantissa the mantissa of the floating-point number, given as unsigned (not negative) * number without hidden bit * @param exponentSize the (maximum) size of the exponent in bits - * @param mantissaSize the (maximum) size of the mantissa in bits + * @param mantissaSize the (maximum) size of the mantissa in bits (excluding the sign bit) * @see #of(Sign, BigInteger, BigInteger, int, int) */ @Deprecated( @@ -120,7 +141,7 @@ public static FloatingPointNumber of( * @param mantissa the mantissa of the floating-point number, given as unsigned (not negative) * number without hidden bit * @param exponentSize the (maximum) size of the exponent in bits - * @param mantissaSize the (maximum) size of the mantissa in bits + * @param mantissaSize the (maximum) size of the mantissa in bits (excluding the sign bit) */ public static FloatingPointNumber of( Sign sign, BigInteger exponent, BigInteger mantissa, int exponentSize, int mantissaSize) { @@ -137,7 +158,7 @@ public static FloatingPointNumber of( * @param bits the bit-representation of the floating-point number, consisting of sign bit, * exponent (without bias) and mantissa (without hidden bit) in this exact ordering * @param exponentSize the size of the exponent in bits - * @param mantissaSize the size of the mantissa in bits + * @param mantissaSize the size of the mantissa in bits (excluding the sign bit) */ public static FloatingPointNumber of(String bits, int exponentSize, int mantissaSize) { Preconditions.checkArgument(0 < exponentSize); @@ -160,24 +181,26 @@ public static FloatingPointNumber of(String bits, int exponentSize, int mantissa /** * Returns true if this floating-point number is an IEEE-754-2008 single precision type with 32 - * bits length consisting of an 8 bit exponent, a 23 bit mantissa and a single sign bit. + * bits length consisting of an 8 bit exponent, a 24 bit mantissa (including the sign bit). * * @return true for IEEE-754 single precision type, false otherwise. */ public boolean isIEEE754SinglePrecision() { + // Mantissa does not include the sign bit return getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE - && getMantissaSize() == SINGLE_PRECISION_MANTISSA_SIZE; + && getMantissaSizeWithoutSignBit() == SINGLE_PRECISION_MANTISSA_SIZE; } /** * Returns true if this floating-point number is an IEEE-754-2008 double precision type with 64 - * bits length consisting of an 11 bit exponent, a 52 bit mantissa and a single sign bit. + * bits length consisting of an 11 bit exponent, a 53 bit mantissa (including the sign bit). * * @return true for IEEE-754 double precision type, false otherwise. */ public boolean isIEEE754DoublePrecision() { + // Mantissa does not include the sign bit return getExponentSize() == DOUBLE_PRECISION_EXPONENT_SIZE - && getMantissaSize() == DOUBLE_PRECISION_MANTISSA_SIZE; + && getMantissaSizeWithoutSignBit() == DOUBLE_PRECISION_MANTISSA_SIZE; } /** compute a representation as Java-based float value, if possible. */ @@ -205,18 +228,18 @@ public double doubleValue() { } private BitSet getBits() { - var mantissaSize = getMantissaSize(); + var mantissaSizeWithoutSign = getMantissaSizeWithoutSignBit(); var exponentSize = getExponentSize(); var mantissa = getMantissa(); var exponent = getExponent(); - var bits = new BitSet(1 + exponentSize + mantissaSize); + var bits = new BitSet(exponentSize + mantissaSizeWithoutSign + 1); if (getMathSign().isNegative()) { - bits.set(exponentSize + mantissaSize); // if negative, set first bit to 1 + bits.set(exponentSize + mantissaSizeWithoutSign); // if negative, set first bit to 1 } for (int i = 0; i < exponentSize; i++) { - bits.set(mantissaSize + i, exponent.testBit(i)); + bits.set(mantissaSizeWithoutSign + i, exponent.testBit(i)); } - for (int i = 0; i < mantissaSize; i++) { + for (int i = 0; i < mantissaSizeWithoutSign; i++) { bits.set(i, mantissa.testBit(i)); } return bits; @@ -228,7 +251,7 @@ private BitSet getBits() { */ @Override public final String toString() { - var length = 1 + getExponentSize() + getMantissaSize(); + var length = getExponentSize() + getMantissaSizeWithSignBit(); var str = new StringBuilder(length); var bits = getBits(); for (int i = 0; i < length; i++) { From c452a8fdc7ffe79402ac419cc176a882042b6183 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:41:07 +0200 Subject: [PATCH 05/67] Extend FP tests with new mantissa API to be unambiguous about the sign bit and add some assertions for mantissa/exponent --- .../test/FloatingPointFormulaManagerTest.java | 253 ++++++++++++++++-- .../IndependentInterpolatingProverTest.java | 13 + 2 files changed, 248 insertions(+), 18 deletions(-) create mode 100644 src/org/sosy_lab/java_smt/test/IndependentInterpolatingProverTest.java diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 74390241cf..48e334b32c 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -75,7 +75,7 @@ public void init() { @Test public void floatingPointType() { - FloatingPointType type = FormulaType.getFloatingPointType(23, 42); + FloatingPointType type = FormulaType.getFloatingPointTypeWithoutSignBit(23, 42); FloatingPointFormula var = fpmgr.makeVariable("x", type); FloatingPointType result = (FloatingPointType) mgr.getFormulaType(var); @@ -83,8 +83,8 @@ public void floatingPointType() { .that(result.getExponentSize()) .isEqualTo(type.getExponentSize()); assertWithMessage("mantissa size") - .that(result.getMantissaSize()) - .isEqualTo(type.getMantissaSize()); + .that(result.getMantissaSizeWithSignBit()) + .isEqualTo(type.getMantissaSizeWithSignBit()); } @Test @@ -258,7 +258,7 @@ public void fpRemainderNormal() throws SolverException, InterruptedException { for (FloatingPointType prec : new FloatingPointType[] { - singlePrecType, doublePrecType, FormulaType.getFloatingPointType(5, 6), + singlePrecType, doublePrecType, FormulaType.getFloatingPointTypeWithoutSignBit(5, 6), }) { final FloatingPointFormula numFive = fpmgr.makeNumber(5, prec); @@ -282,7 +282,7 @@ public void fpRemainderSpecial() throws SolverException, InterruptedException { for (FloatingPointType prec : new FloatingPointType[] { - singlePrecType, doublePrecType, FormulaType.getFloatingPointType(5, 6), + singlePrecType, doublePrecType, FormulaType.getFloatingPointTypeWithoutSignBit(5, 6), }) { final FloatingPointFormula num = fpmgr.makeNumber(42, prec); @@ -499,6 +499,192 @@ public void specialValueFunctionsFrom64Bits2() throws SolverException, Interrupt bmgr.and(bmgr.not(fpmgr.isNaN(x)), bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1)))); } + // Same as specialValueFunctionsFrom32Bits2, but with fallback toIeeeBitvector() implementation. + @Test + public void specialValueFunctionsFrom32Bits2ToIeeeFallback() + throws SolverException, InterruptedException { + requireBitvectors(); + + final FloatingPointFormula x = fpmgr.makeVariable("x32", singlePrecType); + BitvectorFormulaAndBooleanFormula xToIeeeAndAddConstraint = + fpmgr.toIeeeBitvector(x, "bvConst_x"); + BitvectorFormula xToIeee = xToIeeeAndAddConstraint.getBitvectorFormula(); + final BitvectorFormula signBit = bvmgr.extract(xToIeee, 31, 31); + final BitvectorFormula exponent = bvmgr.extract(xToIeee, 30, 23); + final BitvectorFormula mantissa = bvmgr.extract(xToIeee, 22, 0); + final BooleanFormula additionalConstraint = xToIeeeAndAddConstraint.getBooleanFormula(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isInfinity(x), + bmgr.or( + bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x7f80_0000L)), + bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0xff80_0000L)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isZero(x), + bmgr.or( + bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x0000_0000)), + bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x8000_0000L)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isNormal(x), + bmgr.and( + bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0))), + bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1))))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isSubnormal(x), + bmgr.and( + bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0)), + bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0))))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isNaN(x), + bmgr.and( + bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1)), + bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0))))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isNegative(x), + bmgr.and( + bmgr.not(fpmgr.isNaN(x)), + bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1)))))) + .isTautological(); + } + + // Same as specialValueFunctionsFrom64Bits2, but with fallback toIeeeBitvector() implementation. + @Test + public void specialValueFunctionsFrom64Bits2ToIeeeFallback() + throws SolverException, InterruptedException { + requireBitvectors(); + + final FloatingPointFormula x = fpmgr.makeVariable("x64", doublePrecType); + BitvectorFormulaAndBooleanFormula xToIeeeAndAddConstraint = + fpmgr.toIeeeBitvector(x, "bvConst_x"); + BitvectorFormula xToIeee = xToIeeeAndAddConstraint.getBitvectorFormula(); + final BitvectorFormula signBit = bvmgr.extract(xToIeee, 63, 63); + final BitvectorFormula exponent = bvmgr.extract(xToIeee, 62, 52); + final BitvectorFormula mantissa = bvmgr.extract(xToIeee, 51, 0); + final BooleanFormula additionalConstraint = xToIeeeAndAddConstraint.getBooleanFormula(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isInfinity(x), + bmgr.or( + bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x7ff0_0000_0000_0000L)), + bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0xfff0_0000_0000_0000L)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isZero(x), + bmgr.or( + bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x0000_0000_0000_0000L)), + bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x8000_0000_0000_0000L)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isNormal(x), + bmgr.and( + bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0))), + bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, -1))))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isSubnormal(x), + bmgr.and( + bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0)), + bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(52, 0))))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isNaN(x), + bmgr.and( + bvmgr.equal(exponent, bvmgr.makeBitvector(11, -1)), + bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(52, 0))))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isNegative(x), + bmgr.and( + bmgr.not(fpmgr.isNaN(x)), + bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1)))))) + .isTautological(); + } + + @Test + public void floatingPointSinglePrecisionSizeWithBvTransformationTest() { + requireBitvectors(); + int fpSinglePrecSize = 32; + var bv32 = bvmgr.makeBitvector(fpSinglePrecSize, 0); + assertThat(bvmgr.getLength(bv32)).isEqualTo(fpSinglePrecSize); + + requireFloats(); + var singlePrec = FormulaType.getSinglePrecisionFloatingPointType(); + var fpSinglePrec = fpmgr.makeNumber(0.0, singlePrec); + // Sizes of the type and the actual term should match + assertThat(fpmgr.getExponentSize(fpSinglePrec)).isEqualTo(8); + assertThat(fpmgr.getMantissaSizeWithSignBit(fpSinglePrec)).isEqualTo(24); + assertThat(singlePrec.getExponentSize()).isEqualTo(8); + assertThat(singlePrec.getMantissaSizeWithSignBit()).isEqualTo(24); + assertThat(singlePrec.getExponentSize() + singlePrec.getMantissaSizeWithSignBit()) + .isEqualTo(fpSinglePrecSize); + assertThat(singlePrec.getTotalSize()) + .isEqualTo(singlePrec.getExponentSize() + singlePrec.getMantissaSizeWithSignBit()); + + assertThat(bvmgr.getLength(fpmgr.toIeeeBitvector(fpSinglePrec, "dummy1").getBitvectorFormula())) + .isEqualTo(fpSinglePrecSize); + assertThat( + bvmgr.getLength( + fpmgr + .toIeeeBitvector(fpSinglePrec, "dummy2", ImmutableMap.of()) + .getBitvectorFormula())) + .isEqualTo(fpSinglePrecSize); + + if (solverSupportsNativeFPToBitvector()) { + assertThat(bvmgr.getLength(fpmgr.toIeeeBitvector(fpSinglePrec))).isEqualTo(fpSinglePrecSize); + } + } + @Test public void specialDoubles() throws SolverException, InterruptedException { assertThatFormula(fpmgr.assignment(fpmgr.makeNumber(Double.NaN, singlePrecType), nan)) @@ -536,7 +722,7 @@ public void numberConstants() throws SolverException, InterruptedException { checkEqualityOfNumberConstantsFor(3.4028234663852886e+38, doublePrecType); // check unequality for large types - FloatingPointType nearDouble = FormulaType.getFloatingPointType(12, 52); + FloatingPointType nearDouble = FormulaType.getFloatingPointTypeWithoutSignBit(12, 52); FloatingPointFormula h1 = fpmgr.makeNumber(BigDecimal.TEN.pow(309).multiply(BigDecimal.valueOf(1.0001)), nearDouble); FloatingPointFormula h2 = @@ -544,7 +730,7 @@ public void numberConstants() throws SolverException, InterruptedException { assertThatFormula(fpmgr.equalWithFPSemantics(h1, h2)).isUnsatisfiable(); // check equality for short types - FloatingPointType smallType = FormulaType.getFloatingPointType(4, 4); + FloatingPointType smallType = FormulaType.getFloatingPointTypeWithoutSignBit(4, 4); FloatingPointFormula i1 = fpmgr.makeNumber(BigDecimal.TEN.pow(50).multiply(BigDecimal.valueOf(1.001)), smallType); FloatingPointFormula i2 = @@ -573,7 +759,7 @@ public void numberConstants() throws SolverException, InterruptedException { assertThatFormula(fpmgr.isNegative(ni2)).isTautological(); // check equality for short types - FloatingPointType smallType2 = FormulaType.getFloatingPointType(4, 4); + FloatingPointType smallType2 = FormulaType.getFloatingPointTypeWithoutSignBit(4, 4); FloatingPointFormula j1 = fpmgr.makeNumber(BigDecimal.TEN.pow(500).multiply(BigDecimal.valueOf(1.001)), smallType2); FloatingPointFormula j2 = @@ -604,7 +790,7 @@ public void numberConstants() throws SolverException, InterruptedException { // Z3 supports at least FloatingPointType(15, 112). Larger types seem to be rounded. if (!ImmutableSet.of(Solvers.Z3, Solvers.CVC4).contains(solver)) { // check unequality for very large types - FloatingPointType largeType = FormulaType.getFloatingPointType(100, 100); + FloatingPointType largeType = FormulaType.getFloatingPointTypeWithoutSignBit(100, 100); FloatingPointFormula k1 = fpmgr.makeNumber(BigDecimal.TEN.pow(200).multiply(BigDecimal.valueOf(1.001)), largeType); FloatingPointFormula k2 = @@ -641,7 +827,7 @@ public void numberConstantsNearInf() throws SolverException, InterruptedExceptio private void checkNearInf(int mantissa, int exponent, long value) throws SolverException, InterruptedException { - FloatingPointType type = FormulaType.getFloatingPointType(exponent, mantissa); + FloatingPointType type = FormulaType.getFloatingPointTypeWithoutSignBit(exponent, mantissa); FloatingPointFormula fp1 = fpmgr.makeNumber(BigDecimal.valueOf(value), type); assertThatFormula(fpmgr.isInfinity(fp1)).isTautological(); FloatingPointFormula fp2 = fpmgr.makeNumber(BigDecimal.valueOf(value - 1), type); @@ -676,7 +862,7 @@ public void numberConstantsNearMinusInf() throws SolverException, InterruptedExc private void checkNearMinusInf(int mantissa, int exponent, long value) throws SolverException, InterruptedException { - FloatingPointType type = FormulaType.getFloatingPointType(exponent, mantissa); + FloatingPointType type = FormulaType.getFloatingPointTypeWithoutSignBit(exponent, mantissa); FloatingPointFormula fp1 = fpmgr.makeNumber(BigDecimal.valueOf(value), type); assertThatFormula(fpmgr.isInfinity(fp1)).isTautological(); FloatingPointFormula fp2 = fpmgr.makeNumber(BigDecimal.valueOf(value + 1), type); @@ -1215,9 +1401,16 @@ public void fpModelValue() throws SolverException, InterruptedException { Float.MIN_VALUE, Float.MIN_NORMAL, }) { - FloatingPointNumber fiveValue = model.evaluate(fpmgr.makeNumber(f, singlePrecType)); - assertThat(fiveValue.floatValue()).isEqualTo(f); - assertThat(fiveValue.doubleValue()).isEqualTo((double) f); + var constFpNum = fpmgr.makeNumber(f, singlePrecType); + assertThat(fpmgr.getMantissaSizeWithSignBit(constFpNum)) + .isEqualTo(singlePrecType.getMantissaSizeWithSignBit()); + FloatingPointNumber fpValue = model.evaluate(constFpNum); + assertThat(fpValue.getMantissaSizeWithSignBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithSignBit()); + assertThat(fpValue.getMantissaSizeWithoutSignBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithSignBit() - 1); + assertThat(fpValue.floatValue()).isEqualTo(f); + assertThat(fpValue.doubleValue()).isEqualTo((double) f); } } } @@ -1266,16 +1459,28 @@ public void fpFrom32BitPattern() throws SolverException, InterruptedException { final FloatingPointFormula fpFromBv = fpmgr.makeNumber( BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, singlePrecType); + assertThat(fpmgr.getMantissaSizeWithSignBit(fpFromBv) + fpmgr.getExponentSize(fpFromBv)) + .isEqualTo(singlePrecType.getTotalSize()); final FloatingPointNumber fpNumber = FloatingPointNumber.of( sign, BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), singlePrecType.getExponentSize(), - singlePrecType.getMantissaSize()); + singlePrecType.getMantissaSizeWithoutSignBit()); + assertThat(fpNumber.getMantissaSizeWithSignBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithSignBit()); + assertThat(fpNumber.getMantissaSizeWithoutSignBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithSignBit() - 1); final FloatingPointFormula fp1 = fpmgr.makeNumber(fpNumber); + assertThat(fpmgr.getMantissaSizeWithSignBit(fp1) + fpmgr.getExponentSize(fp1)) + .isEqualTo(singlePrecType.getTotalSize()); final FloatingPointFormula fp2 = fpmgr.makeNumber(pFloat, singlePrecType); - return bmgr.and(fpmgr.assignment(fpFromBv, fp1), fpmgr.assignment(fpFromBv, fp2)); + assertThat(fpmgr.getMantissaSizeWithSignBit(fp2) + fpmgr.getExponentSize(fp2)) + .isEqualTo(singlePrecType.getTotalSize()); + final BooleanFormula assignment1 = fpmgr.assignment(fpFromBv, fp1); + final BooleanFormula assignment2 = fpmgr.assignment(fpFromBv, fp2); + return bmgr.and(assignment1, assignment2); }); } @@ -1292,16 +1497,28 @@ public void fpFrom64BitPattern() throws SolverException, InterruptedException { final FloatingPointFormula fpFromBv = fpmgr.makeNumber( BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, doublePrecType); + assertThat(fpmgr.getMantissaSizeWithSignBit(fpFromBv) + fpmgr.getExponentSize(fpFromBv)) + .isEqualTo(doublePrecType.getTotalSize()); final FloatingPointNumber fpNumber = FloatingPointNumber.of( sign, BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), doublePrecType.getExponentSize(), - doublePrecType.getMantissaSize()); + doublePrecType.getMantissaSizeWithoutSignBit()); + assertThat(fpNumber.getMantissaSizeWithSignBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithSignBit()); + assertThat(fpNumber.getMantissaSizeWithoutSignBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithSignBit() - 1); final FloatingPointFormula fp1 = fpmgr.makeNumber(fpNumber); + assertThat(fpmgr.getMantissaSizeWithSignBit(fp1) + fpmgr.getExponentSize(fp1)) + .isEqualTo(doublePrecType.getTotalSize()); final FloatingPointFormula fp2 = fpmgr.makeNumber(pDouble, doublePrecType); - return bmgr.and(fpmgr.assignment(fpFromBv, fp1), fpmgr.assignment(fpFromBv, fp2)); + assertThat(fpmgr.getMantissaSizeWithSignBit(fp2) + fpmgr.getExponentSize(fp2)) + .isEqualTo(doublePrecType.getTotalSize()); + final BooleanFormula assignment1 = fpmgr.assignment(fpFromBv, fp1); + final BooleanFormula assignment2 = fpmgr.assignment(fpFromBv, fp2); + return bmgr.and(assignment1, assignment2); }); } diff --git a/src/org/sosy_lab/java_smt/test/IndependentInterpolatingProverTest.java b/src/org/sosy_lab/java_smt/test/IndependentInterpolatingProverTest.java new file mode 100644 index 0000000000..b57c9e79c0 --- /dev/null +++ b/src/org/sosy_lab/java_smt/test/IndependentInterpolatingProverTest.java @@ -0,0 +1,13 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.test; + +public class IndependentInterpolatingProverTest extends InterpolatingProverTest {} From a6f92b7cd0c7d3f190ca0fb3c2c3c0162c912403 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:43:00 +0200 Subject: [PATCH 06/67] Update Bitwuzla with new unambiguous FP mantissa size getters --- .../solvers/bitwuzla/BitwuzlaFloatingPointManager.java | 10 +++++----- .../solvers/bitwuzla/BitwuzlaFormulaCreator.java | 6 +++--- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java index b301db4521..9746c1c151 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java @@ -94,7 +94,7 @@ protected Term makeNumberImpl( Sort expSort = termManager.mk_bv_sort(type.getExponentSize()); Term expTerm = termManager.mk_bv_value(expSort, exponent.toString(2)); - Sort mantissaSort = termManager.mk_bv_sort(type.getMantissaSize()); + Sort mantissaSort = termManager.mk_bv_sort(type.getMantissaSizeWithoutSignBit()); Term mantissaTerm = termManager.mk_bv_value(mantissaSort, mantissa.toString(2)); return termManager.mk_fp_value(signTerm, expTerm, mantissaTerm); @@ -144,7 +144,7 @@ protected Term castToImpl( pRoundingMode, pNumber, targetType.getExponentSize(), - targetType.getMantissaSize() + 1); + targetType.getMantissaSizeWithSignBit()); } else if (pTargetType.isBitvectorType()) { FormulaType.BitvectorType targetType = (FormulaType.BitvectorType) pTargetType; if (pSigned) { @@ -171,14 +171,14 @@ protected Term castFromImpl( roundingMode, pNumber, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithSignBit()); } else { return termManager.mk_term( Kind.FP_TO_FP_FROM_UBV, roundingMode, pNumber, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithSignBit()); } } else { @@ -193,7 +193,7 @@ protected Term fromIeeeBitvectorImpl(Term pNumber, FloatingPointType pTargetType Kind.FP_TO_FP_FROM_BV, pNumber, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithSignBit()); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index f946331319..fd5c82d284 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -102,7 +102,7 @@ assert getFormulaType(pTerm).isBitvectorType() // system instead use bitwuzla_mk_fp_value_from_real somehow or convert myself @Override public Sort getFloatingPointType(FloatingPointType type) { - return termManager.mk_fp_sort(type.getExponentSize(), type.getMantissaSize() + 1); + return termManager.mk_fp_sort(type.getExponentSize(), type.getMantissaSizeWithSignBit()); } @Override @@ -171,7 +171,7 @@ public FormulaType bitwuzlaSortToType(Sort pSort) { if (pSort.is_fp()) { int exponent = pSort.fp_exp_size(); int mantissa = pSort.fp_sig_size() - 1; - return FormulaType.getFloatingPointType(exponent, mantissa); + return FormulaType.getFloatingPointTypeWithoutSignBit(exponent, mantissa); } else if (pSort.is_bv()) { return FormulaType.getBitvectorTypeWithSize(pSort.bv_size()); } else if (pSort.is_array()) { @@ -380,7 +380,7 @@ public FormulaType getFormulaType(T pFormula) { } int exp = sort.fp_exp_size(); int man = sort.fp_sig_size() - 1; - return (FormulaType) FormulaType.getFloatingPointType(exp, man); + return (FormulaType) FormulaType.getFloatingPointTypeWithoutSignBit(exp, man); } else if (sort.is_rm()) { return (FormulaType) FormulaType.FloatingPointRoundingModeType; } From ca4a3f757daee591fdd1ef815008cfae56afb69a Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:43:05 +0200 Subject: [PATCH 07/67] Update CVC4 with new unambiguous FP mantissa size getters --- .../cvc4/CVC4FloatingPointFormulaManager.java | 51 +++++++++---------- .../solvers/cvc4/CVC4FormulaCreator.java | 6 +-- 2 files changed, 28 insertions(+), 29 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 248f6a55a8..3d0fbd70ec 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -10,13 +10,13 @@ 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; import edu.stanford.CVC4.FloatingPoint; import edu.stanford.CVC4.FloatingPointConvertSort; import edu.stanford.CVC4.FloatingPointSize; import edu.stanford.CVC4.FloatingPointToFPFloatingPoint; +import edu.stanford.CVC4.FloatingPointToFPIEEEBitVector; import edu.stanford.CVC4.FloatingPointToFPSignedBitVector; import edu.stanford.CVC4.FloatingPointToFPUnsignedBitVector; import edu.stanford.CVC4.FloatingPointToSBV; @@ -52,8 +52,8 @@ protected CVC4FloatingPointFormulaManager( private static FloatingPointSize getFPSize(FloatingPointType pType) { long pExponentSize = pType.getExponentSize(); - long pMantissaSize = pType.getMantissaSize(); - return new FloatingPointSize(pExponentSize, pMantissaSize + 1); // plus sign bit + long pMantissaSize = pType.getMantissaSizeWithSignBit(); + return new FloatingPointSize(pExponentSize, pMantissaSize); } @Override @@ -89,11 +89,11 @@ protected Expr makeNumberImpl( BigInteger exponent, BigInteger mantissa, Sign sign, FloatingPointType type) { final String signStr = sign.isNegative() ? "1" : "0"; final String exponentStr = getBvRepresentation(exponent, type.getExponentSize()); - final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSize()); + final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSizeWithoutSignBit()); final String bitvecStr = signStr + exponentStr + mantissaStr; final BitVector bitVector = new BitVector(bitvecStr, 2); final FloatingPoint fp = - new FloatingPoint(type.getExponentSize(), type.getMantissaSize() + 1, bitVector); + new FloatingPoint(type.getExponentSize(), type.getMantissaSizeWithSignBit(), bitVector); return exprManager.mkConst(fp); } @@ -109,7 +109,7 @@ protected Expr makeNumberAndRound(String pN, FloatingPointType pType, Expr pRoun final Rational rat = toRational(pN); final BigInteger upperBound = - getBiggestNumberBeforeInf(pType.getMantissaSize(), pType.getExponentSize()); + getBiggestNumberBeforeInf(pType.getMantissaSizeWithSignBit(), pType.getExponentSize()); if (rat.greater(Rational.fromDecimal(upperBound.negate().toString())) && rat.less(Rational.fromDecimal(upperBound.toString()))) { @@ -218,7 +218,7 @@ protected Expr castFromImpl( } else if (formulaType.isBitvectorType()) { long pExponentSize = pTargetType.getExponentSize(); - long pMantissaSize = pTargetType.getMantissaSize(); + long pMantissaSize = pTargetType.getMantissaSizeWithSignBit(); FloatingPointSize fpSize = new FloatingPointSize(pExponentSize, pMantissaSize + 1); FloatingPointConvertSort fpConvert = new FloatingPointConvertSort(fpSize); final Expr op; @@ -358,31 +358,30 @@ protected Expr isNegative(Expr pParam) { @Override protected Expr fromIeeeBitvectorImpl(Expr bitvector, FloatingPointType pTargetType) { - int mantissaSize = pTargetType.getMantissaSize(); - int exponentSize = pTargetType.getExponentSize(); - int size = pTargetType.getTotalSize(); - assert size == mantissaSize + exponentSize + 1; - - Expr signExtract = exprManager.mkConst(new BitVectorExtract(size - 1, size - 1)); - Expr exponentExtract = exprManager.mkConst(new BitVectorExtract(size - 2, mantissaSize)); - Expr mantissaExtract = exprManager.mkConst(new BitVectorExtract(mantissaSize - 1, 0)); - - Expr sign = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, signExtract, bitvector); - Expr exponent = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, exponentExtract, bitvector); - Expr mantissa = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, mantissaExtract, bitvector); + // This is just named weird, but the CVC4 doc say this is IEEE BV -> FP + FloatingPointConvertSort fpConvertSort = new FloatingPointConvertSort(getFPSize(pTargetType)); + Expr op = exprManager.mkConst(new FloatingPointToFPIEEEBitVector(fpConvertSort)); + return exprManager.mkExpr(op, bitvector); + } - return exprManager.mkExpr(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa); + @Override + protected Expr round(Expr pFormula, FloatingPointRoundingMode pRoundingMode) { + return exprManager.mkExpr(Kind.FLOATINGPOINT_RTI, getRoundingModeImpl(pRoundingMode), pFormula); } @Override - protected Expr toIeeeBitvectorImpl(Expr pNumber) { - // TODO possible work-around: use a tmp-variable "TMP" and add an - // additional constraint "pNumer == fromIeeeBitvectorImpl(TMP)" for it in all use-cases. - throw new UnsupportedOperationException("FP to IEEE-BV is not supported"); + protected int getMantissaSizeImpl(Expr f) { + Type type = f.getType(); + checkArgument(type.isFloatingPoint()); + edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(type); + return (int) fpType.getSignificandSize(); } @Override - protected Expr round(Expr pFormula, FloatingPointRoundingMode pRoundingMode) { - return exprManager.mkExpr(Kind.FLOATINGPOINT_RTI, getRoundingModeImpl(pRoundingMode), pFormula); + protected int getExponentSizeImpl(Expr f) { + Type type = f.getType(); + checkArgument(type.isFloatingPoint()); + edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(type); + return (int) fpType.getExponentSize(); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java index 23e7328956..1dac46d603 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -114,7 +114,7 @@ public Type getBitvectorType(int pBitwidth) { @Override public Type getFloatingPointType(FloatingPointType pType) { return exprManager.mkFloatingPointType( - pType.getExponentSize(), pType.getMantissaSize() + 1); // plus sign bit + pType.getExponentSize(), pType.getMantissaSizeWithSignBit()); } @Override @@ -154,7 +154,7 @@ public FormulaType getFormulaType(T pFormula) { t.isFloatingPoint(), "FloatingPointFormula with actual type %s: %s", t, pFormula); edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(t); return (FormulaType) - FormulaType.getFloatingPointType( + FormulaType.getFloatingPointTypeWithoutSignBit( (int) fpType.getExponentSize(), (int) fpType.getSignificandSize() - 1); // without sign bit @@ -182,7 +182,7 @@ private FormulaType getFormulaTypeFromTermType(Type t) { return FormulaType.getBitvectorTypeWithSize((int) new BitVectorType(t).getSize()); } else if (t.isFloatingPoint()) { edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(t); - return FormulaType.getFloatingPointType( + return FormulaType.getFloatingPointTypeWithoutSignBit( (int) fpType.getExponentSize(), (int) fpType.getSignificandSize() - 1); // without sign bit } else if (t.isRoundingMode()) { From 7bed3f5fa0e1a496264fccb502618eefd7c1bf25 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:43:09 +0200 Subject: [PATCH 08/67] Update CVC5 with new unambiguous FP mantissa size getters --- .../cvc5/CVC5FloatingPointFormulaManager.java | 69 +++++++------------ .../solvers/cvc5/CVC5FormulaCreator.java | 9 +-- 2 files changed, 30 insertions(+), 48 deletions(-) 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 883a8a1f8a..48211fcae0 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -78,7 +78,7 @@ protected Term makeNumberImpl( return termManager.mkFloatingPoint( termManager.mkBitVector(1, sign == Sign.NEGATIVE ? 1 : 0), termManager.mkBitVector(type.getExponentSize(), exponent.toString(16), 16), - termManager.mkBitVector(type.getMantissaSize(), mantissa.toString(16), 16)); + termManager.mkBitVector(type.getMantissaSizeWithoutSignBit(), mantissa.toString(16), 16)); } catch (CVC5ApiException e) { throw new IllegalArgumentException("You tried creating a invalid bitvector", e); @@ -90,7 +90,7 @@ protected Term makeNumberAndRound(String pN, FloatingPointType pType, Term pRoun try { if (isNegativeZero(Double.valueOf(pN))) { return termManager.mkFloatingPointNegZero( - pType.getExponentSize(), pType.getMantissaSize() + 1); + pType.getExponentSize(), pType.getMantissaSizeWithSignBit()); } } catch (CVC5ApiException | NumberFormatException e) { // ignore and fallback to floating point from rational numbers @@ -102,7 +102,7 @@ protected Term makeNumberAndRound(String pN, FloatingPointType pType, Term pRoun termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_REAL, pType.getExponentSize(), - pType.getMantissaSize() + 1); + pType.getMantissaSizeWithSignBit()); Term term = termManager.mkTerm(realToFp, pRoundingMode, termManager.mkReal(rationalValue.toString())); // simplification removes the cast from real to fp and return a bit-precise fp-number. @@ -111,8 +111,8 @@ protected Term makeNumberAndRound(String pN, FloatingPointType pType, Term pRoun throw new IllegalArgumentException( "You tried creating a invalid floating point with exponent size " + pType.getExponentSize() - + ", mantissa size " - + pType.getMantissaSize() + + ", mantissa size (including sign bit)" + + pType.getMantissaSizeWithSignBit() + " and value " + pN + ".", @@ -152,13 +152,13 @@ protected Term makeVariableImpl(String varName, FloatingPointType pType) { protected Term makePlusInfinityImpl(FloatingPointType pType) { try { return termManager.mkFloatingPointPosInf( - pType.getExponentSize(), pType.getMantissaSize() + 1); + pType.getExponentSize(), pType.getMantissaSizeWithSignBit()); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid positive floating point +infinity with exponent size " + pType.getExponentSize() + " and mantissa size " - + pType.getMantissaSize() + + pType.getMantissaSizeWithSignBit() + ".", e); } @@ -168,13 +168,13 @@ protected Term makePlusInfinityImpl(FloatingPointType pType) { protected Term makeMinusInfinityImpl(FloatingPointType pType) { try { return termManager.mkFloatingPointNegInf( - pType.getExponentSize(), pType.getMantissaSize() + 1); + pType.getExponentSize(), pType.getMantissaSizeWithSignBit()); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid negative floating point -infinity with exponent size " + pType.getExponentSize() + " and mantissa size " - + pType.getMantissaSize() + + pType.getMantissaSizeWithSignBit() + ".", e); } @@ -183,13 +183,14 @@ protected Term makeMinusInfinityImpl(FloatingPointType pType) { @Override protected Term makeNaNImpl(FloatingPointType pType) { try { - return termManager.mkFloatingPointNaN(pType.getExponentSize(), pType.getMantissaSize() + 1); + return termManager.mkFloatingPointNaN( + pType.getExponentSize(), pType.getMantissaSizeWithSignBit()); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid NaN with exponent size " + pType.getExponentSize() + " and mantissa size " - + pType.getMantissaSize() + + pType.getMantissaSizeWithSignBit() + ".", e); } @@ -205,7 +206,7 @@ protected Term castToImpl( termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_FP, ((FloatingPointType) pTargetType).getExponentSize(), - ((FloatingPointType) pTargetType).getMantissaSize() + 1); + ((FloatingPointType) pTargetType).getMantissaSizeWithSignBit()); return termManager.mkTerm(fpToFp, pRoundingMode, pNumber); } else if (pTargetType.isBitvectorType()) { @@ -246,7 +247,7 @@ protected Term castFromImpl( termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_REAL, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithSignBit()); return termManager.mkTerm(realToFp, pRoundingMode, pNumber); @@ -256,14 +257,14 @@ protected Term castFromImpl( termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_SBV, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithSignBit()); return termManager.mkTerm(realToSBv, pRoundingMode, pNumber); } else { Op realToUBv = termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_UBV, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithSignBit()); return termManager.mkTerm(realToUBv, pRoundingMode, pNumber); } @@ -278,7 +279,7 @@ protected Term castFromImpl( + " into a FloatingPoint with exponent size " + pTargetType.getExponentSize() + " and mantissa size " - + pTargetType.getMantissaSize() + + pTargetType.getMantissaSizeWithSignBit() + ".", e); } @@ -409,36 +410,16 @@ protected Term isNegative(Term pParam) { @Override protected Term fromIeeeBitvectorImpl(Term bitvector, FloatingPointType pTargetType) { - int mantissaSize = pTargetType.getMantissaSize(); - int exponentSize = pTargetType.getExponentSize(); - int size = pTargetType.getTotalSize(); - assert size == mantissaSize + exponentSize + 1; - - Op signExtract; - Op exponentExtract; - Op mantissaExtract; try { - signExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 1, size - 1); - exponentExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 2, mantissaSize); - mantissaExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, mantissaSize - 1, 0); - } catch (CVC5ApiException e) { - throw new IllegalArgumentException( - "You tried creating a invalid bitvector extract in term " + bitvector + ".", e); + return termManager.mkTerm( + termManager.mkOp( + Kind.FLOATINGPOINT_TO_FP_FROM_IEEE_BV, + pTargetType.getExponentSize(), + pTargetType.getMantissaSizeWithSignBit()), + bitvector); + } catch (CVC5ApiException pE) { + throw new RuntimeException(pE); } - - Term sign = termManager.mkTerm(signExtract, bitvector); - Term exponent = termManager.mkTerm(exponentExtract, bitvector); - Term mantissa = termManager.mkTerm(mantissaExtract, bitvector); - - return termManager.mkTerm(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa); - } - - @Override - protected Term toIeeeBitvectorImpl(Term pNumber) { - // TODO possible work-around: use a tmp-variable "TMP" and add an - // additional constraint "pNumer == fromIeeeBitvectorImpl(TMP)" for it in all use-cases. - // --> This has to be done on user-side, not in JavaSMT. - throw new UnsupportedOperationException("FP to IEEE-BV is not supported"); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java index 946b6be069..381daa2a29 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -142,14 +142,15 @@ public Sort getBitvectorType(int pBitwidth) { public Sort getFloatingPointType(FloatingPointType pType) { try { // plus sign bit - return termManager.mkFloatingPointSort(pType.getExponentSize(), pType.getMantissaSize() + 1); + return termManager.mkFloatingPointSort( + pType.getExponentSize(), pType.getMantissaSizeWithSignBit()); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "Cannot create floatingpoint sort with exponent size " + pType.getExponentSize() + " and mantissa " - + pType.getMantissaSize() - + " (plus sign bit).", + + pType.getMantissaSizeWithSignBit() + + " (including sign bit).", e); } } @@ -223,7 +224,7 @@ private FormulaType getFormulaTypeFromTermType(Sort sort) { return FormulaType.getBitvectorTypeWithSize(sort.getBitVectorSize()); } else if (sort.isFloatingPoint()) { // CVC5 wants the sign bit as part of the mantissa. We add that manually in creation. - return FormulaType.getFloatingPointType( + return FormulaType.getFloatingPointTypeWithoutSignBit( sort.getFloatingPointExponentSize(), sort.getFloatingPointSignificandSize() - 1); } else if (sort.isRoundingMode()) { return FormulaType.FloatingPointRoundingModeType; From 73c14516502242fb6d2a463aefb3d0363fc41686 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:43:16 +0200 Subject: [PATCH 09/67] Update MathSAT5 with new unambiguous FP mantissa size getters --- .../Mathsat5FloatingPointFormulaManager.java | 59 +++++++++++++++---- .../mathsat5/Mathsat5FormulaCreator.java | 17 +++--- 2 files changed, 58 insertions(+), 18 deletions(-) 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 d994620231..d319d07f1d 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java @@ -102,27 +102,41 @@ protected Long makeNumberImpl( BigInteger exponent, BigInteger mantissa, Sign sign, FloatingPointType type) { final String signStr = sign.isNegative() ? "1" : "0"; final String exponentStr = getBvRepresentation(exponent, type.getExponentSize()); - final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSize()); + // MathSAT5 expects the mantissa to not include the sign bit + final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSizeWithSignBit() - 1); 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()); + mathsatEnv, + bitvecValue.toString(), + type.getExponentSize(), + type.getMantissaSizeWithSignBit() - 1); } @Override protected Long makeNumberAndRound(String pN, FloatingPointType pType, Long pRoundingMode) { try { if (isNegativeZero(Double.valueOf(pN))) { + // MathSAT5 expects the mantissa to not include the sign bit return msat_make_fp_neg( mathsatEnv, msat_make_fp_rat_number( - mathsatEnv, "0", pType.getExponentSize(), pType.getMantissaSize(), pRoundingMode)); + mathsatEnv, + "0", + pType.getExponentSize(), + pType.getMantissaSizeWithSignBit() - 1, + pRoundingMode)); } } catch (NumberFormatException e) { // ignore and fallback to floating point from rational numbers } + // MathSAT5 expects the mantissa to not include the sign bit return msat_make_fp_rat_number( - mathsatEnv, pN, pType.getExponentSize(), pType.getMantissaSize(), pRoundingMode); + mathsatEnv, + pN, + pType.getExponentSize(), + pType.getMantissaSizeWithoutSignBit(), + pRoundingMode); } @Override @@ -132,17 +146,23 @@ protected Long makeVariableImpl(String var, FloatingPointType type) { @Override protected Long makePlusInfinityImpl(FloatingPointType type) { - return msat_make_fp_plus_inf(mathsatEnv, type.getExponentSize(), type.getMantissaSize()); + // MathSAT5 expects the mantissa to not include the sign bit + return msat_make_fp_plus_inf( + mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithSignBit() - 1); } @Override protected Long makeMinusInfinityImpl(FloatingPointType type) { - return msat_make_fp_minus_inf(mathsatEnv, type.getExponentSize(), type.getMantissaSize()); + // MathSAT5 expects the mantissa to not include the sign bit + return msat_make_fp_minus_inf( + mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithSignBit() - 1); } @Override protected Long makeNaNImpl(FloatingPointType type) { - return msat_make_fp_nan(mathsatEnv, type.getExponentSize(), type.getMantissaSize()); + // MathSAT5 expects the mantissa to not include the sign bit + return msat_make_fp_nan( + mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithSignBit() - 1); } @Override @@ -150,10 +170,11 @@ protected Long castToImpl( Long pNumber, boolean pSigned, FormulaType pTargetType, Long pRoundingMode) { if (pTargetType.isFloatingPointType()) { FormulaType.FloatingPointType targetType = (FormulaType.FloatingPointType) pTargetType; + // MathSAT5 expects the mantissa to not include the sign bit return msat_make_fp_cast( mathsatEnv, targetType.getExponentSize(), - targetType.getMantissaSize(), + targetType.getMantissaSizeWithSignBit() - 1, pRoundingMode, pNumber); @@ -179,18 +200,19 @@ protected Long castFromImpl( return castToImpl(pNumber, pSigned, pTargetType, pRoundingMode); } else if (formulaType.isBitvectorType()) { + // MathSAT5 expects the mantissa to not include the sign bit if (pSigned) { return msat_make_fp_from_sbv( mathsatEnv, pTargetType.getExponentSize(), - pTargetType.getMantissaSize(), + pTargetType.getMantissaSizeWithSignBit() - 1, pRoundingMode, pNumber); } else { return msat_make_fp_from_ubv( mathsatEnv, pTargetType.getExponentSize(), - pTargetType.getMantissaSize(), + pTargetType.getMantissaSizeWithSignBit() - 1, pRoundingMode, pNumber); } @@ -214,8 +236,12 @@ private Long genericCast(Long pNumber, FormulaType pTargetType) { @Override protected Long fromIeeeBitvectorImpl(Long pNumber, FloatingPointType pTargetType) { + // MathSAT5 expects the mantissa to not include the sign bit return Mathsat5NativeApi.msat_make_fp_from_ieeebv( - mathsatEnv, pTargetType.getExponentSize(), pTargetType.getMantissaSize(), pNumber); + mathsatEnv, + pTargetType.getExponentSize(), + pTargetType.getMantissaSizeWithSignBit() - 1, + pNumber); } @Override @@ -223,6 +249,17 @@ protected Long toIeeeBitvectorImpl(Long pNumber) { return Mathsat5NativeApi.msat_make_fp_as_ieeebv(mathsatEnv, pNumber); } + @Override + protected int getMantissaSizeImpl(Long f) { + // The mantissa includes the sign bit according to the SMTLib2 standard, but MathSAT does not. + return msat_get_fp_type_mant_width(mathsatEnv, msat_term_get_type(f)) + 1; + } + + @Override + protected int getExponentSizeImpl(Long f) { + return msat_get_fp_type_exp_width(mathsatEnv, msat_term_get_type(f)); + } + @Override protected Long negate(Long pNumber) { return msat_make_fp_neg(mathsatEnv, pNumber); diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java index 8bcfe9ebbe..b836c212da 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -214,7 +214,7 @@ private FormulaType getFormulaTypeFromTermType(Long type) { } else if (msat_is_bv_type(env, type)) { return FormulaType.getBitvectorTypeWithSize(msat_get_bv_type_size(env, type)); } else if (msat_is_fp_type(env, type)) { - return FormulaType.getFloatingPointType( + return FormulaType.getFloatingPointTypeWithoutSignBit( msat_get_fp_type_exp_width(env, type), msat_get_fp_type_mant_width(env, type)); } else if (msat_is_fp_roundingmode_type(env, type)) { return FormulaType.FloatingPointRoundingModeType; @@ -242,7 +242,9 @@ public Long getBitvectorType(int pBitwidth) { @Override public Long getFloatingPointType(FloatingPointType pType) { - return msat_get_fp_type(getEnv(), pType.getExponentSize(), pType.getMantissaSize()); + // MathSAT5 automatically adds 1 to the mantissa, as it expects it to be without it. + return msat_get_fp_type( + getEnv(), pType.getExponentSize(), pType.getMantissaSizeWithSignBit() - 1); } @SuppressWarnings("unchecked") @@ -578,13 +580,14 @@ private FloatingPointNumber parseFloatingPoint(String lTermRepresentation) { BigInteger bits = new BigInteger(matcher.group(1)); int expWidth = Integer.parseInt(matcher.group(2)); - int mantWidth = Integer.parseInt(matcher.group(3)); + // The term representation in MathSAT5 does not include the sign bit + int mantWidthWithoutSignBit = Integer.parseInt(matcher.group(3)); - Sign sign = Sign.of(bits.testBit(expWidth + mantWidth)); - BigInteger exponent = extractBitsFrom(bits, mantWidth, expWidth); - BigInteger mantissa = extractBitsFrom(bits, 0, mantWidth); + Sign sign = Sign.of(bits.testBit(expWidth + mantWidthWithoutSignBit)); + BigInteger exponent = extractBitsFrom(bits, mantWidthWithoutSignBit, expWidth); + BigInteger mantissa = extractBitsFrom(bits, 0, mantWidthWithoutSignBit); - return FloatingPointNumber.of(sign, exponent, mantissa, expWidth, mantWidth); + return FloatingPointNumber.of(sign, exponent, mantissa, expWidth, mantWidthWithoutSignBit); } /** From 1ca40f928f62fe525233f8bacefde545124345ed Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:43:22 +0200 Subject: [PATCH 10/67] Update Z3 with new unambiguous FP mantissa size getters --- .../z3/Z3FloatingPointFormulaManager.java | 8 ++++--- .../java_smt/solvers/z3/Z3FormulaCreator.java | 21 ++++++++++++------- 2 files changed, 18 insertions(+), 11 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 84ed3dc559..39079464aa 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java @@ -20,7 +20,8 @@ class Z3FloatingPointFormulaManager extends AbstractFloatingPointFormulaManager { - private static final FloatingPointType highPrec = FormulaType.getFloatingPointType(15, 112); + private static final FloatingPointType highPrec = + FormulaType.getFloatingPointTypeWithoutSignBit(15, 112); private final long z3context; private final long roundingMode; @@ -78,7 +79,8 @@ protected Long makeNumberImpl( final long signSort = getFormulaCreator().getBitvectorType(1); final long expoSort = getFormulaCreator().getBitvectorType(type.getExponentSize()); - final long mantSort = getFormulaCreator().getBitvectorType(type.getMantissaSize()); + final long mantSort = + getFormulaCreator().getBitvectorType(type.getMantissaSizeWithoutSignBit()); final long signBv = Native.mkNumeral(z3context, sign.isNegative() ? "1" : "0", signSort); Native.incRef(z3context, signBv); @@ -99,7 +101,7 @@ protected Long makeNumberAndRound(String pN, FloatingPointType pType, Long pRoun // Z3 does not allow specifying a rounding mode for numerals, // so we create it first with a high precision and then round it down explicitly. if (pType.getExponentSize() <= highPrec.getExponentSize() - || pType.getMantissaSize() <= highPrec.getMantissaSize()) { + || pType.getMantissaSizeWithSignBit() <= highPrec.getMantissaSizeWithSignBit()) { long highPrecNumber = Native.mkNumeral(z3context, pN, mkFpaSort(highPrec)); Native.incRef(z3context, highPrecNumber); long smallPrecNumber = diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java index edd4da657d..e5e8eb0dae 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -242,7 +242,7 @@ public FormulaType getFormulaTypeFromSort(Long pSort) { return FormulaType.getArrayType( getFormulaTypeFromSort(domainSort), getFormulaTypeFromSort(rangeSort)); case Z3_FLOATING_POINT_SORT: - return FormulaType.getFloatingPointType( + return FormulaType.getFloatingPointTypeWithoutSignBit( Native.fpaGetEbits(z3context, pSort), Native.fpaGetSbits(z3context, pSort) - 1); case Z3_ROUNDING_MODE_SORT: return FormulaType.FloatingPointRoundingModeType; @@ -421,7 +421,8 @@ public Long getBitvectorType(int pBitwidth) { @Override public Long getFloatingPointType(FormulaType.FloatingPointType type) { - long fpSort = Native.mkFpaSort(getEnv(), type.getExponentSize(), type.getMantissaSize() + 1); + long fpSort = + Native.mkFpaSort(getEnv(), type.getExponentSize(), type.getMantissaSizeWithSignBit()); Native.incRef(getEnv(), Native.sortToAst(getEnv(), fpSort)); return fpSort; } @@ -970,7 +971,7 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p expo, mant, pType.getExponentSize(), - pType.getMantissaSize()); + pType.getMantissaSizeWithSignBit()); } else if (Native.fpaIsNumeralInf(environment, pValue)) { // Floating Point Inf uses: @@ -979,9 +980,11 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p // - "00..00" as mantissa. String sign = getSign(pValue).isNegative() ? "1" : "0"; return FloatingPointNumber.of( - sign + "1".repeat(pType.getExponentSize()) + "0".repeat(pType.getMantissaSize()), + sign + + "1".repeat(pType.getExponentSize()) + + "0".repeat(pType.getMantissaSizeWithSignBit()), pType.getExponentSize(), - pType.getMantissaSize()); + pType.getMantissaSizeWithSignBit()); } else if (Native.fpaIsNumeralNan(environment, pValue)) { // TODO We are underspecified here and choose several bits on our own. @@ -991,9 +994,11 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p // - "11..11" as exponent, // - an unspecified mantissa (we choose all "1"). return FloatingPointNumber.of( - "0" + "1".repeat(pType.getExponentSize()) + "1".repeat(pType.getMantissaSize()), + "0" + + "1".repeat(pType.getExponentSize()) + + "1".repeat(pType.getMantissaSizeWithSignBit()), pType.getExponentSize(), - pType.getMantissaSize()); + pType.getMantissaSizeWithSignBit()); } else { Sign sign = getSign(pValue); @@ -1006,7 +1011,7 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p new BigInteger(exponent), new BigInteger(mantissa), pType.getExponentSize(), - pType.getMantissaSize()); + pType.getMantissaSizeWithSignBit()); } } From 6d8032108aa4c7a8c96a053eb52cf53ea0e9e977 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:43:31 +0200 Subject: [PATCH 11/67] Update SolverVisitorTest with new unambiguous FP mantissa size getters --- src/org/sosy_lab/java_smt/test/SolverVisitorTest.java | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 56b0200874..bd072cd759 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -477,13 +477,14 @@ public void floatConstantVisit() { Integer.toBinaryString(Float.floatToRawIntBits(entry.getKey().floatValue())), 32, '0')); - checkFloatConstant(FormulaType.getFloatingPointType(5, 10), entry.getKey(), entry.getValue()); + checkFloatConstant( + FormulaType.getFloatingPointTypeWithoutSignBit(5, 10), entry.getKey(), entry.getValue()); } } private void checkFloatConstant(FloatingPointType prec, double value, String bits) { FloatingPointNumber fp = - FloatingPointNumber.of(bits, prec.getExponentSize(), prec.getMantissaSize()); + FloatingPointNumber.of(bits, prec.getExponentSize(), prec.getMantissaSizeWithSignBit()); ConstantsVisitor visitor = new ConstantsVisitor(); mgr.visit(fpmgr.makeNumber(value, prec), visitor); @@ -580,7 +581,7 @@ public void fpToBvTest() { .that(solverToUse()) .isNoneOf(Solvers.CVC4, Solvers.CVC5); - var fpType = FormulaType.getFloatingPointType(5, 10); + var fpType = FormulaType.getFloatingPointTypeWithoutSignBit(5, 10); var visitor = new DefaultFormulaVisitor() { @Override From 44310e089a80d26b2e8c0cb3e31b395f3487d5b6 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 08:52:02 +0200 Subject: [PATCH 12/67] Fix off-by-one FP mantissa bug when casting BV to FP --- .../java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 3d0fbd70ec..06ddc49fda 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -219,7 +219,7 @@ protected Expr castFromImpl( } else if (formulaType.isBitvectorType()) { long pExponentSize = pTargetType.getExponentSize(); long pMantissaSize = pTargetType.getMantissaSizeWithSignBit(); - FloatingPointSize fpSize = new FloatingPointSize(pExponentSize, pMantissaSize + 1); + FloatingPointSize fpSize = new FloatingPointSize(pExponentSize, pMantissaSize); FloatingPointConvertSort fpConvert = new FloatingPointConvertSort(fpSize); final Expr op; if (pSigned) { From 475ce6814c5fc9241f6c071f4fdd56a769d737f9 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 10:30:51 +0200 Subject: [PATCH 13/67] Remove changes left over from PR 512 (to be added back with PR 512!) --- .../AbstractFloatingPointFormulaManager.java | 7 +- .../cvc4/CVC4FloatingPointFormulaManager.java | 16 -- .../Mathsat5FloatingPointFormulaManager.java | 11 - .../test/FloatingPointFormulaManagerTest.java | 200 ------------------ 4 files changed, 6 insertions(+), 228 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 47c847afe2..5082f24634 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -256,7 +256,12 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula pNumber) { return getFormulaCreator().encapsulateBitvector(toIeeeBitvectorImpl(extractInfo(pNumber))); } - protected abstract TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber); + @SuppressWarnings("unused") + protected TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber) { + throw new UnsupportedOperationException( + "Solver does not support transformation from " + + "floating-point numbers to IEEE bitvector"); + } @Override public FloatingPointFormula negate(FloatingPointFormula pNumber) { 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 06ddc49fda..dfc4b84d08 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -368,20 +368,4 @@ protected Expr fromIeeeBitvectorImpl(Expr bitvector, FloatingPointType pTargetTy protected Expr round(Expr pFormula, FloatingPointRoundingMode pRoundingMode) { return exprManager.mkExpr(Kind.FLOATINGPOINT_RTI, getRoundingModeImpl(pRoundingMode), pFormula); } - - @Override - protected int getMantissaSizeImpl(Expr f) { - Type type = f.getType(); - checkArgument(type.isFloatingPoint()); - edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(type); - return (int) fpType.getSignificandSize(); - } - - @Override - protected int getExponentSizeImpl(Expr f) { - Type type = f.getType(); - checkArgument(type.isFloatingPoint()); - edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(type); - return (int) fpType.getExponentSize(); - } } 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 d319d07f1d..11d8e472d6 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java @@ -249,17 +249,6 @@ protected Long toIeeeBitvectorImpl(Long pNumber) { return Mathsat5NativeApi.msat_make_fp_as_ieeebv(mathsatEnv, pNumber); } - @Override - protected int getMantissaSizeImpl(Long f) { - // The mantissa includes the sign bit according to the SMTLib2 standard, but MathSAT does not. - return msat_get_fp_type_mant_width(mathsatEnv, msat_term_get_type(f)) + 1; - } - - @Override - protected int getExponentSizeImpl(Long f) { - return msat_get_fp_type_exp_width(mathsatEnv, msat_term_get_type(f)); - } - @Override protected Long negate(Long pNumber) { return msat_make_fp_neg(mathsatEnv, pNumber); diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 48e334b32c..79f4afbbfe 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -499,192 +499,6 @@ public void specialValueFunctionsFrom64Bits2() throws SolverException, Interrupt bmgr.and(bmgr.not(fpmgr.isNaN(x)), bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1)))); } - // Same as specialValueFunctionsFrom32Bits2, but with fallback toIeeeBitvector() implementation. - @Test - public void specialValueFunctionsFrom32Bits2ToIeeeFallback() - throws SolverException, InterruptedException { - requireBitvectors(); - - final FloatingPointFormula x = fpmgr.makeVariable("x32", singlePrecType); - BitvectorFormulaAndBooleanFormula xToIeeeAndAddConstraint = - fpmgr.toIeeeBitvector(x, "bvConst_x"); - BitvectorFormula xToIeee = xToIeeeAndAddConstraint.getBitvectorFormula(); - final BitvectorFormula signBit = bvmgr.extract(xToIeee, 31, 31); - final BitvectorFormula exponent = bvmgr.extract(xToIeee, 30, 23); - final BitvectorFormula mantissa = bvmgr.extract(xToIeee, 22, 0); - final BooleanFormula additionalConstraint = xToIeeeAndAddConstraint.getBooleanFormula(); - - assertThatFormula( - bmgr.implication( - additionalConstraint, - bmgr.equivalence( - fpmgr.isInfinity(x), - bmgr.or( - bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x7f80_0000L)), - bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0xff80_0000L)))))) - .isTautological(); - - assertThatFormula( - bmgr.implication( - additionalConstraint, - bmgr.equivalence( - fpmgr.isZero(x), - bmgr.or( - bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x0000_0000)), - bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x8000_0000L)))))) - .isTautological(); - - assertThatFormula( - bmgr.implication( - additionalConstraint, - bmgr.equivalence( - fpmgr.isNormal(x), - bmgr.and( - bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0))), - bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1))))))) - .isTautological(); - - assertThatFormula( - bmgr.implication( - additionalConstraint, - bmgr.equivalence( - fpmgr.isSubnormal(x), - bmgr.and( - bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0)), - bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0))))))) - .isTautological(); - - assertThatFormula( - bmgr.implication( - additionalConstraint, - bmgr.equivalence( - fpmgr.isNaN(x), - bmgr.and( - bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1)), - bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0))))))) - .isTautological(); - - assertThatFormula( - bmgr.implication( - additionalConstraint, - bmgr.equivalence( - fpmgr.isNegative(x), - bmgr.and( - bmgr.not(fpmgr.isNaN(x)), - bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1)))))) - .isTautological(); - } - - // Same as specialValueFunctionsFrom64Bits2, but with fallback toIeeeBitvector() implementation. - @Test - public void specialValueFunctionsFrom64Bits2ToIeeeFallback() - throws SolverException, InterruptedException { - requireBitvectors(); - - final FloatingPointFormula x = fpmgr.makeVariable("x64", doublePrecType); - BitvectorFormulaAndBooleanFormula xToIeeeAndAddConstraint = - fpmgr.toIeeeBitvector(x, "bvConst_x"); - BitvectorFormula xToIeee = xToIeeeAndAddConstraint.getBitvectorFormula(); - final BitvectorFormula signBit = bvmgr.extract(xToIeee, 63, 63); - final BitvectorFormula exponent = bvmgr.extract(xToIeee, 62, 52); - final BitvectorFormula mantissa = bvmgr.extract(xToIeee, 51, 0); - final BooleanFormula additionalConstraint = xToIeeeAndAddConstraint.getBooleanFormula(); - - assertThatFormula( - bmgr.implication( - additionalConstraint, - bmgr.equivalence( - fpmgr.isInfinity(x), - bmgr.or( - bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x7ff0_0000_0000_0000L)), - bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0xfff0_0000_0000_0000L)))))) - .isTautological(); - - assertThatFormula( - bmgr.implication( - additionalConstraint, - bmgr.equivalence( - fpmgr.isZero(x), - bmgr.or( - bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x0000_0000_0000_0000L)), - bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x8000_0000_0000_0000L)))))) - .isTautological(); - - assertThatFormula( - bmgr.implication( - additionalConstraint, - bmgr.equivalence( - fpmgr.isNormal(x), - bmgr.and( - bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0))), - bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, -1))))))) - .isTautological(); - - assertThatFormula( - bmgr.implication( - additionalConstraint, - bmgr.equivalence( - fpmgr.isSubnormal(x), - bmgr.and( - bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0)), - bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(52, 0))))))) - .isTautological(); - - assertThatFormula( - bmgr.implication( - additionalConstraint, - bmgr.equivalence( - fpmgr.isNaN(x), - bmgr.and( - bvmgr.equal(exponent, bvmgr.makeBitvector(11, -1)), - bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(52, 0))))))) - .isTautological(); - - assertThatFormula( - bmgr.implication( - additionalConstraint, - bmgr.equivalence( - fpmgr.isNegative(x), - bmgr.and( - bmgr.not(fpmgr.isNaN(x)), - bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1)))))) - .isTautological(); - } - - @Test - public void floatingPointSinglePrecisionSizeWithBvTransformationTest() { - requireBitvectors(); - int fpSinglePrecSize = 32; - var bv32 = bvmgr.makeBitvector(fpSinglePrecSize, 0); - assertThat(bvmgr.getLength(bv32)).isEqualTo(fpSinglePrecSize); - - requireFloats(); - var singlePrec = FormulaType.getSinglePrecisionFloatingPointType(); - var fpSinglePrec = fpmgr.makeNumber(0.0, singlePrec); - // Sizes of the type and the actual term should match - assertThat(fpmgr.getExponentSize(fpSinglePrec)).isEqualTo(8); - assertThat(fpmgr.getMantissaSizeWithSignBit(fpSinglePrec)).isEqualTo(24); - assertThat(singlePrec.getExponentSize()).isEqualTo(8); - assertThat(singlePrec.getMantissaSizeWithSignBit()).isEqualTo(24); - assertThat(singlePrec.getExponentSize() + singlePrec.getMantissaSizeWithSignBit()) - .isEqualTo(fpSinglePrecSize); - assertThat(singlePrec.getTotalSize()) - .isEqualTo(singlePrec.getExponentSize() + singlePrec.getMantissaSizeWithSignBit()); - - assertThat(bvmgr.getLength(fpmgr.toIeeeBitvector(fpSinglePrec, "dummy1").getBitvectorFormula())) - .isEqualTo(fpSinglePrecSize); - assertThat( - bvmgr.getLength( - fpmgr - .toIeeeBitvector(fpSinglePrec, "dummy2", ImmutableMap.of()) - .getBitvectorFormula())) - .isEqualTo(fpSinglePrecSize); - - if (solverSupportsNativeFPToBitvector()) { - assertThat(bvmgr.getLength(fpmgr.toIeeeBitvector(fpSinglePrec))).isEqualTo(fpSinglePrecSize); - } - } - @Test public void specialDoubles() throws SolverException, InterruptedException { assertThatFormula(fpmgr.assignment(fpmgr.makeNumber(Double.NaN, singlePrecType), nan)) @@ -1402,8 +1216,6 @@ public void fpModelValue() throws SolverException, InterruptedException { Float.MIN_NORMAL, }) { var constFpNum = fpmgr.makeNumber(f, singlePrecType); - assertThat(fpmgr.getMantissaSizeWithSignBit(constFpNum)) - .isEqualTo(singlePrecType.getMantissaSizeWithSignBit()); FloatingPointNumber fpValue = model.evaluate(constFpNum); assertThat(fpValue.getMantissaSizeWithSignBit()) .isEqualTo(singlePrecType.getMantissaSizeWithSignBit()); @@ -1459,8 +1271,6 @@ public void fpFrom32BitPattern() throws SolverException, InterruptedException { final FloatingPointFormula fpFromBv = fpmgr.makeNumber( BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, singlePrecType); - assertThat(fpmgr.getMantissaSizeWithSignBit(fpFromBv) + fpmgr.getExponentSize(fpFromBv)) - .isEqualTo(singlePrecType.getTotalSize()); final FloatingPointNumber fpNumber = FloatingPointNumber.of( sign, @@ -1473,11 +1283,7 @@ public void fpFrom32BitPattern() throws SolverException, InterruptedException { assertThat(fpNumber.getMantissaSizeWithoutSignBit()) .isEqualTo(singlePrecType.getMantissaSizeWithSignBit() - 1); final FloatingPointFormula fp1 = fpmgr.makeNumber(fpNumber); - assertThat(fpmgr.getMantissaSizeWithSignBit(fp1) + fpmgr.getExponentSize(fp1)) - .isEqualTo(singlePrecType.getTotalSize()); final FloatingPointFormula fp2 = fpmgr.makeNumber(pFloat, singlePrecType); - assertThat(fpmgr.getMantissaSizeWithSignBit(fp2) + fpmgr.getExponentSize(fp2)) - .isEqualTo(singlePrecType.getTotalSize()); final BooleanFormula assignment1 = fpmgr.assignment(fpFromBv, fp1); final BooleanFormula assignment2 = fpmgr.assignment(fpFromBv, fp2); return bmgr.and(assignment1, assignment2); @@ -1497,8 +1303,6 @@ public void fpFrom64BitPattern() throws SolverException, InterruptedException { final FloatingPointFormula fpFromBv = fpmgr.makeNumber( BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, doublePrecType); - assertThat(fpmgr.getMantissaSizeWithSignBit(fpFromBv) + fpmgr.getExponentSize(fpFromBv)) - .isEqualTo(doublePrecType.getTotalSize()); final FloatingPointNumber fpNumber = FloatingPointNumber.of( sign, @@ -1511,11 +1315,7 @@ public void fpFrom64BitPattern() throws SolverException, InterruptedException { assertThat(fpNumber.getMantissaSizeWithoutSignBit()) .isEqualTo(doublePrecType.getMantissaSizeWithSignBit() - 1); final FloatingPointFormula fp1 = fpmgr.makeNumber(fpNumber); - assertThat(fpmgr.getMantissaSizeWithSignBit(fp1) + fpmgr.getExponentSize(fp1)) - .isEqualTo(doublePrecType.getTotalSize()); final FloatingPointFormula fp2 = fpmgr.makeNumber(pDouble, doublePrecType); - assertThat(fpmgr.getMantissaSizeWithSignBit(fp2) + fpmgr.getExponentSize(fp2)) - .isEqualTo(doublePrecType.getTotalSize()); final BooleanFormula assignment1 = fpmgr.assignment(fpFromBv, fp1); final BooleanFormula assignment2 = fpmgr.assignment(fpFromBv, fp2); return bmgr.and(assignment1, assignment2); From bb3760d7c9ace93e2e14ca6d325bb4449032354d Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 10:46:42 +0200 Subject: [PATCH 14/67] Fix bug in test using the wrong mantissa size for an FP --- src/org/sosy_lab/java_smt/test/SolverVisitorTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index bd072cd759..6fc6eef023 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -484,7 +484,7 @@ public void floatConstantVisit() { private void checkFloatConstant(FloatingPointType prec, double value, String bits) { FloatingPointNumber fp = - FloatingPointNumber.of(bits, prec.getExponentSize(), prec.getMantissaSizeWithSignBit()); + FloatingPointNumber.of(bits, prec.getExponentSize(), prec.getMantissaSizeWithoutSignBit()); ConstantsVisitor visitor = new ConstantsVisitor(); mgr.visit(fpmgr.makeNumber(value, prec), visitor); From 31b0b3837e2d6758d8c4be3320c5540364f664b9 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 13:27:44 +0200 Subject: [PATCH 15/67] Apply checkstyle naming/grammar suggestions --- src/org/sosy_lab/java_smt/api/FormulaType.java | 2 +- .../solvers/cvc5/CVC5FloatingPointFormulaManager.java | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index a6a705a8f6..da62759ba3 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -287,7 +287,7 @@ public boolean isFloatingPointType() { return true; } - /** Returns the size of the exponent */ + /** Returns the size of the exponent. */ public int getExponentSize() { return exponentSize; } 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 48211fcae0..9493b754ff 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -409,14 +409,14 @@ protected Term isNegative(Term pParam) { } @Override - protected Term fromIeeeBitvectorImpl(Term bitvector, FloatingPointType pTargetType) { + protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetType) { try { return termManager.mkTerm( termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_IEEE_BV, pTargetType.getExponentSize(), pTargetType.getMantissaSizeWithSignBit()), - bitvector); + pBitvector); } catch (CVC5ApiException pE) { throw new RuntimeException(pE); } From 4b07b9bbd2120b7efedef8d8767d03328626fe51 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 13:30:00 +0200 Subject: [PATCH 16/67] Fix off-by-one error for mantissa for getFloatingPointTypeWithSignBit() --- src/org/sosy_lab/java_smt/api/FormulaType.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index da62759ba3..9d36fe153c 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -245,7 +245,8 @@ public static FloatingPointType getFloatingPointTypeWithoutSignBit( */ public static FloatingPointType getFloatingPointTypeWithSignBit( int exponentSize, int mantissaSizeWithSignBit) { - return new FloatingPointType(exponentSize, mantissaSizeWithSignBit); + // We save the mantissa without the sign bit internally + return new FloatingPointType(exponentSize, mantissaSizeWithSignBit - 1); } /** From e444b523608d0b39c9335168a608babd7603e00d Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 13:42:14 +0200 Subject: [PATCH 17/67] Update naming of mantissa arguments in constructors for FloatingPointNumber and use new mantissa API instead of the old --- .../api/FloatingPointFormulaManager.java | 2 +- .../java_smt/api/FloatingPointNumber.java | 54 ++++++++++++------- 2 files changed, 35 insertions(+), 21 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index 62bb3afbe4..126bf9b504 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -99,7 +99,7 @@ default FloatingPointFormula makeNumber(FloatingPointNumber number) { number.getExponent(), number.getMantissa(), number.getMathSign(), - getFloatingPointType(number.getExponentSize(), number.getMantissaSize())); + getFloatingPointType(number.getExponentSize(), number.getMantissaSizeWithoutSignBit())); } /** diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index 6c750e3701..19fdb61182 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -86,22 +86,22 @@ public final boolean getSign() { * bit. */ // TODO: mark as soon to be deprecated - public abstract int getMantissaSize(); + public int getMantissaSize() { + return getMantissaSizeWithoutSignBit(); + } /** * Returns the size of the mantissa (also called a coefficient or significant), excluding the sign * bit. */ - public int getMantissaSizeWithoutSignBit() { - return getMantissaSize(); - } + public abstract int getMantissaSizeWithoutSignBit(); /** * Returns the size of the mantissa (also called a coefficient or significant), including the sign * bit. */ public int getMantissaSizeWithSignBit() { - return getMantissaSize() + 1; + return getMantissaSizeWithoutSignBit() + 1; } /** @@ -114,7 +114,8 @@ public int getMantissaSizeWithSignBit() { * @param mantissa the mantissa of the floating-point number, given as unsigned (not negative) * number without hidden bit * @param exponentSize the (maximum) size of the exponent in bits - * @param mantissaSize the (maximum) size of the mantissa in bits (excluding the sign bit) + * @param mantissaSizeWithoutSignBit the (maximum) size of the mantissa in bits (excluding the + * sign bit) * @see #of(Sign, BigInteger, BigInteger, int, int) */ @Deprecated( @@ -122,14 +123,19 @@ public int getMantissaSizeWithSignBit() { forRemoval = true) @InlineMe( replacement = - "FloatingPointNumber.of(Sign.of(sign), exponent, mantissa, exponentSize, mantissaSize)", + "FloatingPointNumber.of(Sign.of(sign), exponent, mantissa, exponentSize," + + " mantissaSizeWithoutSignBit)", imports = { "org.sosy_lab.java_smt.api.FloatingPointNumber", "org.sosy_lab.java_smt.api.FloatingPointNumber.Sign" }) public static FloatingPointNumber of( - boolean sign, BigInteger exponent, BigInteger mantissa, int exponentSize, int mantissaSize) { - return of(Sign.of(sign), exponent, mantissa, exponentSize, mantissaSize); + boolean sign, + BigInteger exponent, + BigInteger mantissa, + int exponentSize, + int mantissaSizeWithoutSignBit) { + return of(Sign.of(sign), exponent, mantissa, exponentSize, mantissaSizeWithoutSignBit); } /** @@ -141,15 +147,21 @@ public static FloatingPointNumber of( * @param mantissa the mantissa of the floating-point number, given as unsigned (not negative) * number without hidden bit * @param exponentSize the (maximum) size of the exponent in bits - * @param mantissaSize the (maximum) size of the mantissa in bits (excluding the sign bit) + * @param mantissaSizeWithoutSignBit the (maximum) size of the mantissa in bits (excluding the + * sign bit) */ public static FloatingPointNumber of( - Sign sign, BigInteger exponent, BigInteger mantissa, int exponentSize, int mantissaSize) { + Sign sign, + BigInteger exponent, + BigInteger mantissa, + int exponentSize, + int mantissaSizeWithoutSignBit) { Preconditions.checkArgument(exponent.bitLength() <= exponentSize); - Preconditions.checkArgument(mantissa.bitLength() <= mantissaSize); + Preconditions.checkArgument(mantissa.bitLength() <= mantissaSizeWithoutSignBit); Preconditions.checkArgument(exponent.compareTo(BigInteger.ZERO) >= 0); Preconditions.checkArgument(mantissa.compareTo(BigInteger.ZERO) >= 0); - return new AutoValue_FloatingPointNumber(sign, exponent, mantissa, exponentSize, mantissaSize); + return new AutoValue_FloatingPointNumber( + sign, exponent, mantissa, exponentSize, mantissaSizeWithoutSignBit); } /** @@ -158,25 +170,27 @@ public static FloatingPointNumber of( * @param bits the bit-representation of the floating-point number, consisting of sign bit, * exponent (without bias) and mantissa (without hidden bit) in this exact ordering * @param exponentSize the size of the exponent in bits - * @param mantissaSize the size of the mantissa in bits (excluding the sign bit) + * @param mantissaSizeWithoutSignBit the size of the mantissa in bits (excluding the sign bit) */ - public static FloatingPointNumber of(String bits, int exponentSize, int mantissaSize) { + public static FloatingPointNumber of( + String bits, int exponentSize, int mantissaSizeWithoutSignBit) { Preconditions.checkArgument(0 < exponentSize); - Preconditions.checkArgument(0 < mantissaSize); + Preconditions.checkArgument(0 < mantissaSizeWithoutSignBit); Preconditions.checkArgument( - bits.length() == 1 + exponentSize + mantissaSize, + bits.length() == 1 + exponentSize + mantissaSizeWithoutSignBit, "Bitsize (%s) of floating point numeral does not match the size of sign, exponent and " + "mantissa (%s + %s + %s).", bits.length(), 1, exponentSize, - mantissaSize); + mantissaSizeWithoutSignBit); Preconditions.checkArgument(bits.chars().allMatch(c -> c == '0' || c == '1')); Sign sign = Sign.of(bits.charAt(0) == '1'); BigInteger exponent = new BigInteger(bits.substring(1, 1 + exponentSize), 2); BigInteger mantissa = - new BigInteger(bits.substring(1 + exponentSize, 1 + exponentSize + mantissaSize), 2); - return of(sign, exponent, mantissa, exponentSize, mantissaSize); + new BigInteger( + bits.substring(1 + exponentSize, 1 + exponentSize + mantissaSizeWithoutSignBit), 2); + return of(sign, exponent, mantissa, exponentSize, mantissaSizeWithoutSignBit); } /** From f1ff09f9989668b1559e9890852a69b0e9fe4dac Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 13:48:11 +0200 Subject: [PATCH 18/67] Fix accidentally added off-by-one bug in CVC4 when building FPs --- .../java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 dfc4b84d08..6e64df179c 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -109,7 +109,7 @@ protected Expr makeNumberAndRound(String pN, FloatingPointType pType, Expr pRoun final Rational rat = toRational(pN); final BigInteger upperBound = - getBiggestNumberBeforeInf(pType.getMantissaSizeWithSignBit(), pType.getExponentSize()); + getBiggestNumberBeforeInf(pType.getMantissaSizeWithoutSignBit(), pType.getExponentSize()); if (rat.greater(Rational.fromDecimal(upperBound.negate().toString())) && rat.less(Rational.fromDecimal(upperBound.toString()))) { From eddaf775d40dc7e7ff9180a4bbc754a11b00ccdc Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 13:50:42 +0200 Subject: [PATCH 19/67] Use new FP mantissa getter in CVC4 and remove magic -1 + improve variable name --- .../solvers/cvc4/CVC4FormulaCreator.java | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java index 1dac46d603..2966126b20 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -154,9 +154,8 @@ public FormulaType getFormulaType(T pFormula) { t.isFloatingPoint(), "FloatingPointFormula with actual type %s: %s", t, pFormula); edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(t); return (FormulaType) - FormulaType.getFloatingPointTypeWithoutSignBit( - (int) fpType.getExponentSize(), - (int) fpType.getSignificandSize() - 1); // without sign bit + FormulaType.getFloatingPointTypeWithSignBit( + (int) fpType.getExponentSize(), (int) fpType.getSignificandSize()); // with sign bit } else if (pFormula instanceof ArrayFormula) { FormulaType arrayIndexType = getArrayFormulaIndexType((ArrayFormula) pFormula); @@ -182,9 +181,8 @@ private FormulaType getFormulaTypeFromTermType(Type t) { return FormulaType.getBitvectorTypeWithSize((int) new BitVectorType(t).getSize()); } else if (t.isFloatingPoint()) { edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(t); - return FormulaType.getFloatingPointTypeWithoutSignBit( - (int) fpType.getExponentSize(), - (int) fpType.getSignificandSize() - 1); // without sign bit + return FormulaType.getFloatingPointTypeWithSignBit( + (int) fpType.getExponentSize(), (int) fpType.getSignificandSize()); // with sign bit } else if (t.isRoundingMode()) { return FormulaType.FloatingPointRoundingModeType; } else if (t.isReal()) { @@ -631,7 +629,8 @@ private FloatingPointNumber convertFloatingPoint(Expr fpExpr) { final var fp = fpExpr.getConstFloatingPoint(); final var fpType = fp.getT(); final var expWidth = Ints.checkedCast(fpType.exponentWidth()); - final var mantWidth = Ints.checkedCast(fpType.significandWidth() - 1); // without sign bit + final var mantWidthWithoutSignBit = Ints.checkedCast(fpType.significandWidth() - 1); // without + // sign bit final var sign = matcher.group("sign"); final var exp = matcher.group("exp"); @@ -639,13 +638,13 @@ private FloatingPointNumber convertFloatingPoint(Expr fpExpr) { Preconditions.checkArgument("1".equals(sign) || "0".equals(sign)); Preconditions.checkArgument(exp.length() == expWidth); - Preconditions.checkArgument(mant.length() == mantWidth); + Preconditions.checkArgument(mant.length() == mantWidthWithoutSignBit); return FloatingPointNumber.of( Sign.of(sign.charAt(0) == '1'), new BigInteger(exp, 2), new BigInteger(mant, 2), expWidth, - mantWidth); + mantWidthWithoutSignBit); } } From 1dae5d1083f8adae52f12136e7fee90659c9a6fb Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 13:53:02 +0200 Subject: [PATCH 20/67] Unify constructors of FloatingPointType by delegating to the same method earlier --- src/org/sosy_lab/java_smt/api/FormulaType.java | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index 9d36fe153c..8d23cdbfb7 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -217,7 +217,7 @@ public String toSMTLIBString() { // TODO: mark as soon to be deprecated public static FloatingPointType getFloatingPointType( int exponentSize, int mantissaSizeWithoutSignBit) { - return new FloatingPointType(exponentSize, mantissaSizeWithoutSignBit); + return getFloatingPointTypeWithoutSignBit(exponentSize, mantissaSizeWithoutSignBit); } /** @@ -245,8 +245,7 @@ public static FloatingPointType getFloatingPointTypeWithoutSignBit( */ public static FloatingPointType getFloatingPointTypeWithSignBit( int exponentSize, int mantissaSizeWithSignBit) { - // We save the mantissa without the sign bit internally - return new FloatingPointType(exponentSize, mantissaSizeWithSignBit - 1); + return getFloatingPointTypeWithoutSignBit(exponentSize, mantissaSizeWithSignBit - 1); } /** From 7755fe61056807d4d373df5c0523ae3669a0f27b Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 14:16:13 +0200 Subject: [PATCH 21/67] Use the SMTLIB2 standards interpretation of including the sign bit in the mantissa size of FPs when parsing FP types from strings --- src/org/sosy_lab/java_smt/api/FormulaType.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index 8d23cdbfb7..7d09b3734c 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -552,7 +552,8 @@ public static FormulaType fromString(String t) { } else if (t.startsWith("FloatingPoint<")) { // FloatingPoint List exman = Splitter.on(',').limit(2).splitToList(t.substring(14, t.length() - 1)); - return FormulaType.getFloatingPointTypeWithoutSignBit( + // SMTLIB2 standard expects the sign bit to be part of the mantissa + return FormulaType.getFloatingPointTypeWithSignBit( Integer.parseInt(exman.get(0).substring(4)), Integer.parseInt(exman.get(1).substring(5))); } else if (t.startsWith("Bitvector<")) { // Bitvector<32> From 83cd136875919b18f3ae5602a44ec28d2062920d Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 14:16:46 +0200 Subject: [PATCH 22/67] Add method for total type size in FloatingPointNumber and use it instead of calculating it by hand each time --- .../sosy_lab/java_smt/api/FloatingPointNumber.java | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index 19fdb61182..9daa143165 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -104,6 +104,14 @@ public int getMantissaSizeWithSignBit() { return getMantissaSizeWithoutSignBit() + 1; } + /** + * Returns the size of the precision, i.e. the size of the exponent + the size of the mantissa + * including sign bit. + */ + public int getTotalPrecisionSize() { + return getMantissaSizeWithSignBit() + getExponentSize(); + } + /** * Get a floating-point number with the given sign, exponent, and mantissa. * @@ -246,7 +254,7 @@ private BitSet getBits() { var exponentSize = getExponentSize(); var mantissa = getMantissa(); var exponent = getExponent(); - var bits = new BitSet(exponentSize + mantissaSizeWithoutSign + 1); + var bits = new BitSet(getTotalPrecisionSize()); if (getMathSign().isNegative()) { bits.set(exponentSize + mantissaSizeWithoutSign); // if negative, set first bit to 1 } @@ -265,7 +273,7 @@ private BitSet getBits() { */ @Override public final String toString() { - var length = getExponentSize() + getMantissaSizeWithSignBit(); + var length = getTotalPrecisionSize(); var str = new StringBuilder(length); var bits = getBits(); for (int i = 0; i < length; i++) { From 96a25658d5deb9d282bd2a89870fab9674af8817 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 18:33:54 +0200 Subject: [PATCH 23/67] Rename method for total type size in FloatingPointNumber to getTotalSize() --- src/org/sosy_lab/java_smt/api/FloatingPointNumber.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index 9daa143165..5a6132ecb3 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -108,7 +108,7 @@ public int getMantissaSizeWithSignBit() { * Returns the size of the precision, i.e. the size of the exponent + the size of the mantissa * including sign bit. */ - public int getTotalPrecisionSize() { + public int getTotalSize() { return getMantissaSizeWithSignBit() + getExponentSize(); } @@ -254,7 +254,7 @@ private BitSet getBits() { var exponentSize = getExponentSize(); var mantissa = getMantissa(); var exponent = getExponent(); - var bits = new BitSet(getTotalPrecisionSize()); + var bits = new BitSet(getTotalSize()); if (getMathSign().isNegative()) { bits.set(exponentSize + mantissaSizeWithoutSign); // if negative, set first bit to 1 } @@ -273,7 +273,7 @@ private BitSet getBits() { */ @Override public final String toString() { - var length = getTotalPrecisionSize(); + var length = getTotalSize(); var str = new StringBuilder(length); var bits = getBits(); for (int i = 0; i < length; i++) { From 885bb68297d19ced19484dfa9daaafd40a45097d Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 19:03:06 +0200 Subject: [PATCH 24/67] Add deprecation of both getMantissaSize() methods with reasoning --- src/org/sosy_lab/java_smt/api/FloatingPointNumber.java | 7 ++++++- src/org/sosy_lab/java_smt/api/FormulaType.java | 7 ++++++- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index 5a6132ecb3..b4cf805085 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -84,8 +84,13 @@ public final boolean getSign() { /** * Returns the size of the mantissa (also called a coefficient or significant), excluding the sign * bit. + * + * @deprecated this method can be confusing, as the SMTLIB2 standard expects the mantissa to + * include the sign bit, but this does not. Use {@link #getMantissaSizeWithoutSignBit()} + * instead if you want the mantissa without the sign bit, and {@link + * #getMantissaSizeWithSignBit()} if you want it to include the sign bit. */ - // TODO: mark as soon to be deprecated + @Deprecated(since = "6.0", forRemoval = true) public int getMantissaSize() { return getMantissaSizeWithoutSignBit(); } diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index 7d09b3734c..9b68241e52 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -295,8 +295,13 @@ public int getExponentSize() { /** * Returns the size of the mantissa (also called a coefficient or significant), excluding the * sign bit. + * + * @deprecated this method can be confusing, as the SMTLIB2 standard expects the mantissa to + * include the sign bit, but this does not. Use {@link #getMantissaSizeWithoutSignBit()} + * instead if you want the mantissa without the sign bit, and {@link + * #getMantissaSizeWithSignBit()} if you want it to include the sign bit. */ - // TODO: mark as soon to be deprecated + @Deprecated(since = "6.0", forRemoval = true) public int getMantissaSize() { return mantissaSize; } From 59713feb8ad93a59b50636c41e26834c305fa3d8 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 14:46:22 +0200 Subject: [PATCH 25/67] Revert CVC4 fromIeeeBitvectorImpl() implementation and use new API calls getMantissaSizeWithoutSignBit() and getTotalSize() --- .../cvc4/CVC4FloatingPointFormulaManager.java | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 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 6e64df179c..1f4423c2b0 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.BitVector; +import edu.stanford.CVC4.BitVectorExtract; import edu.stanford.CVC4.Expr; import edu.stanford.CVC4.ExprManager; import edu.stanford.CVC4.FloatingPoint; @@ -358,10 +359,19 @@ protected Expr isNegative(Expr pParam) { @Override protected Expr fromIeeeBitvectorImpl(Expr bitvector, FloatingPointType pTargetType) { - // This is just named weird, but the CVC4 doc say this is IEEE BV -> FP - FloatingPointConvertSort fpConvertSort = new FloatingPointConvertSort(getFPSize(pTargetType)); - Expr op = exprManager.mkConst(new FloatingPointToFPIEEEBitVector(fpConvertSort)); - return exprManager.mkExpr(op, bitvector); + int mantissaSize = pTargetType.getMantissaSizeWithoutSignBit(); + int size = pTargetType.getTotalSize(); + assert size == pTargetType.getTotalSize(); + + Expr signExtract = exprManager.mkConst(new BitVectorExtract(size - 1, size - 1)); + Expr exponentExtract = exprManager.mkConst(new BitVectorExtract(size - 2, mantissaSize)); + Expr mantissaExtract = exprManager.mkConst(new BitVectorExtract(mantissaSize - 1, 0)); + + Expr sign = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, signExtract, bitvector); + Expr exponent = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, exponentExtract, bitvector); + Expr mantissa = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, mantissaExtract, bitvector); + + return exprManager.mkExpr(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa); } @Override From 05b6c405a1c395fb0daa499b850713e0827a89c8 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 14:46:55 +0200 Subject: [PATCH 26/67] Revert AbstractFloatingPointFormulaManager toIeeeBitvectorImpl() to previous implementation --- .../basicimpl/AbstractFloatingPointFormulaManager.java | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 5082f24634..47c847afe2 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -256,12 +256,7 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula pNumber) { return getFormulaCreator().encapsulateBitvector(toIeeeBitvectorImpl(extractInfo(pNumber))); } - @SuppressWarnings("unused") - protected TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber) { - throw new UnsupportedOperationException( - "Solver does not support transformation from " - + "floating-point numbers to IEEE bitvector"); - } + protected abstract TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber); @Override public FloatingPointFormula negate(FloatingPointFormula pNumber) { From a08a81120d6b66b7b3de7f1dfbe7c617502f1f12 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 14:52:02 +0200 Subject: [PATCH 27/67] Revert CVC4 toIeeeBitvectorImpl() to previous implementation and fix assertion error in fromIeeeBitvectorImpl() --- .../cvc4/CVC4FloatingPointFormulaManager.java | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 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 1f4423c2b0..ec3103a7a5 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -17,7 +17,6 @@ import edu.stanford.CVC4.FloatingPointConvertSort; import edu.stanford.CVC4.FloatingPointSize; import edu.stanford.CVC4.FloatingPointToFPFloatingPoint; -import edu.stanford.CVC4.FloatingPointToFPIEEEBitVector; import edu.stanford.CVC4.FloatingPointToFPSignedBitVector; import edu.stanford.CVC4.FloatingPointToFPUnsignedBitVector; import edu.stanford.CVC4.FloatingPointToSBV; @@ -358,22 +357,29 @@ protected Expr isNegative(Expr pParam) { } @Override - protected Expr fromIeeeBitvectorImpl(Expr bitvector, FloatingPointType pTargetType) { + protected Expr fromIeeeBitvectorImpl(Expr pBitvector, FloatingPointType pTargetType) { int mantissaSize = pTargetType.getMantissaSizeWithoutSignBit(); int size = pTargetType.getTotalSize(); - assert size == pTargetType.getTotalSize(); + assert size == pTargetType.getMantissaSizeWithoutSignBit() + pTargetType.getExponentSize(); Expr signExtract = exprManager.mkConst(new BitVectorExtract(size - 1, size - 1)); Expr exponentExtract = exprManager.mkConst(new BitVectorExtract(size - 2, mantissaSize)); Expr mantissaExtract = exprManager.mkConst(new BitVectorExtract(mantissaSize - 1, 0)); - Expr sign = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, signExtract, bitvector); - Expr exponent = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, exponentExtract, bitvector); - Expr mantissa = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, mantissaExtract, bitvector); + Expr sign = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, signExtract, pBitvector); + Expr exponent = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, exponentExtract, pBitvector); + Expr mantissa = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, mantissaExtract, pBitvector); return exprManager.mkExpr(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa); } + @Override + protected Expr toIeeeBitvectorImpl(Expr pNumber) { + // TODO possible work-around: use a tmp-variable "TMP" and add an + // additional constraint "pNumer == fromIeeeBitvectorImpl(TMP)" for it in all use-cases. + throw new UnsupportedOperationException("FP to IEEE-BV is not supported"); + } + @Override protected Expr round(Expr pFormula, FloatingPointRoundingMode pRoundingMode) { return exprManager.mkExpr(Kind.FLOATINGPOINT_RTI, getRoundingModeImpl(pRoundingMode), pFormula); From a2a7810747043dcb2c164715bbe0509a93f80130 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 14:52:32 +0200 Subject: [PATCH 28/67] Revert CVC5 toIeeeBitvectorImpl() and fromIeeeBitvectorImpl() to previous implementation and use new API for mantissa --- .../cvc5/CVC5FloatingPointFormulaManager.java | 35 ++++++++++++++----- 1 file changed, 27 insertions(+), 8 deletions(-) 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 9493b754ff..d70c0e720c 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -410,16 +410,35 @@ protected Term isNegative(Term pParam) { @Override protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetType) { + int mantissaSize = pTargetType.getMantissaSizeWithoutSignBit(); + int size = pTargetType.getTotalSize(); + assert size == pTargetType.getMantissaSizeWithoutSignBit() + pTargetType.getExponentSize(); + + Op signExtract; + Op exponentExtract; + Op mantissaExtract; try { - return termManager.mkTerm( - termManager.mkOp( - Kind.FLOATINGPOINT_TO_FP_FROM_IEEE_BV, - pTargetType.getExponentSize(), - pTargetType.getMantissaSizeWithSignBit()), - pBitvector); - } catch (CVC5ApiException pE) { - throw new RuntimeException(pE); + signExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 1, size - 1); + exponentExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 2, mantissaSize); + mantissaExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, mantissaSize - 1, 0); + } catch (CVC5ApiException e) { + throw new IllegalArgumentException( + "You tried creating a invalid bitvector extract in term " + pBitvector + ".", e); } + + Term sign = termManager.mkTerm(signExtract, pBitvector); + Term exponent = termManager.mkTerm(exponentExtract, pBitvector); + Term mantissa = termManager.mkTerm(mantissaExtract, pBitvector); + + return termManager.mkTerm(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa); + } + + @Override + protected Term toIeeeBitvectorImpl(Term pNumber) { + // TODO possible work-around: use a tmp-variable "TMP" and add an + // additional constraint "pNumer == fromIeeeBitvectorImpl(TMP)" for it in all use-cases. + // --> This has to be done on user-side, not in JavaSMT. + throw new UnsupportedOperationException("FP to IEEE-BV is not supported"); } @Override From f37786e73563d6bf91e0a16ec635c2467a1d0464 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 15:26:00 +0200 Subject: [PATCH 29/67] Fix error in assertion in CVC5 fromIeeeBitvectorImpl() --- .../solvers/cvc5/CVC5FloatingPointFormulaManager.java | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) 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 d70c0e720c..de2da7739f 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -410,17 +410,18 @@ protected Term isNegative(Term pParam) { @Override protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetType) { - int mantissaSize = pTargetType.getMantissaSizeWithoutSignBit(); + int mantissaSizeWithoutSignBit = pTargetType.getMantissaSizeWithoutSignBit(); int size = pTargetType.getTotalSize(); - assert size == pTargetType.getMantissaSizeWithoutSignBit() + pTargetType.getExponentSize(); + assert size == mantissaSizeWithoutSignBit + pTargetType.getExponentSize(); Op signExtract; Op exponentExtract; Op mantissaExtract; try { signExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 1, size - 1); - exponentExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 2, mantissaSize); - mantissaExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, mantissaSize - 1, 0); + exponentExtract = + termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 2, mantissaSizeWithoutSignBit); + mantissaExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, mantissaSizeWithoutSignBit - 1, 0); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid bitvector extract in term " + pBitvector + ".", e); From 0bd0aa7ca8532576d8396da40ae0450947696a08 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 15:26:06 +0200 Subject: [PATCH 30/67] Fix error in assertion in CVC4 fromIeeeBitvectorImpl() --- .../solvers/cvc4/CVC4FloatingPointFormulaManager.java | 10 ++++++---- 1 file changed, 6 insertions(+), 4 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 ec3103a7a5..43a6797233 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -358,13 +358,15 @@ protected Expr isNegative(Expr pParam) { @Override protected Expr fromIeeeBitvectorImpl(Expr pBitvector, FloatingPointType pTargetType) { - int mantissaSize = pTargetType.getMantissaSizeWithoutSignBit(); + int mantissaSizeWithoutSignBit = pTargetType.getMantissaSizeWithoutSignBit(); int size = pTargetType.getTotalSize(); - assert size == pTargetType.getMantissaSizeWithoutSignBit() + pTargetType.getExponentSize(); + assert size == mantissaSizeWithoutSignBit + pTargetType.getExponentSize(); Expr signExtract = exprManager.mkConst(new BitVectorExtract(size - 1, size - 1)); - Expr exponentExtract = exprManager.mkConst(new BitVectorExtract(size - 2, mantissaSize)); - Expr mantissaExtract = exprManager.mkConst(new BitVectorExtract(mantissaSize - 1, 0)); + Expr exponentExtract = + exprManager.mkConst(new BitVectorExtract(size - 2, mantissaSizeWithoutSignBit)); + Expr mantissaExtract = + exprManager.mkConst(new BitVectorExtract(mantissaSizeWithoutSignBit - 1, 0)); Expr sign = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, signExtract, pBitvector); Expr exponent = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, exponentExtract, pBitvector); From 7331cd128a22d563a48a914763c7c08da923ff4a Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 15:26:50 +0200 Subject: [PATCH 31/67] Add method to check the availability of native FP to BV in tests --- src/org/sosy_lab/java_smt/test/SolverBasedTest0.java | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index e96c7b39f1..df28a06069 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -254,6 +254,17 @@ protected final void requireFPToBitvector() { } } + @SuppressWarnings("CheckReturnValue") + protected final boolean solverSupportsNativeFPToBitvector() { + requireFloats(); + try { + fpmgr.toIeeeBitvector(fpmgr.makeNumber(0, getSinglePrecisionFloatingPointType())); + return true; + } catch (UnsupportedOperationException e) { + return false; + } + } + /** Skip test if the solver does not support quantifiers. */ protected final void requireQuantifiers() { assume() From 031a90087ff5cc56ba3f5afb70da5f93bdf950fe Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 15:45:17 +0200 Subject: [PATCH 32/67] Fix CVC4/5 size assertion in fromIeeeBitvectorImpl() again :D --- .../java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java | 3 ++- .../java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java | 3 ++- 2 files changed, 4 insertions(+), 2 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 43a6797233..ca1427d92c 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -360,7 +360,8 @@ protected Expr isNegative(Expr pParam) { protected Expr fromIeeeBitvectorImpl(Expr pBitvector, FloatingPointType pTargetType) { int mantissaSizeWithoutSignBit = pTargetType.getMantissaSizeWithoutSignBit(); int size = pTargetType.getTotalSize(); - assert size == mantissaSizeWithoutSignBit + pTargetType.getExponentSize(); + // total size = mantissa without sign bit + sign bit + exponent + assert size == mantissaSizeWithoutSignBit + 1 + pTargetType.getExponentSize(); Expr signExtract = exprManager.mkConst(new BitVectorExtract(size - 1, size - 1)); Expr exponentExtract = 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 de2da7739f..6dfb19b9bb 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -412,7 +412,8 @@ protected Term isNegative(Term pParam) { protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetType) { int mantissaSizeWithoutSignBit = pTargetType.getMantissaSizeWithoutSignBit(); int size = pTargetType.getTotalSize(); - assert size == mantissaSizeWithoutSignBit + pTargetType.getExponentSize(); + // total size = mantissa without sign bit + sign bit + exponent + assert size == mantissaSizeWithoutSignBit + 1 + pTargetType.getExponentSize(); Op signExtract; Op exponentExtract; From 3d178115a1df089f7fb3321b728fc28cca21cca0 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 15:51:46 +0200 Subject: [PATCH 33/67] Add FP tests for mantissa size with and without sign bit, as well as the correct BV interpretation of the type/size --- .../test/FloatingPointFormulaManagerTest.java | 196 ++++++++++++++++++ 1 file changed, 196 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 79f4afbbfe..c4ac0d8f34 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -33,6 +33,7 @@ import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign; import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; import org.sosy_lab.java_smt.api.Model; @@ -1228,6 +1229,201 @@ public void fpModelValue() throws SolverException, InterruptedException { } } + // The standard defines the mantissa such that it includes the sign bit, and mantissa + + // exponent equal the total size. This test checks this, + that it holds with to/from IEEE + // bitvector + @Test + public void floatingPointMantissaSignBitWithBitvectorInterpretationSinglePrecision() { + int bvSize32 = singlePrecType.getTotalSize(); + BitvectorFormula bvNumber32 = bvmgr.makeBitvector(bvSize32, BigInteger.ZERO); + // Sanity checks + assertThat(bvSize32).isEqualTo(32); + assertThat(singlePrecType.getExponentSize()).isEqualTo(8); + assertThat(singlePrecType.getMantissaSizeWithoutSignBit()).isEqualTo(23); + assertThat(singlePrecType.getMantissaSizeWithSignBit()).isEqualTo(24); + assertThat(bvmgr.getLength(bvNumber32)).isEqualTo(bvSize32); + assertThat(mgr.getFormulaType(bvNumber32).isBitvectorType()).isTrue(); + assertThat(((BitvectorType) mgr.getFormulaType(bvNumber32)).getSize()).isEqualTo(bvSize32); + + // Transform the BV to FP and check that it conforms to the precision used + FloatingPointFormula bvToFpSinglePrec = fpmgr.fromIeeeBitvector(bvNumber32, singlePrecType); + assertThat(mgr.getFormulaType(bvToFpSinglePrec).isFloatingPointType()).isTrue(); + assertThat(((FloatingPointType) mgr.getFormulaType(bvToFpSinglePrec)).getTotalSize()) + .isEqualTo(singlePrecType.getTotalSize()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpSinglePrec)).getMantissaSizeWithSignBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithSignBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpSinglePrec)) + .getMantissaSizeWithoutSignBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithoutSignBit()); + assertThat(((FloatingPointType) mgr.getFormulaType(bvToFpSinglePrec)).getExponentSize()) + .isEqualTo(singlePrecType.getExponentSize()); + + // The same as above, but build the precision by hand with the different APIs + FloatingPointType fpTypeWithSignBit = + FloatingPointType.getFloatingPointTypeWithSignBit( + singlePrecType.getExponentSize(), singlePrecType.getMantissaSizeWithSignBit()); + FloatingPointType fpTypeWithoutSignBit = + FloatingPointType.getFloatingPointTypeWithoutSignBit( + singlePrecType.getExponentSize(), singlePrecType.getMantissaSizeWithoutSignBit()); + assertThat(fpTypeWithSignBit).isEqualTo(singlePrecType); + assertThat(fpTypeWithoutSignBit).isEqualTo(singlePrecType); + + FloatingPointFormula bvToFpfpTypeWithSignBit = + fpmgr.fromIeeeBitvector(bvNumber32, fpTypeWithSignBit); + assertThat(mgr.getFormulaType(bvToFpfpTypeWithSignBit).isFloatingPointType()).isTrue(); + assertThat(((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)).getTotalSize()) + .isEqualTo(singlePrecType.getTotalSize()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)) + .getMantissaSizeWithSignBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithSignBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)) + .getMantissaSizeWithoutSignBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithoutSignBit()); + assertThat(((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)).getExponentSize()) + .isEqualTo(singlePrecType.getExponentSize()); + + FloatingPointFormula bvToFpfpTypeWithoutSignBit = + fpmgr.fromIeeeBitvector(bvNumber32, fpTypeWithoutSignBit); + assertThat(mgr.getFormulaType(bvToFpfpTypeWithoutSignBit).isFloatingPointType()).isTrue(); + assertThat(((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)).getTotalSize()) + .isEqualTo(singlePrecType.getTotalSize()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)) + .getMantissaSizeWithSignBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithSignBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)) + .getMantissaSizeWithoutSignBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithoutSignBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)).getExponentSize()) + .isEqualTo(singlePrecType.getExponentSize()); + + if (solverSupportsNativeFPToBitvector()) { + BitvectorFormula bvToFpSinglePrecToBv = fpmgr.toIeeeBitvector(bvToFpSinglePrec); + assertThat(bvmgr.getLength(bvToFpSinglePrecToBv)).isEqualTo(bvSize32); + + BitvectorFormula bvToFpTypeWithSignBitToBv = fpmgr.toIeeeBitvector(bvToFpfpTypeWithSignBit); + assertThat(bvmgr.getLength(bvToFpTypeWithSignBitToBv)).isEqualTo(bvSize32); + + BitvectorFormula bvToFpTypeWithoutSignBitToBv = + fpmgr.toIeeeBitvector(bvToFpfpTypeWithoutSignBit); + assertThat(bvmgr.getLength(bvToFpTypeWithoutSignBitToBv)).isEqualTo(bvSize32); + + assume() + .withMessage("Bitwuzla equals on FPs/terms has a problem that needs to be addressed " + + "first") + .that(solver) + .isNotEqualTo(Solvers.BITWUZLA); + + assertThat(bvToFpSinglePrecToBv).isEqualTo(bvNumber32); + assertThat(bvToFpTypeWithSignBitToBv).isEqualTo(bvNumber32); + assertThat(bvToFpTypeWithoutSignBitToBv).isEqualTo(bvNumber32); + } + } + + // The standard defines the mantissa such that it includes the sign bit, and mantissa + + // exponent equal the total size. This test checks this, + that it holds with to/from IEEE + // bitvector + @Test + public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecision() { + int bvSize64 = doublePrecType.getTotalSize(); + BitvectorFormula bvNumberSize64 = bvmgr.makeBitvector(bvSize64, BigInteger.ZERO); + // Sanity checks + assertThat(bvSize64).isEqualTo(64); + assertThat(doublePrecType.getExponentSize()).isEqualTo(11); + assertThat(doublePrecType.getMantissaSizeWithoutSignBit()).isEqualTo(52); + assertThat(doublePrecType.getMantissaSizeWithSignBit()).isEqualTo(53); + assertThat(bvmgr.getLength(bvNumberSize64)).isEqualTo(bvSize64); + assertThat(mgr.getFormulaType(bvNumberSize64).isBitvectorType()).isTrue(); + assertThat(((BitvectorType) mgr.getFormulaType(bvNumberSize64)).getSize()).isEqualTo(bvSize64); + + // Transform the BV to FP and check that it conforms to the precision used + FloatingPointFormula bvToFpDoublePrec = fpmgr.fromIeeeBitvector(bvNumberSize64, doublePrecType); + assertThat(mgr.getFormulaType(bvToFpDoublePrec).isFloatingPointType()).isTrue(); + assertThat(((FloatingPointType) mgr.getFormulaType(bvToFpDoublePrec)).getTotalSize()) + .isEqualTo(doublePrecType.getTotalSize()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpDoublePrec)).getMantissaSizeWithSignBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithSignBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpDoublePrec)) + .getMantissaSizeWithoutSignBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithoutSignBit()); + assertThat(((FloatingPointType) mgr.getFormulaType(bvToFpDoublePrec)).getExponentSize()) + .isEqualTo(doublePrecType.getExponentSize()); + + // The same as above, but build the precision by hand with the different APIs + FloatingPointType fpTypeWithSignBit = + FloatingPointType.getFloatingPointTypeWithSignBit( + doublePrecType.getExponentSize(), doublePrecType.getMantissaSizeWithSignBit()); + FloatingPointType fpTypeWithoutSignBit = + FloatingPointType.getFloatingPointTypeWithoutSignBit( + doublePrecType.getExponentSize(), doublePrecType.getMantissaSizeWithoutSignBit()); + assertThat(fpTypeWithSignBit).isEqualTo(doublePrecType); + assertThat(fpTypeWithoutSignBit).isEqualTo(doublePrecType); + + FloatingPointFormula bvToFpfpTypeWithSignBit = + fpmgr.fromIeeeBitvector(bvNumberSize64, fpTypeWithSignBit); + assertThat(mgr.getFormulaType(bvToFpfpTypeWithSignBit).isFloatingPointType()).isTrue(); + assertThat(((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)).getTotalSize()) + .isEqualTo(doublePrecType.getTotalSize()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)) + .getMantissaSizeWithSignBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithSignBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)) + .getMantissaSizeWithoutSignBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithoutSignBit()); + assertThat(((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)).getExponentSize()) + .isEqualTo(doublePrecType.getExponentSize()); + + FloatingPointFormula bvToFpfpTypeWithoutSignBit = + fpmgr.fromIeeeBitvector(bvNumberSize64, fpTypeWithoutSignBit); + assertThat(mgr.getFormulaType(bvToFpfpTypeWithoutSignBit).isFloatingPointType()).isTrue(); + assertThat(((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)).getTotalSize()) + .isEqualTo(doublePrecType.getTotalSize()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)) + .getMantissaSizeWithSignBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithSignBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)) + .getMantissaSizeWithoutSignBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithoutSignBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)).getExponentSize()) + .isEqualTo(doublePrecType.getExponentSize()); + + if (solverSupportsNativeFPToBitvector()) { + BitvectorFormula bvToFpDoublePrecToBv = fpmgr.toIeeeBitvector(bvToFpDoublePrec); + assertThat(bvmgr.getLength(bvToFpDoublePrecToBv)).isEqualTo(bvSize64); + + + BitvectorFormula bvToFpTypeWithSignBitToBv = fpmgr.toIeeeBitvector(bvToFpfpTypeWithSignBit); + assertThat(bvmgr.getLength(bvToFpTypeWithSignBitToBv)).isEqualTo(bvSize64); + + BitvectorFormula bvToFpTypeWithoutSignBitToBv = + fpmgr.toIeeeBitvector(bvToFpfpTypeWithoutSignBit); + assertThat(bvmgr.getLength(bvToFpTypeWithoutSignBitToBv)).isEqualTo(bvSize64); + + assume() + .withMessage("Bitwuzla equals on FPs/terms has a problem that needs to be addressed " + + "first") + .that(solver) + .isNotEqualTo(Solvers.BITWUZLA); + + assertThat(bvToFpTypeWithSignBitToBv).isEqualTo(bvNumberSize64); + assertThat(bvToFpDoublePrecToBv).isEqualTo(bvNumberSize64); + assertThat(bvToFpTypeWithoutSignBitToBv).isEqualTo(bvNumberSize64); + } + } + @Test @SuppressWarnings({"unchecked", "resource"}) public void fpInterpolation() throws SolverException, InterruptedException { From 55089a046eccadff63630458136c4957ae7760bd Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 16:41:02 +0200 Subject: [PATCH 34/67] Improve constructor naming for FormulaType.FloatingPointType to better show the mantissa does or does not expect the sign bit to be included --- .../sosy_lab/java_smt/api/FormulaType.java | 16 +++-- .../bitwuzla/BitwuzlaFormulaCreator.java | 4 +- .../solvers/cvc4/CVC4FormulaCreator.java | 4 +- .../solvers/cvc5/CVC5FormulaCreator.java | 2 +- .../mathsat5/Mathsat5FormulaCreator.java | 2 +- .../z3/Z3FloatingPointFormulaManager.java | 2 +- .../java_smt/solvers/z3/Z3FormulaCreator.java | 2 +- .../test/FloatingPointFormulaManagerTest.java | 66 ++++++++++--------- .../java_smt/test/SolverVisitorTest.java | 6 +- 9 files changed, 57 insertions(+), 47 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index 9b68241e52..b1f1ebb0b2 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -217,35 +217,37 @@ public String toSMTLIBString() { // TODO: mark as soon to be deprecated public static FloatingPointType getFloatingPointType( int exponentSize, int mantissaSizeWithoutSignBit) { - return getFloatingPointTypeWithoutSignBit(exponentSize, mantissaSizeWithoutSignBit); + return getFloatingPointTypeFromSizesWithoutSignBit(exponentSize, mantissaSizeWithoutSignBit); } /** * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes. - * The mantissa size is expected to not include the sign bit. + * The mantissa size is expected to not include the sign bit. The total size is therefore equal to + * mantissa + exponent + 1. * * @param exponentSize size of the exponent for the base of the floating-point * @param mantissaSizeWithoutSignBit size of the mantissa (also called a coefficient or * significant), excluding the sign bit. * @return the newly constructed {@link FloatingPointType}. */ - public static FloatingPointType getFloatingPointTypeWithoutSignBit( + public static FloatingPointType getFloatingPointTypeFromSizesWithoutSignBit( int exponentSize, int mantissaSizeWithoutSignBit) { return new FloatingPointType(exponentSize, mantissaSizeWithoutSignBit); } /** * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes. - * The mantissa size is expected to not include the sign bit. + * The mantissa size is expected to include the sign bit. The total size is therefore equal to + * mantissa + exponent. * * @param exponentSize size of the exponent for the base of the floating-point * @param mantissaSizeWithSignBit size of the mantissa (also called a coefficient or significant), * including the sign bit. * @return the newly constructed {@link FloatingPointType}. */ - public static FloatingPointType getFloatingPointTypeWithSignBit( + public static FloatingPointType getFloatingPointTypeFromSizesWithSignBit( int exponentSize, int mantissaSizeWithSignBit) { - return getFloatingPointTypeWithoutSignBit(exponentSize, mantissaSizeWithSignBit - 1); + return getFloatingPointTypeFromSizesWithoutSignBit(exponentSize, mantissaSizeWithSignBit - 1); } /** @@ -558,7 +560,7 @@ public static FormulaType fromString(String t) { // FloatingPoint List exman = Splitter.on(',').limit(2).splitToList(t.substring(14, t.length() - 1)); // SMTLIB2 standard expects the sign bit to be part of the mantissa - return FormulaType.getFloatingPointTypeWithSignBit( + return FormulaType.getFloatingPointTypeFromSizesWithSignBit( Integer.parseInt(exman.get(0).substring(4)), Integer.parseInt(exman.get(1).substring(5))); } else if (t.startsWith("Bitvector<")) { // Bitvector<32> diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index fd5c82d284..48c3de8a78 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -171,7 +171,7 @@ public FormulaType bitwuzlaSortToType(Sort pSort) { if (pSort.is_fp()) { int exponent = pSort.fp_exp_size(); int mantissa = pSort.fp_sig_size() - 1; - return FormulaType.getFloatingPointTypeWithoutSignBit(exponent, mantissa); + return FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(exponent, mantissa); } else if (pSort.is_bv()) { return FormulaType.getBitvectorTypeWithSize(pSort.bv_size()); } else if (pSort.is_array()) { @@ -380,7 +380,7 @@ public FormulaType getFormulaType(T pFormula) { } int exp = sort.fp_exp_size(); int man = sort.fp_sig_size() - 1; - return (FormulaType) FormulaType.getFloatingPointTypeWithoutSignBit(exp, man); + return (FormulaType) FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(exp, man); } else if (sort.is_rm()) { return (FormulaType) FormulaType.FloatingPointRoundingModeType; } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java index 2966126b20..e62c78a99c 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -154,7 +154,7 @@ public FormulaType getFormulaType(T pFormula) { t.isFloatingPoint(), "FloatingPointFormula with actual type %s: %s", t, pFormula); edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(t); return (FormulaType) - FormulaType.getFloatingPointTypeWithSignBit( + FormulaType.getFloatingPointTypeFromSizesWithSignBit( (int) fpType.getExponentSize(), (int) fpType.getSignificandSize()); // with sign bit } else if (pFormula instanceof ArrayFormula) { @@ -181,7 +181,7 @@ private FormulaType getFormulaTypeFromTermType(Type t) { return FormulaType.getBitvectorTypeWithSize((int) new BitVectorType(t).getSize()); } else if (t.isFloatingPoint()) { edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(t); - return FormulaType.getFloatingPointTypeWithSignBit( + return FormulaType.getFloatingPointTypeFromSizesWithSignBit( (int) fpType.getExponentSize(), (int) fpType.getSignificandSize()); // with sign bit } else if (t.isRoundingMode()) { return FormulaType.FloatingPointRoundingModeType; diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java index 381daa2a29..177629cbbf 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -224,7 +224,7 @@ private FormulaType getFormulaTypeFromTermType(Sort sort) { return FormulaType.getBitvectorTypeWithSize(sort.getBitVectorSize()); } else if (sort.isFloatingPoint()) { // CVC5 wants the sign bit as part of the mantissa. We add that manually in creation. - return FormulaType.getFloatingPointTypeWithoutSignBit( + return FormulaType.getFloatingPointTypeFromSizesWithoutSignBit( sort.getFloatingPointExponentSize(), sort.getFloatingPointSignificandSize() - 1); } else if (sort.isRoundingMode()) { return FormulaType.FloatingPointRoundingModeType; diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java index b836c212da..d2c20cf938 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -214,7 +214,7 @@ private FormulaType getFormulaTypeFromTermType(Long type) { } else if (msat_is_bv_type(env, type)) { return FormulaType.getBitvectorTypeWithSize(msat_get_bv_type_size(env, type)); } else if (msat_is_fp_type(env, type)) { - return FormulaType.getFloatingPointTypeWithoutSignBit( + return FormulaType.getFloatingPointTypeFromSizesWithoutSignBit( msat_get_fp_type_exp_width(env, type), msat_get_fp_type_mant_width(env, type)); } else if (msat_is_fp_roundingmode_type(env, type)) { return FormulaType.FloatingPointRoundingModeType; 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 39079464aa..e1f2e0bd42 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java @@ -21,7 +21,7 @@ class Z3FloatingPointFormulaManager extends AbstractFloatingPointFormulaManager { private static final FloatingPointType highPrec = - FormulaType.getFloatingPointTypeWithoutSignBit(15, 112); + FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(15, 112); private final long z3context; private final long roundingMode; diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java index e5e8eb0dae..30dec36188 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -242,7 +242,7 @@ public FormulaType getFormulaTypeFromSort(Long pSort) { return FormulaType.getArrayType( getFormulaTypeFromSort(domainSort), getFormulaTypeFromSort(rangeSort)); case Z3_FLOATING_POINT_SORT: - return FormulaType.getFloatingPointTypeWithoutSignBit( + return FormulaType.getFloatingPointTypeFromSizesWithoutSignBit( Native.fpaGetEbits(z3context, pSort), Native.fpaGetSbits(z3context, pSort) - 1); case Z3_ROUNDING_MODE_SORT: return FormulaType.FloatingPointRoundingModeType; diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index c4ac0d8f34..8bf6479773 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -76,7 +76,7 @@ public void init() { @Test public void floatingPointType() { - FloatingPointType type = FormulaType.getFloatingPointTypeWithoutSignBit(23, 42); + FloatingPointType type = FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(23, 42); FloatingPointFormula var = fpmgr.makeVariable("x", type); FloatingPointType result = (FloatingPointType) mgr.getFormulaType(var); @@ -259,7 +259,9 @@ public void fpRemainderNormal() throws SolverException, InterruptedException { for (FloatingPointType prec : new FloatingPointType[] { - singlePrecType, doublePrecType, FormulaType.getFloatingPointTypeWithoutSignBit(5, 6), + singlePrecType, + doublePrecType, + FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(5, 6), }) { final FloatingPointFormula numFive = fpmgr.makeNumber(5, prec); @@ -283,7 +285,9 @@ public void fpRemainderSpecial() throws SolverException, InterruptedException { for (FloatingPointType prec : new FloatingPointType[] { - singlePrecType, doublePrecType, FormulaType.getFloatingPointTypeWithoutSignBit(5, 6), + singlePrecType, + doublePrecType, + FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(5, 6), }) { final FloatingPointFormula num = fpmgr.makeNumber(42, prec); @@ -537,7 +541,7 @@ public void numberConstants() throws SolverException, InterruptedException { checkEqualityOfNumberConstantsFor(3.4028234663852886e+38, doublePrecType); // check unequality for large types - FloatingPointType nearDouble = FormulaType.getFloatingPointTypeWithoutSignBit(12, 52); + FloatingPointType nearDouble = FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(12, 52); FloatingPointFormula h1 = fpmgr.makeNumber(BigDecimal.TEN.pow(309).multiply(BigDecimal.valueOf(1.0001)), nearDouble); FloatingPointFormula h2 = @@ -545,7 +549,7 @@ public void numberConstants() throws SolverException, InterruptedException { assertThatFormula(fpmgr.equalWithFPSemantics(h1, h2)).isUnsatisfiable(); // check equality for short types - FloatingPointType smallType = FormulaType.getFloatingPointTypeWithoutSignBit(4, 4); + FloatingPointType smallType = FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(4, 4); FloatingPointFormula i1 = fpmgr.makeNumber(BigDecimal.TEN.pow(50).multiply(BigDecimal.valueOf(1.001)), smallType); FloatingPointFormula i2 = @@ -574,7 +578,7 @@ public void numberConstants() throws SolverException, InterruptedException { assertThatFormula(fpmgr.isNegative(ni2)).isTautological(); // check equality for short types - FloatingPointType smallType2 = FormulaType.getFloatingPointTypeWithoutSignBit(4, 4); + FloatingPointType smallType2 = FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(4, 4); FloatingPointFormula j1 = fpmgr.makeNumber(BigDecimal.TEN.pow(500).multiply(BigDecimal.valueOf(1.001)), smallType2); FloatingPointFormula j2 = @@ -605,7 +609,8 @@ public void numberConstants() throws SolverException, InterruptedException { // Z3 supports at least FloatingPointType(15, 112). Larger types seem to be rounded. if (!ImmutableSet.of(Solvers.Z3, Solvers.CVC4).contains(solver)) { // check unequality for very large types - FloatingPointType largeType = FormulaType.getFloatingPointTypeWithoutSignBit(100, 100); + FloatingPointType largeType = + FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(100, 100); FloatingPointFormula k1 = fpmgr.makeNumber(BigDecimal.TEN.pow(200).multiply(BigDecimal.valueOf(1.001)), largeType); FloatingPointFormula k2 = @@ -642,7 +647,8 @@ public void numberConstantsNearInf() throws SolverException, InterruptedExceptio private void checkNearInf(int mantissa, int exponent, long value) throws SolverException, InterruptedException { - FloatingPointType type = FormulaType.getFloatingPointTypeWithoutSignBit(exponent, mantissa); + FloatingPointType type = + FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(exponent, mantissa); FloatingPointFormula fp1 = fpmgr.makeNumber(BigDecimal.valueOf(value), type); assertThatFormula(fpmgr.isInfinity(fp1)).isTautological(); FloatingPointFormula fp2 = fpmgr.makeNumber(BigDecimal.valueOf(value - 1), type); @@ -677,7 +683,8 @@ public void numberConstantsNearMinusInf() throws SolverException, InterruptedExc private void checkNearMinusInf(int mantissa, int exponent, long value) throws SolverException, InterruptedException { - FloatingPointType type = FormulaType.getFloatingPointTypeWithoutSignBit(exponent, mantissa); + FloatingPointType type = + FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(exponent, mantissa); FloatingPointFormula fp1 = fpmgr.makeNumber(BigDecimal.valueOf(value), type); assertThatFormula(fpmgr.isInfinity(fp1)).isTautological(); FloatingPointFormula fp2 = fpmgr.makeNumber(BigDecimal.valueOf(value + 1), type); @@ -1262,10 +1269,10 @@ public void floatingPointMantissaSignBitWithBitvectorInterpretationSinglePrecisi // The same as above, but build the precision by hand with the different APIs FloatingPointType fpTypeWithSignBit = - FloatingPointType.getFloatingPointTypeWithSignBit( + FloatingPointType.getFloatingPointTypeFromSizesWithSignBit( singlePrecType.getExponentSize(), singlePrecType.getMantissaSizeWithSignBit()); FloatingPointType fpTypeWithoutSignBit = - FloatingPointType.getFloatingPointTypeWithoutSignBit( + FloatingPointType.getFloatingPointTypeFromSizesWithoutSignBit( singlePrecType.getExponentSize(), singlePrecType.getMantissaSizeWithoutSignBit()); assertThat(fpTypeWithSignBit).isEqualTo(singlePrecType); assertThat(fpTypeWithoutSignBit).isEqualTo(singlePrecType); @@ -1315,8 +1322,8 @@ public void floatingPointMantissaSignBitWithBitvectorInterpretationSinglePrecisi assertThat(bvmgr.getLength(bvToFpTypeWithoutSignBitToBv)).isEqualTo(bvSize32); assume() - .withMessage("Bitwuzla equals on FPs/terms has a problem that needs to be addressed " - + "first") + .withMessage( + "Bitwuzla equals on FPs/terms has a problem that needs to be addressed " + "first") .that(solver) .isNotEqualTo(Solvers.BITWUZLA); @@ -1348,21 +1355,21 @@ public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecisi assertThat(((FloatingPointType) mgr.getFormulaType(bvToFpDoublePrec)).getTotalSize()) .isEqualTo(doublePrecType.getTotalSize()); assertThat( - ((FloatingPointType) mgr.getFormulaType(bvToFpDoublePrec)).getMantissaSizeWithSignBit()) + ((FloatingPointType) mgr.getFormulaType(bvToFpDoublePrec)).getMantissaSizeWithSignBit()) .isEqualTo(doublePrecType.getMantissaSizeWithSignBit()); assertThat( - ((FloatingPointType) mgr.getFormulaType(bvToFpDoublePrec)) - .getMantissaSizeWithoutSignBit()) + ((FloatingPointType) mgr.getFormulaType(bvToFpDoublePrec)) + .getMantissaSizeWithoutSignBit()) .isEqualTo(doublePrecType.getMantissaSizeWithoutSignBit()); assertThat(((FloatingPointType) mgr.getFormulaType(bvToFpDoublePrec)).getExponentSize()) .isEqualTo(doublePrecType.getExponentSize()); // The same as above, but build the precision by hand with the different APIs FloatingPointType fpTypeWithSignBit = - FloatingPointType.getFloatingPointTypeWithSignBit( + FloatingPointType.getFloatingPointTypeFromSizesWithSignBit( doublePrecType.getExponentSize(), doublePrecType.getMantissaSizeWithSignBit()); FloatingPointType fpTypeWithoutSignBit = - FloatingPointType.getFloatingPointTypeWithoutSignBit( + FloatingPointType.getFloatingPointTypeFromSizesWithoutSignBit( doublePrecType.getExponentSize(), doublePrecType.getMantissaSizeWithoutSignBit()); assertThat(fpTypeWithSignBit).isEqualTo(doublePrecType); assertThat(fpTypeWithoutSignBit).isEqualTo(doublePrecType); @@ -1373,12 +1380,12 @@ public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecisi assertThat(((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)).getTotalSize()) .isEqualTo(doublePrecType.getTotalSize()); assertThat( - ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)) - .getMantissaSizeWithSignBit()) + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)) + .getMantissaSizeWithSignBit()) .isEqualTo(doublePrecType.getMantissaSizeWithSignBit()); assertThat( - ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)) - .getMantissaSizeWithoutSignBit()) + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)) + .getMantissaSizeWithoutSignBit()) .isEqualTo(doublePrecType.getMantissaSizeWithoutSignBit()); assertThat(((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)).getExponentSize()) .isEqualTo(doublePrecType.getExponentSize()); @@ -1389,22 +1396,21 @@ public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecisi assertThat(((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)).getTotalSize()) .isEqualTo(doublePrecType.getTotalSize()); assertThat( - ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)) - .getMantissaSizeWithSignBit()) + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)) + .getMantissaSizeWithSignBit()) .isEqualTo(doublePrecType.getMantissaSizeWithSignBit()); assertThat( - ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)) - .getMantissaSizeWithoutSignBit()) + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)) + .getMantissaSizeWithoutSignBit()) .isEqualTo(doublePrecType.getMantissaSizeWithoutSignBit()); assertThat( - ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)).getExponentSize()) + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)).getExponentSize()) .isEqualTo(doublePrecType.getExponentSize()); if (solverSupportsNativeFPToBitvector()) { BitvectorFormula bvToFpDoublePrecToBv = fpmgr.toIeeeBitvector(bvToFpDoublePrec); assertThat(bvmgr.getLength(bvToFpDoublePrecToBv)).isEqualTo(bvSize64); - BitvectorFormula bvToFpTypeWithSignBitToBv = fpmgr.toIeeeBitvector(bvToFpfpTypeWithSignBit); assertThat(bvmgr.getLength(bvToFpTypeWithSignBitToBv)).isEqualTo(bvSize64); @@ -1413,8 +1419,8 @@ public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecisi assertThat(bvmgr.getLength(bvToFpTypeWithoutSignBitToBv)).isEqualTo(bvSize64); assume() - .withMessage("Bitwuzla equals on FPs/terms has a problem that needs to be addressed " - + "first") + .withMessage( + "Bitwuzla equals on FPs/terms has a problem that needs to be addressed " + "first") .that(solver) .isNotEqualTo(Solvers.BITWUZLA); diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 6fc6eef023..6e3a0403a7 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -478,7 +478,9 @@ public void floatConstantVisit() { 32, '0')); checkFloatConstant( - FormulaType.getFloatingPointTypeWithoutSignBit(5, 10), entry.getKey(), entry.getValue()); + FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(5, 10), + entry.getKey(), + entry.getValue()); } } @@ -581,7 +583,7 @@ public void fpToBvTest() { .that(solverToUse()) .isNoneOf(Solvers.CVC4, Solvers.CVC5); - var fpType = FormulaType.getFloatingPointTypeWithoutSignBit(5, 10); + var fpType = FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(5, 10); var visitor = new DefaultFormulaVisitor() { @Override From d836779092463cdac0ce8190ceebb543c67822fb Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 16:41:52 +0200 Subject: [PATCH 35/67] Add total size check to FP checks for single/double precision in FloatingPointNumber --- src/org/sosy_lab/java_smt/api/FloatingPointNumber.java | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index b4cf805085..a39ec2968e 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -213,8 +213,9 @@ public static FloatingPointNumber of( * @return true for IEEE-754 single precision type, false otherwise. */ public boolean isIEEE754SinglePrecision() { - // Mantissa does not include the sign bit - return getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE + // Mantissa does not include the sign bit internally + return getTotalSize() == SINGLE_PRECISION_EXPONENT_SIZE + SINGLE_PRECISION_MANTISSA_SIZE + 1 + && getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE && getMantissaSizeWithoutSignBit() == SINGLE_PRECISION_MANTISSA_SIZE; } @@ -225,8 +226,9 @@ public boolean isIEEE754SinglePrecision() { * @return true for IEEE-754 double precision type, false otherwise. */ public boolean isIEEE754DoublePrecision() { - // Mantissa does not include the sign bit - return getExponentSize() == DOUBLE_PRECISION_EXPONENT_SIZE + // Mantissa does not include the sign bit internally + return getTotalSize() == DOUBLE_PRECISION_EXPONENT_SIZE + DOUBLE_PRECISION_MANTISSA_SIZE + 1 + && getExponentSize() == DOUBLE_PRECISION_EXPONENT_SIZE && getMantissaSizeWithoutSignBit() == DOUBLE_PRECISION_MANTISSA_SIZE; } From 0885fd00bc079c43bd78b5eb32649ade588bc539 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 17:12:35 +0200 Subject: [PATCH 36/67] Improve JavaDoc of FloatingPointType constructors --- .../sosy_lab/java_smt/api/FormulaType.java | 28 +++++++++++++++---- 1 file changed, 23 insertions(+), 5 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index b1f1ebb0b2..5cfbbdeea0 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -209,12 +209,18 @@ public String toSMTLIBString() { * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes. * The mantissa size is expected to not include the sign bit. * + * @deprecated this method can be confusing, as the SMTLIB2 standard expects the mantissa to + * include the sign bit, but this method expects the mantissa argument without the sign bit. + * Use {@link #getFloatingPointTypeFromSizesWithoutSignBit(int, int)} instead if you want to + * construct a {@link FloatingPointType} with the constructing method treating the mantissa + * argument without the sign bit, and {@link #getFloatingPointTypeFromSizesWithSignBit(int, + * int)} if you want it to include the sign bit in the size of the mantissa argument. * @param exponentSize size of the exponent for the base of the floating-point * @param mantissaSizeWithoutSignBit size of the mantissa (also called a coefficient or * significant), excluding the sign bit. * @return the newly constructed {@link FloatingPointType}. */ - // TODO: mark as soon to be deprecated + @Deprecated(since = "6.0", forRemoval = true) public static FloatingPointType getFloatingPointType( int exponentSize, int mantissaSizeWithoutSignBit) { return getFloatingPointTypeFromSizesWithoutSignBit(exponentSize, mantissaSizeWithoutSignBit); @@ -222,8 +228,14 @@ public static FloatingPointType getFloatingPointType( /** * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes. - * The mantissa size is expected to not include the sign bit. The total size is therefore equal to - * mantissa + exponent + 1. + * The mantissa size is expected to not include the sign bit. The total size of the constructed + * type is equal to the addition of the two arguments plus one, as in: total size == exponentSize + * + mantissaSizeWithoutSignBit + 1. + * + *

Using the arguments e and m, calling this method with + * getFloatingPointTypeFromSizesWithoutSignBit (e, m) returns a type equal to a type constructed + * by {@link #getFloatingPointTypeFromSizesWithSignBit(int, int)} with the same arguments e and m + * as before, but m incremented by 1, as in getFloatingPointTypeFromSizesWithSignBit(e, m + 1). * * @param exponentSize size of the exponent for the base of the floating-point * @param mantissaSizeWithoutSignBit size of the mantissa (also called a coefficient or @@ -237,8 +249,14 @@ public static FloatingPointType getFloatingPointTypeFromSizesWithoutSignBit( /** * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes. - * The mantissa size is expected to include the sign bit. The total size is therefore equal to - * mantissa + exponent. + * The mantissa size is expected to include the sign bit. The total size of the constructed type + * is equal to the addition of the two arguments, as in: total size == exponentSize + + * mantissaSizeWithSignBit. + * + *

Using the arguments e and m, calling this method with + * getFloatingPointTypeFromSizesWithSignBit(e, m) returns a type equal to a type constructed by + * {@link #getFloatingPointTypeFromSizesWithoutSignBit(int, int)} with the same arguments e and m + * as before, but m decremented by 1, as in getFloatingPointTypeFromSizesWithoutSignBit(e, m - 1). * * @param exponentSize size of the exponent for the base of the floating-point * @param mantissaSizeWithSignBit size of the mantissa (also called a coefficient or significant), From 23cdc675bb4b3c9971c1c187f3e55ac2e367a7da Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 17:20:10 +0200 Subject: [PATCH 37/67] Update variable/const names of mantissas in FloatingPointNumber/FloatingPointType to reflect inclusion of sign bit --- .../java_smt/api/FloatingPointNumber.java | 14 +++++---- .../sosy_lab/java_smt/api/FormulaType.java | 29 ++++++++++--------- .../test/FloatingPointNumberTest.java | 12 +++++--- 3 files changed, 32 insertions(+), 23 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index a39ec2968e..bd904b8924 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -25,9 +25,9 @@ public abstract class FloatingPointNumber { // Mantissas do not include the sign bit public static final int SINGLE_PRECISION_EXPONENT_SIZE = 8; - public static final int SINGLE_PRECISION_MANTISSA_SIZE = 23; + public static final int SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT = 23; public static final int DOUBLE_PRECISION_EXPONENT_SIZE = 11; - public static final int DOUBLE_PRECISION_MANTISSA_SIZE = 52; + public static final int DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT = 52; public enum Sign { POSITIVE, @@ -214,9 +214,10 @@ public static FloatingPointNumber of( */ public boolean isIEEE754SinglePrecision() { // Mantissa does not include the sign bit internally - return getTotalSize() == SINGLE_PRECISION_EXPONENT_SIZE + SINGLE_PRECISION_MANTISSA_SIZE + 1 + return getTotalSize() + == SINGLE_PRECISION_EXPONENT_SIZE + SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT + 1 && getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE - && getMantissaSizeWithoutSignBit() == SINGLE_PRECISION_MANTISSA_SIZE; + && getMantissaSizeWithoutSignBit() == SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT; } /** @@ -227,9 +228,10 @@ && getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE */ public boolean isIEEE754DoublePrecision() { // Mantissa does not include the sign bit internally - return getTotalSize() == DOUBLE_PRECISION_EXPONENT_SIZE + DOUBLE_PRECISION_MANTISSA_SIZE + 1 + return getTotalSize() + == DOUBLE_PRECISION_EXPONENT_SIZE + DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT + 1 && getExponentSize() == DOUBLE_PRECISION_EXPONENT_SIZE - && getMantissaSizeWithoutSignBit() == DOUBLE_PRECISION_MANTISSA_SIZE; + && getMantissaSizeWithoutSignBit() == DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT; } /** compute a representation as Java-based float value, if possible. */ diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index 5cfbbdeea0..4b407728d4 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -9,9 +9,9 @@ package org.sosy_lab.java_smt.api; import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_EXPONENT_SIZE; -import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_MANTISSA_SIZE; +import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT; import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_EXPONENT_SIZE; -import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_MANTISSA_SIZE; +import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT; import com.google.common.base.Joiner; import com.google.common.base.Preconditions; @@ -288,18 +288,20 @@ public static FloatingPointType getDoublePrecisionFloatingPointType() { public static final class FloatingPointType extends FormulaType { private static final FloatingPointType SINGLE_PRECISION_FP_TYPE = - new FloatingPointType(SINGLE_PRECISION_EXPONENT_SIZE, SINGLE_PRECISION_MANTISSA_SIZE); + new FloatingPointType( + SINGLE_PRECISION_EXPONENT_SIZE, SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT); private static final FloatingPointType DOUBLE_PRECISION_FP_TYPE = - new FloatingPointType(DOUBLE_PRECISION_EXPONENT_SIZE, DOUBLE_PRECISION_MANTISSA_SIZE); + new FloatingPointType( + DOUBLE_PRECISION_EXPONENT_SIZE, DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT); private final int exponentSize; // The SMTLib2 standard defines the mantissa size as including the sign bit. We do not include // it here though. - private final int mantissaSize; + private final int mantissaSizeWithoutSignBit; - private FloatingPointType(int pExponentSize, int pMantissaSize) { + private FloatingPointType(int pExponentSize, int pMantissaSizeWithoutSignBit) { exponentSize = pExponentSize; - mantissaSize = pMantissaSize; + mantissaSizeWithoutSignBit = pMantissaSizeWithoutSignBit; } @Override @@ -323,7 +325,7 @@ public int getExponentSize() { */ @Deprecated(since = "6.0", forRemoval = true) public int getMantissaSize() { - return mantissaSize; + return mantissaSizeWithoutSignBit; } /** @@ -331,7 +333,7 @@ public int getMantissaSize() { * sign bit. */ public int getMantissaSizeWithoutSignBit() { - return mantissaSize; + return mantissaSizeWithoutSignBit; } /** @@ -339,7 +341,7 @@ public int getMantissaSizeWithoutSignBit() { * sign bit. */ public int getMantissaSizeWithSignBit() { - return mantissaSize + 1; + return mantissaSizeWithoutSignBit + 1; } /** @@ -347,12 +349,12 @@ public int getMantissaSizeWithSignBit() { * (including the sign bit). */ public int getTotalSize() { - return exponentSize + mantissaSize + 1; + return exponentSize + mantissaSizeWithoutSignBit + 1; } @Override public int hashCode() { - return (31 + exponentSize) * 31 + mantissaSize; + return (31 + exponentSize) * 31 + mantissaSizeWithoutSignBit; } @Override @@ -364,7 +366,8 @@ public boolean equals(Object obj) { return false; } FloatingPointType other = (FloatingPointType) obj; - return this.exponentSize == other.exponentSize && this.mantissaSize == other.mantissaSize; + return this.exponentSize == other.exponentSize + && this.mantissaSizeWithoutSignBit == other.mantissaSizeWithoutSignBit; } @Override diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java index 831f68ad17..fb546ba873 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java @@ -11,9 +11,9 @@ import static com.google.common.truth.Truth.assertThat; import static org.junit.Assert.assertThrows; import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_EXPONENT_SIZE; -import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_MANTISSA_SIZE; +import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT; import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_EXPONENT_SIZE; -import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_MANTISSA_SIZE; +import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT; import com.google.common.base.Strings; import java.math.BigInteger; @@ -50,7 +50,9 @@ public void floatingPointNumberWithSinglePrecision() { var bits = Strings.padStart(Integer.toBinaryString(Float.floatToRawIntBits(f)), 32, '0'); var fpNum = FloatingPointNumber.of( - bits, SINGLE_PRECISION_EXPONENT_SIZE, SINGLE_PRECISION_MANTISSA_SIZE); + bits, + SINGLE_PRECISION_EXPONENT_SIZE, + SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT); assertThat(fpNum.floatValue()).isEqualTo(f); assertThat(fpNum.doubleValue()).isEqualTo((double) f); // float is a strict subtype of double. } @@ -83,7 +85,9 @@ public void floatingPointNumberWithDoublePrecision() { var bits = Strings.padStart(Long.toBinaryString(Double.doubleToRawLongBits(d)), 64, '0'); var fpNum = FloatingPointNumber.of( - bits, DOUBLE_PRECISION_EXPONENT_SIZE, DOUBLE_PRECISION_MANTISSA_SIZE); + bits, + DOUBLE_PRECISION_EXPONENT_SIZE, + DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT); assertThat(fpNum.doubleValue()).isEqualTo(d); } } From d67273c6e448c63419886bca23e928ed7e00a188 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 17:25:11 +0200 Subject: [PATCH 38/67] Improve CVC5 documentation in regard to mantissa including the sign bit + improve test error message for exponent/mantissa equality --- .../solvers/cvc5/CVC5FloatingPointFormulaManager.java | 8 ++++---- .../java_smt/test/FloatingPointFormulaManagerTest.java | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) 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 6dfb19b9bb..e41e991916 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -157,7 +157,7 @@ protected Term makePlusInfinityImpl(FloatingPointType pType) { throw new IllegalArgumentException( "You tried creating a invalid positive floating point +infinity with exponent size " + pType.getExponentSize() - + " and mantissa size " + + " and mantissa size (including the sign bit)" + pType.getMantissaSizeWithSignBit() + ".", e); @@ -173,7 +173,7 @@ protected Term makeMinusInfinityImpl(FloatingPointType pType) { throw new IllegalArgumentException( "You tried creating a invalid negative floating point -infinity with exponent size " + pType.getExponentSize() - + " and mantissa size " + + " and mantissa size (including the sign bit)" + pType.getMantissaSizeWithSignBit() + ".", e); @@ -189,7 +189,7 @@ protected Term makeNaNImpl(FloatingPointType pType) { throw new IllegalArgumentException( "You tried creating a invalid NaN with exponent size " + pType.getExponentSize() - + " and mantissa size " + + " and mantissa size (including the sign bit)" + pType.getMantissaSizeWithSignBit() + ".", e); @@ -278,7 +278,7 @@ protected Term castFromImpl( + pNumber + " into a FloatingPoint with exponent size " + pTargetType.getExponentSize() - + " and mantissa size " + + " and mantissa size (including the sign bit)" + pTargetType.getMantissaSizeWithSignBit() + ".", e); diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 8bf6479773..b78ee597c7 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -80,10 +80,10 @@ public void floatingPointType() { FloatingPointFormula var = fpmgr.makeVariable("x", type); FloatingPointType result = (FloatingPointType) mgr.getFormulaType(var); - assertWithMessage("exponent size") + assertWithMessage("exponent sizes not equal") .that(result.getExponentSize()) .isEqualTo(type.getExponentSize()); - assertWithMessage("mantissa size") + assertWithMessage("mantissa sizes not equal") .that(result.getMantissaSizeWithSignBit()) .isEqualTo(type.getMantissaSizeWithSignBit()); } From b7b8affe4c2b6fc574f22831203c42b09be3d994 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 17:28:47 +0200 Subject: [PATCH 39/67] Update code with "getMantissaSizeWithSignBit() - 1" in MathSAT5 to use getMantissaSizeWithoutSignBit() --- .../Mathsat5FloatingPointFormulaManager.java | 20 +++++++++---------- .../mathsat5/Mathsat5FormulaCreator.java | 2 +- 2 files changed, 11 insertions(+), 11 deletions(-) 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 11d8e472d6..7abbdea164 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java @@ -103,14 +103,14 @@ protected Long makeNumberImpl( final String signStr = sign.isNegative() ? "1" : "0"; final String exponentStr = getBvRepresentation(exponent, type.getExponentSize()); // MathSAT5 expects the mantissa to not include the sign bit - final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSizeWithSignBit() - 1); + final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSizeWithoutSignBit()); 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.getMantissaSizeWithSignBit() - 1); + type.getMantissaSizeWithoutSignBit()); } @Override @@ -124,7 +124,7 @@ protected Long makeNumberAndRound(String pN, FloatingPointType pType, Long pRoun mathsatEnv, "0", pType.getExponentSize(), - pType.getMantissaSizeWithSignBit() - 1, + pType.getMantissaSizeWithoutSignBit(), pRoundingMode)); } } catch (NumberFormatException e) { @@ -148,21 +148,21 @@ protected Long makeVariableImpl(String var, FloatingPointType type) { protected Long makePlusInfinityImpl(FloatingPointType type) { // MathSAT5 expects the mantissa to not include the sign bit return msat_make_fp_plus_inf( - mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithSignBit() - 1); + mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithoutSignBit()); } @Override protected Long makeMinusInfinityImpl(FloatingPointType type) { // MathSAT5 expects the mantissa to not include the sign bit return msat_make_fp_minus_inf( - mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithSignBit() - 1); + mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithoutSignBit()); } @Override protected Long makeNaNImpl(FloatingPointType type) { // MathSAT5 expects the mantissa to not include the sign bit return msat_make_fp_nan( - mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithSignBit() - 1); + mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithoutSignBit()); } @Override @@ -174,7 +174,7 @@ protected Long castToImpl( return msat_make_fp_cast( mathsatEnv, targetType.getExponentSize(), - targetType.getMantissaSizeWithSignBit() - 1, + targetType.getMantissaSizeWithoutSignBit(), pRoundingMode, pNumber); @@ -205,14 +205,14 @@ protected Long castFromImpl( return msat_make_fp_from_sbv( mathsatEnv, pTargetType.getExponentSize(), - pTargetType.getMantissaSizeWithSignBit() - 1, + pTargetType.getMantissaSizeWithoutSignBit(), pRoundingMode, pNumber); } else { return msat_make_fp_from_ubv( mathsatEnv, pTargetType.getExponentSize(), - pTargetType.getMantissaSizeWithSignBit() - 1, + pTargetType.getMantissaSizeWithoutSignBit(), pRoundingMode, pNumber); } @@ -240,7 +240,7 @@ protected Long fromIeeeBitvectorImpl(Long pNumber, FloatingPointType pTargetType return Mathsat5NativeApi.msat_make_fp_from_ieeebv( mathsatEnv, pTargetType.getExponentSize(), - pTargetType.getMantissaSizeWithSignBit() - 1, + pTargetType.getMantissaSizeWithoutSignBit(), pNumber); } diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java index d2c20cf938..0e0747f5ad 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -244,7 +244,7 @@ public Long getBitvectorType(int pBitwidth) { public Long getFloatingPointType(FloatingPointType pType) { // MathSAT5 automatically adds 1 to the mantissa, as it expects it to be without it. return msat_get_fp_type( - getEnv(), pType.getExponentSize(), pType.getMantissaSizeWithSignBit() - 1); + getEnv(), pType.getExponentSize(), pType.getMantissaSizeWithoutSignBit()); } @SuppressWarnings("unchecked") From 225ba7a497eece7a36532b549dc1d13ddbda6d20 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 17:33:53 +0200 Subject: [PATCH 40/67] Add info about the mantissa size to MathSAT5 native API --- .../solvers/mathsat5/Mathsat5NativeApi.java | 41 +++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java index f0862ddaf8..86bfbc59ca 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java @@ -245,6 +245,10 @@ public static void msat_set_option_checked(long cfg, String option, String value public static native long msat_get_array_element_type(long e, long t); + /** + * MathSAT5 expects the mantissa argument for floating-points and floating-point types to not + * include the sign bit! + */ public static native long msat_get_fp_type(long e, int exp_with, int mant_with); public static native long msat_get_fp_roundingmode_type(long e); @@ -272,6 +276,7 @@ public static native long msat_get_function_type( public static native int msat_get_fp_type_exp_width(long e, long t); + /** MathSAT5 returns the mantissa argument without the sign bit! */ public static native int msat_get_fp_type_mant_width(long e, long t); public static native boolean msat_is_fp_roundingmode_type(long e, long t); @@ -463,6 +468,10 @@ public static long msat_existentially_quantify(long env, long term, long[] args) public static native long msat_make_fp_round_to_int(long e, long rounding, long t); + /** + * MathSAT5 expects the mantissa argument for floating-points and floating-point types to not + * include the sign bit! + */ public static native long msat_make_fp_cast( long e, long exp_w, long mant_w, long rounding, long t); @@ -470,14 +479,26 @@ public static native long msat_make_fp_cast( public static native long msat_make_fp_to_ubv(long e, long width, long rounding, long t); + /** + * MathSAT5 expects the mantissa argument for floating-points and floating-point types to not + * include the sign bit! + */ public static native long msat_make_fp_from_sbv( long e, long exp_w, long mant_w, long rounding, long t); + /** + * MathSAT5 expects the mantissa argument for floating-points and floating-point types to not + * include the sign bit! + */ public static native long msat_make_fp_from_ubv( long e, long exp_w, long mant_w, long rounding, long t); public static native long msat_make_fp_as_ieeebv(long e, long t); + /** + * MathSAT5 expects the mantissa argument for floating-points and floating-point types to not + * include the sign bit! + */ public static native long msat_make_fp_from_ieeebv(long e, long exp_w, long mant_w, long t); public static native long msat_make_fp_isnan(long e, long t); @@ -494,15 +515,35 @@ public static native long msat_make_fp_from_ubv( public static native long msat_make_fp_ispos(long e, long t); + /** + * MathSAT5 expects the mantissa argument for floating-points and floating-point types to not + * include the sign bit! + */ public static native long msat_make_fp_plus_inf(long e, long exp_w, long mant_w); + /** + * MathSAT5 expects the mantissa argument for floating-points and floating-point types to not + * include the sign bit! + */ public static native long msat_make_fp_minus_inf(long e, long exp_w, long mant_w); + /** + * MathSAT5 expects the mantissa argument for floating-points and floating-point types to not + * include the sign bit! + */ public static native long msat_make_fp_nan(long e, long exp_w, long mant_w); + /** + * MathSAT5 expects the mantissa argument for floating-points and floating-point types to not + * include the sign bit! + */ public static native long msat_make_fp_rat_number( long e, String numRep, long exp_w, long mant_w, long rounding); + /** + * MathSAT5 expects the mantissa argument for floating-points and floating-point types to not + * include the sign bit! + */ public static native long msat_make_fp_bits_number( long e, String bitRep, long exp_w, long mant_w); From 9df8b669c9a3b6b08da9ebad53e47efd509d989d Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 17:44:19 +0200 Subject: [PATCH 41/67] Add inlineMe annotations with replacements to newly deprecated FP methods --- src/org/sosy_lab/java_smt/api/FloatingPointNumber.java | 3 ++- src/org/sosy_lab/java_smt/api/FormulaType.java | 6 ++++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index bd904b8924..5099f9ddc5 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -91,7 +91,8 @@ public final boolean getSign() { * #getMantissaSizeWithSignBit()} if you want it to include the sign bit. */ @Deprecated(since = "6.0", forRemoval = true) - public int getMantissaSize() { + @InlineMe(replacement = "this.getMantissaSizeWithoutSignBit()") + public final int getMantissaSize() { return getMantissaSizeWithoutSignBit(); } diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index 4b407728d4..51a4b0946c 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -18,6 +18,7 @@ import com.google.common.base.Splitter; import com.google.common.collect.ImmutableSet; import com.google.errorprone.annotations.Immutable; +import com.google.errorprone.annotations.InlineMe; import java.util.List; import java.util.Set; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; @@ -221,6 +222,11 @@ public String toSMTLIBString() { * @return the newly constructed {@link FloatingPointType}. */ @Deprecated(since = "6.0", forRemoval = true) + @InlineMe( + replacement = + "FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(exponentSize," + + " mantissaSizeWithoutSignBit)", + imports = "org.sosy_lab.java_smt.api.FormulaType") public static FloatingPointType getFloatingPointType( int exponentSize, int mantissaSizeWithoutSignBit) { return getFloatingPointTypeFromSizesWithoutSignBit(exponentSize, mantissaSizeWithoutSignBit); From 7207b71a417bb51ff788ed262c3828050b4db20b Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 17:44:52 +0200 Subject: [PATCH 42/67] Update more deprecated FP API with the new alternatives and simplify calls --- .../api/FloatingPointFormulaManager.java | 5 +-- .../test/FloatingPointFormulaManagerTest.java | 35 ++++++++----------- 2 files changed, 18 insertions(+), 22 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index 126bf9b504..a70d10544e 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -8,7 +8,7 @@ package org.sosy_lab.java_smt.api; -import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointType; +import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointTypeFromSizesWithoutSignBit; import java.math.BigDecimal; import java.math.BigInteger; @@ -99,7 +99,8 @@ default FloatingPointFormula makeNumber(FloatingPointNumber number) { number.getExponent(), number.getMantissa(), number.getMathSign(), - getFloatingPointType(number.getExponentSize(), number.getMantissaSizeWithoutSignBit())); + getFloatingPointTypeFromSizesWithoutSignBit( + number.getExponentSize(), number.getMantissaSizeWithoutSignBit())); } /** diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index b78ee597c7..46467a8094 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -12,6 +12,8 @@ import static com.google.common.truth.Truth.assertWithMessage; import static com.google.common.truth.TruthJUnit.assume; import static org.junit.Assert.assertThrows; +import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointTypeFromSizesWithSignBit; +import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointTypeFromSizesWithoutSignBit; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; import com.google.common.collect.ImmutableList; @@ -76,7 +78,7 @@ public void init() { @Test public void floatingPointType() { - FloatingPointType type = FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(23, 42); + FloatingPointType type = getFloatingPointTypeFromSizesWithoutSignBit(23, 42); FloatingPointFormula var = fpmgr.makeVariable("x", type); FloatingPointType result = (FloatingPointType) mgr.getFormulaType(var); @@ -259,9 +261,7 @@ public void fpRemainderNormal() throws SolverException, InterruptedException { for (FloatingPointType prec : new FloatingPointType[] { - singlePrecType, - doublePrecType, - FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(5, 6), + singlePrecType, doublePrecType, getFloatingPointTypeFromSizesWithoutSignBit(5, 6), }) { final FloatingPointFormula numFive = fpmgr.makeNumber(5, prec); @@ -285,9 +285,7 @@ public void fpRemainderSpecial() throws SolverException, InterruptedException { for (FloatingPointType prec : new FloatingPointType[] { - singlePrecType, - doublePrecType, - FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(5, 6), + singlePrecType, doublePrecType, getFloatingPointTypeFromSizesWithoutSignBit(5, 6), }) { final FloatingPointFormula num = fpmgr.makeNumber(42, prec); @@ -541,7 +539,7 @@ public void numberConstants() throws SolverException, InterruptedException { checkEqualityOfNumberConstantsFor(3.4028234663852886e+38, doublePrecType); // check unequality for large types - FloatingPointType nearDouble = FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(12, 52); + FloatingPointType nearDouble = getFloatingPointTypeFromSizesWithoutSignBit(12, 52); FloatingPointFormula h1 = fpmgr.makeNumber(BigDecimal.TEN.pow(309).multiply(BigDecimal.valueOf(1.0001)), nearDouble); FloatingPointFormula h2 = @@ -549,7 +547,7 @@ public void numberConstants() throws SolverException, InterruptedException { assertThatFormula(fpmgr.equalWithFPSemantics(h1, h2)).isUnsatisfiable(); // check equality for short types - FloatingPointType smallType = FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(4, 4); + FloatingPointType smallType = getFloatingPointTypeFromSizesWithoutSignBit(4, 4); FloatingPointFormula i1 = fpmgr.makeNumber(BigDecimal.TEN.pow(50).multiply(BigDecimal.valueOf(1.001)), smallType); FloatingPointFormula i2 = @@ -578,7 +576,7 @@ public void numberConstants() throws SolverException, InterruptedException { assertThatFormula(fpmgr.isNegative(ni2)).isTautological(); // check equality for short types - FloatingPointType smallType2 = FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(4, 4); + FloatingPointType smallType2 = getFloatingPointTypeFromSizesWithoutSignBit(4, 4); FloatingPointFormula j1 = fpmgr.makeNumber(BigDecimal.TEN.pow(500).multiply(BigDecimal.valueOf(1.001)), smallType2); FloatingPointFormula j2 = @@ -609,8 +607,7 @@ public void numberConstants() throws SolverException, InterruptedException { // Z3 supports at least FloatingPointType(15, 112). Larger types seem to be rounded. if (!ImmutableSet.of(Solvers.Z3, Solvers.CVC4).contains(solver)) { // check unequality for very large types - FloatingPointType largeType = - FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(100, 100); + FloatingPointType largeType = getFloatingPointTypeFromSizesWithoutSignBit(100, 100); FloatingPointFormula k1 = fpmgr.makeNumber(BigDecimal.TEN.pow(200).multiply(BigDecimal.valueOf(1.001)), largeType); FloatingPointFormula k2 = @@ -647,8 +644,7 @@ public void numberConstantsNearInf() throws SolverException, InterruptedExceptio private void checkNearInf(int mantissa, int exponent, long value) throws SolverException, InterruptedException { - FloatingPointType type = - FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(exponent, mantissa); + FloatingPointType type = getFloatingPointTypeFromSizesWithoutSignBit(exponent, mantissa); FloatingPointFormula fp1 = fpmgr.makeNumber(BigDecimal.valueOf(value), type); assertThatFormula(fpmgr.isInfinity(fp1)).isTautological(); FloatingPointFormula fp2 = fpmgr.makeNumber(BigDecimal.valueOf(value - 1), type); @@ -683,8 +679,7 @@ public void numberConstantsNearMinusInf() throws SolverException, InterruptedExc private void checkNearMinusInf(int mantissa, int exponent, long value) throws SolverException, InterruptedException { - FloatingPointType type = - FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(exponent, mantissa); + FloatingPointType type = getFloatingPointTypeFromSizesWithoutSignBit(exponent, mantissa); FloatingPointFormula fp1 = fpmgr.makeNumber(BigDecimal.valueOf(value), type); assertThatFormula(fpmgr.isInfinity(fp1)).isTautological(); FloatingPointFormula fp2 = fpmgr.makeNumber(BigDecimal.valueOf(value + 1), type); @@ -1269,10 +1264,10 @@ public void floatingPointMantissaSignBitWithBitvectorInterpretationSinglePrecisi // The same as above, but build the precision by hand with the different APIs FloatingPointType fpTypeWithSignBit = - FloatingPointType.getFloatingPointTypeFromSizesWithSignBit( + getFloatingPointTypeFromSizesWithSignBit( singlePrecType.getExponentSize(), singlePrecType.getMantissaSizeWithSignBit()); FloatingPointType fpTypeWithoutSignBit = - FloatingPointType.getFloatingPointTypeFromSizesWithoutSignBit( + getFloatingPointTypeFromSizesWithoutSignBit( singlePrecType.getExponentSize(), singlePrecType.getMantissaSizeWithoutSignBit()); assertThat(fpTypeWithSignBit).isEqualTo(singlePrecType); assertThat(fpTypeWithoutSignBit).isEqualTo(singlePrecType); @@ -1366,10 +1361,10 @@ public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecisi // The same as above, but build the precision by hand with the different APIs FloatingPointType fpTypeWithSignBit = - FloatingPointType.getFloatingPointTypeFromSizesWithSignBit( + getFloatingPointTypeFromSizesWithSignBit( doublePrecType.getExponentSize(), doublePrecType.getMantissaSizeWithSignBit()); FloatingPointType fpTypeWithoutSignBit = - FloatingPointType.getFloatingPointTypeFromSizesWithoutSignBit( + getFloatingPointTypeFromSizesWithoutSignBit( doublePrecType.getExponentSize(), doublePrecType.getMantissaSizeWithoutSignBit()); assertThat(fpTypeWithSignBit).isEqualTo(doublePrecType); assertThat(fpTypeWithoutSignBit).isEqualTo(doublePrecType); From 5086ae7daad65e60a1c423cf2077de5eb768cce3 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 17:49:07 +0200 Subject: [PATCH 43/67] Update one more FP type constructor in CVC5 to better include the mantissa --- .../sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java index 177629cbbf..3d60a92d72 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -224,8 +224,8 @@ private FormulaType getFormulaTypeFromTermType(Sort sort) { return FormulaType.getBitvectorTypeWithSize(sort.getBitVectorSize()); } else if (sort.isFloatingPoint()) { // CVC5 wants the sign bit as part of the mantissa. We add that manually in creation. - return FormulaType.getFloatingPointTypeFromSizesWithoutSignBit( - sort.getFloatingPointExponentSize(), sort.getFloatingPointSignificandSize() - 1); + return FormulaType.getFloatingPointTypeFromSizesWithSignBit( + sort.getFloatingPointExponentSize(), sort.getFloatingPointSignificandSize()); } else if (sort.isRoundingMode()) { return FormulaType.FloatingPointRoundingModeType; } else if (sort.isReal()) { From 6cb15ea71c1fa7473ce8b967fa9ec72aa9247210 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 17:51:35 +0200 Subject: [PATCH 44/67] Update a mantissa size variable name to include sign bit in CVC4FloatingPointFormulaManager --- .../solvers/cvc4/CVC4FloatingPointFormulaManager.java | 5 +++-- 1 file changed, 3 insertions(+), 2 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 ca1427d92c..79e508609c 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -126,10 +126,11 @@ protected Expr makeNumberAndRound(String pN, FloatingPointType pType, Expr pRoun } // TODO lookup why this number works: 2**(2**(exp-1)) - 2**(2**(exp-1)-2-mant) - private static BigInteger getBiggestNumberBeforeInf(int mantissa, int exponent) { + private static BigInteger getBiggestNumberBeforeInf(int mantissaWithoutSignBit, int exponent) { int boundExponent = BigInteger.valueOf(2).pow(exponent - 1).intValueExact(); BigInteger upperBoundExponent = BigInteger.valueOf(2).pow(boundExponent); - int mantissaExponent = BigInteger.valueOf(2).pow(exponent - 1).intValueExact() - 2 - mantissa; + int mantissaExponent = + BigInteger.valueOf(2).pow(exponent - 1).intValueExact() - 2 - mantissaWithoutSignBit; if (mantissaExponent >= 0) { // ignore negative mantissaExponent upperBoundExponent = upperBoundExponent.subtract(BigInteger.valueOf(2).pow(mantissaExponent)); } From f760eb149fb52e6965b81cc815e076a69213f09b Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 17:59:08 +0200 Subject: [PATCH 45/67] Update a mantissa size variable names to include sign bit in BitwuzlaFormulaCreator and switch to appropriate type constructors --- .../solvers/bitwuzla/BitwuzlaFormulaCreator.java | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index 48c3de8a78..9644c28053 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -170,8 +170,8 @@ public FormulaType bitwuzlaSortToType(Sort pSort) { // UFs play by different rules. For them, we need to extract the domain if (pSort.is_fp()) { int exponent = pSort.fp_exp_size(); - int mantissa = pSort.fp_sig_size() - 1; - return FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(exponent, mantissa); + int mantissaWithSignBit = pSort.fp_sig_size(); + return FormulaType.getFloatingPointTypeFromSizesWithSignBit(exponent, mantissaWithSignBit); } else if (pSort.is_bv()) { return FormulaType.getBitvectorTypeWithSize(pSort.bv_size()); } else if (pSort.is_array()) { @@ -379,8 +379,9 @@ public FormulaType getFormulaType(T pFormula) { "FloatingPointFormula with actual type " + sort + ": " + pFormula); } int exp = sort.fp_exp_size(); - int man = sort.fp_sig_size() - 1; - return (FormulaType) FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(exp, man); + int mantissaWithSignBit = sort.fp_sig_size(); + return (FormulaType) + FormulaType.getFloatingPointTypeFromSizesWithSignBit(exp, mantissaWithSignBit); } else if (sort.is_rm()) { return (FormulaType) FormulaType.FloatingPointRoundingModeType; } @@ -590,9 +591,9 @@ public Object convertValue(Term term) { return new BigInteger(term.to_bv(), 2); } if (sort.is_fp()) { - int sizeExponent = sort.fp_exp_size(); - int sizeMantissa = sort.fp_sig_size() - 1; - return FloatingPointNumber.of(term.to_bv(), sizeExponent, sizeMantissa); + int exponentSize = sort.fp_exp_size(); + int mantissaSizeWithoutSignBit = sort.fp_sig_size() - 1; + return FloatingPointNumber.of(term.to_bv(), exponentSize, mantissaSizeWithoutSignBit); } throw new AssertionError("Unknown value type."); } From f7c59161c44004dd4225208bed2b927e7af269f8 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 3 Sep 2025 18:06:16 +0200 Subject: [PATCH 46/67] Update an FP type constructor in Z3 to a better one --- src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java index 30dec36188..31a8c6385a 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -242,8 +242,8 @@ public FormulaType getFormulaTypeFromSort(Long pSort) { return FormulaType.getArrayType( getFormulaTypeFromSort(domainSort), getFormulaTypeFromSort(rangeSort)); case Z3_FLOATING_POINT_SORT: - return FormulaType.getFloatingPointTypeFromSizesWithoutSignBit( - Native.fpaGetEbits(z3context, pSort), Native.fpaGetSbits(z3context, pSort) - 1); + return FormulaType.getFloatingPointTypeFromSizesWithSignBit( + Native.fpaGetEbits(z3context, pSort), Native.fpaGetSbits(z3context, pSort)); case Z3_ROUNDING_MODE_SORT: return FormulaType.FloatingPointRoundingModeType; case Z3_RE_SORT: From fbea69fba43ee7f9c52a8f34018e7df869a90491 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 5 Sep 2025 17:41:45 +0200 Subject: [PATCH 47/67] Simplify calculation of total size of FP type --- src/org/sosy_lab/java_smt/api/FormulaType.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index 51a4b0946c..8701a29038 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -355,7 +355,7 @@ public int getMantissaSizeWithSignBit() { * (including the sign bit). */ public int getTotalSize() { - return exponentSize + mantissaSizeWithoutSignBit + 1; + return exponentSize + getMantissaSizeWithSignBit(); } @Override From e043988fb192d1aee5263b0f257bcd5ed5f47736 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 5 Sep 2025 18:05:21 +0200 Subject: [PATCH 48/67] Refactor some FP/precision sizes/mantissa code in CVC4 --- .../solvers/cvc4/CVC4FloatingPointFormulaManager.java | 8 ++------ .../java_smt/solvers/cvc4/CVC4FormulaCreator.java | 4 ++-- 2 files changed, 4 insertions(+), 8 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 79e508609c..8142d5f97f 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -49,11 +49,8 @@ protected CVC4FloatingPointFormulaManager( // TODO Is there a difference in `FloatingPointSize` and `FloatingPointType` in CVC4? // They are both just pairs of `exponent size` and `significant size`. - private static FloatingPointSize getFPSize(FloatingPointType pType) { - long pExponentSize = pType.getExponentSize(); - long pMantissaSize = pType.getMantissaSizeWithSignBit(); - return new FloatingPointSize(pExponentSize, pMantissaSize); + return new FloatingPointSize(pType.getExponentSize(), pType.getMantissaSizeWithSignBit()); } @Override @@ -129,8 +126,7 @@ protected Expr makeNumberAndRound(String pN, FloatingPointType pType, Expr pRoun private static BigInteger getBiggestNumberBeforeInf(int mantissaWithoutSignBit, int exponent) { int boundExponent = BigInteger.valueOf(2).pow(exponent - 1).intValueExact(); BigInteger upperBoundExponent = BigInteger.valueOf(2).pow(boundExponent); - int mantissaExponent = - BigInteger.valueOf(2).pow(exponent - 1).intValueExact() - 2 - mantissaWithoutSignBit; + int mantissaExponent = boundExponent - 2 - mantissaWithoutSignBit; if (mantissaExponent >= 0) { // ignore negative mantissaExponent upperBoundExponent = upperBoundExponent.subtract(BigInteger.valueOf(2).pow(mantissaExponent)); } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java index e62c78a99c..fbd6a381e8 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -629,8 +629,8 @@ private FloatingPointNumber convertFloatingPoint(Expr fpExpr) { final var fp = fpExpr.getConstFloatingPoint(); final var fpType = fp.getT(); final var expWidth = Ints.checkedCast(fpType.exponentWidth()); - final var mantWidthWithoutSignBit = Ints.checkedCast(fpType.significandWidth() - 1); // without - // sign bit + // CVC4 returns the mantissa with the sign bit, hence - 1 + final var mantWidthWithoutSignBit = Ints.checkedCast(fpType.significandWidth() - 1); final var sign = matcher.group("sign"); final var exp = matcher.group("exp"); From d9d2b3eb634f109da60f9e1997ce110bdef7f499 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 5 Sep 2025 18:10:38 +0200 Subject: [PATCH 49/67] Remove accidentally added class --- .../test/IndependentInterpolatingProverTest.java | 13 ------------- 1 file changed, 13 deletions(-) delete mode 100644 src/org/sosy_lab/java_smt/test/IndependentInterpolatingProverTest.java diff --git a/src/org/sosy_lab/java_smt/test/IndependentInterpolatingProverTest.java b/src/org/sosy_lab/java_smt/test/IndependentInterpolatingProverTest.java deleted file mode 100644 index b57c9e79c0..0000000000 --- a/src/org/sosy_lab/java_smt/test/IndependentInterpolatingProverTest.java +++ /dev/null @@ -1,13 +0,0 @@ -/* - * This file is part of JavaSMT, - * an API wrapper for a collection of SMT solvers: - * https://github.com/sosy-lab/java-smt - * - * SPDX-FileCopyrightText: 2024 Dirk Beyer - * - * SPDX-License-Identifier: Apache-2.0 - */ - -package org.sosy_lab.java_smt.test; - -public class IndependentInterpolatingProverTest extends InterpolatingProverTest {} From 1aba81dad9561d2b4fd619b43d4e20eedb21cd35 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 5 Sep 2025 18:11:43 +0200 Subject: [PATCH 50/67] Use the correct getter for mantissas in Z3FormulaCreator for FPs --- .../java_smt/solvers/z3/Z3FormulaCreator.java | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java index 31a8c6385a..e1e56a3b68 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -971,7 +971,7 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p expo, mant, pType.getExponentSize(), - pType.getMantissaSizeWithSignBit()); + pType.getMantissaSizeWithoutSignBit()); } else if (Native.fpaIsNumeralInf(environment, pValue)) { // Floating Point Inf uses: @@ -982,9 +982,9 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p return FloatingPointNumber.of( sign + "1".repeat(pType.getExponentSize()) - + "0".repeat(pType.getMantissaSizeWithSignBit()), + + "0".repeat(pType.getMantissaSizeWithoutSignBit()), pType.getExponentSize(), - pType.getMantissaSizeWithSignBit()); + pType.getMantissaSizeWithoutSignBit()); } else if (Native.fpaIsNumeralNan(environment, pValue)) { // TODO We are underspecified here and choose several bits on our own. @@ -996,9 +996,9 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p return FloatingPointNumber.of( "0" + "1".repeat(pType.getExponentSize()) - + "1".repeat(pType.getMantissaSizeWithSignBit()), + + "1".repeat(pType.getMantissaSizeWithoutSignBit()), pType.getExponentSize(), - pType.getMantissaSizeWithSignBit()); + pType.getMantissaSizeWithoutSignBit()); } else { Sign sign = getSign(pValue); @@ -1011,7 +1011,7 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p new BigInteger(exponent), new BigInteger(mantissa), pType.getExponentSize(), - pType.getMantissaSizeWithSignBit()); + pType.getMantissaSizeWithoutSignBit()); } } From dd83ed44e989176beac9fbbad05ea17ee948b1a7 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 7 Sep 2025 12:57:58 +0200 Subject: [PATCH 51/67] Split BV to FP to BV tests and remove solverSupportsNativeFPToBitvector() method --- .../test/FloatingPointFormulaManagerTest.java | 113 ++++++++++++------ .../java_smt/test/SolverBasedTest0.java | 11 -- 2 files changed, 75 insertions(+), 49 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 46467a8094..85b7788eec 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -1235,7 +1235,7 @@ public void fpModelValue() throws SolverException, InterruptedException { // exponent equal the total size. This test checks this, + that it holds with to/from IEEE // bitvector @Test - public void floatingPointMantissaSignBitWithBitvectorInterpretationSinglePrecision() { + public void bitvectorToFloatingPointMantissaSignBitInterpretationSinglePrecision() { int bvSize32 = singlePrecType.getTotalSize(); BitvectorFormula bvNumber32 = bvmgr.makeBitvector(bvSize32, BigInteger.ZERO); // Sanity checks @@ -1304,35 +1304,53 @@ public void floatingPointMantissaSignBitWithBitvectorInterpretationSinglePrecisi assertThat( ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)).getExponentSize()) .isEqualTo(singlePrecType.getExponentSize()); + } + + @Test + public void floatingPointMantissaSignBitWithBitvectorInterpretationSinglePrecision() { + requireFPToBitvector(); + + int bvSize32 = singlePrecType.getTotalSize(); + BitvectorFormula bvNumber32 = bvmgr.makeBitvector(bvSize32, BigInteger.ZERO); + FloatingPointFormula bvToFpSinglePrec = fpmgr.fromIeeeBitvector(bvNumber32, singlePrecType); + FloatingPointType fpTypeWithSignBit = + getFloatingPointTypeFromSizesWithSignBit( + singlePrecType.getExponentSize(), singlePrecType.getMantissaSizeWithSignBit()); + FloatingPointType fpTypeWithoutSignBit = + getFloatingPointTypeFromSizesWithoutSignBit( + singlePrecType.getExponentSize(), singlePrecType.getMantissaSizeWithoutSignBit()); + FloatingPointFormula bvToFpfpTypeWithSignBit = + fpmgr.fromIeeeBitvector(bvNumber32, fpTypeWithSignBit); + FloatingPointFormula bvToFpfpTypeWithoutSignBit = + fpmgr.fromIeeeBitvector(bvNumber32, fpTypeWithoutSignBit); - if (solverSupportsNativeFPToBitvector()) { - BitvectorFormula bvToFpSinglePrecToBv = fpmgr.toIeeeBitvector(bvToFpSinglePrec); - assertThat(bvmgr.getLength(bvToFpSinglePrecToBv)).isEqualTo(bvSize32); + // Check FP to BV conversion in regard to precision (all above is asserted in + // bitvectorToFloatingPointMantissaSignBitInterpretationSinglePrecision()) + BitvectorFormula bvToFpSinglePrecToBv = fpmgr.toIeeeBitvector(bvToFpSinglePrec); + assertThat(bvmgr.getLength(bvToFpSinglePrecToBv)).isEqualTo(bvSize32); - BitvectorFormula bvToFpTypeWithSignBitToBv = fpmgr.toIeeeBitvector(bvToFpfpTypeWithSignBit); - assertThat(bvmgr.getLength(bvToFpTypeWithSignBitToBv)).isEqualTo(bvSize32); + BitvectorFormula bvToFpTypeWithSignBitToBv = fpmgr.toIeeeBitvector(bvToFpfpTypeWithSignBit); + assertThat(bvmgr.getLength(bvToFpTypeWithSignBitToBv)).isEqualTo(bvSize32); - BitvectorFormula bvToFpTypeWithoutSignBitToBv = - fpmgr.toIeeeBitvector(bvToFpfpTypeWithoutSignBit); - assertThat(bvmgr.getLength(bvToFpTypeWithoutSignBitToBv)).isEqualTo(bvSize32); + BitvectorFormula bvToFpTypeWithoutSignBitToBv = + fpmgr.toIeeeBitvector(bvToFpfpTypeWithoutSignBit); + assertThat(bvmgr.getLength(bvToFpTypeWithoutSignBitToBv)).isEqualTo(bvSize32); - assume() - .withMessage( - "Bitwuzla equals on FPs/terms has a problem that needs to be addressed " + "first") - .that(solver) - .isNotEqualTo(Solvers.BITWUZLA); + assume() + .withMessage("Bitwuzla equals on FPs/terms has a problem that needs to be addressed first") + .that(solver) + .isNotEqualTo(Solvers.BITWUZLA); - assertThat(bvToFpSinglePrecToBv).isEqualTo(bvNumber32); - assertThat(bvToFpTypeWithSignBitToBv).isEqualTo(bvNumber32); - assertThat(bvToFpTypeWithoutSignBitToBv).isEqualTo(bvNumber32); - } + assertThat(bvToFpSinglePrecToBv).isEqualTo(bvNumber32); + assertThat(bvToFpTypeWithSignBitToBv).isEqualTo(bvNumber32); + assertThat(bvToFpTypeWithoutSignBitToBv).isEqualTo(bvNumber32); } // The standard defines the mantissa such that it includes the sign bit, and mantissa + - // exponent equal the total size. This test checks this, + that it holds with to/from IEEE - // bitvector + // exponent equal the total size. This test checks this, + that it holds with from + // bitvector to IEEE FP @Test - public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecision() { + public void bitvectorToFloatingPointMantissaSignBitInterpretationDoublePrecision() { int bvSize64 = doublePrecType.getTotalSize(); BitvectorFormula bvNumberSize64 = bvmgr.makeBitvector(bvSize64, BigInteger.ZERO); // Sanity checks @@ -1401,28 +1419,47 @@ public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecisi assertThat( ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)).getExponentSize()) .isEqualTo(doublePrecType.getExponentSize()); + } + + // Checks the correct precision/exponent/mantissa in FP to BV conversion + @Test + public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecision() { + requireFPToBitvector(); + + int bvSize64 = doublePrecType.getTotalSize(); + BitvectorFormula bvNumberSize64 = bvmgr.makeBitvector(bvSize64, BigInteger.ZERO); + FloatingPointFormula bvToFpDoublePrec = fpmgr.fromIeeeBitvector(bvNumberSize64, doublePrecType); + FloatingPointType fpTypeWithSignBit = + getFloatingPointTypeFromSizesWithSignBit( + doublePrecType.getExponentSize(), doublePrecType.getMantissaSizeWithSignBit()); + FloatingPointType fpTypeWithoutSignBit = + getFloatingPointTypeFromSizesWithoutSignBit( + doublePrecType.getExponentSize(), doublePrecType.getMantissaSizeWithoutSignBit()); + FloatingPointFormula bvToFpfpTypeWithSignBit = + fpmgr.fromIeeeBitvector(bvNumberSize64, fpTypeWithSignBit); + FloatingPointFormula bvToFpfpTypeWithoutSignBit = + fpmgr.fromIeeeBitvector(bvNumberSize64, fpTypeWithoutSignBit); - if (solverSupportsNativeFPToBitvector()) { - BitvectorFormula bvToFpDoublePrecToBv = fpmgr.toIeeeBitvector(bvToFpDoublePrec); - assertThat(bvmgr.getLength(bvToFpDoublePrecToBv)).isEqualTo(bvSize64); + // Check FP to BV conversion in regard to precision (all above is asserted in + // bitvectorToFloatingPointMantissaSignBitInterpretationDoublePrecision()) + BitvectorFormula bvToFpDoublePrecToBv = fpmgr.toIeeeBitvector(bvToFpDoublePrec); + assertThat(bvmgr.getLength(bvToFpDoublePrecToBv)).isEqualTo(bvSize64); - BitvectorFormula bvToFpTypeWithSignBitToBv = fpmgr.toIeeeBitvector(bvToFpfpTypeWithSignBit); - assertThat(bvmgr.getLength(bvToFpTypeWithSignBitToBv)).isEqualTo(bvSize64); + BitvectorFormula bvToFpTypeWithSignBitToBv = fpmgr.toIeeeBitvector(bvToFpfpTypeWithSignBit); + assertThat(bvmgr.getLength(bvToFpTypeWithSignBitToBv)).isEqualTo(bvSize64); - BitvectorFormula bvToFpTypeWithoutSignBitToBv = - fpmgr.toIeeeBitvector(bvToFpfpTypeWithoutSignBit); - assertThat(bvmgr.getLength(bvToFpTypeWithoutSignBitToBv)).isEqualTo(bvSize64); + BitvectorFormula bvToFpTypeWithoutSignBitToBv = + fpmgr.toIeeeBitvector(bvToFpfpTypeWithoutSignBit); + assertThat(bvmgr.getLength(bvToFpTypeWithoutSignBitToBv)).isEqualTo(bvSize64); - assume() - .withMessage( - "Bitwuzla equals on FPs/terms has a problem that needs to be addressed " + "first") - .that(solver) - .isNotEqualTo(Solvers.BITWUZLA); + assume() + .withMessage("Bitwuzla equals on FPs/terms has a problem that needs to be addressed first") + .that(solver) + .isNotEqualTo(Solvers.BITWUZLA); - assertThat(bvToFpTypeWithSignBitToBv).isEqualTo(bvNumberSize64); - assertThat(bvToFpDoublePrecToBv).isEqualTo(bvNumberSize64); - assertThat(bvToFpTypeWithoutSignBitToBv).isEqualTo(bvNumberSize64); - } + assertThat(bvToFpTypeWithSignBitToBv).isEqualTo(bvNumberSize64); + assertThat(bvToFpDoublePrecToBv).isEqualTo(bvNumberSize64); + assertThat(bvToFpTypeWithoutSignBitToBv).isEqualTo(bvNumberSize64); } @Test diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index df28a06069..e96c7b39f1 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -254,17 +254,6 @@ protected final void requireFPToBitvector() { } } - @SuppressWarnings("CheckReturnValue") - protected final boolean solverSupportsNativeFPToBitvector() { - requireFloats(); - try { - fpmgr.toIeeeBitvector(fpmgr.makeNumber(0, getSinglePrecisionFloatingPointType())); - return true; - } catch (UnsupportedOperationException e) { - return false; - } - } - /** Skip test if the solver does not support quantifiers. */ protected final void requireQuantifiers() { assume() From c83f96fd7b6124bb574fb672f79780cf622e5bf8 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 7 Sep 2025 14:54:27 +0200 Subject: [PATCH 52/67] Update all names referencing the hidden bit in Floating-Point precisions as sign bit to "hidden" bit --- .../java_smt/api/BitvectorFormulaManager.java | 6 +- .../api/FloatingPointFormulaManager.java | 10 +- .../java_smt/api/FloatingPointNumber.java | 92 +++++------ .../sosy_lab/java_smt/api/FormulaType.java | 127 +++++++-------- .../BitwuzlaFloatingPointManager.java | 10 +- .../bitwuzla/BitwuzlaFormulaCreator.java | 15 +- .../cvc4/CVC4FloatingPointFormulaManager.java | 25 +-- .../solvers/cvc4/CVC4FormulaCreator.java | 12 +- .../cvc5/CVC5FloatingPointFormulaManager.java | 52 +++--- .../solvers/cvc5/CVC5FormulaCreator.java | 14 +- .../Mathsat5AbstractNativeApiTest.java | 4 +- .../Mathsat5FloatingPointFormulaManager.java | 41 ++--- .../mathsat5/Mathsat5FormulaCreator.java | 6 +- .../solvers/mathsat5/Mathsat5NativeApi.java | 22 +-- .../z3/Z3FloatingPointFormulaManager.java | 6 +- .../java_smt/solvers/z3/Z3FormulaCreator.java | 16 +- .../test/FloatingPointFormulaManagerTest.java | 148 +++++++++--------- .../test/FloatingPointNumberTest.java | 8 +- .../java_smt/test/SolverVisitorTest.java | 7 +- 19 files changed, 319 insertions(+), 302 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java index 5d81bb8625..686500b882 100644 --- a/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java @@ -208,8 +208,8 @@ default BitvectorFormula modulo( *

We refer to the SMTLIB standard version 2.6 for the remainder operator in BV theory for * additional information. * - * @param dividend dividend of the operation. The sign bit is carried over from this bitvector for - * signed operations. + * @param dividend dividend of the operation. The hidden bit is carried over from this bitvector + * for signed operations. * @param divisor divisor of the operation. * @param signed whether to interpret all operands as signed or as unsigned numbers. */ @@ -407,7 +407,7 @@ default BitvectorFormula extract(BitvectorFormula number, int msb, int lsb, bool * * @param number The bitvector to extend. * @param extensionBits How many bits to add. - * @param signed Whether the extension should depend on the sign bit. + * @param signed Whether the extension should depend on the hidden bit. */ BitvectorFormula extend(BitvectorFormula number, int extensionBits, boolean signed); diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index a70d10544e..c3dd67e401 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -8,7 +8,7 @@ package org.sosy_lab.java_smt.api; -import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointTypeFromSizesWithoutSignBit; +import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointTypeFromSizesWithoutHiddenBit; import java.math.BigDecimal; import java.math.BigInteger; @@ -99,8 +99,8 @@ default FloatingPointFormula makeNumber(FloatingPointNumber number) { number.getExponent(), number.getMantissa(), number.getMathSign(), - getFloatingPointTypeFromSizesWithoutSignBit( - number.getExponentSize(), number.getMantissaSizeWithoutSignBit())); + getFloatingPointTypeFromSizesWithoutHiddenBit( + number.getExponentSize(), number.getMantissaSizeWithoutHiddenBit())); } /** @@ -276,7 +276,7 @@ FloatingPointFormula castFrom( /** * Create a formula that interprets the given bitvector as a floating-point value in the IEEE * format, according to the given type. The sum of the sizes of exponent and mantissa of the - * target type plus 1 (for the sign bit) needs to be equal to the size of the bitvector. + * target type plus 1 (for the hidden bit) needs to be equal to the size of the bitvector. * *

Note: This method will return a value that is (numerically) far away from the original * value. This method is completely different from {@link #castFrom}, which will produce a @@ -287,7 +287,7 @@ FloatingPointFormula castFrom( /** * Create a formula that produces a representation of the given floating-point value as a * bitvector conforming to the IEEE format. The size of the resulting bitvector is the sum of the - * sizes of the exponent and mantissa of the input formula plus 1 (for the sign bit). + * sizes of the exponent and mantissa of the input formula plus 1 (for the hidden bit). */ BitvectorFormula toIeeeBitvector(FloatingPointFormula number); diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index 5099f9ddc5..12b479171e 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -23,11 +23,11 @@ @AutoValue public abstract class FloatingPointNumber { - // Mantissas do not include the sign bit + // Mantissas do not include the hidden bit public static final int SINGLE_PRECISION_EXPONENT_SIZE = 8; - public static final int SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT = 23; + public static final int SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT = 23; public static final int DOUBLE_PRECISION_EXPONENT_SIZE = 11; - public static final int DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT = 52; + public static final int DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT = 52; public enum Sign { POSITIVE, @@ -86,36 +86,36 @@ public final boolean getSign() { * bit. * * @deprecated this method can be confusing, as the SMTLIB2 standard expects the mantissa to - * include the sign bit, but this does not. Use {@link #getMantissaSizeWithoutSignBit()} - * instead if you want the mantissa without the sign bit, and {@link - * #getMantissaSizeWithSignBit()} if you want it to include the sign bit. + * include the hidden bit, but this does not. Use {@link #getMantissaSizeWithoutHiddenBit()} + * instead if you want the mantissa without the hidden bit, and {@link + * #getMantissaSizeWithHiddenBit()} if you want it to include the hidden bit. */ @Deprecated(since = "6.0", forRemoval = true) - @InlineMe(replacement = "this.getMantissaSizeWithoutSignBit()") + @InlineMe(replacement = "this.getMantissaSizeWithoutHiddenBit()") public final int getMantissaSize() { - return getMantissaSizeWithoutSignBit(); + return getMantissaSizeWithoutHiddenBit(); } /** - * Returns the size of the mantissa (also called a coefficient or significant), excluding the sign - * bit. + * Returns the size of the mantissa (also called a coefficient or significant), excluding the + * hidden bit. */ - public abstract int getMantissaSizeWithoutSignBit(); + public abstract int getMantissaSizeWithoutHiddenBit(); /** - * Returns the size of the mantissa (also called a coefficient or significant), including the sign - * bit. + * Returns the size of the mantissa (also called a coefficient or significant), including the + * hidden bit. */ - public int getMantissaSizeWithSignBit() { - return getMantissaSizeWithoutSignBit() + 1; + public int getMantissaSizeWithHiddenBit() { + return getMantissaSizeWithoutHiddenBit() + 1; } /** * Returns the size of the precision, i.e. the size of the exponent + the size of the mantissa - * including sign bit. + * including hidden bit. */ public int getTotalSize() { - return getMantissaSizeWithSignBit() + getExponentSize(); + return getMantissaSizeWithHiddenBit() + getExponentSize(); } /** @@ -128,8 +128,8 @@ public int getTotalSize() { * @param mantissa the mantissa of the floating-point number, given as unsigned (not negative) * number without hidden bit * @param exponentSize the (maximum) size of the exponent in bits - * @param mantissaSizeWithoutSignBit the (maximum) size of the mantissa in bits (excluding the - * sign bit) + * @param mantissaSizeWithoutHiddenBit the (maximum) size of the mantissa in bits (excluding the + * hidden bit) * @see #of(Sign, BigInteger, BigInteger, int, int) */ @Deprecated( @@ -138,7 +138,7 @@ public int getTotalSize() { @InlineMe( replacement = "FloatingPointNumber.of(Sign.of(sign), exponent, mantissa, exponentSize," - + " mantissaSizeWithoutSignBit)", + + " mantissaSizeWithoutHiddenBit)", imports = { "org.sosy_lab.java_smt.api.FloatingPointNumber", "org.sosy_lab.java_smt.api.FloatingPointNumber.Sign" @@ -148,8 +148,8 @@ public static FloatingPointNumber of( BigInteger exponent, BigInteger mantissa, int exponentSize, - int mantissaSizeWithoutSignBit) { - return of(Sign.of(sign), exponent, mantissa, exponentSize, mantissaSizeWithoutSignBit); + int mantissaSizeWithoutHiddenBit) { + return of(Sign.of(sign), exponent, mantissa, exponentSize, mantissaSizeWithoutHiddenBit); } /** @@ -161,78 +161,82 @@ public static FloatingPointNumber of( * @param mantissa the mantissa of the floating-point number, given as unsigned (not negative) * number without hidden bit * @param exponentSize the (maximum) size of the exponent in bits - * @param mantissaSizeWithoutSignBit the (maximum) size of the mantissa in bits (excluding the - * sign bit) + * @param mantissaSizeWithoutHiddenBit the (maximum) size of the mantissa in bits (excluding the + * hidden bit) */ public static FloatingPointNumber of( Sign sign, BigInteger exponent, BigInteger mantissa, int exponentSize, - int mantissaSizeWithoutSignBit) { + int mantissaSizeWithoutHiddenBit) { Preconditions.checkArgument(exponent.bitLength() <= exponentSize); - Preconditions.checkArgument(mantissa.bitLength() <= mantissaSizeWithoutSignBit); + Preconditions.checkArgument(mantissa.bitLength() <= mantissaSizeWithoutHiddenBit); Preconditions.checkArgument(exponent.compareTo(BigInteger.ZERO) >= 0); Preconditions.checkArgument(mantissa.compareTo(BigInteger.ZERO) >= 0); return new AutoValue_FloatingPointNumber( - sign, exponent, mantissa, exponentSize, mantissaSizeWithoutSignBit); + sign, exponent, mantissa, exponentSize, mantissaSizeWithoutHiddenBit); } /** * Get a floating-point number encoded as bitvector as defined by IEEE 754. * - * @param bits the bit-representation of the floating-point number, consisting of sign bit, + * @param bits the bit-representation of the floating-point number, consisting of hidden bit, * exponent (without bias) and mantissa (without hidden bit) in this exact ordering * @param exponentSize the size of the exponent in bits - * @param mantissaSizeWithoutSignBit the size of the mantissa in bits (excluding the sign bit) + * @param mantissaSizeWithoutHiddenBit the size of the mantissa in bits (excluding the hidden bit) */ public static FloatingPointNumber of( - String bits, int exponentSize, int mantissaSizeWithoutSignBit) { + String bits, int exponentSize, int mantissaSizeWithoutHiddenBit) { Preconditions.checkArgument(0 < exponentSize); - Preconditions.checkArgument(0 < mantissaSizeWithoutSignBit); + Preconditions.checkArgument(0 < mantissaSizeWithoutHiddenBit); Preconditions.checkArgument( - bits.length() == 1 + exponentSize + mantissaSizeWithoutSignBit, + bits.length() == 1 + exponentSize + mantissaSizeWithoutHiddenBit, "Bitsize (%s) of floating point numeral does not match the size of sign, exponent and " + "mantissa (%s + %s + %s).", bits.length(), 1, exponentSize, - mantissaSizeWithoutSignBit); + mantissaSizeWithoutHiddenBit); Preconditions.checkArgument(bits.chars().allMatch(c -> c == '0' || c == '1')); Sign sign = Sign.of(bits.charAt(0) == '1'); BigInteger exponent = new BigInteger(bits.substring(1, 1 + exponentSize), 2); BigInteger mantissa = new BigInteger( - bits.substring(1 + exponentSize, 1 + exponentSize + mantissaSizeWithoutSignBit), 2); - return of(sign, exponent, mantissa, exponentSize, mantissaSizeWithoutSignBit); + bits.substring(1 + exponentSize, 1 + exponentSize + mantissaSizeWithoutHiddenBit), 2); + return of(sign, exponent, mantissa, exponentSize, mantissaSizeWithoutHiddenBit); } /** * Returns true if this floating-point number is an IEEE-754-2008 single precision type with 32 - * bits length consisting of an 8 bit exponent, a 24 bit mantissa (including the sign bit). + * bits length consisting of an 8 bit exponent, a 24 bit mantissa (including the hidden bit). * * @return true for IEEE-754 single precision type, false otherwise. */ public boolean isIEEE754SinglePrecision() { - // Mantissa does not include the sign bit internally + // Mantissa does not include the hidden bit internally return getTotalSize() - == SINGLE_PRECISION_EXPONENT_SIZE + SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT + 1 + == SINGLE_PRECISION_EXPONENT_SIZE + + SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT + + 1 && getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE - && getMantissaSizeWithoutSignBit() == SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT; + && getMantissaSizeWithoutHiddenBit() == SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT; } /** * Returns true if this floating-point number is an IEEE-754-2008 double precision type with 64 - * bits length consisting of an 11 bit exponent, a 53 bit mantissa (including the sign bit). + * bits length consisting of an 11 bit exponent, a 53 bit mantissa (including the hidden bit). * * @return true for IEEE-754 double precision type, false otherwise. */ public boolean isIEEE754DoublePrecision() { - // Mantissa does not include the sign bit internally + // Mantissa does not include the hidden bit internally return getTotalSize() - == DOUBLE_PRECISION_EXPONENT_SIZE + DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT + 1 + == DOUBLE_PRECISION_EXPONENT_SIZE + + DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT + + 1 && getExponentSize() == DOUBLE_PRECISION_EXPONENT_SIZE - && getMantissaSizeWithoutSignBit() == DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT; + && getMantissaSizeWithoutHiddenBit() == DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT; } /** compute a representation as Java-based float value, if possible. */ @@ -260,7 +264,7 @@ public double doubleValue() { } private BitSet getBits() { - var mantissaSizeWithoutSign = getMantissaSizeWithoutSignBit(); + var mantissaSizeWithoutSign = getMantissaSizeWithoutHiddenBit(); var exponentSize = getExponentSize(); var mantissa = getMantissa(); var exponent = getExponent(); diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index 8701a29038..c69f8c5417 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -9,9 +9,9 @@ package org.sosy_lab.java_smt.api; import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_EXPONENT_SIZE; -import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT; +import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT; import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_EXPONENT_SIZE; -import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_SIGN_BIT; +import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT; import com.google.common.base.Joiner; import com.google.common.base.Preconditions; @@ -208,75 +208,80 @@ public String toSMTLIBString() { /** * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes. - * The mantissa size is expected to not include the sign bit. + * The mantissa size is expected to not include the hidden bit. * * @deprecated this method can be confusing, as the SMTLIB2 standard expects the mantissa to - * include the sign bit, but this method expects the mantissa argument without the sign bit. - * Use {@link #getFloatingPointTypeFromSizesWithoutSignBit(int, int)} instead if you want to - * construct a {@link FloatingPointType} with the constructing method treating the mantissa - * argument without the sign bit, and {@link #getFloatingPointTypeFromSizesWithSignBit(int, - * int)} if you want it to include the sign bit in the size of the mantissa argument. + * include the hidden bit, but this method expects the mantissa argument without the hidden + * bit. Use {@link #getFloatingPointTypeFromSizesWithoutHiddenBit(int, int)} instead if you + * want to construct a {@link FloatingPointType} with the constructing method treating the + * mantissa argument without the hidden bit, and {@link + * #getFloatingPointTypeFromSizesWithHiddenBit(int, int)} if you want it to include the hidden + * bit in the size of the mantissa argument. * @param exponentSize size of the exponent for the base of the floating-point - * @param mantissaSizeWithoutSignBit size of the mantissa (also called a coefficient or - * significant), excluding the sign bit. + * @param mantissaSizeWithoutHiddenBit size of the mantissa (also called a coefficient or + * significant), excluding the hidden bit. * @return the newly constructed {@link FloatingPointType}. */ @Deprecated(since = "6.0", forRemoval = true) @InlineMe( replacement = - "FormulaType.getFloatingPointTypeFromSizesWithoutSignBit(exponentSize," - + " mantissaSizeWithoutSignBit)", + "FormulaType.getFloatingPointTypeFromSizesWithoutHiddenBit(exponentSize," + + " mantissaSizeWithoutHiddenBit)", imports = "org.sosy_lab.java_smt.api.FormulaType") public static FloatingPointType getFloatingPointType( - int exponentSize, int mantissaSizeWithoutSignBit) { - return getFloatingPointTypeFromSizesWithoutSignBit(exponentSize, mantissaSizeWithoutSignBit); + int exponentSize, int mantissaSizeWithoutHiddenBit) { + return getFloatingPointTypeFromSizesWithoutHiddenBit( + exponentSize, mantissaSizeWithoutHiddenBit); } /** * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes. - * The mantissa size is expected to not include the sign bit. The total size of the constructed + * The mantissa size is expected to not include the hidden bit. The total size of the constructed * type is equal to the addition of the two arguments plus one, as in: total size == exponentSize - * + mantissaSizeWithoutSignBit + 1. + * + mantissaSizeWithoutHiddenBit + 1. * *

Using the arguments e and m, calling this method with - * getFloatingPointTypeFromSizesWithoutSignBit (e, m) returns a type equal to a type constructed - * by {@link #getFloatingPointTypeFromSizesWithSignBit(int, int)} with the same arguments e and m - * as before, but m incremented by 1, as in getFloatingPointTypeFromSizesWithSignBit(e, m + 1). + * getFloatingPointTypeFromSizesWithoutHiddenBit (e, m) returns a type equal to a type constructed + * by {@link #getFloatingPointTypeFromSizesWithHiddenBit(int, int)} with the same arguments e and + * m as before, but m incremented by 1, as in getFloatingPointTypeFromSizesWithHiddenBit(e, m + + * 1). * * @param exponentSize size of the exponent for the base of the floating-point - * @param mantissaSizeWithoutSignBit size of the mantissa (also called a coefficient or - * significant), excluding the sign bit. + * @param mantissaSizeWithoutHiddenBit size of the mantissa (also called a coefficient or + * significant), excluding the hidden bit. * @return the newly constructed {@link FloatingPointType}. */ - public static FloatingPointType getFloatingPointTypeFromSizesWithoutSignBit( - int exponentSize, int mantissaSizeWithoutSignBit) { - return new FloatingPointType(exponentSize, mantissaSizeWithoutSignBit); + public static FloatingPointType getFloatingPointTypeFromSizesWithoutHiddenBit( + int exponentSize, int mantissaSizeWithoutHiddenBit) { + return new FloatingPointType(exponentSize, mantissaSizeWithoutHiddenBit); } /** * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes. - * The mantissa size is expected to include the sign bit. The total size of the constructed type + * The mantissa size is expected to include the hidden bit. The total size of the constructed type * is equal to the addition of the two arguments, as in: total size == exponentSize + - * mantissaSizeWithSignBit. + * mantissaSizeWithHiddenBit. * *

Using the arguments e and m, calling this method with - * getFloatingPointTypeFromSizesWithSignBit(e, m) returns a type equal to a type constructed by - * {@link #getFloatingPointTypeFromSizesWithoutSignBit(int, int)} with the same arguments e and m - * as before, but m decremented by 1, as in getFloatingPointTypeFromSizesWithoutSignBit(e, m - 1). + * getFloatingPointTypeFromSizesWithHiddenBit(e, m) returns a type equal to a type constructed by + * {@link #getFloatingPointTypeFromSizesWithoutHiddenBit(int, int)} with the same arguments e and + * m as before, but m decremented by 1, as in getFloatingPointTypeFromSizesWithoutHiddenBit(e, m - + * 1). * * @param exponentSize size of the exponent for the base of the floating-point - * @param mantissaSizeWithSignBit size of the mantissa (also called a coefficient or significant), - * including the sign bit. + * @param mantissaSizeWithHiddenBit size of the mantissa (also called a coefficient or + * significant), including the hidden bit. * @return the newly constructed {@link FloatingPointType}. */ - public static FloatingPointType getFloatingPointTypeFromSizesWithSignBit( - int exponentSize, int mantissaSizeWithSignBit) { - return getFloatingPointTypeFromSizesWithoutSignBit(exponentSize, mantissaSizeWithSignBit - 1); + public static FloatingPointType getFloatingPointTypeFromSizesWithHiddenBit( + int exponentSize, int mantissaSizeWithHiddenBit) { + return getFloatingPointTypeFromSizesWithoutHiddenBit( + exponentSize, mantissaSizeWithHiddenBit - 1); } /** * @return single precision {@link FloatingPointType} with exponent sized 8, and mantissa sized 24 - * (including the sign bit). + * (including the hidden bit). */ public static FloatingPointType getSinglePrecisionFloatingPointType() { return FloatingPointType.SINGLE_PRECISION_FP_TYPE; @@ -284,7 +289,7 @@ public static FloatingPointType getSinglePrecisionFloatingPointType() { /** * @return double precision {@link FloatingPointType} with exponent sized 11, and mantissa sized - * 53 (including the sign bit). + * 53 (including the hidden bit). */ public static FloatingPointType getDoublePrecisionFloatingPointType() { return FloatingPointType.DOUBLE_PRECISION_FP_TYPE; @@ -295,19 +300,19 @@ public static final class FloatingPointType extends FormulaType

We refer to the SMTLIB standard version 2.6 for the remainder operator in BV theory for * additional information. * - * @param dividend dividend of the operation. The hidden bit is carried over from this bitvector - * for signed operations. + * @param dividend dividend of the operation. The sign bit is carried over from this bitvector for + * signed operations. * @param divisor divisor of the operation. * @param signed whether to interpret all operands as signed or as unsigned numbers. */ @@ -407,7 +407,7 @@ default BitvectorFormula extract(BitvectorFormula number, int msb, int lsb, bool * * @param number The bitvector to extend. * @param extensionBits How many bits to add. - * @param signed Whether the extension should depend on the hidden bit. + * @param signed Whether the extension should depend on the sign bit. */ BitvectorFormula extend(BitvectorFormula number, int extensionBits, boolean signed); From 00dc03397166c31a2fc5913e55689a542ae5fa2a Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 7 Sep 2025 15:09:56 +0200 Subject: [PATCH 54/67] Improve some JavaDoc in FloatingPointFormulaManager.java in relation to FP sizes and the hidden bit --- .../sosy_lab/java_smt/api/FloatingPointFormulaManager.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index c3dd67e401..e8c7377604 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -275,8 +275,8 @@ FloatingPointFormula castFrom( /** * Create a formula that interprets the given bitvector as a floating-point value in the IEEE - * format, according to the given type. The sum of the sizes of exponent and mantissa of the - * target type plus 1 (for the hidden bit) needs to be equal to the size of the bitvector. + * format, according to the given type. The sum of the sizes of exponent and mantissa (including + * the hidden bit) of the target type needs to be equal to the size of the bitvector. * *

Note: This method will return a value that is (numerically) far away from the original * value. This method is completely different from {@link #castFrom}, which will produce a @@ -287,7 +287,7 @@ FloatingPointFormula castFrom( /** * Create a formula that produces a representation of the given floating-point value as a * bitvector conforming to the IEEE format. The size of the resulting bitvector is the sum of the - * sizes of the exponent and mantissa of the input formula plus 1 (for the hidden bit). + * sizes of the exponent and mantissa (including the hidden bit) of the input formula. */ BitvectorFormula toIeeeBitvector(FloatingPointFormula number); From 20a8f4829765db9527c460e34c76ffc87a24de60 Mon Sep 17 00:00:00 2001 From: BaierD Date: Thu, 11 Sep 2025 22:28:38 +0200 Subject: [PATCH 55/67] Add tests for FP type (precision) toString(), fromString(), and toSMTLIB2String() --- .../test/FloatingPointNumberTest.java | 74 +++++++++++++++++++ 1 file changed, 74 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java index 218311854b..93239822d3 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java @@ -14,12 +14,19 @@ import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT; import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_EXPONENT_SIZE; import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT; +import static org.sosy_lab.java_smt.api.FormulaType.getDoublePrecisionFloatingPointType; +import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointTypeFromSizesWithHiddenBit; +import static org.sosy_lab.java_smt.api.FormulaType.getSinglePrecisionFloatingPointType; import com.google.common.base.Strings; +import com.google.common.collect.ImmutableSet; import java.math.BigInteger; +import java.util.Set; import org.junit.Test; import org.sosy_lab.java_smt.api.FloatingPointNumber; import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; public class FloatingPointNumberTest { @@ -99,4 +106,71 @@ public void floatingPointNumberWithArbitraryPrecision() { assertThrows(IllegalArgumentException.class, fpNum::floatValue); assertThrows(IllegalArgumentException.class, fpNum::doubleValue); } + + private static final Set precisionsToTest = + ImmutableSet.of( + getSinglePrecisionFloatingPointType(), + getDoublePrecisionFloatingPointType(), + getFloatingPointTypeFromSizesWithHiddenBit(8, 24), + getFloatingPointTypeFromSizesWithHiddenBit(8, 23), + getFloatingPointTypeFromSizesWithHiddenBit(8, 25), + getFloatingPointTypeFromSizesWithHiddenBit(11, 53), + getFloatingPointTypeFromSizesWithHiddenBit(11, 54), + getFloatingPointTypeFromSizesWithHiddenBit(11, 55), + getFloatingPointTypeFromSizesWithHiddenBit(10, 54), + getFloatingPointTypeFromSizesWithHiddenBit(12, 54), + getFloatingPointTypeFromSizesWithHiddenBit(7, 24), + getFloatingPointTypeFromSizesWithHiddenBit(9, 24)); + + @Test + public void precisionToString() { + for (FloatingPointType precisionToTest : precisionsToTest) { + String singlePrecString = precisionToTest.toString(); + FormulaType typeFromString = FormulaType.fromString(singlePrecString); + assertThat(typeFromString.isFloatingPointType()).isTrue(); + FloatingPointType fpTypeFromString = (FloatingPointType) typeFromString; + assertThat(fpTypeFromString.getTotalSize()).isEqualTo(precisionToTest.getTotalSize()); + assertThat(fpTypeFromString.getExponentSize()).isEqualTo(precisionToTest.getExponentSize()); + assertThat(fpTypeFromString.getMantissaSizeWithoutHiddenBit()) + .isEqualTo(precisionToTest.getMantissaSizeWithoutHiddenBit()); + assertThat(fpTypeFromString.getMantissaSizeWithHiddenBit()) + .isEqualTo(precisionToTest.getMantissaSizeWithHiddenBit()); + assertThat(typeFromString).isEqualTo(precisionToTest); + } + } + + @Test + public void precisionToSMTLIB2String() { + for (FloatingPointType precisionToTest : precisionsToTest) { + String smtlib2StringFromPrecision = precisionToTest.toSMTLIBString(); + String expectedString1 = + "(_ FloatingPoint " + + precisionToTest.getExponentSize() + + " " + + precisionToTest.getMantissaSizeWithHiddenBit() + + ")"; + assertThat(smtlib2StringFromPrecision).isEqualTo(expectedString1); + String expectedString2 = + "(_ FloatingPoint " + + precisionToTest.getExponentSize() + + " " + + (precisionToTest.getMantissaSizeWithoutHiddenBit() + 1) + + ")"; + assertThat(smtlib2StringFromPrecision).isEqualTo(expectedString2); + } + } + + @Test + public void singlePrecisionToSMTLIB2String() { + String singlePrecSMTLIB2String = getSinglePrecisionFloatingPointType().toSMTLIBString(); + // We know the expected SMTLIB2 String + assertThat(singlePrecSMTLIB2String).isEqualTo("(_ FloatingPoint 8 24)"); + } + + @Test + public void doublePrecisionToSMTLIB2String() { + String singlePrecSMTLIB2String = getDoublePrecisionFloatingPointType().toSMTLIBString(); + // We know the expected SMTLIB2 String + assertThat(singlePrecSMTLIB2String).isEqualTo("(_ FloatingPoint 11 53)"); + } } From 6769850d921cd41a8cda14d881b73ead9a804588 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 12 Sep 2025 09:21:14 +0200 Subject: [PATCH 56/67] Remove @InlineMe annotation for deprecated call getMantissaSize(), as there are 2 possible replacements and the user should decide which fits best --- src/org/sosy_lab/java_smt/api/FloatingPointNumber.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index 12b479171e..557d2b0e8e 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -91,7 +91,6 @@ public final boolean getSign() { * #getMantissaSizeWithHiddenBit()} if you want it to include the hidden bit. */ @Deprecated(since = "6.0", forRemoval = true) - @InlineMe(replacement = "this.getMantissaSizeWithoutHiddenBit()") public final int getMantissaSize() { return getMantissaSizeWithoutHiddenBit(); } From 015c145971212370583861ed420d9f6d7ca4e5cc Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 12 Sep 2025 09:23:07 +0200 Subject: [PATCH 57/67] Remove @InlineMe annotation for deprecated call getMantissaSize(), as there are 2 possible replacements and the user should decide which fits best --- src/org/sosy_lab/java_smt/api/FloatingPointNumber.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index 557d2b0e8e..7dd6b77605 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -91,6 +91,7 @@ public final boolean getSign() { * #getMantissaSizeWithHiddenBit()} if you want it to include the hidden bit. */ @Deprecated(since = "6.0", forRemoval = true) + @SuppressWarnings("InlineMeSuggester") public final int getMantissaSize() { return getMantissaSizeWithoutHiddenBit(); } From 9aff78a2bfecf2fe34f768cb323131c38514dcbf Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 12 Sep 2025 10:10:36 +0200 Subject: [PATCH 58/67] Disable parts of FP to IEEE BV tests for Z3, as it returns a query instead of a const BV --- .../test/FloatingPointFormulaManagerTest.java | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 9d72a9c773..c2e915dc0c 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -12,6 +12,7 @@ import static com.google.common.truth.Truth.assertWithMessage; import static com.google.common.truth.TruthJUnit.assume; import static org.junit.Assert.assertThrows; +import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.Z3; import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointTypeFromSizesWithHiddenBit; import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointTypeFromSizesWithoutHiddenBit; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; @@ -605,7 +606,7 @@ public void numberConstants() throws SolverException, InterruptedException { assertThatFormula(fpmgr.isNegative(nj2)).isTautological(); // Z3 supports at least FloatingPointType(15, 112). Larger types seem to be rounded. - if (!ImmutableSet.of(Solvers.Z3, Solvers.CVC4).contains(solver)) { + if (!ImmutableSet.of(Z3, Solvers.CVC4).contains(solver)) { // check unequality for very large types FloatingPointType largeType = getFloatingPointTypeFromSizesWithoutHiddenBit(100, 100); FloatingPointFormula k1 = @@ -1342,6 +1343,13 @@ public void floatingPointMantissaSignBitWithBitvectorInterpretationSinglePrecisi .that(solver) .isNotEqualTo(Solvers.BITWUZLA); + // Z3 returns "(fp.to_ieee_bv ((_ to_fp 8 24) #x00000000))" for bvNumber32, which is valid, + // but we should ask whether they can improve this + assume() + .withMessage("Z3 returns a formula consisting of the transformation") + .that(solver) + .isNotEqualTo(Z3); + assertThat(bvToFpSinglePrecToBv).isEqualTo(bvNumber32); assertThat(bvToFpTypeWithSignBitToBv).isEqualTo(bvNumber32); assertThat(bvToFpTypeWithoutSignBitToBv).isEqualTo(bvNumber32); @@ -1459,6 +1467,11 @@ public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecisi .that(solver) .isNotEqualTo(Solvers.BITWUZLA); + assume() + .withMessage("Z3 returns a formula consisting of the transformation") + .that(solver) + .isNotEqualTo(Z3); + assertThat(bvToFpTypeWithSignBitToBv).isEqualTo(bvNumberSize64); assertThat(bvToFpDoublePrecToBv).isEqualTo(bvNumberSize64); assertThat(bvToFpTypeWithoutSignBitToBv).isEqualTo(bvNumberSize64); From ddac0782fc3850a1ce32efb05d64dbea96faf596 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 12 Sep 2025 10:51:55 +0200 Subject: [PATCH 59/67] Enable FP to IEEE BV precision tests for Z3 and Bitwuzla fully by using the solver to check equality instead of equals() --- .../test/FloatingPointFormulaManagerTest.java | 40 +++++-------------- 1 file changed, 10 insertions(+), 30 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index c2e915dc0c..3854a7a776 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -1309,7 +1309,8 @@ public void bitvectorToFloatingPointMantissaSignBitInterpretationSinglePrecision } @Test - public void floatingPointMantissaSignBitWithBitvectorInterpretationSinglePrecision() { + public void floatingPointMantissaSignBitWithBitvectorInterpretationSinglePrecision() + throws SolverException, InterruptedException { requireFPToBitvector(); int bvSize32 = singlePrecType.getTotalSize(); @@ -1338,21 +1339,9 @@ public void floatingPointMantissaSignBitWithBitvectorInterpretationSinglePrecisi fpmgr.toIeeeBitvector(bvToFpfpTypeWithoutSignBit); assertThat(bvmgr.getLength(bvToFpTypeWithoutSignBitToBv)).isEqualTo(bvSize32); - assume() - .withMessage("Bitwuzla equals on FPs/terms has a problem that needs to be addressed first") - .that(solver) - .isNotEqualTo(Solvers.BITWUZLA); - - // Z3 returns "(fp.to_ieee_bv ((_ to_fp 8 24) #x00000000))" for bvNumber32, which is valid, - // but we should ask whether they can improve this - assume() - .withMessage("Z3 returns a formula consisting of the transformation") - .that(solver) - .isNotEqualTo(Z3); - - assertThat(bvToFpSinglePrecToBv).isEqualTo(bvNumber32); - assertThat(bvToFpTypeWithSignBitToBv).isEqualTo(bvNumber32); - assertThat(bvToFpTypeWithoutSignBitToBv).isEqualTo(bvNumber32); + assertThatFormula(bvmgr.equal(bvToFpSinglePrecToBv, bvNumber32)).isTautological(); + assertThatFormula(bvmgr.equal(bvToFpTypeWithSignBitToBv, bvNumber32)).isTautological(); + assertThatFormula(bvmgr.equal(bvToFpTypeWithoutSignBitToBv, bvNumber32)).isTautological(); } // The standard defines the mantissa such that it includes the hidden bit, and mantissa + @@ -1433,7 +1422,8 @@ public void bitvectorToFloatingPointMantissaSignBitInterpretationDoublePrecision // Checks the correct precision/exponent/mantissa in FP to BV conversion @Test - public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecision() { + public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecision() + throws SolverException, InterruptedException { requireFPToBitvector(); int bvSize64 = doublePrecType.getTotalSize(); @@ -1462,19 +1452,9 @@ public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecisi fpmgr.toIeeeBitvector(bvToFpfpTypeWithoutSignBit); assertThat(bvmgr.getLength(bvToFpTypeWithoutSignBitToBv)).isEqualTo(bvSize64); - assume() - .withMessage("Bitwuzla equals on FPs/terms has a problem that needs to be addressed first") - .that(solver) - .isNotEqualTo(Solvers.BITWUZLA); - - assume() - .withMessage("Z3 returns a formula consisting of the transformation") - .that(solver) - .isNotEqualTo(Z3); - - assertThat(bvToFpTypeWithSignBitToBv).isEqualTo(bvNumberSize64); - assertThat(bvToFpDoublePrecToBv).isEqualTo(bvNumberSize64); - assertThat(bvToFpTypeWithoutSignBitToBv).isEqualTo(bvNumberSize64); + assertThatFormula(bvmgr.equal(bvToFpTypeWithSignBitToBv, bvNumberSize64)).isTautological(); + assertThatFormula(bvmgr.equal(bvToFpDoublePrecToBv, bvNumberSize64)).isTautological(); + assertThatFormula(bvmgr.equal(bvToFpTypeWithoutSignBitToBv, bvNumberSize64)).isTautological(); } @Test From 52d6e30837cef30534c1842d9098f386a2a4e8b1 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 12 Sep 2025 12:05:17 +0200 Subject: [PATCH 60/67] Re-add removed FP single/double mantissa size constants and deprecate them so that we can remove them from the public API --- .../java_smt/api/FloatingPointNumber.java | 25 ++++++++++++++++--- .../sosy_lab/java_smt/api/FormulaType.java | 3 +++ 2 files changed, 25 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index 7dd6b77605..41d79d4fa2 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -23,11 +23,30 @@ @AutoValue public abstract class FloatingPointNumber { - // Mantissas do not include the hidden bit + // TODO: remove deprecated constants from public API after 6.0 release (and delete the unused). + @Deprecated(since = "6.0", forRemoval = true) public static final int SINGLE_PRECISION_EXPONENT_SIZE = 8; - public static final int SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT = 23; + + /** + * @deprecated this constant can be confusing, as the SMTLIB2 standard expects the mantissa to + * include the hidden bit, but this constant does not. + */ + @Deprecated(since = "6.0", forRemoval = true) + public static final int SINGLE_PRECISION_MANTISSA_SIZE = 23; + + protected static final int SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT = 23; + + @Deprecated(since = "6.0", forRemoval = true) public static final int DOUBLE_PRECISION_EXPONENT_SIZE = 11; - public static final int DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT = 52; + + /** + * @deprecated this constant can be confusing, as the SMTLIB2 standard expects the mantissa to + * include the hidden bit, but this constant does not. + */ + @Deprecated(since = "6.0", forRemoval = true) + public static final int DOUBLE_PRECISION_MANTISSA_SIZE = 52; + + protected static final int DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT = 52; public enum Sign { POSITIVE, diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index c69f8c5417..4c1cb1a899 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -298,9 +298,12 @@ public static FloatingPointType getDoublePrecisionFloatingPointType() { @Immutable public static final class FloatingPointType extends FormulaType { + @SuppressWarnings("removal") private static final FloatingPointType SINGLE_PRECISION_FP_TYPE = new FloatingPointType( SINGLE_PRECISION_EXPONENT_SIZE, SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT); + + @SuppressWarnings("removal") private static final FloatingPointType DOUBLE_PRECISION_FP_TYPE = new FloatingPointType( DOUBLE_PRECISION_EXPONENT_SIZE, DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT); From 5dd10cadeed11ed4902735e99a75f33ba08b5004 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 12 Sep 2025 12:05:54 +0200 Subject: [PATCH 61/67] Add FP single/double precision sizes to FloatingPointNumberTest.java, as we don't want to use the deprecated public API --- .../sosy_lab/java_smt/test/FloatingPointNumberTest.java | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java index 93239822d3..fdc057e907 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java @@ -10,10 +10,6 @@ import static com.google.common.truth.Truth.assertThat; import static org.junit.Assert.assertThrows; -import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_EXPONENT_SIZE; -import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT; -import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_EXPONENT_SIZE; -import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT; import static org.sosy_lab.java_smt.api.FormulaType.getDoublePrecisionFloatingPointType; import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointTypeFromSizesWithHiddenBit; import static org.sosy_lab.java_smt.api.FormulaType.getSinglePrecisionFloatingPointType; @@ -30,6 +26,11 @@ public class FloatingPointNumberTest { + private static final int SINGLE_PRECISION_EXPONENT_SIZE = 8; + private static final int SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT = 23; + private static final int DOUBLE_PRECISION_EXPONENT_SIZE = 11; + private static final int DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT = 52; + @Test public void floatingPointNumberWithSinglePrecision() { for (float f : From e08a75aff8d7552a3d60da0517edd887ccc64a71 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 12 Sep 2025 12:48:54 +0200 Subject: [PATCH 62/67] Fix incorrect JavaDoc for FP precision total size API and make the calculation explicit in the code --- src/org/sosy_lab/java_smt/api/FloatingPointNumber.java | 6 +++--- src/org/sosy_lab/java_smt/api/FormulaType.java | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index 41d79d4fa2..071a1a7635 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -130,11 +130,11 @@ public int getMantissaSizeWithHiddenBit() { } /** - * Returns the size of the precision, i.e. the size of the exponent + the size of the mantissa - * including hidden bit. + * Returns the size of the precision, i.e. the single sign bit + the size of the exponent + the + * size of the mantissa (excluding the hidden bit). */ public int getTotalSize() { - return getMantissaSizeWithHiddenBit() + getExponentSize(); + return getMantissaSizeWithoutHiddenBit() + getExponentSize() + 1; } /** diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index 4c1cb1a899..3d9d4bdc26 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -359,11 +359,11 @@ public int getMantissaSizeWithHiddenBit() { } /** - * Return the total size of a value of this type in bits. Equal to exponent + mantissa - * (including the hidden bit). + * Return the total size of a value of this type in bits. Equal to sign bit + size of the + * exponent + size of the mantissa (excluding the hidden bit). */ public int getTotalSize() { - return exponentSize + getMantissaSizeWithHiddenBit(); + return exponentSize + getMantissaSizeWithoutHiddenBit() + 1; } @Override From bd8c6bd1858f93faf7526bc0dcff3e923b21c2c8 Mon Sep 17 00:00:00 2001 From: "Baier D." Date: Mon, 22 Sep 2025 13:48:56 +0200 Subject: [PATCH 63/67] Explicitly name sign bit in FloatingPointNumber constructor JavaDoc, as it is used when constructing Co-authored-by: Philipp Wendler <2545335+PhilippWendler@users.noreply.github.com> --- src/org/sosy_lab/java_smt/api/FloatingPointNumber.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index 071a1a7635..0c312a4aef 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -200,7 +200,7 @@ public static FloatingPointNumber of( /** * Get a floating-point number encoded as bitvector as defined by IEEE 754. * - * @param bits the bit-representation of the floating-point number, consisting of hidden bit, + * @param bits the bit-representation of the floating-point number, consisting of sign bit, * exponent (without bias) and mantissa (without hidden bit) in this exact ordering * @param exponentSize the size of the exponent in bits * @param mantissaSizeWithoutHiddenBit the size of the mantissa in bits (excluding the hidden bit) From 55901fc7667df9a9b17a6e9aa8200f9eb9c6349a Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 22 Sep 2025 13:18:45 +0200 Subject: [PATCH 64/67] Remove @InlineMe from deprecated method getFloatingPointType() so that users explicitly have to choose one of the 2 successor methods --- src/org/sosy_lab/java_smt/api/FormulaType.java | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index 3d9d4bdc26..b1063b77bf 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -18,7 +18,6 @@ import com.google.common.base.Splitter; import com.google.common.collect.ImmutableSet; import com.google.errorprone.annotations.Immutable; -import com.google.errorprone.annotations.InlineMe; import java.util.List; import java.util.Set; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; @@ -223,11 +222,7 @@ public String toSMTLIBString() { * @return the newly constructed {@link FloatingPointType}. */ @Deprecated(since = "6.0", forRemoval = true) - @InlineMe( - replacement = - "FormulaType.getFloatingPointTypeFromSizesWithoutHiddenBit(exponentSize," - + " mantissaSizeWithoutHiddenBit)", - imports = "org.sosy_lab.java_smt.api.FormulaType") + @SuppressWarnings("InlineMeSuggester") public static FloatingPointType getFloatingPointType( int exponentSize, int mantissaSizeWithoutHiddenBit) { return getFloatingPointTypeFromSizesWithoutHiddenBit( From b835125f3f8e912064005f8e3c01518f63a1a7af Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 22 Sep 2025 13:19:39 +0200 Subject: [PATCH 65/67] Rename wrongly named variable in Mathsat5 FP impl --- .../mathsat5/Mathsat5AbstractNativeApiTest.java | 12 +++++++----- .../solvers/mathsat5/Mathsat5FormulaCreator.java | 10 +++++----- 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java index a7bbeecf1a..9ab45b19ff 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java @@ -93,9 +93,10 @@ public void fpMantissaDoesNotIncludeSignBit() { assertThat(msat_get_bv_type_size(env, msat_term_get_type(bvNumber))).isEqualTo(totalBVSize); int exponent = 8; - int mantissaWithoutSign = 23; // excluding hidden bit - long fpSinglePrecType = msat_get_fp_type(env, exponent, mantissaWithoutSign); - assertThat(msat_get_fp_type_mant_width(env, fpSinglePrecType)).isEqualTo(mantissaWithoutSign); + int mantissaWithoutHiddenBit = 23; + long fpSinglePrecType = msat_get_fp_type(env, exponent, mantissaWithoutHiddenBit); + assertThat(msat_get_fp_type_mant_width(env, fpSinglePrecType)) + .isEqualTo(mantissaWithoutHiddenBit); assertThat(msat_get_fp_type_exp_width(env, fpSinglePrecType)).isEqualTo(exponent); // total size is exp + man + 1 assertThat( @@ -105,10 +106,11 @@ public void fpMantissaDoesNotIncludeSignBit() { .isEqualTo(totalBVSize); long bvToFpSinglePrec = - Mathsat5NativeApi.msat_make_fp_from_ieeebv(env, exponent, mantissaWithoutSign, bvNumber); + Mathsat5NativeApi.msat_make_fp_from_ieeebv( + env, exponent, mantissaWithoutHiddenBit, bvNumber); assertThat(msat_type_equals(msat_term_get_type(bvToFpSinglePrec), fpSinglePrecType)).isTrue(); assertThat(msat_get_fp_type_mant_width(env, msat_term_get_type(bvToFpSinglePrec))) - .isEqualTo(mantissaWithoutSign); + .isEqualTo(mantissaWithoutHiddenBit); assertThat(msat_get_fp_type_exp_width(env, msat_term_get_type(bvToFpSinglePrec))) .isEqualTo(exponent); diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java index c3a9e6a148..c199cc4cc2 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -581,13 +581,13 @@ private FloatingPointNumber parseFloatingPoint(String lTermRepresentation) { BigInteger bits = new BigInteger(matcher.group(1)); int expWidth = Integer.parseInt(matcher.group(2)); // The term representation in MathSAT5 does not include the hidden bit - int mantWidthWithoutSignBit = Integer.parseInt(matcher.group(3)); + int mantWidthWithoutHiddenBit = Integer.parseInt(matcher.group(3)); - Sign sign = Sign.of(bits.testBit(expWidth + mantWidthWithoutSignBit)); - BigInteger exponent = extractBitsFrom(bits, mantWidthWithoutSignBit, expWidth); - BigInteger mantissa = extractBitsFrom(bits, 0, mantWidthWithoutSignBit); + Sign sign = Sign.of(bits.testBit(expWidth + mantWidthWithoutHiddenBit)); + BigInteger exponent = extractBitsFrom(bits, mantWidthWithoutHiddenBit, expWidth); + BigInteger mantissa = extractBitsFrom(bits, 0, mantWidthWithoutHiddenBit); - return FloatingPointNumber.of(sign, exponent, mantissa, expWidth, mantWidthWithoutSignBit); + return FloatingPointNumber.of(sign, exponent, mantissa, expWidth, mantWidthWithoutHiddenBit); } /** From 056ca12d6823bae1616f51b7a572905c277b4eaa Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 22 Sep 2025 13:21:54 +0200 Subject: [PATCH 66/67] Rename wrongly named variable in CVC4 FP impl --- .../sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java index 0b9abcf4bd..f6a3979024 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -630,7 +630,7 @@ private FloatingPointNumber convertFloatingPoint(Expr fpExpr) { final var fpType = fp.getT(); final var expWidth = Ints.checkedCast(fpType.exponentWidth()); // CVC4 returns the mantissa with the hidden bit, hence - 1 - final var mantWidthWithoutSignBit = Ints.checkedCast(fpType.significandWidth() - 1); + final var mantWidthWithoutHiddenBit = Ints.checkedCast(fpType.significandWidth() - 1); final var sign = matcher.group("sign"); final var exp = matcher.group("exp"); @@ -638,13 +638,13 @@ private FloatingPointNumber convertFloatingPoint(Expr fpExpr) { Preconditions.checkArgument("1".equals(sign) || "0".equals(sign)); Preconditions.checkArgument(exp.length() == expWidth); - Preconditions.checkArgument(mant.length() == mantWidthWithoutSignBit); + Preconditions.checkArgument(mant.length() == mantWidthWithoutHiddenBit); return FloatingPointNumber.of( Sign.of(sign.charAt(0) == '1'), new BigInteger(exp, 2), new BigInteger(mant, 2), expWidth, - mantWidthWithoutSignBit); + mantWidthWithoutHiddenBit); } } From 234452d9421ff325d6cc9367c176efcebea3c219 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 22 Sep 2025 13:45:14 +0200 Subject: [PATCH 67/67] Change comment about total FP precision size in fromIeeeBitvectorImpl() for CVC4/5 to reflect what we do in the method better --- .../java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java | 2 +- .../java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java | 2 +- 2 files changed, 2 insertions(+), 2 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 e0e059671a..29fe7b2c4d 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -358,7 +358,7 @@ protected Expr isNegative(Expr pParam) { protected Expr fromIeeeBitvectorImpl(Expr pBitvector, FloatingPointType pTargetType) { int mantissaSizeWithoutHiddenBit = pTargetType.getMantissaSizeWithoutHiddenBit(); int size = pTargetType.getTotalSize(); - // total size = mantissa without hidden bit + hidden bit + exponent + // total size = mantissa without hidden bit + sign bit + exponent assert size == mantissaSizeWithoutHiddenBit + 1 + pTargetType.getExponentSize(); Expr signExtract = exprManager.mkConst(new BitVectorExtract(size - 1, size - 1)); 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 1f000b881f..32c6f7c7ef 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -413,7 +413,7 @@ protected Term isNegative(Term pParam) { protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetType) { int mantissaSizeWithoutHiddenBit = pTargetType.getMantissaSizeWithoutHiddenBit(); int size = pTargetType.getTotalSize(); - // total size = mantissa without hidden bit + hidden bit + exponent + // total size = mantissa without hidden bit + sign bit + exponent assert size == mantissaSizeWithoutHiddenBit + 1 + pTargetType.getExponentSize(); Op signExtract;