diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java
index 62bb3afbe4..91a9d7d6bc 100644
--- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java
@@ -8,13 +8,15 @@
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.getFloatingPointTypeWithoutSignBit;
import java.math.BigDecimal;
import java.math.BigInteger;
+import java.util.Map;
import org.sosy_lab.common.rationals.Rational;
import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign;
import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
+import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula;
/**
* Floating point operations.
@@ -99,7 +101,8 @@ default FloatingPointFormula makeNumber(FloatingPointNumber number) {
number.getExponent(),
number.getMantissa(),
number.getMathSign(),
- getFloatingPointType(number.getExponentSize(), number.getMantissaSize()));
+ getFloatingPointTypeWithoutSignBit(
+ number.getExponentSize(), number.getMantissaSizeWithoutSignBit()));
}
/**
@@ -285,11 +288,70 @@ 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).
+ * bitvector conforming to the IEEE 754-2008 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).
*/
BitvectorFormula toIeeeBitvector(FloatingPointFormula number);
+ /**
+ * Create a formula that produces a representation of the given floating-point value as a
+ * bitvector conforming to the IEEE 754-2008 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).
+ * This implementation can be used independently of {@link
+ * #toIeeeBitvector(FloatingPointFormula)}, as it does not rely on an SMT solvers support for
+ * {@link #toIeeeBitvector(FloatingPointFormula)}. Behavior for special FP values (NaN, Inf, etc.)
+ * is not defined, and returned values are solver dependent. In case you want to define how to
+ * handle those values, please use {@link #toIeeeBitvector(FloatingPointFormula, String, Map)}.
+ * This method is based on a suggestion in the SMTLib2 standard ( source) implementation:
+ *
+ * (declare-fun b () (_ BitVec m))
+ *
+ *
(assert (= ((_ to_fp eb sb) b) f))
+ *
+ * @param number the {@link FloatingPointFormula} to be converted into an IEEE bitvector.
+ * @param bitvectorConstantName the name of the returned {@link BitvectorFormula}.
+ * @return {@link BitvectorFormulaAndBooleanFormula} consisting of the transformed input
+ * floating-point as a {@link BitvectorFormula} and the additional constraint as {@link
+ * BooleanFormula}.
+ */
+ BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+ FloatingPointFormula number, String bitvectorConstantName);
+
+ /**
+ * Create a formula that produces a representation of the given floating-point value as a
+ * bitvector conforming to the IEEE 754-2008 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).
+ * This implementation can be used independently of {@link
+ * #toIeeeBitvector(FloatingPointFormula)}, as it does not rely on an SMT solvers support for
+ * {@link #toIeeeBitvector(FloatingPointFormula)}. Behavior for special FP values (NaN, Inf, etc.)
+ * can be defined using the specialFPConstantHandling parameter. This method is based on a
+ * suggestion in the SMTLib2 standard ( source) implementation:
+ *
+ *
(declare-fun b () (_ BitVec m))
+ *
+ *
(assert (= ((_ to_fp eb sb) b) f))
+ *
+ * @param number the {@link FloatingPointFormula} to be converted into an IEEE bitvector.
+ * @param bitvectorConstantName the name of the returned {@link BitvectorFormula}.
+ * @param specialFPConstantHandling a {@link Map} defining the returned {@link BitvectorFormula}
+ * for special {@link FloatingPointFormula} constant numbers. You are only allowed to specify
+ * a mapping for special FP numbers with more than one well-defined bitvector representation,
+ * i.e. NaN and +/- Infinity. The width of the mapped bitvector values has to match the
+ * expected width of the bitvector return value. The {@link FloatingPointType}, i.e.
+ * precision, of the key FP numbers has to match the {@link FloatingPointType} of the
+ * parameter {@code number}. For an empty {@link Map}, or missing mappings, this method
+ * behaves like {@link #toIeeeBitvector(FloatingPointFormula, String)}.
+ * @return {@link BitvectorFormulaAndBooleanFormula} consisting of the transformed input
+ * floating-point as a {@link BitvectorFormula} and the additional constraint as {@link
+ * BooleanFormula}.
+ */
+ BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+ FloatingPointFormula number,
+ String bitvectorConstantName,
+ Map specialFPConstantHandling);
+
FloatingPointFormula round(FloatingPointFormula formula, FloatingPointRoundingMode roundingMode);
// ----------------- Arithmetic relations, return type NumeralFormula -----------------
@@ -467,4 +529,13 @@ FloatingPointFormula multiply(
*
*/
BooleanFormula isNegative(FloatingPointFormula number);
+
+ /**
+ * Returns the size of the mantissa (also called a coefficient or significant), including the sign
+ * bit, for the given {@link FloatingPointFormula}.
+ */
+ int getMantissaSizeWithSignBit(FloatingPointFormula number);
+
+ /** Returns the size of the exponent for the given {@link FloatingPointFormula}. */
+ int getExponentSize(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..6c750e3701 100644
--- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java
+++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java
@@ -23,6 +23,7 @@
@AutoValue
public abstract class FloatingPointNumber {
+ // Mantissas do not include the sign bit
public static final int SINGLE_PRECISION_EXPONENT_SIZE = 8;
public static final int SINGLE_PRECISION_MANTISSA_SIZE = 23;
public static final int DOUBLE_PRECISION_EXPONENT_SIZE = 11;
@@ -80,8 +81,29 @@ public final boolean getSign() {
public abstract int getExponentSize();
+ /**
+ * Returns the size of the mantissa (also called a coefficient or significant), excluding the sign
+ * bit.
+ */
+ // TODO: mark as soon to be deprecated
public abstract int getMantissaSize();
+ /**
+ * Returns the size of the mantissa (also called a coefficient or significant), excluding the sign
+ * bit.
+ */
+ public int getMantissaSizeWithoutSignBit() {
+ return getMantissaSize();
+ }
+
+ /**
+ * Returns the size of the mantissa (also called a coefficient or significant), including the sign
+ * bit.
+ */
+ public int getMantissaSizeWithSignBit() {
+ return getMantissaSize() + 1;
+ }
+
/**
* Get a floating-point number with the given sign, exponent, and mantissa.
*
@@ -92,7 +114,7 @@ public final boolean getSign() {
* @param mantissa the mantissa of the floating-point number, given as unsigned (not negative)
* number without hidden bit
* @param exponentSize the (maximum) size of the exponent in bits
- * @param mantissaSize the (maximum) size of the mantissa in bits
+ * @param mantissaSize the (maximum) size of the mantissa in bits (excluding the sign bit)
* @see #of(Sign, BigInteger, BigInteger, int, int)
*/
@Deprecated(
@@ -119,7 +141,7 @@ public static FloatingPointNumber of(
* @param mantissa the mantissa of the floating-point number, given as unsigned (not negative)
* number without hidden bit
* @param exponentSize the (maximum) size of the exponent in bits
- * @param mantissaSize the (maximum) size of the mantissa in bits
+ * @param mantissaSize the (maximum) size of the mantissa in bits (excluding the sign bit)
*/
public static FloatingPointNumber of(
Sign sign, BigInteger exponent, BigInteger mantissa, int exponentSize, int mantissaSize) {
@@ -136,7 +158,7 @@ public static FloatingPointNumber of(
* @param bits the bit-representation of the floating-point number, consisting of sign bit,
* exponent (without bias) and mantissa (without hidden bit) in this exact ordering
* @param exponentSize the size of the exponent in bits
- * @param mantissaSize the size of the mantissa in bits
+ * @param mantissaSize the size of the mantissa in bits (excluding the sign bit)
*/
public static FloatingPointNumber of(String bits, int exponentSize, int mantissaSize) {
Preconditions.checkArgument(0 < exponentSize);
@@ -159,24 +181,26 @@ public static FloatingPointNumber of(String bits, int exponentSize, int mantissa
/**
* Returns true if this floating-point number is an IEEE-754-2008 single precision type with 32
- * bits length consisting of an 8 bit exponent, a 23 bit mantissa and a single sign bit.
+ * bits length consisting of an 8 bit exponent, a 24 bit mantissa (including the sign bit).
*
* @return true for IEEE-754 single precision type, false otherwise.
*/
public boolean isIEEE754SinglePrecision() {
+ // Mantissa does not include the sign bit
return getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE
- && getMantissaSize() == SINGLE_PRECISION_MANTISSA_SIZE;
+ && getMantissaSizeWithoutSignBit() == SINGLE_PRECISION_MANTISSA_SIZE;
}
/**
* Returns true if this floating-point number is an IEEE-754-2008 double precision type with 64
- * bits length consisting of an 11 bit exponent, a 52 bit mantissa and a single sign bit.
+ * bits length consisting of an 11 bit exponent, a 53 bit mantissa (including the sign bit).
*
* @return true for IEEE-754 double precision type, false otherwise.
*/
public boolean isIEEE754DoublePrecision() {
+ // Mantissa does not include the sign bit
return getExponentSize() == DOUBLE_PRECISION_EXPONENT_SIZE
- && getMantissaSize() == DOUBLE_PRECISION_MANTISSA_SIZE;
+ && getMantissaSizeWithoutSignBit() == DOUBLE_PRECISION_MANTISSA_SIZE;
}
/** compute a representation as Java-based float value, if possible. */
@@ -204,18 +228,18 @@ public double doubleValue() {
}
private BitSet getBits() {
- var mantissaSize = getMantissaSize();
+ var mantissaSizeWithoutSign = getMantissaSizeWithoutSignBit();
var exponentSize = getExponentSize();
var mantissa = getMantissa();
var exponent = getExponent();
- var bits = new BitSet(1 + exponentSize + mantissaSize);
+ var bits = new BitSet(exponentSize + mantissaSizeWithoutSign + 1);
if (getMathSign().isNegative()) {
- bits.set(exponentSize + mantissaSize); // if negative, set first bit to 1
+ bits.set(exponentSize + mantissaSizeWithoutSign); // if negative, set first bit to 1
}
for (int i = 0; i < exponentSize; i++) {
- bits.set(mantissaSize + i, exponent.testBit(i));
+ bits.set(mantissaSizeWithoutSign + i, exponent.testBit(i));
}
- for (int i = 0; i < mantissaSize; i++) {
+ for (int i = 0; i < mantissaSizeWithoutSign; i++) {
bits.set(i, mantissa.testBit(i));
}
return bits;
@@ -227,7 +251,7 @@ private BitSet getBits() {
*/
@Override
public final String toString() {
- var length = 1 + getExponentSize() + getMantissaSize();
+ var length = getExponentSize() + getMantissaSizeWithSignBit();
var str = new StringBuilder(length);
var bits = getBits();
for (int i = 0; i < length; i++) {
diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java
index d5beea79cc..da62759ba3 100644
--- a/src/org/sosy_lab/java_smt/api/FormulaType.java
+++ b/src/org/sosy_lab/java_smt/api/FormulaType.java
@@ -205,14 +205,61 @@ public String toSMTLIBString() {
}
}
- public static FloatingPointType getFloatingPointType(int exponentSize, int mantissaSize) {
- return new FloatingPointType(exponentSize, mantissaSize);
+ /**
+ * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes.
+ * The mantissa size is expected to not include the sign bit.
+ *
+ * @param exponentSize size of the exponent for the base of the floating-point
+ * @param mantissaSizeWithoutSignBit size of the mantissa (also called a coefficient or
+ * significant), excluding the sign bit.
+ * @return the newly constructed {@link FloatingPointType}.
+ */
+ // TODO: mark as soon to be deprecated
+ public static FloatingPointType getFloatingPointType(
+ int exponentSize, int mantissaSizeWithoutSignBit) {
+ return new FloatingPointType(exponentSize, mantissaSizeWithoutSignBit);
+ }
+
+ /**
+ * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes.
+ * The mantissa size is expected to not include the sign bit.
+ *
+ * @param exponentSize size of the exponent for the base of the floating-point
+ * @param mantissaSizeWithoutSignBit size of the mantissa (also called a coefficient or
+ * significant), excluding the sign bit.
+ * @return the newly constructed {@link FloatingPointType}.
+ */
+ public static FloatingPointType getFloatingPointTypeWithoutSignBit(
+ int exponentSize, int mantissaSizeWithoutSignBit) {
+ return new FloatingPointType(exponentSize, mantissaSizeWithoutSignBit);
+ }
+
+ /**
+ * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes.
+ * The mantissa size is expected to not include the sign bit.
+ *
+ * @param exponentSize size of the exponent for the base of the floating-point
+ * @param mantissaSizeWithSignBit size of the mantissa (also called a coefficient or significant),
+ * including the sign bit.
+ * @return the newly constructed {@link FloatingPointType}.
+ */
+ public static FloatingPointType getFloatingPointTypeWithSignBit(
+ int exponentSize, int mantissaSizeWithSignBit) {
+ return new FloatingPointType(exponentSize, mantissaSizeWithSignBit);
}
+ /**
+ * @return single precision {@link FloatingPointType} with exponent sized 8, and mantissa sized 24
+ * (including the sign bit).
+ */
public static FloatingPointType getSinglePrecisionFloatingPointType() {
return FloatingPointType.SINGLE_PRECISION_FP_TYPE;
}
+ /**
+ * @return double precision {@link FloatingPointType} with exponent sized 11, and mantissa sized
+ * 53 (including the sign bit).
+ */
public static FloatingPointType getDoublePrecisionFloatingPointType() {
return FloatingPointType.DOUBLE_PRECISION_FP_TYPE;
}
@@ -226,6 +273,8 @@ public static final class FloatingPointType extends FormulaType";
+ return "FloatingPoint";
}
@Override
public String toSMTLIBString() {
- return "(_ FloatingPoint " + exponentSize + " " + mantissaSize + ")";
+ return "(_ FloatingPoint " + exponentSize + " " + getMantissaSizeWithSignBit() + ")";
}
}
@@ -478,7 +552,7 @@ public static FormulaType fromString(String t) {
} else if (t.startsWith("FloatingPoint<")) {
// FloatingPoint
List exman = Splitter.on(',').limit(2).splitToList(t.substring(14, t.length() - 1));
- return FormulaType.getFloatingPointType(
+ return FormulaType.getFloatingPointTypeWithoutSignBit(
Integer.parseInt(exman.get(0).substring(4)), Integer.parseInt(exman.get(1).substring(5)));
} else if (t.startsWith("Bitvector<")) {
// Bitvector<32>
diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java
index 47c847afe2..2653558406 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java
@@ -8,13 +8,19 @@
package org.sosy_lab.java_smt.basicimpl;
+import static com.google.common.base.Preconditions.checkArgument;
+import static com.google.common.base.Preconditions.checkNotNull;
+import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointType;
import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName;
-import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableMap;
+import com.google.common.collect.ImmutableSet;
import java.math.BigDecimal;
import java.math.BigInteger;
import java.util.HashMap;
import java.util.Map;
+import java.util.Map.Entry;
+import java.util.Set;
import org.sosy_lab.common.rationals.Rational;
import org.sosy_lab.java_smt.api.BitvectorFormula;
import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -45,10 +51,18 @@ public abstract class AbstractFloatingPointFormulaManager roundingModes;
+ private final AbstractBitvectorFormulaManager bvMgr;
+
+ private final AbstractBooleanFormulaManager bMgr;
+
protected AbstractFloatingPointFormulaManager(
- FormulaCreator pCreator) {
+ FormulaCreator pCreator,
+ AbstractBitvectorFormulaManager pBvMgr,
+ AbstractBooleanFormulaManager pBMgr) {
super(pCreator);
roundingModes = new HashMap<>();
+ bvMgr = pBvMgr;
+ bMgr = pBMgr;
}
protected abstract TFormulaInfo getDefaultRoundingMode();
@@ -145,7 +159,7 @@ protected abstract TFormulaInfo makeNumberImpl(
BigInteger exponent, BigInteger mantissa, Sign sign, FloatingPointType type);
protected static boolean isNegativeZero(Double pN) {
- Preconditions.checkNotNull(pN);
+ checkNotNull(pN);
return Double.valueOf("-0.0").equals(pN);
}
@@ -256,7 +270,95 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula pNumber) {
return getFormulaCreator().encapsulateBitvector(toIeeeBitvectorImpl(extractInfo(pNumber)));
}
- protected abstract TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber);
+ @SuppressWarnings("unused")
+ protected TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber) {
+ throw new UnsupportedOperationException(
+ "The chosen solver does not support transforming "
+ + "FloatingPointFormula to IEEE bitvectors. Try using the fallback "
+ + "methods toIeeeBitvector"
+ + "(FloatingPointFormula, String) and/or "
+ + "toIeeeBitvector(FloatingPointFormula, String, Map)");
+ }
+
+ @Override
+ public BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+ FloatingPointFormula f, String bitvectorConstantName) {
+ return toIeeeBitvector(f, bitvectorConstantName, ImmutableMap.of());
+ }
+
+ @Override
+ public BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+ FloatingPointFormula f,
+ String bitvectorConstantName,
+ Map specialFPConstantHandling) {
+
+ FormulaType.FloatingPointType fpType =
+ (FloatingPointType) getFormulaCreator().getFormulaType(f);
+ int mantissaSizeWithSignBit = fpType.getMantissaSizeWithSignBit();
+ int exponentSize = fpType.getExponentSize();
+ BitvectorFormula bvFormula =
+ bvMgr.makeVariable(mantissaSizeWithSignBit + exponentSize, bitvectorConstantName);
+
+ // When building new Fp types, we don't include the sign bit
+ FloatingPointFormula fromIeeeBitvector =
+ fromIeeeBitvector(
+ bvFormula, getFloatingPointType(exponentSize, mantissaSizeWithSignBit - 1));
+
+ // assignment() allows a value to be NaN etc.
+ // Note: All fp.to_* functions are unspecified for NaN and infinity input values in the
+ // standard, what solvers return might be distinct.
+ BooleanFormula additionalConstraint = assignment(fromIeeeBitvector, f);
+
+ // Build special numbers so that we can compare them in the map
+ FloatingPointType precision = getFloatingPointType(exponentSize, mantissaSizeWithSignBit - 1);
+ Set specialNumbers =
+ ImmutableSet.of(
+ makeNaN(precision), makePlusInfinity(precision), makeMinusInfinity(precision));
+
+ BitvectorFormula toIeeeBv = bvFormula;
+ for (Entry entry :
+ specialFPConstantHandling.entrySet()) {
+ FloatingPointFormula fpConst = entry.getKey();
+
+ // We check that FP const special numbers are used (info from SMTLib2-standard)
+ // NaN has multiple possible definitions.
+ // +/- Infinity each has 2; e.g., +infinity for sort (_ FloatingPoint 2 3) is represented
+ // equivalently by (_ +oo 2 3) and (fp #b0 #b11 #b00).
+ // -0 only has one representation; i.e. (_ -zero 3 2) abbreviates (fp #b1 #b000 #b0), and
+ // is therefore disallowed.
+ // This automatically checks the correct precision as well!
+ checkArgument(
+ specialNumbers.contains(fpConst),
+ "You are only allowed to specify a mapping for special FP numbers with more than one"
+ + " well-defined bitvector representation, i.e. NaN and +/- Infinity. Their precision"
+ + " has to match the precision of the formula to be represented as bitvector.");
+
+ BitvectorFormula bvTerm = entry.getValue();
+ checkArgument(
+ bvMgr.getLength(bvTerm) == bvMgr.getLength(bvFormula),
+ "The size of the bitvector terms used as mapped values needs to be equal to the size of"
+ + " the bitvector returned by this method");
+
+ BooleanFormula assumption = assignment(fpConst, f);
+ toIeeeBv = bMgr.ifThenElse(assumption, bvTerm, toIeeeBv);
+ }
+
+ return BitvectorFormulaAndBooleanFormula.of(toIeeeBv, additionalConstraint);
+ }
+
+ @Override
+ public int getMantissaSizeWithSignBit(FloatingPointFormula f) {
+ return getMantissaSizeWithSignBitImpl(extractInfo(f));
+ }
+
+ protected abstract int getMantissaSizeWithSignBitImpl(TFormulaInfo f);
+
+ @Override
+ public int getExponentSize(FloatingPointFormula f) {
+ return getExponentSizeImpl(extractInfo(f));
+ }
+
+ protected abstract int getExponentSizeImpl(TFormulaInfo f);
@Override
public FloatingPointFormula negate(FloatingPointFormula pNumber) {
@@ -519,4 +621,28 @@ protected static String getBvRepresentation(BigInteger integer, int size) {
}
return String.copyValueOf(values);
}
+
+ public static final class BitvectorFormulaAndBooleanFormula {
+ private final BitvectorFormula bitvectorFormula;
+ private final BooleanFormula booleanFormula;
+
+ private BitvectorFormulaAndBooleanFormula(
+ BitvectorFormula pBitvectorFormula, BooleanFormula pBooleanFormula) {
+ bitvectorFormula = checkNotNull(pBitvectorFormula);
+ booleanFormula = checkNotNull(pBooleanFormula);
+ }
+
+ private static BitvectorFormulaAndBooleanFormula of(
+ BitvectorFormula pBitvectorFormula, BooleanFormula pBooleanFormula) {
+ return new BitvectorFormulaAndBooleanFormula(pBitvectorFormula, pBooleanFormula);
+ }
+
+ public BitvectorFormula getBitvectorFormula() {
+ return bitvectorFormula;
+ }
+
+ public BooleanFormula getBooleanFormula() {
+ return booleanFormula;
+ }
+ }
}
diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java
index 74b1677375..cc0ca778a1 100644
--- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java
@@ -10,6 +10,7 @@
import java.math.BigDecimal;
import java.math.BigInteger;
+import java.util.Map;
import org.sosy_lab.common.rationals.Rational;
import org.sosy_lab.java_smt.api.BitvectorFormula;
import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -20,6 +21,7 @@
import org.sosy_lab.java_smt.api.Formula;
import org.sosy_lab.java_smt.api.FormulaType;
import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
+import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula;
public class DebuggingFloatingPointFormulaManager implements FloatingPointFormulaManager {
private final FloatingPointFormulaManager delegate;
@@ -206,6 +208,36 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula number) {
return result;
}
+ @Override
+ public BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+ FloatingPointFormula number, String bitvectorConstantName) {
+ debugging.assertThreadLocal();
+ debugging.assertFormulaInContext(number);
+ BitvectorFormulaAndBooleanFormula res = delegate.toIeeeBitvector(number, bitvectorConstantName);
+ debugging.addFormulaTerm(res.getBitvectorFormula());
+ debugging.addFormulaTerm(res.getBooleanFormula());
+ return res;
+ }
+
+ @Override
+ public BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+ FloatingPointFormula number,
+ String bitvectorConstantName,
+ Map specialFPConstantHandling) {
+ debugging.assertThreadLocal();
+ debugging.assertFormulaInContext(number);
+ specialFPConstantHandling.forEach(
+ (key, value) -> {
+ debugging.assertFormulaInContext(key);
+ debugging.assertFormulaInContext(value);
+ });
+ BitvectorFormulaAndBooleanFormula res =
+ delegate.toIeeeBitvector(number, bitvectorConstantName, specialFPConstantHandling);
+ debugging.addFormulaTerm(res.getBitvectorFormula());
+ debugging.addFormulaTerm(res.getBooleanFormula());
+ return res;
+ }
+
@Override
public FloatingPointFormula round(
FloatingPointFormula formula, FloatingPointRoundingMode roundingMode) {
@@ -491,4 +523,18 @@ public BooleanFormula isNegative(FloatingPointFormula number) {
debugging.addFormulaTerm(result);
return result;
}
+
+ @Override
+ public int getMantissaSizeWithSignBit(FloatingPointFormula number) {
+ debugging.assertThreadLocal();
+ debugging.assertFormulaInContext(number);
+ return delegate.getMantissaSizeWithSignBit(number);
+ }
+
+ @Override
+ public int getExponentSize(FloatingPointFormula number) {
+ debugging.assertThreadLocal();
+ debugging.assertFormulaInContext(number);
+ return delegate.getExponentSize(number);
+ }
}
diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java
index 415b7cb00f..e0756d53f8 100644
--- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java
@@ -12,6 +12,7 @@
import java.math.BigDecimal;
import java.math.BigInteger;
+import java.util.Map;
import org.sosy_lab.common.rationals.Rational;
import org.sosy_lab.java_smt.api.BitvectorFormula;
import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -22,6 +23,7 @@
import org.sosy_lab.java_smt.api.Formula;
import org.sosy_lab.java_smt.api.FormulaType;
import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
+import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula;
class StatisticsFloatingPointFormulaManager implements FloatingPointFormulaManager {
@@ -166,6 +168,21 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula pNumber) {
return delegate.toIeeeBitvector(pNumber);
}
+ @Override
+ public BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+ FloatingPointFormula number, String bitvectorConstantName) {
+ stats.fpOperations.getAndIncrement();
+ return delegate.toIeeeBitvector(number, bitvectorConstantName);
+ }
+
+ @Override
+ public BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+ FloatingPointFormula number,
+ String bitvectorConstantName,
+ Map specialFPConstantHandling) {
+ return delegate.toIeeeBitvector(number, bitvectorConstantName, specialFPConstantHandling);
+ }
+
@Override
public FloatingPointFormula round(
FloatingPointFormula pFormula, FloatingPointRoundingMode pRoundingMode) {
@@ -352,4 +369,16 @@ public BooleanFormula isNegative(FloatingPointFormula pNumber) {
stats.fpOperations.getAndIncrement();
return delegate.isNegative(pNumber);
}
+
+ @Override
+ public int getMantissaSizeWithSignBit(FloatingPointFormula pNumber) {
+ stats.fpOperations.getAndIncrement();
+ return delegate.getMantissaSizeWithSignBit(pNumber);
+ }
+
+ @Override
+ public int getExponentSize(FloatingPointFormula pNumber) {
+ stats.fpOperations.getAndIncrement();
+ return delegate.getExponentSize(pNumber);
+ }
}
diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java
index 3d922f71a8..4b7b7b3a63 100644
--- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java
@@ -12,6 +12,7 @@
import java.math.BigDecimal;
import java.math.BigInteger;
+import java.util.Map;
import org.sosy_lab.common.rationals.Rational;
import org.sosy_lab.java_smt.api.BitvectorFormula;
import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -23,6 +24,7 @@
import org.sosy_lab.java_smt.api.FormulaType;
import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
import org.sosy_lab.java_smt.api.SolverContext;
+import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula;
class SynchronizedFloatingPointFormulaManager implements FloatingPointFormulaManager {
@@ -186,6 +188,24 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula pNumber) {
}
}
+ @Override
+ public BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+ FloatingPointFormula number, String bitvectorConstantName) {
+ synchronized (sync) {
+ return delegate.toIeeeBitvector(number, bitvectorConstantName);
+ }
+ }
+
+ @Override
+ public BitvectorFormulaAndBooleanFormula toIeeeBitvector(
+ FloatingPointFormula number,
+ String bitvectorConstantName,
+ Map specialFPConstantHandling) {
+ synchronized (sync) {
+ return delegate.toIeeeBitvector(number, bitvectorConstantName, specialFPConstantHandling);
+ }
+ }
+
@Override
public FloatingPointFormula round(
FloatingPointFormula pFormula, FloatingPointRoundingMode pRoundingMode) {
@@ -400,4 +420,18 @@ public BooleanFormula isNegative(FloatingPointFormula pNumber) {
return delegate.isNegative(pNumber);
}
}
+
+ @Override
+ public int getMantissaSizeWithSignBit(FloatingPointFormula pNumber) {
+ synchronized (sync) {
+ return delegate.getMantissaSizeWithSignBit(pNumber);
+ }
+ }
+
+ @Override
+ public int getExponentSize(FloatingPointFormula pNumber) {
+ synchronized (sync) {
+ return delegate.getExponentSize(pNumber);
+ }
+ }
}
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 cb03e5aa6d..f5ee0f07f7 100644
--- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java
@@ -25,17 +25,16 @@
public class BitwuzlaFloatingPointManager
extends AbstractFloatingPointFormulaManager {
- private final BitwuzlaFormulaCreator bitwuzlaCreator;
+
private final TermManager termManager;
private final Term roundingMode;
- // Keeps track of the temporary variables that are created for fp-to-bv casts
- private static int counter = 0;
-
protected BitwuzlaFloatingPointManager(
- BitwuzlaFormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode) {
- super(pCreator);
- bitwuzlaCreator = pCreator;
+ BitwuzlaFormulaCreator pCreator,
+ FloatingPointRoundingMode pFloatingPointRoundingMode,
+ BitwuzlaBitvectorFormulaManager pBvMgr,
+ BitwuzlaBooleanFormulaManager pBmgr) {
+ super(pCreator, pBvMgr, pBmgr);
termManager = pCreator.getTermManager();
roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode);
}
@@ -84,7 +83,7 @@ protected Term makeNumberImpl(
Sort expSort = termManager.mk_bv_sort(type.getExponentSize());
Term expTerm = termManager.mk_bv_value(expSort, exponent.toString(2));
- Sort mantissaSort = termManager.mk_bv_sort(type.getMantissaSize());
+ Sort mantissaSort = termManager.mk_bv_sort(type.getMantissaSizeWithoutSignBit());
Term mantissaTerm = termManager.mk_bv_value(mantissaSort, mantissa.toString(2));
return termManager.mk_fp_value(signTerm, expTerm, mantissaTerm);
@@ -134,7 +133,7 @@ protected Term castToImpl(
pRoundingMode,
pNumber,
targetType.getExponentSize(),
- targetType.getMantissaSize() + 1);
+ targetType.getMantissaSizeWithSignBit());
} else if (pTargetType.isBitvectorType()) {
FormulaType.BitvectorType targetType = (FormulaType.BitvectorType) pTargetType;
if (pSigned) {
@@ -148,6 +147,16 @@ protected Term castToImpl(
}
}
+ @Override
+ protected int getMantissaSizeWithSignBitImpl(Term fp) {
+ return fp.sort().fp_sig_size();
+ }
+
+ @Override
+ protected int getExponentSizeImpl(Term fp) {
+ return fp.sort().fp_exp_size();
+ }
+
@Override
protected Term castFromImpl(
Term pNumber, boolean pSigned, FloatingPointType pTargetType, Term pRoundingMode) {
@@ -161,14 +170,14 @@ protected Term castFromImpl(
roundingMode,
pNumber,
pTargetType.getExponentSize(),
- pTargetType.getMantissaSize() + 1);
+ pTargetType.getMantissaSizeWithSignBit());
} else {
return termManager.mk_term(
Kind.FP_TO_FP_FROM_UBV,
roundingMode,
pNumber,
pTargetType.getExponentSize(),
- pTargetType.getMantissaSize() + 1);
+ pTargetType.getMantissaSizeWithSignBit());
}
} else {
@@ -183,49 +192,7 @@ protected Term fromIeeeBitvectorImpl(Term pNumber, FloatingPointType pTargetType
Kind.FP_TO_FP_FROM_BV,
pNumber,
pTargetType.getExponentSize(),
- pTargetType.getMantissaSize() + 1);
- }
-
- @Override
- protected Term toIeeeBitvectorImpl(Term pNumber) {
- int sizeExp = pNumber.sort().fp_exp_size();
- int sizeSig = pNumber.sort().fp_sig_size();
-
- Sort bvSort = termManager.mk_bv_sort(sizeExp + sizeSig);
-
- // The following code creates a new variable that is returned as result.
- // Additionally, we track constraints about the equality of the new variable and the FP number,
- // which is added onto the prover stack whenever the new variable is used as assertion.
-
- // TODO This internal implementation is a technical dept and should be removed.
- // The additional constraints are not transparent in all cases, e.g., when visiting a
- // formula, creating a model, or transferring the assertions onto another prover stack.
- // A better way would be a direct implementation of this in Bitwuzla, without interfering
- // with JavaSMT.
-
- // Note that NaN is handled as a special case in this method. This is not strictly necessary,
- // but if we just use "fpTerm = to_fp(bvVar)" the NaN will be given a random payload (and
- // sign). Since NaN payloads are not preserved here anyway we might as well pick a canonical
- // representation, e.g., which is "0 11111111 10000000000000000000000" for single precision.
- String nanRepr = "0" + "1".repeat(sizeExp + 1) + "0".repeat(sizeSig - 2);
- Term bvNaN = termManager.mk_bv_value(bvSort, nanRepr);
-
- // TODO creating our own utility variables might eb unexpected from the user.
- // We might need to exclude such variables in models and formula traversal.
- String newVariable = "__JAVASMT__CAST_FROM_BV_" + counter++;
- Term bvVar = termManager.mk_const(bvSort, newVariable);
- Term equal =
- termManager.mk_term(
- Kind.ITE,
- termManager.mk_term(Kind.FP_IS_NAN, pNumber),
- termManager.mk_term(Kind.EQUAL, bvVar, bvNaN),
- termManager.mk_term(
- Kind.EQUAL,
- termManager.mk_term(Kind.FP_TO_FP_FROM_BV, bvVar, sizeExp, sizeSig),
- pNumber));
-
- bitwuzlaCreator.addConstraintForVariable(newVariable, equal);
- return bvVar;
+ pTargetType.getMantissaSizeWithSignBit());
}
@Override
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java
index f946331319..fd5c82d284 100644
--- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java
@@ -102,7 +102,7 @@ assert getFormulaType(pTerm).isBitvectorType()
// system instead use bitwuzla_mk_fp_value_from_real somehow or convert myself
@Override
public Sort getFloatingPointType(FloatingPointType type) {
- return termManager.mk_fp_sort(type.getExponentSize(), type.getMantissaSize() + 1);
+ return termManager.mk_fp_sort(type.getExponentSize(), type.getMantissaSizeWithSignBit());
}
@Override
@@ -171,7 +171,7 @@ public FormulaType bitwuzlaSortToType(Sort pSort) {
if (pSort.is_fp()) {
int exponent = pSort.fp_exp_size();
int mantissa = pSort.fp_sig_size() - 1;
- return FormulaType.getFloatingPointType(exponent, mantissa);
+ return FormulaType.getFloatingPointTypeWithoutSignBit(exponent, mantissa);
} else if (pSort.is_bv()) {
return FormulaType.getBitvectorTypeWithSize(pSort.bv_size());
} else if (pSort.is_array()) {
@@ -380,7 +380,7 @@ public FormulaType getFormulaType(T pFormula) {
}
int exp = sort.fp_exp_size();
int man = sort.fp_sig_size() - 1;
- return (FormulaType) FormulaType.getFloatingPointType(exp, man);
+ return (FormulaType) FormulaType.getFloatingPointTypeWithoutSignBit(exp, man);
} else if (sort.is_rm()) {
return (FormulaType) FormulaType.FloatingPointRoundingModeType;
}
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java
index 6ccc1c31ae..77110ba71e 100644
--- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java
@@ -172,7 +172,8 @@ public static BitwuzlaSolverContext create(
BitwuzlaQuantifiedFormulaManager quantifierTheory =
new BitwuzlaQuantifiedFormulaManager(creator);
BitwuzlaFloatingPointManager floatingPointTheory =
- new BitwuzlaFloatingPointManager(creator, pFloatingPointRoundingMode);
+ new BitwuzlaFloatingPointManager(
+ creator, pFloatingPointRoundingMode, bitvectorTheory, booleanTheory);
BitwuzlaArrayFormulaManager arrayTheory = new BitwuzlaArrayFormulaManager(creator);
BitwuzlaFormulaManager manager =
new BitwuzlaFormulaManager(
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..b62f959500 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java
@@ -8,15 +8,17 @@
package org.sosy_lab.java_smt.solvers.cvc4;
+import static com.google.common.base.Preconditions.checkArgument;
+
import com.google.common.collect.ImmutableList;
import edu.stanford.CVC4.BitVector;
-import edu.stanford.CVC4.BitVectorExtract;
import edu.stanford.CVC4.Expr;
import edu.stanford.CVC4.ExprManager;
import edu.stanford.CVC4.FloatingPoint;
import edu.stanford.CVC4.FloatingPointConvertSort;
import edu.stanford.CVC4.FloatingPointSize;
import edu.stanford.CVC4.FloatingPointToFPFloatingPoint;
+import edu.stanford.CVC4.FloatingPointToFPIEEEBitVector;
import edu.stanford.CVC4.FloatingPointToFPSignedBitVector;
import edu.stanford.CVC4.FloatingPointToFPUnsignedBitVector;
import edu.stanford.CVC4.FloatingPointToSBV;
@@ -41,8 +43,11 @@ public class CVC4FloatingPointFormulaManager
private final Expr roundingMode;
protected CVC4FloatingPointFormulaManager(
- CVC4FormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode) {
- super(pCreator);
+ CVC4FormulaCreator pCreator,
+ FloatingPointRoundingMode pFloatingPointRoundingMode,
+ CVC4BitvectorFormulaManager pBvFormulaManager,
+ CVC4BooleanFormulaManager pBoolFormulaManager) {
+ super(pCreator, pBvFormulaManager, pBoolFormulaManager);
exprManager = pCreator.getEnv();
roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode);
}
@@ -52,8 +57,8 @@ protected CVC4FloatingPointFormulaManager(
private static FloatingPointSize getFPSize(FloatingPointType pType) {
long pExponentSize = pType.getExponentSize();
- long pMantissaSize = pType.getMantissaSize();
- return new FloatingPointSize(pExponentSize, pMantissaSize + 1); // plus sign bit
+ long pMantissaSize = pType.getMantissaSizeWithSignBit();
+ return new FloatingPointSize(pExponentSize, pMantissaSize);
}
@Override
@@ -89,11 +94,11 @@ protected Expr makeNumberImpl(
BigInteger exponent, BigInteger mantissa, Sign sign, FloatingPointType type) {
final String signStr = sign.isNegative() ? "1" : "0";
final String exponentStr = getBvRepresentation(exponent, type.getExponentSize());
- final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSize());
+ final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSizeWithoutSignBit());
final String bitvecStr = signStr + exponentStr + mantissaStr;
final BitVector bitVector = new BitVector(bitvecStr, 2);
final FloatingPoint fp =
- new FloatingPoint(type.getExponentSize(), type.getMantissaSize() + 1, bitVector);
+ new FloatingPoint(type.getExponentSize(), type.getMantissaSizeWithSignBit(), bitVector);
return exprManager.mkConst(fp);
}
@@ -109,7 +114,7 @@ protected Expr makeNumberAndRound(String pN, FloatingPointType pType, Expr pRoun
final Rational rat = toRational(pN);
final BigInteger upperBound =
- getBiggestNumberBeforeInf(pType.getMantissaSize(), pType.getExponentSize());
+ getBiggestNumberBeforeInf(pType.getMantissaSizeWithSignBit(), pType.getExponentSize());
if (rat.greater(Rational.fromDecimal(upperBound.negate().toString()))
&& rat.less(Rational.fromDecimal(upperBound.toString()))) {
@@ -218,8 +223,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.getMantissaSizeWithSignBit();
+ FloatingPointSize fpSize = new FloatingPointSize(pExponentSize, pMantissaSize);
FloatingPointConvertSort fpConvert = new FloatingPointConvertSort(fpSize);
final Expr op;
if (pSigned) {
@@ -358,31 +363,30 @@ protected Expr isNegative(Expr pParam) {
@Override
protected Expr fromIeeeBitvectorImpl(Expr bitvector, FloatingPointType pTargetType) {
- int mantissaSize = pTargetType.getMantissaSize();
- int exponentSize = pTargetType.getExponentSize();
- int size = pTargetType.getTotalSize();
- assert size == mantissaSize + exponentSize + 1;
-
- Expr signExtract = exprManager.mkConst(new BitVectorExtract(size - 1, size - 1));
- Expr exponentExtract = exprManager.mkConst(new BitVectorExtract(size - 2, mantissaSize));
- Expr mantissaExtract = exprManager.mkConst(new BitVectorExtract(mantissaSize - 1, 0));
-
- Expr sign = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, signExtract, bitvector);
- Expr exponent = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, exponentExtract, bitvector);
- Expr mantissa = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, mantissaExtract, bitvector);
+ // This is just named weird, but the CVC4 doc say this is IEEE BV -> FP
+ FloatingPointConvertSort fpConvertSort = new FloatingPointConvertSort(getFPSize(pTargetType));
+ Expr op = exprManager.mkConst(new FloatingPointToFPIEEEBitVector(fpConvertSort));
+ return exprManager.mkExpr(op, bitvector);
+ }
- return exprManager.mkExpr(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa);
+ @Override
+ protected Expr round(Expr pFormula, FloatingPointRoundingMode pRoundingMode) {
+ return exprManager.mkExpr(Kind.FLOATINGPOINT_RTI, getRoundingModeImpl(pRoundingMode), pFormula);
}
@Override
- protected Expr toIeeeBitvectorImpl(Expr pNumber) {
- // TODO possible work-around: use a tmp-variable "TMP" and add an
- // additional constraint "pNumer == fromIeeeBitvectorImpl(TMP)" for it in all use-cases.
- throw new UnsupportedOperationException("FP to IEEE-BV is not supported");
+ protected int getMantissaSizeWithSignBitImpl(Expr f) {
+ Type type = f.getType();
+ checkArgument(type.isFloatingPoint());
+ edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(type);
+ return (int) fpType.getSignificandSize();
}
@Override
- protected Expr round(Expr pFormula, FloatingPointRoundingMode pRoundingMode) {
- return exprManager.mkExpr(Kind.FLOATINGPOINT_RTI, getRoundingModeImpl(pRoundingMode), pFormula);
+ protected int getExponentSizeImpl(Expr f) {
+ Type type = f.getType();
+ checkArgument(type.isFloatingPoint());
+ edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(type);
+ return (int) fpType.getExponentSize();
}
}
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java
index 23e7328956..1dac46d603 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java
@@ -114,7 +114,7 @@ public Type getBitvectorType(int pBitwidth) {
@Override
public Type getFloatingPointType(FloatingPointType pType) {
return exprManager.mkFloatingPointType(
- pType.getExponentSize(), pType.getMantissaSize() + 1); // plus sign bit
+ pType.getExponentSize(), pType.getMantissaSizeWithSignBit());
}
@Override
@@ -154,7 +154,7 @@ public FormulaType getFormulaType(T pFormula) {
t.isFloatingPoint(), "FloatingPointFormula with actual type %s: %s", t, pFormula);
edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(t);
return (FormulaType)
- FormulaType.getFloatingPointType(
+ FormulaType.getFloatingPointTypeWithoutSignBit(
(int) fpType.getExponentSize(),
(int) fpType.getSignificandSize() - 1); // without sign bit
@@ -182,7 +182,7 @@ private FormulaType getFormulaTypeFromTermType(Type t) {
return FormulaType.getBitvectorTypeWithSize((int) new BitVectorType(t).getSize());
} else if (t.isFloatingPoint()) {
edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(t);
- return FormulaType.getFloatingPointType(
+ return FormulaType.getFloatingPointTypeWithoutSignBit(
(int) fpType.getExponentSize(),
(int) fpType.getSignificandSize() - 1); // without sign bit
} else if (t.isRoundingMode()) {
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java
index b5bd086812..6dff64284d 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java
@@ -80,7 +80,9 @@ public static SolverContext create(
CVC4FloatingPointFormulaManager fpTheory;
if (Configuration.isBuiltWithSymFPU()) {
- fpTheory = new CVC4FloatingPointFormulaManager(creator, pFloatingPointRoundingMode);
+ fpTheory =
+ new CVC4FloatingPointFormulaManager(
+ creator, pFloatingPointRoundingMode, bitvectorTheory, booleanTheory);
} else {
fpTheory = null;
pLogger.log(Level.INFO, "CVC4 was built without support for FloatingPoint theory");
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..ca4c2f339a 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java
@@ -35,8 +35,11 @@ public class CVC5FloatingPointFormulaManager
private final Term roundingMode;
protected CVC5FloatingPointFormulaManager(
- CVC5FormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode) {
- super(pCreator);
+ CVC5FormulaCreator pCreator,
+ FloatingPointRoundingMode pFloatingPointRoundingMode,
+ CVC5BitvectorFormulaManager pBvFormulaManager,
+ CVC5BooleanFormulaManager pBoolFormulaManager) {
+ super(pCreator, pBvFormulaManager, pBoolFormulaManager);
termManager = pCreator.getEnv();
solver = pCreator.getSolver();
roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode);
@@ -78,7 +81,7 @@ protected Term makeNumberImpl(
return termManager.mkFloatingPoint(
termManager.mkBitVector(1, sign == Sign.NEGATIVE ? 1 : 0),
termManager.mkBitVector(type.getExponentSize(), exponent.toString(16), 16),
- termManager.mkBitVector(type.getMantissaSize(), mantissa.toString(16), 16));
+ termManager.mkBitVector(type.getMantissaSizeWithoutSignBit(), mantissa.toString(16), 16));
} catch (CVC5ApiException e) {
throw new IllegalArgumentException("You tried creating a invalid bitvector", e);
@@ -90,7 +93,7 @@ protected Term makeNumberAndRound(String pN, FloatingPointType pType, Term pRoun
try {
if (isNegativeZero(Double.valueOf(pN))) {
return termManager.mkFloatingPointNegZero(
- pType.getExponentSize(), pType.getMantissaSize() + 1);
+ pType.getExponentSize(), pType.getMantissaSizeWithSignBit());
}
} catch (CVC5ApiException | NumberFormatException e) {
// ignore and fallback to floating point from rational numbers
@@ -102,7 +105,7 @@ protected Term makeNumberAndRound(String pN, FloatingPointType pType, Term pRoun
termManager.mkOp(
Kind.FLOATINGPOINT_TO_FP_FROM_REAL,
pType.getExponentSize(),
- pType.getMantissaSize() + 1);
+ pType.getMantissaSizeWithSignBit());
Term term =
termManager.mkTerm(realToFp, pRoundingMode, termManager.mkReal(rationalValue.toString()));
// simplification removes the cast from real to fp and return a bit-precise fp-number.
@@ -111,8 +114,8 @@ protected Term makeNumberAndRound(String pN, FloatingPointType pType, Term pRoun
throw new IllegalArgumentException(
"You tried creating a invalid floating point with exponent size "
+ pType.getExponentSize()
- + ", mantissa size "
- + pType.getMantissaSize()
+ + ", mantissa size (including sign bit)"
+ + pType.getMantissaSizeWithSignBit()
+ " and value "
+ pN
+ ".",
@@ -152,13 +155,13 @@ protected Term makeVariableImpl(String varName, FloatingPointType pType) {
protected Term makePlusInfinityImpl(FloatingPointType pType) {
try {
return termManager.mkFloatingPointPosInf(
- pType.getExponentSize(), pType.getMantissaSize() + 1);
+ pType.getExponentSize(), pType.getMantissaSizeWithSignBit());
} catch (CVC5ApiException e) {
throw new IllegalArgumentException(
"You tried creating a invalid positive floating point +infinity with exponent size "
+ pType.getExponentSize()
+ " and mantissa size "
- + pType.getMantissaSize()
+ + pType.getMantissaSizeWithSignBit()
+ ".",
e);
}
@@ -168,13 +171,13 @@ protected Term makePlusInfinityImpl(FloatingPointType pType) {
protected Term makeMinusInfinityImpl(FloatingPointType pType) {
try {
return termManager.mkFloatingPointNegInf(
- pType.getExponentSize(), pType.getMantissaSize() + 1);
+ pType.getExponentSize(), pType.getMantissaSizeWithSignBit());
} catch (CVC5ApiException e) {
throw new IllegalArgumentException(
"You tried creating a invalid negative floating point -infinity with exponent size "
+ pType.getExponentSize()
+ " and mantissa size "
- + pType.getMantissaSize()
+ + pType.getMantissaSizeWithSignBit()
+ ".",
e);
}
@@ -183,13 +186,14 @@ protected Term makeMinusInfinityImpl(FloatingPointType pType) {
@Override
protected Term makeNaNImpl(FloatingPointType pType) {
try {
- return termManager.mkFloatingPointNaN(pType.getExponentSize(), pType.getMantissaSize() + 1);
+ return termManager.mkFloatingPointNaN(
+ pType.getExponentSize(), pType.getMantissaSizeWithSignBit());
} catch (CVC5ApiException e) {
throw new IllegalArgumentException(
"You tried creating a invalid NaN with exponent size "
+ pType.getExponentSize()
+ " and mantissa size "
- + pType.getMantissaSize()
+ + pType.getMantissaSizeWithSignBit()
+ ".",
e);
}
@@ -205,7 +209,7 @@ protected Term castToImpl(
termManager.mkOp(
Kind.FLOATINGPOINT_TO_FP_FROM_FP,
((FloatingPointType) pTargetType).getExponentSize(),
- ((FloatingPointType) pTargetType).getMantissaSize() + 1);
+ ((FloatingPointType) pTargetType).getMantissaSizeWithSignBit());
return termManager.mkTerm(fpToFp, pRoundingMode, pNumber);
} else if (pTargetType.isBitvectorType()) {
@@ -246,7 +250,7 @@ protected Term castFromImpl(
termManager.mkOp(
Kind.FLOATINGPOINT_TO_FP_FROM_REAL,
pTargetType.getExponentSize(),
- pTargetType.getMantissaSize() + 1);
+ pTargetType.getMantissaSizeWithSignBit());
return termManager.mkTerm(realToFp, pRoundingMode, pNumber);
@@ -256,14 +260,14 @@ protected Term castFromImpl(
termManager.mkOp(
Kind.FLOATINGPOINT_TO_FP_FROM_SBV,
pTargetType.getExponentSize(),
- pTargetType.getMantissaSize() + 1);
+ pTargetType.getMantissaSizeWithSignBit());
return termManager.mkTerm(realToSBv, pRoundingMode, pNumber);
} else {
Op realToUBv =
termManager.mkOp(
Kind.FLOATINGPOINT_TO_FP_FROM_UBV,
pTargetType.getExponentSize(),
- pTargetType.getMantissaSize() + 1);
+ pTargetType.getMantissaSizeWithSignBit());
return termManager.mkTerm(realToUBv, pRoundingMode, pNumber);
}
@@ -278,7 +282,7 @@ protected Term castFromImpl(
+ " into a FloatingPoint with exponent size "
+ pTargetType.getExponentSize()
+ " and mantissa size "
- + pTargetType.getMantissaSize()
+ + pTargetType.getMantissaSizeWithSignBit()
+ ".",
e);
}
@@ -408,41 +412,33 @@ protected Term isNegative(Term pParam) {
}
@Override
- protected Term fromIeeeBitvectorImpl(Term bitvector, FloatingPointType pTargetType) {
- int mantissaSize = pTargetType.getMantissaSize();
- int exponentSize = pTargetType.getExponentSize();
- int size = pTargetType.getTotalSize();
- assert size == mantissaSize + exponentSize + 1;
-
- Op signExtract;
- Op exponentExtract;
- Op mantissaExtract;
+ protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetType) {
try {
- signExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 1, size - 1);
- exponentExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 2, mantissaSize);
- mantissaExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, mantissaSize - 1, 0);
- } catch (CVC5ApiException e) {
- throw new IllegalArgumentException(
- "You tried creating a invalid bitvector extract in term " + bitvector + ".", e);
+ return termManager.mkTerm(
+ termManager.mkOp(
+ Kind.FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
+ pTargetType.getExponentSize(),
+ pTargetType.getMantissaSizeWithSignBit()),
+ pBitvector);
+ } catch (CVC5ApiException pE) {
+ throw new RuntimeException(pE);
}
+ }
- Term sign = termManager.mkTerm(signExtract, bitvector);
- Term exponent = termManager.mkTerm(exponentExtract, bitvector);
- Term mantissa = termManager.mkTerm(mantissaExtract, bitvector);
-
- return termManager.mkTerm(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa);
+ @Override
+ protected Term round(Term pFormula, FloatingPointRoundingMode pRoundingMode) {
+ return termManager.mkTerm(Kind.FLOATINGPOINT_RTI, getRoundingModeImpl(pRoundingMode), pFormula);
}
@Override
- protected Term toIeeeBitvectorImpl(Term pNumber) {
- // TODO possible work-around: use a tmp-variable "TMP" and add an
- // additional constraint "pNumer == fromIeeeBitvectorImpl(TMP)" for it in all use-cases.
- // --> This has to be done on user-side, not in JavaSMT.
- throw new UnsupportedOperationException("FP to IEEE-BV is not supported");
+ protected int getMantissaSizeWithSignBitImpl(Term f) {
+ Sort sort = f.getSort();
+ return sort.getFloatingPointSignificandSize();
}
@Override
- protected Term round(Term pFormula, FloatingPointRoundingMode pRoundingMode) {
- return termManager.mkTerm(Kind.FLOATINGPOINT_RTI, getRoundingModeImpl(pRoundingMode), pFormula);
+ protected int getExponentSizeImpl(Term f) {
+ Sort sort = f.getSort();
+ return sort.getFloatingPointExponentSize();
}
}
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java
index 946b6be069..381daa2a29 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java
@@ -142,14 +142,15 @@ public Sort getBitvectorType(int pBitwidth) {
public Sort getFloatingPointType(FloatingPointType pType) {
try {
// plus sign bit
- return termManager.mkFloatingPointSort(pType.getExponentSize(), pType.getMantissaSize() + 1);
+ return termManager.mkFloatingPointSort(
+ pType.getExponentSize(), pType.getMantissaSizeWithSignBit());
} catch (CVC5ApiException e) {
throw new IllegalArgumentException(
"Cannot create floatingpoint sort with exponent size "
+ pType.getExponentSize()
+ " and mantissa "
- + pType.getMantissaSize()
- + " (plus sign bit).",
+ + pType.getMantissaSizeWithSignBit()
+ + " (including sign bit).",
e);
}
}
@@ -223,7 +224,7 @@ private FormulaType getFormulaTypeFromTermType(Sort sort) {
return FormulaType.getBitvectorTypeWithSize(sort.getBitVectorSize());
} else if (sort.isFloatingPoint()) {
// CVC5 wants the sign bit as part of the mantissa. We add that manually in creation.
- return FormulaType.getFloatingPointType(
+ return FormulaType.getFloatingPointTypeWithoutSignBit(
sort.getFloatingPointExponentSize(), sort.getFloatingPointSignificandSize() - 1);
} else if (sort.isRoundingMode()) {
return FormulaType.FloatingPointRoundingModeType;
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java
index 97e0d269b2..696334c8ee 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java
@@ -150,7 +150,8 @@ public static SolverContext create(
CVC5BitvectorFormulaManager bitvectorTheory =
new CVC5BitvectorFormulaManager(pCreator, booleanTheory);
CVC5FloatingPointFormulaManager fpTheory =
- new CVC5FloatingPointFormulaManager(pCreator, pFloatingPointRoundingMode);
+ new CVC5FloatingPointFormulaManager(
+ pCreator, pFloatingPointRoundingMode, bitvectorTheory, booleanTheory);
CVC5QuantifiedFormulaManager qfTheory = new CVC5QuantifiedFormulaManager(pCreator);
CVC5ArrayFormulaManager arrayTheory = new CVC5ArrayFormulaManager(pCreator);
CVC5SLFormulaManager slTheory = new CVC5SLFormulaManager(pCreator);
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java
index bd277cf91a..129b2669a8 100644
--- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java
+++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java
@@ -35,6 +35,7 @@
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_repr;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_to_smtlib2_ext;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_to_smtlib2_term;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_type_equals;
import org.junit.After;
import org.junit.Ignore;
@@ -79,6 +80,44 @@ public void fpMantWidth() {
assertThat(msat_get_fp_type_mant_width(env, type)).isEqualTo(23);
}
+ /*
+ * MathSAT5, compared to all other solvers and the standard, does not expect the sign bit to be
+ * included in the mantissa!
+ */
+ @Test
+ public void fpMantissaDoesNotIncludeSignBit() {
+ int totalBVSize = 32;
+ long bvNumber = msat_make_bv_number(env, "42", totalBVSize, 10);
+ long bvType = msat_term_get_type(bvNumber);
+ assertThat(msat_get_bv_type_size(env, bvType)).isEqualTo(totalBVSize);
+ assertThat(msat_get_bv_type_size(env, msat_term_get_type(bvNumber))).isEqualTo(totalBVSize);
+
+ int exponent = 8;
+ int mantissaWithoutSign = 23; // excluding sign bit
+ long fpSinglePrecType = msat_get_fp_type(env, exponent, mantissaWithoutSign);
+ assertThat(msat_get_fp_type_mant_width(env, fpSinglePrecType)).isEqualTo(mantissaWithoutSign);
+ assertThat(msat_get_fp_type_exp_width(env, fpSinglePrecType)).isEqualTo(exponent);
+ // total size is exp + man + 1
+ assertThat(
+ msat_get_fp_type_mant_width(env, fpSinglePrecType)
+ + msat_get_fp_type_exp_width(env, fpSinglePrecType)
+ + 1)
+ .isEqualTo(totalBVSize);
+
+ long bvToFpSinglePrec =
+ Mathsat5NativeApi.msat_make_fp_from_ieeebv(env, exponent, mantissaWithoutSign, bvNumber);
+ assertThat(msat_type_equals(msat_term_get_type(bvToFpSinglePrec), fpSinglePrecType)).isTrue();
+ assertThat(msat_get_fp_type_mant_width(env, msat_term_get_type(bvToFpSinglePrec)))
+ .isEqualTo(mantissaWithoutSign);
+ assertThat(msat_get_fp_type_exp_width(env, msat_term_get_type(bvToFpSinglePrec)))
+ .isEqualTo(exponent);
+
+ long bvToFpSinglePrecToBv = Mathsat5NativeApi.msat_make_fp_as_ieeebv(env, bvToFpSinglePrec);
+ assertThat(msat_type_equals(msat_term_get_type(bvToFpSinglePrecToBv), bvType)).isTrue();
+ assertThat(msat_get_bv_type_size(env, msat_term_get_type(bvToFpSinglePrecToBv)))
+ .isEqualTo(totalBVSize);
+ }
+
@Test
public void fpExpWidthIllegal() {
long type = msat_get_integer_type(env);
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..2eb6eb2750 100644
--- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java
@@ -8,6 +8,8 @@
package org.sosy_lab.java_smt.solvers.mathsat5;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_fp_type_exp_width;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_fp_type_mant_width;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_equal;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_abs;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_bits_number;
@@ -61,8 +63,11 @@ class Mathsat5FloatingPointFormulaManager
private final long roundingMode;
Mathsat5FloatingPointFormulaManager(
- Mathsat5FormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode) {
- super(pCreator);
+ Mathsat5FormulaCreator pCreator,
+ FloatingPointRoundingMode pFloatingPointRoundingMode,
+ Mathsat5BitvectorFormulaManager pBvFormulaManager,
+ Mathsat5BooleanFormulaManager pBoolFormulaManager) {
+ super(pCreator, pBvFormulaManager, pBoolFormulaManager);
mathsatEnv = pCreator.getEnv();
roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode);
@@ -102,27 +107,41 @@ protected Long makeNumberImpl(
BigInteger exponent, BigInteger mantissa, Sign sign, FloatingPointType type) {
final String signStr = sign.isNegative() ? "1" : "0";
final String exponentStr = getBvRepresentation(exponent, type.getExponentSize());
- final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSize());
+ // MathSAT5 expects the mantissa to not include the sign bit
+ final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSizeWithSignBit() - 1);
final String bitvecForm = signStr + exponentStr + mantissaStr;
final BigInteger bitvecValue = new BigInteger(bitvecForm, 2);
return msat_make_fp_bits_number(
- mathsatEnv, bitvecValue.toString(), type.getExponentSize(), type.getMantissaSize());
+ mathsatEnv,
+ bitvecValue.toString(),
+ type.getExponentSize(),
+ type.getMantissaSizeWithSignBit() - 1);
}
@Override
protected Long makeNumberAndRound(String pN, FloatingPointType pType, Long pRoundingMode) {
try {
if (isNegativeZero(Double.valueOf(pN))) {
+ // MathSAT5 expects the mantissa to not include the sign bit
return msat_make_fp_neg(
mathsatEnv,
msat_make_fp_rat_number(
- mathsatEnv, "0", pType.getExponentSize(), pType.getMantissaSize(), pRoundingMode));
+ mathsatEnv,
+ "0",
+ pType.getExponentSize(),
+ pType.getMantissaSizeWithSignBit() - 1,
+ pRoundingMode));
}
} catch (NumberFormatException e) {
// ignore and fallback to floating point from rational numbers
}
+ // MathSAT5 expects the mantissa to not include the sign bit
return msat_make_fp_rat_number(
- mathsatEnv, pN, pType.getExponentSize(), pType.getMantissaSize(), pRoundingMode);
+ mathsatEnv,
+ pN,
+ pType.getExponentSize(),
+ pType.getMantissaSizeWithoutSignBit(),
+ pRoundingMode);
}
@Override
@@ -132,17 +151,23 @@ protected Long makeVariableImpl(String var, FloatingPointType type) {
@Override
protected Long makePlusInfinityImpl(FloatingPointType type) {
- return msat_make_fp_plus_inf(mathsatEnv, type.getExponentSize(), type.getMantissaSize());
+ // MathSAT5 expects the mantissa to not include the sign bit
+ return msat_make_fp_plus_inf(
+ mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithSignBit() - 1);
}
@Override
protected Long makeMinusInfinityImpl(FloatingPointType type) {
- return msat_make_fp_minus_inf(mathsatEnv, type.getExponentSize(), type.getMantissaSize());
+ // MathSAT5 expects the mantissa to not include the sign bit
+ return msat_make_fp_minus_inf(
+ mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithSignBit() - 1);
}
@Override
protected Long makeNaNImpl(FloatingPointType type) {
- return msat_make_fp_nan(mathsatEnv, type.getExponentSize(), type.getMantissaSize());
+ // MathSAT5 expects the mantissa to not include the sign bit
+ return msat_make_fp_nan(
+ mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithSignBit() - 1);
}
@Override
@@ -150,10 +175,11 @@ protected Long castToImpl(
Long pNumber, boolean pSigned, FormulaType pTargetType, Long pRoundingMode) {
if (pTargetType.isFloatingPointType()) {
FormulaType.FloatingPointType targetType = (FormulaType.FloatingPointType) pTargetType;
+ // MathSAT5 expects the mantissa to not include the sign bit
return msat_make_fp_cast(
mathsatEnv,
targetType.getExponentSize(),
- targetType.getMantissaSize(),
+ targetType.getMantissaSizeWithSignBit() - 1,
pRoundingMode,
pNumber);
@@ -179,18 +205,19 @@ protected Long castFromImpl(
return castToImpl(pNumber, pSigned, pTargetType, pRoundingMode);
} else if (formulaType.isBitvectorType()) {
+ // MathSAT5 expects the mantissa to not include the sign bit
if (pSigned) {
return msat_make_fp_from_sbv(
mathsatEnv,
pTargetType.getExponentSize(),
- pTargetType.getMantissaSize(),
+ pTargetType.getMantissaSizeWithSignBit() - 1,
pRoundingMode,
pNumber);
} else {
return msat_make_fp_from_ubv(
mathsatEnv,
pTargetType.getExponentSize(),
- pTargetType.getMantissaSize(),
+ pTargetType.getMantissaSizeWithSignBit() - 1,
pRoundingMode,
pNumber);
}
@@ -214,8 +241,12 @@ private Long genericCast(Long pNumber, FormulaType pTargetType) {
@Override
protected Long fromIeeeBitvectorImpl(Long pNumber, FloatingPointType pTargetType) {
+ // MathSAT5 expects the mantissa to not include the sign bit
return Mathsat5NativeApi.msat_make_fp_from_ieeebv(
- mathsatEnv, pTargetType.getExponentSize(), pTargetType.getMantissaSize(), pNumber);
+ mathsatEnv,
+ pTargetType.getExponentSize(),
+ pTargetType.getMantissaSizeWithSignBit() - 1,
+ pNumber);
}
@Override
@@ -223,6 +254,17 @@ protected Long toIeeeBitvectorImpl(Long pNumber) {
return Mathsat5NativeApi.msat_make_fp_as_ieeebv(mathsatEnv, pNumber);
}
+ @Override
+ protected int getMantissaSizeWithSignBitImpl(Long f) {
+ // The mantissa includes the sign bit according to the SMTLib2 standard, but MathSAT does not.
+ return msat_get_fp_type_mant_width(mathsatEnv, msat_term_get_type(f)) + 1;
+ }
+
+ @Override
+ protected int getExponentSizeImpl(Long f) {
+ return msat_get_fp_type_exp_width(mathsatEnv, msat_term_get_type(f));
+ }
+
@Override
protected Long negate(Long pNumber) {
return msat_make_fp_neg(mathsatEnv, pNumber);
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java
index ff35694c4a..d39b2f7d3b 100644
--- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java
@@ -213,7 +213,7 @@ private FormulaType getFormulaTypeFromTermType(Long type) {
} else if (msat_is_bv_type(env, type)) {
return FormulaType.getBitvectorTypeWithSize(msat_get_bv_type_size(env, type));
} else if (msat_is_fp_type(env, type)) {
- return FormulaType.getFloatingPointType(
+ return FormulaType.getFloatingPointTypeWithoutSignBit(
msat_get_fp_type_exp_width(env, type), msat_get_fp_type_mant_width(env, type));
} else if (msat_is_fp_roundingmode_type(env, type)) {
return FormulaType.FloatingPointRoundingModeType;
@@ -241,7 +241,9 @@ public Long getBitvectorType(int pBitwidth) {
@Override
public Long getFloatingPointType(FloatingPointType pType) {
- return msat_get_fp_type(getEnv(), pType.getExponentSize(), pType.getMantissaSize());
+ // MathSAT5 automatically adds 1 to the mantissa, as it expects it to be without it.
+ return msat_get_fp_type(
+ getEnv(), pType.getExponentSize(), pType.getMantissaSizeWithSignBit() - 1);
}
@SuppressWarnings("unchecked")
@@ -575,13 +577,14 @@ private FloatingPointNumber parseFloatingPoint(String lTermRepresentation) {
BigInteger bits = new BigInteger(matcher.group(1));
int expWidth = Integer.parseInt(matcher.group(2));
- int mantWidth = Integer.parseInt(matcher.group(3));
+ // The term representation in MathSAT5 does not include the sign bit
+ int mantWidthWithoutSignBit = Integer.parseInt(matcher.group(3));
- Sign sign = Sign.of(bits.testBit(expWidth + mantWidth));
- BigInteger exponent = extractBitsFrom(bits, mantWidth, expWidth);
- BigInteger mantissa = extractBitsFrom(bits, 0, mantWidth);
+ Sign sign = Sign.of(bits.testBit(expWidth + mantWidthWithoutSignBit));
+ BigInteger exponent = extractBitsFrom(bits, mantWidthWithoutSignBit, expWidth);
+ BigInteger mantissa = extractBitsFrom(bits, 0, mantWidthWithoutSignBit);
- return FloatingPointNumber.of(sign, exponent, mantissa, expWidth, mantWidth);
+ return FloatingPointNumber.of(sign, exponent, mantissa, expWidth, mantWidthWithoutSignBit);
}
/**
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java
index 8ca17b8a2a..aaec8987bf 100644
--- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java
@@ -192,7 +192,8 @@ public static Mathsat5SolverContext create(
Mathsat5BitvectorFormulaManager bitvectorTheory =
new Mathsat5BitvectorFormulaManager(creator, booleanTheory);
Mathsat5FloatingPointFormulaManager floatingPointTheory =
- new Mathsat5FloatingPointFormulaManager(creator, pFloatingPointRoundingMode);
+ new Mathsat5FloatingPointFormulaManager(
+ creator, pFloatingPointRoundingMode, bitvectorTheory, booleanTheory);
Mathsat5ArrayFormulaManager arrayTheory = new Mathsat5ArrayFormulaManager(creator);
Mathsat5EnumerationFormulaManager enumerationTheory =
new Mathsat5EnumerationFormulaManager(creator);
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..d7714c401f 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java
@@ -20,14 +20,18 @@
class Z3FloatingPointFormulaManager
extends AbstractFloatingPointFormulaManager {
- private static final FloatingPointType highPrec = FormulaType.getFloatingPointType(15, 112);
+ private static final FloatingPointType highPrec =
+ FormulaType.getFloatingPointTypeWithoutSignBit(15, 112);
private final long z3context;
private final long roundingMode;
Z3FloatingPointFormulaManager(
- Z3FormulaCreator creator, FloatingPointRoundingMode pFloatingPointRoundingMode) {
- super(creator);
+ Z3FormulaCreator creator,
+ FloatingPointRoundingMode pFloatingPointRoundingMode,
+ Z3BitvectorFormulaManager pBvFormulaManager,
+ Z3BooleanFormulaManager pBoolFormulaManager) {
+ super(creator, pBvFormulaManager, pBoolFormulaManager);
z3context = creator.getEnv();
roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode);
}
@@ -78,7 +82,8 @@ protected Long makeNumberImpl(
final long signSort = getFormulaCreator().getBitvectorType(1);
final long expoSort = getFormulaCreator().getBitvectorType(type.getExponentSize());
- final long mantSort = getFormulaCreator().getBitvectorType(type.getMantissaSize());
+ final long mantSort =
+ getFormulaCreator().getBitvectorType(type.getMantissaSizeWithoutSignBit());
final long signBv = Native.mkNumeral(z3context, sign.isNegative() ? "1" : "0", signSort);
Native.incRef(z3context, signBv);
@@ -99,7 +104,7 @@ protected Long makeNumberAndRound(String pN, FloatingPointType pType, Long pRoun
// Z3 does not allow specifying a rounding mode for numerals,
// so we create it first with a high precision and then round it down explicitly.
if (pType.getExponentSize() <= highPrec.getExponentSize()
- || pType.getMantissaSize() <= highPrec.getMantissaSize()) {
+ || pType.getMantissaSizeWithSignBit() <= highPrec.getMantissaSizeWithSignBit()) {
long highPrecNumber = Native.mkNumeral(z3context, pN, mkFpaSort(highPrec));
Native.incRef(z3context, highPrecNumber);
long smallPrecNumber =
@@ -314,4 +319,14 @@ protected Long isNegative(Long pParam) {
protected Long round(Long pFormula, FloatingPointRoundingMode pRoundingMode) {
return Native.mkFpaRoundToIntegral(z3context, getRoundingModeImpl(pRoundingMode), pFormula);
}
+
+ @Override
+ protected int getMantissaSizeWithSignBitImpl(Long f) {
+ return Native.fpaGetEbits(z3context, Native.getSort(z3context, f));
+ }
+
+ @Override
+ protected int getExponentSizeImpl(Long f) {
+ return Native.fpaGetSbits(z3context, Native.getSort(z3context, f));
+ }
}
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 bde94b3e5f..890b5d8eac 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java
@@ -241,7 +241,7 @@ public FormulaType getFormulaTypeFromSort(Long pSort) {
return FormulaType.getArrayType(
getFormulaTypeFromSort(domainSort), getFormulaTypeFromSort(rangeSort));
case Z3_FLOATING_POINT_SORT:
- return FormulaType.getFloatingPointType(
+ return FormulaType.getFloatingPointTypeWithoutSignBit(
Native.fpaGetEbits(z3context, pSort), Native.fpaGetSbits(z3context, pSort) - 1);
case Z3_ROUNDING_MODE_SORT:
return FormulaType.FloatingPointRoundingModeType;
@@ -420,7 +420,8 @@ public Long getBitvectorType(int pBitwidth) {
@Override
public Long getFloatingPointType(FormulaType.FloatingPointType type) {
- long fpSort = Native.mkFpaSort(getEnv(), type.getExponentSize(), type.getMantissaSize() + 1);
+ long fpSort =
+ Native.mkFpaSort(getEnv(), type.getExponentSize(), type.getMantissaSizeWithSignBit());
Native.incRef(getEnv(), Native.sortToAst(getEnv(), fpSort));
return fpSort;
}
@@ -967,7 +968,7 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p
expo,
mant,
pType.getExponentSize(),
- pType.getMantissaSize());
+ pType.getMantissaSizeWithSignBit());
} else if (Native.fpaIsNumeralInf(environment, pValue)) {
// Floating Point Inf uses:
@@ -976,9 +977,11 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p
// - "00..00" as mantissa.
String sign = getSign(pValue).isNegative() ? "1" : "0";
return FloatingPointNumber.of(
- sign + "1".repeat(pType.getExponentSize()) + "0".repeat(pType.getMantissaSize()),
+ sign
+ + "1".repeat(pType.getExponentSize())
+ + "0".repeat(pType.getMantissaSizeWithSignBit()),
pType.getExponentSize(),
- pType.getMantissaSize());
+ pType.getMantissaSizeWithSignBit());
} else if (Native.fpaIsNumeralNan(environment, pValue)) {
// TODO We are underspecified here and choose several bits on our own.
@@ -988,9 +991,11 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p
// - "11..11" as exponent,
// - an unspecified mantissa (we choose all "1").
return FloatingPointNumber.of(
- "0" + "1".repeat(pType.getExponentSize()) + "1".repeat(pType.getMantissaSize()),
+ "0"
+ + "1".repeat(pType.getExponentSize())
+ + "1".repeat(pType.getMantissaSizeWithSignBit()),
pType.getExponentSize(),
- pType.getMantissaSize());
+ pType.getMantissaSizeWithSignBit());
} else {
Sign sign = getSign(pValue);
@@ -1003,7 +1008,7 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p
new BigInteger(exponent),
new BigInteger(mantissa),
pType.getExponentSize(),
- pType.getMantissaSize());
+ pType.getMantissaSizeWithSignBit());
}
}
diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java
index 7d408faf11..80f9bd6904 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java
@@ -186,7 +186,8 @@ public static synchronized Z3SolverContext create(
Z3BitvectorFormulaManager bitvectorTheory =
new Z3BitvectorFormulaManager(creator, booleanTheory);
Z3FloatingPointFormulaManager floatingPointTheory =
- new Z3FloatingPointFormulaManager(creator, pFloatingPointRoundingMode);
+ new Z3FloatingPointFormulaManager(
+ creator, pFloatingPointRoundingMode, bitvectorTheory, booleanTheory);
Z3QuantifiedFormulaManager quantifierManager = new Z3QuantifiedFormulaManager(creator);
Z3ArrayFormulaManager arrayManager = new Z3ArrayFormulaManager(creator);
Z3StringFormulaManager stringTheory = new Z3StringFormulaManager(creator);
diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java
index 74390241cf..00b1af6168 100644
--- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java
+++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java
@@ -15,6 +15,7 @@
import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableMap;
import com.google.common.collect.ImmutableSet;
import com.google.common.collect.Lists;
import java.math.BigDecimal;
@@ -41,6 +42,7 @@
import org.sosy_lab.java_smt.api.ProverEnvironment;
import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula;
public class FloatingPointFormulaManagerTest
extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
@@ -73,9 +75,35 @@ public void init() {
one = fpmgr.makeNumber(1.0, singlePrecType);
}
+ @Test
+ public void testSpecialNumberIdentity() {
+ assertThat(fpmgr.makeNaN(singlePrecType)).isEqualTo(nan);
+ assertThat(fpmgr.makePlusInfinity(singlePrecType)).isEqualTo(posInf);
+ assertThat(fpmgr.makeMinusInfinity(singlePrecType)).isEqualTo(negInf);
+ assertThat(fpmgr.makeNumber(0.0, singlePrecType)).isEqualTo(zero);
+ assertThat(fpmgr.makeNumber(-0.0, singlePrecType)).isEqualTo(negZero);
+
+ assertThat(fpmgr.makeNaN(doublePrecType)).isEqualTo(fpmgr.makeNaN(doublePrecType));
+ assertThat(fpmgr.makePlusInfinity(doublePrecType))
+ .isEqualTo(fpmgr.makePlusInfinity(doublePrecType));
+ assertThat(fpmgr.makeMinusInfinity(doublePrecType))
+ .isEqualTo(fpmgr.makeMinusInfinity(doublePrecType));
+ assertThat(fpmgr.makeNumber(0.0, doublePrecType))
+ .isEqualTo(fpmgr.makeNumber(0.0, doublePrecType));
+ assertThat(fpmgr.makeNumber(-0.0, doublePrecType))
+ .isEqualTo(fpmgr.makeNumber(-0.0, doublePrecType));
+
+ // Different precisions should not be equal
+ assertThat(fpmgr.makeNaN(doublePrecType)).isNotEqualTo(nan);
+ assertThat(fpmgr.makePlusInfinity(doublePrecType)).isNotEqualTo(posInf);
+ assertThat(fpmgr.makeMinusInfinity(doublePrecType)).isNotEqualTo(negInf);
+ assertThat(fpmgr.makeNumber(0.0, doublePrecType)).isNotEqualTo(zero);
+ assertThat(fpmgr.makeNumber(-0.0, doublePrecType)).isNotEqualTo(negZero);
+ }
+
@Test
public void floatingPointType() {
- FloatingPointType type = FormulaType.getFloatingPointType(23, 42);
+ FloatingPointType type = FormulaType.getFloatingPointTypeWithoutSignBit(23, 42);
FloatingPointFormula var = fpmgr.makeVariable("x", type);
FloatingPointType result = (FloatingPointType) mgr.getFormulaType(var);
@@ -83,8 +111,8 @@ public void floatingPointType() {
.that(result.getExponentSize())
.isEqualTo(type.getExponentSize());
assertWithMessage("mantissa size")
- .that(result.getMantissaSize())
- .isEqualTo(type.getMantissaSize());
+ .that(result.getMantissaSizeWithSignBit())
+ .isEqualTo(type.getMantissaSizeWithSignBit());
}
@Test
@@ -258,7 +286,7 @@ public void fpRemainderNormal() throws SolverException, InterruptedException {
for (FloatingPointType prec :
new FloatingPointType[] {
- singlePrecType, doublePrecType, FormulaType.getFloatingPointType(5, 6),
+ singlePrecType, doublePrecType, FormulaType.getFloatingPointTypeWithoutSignBit(5, 6),
}) {
final FloatingPointFormula numFive = fpmgr.makeNumber(5, prec);
@@ -282,7 +310,7 @@ public void fpRemainderSpecial() throws SolverException, InterruptedException {
for (FloatingPointType prec :
new FloatingPointType[] {
- singlePrecType, doublePrecType, FormulaType.getFloatingPointType(5, 6),
+ singlePrecType, doublePrecType, FormulaType.getFloatingPointTypeWithoutSignBit(5, 6),
}) {
final FloatingPointFormula num = fpmgr.makeNumber(42, prec);
@@ -408,7 +436,7 @@ public void specialValueFunctionsFrom64Bits() throws SolverException, Interrupte
@Test
public void specialValueFunctionsFrom32Bits2() throws SolverException, InterruptedException {
requireBitvectors();
- requireFPToBitvector();
+ requireNativeFPToBitvector();
final FloatingPointFormula x = fpmgr.makeVariable("x32", singlePrecType);
final BitvectorFormula signBit = bvmgr.extract(fpmgr.toIeeeBitvector(x), 31, 31);
@@ -453,7 +481,7 @@ public void specialValueFunctionsFrom32Bits2() throws SolverException, Interrupt
@Test
public void specialValueFunctionsFrom64Bits2() throws SolverException, InterruptedException {
requireBitvectors();
- requireFPToBitvector();
+ requireNativeFPToBitvector();
final FloatingPointFormula x = fpmgr.makeVariable("x64", doublePrecType);
final BitvectorFormula signBit = bvmgr.extract(fpmgr.toIeeeBitvector(x), 63, 63);
@@ -499,6 +527,346 @@ public void specialValueFunctionsFrom64Bits2() throws SolverException, Interrupt
bmgr.and(bmgr.not(fpmgr.isNaN(x)), bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1))));
}
+ // Same as specialValueFunctionsFrom32Bits2, but with fallback toIeeeBitvector() implementation.
+ @Test
+ public void specialValueFunctionsFrom32Bits2ToIeeeFallback()
+ throws SolverException, InterruptedException {
+ requireBitvectors();
+
+ final FloatingPointFormula x = fpmgr.makeVariable("x32", singlePrecType);
+ BitvectorFormulaAndBooleanFormula xToIeeeAndAddConstraint =
+ fpmgr.toIeeeBitvector(x, "bvConst_x");
+ BitvectorFormula xToIeee = xToIeeeAndAddConstraint.getBitvectorFormula();
+ final BitvectorFormula signBit = bvmgr.extract(xToIeee, 31, 31);
+ final BitvectorFormula exponent = bvmgr.extract(xToIeee, 30, 23);
+ final BitvectorFormula mantissa = bvmgr.extract(xToIeee, 22, 0);
+ final BooleanFormula additionalConstraint = xToIeeeAndAddConstraint.getBooleanFormula();
+
+ assertThatFormula(
+ bmgr.implication(
+ additionalConstraint,
+ bmgr.equivalence(
+ fpmgr.isInfinity(x),
+ bmgr.or(
+ bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x7f80_0000L)),
+ bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0xff80_0000L))))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ additionalConstraint,
+ bmgr.equivalence(
+ fpmgr.isZero(x),
+ bmgr.or(
+ bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x0000_0000)),
+ bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x8000_0000L))))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ additionalConstraint,
+ bmgr.equivalence(
+ fpmgr.isNormal(x),
+ bmgr.and(
+ bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0))),
+ bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1)))))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ additionalConstraint,
+ bmgr.equivalence(
+ fpmgr.isSubnormal(x),
+ bmgr.and(
+ bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0)),
+ bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0)))))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ additionalConstraint,
+ bmgr.equivalence(
+ fpmgr.isNaN(x),
+ bmgr.and(
+ bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1)),
+ bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0)))))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ additionalConstraint,
+ bmgr.equivalence(
+ fpmgr.isNegative(x),
+ bmgr.and(
+ bmgr.not(fpmgr.isNaN(x)),
+ bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1))))))
+ .isTautological();
+ }
+
+ // Same as specialValueFunctionsFrom64Bits2, but with fallback toIeeeBitvector() implementation.
+ @Test
+ public void specialValueFunctionsFrom64Bits2ToIeeeFallback()
+ throws SolverException, InterruptedException {
+ requireBitvectors();
+
+ final FloatingPointFormula x = fpmgr.makeVariable("x64", doublePrecType);
+ BitvectorFormulaAndBooleanFormula xToIeeeAndAddConstraint =
+ fpmgr.toIeeeBitvector(x, "bvConst_x");
+ BitvectorFormula xToIeee = xToIeeeAndAddConstraint.getBitvectorFormula();
+ final BitvectorFormula signBit = bvmgr.extract(xToIeee, 63, 63);
+ final BitvectorFormula exponent = bvmgr.extract(xToIeee, 62, 52);
+ final BitvectorFormula mantissa = bvmgr.extract(xToIeee, 51, 0);
+ final BooleanFormula additionalConstraint = xToIeeeAndAddConstraint.getBooleanFormula();
+
+ assertThatFormula(
+ bmgr.implication(
+ additionalConstraint,
+ bmgr.equivalence(
+ fpmgr.isInfinity(x),
+ bmgr.or(
+ bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x7ff0_0000_0000_0000L)),
+ bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0xfff0_0000_0000_0000L))))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ additionalConstraint,
+ bmgr.equivalence(
+ fpmgr.isZero(x),
+ bmgr.or(
+ bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x0000_0000_0000_0000L)),
+ bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x8000_0000_0000_0000L))))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ additionalConstraint,
+ bmgr.equivalence(
+ fpmgr.isNormal(x),
+ bmgr.and(
+ bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0))),
+ bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, -1)))))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ additionalConstraint,
+ bmgr.equivalence(
+ fpmgr.isSubnormal(x),
+ bmgr.and(
+ bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0)),
+ bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(52, 0)))))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ additionalConstraint,
+ bmgr.equivalence(
+ fpmgr.isNaN(x),
+ bmgr.and(
+ bvmgr.equal(exponent, bvmgr.makeBitvector(11, -1)),
+ bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(52, 0)))))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ additionalConstraint,
+ bmgr.equivalence(
+ fpmgr.isNegative(x),
+ bmgr.and(
+ bmgr.not(fpmgr.isNaN(x)),
+ bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1))))))
+ .isTautological();
+ }
+
+ // Same as specialValueFunctionsFrom32Bits2, but with fallback toIeeeBitvector() implementation
+ // with mapped special numbers.
+ @Test
+ public void specialValueFunctionsFrom32Bits2ToIeeeFallbackAlternatives()
+ throws SolverException, InterruptedException {
+ requireBitvectors();
+
+ final FloatingPointFormula x = fpmgr.makeVariable("x32", singlePrecType);
+ var nanBv = bvmgr.makeBitvector(32, 0x0110_0000L);
+ var negInfBv = bvmgr.makeBitvector(32, 0x7f80_0000L);
+ var posInfBv = bvmgr.makeBitvector(32, 0xff80_0000L);
+ BitvectorFormulaAndBooleanFormula xToIeeeAndAddConstraint =
+ fpmgr.toIeeeBitvector(
+ x,
+ "bvConst_x",
+ ImmutableMap.of(
+ fpmgr.makePlusInfinity(singlePrecType),
+ posInfBv,
+ fpmgr.makeMinusInfinity(singlePrecType),
+ negInfBv,
+ fpmgr.makeNaN(singlePrecType),
+ nanBv));
+ BitvectorFormula xToIeee = xToIeeeAndAddConstraint.getBitvectorFormula();
+ final BitvectorFormula signBit = bvmgr.extract(xToIeee, 31, 31);
+ final BitvectorFormula exponent = bvmgr.extract(xToIeee, 30, 23);
+ final BitvectorFormula mantissa = bvmgr.extract(xToIeee, 22, 0);
+ final BooleanFormula additionalConstraint = xToIeeeAndAddConstraint.getBooleanFormula();
+
+ assertThatFormula(
+ bmgr.implication(
+ bmgr.and(additionalConstraint, bmgr.not(fpmgr.isNegative(x)), fpmgr.isInfinity(x)),
+ bvmgr.equal(xToIeee, posInfBv)))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ bmgr.and(fpmgr.isNegative(x), fpmgr.isInfinity(x), additionalConstraint),
+ bvmgr.equal(xToIeee, negInfBv)))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ bmgr.and(fpmgr.isNaN(x), additionalConstraint), bvmgr.equal(xToIeee, nanBv)))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ bmgr.and(fpmgr.isZero(x), additionalConstraint),
+ bmgr.or(
+ bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x0000_0000)),
+ bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x8000_0000L)))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ bmgr.and(fpmgr.isNormal(x), additionalConstraint),
+ bmgr.and(
+ bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0))),
+ bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1))))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ bmgr.and(fpmgr.isSubnormal(x), additionalConstraint),
+ bmgr.and(
+ bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0)),
+ bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0))))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ bmgr.and(fpmgr.isNegative(x), bmgr.not(fpmgr.isInfinity(x)), additionalConstraint),
+ bmgr.and(
+ bmgr.not(fpmgr.isNaN(x)), bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1)))))
+ .isTautological();
+ }
+
+ // Same as specialValueFunctionsFrom64Bits2, but with fallback toIeeeBitvector() implementation
+ // with redefinitions for special values.
+ @Test
+ public void specialValueFunctionsFrom64Bits2ToIeeeFallbackAlternatives()
+ throws SolverException, InterruptedException {
+ requireBitvectors();
+
+ final FloatingPointFormula x = fpmgr.makeVariable("x64", doublePrecType);
+ var nanBv = bvmgr.makeBitvector(64, 0x0111_1000_0000_0000L);
+ var negInfBv = bvmgr.makeBitvector(64, 0x0000_0000_0000_0001L);
+ var posInfBv = bvmgr.makeBitvector(64, 0x0000_0000_0000_0000L);
+ BitvectorFormulaAndBooleanFormula xToIeeeAndAddConstraint =
+ fpmgr.toIeeeBitvector(
+ x,
+ "bvConst_x",
+ ImmutableMap.of(
+ fpmgr.makePlusInfinity(doublePrecType),
+ posInfBv,
+ fpmgr.makeMinusInfinity(doublePrecType),
+ negInfBv,
+ fpmgr.makeNaN(doublePrecType),
+ nanBv));
+ BitvectorFormula xToIeee = xToIeeeAndAddConstraint.getBitvectorFormula();
+ final BitvectorFormula signBit = bvmgr.extract(xToIeee, 63, 63);
+ final BitvectorFormula exponent = bvmgr.extract(xToIeee, 62, 52);
+ final BitvectorFormula mantissa = bvmgr.extract(xToIeee, 51, 0);
+ final BooleanFormula additionalConstraint = xToIeeeAndAddConstraint.getBooleanFormula();
+
+ assertThatFormula(
+ bmgr.implication(
+ bmgr.and(bmgr.not(fpmgr.isNegative(x)), fpmgr.isInfinity(x), additionalConstraint),
+ bvmgr.equal(xToIeee, posInfBv)))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ bmgr.and(fpmgr.isNegative(x), fpmgr.isInfinity(x), additionalConstraint),
+ bvmgr.equal(xToIeee, negInfBv)))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ bmgr.and(fpmgr.isNaN(x), additionalConstraint), bvmgr.equal(xToIeee, nanBv)))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ bmgr.and(fpmgr.isZero(x), additionalConstraint),
+ bmgr.or(
+ bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x0000_0000_0000_0000L)),
+ bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x8000_0000_0000_0000L)))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ bmgr.and(fpmgr.isNormal(x), additionalConstraint),
+ bmgr.and(
+ bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0))),
+ bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, -1))))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ bmgr.and(fpmgr.isSubnormal(x), additionalConstraint),
+ bmgr.and(
+ bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0)),
+ bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(52, 0))))))
+ .isTautological();
+
+ assertThatFormula(
+ bmgr.implication(
+ bmgr.and(fpmgr.isNegative(x), bmgr.not(fpmgr.isInfinity(x)), additionalConstraint),
+ bmgr.and(
+ bmgr.not(fpmgr.isNaN(x)), bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1)))))
+ .isTautological();
+ }
+
+ @Test
+ public void floatingPointSinglePrecisionSizeWithBvTransformationTest() {
+ requireBitvectors();
+ int fpSinglePrecSize = 32;
+ var bv32 = bvmgr.makeBitvector(fpSinglePrecSize, 0);
+ assertThat(bvmgr.getLength(bv32)).isEqualTo(fpSinglePrecSize);
+
+ requireFloats();
+ var singlePrec = FormulaType.getSinglePrecisionFloatingPointType();
+ var fpSinglePrec = fpmgr.makeNumber(0.0, singlePrec);
+ // Sizes of the type and the actual term should match
+ assertThat(fpmgr.getExponentSize(fpSinglePrec)).isEqualTo(8);
+ assertThat(fpmgr.getMantissaSizeWithSignBit(fpSinglePrec)).isEqualTo(24);
+ assertThat(singlePrec.getExponentSize()).isEqualTo(8);
+ assertThat(singlePrec.getMantissaSizeWithSignBit()).isEqualTo(24);
+ assertThat(singlePrec.getExponentSize() + singlePrec.getMantissaSizeWithSignBit())
+ .isEqualTo(fpSinglePrecSize);
+ assertThat(singlePrec.getTotalSize())
+ .isEqualTo(singlePrec.getExponentSize() + singlePrec.getMantissaSizeWithSignBit());
+
+ assertThat(bvmgr.getLength(fpmgr.toIeeeBitvector(fpSinglePrec, "dummy1").getBitvectorFormula()))
+ .isEqualTo(fpSinglePrecSize);
+ assertThat(
+ bvmgr.getLength(
+ fpmgr
+ .toIeeeBitvector(fpSinglePrec, "dummy2", ImmutableMap.of())
+ .getBitvectorFormula()))
+ .isEqualTo(fpSinglePrecSize);
+
+ if (solverSupportsNativeFPToBitvector()) {
+ assertThat(bvmgr.getLength(fpmgr.toIeeeBitvector(fpSinglePrec))).isEqualTo(fpSinglePrecSize);
+ }
+ }
+
@Test
public void specialDoubles() throws SolverException, InterruptedException {
assertThatFormula(fpmgr.assignment(fpmgr.makeNumber(Double.NaN, singlePrecType), nan))
@@ -536,7 +904,7 @@ public void numberConstants() throws SolverException, InterruptedException {
checkEqualityOfNumberConstantsFor(3.4028234663852886e+38, doublePrecType);
// check unequality for large types
- FloatingPointType nearDouble = FormulaType.getFloatingPointType(12, 52);
+ FloatingPointType nearDouble = FormulaType.getFloatingPointTypeWithoutSignBit(12, 52);
FloatingPointFormula h1 =
fpmgr.makeNumber(BigDecimal.TEN.pow(309).multiply(BigDecimal.valueOf(1.0001)), nearDouble);
FloatingPointFormula h2 =
@@ -544,7 +912,7 @@ public void numberConstants() throws SolverException, InterruptedException {
assertThatFormula(fpmgr.equalWithFPSemantics(h1, h2)).isUnsatisfiable();
// check equality for short types
- FloatingPointType smallType = FormulaType.getFloatingPointType(4, 4);
+ FloatingPointType smallType = FormulaType.getFloatingPointTypeWithoutSignBit(4, 4);
FloatingPointFormula i1 =
fpmgr.makeNumber(BigDecimal.TEN.pow(50).multiply(BigDecimal.valueOf(1.001)), smallType);
FloatingPointFormula i2 =
@@ -573,7 +941,7 @@ public void numberConstants() throws SolverException, InterruptedException {
assertThatFormula(fpmgr.isNegative(ni2)).isTautological();
// check equality for short types
- FloatingPointType smallType2 = FormulaType.getFloatingPointType(4, 4);
+ FloatingPointType smallType2 = FormulaType.getFloatingPointTypeWithoutSignBit(4, 4);
FloatingPointFormula j1 =
fpmgr.makeNumber(BigDecimal.TEN.pow(500).multiply(BigDecimal.valueOf(1.001)), smallType2);
FloatingPointFormula j2 =
@@ -604,7 +972,7 @@ public void numberConstants() throws SolverException, InterruptedException {
// Z3 supports at least FloatingPointType(15, 112). Larger types seem to be rounded.
if (!ImmutableSet.of(Solvers.Z3, Solvers.CVC4).contains(solver)) {
// check unequality for very large types
- FloatingPointType largeType = FormulaType.getFloatingPointType(100, 100);
+ FloatingPointType largeType = FormulaType.getFloatingPointTypeWithoutSignBit(100, 100);
FloatingPointFormula k1 =
fpmgr.makeNumber(BigDecimal.TEN.pow(200).multiply(BigDecimal.valueOf(1.001)), largeType);
FloatingPointFormula k2 =
@@ -641,7 +1009,7 @@ public void numberConstantsNearInf() throws SolverException, InterruptedExceptio
private void checkNearInf(int mantissa, int exponent, long value)
throws SolverException, InterruptedException {
- FloatingPointType type = FormulaType.getFloatingPointType(exponent, mantissa);
+ FloatingPointType type = FormulaType.getFloatingPointTypeWithoutSignBit(exponent, mantissa);
FloatingPointFormula fp1 = fpmgr.makeNumber(BigDecimal.valueOf(value), type);
assertThatFormula(fpmgr.isInfinity(fp1)).isTautological();
FloatingPointFormula fp2 = fpmgr.makeNumber(BigDecimal.valueOf(value - 1), type);
@@ -676,7 +1044,7 @@ public void numberConstantsNearMinusInf() throws SolverException, InterruptedExc
private void checkNearMinusInf(int mantissa, int exponent, long value)
throws SolverException, InterruptedException {
- FloatingPointType type = FormulaType.getFloatingPointType(exponent, mantissa);
+ FloatingPointType type = FormulaType.getFloatingPointTypeWithoutSignBit(exponent, mantissa);
FloatingPointFormula fp1 = fpmgr.makeNumber(BigDecimal.valueOf(value), type);
assertThatFormula(fpmgr.isInfinity(fp1)).isTautological();
FloatingPointFormula fp2 = fpmgr.makeNumber(BigDecimal.valueOf(value + 1), type);
@@ -956,7 +1324,7 @@ public void fpTraversalWithRoundingMode() {
@Test
public void fpIeeeConversionTypes() {
- requireFPToBitvector();
+ requireNativeFPToBitvector();
FloatingPointFormula var = fpmgr.makeVariable("var", singlePrecType);
assertThat(mgr.getFormulaType(fpmgr.toIeeeBitvector(var)))
@@ -965,7 +1333,7 @@ public void fpIeeeConversionTypes() {
@Test
public void fpIeeeConversion() throws SolverException, InterruptedException {
- requireFPToBitvector();
+ requireNativeFPToBitvector();
FloatingPointFormula var = fpmgr.makeVariable("var", singlePrecType);
assertThatFormula(
@@ -976,7 +1344,7 @@ public void fpIeeeConversion() throws SolverException, InterruptedException {
@Test
public void ieeeFpConversion() throws SolverException, InterruptedException {
- requireFPToBitvector();
+ requireNativeFPToBitvector();
BitvectorFormula var = bvmgr.makeBitvector(32, 123456789);
assertThatFormula(
@@ -1046,7 +1414,7 @@ public void checkIeeeBv2FpConversion64() throws SolverException, InterruptedExce
@Test
public void checkIeeeFp2BvConversion32() throws SolverException, InterruptedException {
- requireFPToBitvector();
+ requireNativeFPToBitvector();
proveForAll(
// makeBV(value.bits) == fromFP(makeFP(value.float))
@@ -1059,7 +1427,7 @@ public void checkIeeeFp2BvConversion32() throws SolverException, InterruptedExce
@Test
public void checkIeeeFp2BvConversion64() throws SolverException, InterruptedException {
- requireFPToBitvector();
+ requireNativeFPToBitvector();
proveForAll(
// makeBV(value.bits) == fromFP(makeFP(value.float))
@@ -1215,9 +1583,16 @@ public void fpModelValue() throws SolverException, InterruptedException {
Float.MIN_VALUE,
Float.MIN_NORMAL,
}) {
- FloatingPointNumber fiveValue = model.evaluate(fpmgr.makeNumber(f, singlePrecType));
- assertThat(fiveValue.floatValue()).isEqualTo(f);
- assertThat(fiveValue.doubleValue()).isEqualTo((double) f);
+ var constFpNum = fpmgr.makeNumber(f, singlePrecType);
+ assertThat(fpmgr.getMantissaSizeWithSignBit(constFpNum))
+ .isEqualTo(singlePrecType.getMantissaSizeWithSignBit());
+ FloatingPointNumber fpValue = model.evaluate(constFpNum);
+ assertThat(fpValue.getMantissaSizeWithSignBit())
+ .isEqualTo(singlePrecType.getMantissaSizeWithSignBit());
+ assertThat(fpValue.getMantissaSizeWithoutSignBit())
+ .isEqualTo(singlePrecType.getMantissaSizeWithSignBit() - 1);
+ assertThat(fpValue.floatValue()).isEqualTo(f);
+ assertThat(fpValue.doubleValue()).isEqualTo((double) f);
}
}
}
@@ -1266,16 +1641,28 @@ public void fpFrom32BitPattern() throws SolverException, InterruptedException {
final FloatingPointFormula fpFromBv =
fpmgr.makeNumber(
BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, singlePrecType);
+ assertThat(fpmgr.getMantissaSizeWithSignBit(fpFromBv) + fpmgr.getExponentSize(fpFromBv))
+ .isEqualTo(singlePrecType.getTotalSize());
final FloatingPointNumber fpNumber =
FloatingPointNumber.of(
sign,
BigInteger.valueOf(exponent),
BigInteger.valueOf(mantissa),
singlePrecType.getExponentSize(),
- singlePrecType.getMantissaSize());
+ singlePrecType.getMantissaSizeWithoutSignBit());
+ assertThat(fpNumber.getMantissaSizeWithSignBit())
+ .isEqualTo(singlePrecType.getMantissaSizeWithSignBit());
+ assertThat(fpNumber.getMantissaSizeWithoutSignBit())
+ .isEqualTo(singlePrecType.getMantissaSizeWithSignBit() - 1);
final FloatingPointFormula fp1 = fpmgr.makeNumber(fpNumber);
+ assertThat(fpmgr.getMantissaSizeWithSignBit(fp1) + fpmgr.getExponentSize(fp1))
+ .isEqualTo(singlePrecType.getTotalSize());
final FloatingPointFormula fp2 = fpmgr.makeNumber(pFloat, singlePrecType);
- return bmgr.and(fpmgr.assignment(fpFromBv, fp1), fpmgr.assignment(fpFromBv, fp2));
+ assertThat(fpmgr.getMantissaSizeWithSignBit(fp2) + fpmgr.getExponentSize(fp2))
+ .isEqualTo(singlePrecType.getTotalSize());
+ final BooleanFormula assignment1 = fpmgr.assignment(fpFromBv, fp1);
+ final BooleanFormula assignment2 = fpmgr.assignment(fpFromBv, fp2);
+ return bmgr.and(assignment1, assignment2);
});
}
@@ -1292,16 +1679,28 @@ public void fpFrom64BitPattern() throws SolverException, InterruptedException {
final FloatingPointFormula fpFromBv =
fpmgr.makeNumber(
BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, doublePrecType);
+ assertThat(fpmgr.getMantissaSizeWithSignBit(fpFromBv) + fpmgr.getExponentSize(fpFromBv))
+ .isEqualTo(doublePrecType.getTotalSize());
final FloatingPointNumber fpNumber =
FloatingPointNumber.of(
sign,
BigInteger.valueOf(exponent),
BigInteger.valueOf(mantissa),
doublePrecType.getExponentSize(),
- doublePrecType.getMantissaSize());
+ doublePrecType.getMantissaSizeWithoutSignBit());
+ assertThat(fpNumber.getMantissaSizeWithSignBit())
+ .isEqualTo(doublePrecType.getMantissaSizeWithSignBit());
+ assertThat(fpNumber.getMantissaSizeWithoutSignBit())
+ .isEqualTo(doublePrecType.getMantissaSizeWithSignBit() - 1);
final FloatingPointFormula fp1 = fpmgr.makeNumber(fpNumber);
+ assertThat(fpmgr.getMantissaSizeWithSignBit(fp1) + fpmgr.getExponentSize(fp1))
+ .isEqualTo(doublePrecType.getTotalSize());
final FloatingPointFormula fp2 = fpmgr.makeNumber(pDouble, doublePrecType);
- return bmgr.and(fpmgr.assignment(fpFromBv, fp1), fpmgr.assignment(fpFromBv, fp2));
+ assertThat(fpmgr.getMantissaSizeWithSignBit(fp2) + fpmgr.getExponentSize(fp2))
+ .isEqualTo(doublePrecType.getTotalSize());
+ final BooleanFormula assignment1 = fpmgr.assignment(fpFromBv, fp1);
+ final BooleanFormula assignment2 = fpmgr.assignment(fpFromBv, fp2);
+ return bmgr.and(assignment1, assignment2);
});
}
diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java
index e96c7b39f1..85cd1c1574 100644
--- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java
+++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java
@@ -242,18 +242,34 @@ protected final void requireBitvectorToInt() {
}
@SuppressWarnings("CheckReturnValue")
- protected final void requireFPToBitvector() {
+ protected final void requireNativeFPToBitvector() {
requireFloats();
try {
fpmgr.toIeeeBitvector(fpmgr.makeNumber(0, getSinglePrecisionFloatingPointType()));
} catch (UnsupportedOperationException e) {
assume()
- .withMessage("Solver %s does not yet support FP-to-BV conversion", solverToUse())
+ .withMessage(
+ "Solver %s does not support FP-to-BV conversion, use the fallback methods "
+ + "FloatingPointFormulaManager#toIeeeBitvector(FloatingPointFormula, "
+ + "String, Map) and/or FloatingPointFormulaManager#toIeeeBitvector"
+ + "(FloatingPointFormula, String).",
+ solverToUse())
.that(solverToUse())
.isNull();
}
}
+ @SuppressWarnings("CheckReturnValue")
+ protected final boolean solverSupportsNativeFPToBitvector() {
+ requireFloats();
+ try {
+ fpmgr.toIeeeBitvector(fpmgr.makeNumber(0, getSinglePrecisionFloatingPointType()));
+ return true;
+ } catch (UnsupportedOperationException e) {
+ return false;
+ }
+ }
+
/** Skip test if the solver does not support quantifiers. */
protected final void requireQuantifiers() {
assume()
diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java
index 56b0200874..bd072cd759 100644
--- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java
+++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java
@@ -477,13 +477,14 @@ public void floatConstantVisit() {
Integer.toBinaryString(Float.floatToRawIntBits(entry.getKey().floatValue())),
32,
'0'));
- checkFloatConstant(FormulaType.getFloatingPointType(5, 10), entry.getKey(), entry.getValue());
+ checkFloatConstant(
+ FormulaType.getFloatingPointTypeWithoutSignBit(5, 10), entry.getKey(), entry.getValue());
}
}
private void checkFloatConstant(FloatingPointType prec, double value, String bits) {
FloatingPointNumber fp =
- FloatingPointNumber.of(bits, prec.getExponentSize(), prec.getMantissaSize());
+ FloatingPointNumber.of(bits, prec.getExponentSize(), prec.getMantissaSizeWithSignBit());
ConstantsVisitor visitor = new ConstantsVisitor();
mgr.visit(fpmgr.makeNumber(value, prec), visitor);
@@ -580,7 +581,7 @@ public void fpToBvTest() {
.that(solverToUse())
.isNoneOf(Solvers.CVC4, Solvers.CVC5);
- var fpType = FormulaType.getFloatingPointType(5, 10);
+ var fpType = FormulaType.getFloatingPointTypeWithoutSignBit(5, 10);
var visitor =
new DefaultFormulaVisitor() {
@Override