diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index 62bb3afbe4..e8c7377604 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.getFloatingPointTypeFromSizesWithoutHiddenBit; 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.getMantissaSize())); + getFloatingPointTypeFromSizesWithoutHiddenBit( + number.getExponentSize(), number.getMantissaSizeWithoutHiddenBit())); } /** @@ -274,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 sign 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 @@ -286,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 (including the hidden bit) of the input formula. */ 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 fe3c14b1ca..0c312a4aef 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -23,11 +23,31 @@ @AutoValue public abstract class FloatingPointNumber { + // 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; + + /** + * @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; + + /** + * @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, NEGATIVE; @@ -80,7 +100,42 @@ public final boolean getSign() { public abstract int getExponentSize(); - public abstract int getMantissaSize(); + /** + * 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 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) + @SuppressWarnings("InlineMeSuggester") + public final int getMantissaSize() { + return getMantissaSizeWithoutHiddenBit(); + } + + /** + * Returns the size of the mantissa (also called a coefficient or significant), excluding the + * hidden bit. + */ + public abstract int getMantissaSizeWithoutHiddenBit(); + + /** + * Returns the size of the mantissa (also called a coefficient or significant), including the + * hidden bit. + */ + public int getMantissaSizeWithHiddenBit() { + return getMantissaSizeWithoutHiddenBit() + 1; + } + + /** + * 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 getMantissaSizeWithoutHiddenBit() + getExponentSize() + 1; + } /** * Get a floating-point number with the given sign, exponent, and mantissa. @@ -92,7 +147,8 @@ 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 mantissaSizeWithoutHiddenBit the (maximum) size of the mantissa in bits (excluding the + * hidden bit) * @see #of(Sign, BigInteger, BigInteger, int, int) */ @Deprecated( @@ -100,14 +156,19 @@ public final boolean getSign() { forRemoval = true) @InlineMe( replacement = - "FloatingPointNumber.of(Sign.of(sign), exponent, mantissa, exponentSize, mantissaSize)", + "FloatingPointNumber.of(Sign.of(sign), exponent, mantissa, exponentSize," + + " mantissaSizeWithoutHiddenBit)", 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 mantissaSizeWithoutHiddenBit) { + return of(Sign.of(sign), exponent, mantissa, exponentSize, mantissaSizeWithoutHiddenBit); } /** @@ -119,15 +180,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 + * @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 mantissaSize) { + Sign sign, + BigInteger exponent, + BigInteger mantissa, + int exponentSize, + int mantissaSizeWithoutHiddenBit) { Preconditions.checkArgument(exponent.bitLength() <= exponentSize); - Preconditions.checkArgument(mantissa.bitLength() <= mantissaSize); + 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, mantissaSize); + return new AutoValue_FloatingPointNumber( + sign, exponent, mantissa, exponentSize, mantissaSizeWithoutHiddenBit); } /** @@ -136,47 +203,59 @@ 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 mantissaSizeWithoutHiddenBit the size of the mantissa in bits (excluding the hidden bit) */ - public static FloatingPointNumber of(String bits, int exponentSize, int mantissaSize) { + public static FloatingPointNumber of( + String bits, int exponentSize, int mantissaSizeWithoutHiddenBit) { Preconditions.checkArgument(0 < exponentSize); - Preconditions.checkArgument(0 < mantissaSize); + Preconditions.checkArgument(0 < mantissaSizeWithoutHiddenBit); Preconditions.checkArgument( - bits.length() == 1 + exponentSize + mantissaSize, + 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, - mantissaSize); + 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 + mantissaSize), 2); - return of(sign, exponent, mantissa, exponentSize, mantissaSize); + new BigInteger( + 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 23 bit mantissa and a single 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() { - return getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE - && getMantissaSize() == SINGLE_PRECISION_MANTISSA_SIZE; + // Mantissa does not include the hidden bit internally + return getTotalSize() + == SINGLE_PRECISION_EXPONENT_SIZE + + SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT + + 1 + && getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE + && 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 52 bit mantissa and a single 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() { - return getExponentSize() == DOUBLE_PRECISION_EXPONENT_SIZE - && getMantissaSize() == DOUBLE_PRECISION_MANTISSA_SIZE; + // Mantissa does not include the hidden bit internally + return getTotalSize() + == DOUBLE_PRECISION_EXPONENT_SIZE + + DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT + + 1 + && getExponentSize() == DOUBLE_PRECISION_EXPONENT_SIZE + && getMantissaSizeWithoutHiddenBit() == DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT; } /** compute a representation as Java-based float value, if possible. */ @@ -204,18 +283,18 @@ public double doubleValue() { } private BitSet getBits() { - var mantissaSize = getMantissaSize(); + var mantissaSizeWithoutSign = getMantissaSizeWithoutHiddenBit(); var exponentSize = getExponentSize(); var mantissa = getMantissa(); var exponent = getExponent(); - var bits = new BitSet(1 + exponentSize + mantissaSize); + var bits = new BitSet(getTotalSize()); 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; @@ -227,7 +306,7 @@ private BitSet getBits() { */ @Override public final String toString() { - var length = 1 + getExponentSize() + getMantissaSize(); + var length = getTotalSize(); var str = new StringBuilder(length); var bits = getBits(); for (int i = 0; i < length; i++) { diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index d5beea79cc..8c2462ff28 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_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; +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; @@ -205,14 +205,87 @@ 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 hidden bit. + * + * @deprecated this method can be confusing, as the SMTLIB2 standard expects the mantissa to + * 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 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) + @SuppressWarnings("InlineMeSuggester") + public static FloatingPointType getFloatingPointType( + 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 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 + * + mantissaSizeWithoutHiddenBit + 1. + * + *

Using the arguments e and m, calling this method with + * 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 mantissaSizeWithoutHiddenBit size of the mantissa (also called a coefficient or + * significant), excluding the hidden bit. + * @return the newly constructed {@link FloatingPointType}. + */ + 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 hidden bit. The total size of the constructed type + * is equal to the addition of the two arguments, as in: total size == exponentSize + + * mantissaSizeWithHiddenBit. + * + *

Using the arguments e and m, calling this method with + * 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 mantissaSizeWithHiddenBit size of the mantissa (also called a coefficient or + * significant), including the hidden bit. + * @return the newly constructed {@link FloatingPointType}. + */ + 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 hidden 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 hidden bit). + */ public static FloatingPointType getDoublePrecisionFloatingPointType() { return FloatingPointType.DOUBLE_PRECISION_FP_TYPE; } @@ -220,17 +293,24 @@ 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); + 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); + new FloatingPointType( + DOUBLE_PRECISION_EXPONENT_SIZE, DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT); private final int exponentSize; - private final int mantissaSize; + // The SMTLib2 standard defines the mantissa size as including the hidden bit. We do not include + // it here though. + private final int mantissaSizeWithoutHiddenBit; - private FloatingPointType(int pExponentSize, int pMantissaSize) { + private FloatingPointType(int pExponentSize, int pMantissaSizeWithoutHiddenBit) { exponentSize = pExponentSize; - mantissaSize = pMantissaSize; + mantissaSizeWithoutHiddenBit = pMantissaSizeWithoutHiddenBit; } @Override @@ -238,22 +318,52 @@ public boolean isFloatingPointType() { return true; } + /** Returns the size of the exponent. */ public int getExponentSize() { return exponentSize; } + /** + * Returns the size of the mantissa (also called a coefficient or significant), excluding the + * hidden bit. + * + * @deprecated this method can be confusing, as the SMTLIB2 standard expects the mantissa to + * 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) public int getMantissaSize() { - return mantissaSize; + return mantissaSizeWithoutHiddenBit; + } + + /** + * Returns the size of the mantissa (also called a coefficient or significant), excluding the + * hidden bit. + */ + public int getMantissaSizeWithoutHiddenBit() { + return mantissaSizeWithoutHiddenBit; + } + + /** + * Returns the size of the mantissa (also called a coefficient or significant), including the + * hidden bit. + */ + public int getMantissaSizeWithHiddenBit() { + return mantissaSizeWithoutHiddenBit + 1; } - /** Return the total size of a value of this type in bits. */ + /** + * 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 + mantissaSize + 1; + return exponentSize + getMantissaSizeWithoutHiddenBit() + 1; } @Override public int hashCode() { - return (31 + exponentSize) * 31 + mantissaSize; + return (31 + exponentSize) * 31 + mantissaSizeWithoutHiddenBit; } @Override @@ -265,17 +375,20 @@ 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.mantissaSizeWithoutHiddenBit == other.mantissaSizeWithoutHiddenBit; } @Override public String toString() { - return "FloatingPoint"; + // We align what we do here with the SMTLIB2 standard, which expects the hidden bit to be part + // of the mantissa. + return "FloatingPoint"; } @Override public String toSMTLIBString() { - return "(_ FloatingPoint " + exponentSize + " " + mantissaSize + ")"; + return "(_ FloatingPoint " + exponentSize + " " + getMantissaSizeWithHiddenBit() + ")"; } } @@ -476,16 +589,18 @@ public static FormulaType fromString(String t) { } else if (FloatingPointRoundingModeType.toString().equals(t)) { return FloatingPointRoundingModeType; } else if (t.startsWith("FloatingPoint<")) { - // FloatingPoint + // Example: FloatingPoint List exman = Splitter.on(',').limit(2).splitToList(t.substring(14, t.length() - 1)); - return FormulaType.getFloatingPointType( + // We align what we do here with the SMTLIB2 standard, which expects the hidden bit to be part + // of the mantissa. + return FormulaType.getFloatingPointTypeFromSizesWithHiddenBit( Integer.parseInt(exman.get(0).substring(4)), Integer.parseInt(exman.get(1).substring(5))); } else if (t.startsWith("Bitvector<")) { - // Bitvector<32> + // Example: Bitvector<32> return FormulaType.getBitvectorTypeWithSize( Integer.parseInt(t.substring(10, t.length() - 1))); } else if (t.matches(".*\\(.*\\)")) { - // Color (Red, Green, Blue) + // Example: Color (Red, Green, Blue) String name = t.substring(0, t.indexOf("(") - 1); String elementsStr = t.substring(t.indexOf("(") + 1, t.length() - 1); Set elements = ImmutableSet.copyOf(Splitter.on(", ").split(elementsStr)); 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..f09184129e 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.getMantissaSizeWithoutHiddenBit()); 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.getMantissaSizeWithHiddenBit()); } 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.getMantissaSizeWithHiddenBit()); } else { return termManager.mk_term( Kind.FP_TO_FP_FROM_UBV, roundingMode, pNumber, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithHiddenBit()); } } 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.getMantissaSizeWithHiddenBit()); } @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..8be8041462 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.getMantissaSizeWithHiddenBit()); } @Override @@ -170,8 +170,9 @@ 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.getFloatingPointType(exponent, mantissa); + int mantissaWithHiddenBit = pSort.fp_sig_size(); + return FormulaType.getFloatingPointTypeFromSizesWithHiddenBit( + exponent, mantissaWithHiddenBit); } else if (pSort.is_bv()) { return FormulaType.getBitvectorTypeWithSize(pSort.bv_size()); } else if (pSort.is_array()) { @@ -379,8 +380,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.getFloatingPointType(exp, man); + int mantissaWithHiddenBit = sort.fp_sig_size(); + return (FormulaType) + FormulaType.getFloatingPointTypeFromSizesWithHiddenBit(exp, mantissaWithHiddenBit); } else if (sort.is_rm()) { return (FormulaType) FormulaType.FloatingPointRoundingModeType; } @@ -590,9 +592,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 mantissaSizeWithoutHiddenBit = sort.fp_sig_size() - 1; + return FloatingPointNumber.of(term.to_bv(), exponentSize, mantissaSizeWithoutHiddenBit); } throw new AssertionError("Unknown value type."); } 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..29fe7b2c4d 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.getMantissaSize(); - return new FloatingPointSize(pExponentSize, pMantissaSize + 1); // plus sign bit + return new FloatingPointSize(pType.getExponentSize(), pType.getMantissaSizeWithHiddenBit()); } @Override @@ -89,11 +86,12 @@ 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.getMantissaSizeWithoutHiddenBit()); 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.getMantissaSizeWithHiddenBit(), bitVector); return exprManager.mkConst(fp); } @@ -109,7 +107,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.getMantissaSizeWithoutHiddenBit(), pType.getExponentSize()); if (rat.greater(Rational.fromDecimal(upperBound.negate().toString())) && rat.less(Rational.fromDecimal(upperBound.toString()))) { @@ -126,10 +124,10 @@ 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 mantissaWithoutHiddenBit, 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 = boundExponent - 2 - mantissaWithoutHiddenBit; if (mantissaExponent >= 0) { // ignore negative mantissaExponent upperBoundExponent = upperBoundExponent.subtract(BigInteger.valueOf(2).pow(mantissaExponent)); } @@ -218,8 +216,8 @@ protected Expr castFromImpl( } else if (formulaType.isBitvectorType()) { long pExponentSize = pTargetType.getExponentSize(); - long pMantissaSize = pTargetType.getMantissaSize(); - FloatingPointSize fpSize = new FloatingPointSize(pExponentSize, pMantissaSize + 1); + long pMantissaSize = pTargetType.getMantissaSizeWithHiddenBit(); + FloatingPointSize fpSize = new FloatingPointSize(pExponentSize, pMantissaSize); FloatingPointConvertSort fpConvert = new FloatingPointConvertSort(fpSize); final Expr op; if (pSigned) { @@ -357,19 +355,21 @@ protected Expr isNegative(Expr pParam) { } @Override - protected Expr fromIeeeBitvectorImpl(Expr bitvector, FloatingPointType pTargetType) { - int mantissaSize = pTargetType.getMantissaSize(); - int exponentSize = pTargetType.getExponentSize(); + protected Expr fromIeeeBitvectorImpl(Expr pBitvector, FloatingPointType pTargetType) { + int mantissaSizeWithoutHiddenBit = pTargetType.getMantissaSizeWithoutHiddenBit(); int size = pTargetType.getTotalSize(); - assert size == mantissaSize + exponentSize + 1; + // 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)); - 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 exponentExtract = + exprManager.mkConst(new BitVectorExtract(size - 2, mantissaSizeWithoutHiddenBit)); + Expr mantissaExtract = + exprManager.mkConst(new BitVectorExtract(mantissaSizeWithoutHiddenBit - 1, 0)); + + 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); } 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..f6a3979024 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.getMantissaSizeWithHiddenBit()); } @Override @@ -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.getFloatingPointType( - (int) fpType.getExponentSize(), - (int) fpType.getSignificandSize() - 1); // without sign bit + FormulaType.getFloatingPointTypeFromSizesWithHiddenBit( + (int) fpType.getExponentSize(), (int) fpType.getSignificandSize()); // with hidden 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.getFloatingPointType( - (int) fpType.getExponentSize(), - (int) fpType.getSignificandSize() - 1); // without sign bit + return FormulaType.getFloatingPointTypeFromSizesWithHiddenBit( + (int) fpType.getExponentSize(), (int) fpType.getSignificandSize()); // with hidden 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 + // CVC4 returns the mantissa with the hidden bit, hence - 1 + final var mantWidthWithoutHiddenBit = Ints.checkedCast(fpType.significandWidth() - 1); 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() == mantWidthWithoutHiddenBit); return FloatingPointNumber.of( Sign.of(sign.charAt(0) == '1'), new BigInteger(exp, 2), new BigInteger(mant, 2), expWidth, - mantWidth); + mantWidthWithoutHiddenBit); } } 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..32c6f7c7ef 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,8 @@ 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.getMantissaSizeWithoutHiddenBit(), mantissa.toString(16), 16)); } catch (CVC5ApiException e) { throw new IllegalArgumentException("You tried creating a invalid bitvector", e); @@ -90,7 +91,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.getMantissaSizeWithHiddenBit()); } } catch (CVC5ApiException | NumberFormatException e) { // ignore and fallback to floating point from rational numbers @@ -102,7 +103,7 @@ protected Term makeNumberAndRound(String pN, FloatingPointType pType, Term pRoun termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_REAL, pType.getExponentSize(), - pType.getMantissaSize() + 1); + pType.getMantissaSizeWithHiddenBit()); 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 +112,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 hidden bit)" + + pType.getMantissaSizeWithHiddenBit() + " and value " + pN + ".", @@ -152,13 +153,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.getMantissaSizeWithHiddenBit()); } 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() + + " and mantissa size (including the hidden bit)" + + pType.getMantissaSizeWithHiddenBit() + ".", e); } @@ -168,13 +169,13 @@ protected Term makePlusInfinityImpl(FloatingPointType pType) { protected Term makeMinusInfinityImpl(FloatingPointType pType) { try { return termManager.mkFloatingPointNegInf( - pType.getExponentSize(), pType.getMantissaSize() + 1); + pType.getExponentSize(), pType.getMantissaSizeWithHiddenBit()); } 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() + + " and mantissa size (including the hidden bit)" + + pType.getMantissaSizeWithHiddenBit() + ".", e); } @@ -183,13 +184,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.getMantissaSizeWithHiddenBit()); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid NaN with exponent size " + pType.getExponentSize() - + " and mantissa size " - + pType.getMantissaSize() + + " and mantissa size (including the hidden bit)" + + pType.getMantissaSizeWithHiddenBit() + ".", e); } @@ -205,7 +207,7 @@ protected Term castToImpl( termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_FP, ((FloatingPointType) pTargetType).getExponentSize(), - ((FloatingPointType) pTargetType).getMantissaSize() + 1); + ((FloatingPointType) pTargetType).getMantissaSizeWithHiddenBit()); return termManager.mkTerm(fpToFp, pRoundingMode, pNumber); } else if (pTargetType.isBitvectorType()) { @@ -246,7 +248,7 @@ protected Term castFromImpl( termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_REAL, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithHiddenBit()); return termManager.mkTerm(realToFp, pRoundingMode, pNumber); @@ -256,14 +258,14 @@ protected Term castFromImpl( termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_SBV, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithHiddenBit()); return termManager.mkTerm(realToSBv, pRoundingMode, pNumber); } else { Op realToUBv = termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_UBV, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithHiddenBit()); return termManager.mkTerm(realToUBv, pRoundingMode, pNumber); } @@ -277,8 +279,8 @@ protected Term castFromImpl( + pNumber + " into a FloatingPoint with exponent size " + pTargetType.getExponentSize() - + " and mantissa size " - + pTargetType.getMantissaSize() + + " and mantissa size (including the hidden bit)" + + pTargetType.getMantissaSizeWithHiddenBit() + ".", e); } @@ -408,27 +410,29 @@ protected Term isNegative(Term pParam) { } @Override - protected Term fromIeeeBitvectorImpl(Term bitvector, FloatingPointType pTargetType) { - int mantissaSize = pTargetType.getMantissaSize(); - int exponentSize = pTargetType.getExponentSize(); + protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetType) { + int mantissaSizeWithoutHiddenBit = pTargetType.getMantissaSizeWithoutHiddenBit(); int size = pTargetType.getTotalSize(); - assert size == mantissaSize + exponentSize + 1; + // total size = mantissa without hidden bit + sign bit + exponent + assert size == mantissaSizeWithoutHiddenBit + 1 + 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, mantissaSizeWithoutHiddenBit); + mantissaExtract = + termManager.mkOp(Kind.BITVECTOR_EXTRACT, mantissaSizeWithoutHiddenBit - 1, 0); } catch (CVC5ApiException e) { throw new IllegalArgumentException( - "You tried creating a invalid bitvector extract in term " + bitvector + ".", e); + "You tried creating a invalid bitvector extract in term " + pBitvector + ".", e); } - Term sign = termManager.mkTerm(signExtract, bitvector); - Term exponent = termManager.mkTerm(exponentExtract, bitvector); - Term mantissa = termManager.mkTerm(mantissaExtract, bitvector); + 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); } 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..15cefc9eab 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -141,15 +141,16 @@ public Sort getBitvectorType(int pBitwidth) { @Override public Sort getFloatingPointType(FloatingPointType pType) { try { - // plus sign bit - return termManager.mkFloatingPointSort(pType.getExponentSize(), pType.getMantissaSize() + 1); + // plus hidden bit + return termManager.mkFloatingPointSort( + pType.getExponentSize(), pType.getMantissaSizeWithHiddenBit()); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "Cannot create floatingpoint sort with exponent size " + pType.getExponentSize() + " and mantissa " - + pType.getMantissaSize() - + " (plus sign bit).", + + pType.getMantissaSizeWithHiddenBit() + + " (including hidden bit).", e); } } @@ -222,9 +223,9 @@ private FormulaType getFormulaTypeFromTermType(Sort sort) { } else if (sort.isBitVector()) { 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( - sort.getFloatingPointExponentSize(), sort.getFloatingPointSignificandSize() - 1); + // CVC5 wants the hidden bit as part of the mantissa. We add that manually in creation. + return FormulaType.getFloatingPointTypeFromSizesWithHiddenBit( + sort.getFloatingPointExponentSize(), sort.getFloatingPointSignificandSize()); } else if (sort.isRoundingMode()) { return FormulaType.FloatingPointRoundingModeType; } else if (sort.isReal()) { @@ -838,7 +839,7 @@ public Object convertValue(Term expForType, Term value) { private FloatingPointNumber convertFloatingPoint(Term value) throws CVC5ApiException { final var fpValue = value.getFloatingPointValue(); final var expWidth = Ints.checkedCast(fpValue.first); - final var mantWidth = Ints.checkedCast(fpValue.second - 1); // without sign bit + final var mantWidth = Ints.checkedCast(fpValue.second - 1); // without hidden bit final var bvValue = fpValue.third; Preconditions.checkState(bvValue.isBitVectorValue()); final var bits = bvValue.getBitVectorValue(); 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..9ab45b19ff 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,46 @@ 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 hidden 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 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( + 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, 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(mantissaWithoutHiddenBit); + 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); 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..1302f2d0d5 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,42 @@ 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 hidden bit + final String mantissaStr = + getBvRepresentation(mantissa, type.getMantissaSizeWithoutHiddenBit()); 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.getMantissaSizeWithoutHiddenBit()); } @Override protected Long makeNumberAndRound(String pN, FloatingPointType pType, Long pRoundingMode) { try { if (isNegativeZero(Double.valueOf(pN))) { + // MathSAT5 expects the mantissa to not include the hidden bit return msat_make_fp_neg( mathsatEnv, msat_make_fp_rat_number( - mathsatEnv, "0", pType.getExponentSize(), pType.getMantissaSize(), pRoundingMode)); + mathsatEnv, + "0", + pType.getExponentSize(), + pType.getMantissaSizeWithoutHiddenBit(), + pRoundingMode)); } } catch (NumberFormatException e) { // ignore and fallback to floating point from rational numbers } + // MathSAT5 expects the mantissa to not include the hidden bit return msat_make_fp_rat_number( - mathsatEnv, pN, pType.getExponentSize(), pType.getMantissaSize(), pRoundingMode); + mathsatEnv, + pN, + pType.getExponentSize(), + pType.getMantissaSizeWithoutHiddenBit(), + pRoundingMode); } @Override @@ -132,17 +147,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 hidden bit + return msat_make_fp_plus_inf( + mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithoutHiddenBit()); } @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 hidden bit + return msat_make_fp_minus_inf( + mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithoutHiddenBit()); } @Override protected Long makeNaNImpl(FloatingPointType type) { - return msat_make_fp_nan(mathsatEnv, type.getExponentSize(), type.getMantissaSize()); + // MathSAT5 expects the mantissa to not include the hidden bit + return msat_make_fp_nan( + mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithoutHiddenBit()); } @Override @@ -150,10 +171,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 hidden bit return msat_make_fp_cast( mathsatEnv, targetType.getExponentSize(), - targetType.getMantissaSize(), + targetType.getMantissaSizeWithoutHiddenBit(), pRoundingMode, pNumber); @@ -179,18 +201,19 @@ protected Long castFromImpl( return castToImpl(pNumber, pSigned, pTargetType, pRoundingMode); } else if (formulaType.isBitvectorType()) { + // MathSAT5 expects the mantissa to not include the hidden bit if (pSigned) { return msat_make_fp_from_sbv( mathsatEnv, pTargetType.getExponentSize(), - pTargetType.getMantissaSize(), + pTargetType.getMantissaSizeWithoutHiddenBit(), pRoundingMode, pNumber); } else { return msat_make_fp_from_ubv( mathsatEnv, pTargetType.getExponentSize(), - pTargetType.getMantissaSize(), + pTargetType.getMantissaSizeWithoutHiddenBit(), pRoundingMode, pNumber); } @@ -214,8 +237,12 @@ private Long genericCast(Long pNumber, FormulaType pTargetType) { @Override protected Long fromIeeeBitvectorImpl(Long pNumber, FloatingPointType pTargetType) { + // MathSAT5 expects the mantissa to not include the hidden bit return Mathsat5NativeApi.msat_make_fp_from_ieeebv( - mathsatEnv, pTargetType.getExponentSize(), pTargetType.getMantissaSize(), pNumber); + mathsatEnv, + pTargetType.getExponentSize(), + pTargetType.getMantissaSizeWithoutHiddenBit(), + pNumber); } @Override 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..c199cc4cc2 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.getFloatingPointTypeFromSizesWithoutHiddenBit( 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.getMantissaSizeWithoutHiddenBit()); } @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 hidden bit + int mantWidthWithoutHiddenBit = 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 + mantWidthWithoutHiddenBit)); + BigInteger exponent = extractBitsFrom(bits, mantWidthWithoutHiddenBit, expWidth); + BigInteger mantissa = extractBitsFrom(bits, 0, mantWidthWithoutHiddenBit); - return FloatingPointNumber.of(sign, exponent, mantissa, expWidth, mantWidth); + return FloatingPointNumber.of(sign, exponent, mantissa, expWidth, mantWidthWithoutHiddenBit); } /** 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..b0789bd39b 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 hidden 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 hidden 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 hidden 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 hidden 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 hidden 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 hidden 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 hidden 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 hidden 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 hidden 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 hidden 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 hidden bit! + */ public static native long msat_make_fp_bits_number( long e, String bitRep, long exp_w, long mant_w); 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..8f350bd9e2 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.getFloatingPointTypeFromSizesWithoutHiddenBit(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.getMantissaSizeWithoutHiddenBit()); 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.getMantissaSizeWithHiddenBit() <= highPrec.getMantissaSizeWithHiddenBit()) { 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..52a5b8241e 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.getFloatingPointType( - Native.fpaGetEbits(z3context, pSort), Native.fpaGetSbits(z3context, pSort) - 1); + return FormulaType.getFloatingPointTypeFromSizesWithHiddenBit( + Native.fpaGetEbits(z3context, pSort), Native.fpaGetSbits(z3context, pSort)); case Z3_ROUNDING_MODE_SORT: return FormulaType.FloatingPointRoundingModeType; case Z3_RE_SORT: @@ -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.getMantissaSizeWithHiddenBit()); 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.getMantissaSizeWithoutHiddenBit()); } 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.getMantissaSizeWithoutHiddenBit()), pType.getExponentSize(), - pType.getMantissaSize()); + pType.getMantissaSizeWithoutHiddenBit()); } 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.getMantissaSizeWithoutHiddenBit()), pType.getExponentSize(), - pType.getMantissaSize()); + pType.getMantissaSizeWithoutHiddenBit()); } 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.getMantissaSizeWithoutHiddenBit()); } } diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 74390241cf..3854a7a776 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -12,6 +12,9 @@ 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; import com.google.common.collect.ImmutableList; @@ -33,6 +36,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; @@ -75,16 +79,16 @@ public void init() { @Test public void floatingPointType() { - FloatingPointType type = FormulaType.getFloatingPointType(23, 42); + FloatingPointType type = getFloatingPointTypeFromSizesWithoutHiddenBit(23, 42); 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") - .that(result.getMantissaSize()) - .isEqualTo(type.getMantissaSize()); + assertWithMessage("mantissa sizes not equal") + .that(result.getMantissaSizeWithHiddenBit()) + .isEqualTo(type.getMantissaSizeWithHiddenBit()); } @Test @@ -258,7 +262,7 @@ public void fpRemainderNormal() throws SolverException, InterruptedException { for (FloatingPointType prec : new FloatingPointType[] { - singlePrecType, doublePrecType, FormulaType.getFloatingPointType(5, 6), + singlePrecType, doublePrecType, getFloatingPointTypeFromSizesWithoutHiddenBit(5, 6), }) { final FloatingPointFormula numFive = fpmgr.makeNumber(5, prec); @@ -282,7 +286,7 @@ public void fpRemainderSpecial() throws SolverException, InterruptedException { for (FloatingPointType prec : new FloatingPointType[] { - singlePrecType, doublePrecType, FormulaType.getFloatingPointType(5, 6), + singlePrecType, doublePrecType, getFloatingPointTypeFromSizesWithoutHiddenBit(5, 6), }) { final FloatingPointFormula num = fpmgr.makeNumber(42, prec); @@ -536,7 +540,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 = getFloatingPointTypeFromSizesWithoutHiddenBit(12, 52); FloatingPointFormula h1 = fpmgr.makeNumber(BigDecimal.TEN.pow(309).multiply(BigDecimal.valueOf(1.0001)), nearDouble); FloatingPointFormula h2 = @@ -544,7 +548,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 = getFloatingPointTypeFromSizesWithoutHiddenBit(4, 4); FloatingPointFormula i1 = fpmgr.makeNumber(BigDecimal.TEN.pow(50).multiply(BigDecimal.valueOf(1.001)), smallType); FloatingPointFormula i2 = @@ -573,7 +577,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 = getFloatingPointTypeFromSizesWithoutHiddenBit(4, 4); FloatingPointFormula j1 = fpmgr.makeNumber(BigDecimal.TEN.pow(500).multiply(BigDecimal.valueOf(1.001)), smallType2); FloatingPointFormula j2 = @@ -602,9 +606,9 @@ 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 = FormulaType.getFloatingPointType(100, 100); + FloatingPointType largeType = getFloatingPointTypeFromSizesWithoutHiddenBit(100, 100); FloatingPointFormula k1 = fpmgr.makeNumber(BigDecimal.TEN.pow(200).multiply(BigDecimal.valueOf(1.001)), largeType); FloatingPointFormula k2 = @@ -641,7 +645,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 = getFloatingPointTypeFromSizesWithoutHiddenBit(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 +680,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 = getFloatingPointTypeFromSizesWithoutHiddenBit(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,14 +1219,244 @@ 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); + FloatingPointNumber fpValue = model.evaluate(constFpNum); + assertThat(fpValue.getMantissaSizeWithHiddenBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithHiddenBit()); + assertThat(fpValue.getMantissaSizeWithoutHiddenBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithHiddenBit() - 1); + assertThat(fpValue.floatValue()).isEqualTo(f); + assertThat(fpValue.doubleValue()).isEqualTo((double) f); } } } } + // The standard defines the mantissa such that it includes the hidden bit, and mantissa + + // exponent equal the total size. This test checks this, + that it holds with to/from IEEE + // bitvector + @Test + public void bitvectorToFloatingPointMantissaSignBitInterpretationSinglePrecision() { + int bvSize32 = singlePrecType.getTotalSize(); + BitvectorFormula bvNumber32 = bvmgr.makeBitvector(bvSize32, BigInteger.ZERO); + // Sanity checks + assertThat(bvSize32).isEqualTo(32); + assertThat(singlePrecType.getExponentSize()).isEqualTo(8); + assertThat(singlePrecType.getMantissaSizeWithoutHiddenBit()).isEqualTo(23); + assertThat(singlePrecType.getMantissaSizeWithHiddenBit()).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)) + .getMantissaSizeWithHiddenBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithHiddenBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpSinglePrec)) + .getMantissaSizeWithoutHiddenBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithoutHiddenBit()); + 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 = + getFloatingPointTypeFromSizesWithHiddenBit( + singlePrecType.getExponentSize(), singlePrecType.getMantissaSizeWithHiddenBit()); + FloatingPointType fpTypeWithoutSignBit = + getFloatingPointTypeFromSizesWithoutHiddenBit( + singlePrecType.getExponentSize(), singlePrecType.getMantissaSizeWithoutHiddenBit()); + 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)) + .getMantissaSizeWithHiddenBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithHiddenBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)) + .getMantissaSizeWithoutHiddenBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithoutHiddenBit()); + 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)) + .getMantissaSizeWithHiddenBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithHiddenBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)) + .getMantissaSizeWithoutHiddenBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithoutHiddenBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)).getExponentSize()) + .isEqualTo(singlePrecType.getExponentSize()); + } + + @Test + public void floatingPointMantissaSignBitWithBitvectorInterpretationSinglePrecision() + throws SolverException, InterruptedException { + requireFPToBitvector(); + + int bvSize32 = singlePrecType.getTotalSize(); + BitvectorFormula bvNumber32 = bvmgr.makeBitvector(bvSize32, BigInteger.ZERO); + FloatingPointFormula bvToFpSinglePrec = fpmgr.fromIeeeBitvector(bvNumber32, singlePrecType); + FloatingPointType fpTypeWithSignBit = + getFloatingPointTypeFromSizesWithHiddenBit( + singlePrecType.getExponentSize(), singlePrecType.getMantissaSizeWithHiddenBit()); + FloatingPointType fpTypeWithoutSignBit = + getFloatingPointTypeFromSizesWithoutHiddenBit( + singlePrecType.getExponentSize(), singlePrecType.getMantissaSizeWithoutHiddenBit()); + FloatingPointFormula bvToFpfpTypeWithSignBit = + fpmgr.fromIeeeBitvector(bvNumber32, fpTypeWithSignBit); + FloatingPointFormula bvToFpfpTypeWithoutSignBit = + fpmgr.fromIeeeBitvector(bvNumber32, fpTypeWithoutSignBit); + + // 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 bvToFpTypeWithoutSignBitToBv = + fpmgr.toIeeeBitvector(bvToFpfpTypeWithoutSignBit); + assertThat(bvmgr.getLength(bvToFpTypeWithoutSignBitToBv)).isEqualTo(bvSize32); + + 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 + + // exponent equal the total size. This test checks this, + that it holds with from + // bitvector to IEEE FP + @Test + public void bitvectorToFloatingPointMantissaSignBitInterpretationDoublePrecision() { + int bvSize64 = doublePrecType.getTotalSize(); + BitvectorFormula bvNumberSize64 = bvmgr.makeBitvector(bvSize64, BigInteger.ZERO); + // Sanity checks + assertThat(bvSize64).isEqualTo(64); + assertThat(doublePrecType.getExponentSize()).isEqualTo(11); + assertThat(doublePrecType.getMantissaSizeWithoutHiddenBit()).isEqualTo(52); + assertThat(doublePrecType.getMantissaSizeWithHiddenBit()).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)) + .getMantissaSizeWithHiddenBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithHiddenBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpDoublePrec)) + .getMantissaSizeWithoutHiddenBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithoutHiddenBit()); + 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 = + getFloatingPointTypeFromSizesWithHiddenBit( + doublePrecType.getExponentSize(), doublePrecType.getMantissaSizeWithHiddenBit()); + FloatingPointType fpTypeWithoutSignBit = + getFloatingPointTypeFromSizesWithoutHiddenBit( + doublePrecType.getExponentSize(), doublePrecType.getMantissaSizeWithoutHiddenBit()); + 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)) + .getMantissaSizeWithHiddenBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithHiddenBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithSignBit)) + .getMantissaSizeWithoutHiddenBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithoutHiddenBit()); + 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)) + .getMantissaSizeWithHiddenBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithHiddenBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)) + .getMantissaSizeWithoutHiddenBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithoutHiddenBit()); + assertThat( + ((FloatingPointType) mgr.getFormulaType(bvToFpfpTypeWithoutSignBit)).getExponentSize()) + .isEqualTo(doublePrecType.getExponentSize()); + } + + // Checks the correct precision/exponent/mantissa in FP to BV conversion + @Test + public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecision() + throws SolverException, InterruptedException { + requireFPToBitvector(); + + int bvSize64 = doublePrecType.getTotalSize(); + BitvectorFormula bvNumberSize64 = bvmgr.makeBitvector(bvSize64, BigInteger.ZERO); + FloatingPointFormula bvToFpDoublePrec = fpmgr.fromIeeeBitvector(bvNumberSize64, doublePrecType); + FloatingPointType fpTypeWithSignBit = + getFloatingPointTypeFromSizesWithHiddenBit( + doublePrecType.getExponentSize(), doublePrecType.getMantissaSizeWithHiddenBit()); + FloatingPointType fpTypeWithoutSignBit = + getFloatingPointTypeFromSizesWithoutHiddenBit( + doublePrecType.getExponentSize(), doublePrecType.getMantissaSizeWithoutHiddenBit()); + FloatingPointFormula bvToFpfpTypeWithSignBit = + fpmgr.fromIeeeBitvector(bvNumberSize64, fpTypeWithSignBit); + FloatingPointFormula bvToFpfpTypeWithoutSignBit = + fpmgr.fromIeeeBitvector(bvNumberSize64, fpTypeWithoutSignBit); + + // 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 bvToFpTypeWithoutSignBitToBv = + fpmgr.toIeeeBitvector(bvToFpfpTypeWithoutSignBit); + assertThat(bvmgr.getLength(bvToFpTypeWithoutSignBitToBv)).isEqualTo(bvSize64); + + assertThatFormula(bvmgr.equal(bvToFpTypeWithSignBitToBv, bvNumberSize64)).isTautological(); + assertThatFormula(bvmgr.equal(bvToFpDoublePrecToBv, bvNumberSize64)).isTautological(); + assertThatFormula(bvmgr.equal(bvToFpTypeWithoutSignBitToBv, bvNumberSize64)).isTautological(); + } + @Test @SuppressWarnings({"unchecked", "resource"}) public void fpInterpolation() throws SolverException, InterruptedException { @@ -1272,10 +1506,16 @@ public void fpFrom32BitPattern() throws SolverException, InterruptedException { BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), singlePrecType.getExponentSize(), - singlePrecType.getMantissaSize()); + singlePrecType.getMantissaSizeWithoutHiddenBit()); + assertThat(fpNumber.getMantissaSizeWithHiddenBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithHiddenBit()); + assertThat(fpNumber.getMantissaSizeWithoutHiddenBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithHiddenBit() - 1); final FloatingPointFormula fp1 = fpmgr.makeNumber(fpNumber); final FloatingPointFormula fp2 = fpmgr.makeNumber(pFloat, singlePrecType); - return bmgr.and(fpmgr.assignment(fpFromBv, fp1), fpmgr.assignment(fpFromBv, fp2)); + final BooleanFormula assignment1 = fpmgr.assignment(fpFromBv, fp1); + final BooleanFormula assignment2 = fpmgr.assignment(fpFromBv, fp2); + return bmgr.and(assignment1, assignment2); }); } @@ -1298,10 +1538,16 @@ public void fpFrom64BitPattern() throws SolverException, InterruptedException { BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), doublePrecType.getExponentSize(), - doublePrecType.getMantissaSize()); + doublePrecType.getMantissaSizeWithoutHiddenBit()); + assertThat(fpNumber.getMantissaSizeWithHiddenBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithHiddenBit()); + assertThat(fpNumber.getMantissaSizeWithoutHiddenBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithHiddenBit() - 1); final FloatingPointFormula fp1 = fpmgr.makeNumber(fpNumber); final FloatingPointFormula fp2 = fpmgr.makeNumber(pDouble, doublePrecType); - return bmgr.and(fpmgr.assignment(fpFromBv, fp1), fpmgr.assignment(fpFromBv, fp2)); + 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/FloatingPointNumberTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java index 831f68ad17..fdc057e907 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java @@ -10,19 +10,27 @@ 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.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.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 { + 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 : @@ -50,7 +58,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_HIDDEN_BIT); assertThat(fpNum.floatValue()).isEqualTo(f); assertThat(fpNum.doubleValue()).isEqualTo((double) f); // float is a strict subtype of double. } @@ -83,7 +93,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_HIDDEN_BIT); assertThat(fpNum.doubleValue()).isEqualTo(d); } } @@ -95,4 +107,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)"); + } } diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 56b0200874..f9a4670bb3 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -477,13 +477,17 @@ public void floatConstantVisit() { Integer.toBinaryString(Float.floatToRawIntBits(entry.getKey().floatValue())), 32, '0')); - checkFloatConstant(FormulaType.getFloatingPointType(5, 10), entry.getKey(), entry.getValue()); + checkFloatConstant( + FormulaType.getFloatingPointTypeFromSizesWithoutHiddenBit(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.getMantissaSizeWithoutHiddenBit()); ConstantsVisitor visitor = new ConstantsVisitor(); mgr.visit(fpmgr.makeNumber(value, prec), visitor); @@ -580,7 +584,7 @@ public void fpToBvTest() { .that(solverToUse()) .isNoneOf(Solvers.CVC4, Solvers.CVC5); - var fpType = FormulaType.getFloatingPointType(5, 10); + var fpType = FormulaType.getFloatingPointTypeFromSizesWithoutHiddenBit(5, 10); var visitor = new DefaultFormulaVisitor() { @Override