diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index 16a04dcb17..bc89215d47 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -299,12 +299,43 @@ FloatingPointFormula castFrom( FloatingPointFormula fromIeeeBitvector(BitvectorFormula number, FloatingPointType pTargetType); /** - * Create a formula that produces a representation of the given floating-point value as a - * bitvector conforming to the IEEE 754-2008 FP format. The bit size of the resulting bitvector is - * equal to the total size of the {@link FloatingPointNumber}s precision. + * Returns a {@link BitvectorFormula} equal to the representation of the given floating-point + * value as a bitvector conforming to the IEEE 754-2008 FP format. The bit size of the resulting + * bitvector is equal to the {@link FloatingPointType#getTotalSize()} of the {@link + * FloatingPointFormula}. This method is not natively supported by all solvers, and SMTLIB2 output + * generated containing formulas originating from this method is often not parsable by other + * solvers. You can use the method {@link #bitwiseEqual(FloatingPointFormula, BitvectorFormula)} + * to avoid both problems. */ BitvectorFormula toIeeeBitvector(FloatingPointFormula number); + /** + * Create a {@link BooleanFormula} representing the equality of the bitvector representation of + * the given {@link FloatingPointFormula}s value, conforming to the IEEE 754-2008 floating-point + * format, with the given {@link BitvectorFormula}. The size of the given {@link BitvectorFormula} + * has to be equal to the size returned by {@link FloatingPointType#getTotalSize()} of the given + * {@link FloatingPointFormula}. 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 solver dependent. This method is based on a suggestion in the (SMTLIB2 standard) and is equal to: + * + *

assignment(fromIeeeBitvector(bitvectorValue), floatValue) + * + *

Note: SMTLIB2 output of this method uses the SMTLIB2 function symbol 'to_fp', for example + * like this: (assert (= ((_ to_fp eb sb) bitvectorValue) floatValue)) with eb being the bit size + * returned by {@link FloatingPointType#getExponentSize()} and sb being the bit size returned by + * {@link FloatingPointType#getMantissaSizeWithHiddenBit()} of the {@link FloatingPointType} of + * floatValue. + * + * @param floatValue the {@link FloatingPointFormula} to be converted into an IEEE bitvector. + * @param bitvectorValue a {@link BitvectorFormula} that is set to be equal to the IEEE bitvector + * representation of the {@link FloatingPointFormula} parameter. + * @return a {@link BooleanFormula} representing the result of the equality of the two parameters, + * i.e. (= ((_ to_fp eb sb) bitvectorValue) floatValue). + */ + BooleanFormula bitwiseEqual(FloatingPointFormula floatValue, BitvectorFormula bitvectorValue); + FloatingPointFormula round(FloatingPointFormula formula, FloatingPointRoundingMode roundingMode); // ----------------- Arithmetic relations, return type NumeralFormula ----------------- diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index c662162411..86e69e27c1 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -8,13 +8,15 @@ 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.basicimpl.AbstractFormulaManager.checkVariableName; -import com.google.common.base.Preconditions; import java.math.BigDecimal; import java.math.BigInteger; import java.util.HashMap; import java.util.Map; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.MoreStrings; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.BitvectorFormula; @@ -48,10 +50,14 @@ public abstract class AbstractFloatingPointFormulaManager roundingModes; + private final AbstractBitvectorFormulaManager bvMgr; + protected AbstractFloatingPointFormulaManager( - FormulaCreator pCreator) { + FormulaCreator pCreator, + AbstractBitvectorFormulaManager pBvMgr) { super(pCreator); roundingModes = new HashMap<>(); + bvMgr = pBvMgr; } protected abstract TFormulaInfo getDefaultRoundingMode(); @@ -75,30 +81,62 @@ public FloatingPointRoundingMode fromRoundingModeFormula( return getFormulaCreator().getRoundingMode(extractInfo(pRoundingModeFormula)); } - protected FloatingPointFormula wrap(TFormulaInfo pTerm) { + /** + * Wraps a native floating-point term in a JavaSMT {@link FloatingPointFormula}. If the {@link + * FloatingPointType} of the term is not available, please use {@link + * AbstractFloatingPointFormulaManager#wrap(Object)} + * + * @param pTypeForAssertions the {@link FloatingPointType} used to create pTerm. This argument is + * only used to verify the exponent and mantissa sizes of pTerm. + */ + protected FloatingPointFormula wrap( + TFormulaInfo pTerm, @Nullable FloatingPointType pTypeForAssertions) { + FormulaType type = getFormulaCreator().getFormulaType(pTerm); + // The type derived from the term in the creator is usually built from the exponent and + // mantissa sizes, hence comparing it to the type used to create the FP term checks that it + // was created correctly. (There are other tests checking FP type correctness) + if (pTypeForAssertions != null) { + assert type.equals(pTypeForAssertions) + : "Floating-Point formula %s with type %s is not equal to expected type %s" + .formatted(pTerm, type, pTypeForAssertions); + } else { + assert type.isFloatingPointType() + : "Floating-Point formula %s has unexpected type: %s".formatted(pTerm, type); + } + return getFormulaCreator().encapsulateFloatingPoint(pTerm); } + /** + * Wraps a native floating-point term in a JavaSMT {@link FloatingPointFormula}. Please use {@link + * AbstractFloatingPointFormulaManager#wrap(Object, FloatingPointType)} if the {@link + * FloatingPointType} of the term is available. + */ + protected FloatingPointFormula wrap(TFormulaInfo pTerm) { + return wrap(pTerm, null); + } + @Override public FloatingPointFormula makeNumber(Rational n, FormulaType.FloatingPointType type) { - return wrap(makeNumberImpl(n.toString(), type, getDefaultRoundingMode())); + return wrap(makeNumberImpl(n.toString(), type, getDefaultRoundingMode()), type); } @Override public FloatingPointFormula makeNumber( Rational n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode) { - return wrap(makeNumberImpl(n.toString(), type, getRoundingMode(pFloatingPointRoundingMode))); + return wrap( + makeNumberImpl(n.toString(), type, getRoundingMode(pFloatingPointRoundingMode)), type); } @Override public FloatingPointFormula makeNumber(double n, FormulaType.FloatingPointType type) { - return wrap(makeNumberImpl(n, type, getDefaultRoundingMode())); + return wrap(makeNumberImpl(n, type, getDefaultRoundingMode()), type); } @Override public FloatingPointFormula makeNumber( double n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode) { - return wrap(makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode))); + return wrap(makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode)), type); } protected abstract TFormulaInfo makeNumberImpl( @@ -106,13 +144,13 @@ protected abstract TFormulaInfo makeNumberImpl( @Override public FloatingPointFormula makeNumber(BigDecimal n, FormulaType.FloatingPointType type) { - return wrap(makeNumberImpl(n, type, getDefaultRoundingMode())); + return wrap(makeNumberImpl(n, type, getDefaultRoundingMode()), type); } @Override public FloatingPointFormula makeNumber( BigDecimal n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode) { - return wrap(makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode))); + return wrap(makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode)), type); } protected TFormulaInfo makeNumberImpl( @@ -122,13 +160,13 @@ protected TFormulaInfo makeNumberImpl( @Override public FloatingPointFormula makeNumber(String n, FormulaType.FloatingPointType type) { - return wrap(makeNumberImpl(n, type, getDefaultRoundingMode())); + return wrap(makeNumberImpl(n, type, getDefaultRoundingMode()), type); } @Override public FloatingPointFormula makeNumber( String n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode) { - return wrap(makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode))); + return wrap(makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode)), type); } /** directly catch the most common special String constants. */ @@ -148,14 +186,14 @@ protected TFormulaInfo makeNumberImpl( @Override public FloatingPointFormula makeNumber( BigInteger exponent, BigInteger mantissa, Sign sign, FloatingPointType type) { - return wrap(makeNumberImpl(exponent, mantissa, sign, type)); + return wrap(makeNumberImpl(exponent, mantissa, sign, type), type); } 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); } @@ -171,7 +209,7 @@ protected abstract TFormulaInfo makeNumberAndRound( @Override public FloatingPointFormula makeVariable(String pVar, FormulaType.FloatingPointType pType) { checkVariableName(pVar); - return wrap(makeVariableImpl(pVar, pType)); + return wrap(makeVariableImpl(pVar, pType), pType); } protected abstract TFormulaInfo makeVariableImpl( @@ -179,21 +217,21 @@ protected abstract TFormulaInfo makeVariableImpl( @Override public FloatingPointFormula makePlusInfinity(FormulaType.FloatingPointType pType) { - return wrap(makePlusInfinityImpl(pType)); + return wrap(makePlusInfinityImpl(pType), pType); } protected abstract TFormulaInfo makePlusInfinityImpl(FormulaType.FloatingPointType pType); @Override public FloatingPointFormula makeMinusInfinity(FormulaType.FloatingPointType pType) { - return wrap(makeMinusInfinityImpl(pType)); + return wrap(makeMinusInfinityImpl(pType), pType); } protected abstract TFormulaInfo makeMinusInfinityImpl(FormulaType.FloatingPointType pType); @Override public FloatingPointFormula makeNaN(FormulaType.FloatingPointType pType) { - return wrap(makeNaNImpl(pType)); + return wrap(makeNaNImpl(pType), pType); } protected abstract TFormulaInfo makeNaNImpl(FormulaType.FloatingPointType pType); @@ -232,7 +270,9 @@ protected abstract TFormulaInfo castToImpl( @Override public FloatingPointFormula castFrom( Formula pNumber, boolean pSigned, FormulaType.FloatingPointType pTargetType) { - return wrap(castFromImpl(extractInfo(pNumber), pSigned, pTargetType, getDefaultRoundingMode())); + return wrap( + castFromImpl(extractInfo(pNumber), pSigned, pTargetType, getDefaultRoundingMode()), + pTargetType); } @Override @@ -243,7 +283,8 @@ public FloatingPointFormula castFrom( FloatingPointRoundingMode pFloatingPointRoundingMode) { return wrap( castFromImpl( - extractInfo(number), signed, targetType, getRoundingMode(pFloatingPointRoundingMode))); + extractInfo(number), signed, targetType, getRoundingMode(pFloatingPointRoundingMode)), + targetType); } protected abstract TFormulaInfo castFromImpl( @@ -256,7 +297,7 @@ protected abstract TFormulaInfo castFromImpl( public FloatingPointFormula fromIeeeBitvector( BitvectorFormula pNumber, FloatingPointType pTargetType) { BitvectorType bvType = (BitvectorType) formulaCreator.getFormulaType(pNumber); - Preconditions.checkArgument( + checkArgument( bvType.getSize() == pTargetType.getTotalSize(), MoreStrings.lazyString( () -> @@ -273,7 +314,34 @@ 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 " + + "floating-point formulas to IEEE bitvectors natively"); + } + + @Override + public BooleanFormula bitwiseEqual( + FloatingPointFormula floatValue, BitvectorFormula bitvectorValue) { + FormulaType.FloatingPointType fpType = + (FloatingPointType) getFormulaCreator().getFormulaType(floatValue); + checkArgument( + fpType.getTotalSize() == bvMgr.getLength(bitvectorValue), + "The size of the bitvector term %s is %s, but needs to be equal to the size of" + + " the Floating-Point term %s with size %s", + bitvectorValue, + bvMgr.getLength(bitvectorValue), + floatValue, + fpType.getTotalSize()); + + FloatingPointFormula fromIeeeBitvector = fromIeeeBitvector(bitvectorValue, fpType); + + // We use assignment(), as it allows a fp 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. + return assignment(fromIeeeBitvector, floatValue); + } @Override public FloatingPointFormula negate(FloatingPointFormula pNumber) { diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java index bf9d444153..1313c2ef42 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -377,23 +377,28 @@ protected List parseAllImpl(String formulaStr) throws IllegalArgum ImmutableList.Builder declarationTokens = ImmutableList.builder(); ImmutableList.Builder definitionTokens = ImmutableList.builder(); ImmutableList.Builder assertTokens = ImmutableList.builder(); - for (String token : SMTLibTokenizer.of(formulaStr)) { - if (SMTLibTokenizer.isDeclarationToken(token)) { - declarationTokens.add(token); - } - if (SMTLibTokenizer.isDefinitionToken(token)) { - definitionTokens.add(token); - } - if (SMTLibTokenizer.isAssertToken(token)) { - assertTokens.add(token); + try { + for (String token : SMTLibTokenizer.of(formulaStr)) { + if (SMTLibTokenizer.isDeclarationToken(token)) { + declarationTokens.add(token); + } + if (SMTLibTokenizer.isDefinitionToken(token)) { + definitionTokens.add(token); + } + if (SMTLibTokenizer.isAssertToken(token)) { + assertTokens.add(token); + } } - } - String definitions = - Joiner.on("").join(declarationTokens.build()) - + Joiner.on("").join(definitionTokens.build()); + String definitions = + Joiner.on("").join(declarationTokens.build()) + + Joiner.on("").join(definitionTokens.build()); + + return Collections3.transformedImmutableListCopy( + assertTokens.build(), assertion -> parseImpl(definitions + assertion)); - return Collections3.transformedImmutableListCopy( - assertTokens.build(), assertion -> parseImpl(definitions + assertion)); + } catch (IllegalArgumentException illegalArgumentException) { + throw throwIllegalArgumentExceptionWithBetterErrorMessage(illegalArgumentException); + } } /** @@ -1046,4 +1051,29 @@ void applySetLogicCommand() { } } } + + /** + * Returns the given {@link IllegalArgumentException} with a potentially improved error message. + * For example: the 'as_ieee_bv' and 'to_ieee_bv' operations are not supported by all SMT solvers, + * as the standard does not define those. We add an explanation to error messages containing those + * operations that explain how to build SMTLIB2 conforming and well accepted SMTLIB2. + * + * @param illegalArgumentException original {@link IllegalArgumentException} wrapping a solvers or + * our initial error message from parsing SMTLIB2. + * @return a {@link IllegalArgumentException} that should be thrown in all cases. Might be the + * original exception. + */ + private IllegalArgumentException throwIllegalArgumentExceptionWithBetterErrorMessage( + IllegalArgumentException illegalArgumentException) throws IllegalArgumentException { + final String msg = illegalArgumentException.getMessage(); + if (msg != null && (msg.contains("to_ieee_bv") || msg.contains("as_ieee_bv"))) { + // Better error message for certain cases, explaining common problems + final String additionalMessage = + "; Note: operations 'to_ieee_bv' and 'as_ieee_bv' are not supported in most SMT" + + " solvers. You can try using the SMTLIB2 standards preferred way to encode this" + + " operation by utilizing the 'to_fp' operation."; + return new IllegalArgumentException(msg + additionalMessage, illegalArgumentException); + } + return illegalArgumentException; + } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java index eba79ffb69..26c9228385 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java @@ -165,10 +165,6 @@ protected BitvectorFormula encapsulateBitvector(TFormulaInfo pTerm) { } protected FloatingPointFormula encapsulateFloatingPoint(TFormulaInfo pTerm) { - checkArgument( - getFormulaType(pTerm).isFloatingPointType(), - "Floatingpoint formula has unexpected type: %s", - getFormulaType(pTerm)); return new FloatingPointFormulaImpl<>(pTerm); } 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 50da612173..eac100fc7c 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java @@ -224,6 +224,17 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula number) { return result; } + @Override + public BooleanFormula bitwiseEqual( + FloatingPointFormula floatValue, BitvectorFormula bitvectorValue) { + debugging.assertThreadLocal(); + debugging.assertFormulaInContext(floatValue); + debugging.assertFormulaInContext(bitvectorValue); + BooleanFormula res = delegate.bitwiseEqual(floatValue, bitvectorValue); + debugging.addFormulaTerm(res); + return res; + } + @Override public FloatingPointFormula round( FloatingPointFormula formula, FloatingPointRoundingMode roundingMode) { 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 5f1b58b7aa..f8b46a8119 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java @@ -181,6 +181,13 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula pNumber) { return delegate.toIeeeBitvector(pNumber); } + @Override + public BooleanFormula bitwiseEqual( + FloatingPointFormula floatValue, BitvectorFormula bitvectorValue) { + stats.fpOperations.getAndIncrement(); + return delegate.bitwiseEqual(floatValue, bitvectorValue); + } + @Override public FloatingPointFormula round( FloatingPointFormula pFormula, FloatingPointRoundingMode pRoundingMode) { 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 4dd8354be5..46919a2e63 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java @@ -203,6 +203,14 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula pNumber) { } } + @Override + public BooleanFormula bitwiseEqual( + FloatingPointFormula floatValue, BitvectorFormula bitvectorValue) { + synchronized (sync) { + return delegate.bitwiseEqual(floatValue, bitvectorValue); + } + } + @Override public FloatingPointFormula round( FloatingPointFormula pFormula, FloatingPointRoundingMode pRoundingMode) { diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceFloatingPointFormulaManager.java index c4175d4324..8ea79b7711 100644 --- a/src/org/sosy_lab/java_smt/delegate/trace/TraceFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceFloatingPointFormulaManager.java @@ -244,6 +244,16 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula number) { () -> delegate.toIeeeBitvector(number)); } + @Override + public BooleanFormula bitwiseEqual( + FloatingPointFormula floatValue, BitvectorFormula bitvectorValue) { + return logger.logDef( + "mgr.getFloatingPointFormulaManager()", + "toIeeeBitvector(%s, %s)" + .formatted(logger.toVariable(floatValue), logger.toVariable(bitvectorValue)), + () -> delegate.bitwiseEqual(floatValue, bitvectorValue)); + } + @Override public FloatingPointFormula round( FloatingPointFormula formula, FloatingPointRoundingMode roundingMode) { 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 325b68188d..92bb54cd65 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java @@ -30,8 +30,10 @@ class BitwuzlaFloatingPointManager private final Term roundingMode; BitwuzlaFloatingPointManager( - BitwuzlaFormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode) { - super(pCreator); + BitwuzlaFormulaCreator pCreator, + FloatingPointRoundingMode pFloatingPointRoundingMode, + BitwuzlaBitvectorFormulaManager pBvMgr) { + super(pCreator, pBvMgr); termManager = pCreator.getEnv(); roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode); } 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 2b97d2a98f..1a1838a51d 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -100,8 +100,6 @@ public Sort getArrayType(Sort indexType, Sort elementType) { @Override protected FloatingPointFormula encapsulateFloatingPoint(Term pTerm) { - assert getFormulaType(pTerm).isFloatingPointType() - : "%s is no FP, but %s (%s)".formatted(pTerm, pTerm.sort(), getFormulaType(pTerm)); return new BitwuzlaFloatingPointFormula(pTerm); } 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 99d20c33ad..f50ce47f9b 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java @@ -131,7 +131,7 @@ public static BitwuzlaSolverContext create( BitwuzlaQuantifiedFormulaManager quantifierTheory = new BitwuzlaQuantifiedFormulaManager(creator); BitwuzlaFloatingPointManager floatingPointTheory = - new BitwuzlaFloatingPointManager(creator, pFloatingPointRoundingMode); + new BitwuzlaFloatingPointManager(creator, pFloatingPointRoundingMode, bitvectorTheory); 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 cd242895fe..5942086f5d 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -40,9 +40,11 @@ class CVC4FloatingPointFormulaManager private final ExprManager exprManager; private final Expr roundingMode; - CVC4FloatingPointFormulaManager( - CVC4FormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode) { - super(pCreator); + protected CVC4FloatingPointFormulaManager( + CVC4FormulaCreator pCreator, + FloatingPointRoundingMode pFloatingPointRoundingMode, + CVC4BitvectorFormulaManager pBvFormulaManager) { + super(pCreator, pBvFormulaManager); exprManager = pCreator.getEnv(); roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode); } 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 6fb58c4470..74eac91583 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -230,8 +230,6 @@ assert getFormulaType(pTerm).isBitvectorType() @Override protected FloatingPointFormula encapsulateFloatingPoint(Expr pTerm) { - assert getFormulaType(pTerm).isFloatingPointType() - : "%s is no FP, but %s (%s)".formatted(pTerm, pTerm.getType(), getFormulaType(pTerm)); return new CVC4FloatingPointFormula(pTerm); } 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 4bf383f272..3bbd88d67b 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,8 @@ public static SolverContext create( CVC4FloatingPointFormulaManager fpTheory; if (Configuration.isBuiltWithSymFPU()) { - fpTheory = new CVC4FloatingPointFormulaManager(creator, pFloatingPointRoundingMode); + fpTheory = + new CVC4FloatingPointFormulaManager(creator, pFloatingPointRoundingMode, bitvectorTheory); } 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 74b6ec218b..aa2880b647 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -34,9 +34,11 @@ class CVC5FloatingPointFormulaManager private final Solver solver; private final Term roundingMode; - CVC5FloatingPointFormulaManager( - CVC5FormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode) { - super(pCreator); + protected CVC5FloatingPointFormulaManager( + CVC5FormulaCreator pCreator, + FloatingPointRoundingMode pFloatingPointRoundingMode, + CVC5BitvectorFormulaManager pBvFormulaManager) { + super(pCreator, pBvFormulaManager); termManager = pCreator.getEnv(); solver = pCreator.getSolver(); roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode); 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 659c462b4b..93fbd95b3b 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -322,8 +322,6 @@ assert getFormulaType(pTerm).isBitvectorType() @Override protected FloatingPointFormula encapsulateFloatingPoint(Term pTerm) { - assert getFormulaType(pTerm).isFloatingPointType() - : "%s is no FP, but %s (%s)".formatted(pTerm, pTerm.getSort(), getFormulaType(pTerm)); return new CVC5FloatingPointFormula(pTerm); } 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 e7e1860433..c7d94cf689 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java @@ -158,7 +158,7 @@ public static SolverContext create( CVC5BitvectorFormulaManager bitvectorTheory = new CVC5BitvectorFormulaManager(pCreator, booleanTheory); CVC5FloatingPointFormulaManager fpTheory = - new CVC5FloatingPointFormulaManager(pCreator, pFloatingPointRoundingMode); + new CVC5FloatingPointFormulaManager(pCreator, pFloatingPointRoundingMode, bitvectorTheory); CVC5QuantifiedFormulaManager qfTheory = new CVC5QuantifiedFormulaManager(pCreator, newSolver); CVC5ArrayFormulaManager arrayTheory = new CVC5ArrayFormulaManager(pCreator); CVC5SLFormulaManager slTheory = new CVC5SLFormulaManager(pCreator); 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 9562ce7e9a..dca7fe6c38 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java @@ -61,8 +61,10 @@ class Mathsat5FloatingPointFormulaManager private final long roundingMode; Mathsat5FloatingPointFormulaManager( - Mathsat5FormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode) { - super(pCreator); + Mathsat5FormulaCreator pCreator, + FloatingPointRoundingMode pFloatingPointRoundingMode, + Mathsat5BitvectorFormulaManager pBvFormulaManager) { + super(pCreator, pBvFormulaManager); mathsatEnv = pCreator.getEnv(); roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode); 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 a9bb19b500..4346da3ff3 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -301,7 +301,6 @@ public BitvectorFormula encapsulateBitvector(Long pTerm) { @Override protected FloatingPointFormula encapsulateFloatingPoint(Long pTerm) { - assert getFormulaType(pTerm).isFloatingPointType(); return new Mathsat5FloatingPointFormula(pTerm); } 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 14ff32556d..a498993564 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java @@ -212,7 +212,8 @@ public static Mathsat5SolverContext create( Mathsat5BitvectorFormulaManager bitvectorTheory = new Mathsat5BitvectorFormulaManager(creator, booleanTheory); Mathsat5FloatingPointFormulaManager floatingPointTheory = - new Mathsat5FloatingPointFormulaManager(creator, pFloatingPointRoundingMode); + new Mathsat5FloatingPointFormulaManager( + creator, pFloatingPointRoundingMode, bitvectorTheory); Mathsat5ArrayFormulaManager arrayTheory = new Mathsat5ArrayFormulaManager(creator); Mathsat5EnumerationFormulaManager enumerationTheory = null; if (!settings.loadOptimathsat5) { 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 845096ae3c..d46231e2aa 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java @@ -29,8 +29,10 @@ class Z3FloatingPointFormulaManager private final long roundingMode; Z3FloatingPointFormulaManager( - Z3FormulaCreator creator, FloatingPointRoundingMode pFloatingPointRoundingMode) { - super(creator); + Z3FormulaCreator creator, + FloatingPointRoundingMode pFloatingPointRoundingMode, + Z3BitvectorFormulaManager pBvFormulaManager) { + super(creator, pBvFormulaManager); z3context = creator.getEnv(); roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode); } 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 ed679a6597..e73f6f3e0a 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -357,7 +357,6 @@ public BitvectorFormula encapsulateBitvector(Long pTerm) { @Override protected FloatingPointFormula encapsulateFloatingPoint(Long pTerm) { - assert getFormulaType(pTerm).isFloatingPointType(); cleanupReferences(); return storePhantomReference(new Z3FloatingPointFormula(getEnv(), pTerm), pTerm); } 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 f36d9e5643..1111abdb71 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java @@ -334,7 +334,7 @@ public static synchronized Z3SolverContext create( Z3BitvectorFormulaManager bitvectorTheory = new Z3BitvectorFormulaManager(creator, booleanTheory); Z3FloatingPointFormulaManager floatingPointTheory = - new Z3FloatingPointFormulaManager(creator, pFloatingPointRoundingMode); + new Z3FloatingPointFormulaManager(creator, pFloatingPointRoundingMode, bitvectorTheory); Z3QuantifiedFormulaManager quantifierManager = new Z3QuantifiedFormulaManager(creator); Z3ArrayFormulaManager arrayManager = new Z3ArrayFormulaManager(creator); Z3StringFormulaManager stringTheory = new Z3StringFormulaManager(creator); diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFloatingPointFormulaManager.java index 348557244a..25773ad3e1 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFloatingPointFormulaManager.java @@ -29,8 +29,10 @@ class Z3LegacyFloatingPointFormulaManager private final long roundingMode; Z3LegacyFloatingPointFormulaManager( - Z3LegacyFormulaCreator creator, FloatingPointRoundingMode pFloatingPointRoundingMode) { - super(creator); + Z3LegacyFormulaCreator creator, + Z3LegacyBitvectorFormulaManager bvMgr, + FloatingPointRoundingMode pFloatingPointRoundingMode) { + super(creator, bvMgr); z3context = creator.getEnv(); roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode); } diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java index 50753cc294..95ed4e3aae 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java @@ -363,7 +363,6 @@ public BitvectorFormula encapsulateBitvector(Long pTerm) { @Override protected FloatingPointFormula encapsulateFloatingPoint(Long pTerm) { - assert getFormulaType(pTerm).isFloatingPointType(); cleanupReferences(); return storePhantomReference(new Z3FloatingPointLegacyFormula(getEnv(), pTerm), pTerm); } diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacySolverContext.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacySolverContext.java index d61ccae983..c4086ef0b8 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacySolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacySolverContext.java @@ -176,7 +176,8 @@ public static synchronized Z3LegacySolverContext create( Z3LegacyBitvectorFormulaManager bitvectorTheory = new Z3LegacyBitvectorFormulaManager(creator, booleanTheory); Z3LegacyFloatingPointFormulaManager floatingPointTheory = - new Z3LegacyFloatingPointFormulaManager(creator, pFloatingPointRoundingMode); + new Z3LegacyFloatingPointFormulaManager( + creator, bitvectorTheory, pFloatingPointRoundingMode); Z3LegacyQuantifiedFormulaManager quantifierManager = new Z3LegacyQuantifiedFormulaManager(creator); Z3LegacyArrayFormulaManager arrayManager = new Z3LegacyArrayFormulaManager(creator); diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index bce77f9d2e..44a8f89b8d 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -17,12 +17,15 @@ 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; import java.math.BigInteger; import java.util.List; +import java.util.Map.Entry; import java.util.Random; +import java.util.Set; import java.util.function.Function; import org.junit.Before; import org.junit.Test; @@ -57,6 +60,28 @@ public class FloatingPointFormulaManagerTest // numbers are small enough to be precise with single precision private static final int[] SINGLE_PREC_INTS = new int[] {0, 1, 2, 5, 10, 20, 50, 100, 200, 500}; + // Multiple distinct NaN numbers (not all, just some common ones) as defined in IEEE 754-2008 as + // 32 bit bitvectors for single-precision floating-point numbers. All bitvectors are defined as + // IEEE 754 (sign bit + exponent bits + mantissa bits (without hidden bit)) + private static final Set SINGLE_PRECISION_NANS_BITWISE = + ImmutableSet.of( + "01111111110000000000000000000000", + "11111111110000000000000000000000", + "01111111100000000000000000000001", + "11111111100000000000000000000001", + "01111111111111111111111111111111", + "11111111111111111111111111111111", + "01111111100000000000000000001100"); + // Other special FP values (single precision, defined as above) + private static final String SINGLE_PRECISION_POSITIVE_INFINITY_BITWISE = + "01111111100000000000000000000000"; + private static final String SINGLE_PRECISION_NEGATIVE_INFINITY_BITWISE = + "11111111100000000000000000000000"; + private static final String SINGLE_PRECISION_POSITIVE_ZERO_BITWISE = + "00000000000000000000000000000000"; + private static final String SINGLE_PRECISION_NEGATIVE_ZERO_BITWISE = + "10000000000000000000000000000000"; + private static final int NUM_RANDOM_TESTS = 50; private FloatingPointType singlePrecType; @@ -82,6 +107,32 @@ 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 = getFloatingPointTypeFromSizesWithoutHiddenBit(23, 42); @@ -527,7 +578,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); @@ -572,7 +623,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); @@ -618,6 +669,476 @@ 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 fpX = fpmgr.makeVariable("x32", singlePrecType); + final BitvectorFormula bvX = bvmgr.makeVariable(singlePrecType.getTotalSize(), "bvConst_x"); + BooleanFormula fpXToBvConstraint = fpmgr.bitwiseEqual(fpX, bvX); + + final BitvectorFormula signBit = bvmgr.extract(bvX, 31, 31); + final BitvectorFormula exponent = bvmgr.extract(bvX, 30, 23); + final BitvectorFormula mantissa = bvmgr.extract(bvX, 22, 0); + + assertThatFormula( + bmgr.implication( + fpXToBvConstraint, + bmgr.equivalence( + fpmgr.isInfinity(fpX), + bmgr.or( + bvmgr.equal(bvX, bvmgr.makeBitvector(32, 0x7f80_0000L)), + bvmgr.equal(bvX, bvmgr.makeBitvector(32, 0xff80_0000L)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + fpXToBvConstraint, + bmgr.equivalence( + fpmgr.isZero(fpX), + bmgr.or( + bvmgr.equal(bvX, bvmgr.makeBitvector(32, 0x0000_0000)), + bvmgr.equal(bvX, bvmgr.makeBitvector(32, 0x8000_0000L)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + fpXToBvConstraint, + bmgr.equivalence( + fpmgr.isNormal(fpX), + bmgr.and( + bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0))), + bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1))))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + fpXToBvConstraint, + bmgr.equivalence( + fpmgr.isSubnormal(fpX), + bmgr.and( + bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0)), + bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0))))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + fpXToBvConstraint, + bmgr.equivalence( + fpmgr.isNaN(fpX), + bmgr.and( + bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1)), + bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0))))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + fpXToBvConstraint, + bmgr.equivalence( + fpmgr.isNegative(fpX), + bmgr.and( + bmgr.not(fpmgr.isNaN(fpX)), + 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); + final BitvectorFormula xToIeeeBv = + bvmgr.makeVariable(doublePrecType.getTotalSize(), "bvConst_x"); + BooleanFormula xToIeeeConstraint = fpmgr.bitwiseEqual(x, xToIeeeBv); + + final BitvectorFormula signBit = bvmgr.extract(xToIeeeBv, 63, 63); + final BitvectorFormula exponent = bvmgr.extract(xToIeeeBv, 62, 52); + final BitvectorFormula mantissa = bvmgr.extract(xToIeeeBv, 51, 0); + + assertThatFormula( + bmgr.implication( + xToIeeeConstraint, + bmgr.equivalence( + fpmgr.isInfinity(x), + bmgr.or( + bvmgr.equal(xToIeeeBv, bvmgr.makeBitvector(64, 0x7ff0_0000_0000_0000L)), + bvmgr.equal(xToIeeeBv, bvmgr.makeBitvector(64, 0xfff0_0000_0000_0000L)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + xToIeeeConstraint, + bmgr.equivalence( + fpmgr.isZero(x), + bmgr.or( + bvmgr.equal(xToIeeeBv, bvmgr.makeBitvector(64, 0x0000_0000_0000_0000L)), + bvmgr.equal(xToIeeeBv, bvmgr.makeBitvector(64, 0x8000_0000_0000_0000L)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + xToIeeeConstraint, + 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( + xToIeeeConstraint, + 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( + xToIeeeConstraint, + 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( + xToIeeeConstraint, + bmgr.equivalence( + fpmgr.isNegative(x), + bmgr.and( + bmgr.not(fpmgr.isNaN(x)), + bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1)))))) + .isTautological(); + } + + // Tests +-0 and +-Infinity from BV -> FP and that the FP model values are == to the original BV + @Test + public void floatingPointSpecialNumberFromBitvector32() + throws SolverException, InterruptedException { + + ImmutableMap fpSpecialNumBvsAndNames = + ImmutableMap.of( + SINGLE_PRECISION_POSITIVE_ZERO_BITWISE, + "+0.0", + SINGLE_PRECISION_NEGATIVE_ZERO_BITWISE, + "-0.0", + SINGLE_PRECISION_POSITIVE_INFINITY_BITWISE, + "+Infinity", + SINGLE_PRECISION_NEGATIVE_INFINITY_BITWISE, + "-Infinity"); + + for (Entry fpSpecialNumBvAndName : fpSpecialNumBvsAndNames.entrySet()) { + String specialFpNumAsBv = fpSpecialNumBvAndName.getKey(); + String stringRepresentation = fpSpecialNumBvAndName.getValue(); + + final BitvectorFormula bv = + bvmgr.makeBitvector( + singlePrecType.getTotalSize(), BigInteger.valueOf(Long.valueOf(specialFpNumAsBv, 2))); + final FloatingPointFormula fpFromBv = fpmgr.makeVariable("fpFromBv", singlePrecType); + final FloatingPointFormula someFP = fpmgr.makeVariable("someFPNumber", singlePrecType); + // toIeeeBitvector(FloatingPointFormula, BitvectorFormula) is built from fromIeeeBitvector()! + BooleanFormula bvToIeeeFPConstraint = fpmgr.bitwiseEqual(fpFromBv, bv); + + BooleanFormula fpFromBvIsNotNan = bmgr.not(fpmgr.isNaN(fpFromBv)); + assertThatFormula(bmgr.implication(bvToIeeeFPConstraint, fpFromBvIsNotNan)).isTautological(); + + BooleanFormula fpFromBvIsNotEqualNaN = + bmgr.not(fpmgr.equalWithFPSemantics(fpmgr.makeNaN(singlePrecType), fpFromBv)); + assertThatFormula(bmgr.implication(bvToIeeeFPConstraint, fpFromBvIsNotEqualNaN)) + .isTautological(); + + BooleanFormula fpFromBvIsEqualItself = fpmgr.equalWithFPSemantics(fpFromBv, fpFromBv); + assertThatFormula(bmgr.implication(bvToIeeeFPConstraint, fpFromBvIsEqualItself)) + .isTautological(); + + if (stringRepresentation.contains("0")) { + assertThatFormula(bmgr.implication(bvToIeeeFPConstraint, fpmgr.isZero(fpFromBv))) + .isTautological(); + } else { + assertThatFormula(bmgr.implication(bvToIeeeFPConstraint, fpmgr.isInfinity(fpFromBv))) + .isTautological(); + } + + for (String specialFpNum : ImmutableSet.of("+0.0", "-0.0", "+Infinity", "-Infinity")) { + BooleanFormula fpFromBvIsEqualSpecialNum = + fpmgr.equalWithFPSemantics(fpmgr.makeNumber(specialFpNum, singlePrecType), fpFromBv); + if (stringRepresentation.contains("0") && specialFpNum.contains("0")) { + // All zero equality is always true (i.e. they ignore the sign bit) + assertThatFormula(bmgr.implication(bvToIeeeFPConstraint, fpFromBvIsEqualSpecialNum)) + .isTautological(); + } else if (stringRepresentation.equals(specialFpNum)) { + // Infinity equality takes the sign bit into account + assertThatFormula(bmgr.implication(bvToIeeeFPConstraint, fpFromBvIsEqualSpecialNum)) + .isTautological(); + } else { + assertThatFormula(bmgr.and(bvToIeeeFPConstraint, fpFromBvIsEqualSpecialNum)) + .isUnsatisfiable(); + } + } + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + prover.push(bvToIeeeFPConstraint); // has to be true! + prover.push(fpmgr.equalWithFPSemantics(someFP, fpFromBv)); + assertThat(prover).isSatisfiable(); + + try (Model model = prover.getModel()) { + FloatingPointNumber fpValue = model.evaluate(someFP); + String fpAsString = fpValue.toString(); + + // 0.0 and -0.0 are equal for FP equality, hence a solver might return any + switch (solver) { + case Z3, Z3_WITH_INTERPOLATION -> { + if (specialFpNumAsBv.equals(SINGLE_PRECISION_POSITIVE_ZERO_BITWISE)) { + assertThat(fpAsString).isEqualTo(SINGLE_PRECISION_NEGATIVE_ZERO_BITWISE); + } else if (specialFpNumAsBv.equals(SINGLE_PRECISION_NEGATIVE_ZERO_BITWISE)) { + assertThat(fpAsString).isEqualTo(SINGLE_PRECISION_POSITIVE_ZERO_BITWISE); + } else { + assertThat(fpAsString).isEqualTo(specialFpNumAsBv); + } + } + case MATHSAT5 -> { + if (specialFpNumAsBv.equals(SINGLE_PRECISION_NEGATIVE_ZERO_BITWISE)) { + assertThat(fpAsString).isEqualTo(SINGLE_PRECISION_POSITIVE_ZERO_BITWISE); + } else { + assertThat(fpAsString).isEqualTo(specialFpNumAsBv); + } + } + case BITWUZLA, CVC4, CVC5, BOOLECTOR, PRINCESS, OPENSMT, SMTINTERPOL, YICES2 -> + assertThat(fpAsString).isEqualTo(specialFpNumAsBv); + } + } + } + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + prover.push(bvToIeeeFPConstraint); // has to be true! + prover.push(fpmgr.assignment(someFP, fpFromBv)); + assertThat(prover).isSatisfiable(); + + // If we use assignment instead of FP equality, the result needs to be 1:1 + try (Model model = prover.getModel()) { + FloatingPointNumber fpValue = model.evaluate(someFP); + assertThat(fpValue.toString()).isEqualTo(specialFpNumAsBv); + } + } + } + } + + // Test that multiple FP NaNs built from bitvectors compare to NaN in SMT FP theory and their + // values and that a solver always just returns a single NaN bitwise representation per default + @Test + public void toIeeeBitvectorFallbackEqualityWithDistinctNaN32() + throws SolverException, InterruptedException { + requireBitvectors(); + + // Solvers transform arbitrary input NaNs into a single NaN representation + String defaultNaN = null; + + for (String nanString : SINGLE_PRECISION_NANS_BITWISE) { + final BitvectorFormula bvNaN = + bvmgr.makeBitvector( + singlePrecType.getTotalSize(), BigInteger.valueOf(Long.valueOf(nanString, 2))); + final FloatingPointFormula fpFromBv = fpmgr.makeVariable("bvNaN", singlePrecType); + // toIeeeBitvector(FloatingPointFormula, BitvectorFormula) is built from fromIeeeBitvector() + BooleanFormula xToIeeeConstraint = fpmgr.bitwiseEqual(fpFromBv, bvNaN); + + BooleanFormula fpFromBvIsNan = fpmgr.isNaN(fpFromBv); + BooleanFormula fpFromBvIsNotEqualNaN = + bmgr.not(fpmgr.equalWithFPSemantics(fpmgr.makeNaN(singlePrecType), fpFromBv)); + BooleanFormula fpFromBvIsNotEqualItself = + bmgr.not(fpmgr.equalWithFPSemantics(fpFromBv, fpFromBv)); + BooleanFormula assertion = + bmgr.implication( + xToIeeeConstraint, + bmgr.and(fpFromBvIsNan, fpFromBvIsNotEqualNaN, fpFromBvIsNotEqualItself)); + + assertThatFormula(assertion).isTautological(); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + prover.push(xToIeeeConstraint); // xToIeeeConstraint has to be true! + prover.push(assertion); + assertThat(prover).isSatisfiable(); + + try (Model model = prover.getModel()) { + BigInteger bvAsBigInt = model.evaluate(bvNaN); + // toBinaryString() is not returning the sign bit if its 0, so we need to add it + String bvAsBvString = Long.toBinaryString(model.evaluate(bvNaN).longValueExact()); + if (bvAsBvString.length() != singlePrecType.getTotalSize()) { + if (bvAsBigInt.signum() >= 0) { + bvAsBvString = "0" + bvAsBvString; + } + } + + // The used bitvector is really a (known) NaN + assertThat(bvAsBvString).isIn(SINGLE_PRECISION_NANS_BITWISE); + + FloatingPointNumber fpNanValue = model.evaluate(fpFromBv); + // The FP is also a (known) NaN + String fpNanAsString = fpNanValue.toString(); + assertThat(fpNanAsString).isIn(SINGLE_PRECISION_NANS_BITWISE); + if (defaultNaN == null) { + defaultNaN = fpNanAsString; + } else { + assertThat(fpNanAsString).isEqualTo(defaultNaN); + } + } + } + } + } + + @Test + public void toIeeeBitvectorFallbackEqualityWithNaN32() + throws SolverException, InterruptedException { + requireBitvectors(); + + for (String nanString : SINGLE_PRECISION_NANS_BITWISE) { + final BitvectorFormula bvNaN = + bvmgr.makeBitvector( + singlePrecType.getTotalSize(), BigInteger.valueOf(Long.valueOf(nanString, 2))); + final FloatingPointFormula fpFromBv = fpmgr.makeVariable("fp_from_bv", singlePrecType); + BooleanFormula xToIeeeConstraint = fpmgr.bitwiseEqual(fpFromBv, bvNaN); + + BooleanFormula fpFromBvIsEqualNaN = + fpmgr.equalWithFPSemantics(fpmgr.makeNaN(singlePrecType), fpFromBv); + BooleanFormula fpFromBvIsEqualItself = fpmgr.equalWithFPSemantics(fpFromBv, fpFromBv); + + assertThatFormula(bmgr.implication(xToIeeeConstraint, bmgr.not(fpFromBvIsEqualNaN))) + .isTautological(); + assertThatFormula(bmgr.implication(xToIeeeConstraint, bmgr.not(fpFromBvIsEqualItself))) + .isTautological(); + } + } + + @Test + public void fromIeeeBitvectorEqualityWithNaN32() throws SolverException, InterruptedException { + requireBitvectors(); + + for (String nanString : SINGLE_PRECISION_NANS_BITWISE) { + final BitvectorFormula bvNaN = + bvmgr.makeBitvector( + singlePrecType.getTotalSize(), BigInteger.valueOf(Long.valueOf(nanString, 2))); + final FloatingPointFormula fpFromBv = fpmgr.fromIeeeBitvector(bvNaN, singlePrecType); + + BooleanFormula fpFromBvIsEqualNaN = + fpmgr.equalWithFPSemantics(fpmgr.makeNaN(singlePrecType), fpFromBv); + BooleanFormula fpFromBvIsEqualItself = fpmgr.equalWithFPSemantics(fpFromBv, fpFromBv); + + assertThatFormula(bmgr.not(fpFromBvIsEqualNaN)).isTautological(); + assertThatFormula(bmgr.not(fpFromBvIsEqualItself)).isTautological(); + } + } + + // Tests FP NaN to bitvector representations + @Test + public void toIeeeBitvectorNaNRepresentation32() throws SolverException, InterruptedException { + requireBitvectors(); + + final BitvectorFormula bvNaN = bvmgr.makeVariable(singlePrecType.getTotalSize(), "bvNaN"); + + final FloatingPointFormula fpNan = fpmgr.makeNaN(singlePrecType); + BooleanFormula xToIeeeConstraint = fpmgr.bitwiseEqual(fpNan, bvNaN); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + prover.push(xToIeeeConstraint); + assertThat(prover).isSatisfiable(); + + try (Model model = prover.getModel()) { + BigInteger bvNaNAsBigInt = model.evaluate(bvNaN); + // toBinaryString() is not returning the sign bit if its 0, so we need to add it + String bvAsBvString = Long.toBinaryString(model.evaluate(bvNaN).longValueExact()); + if (bvAsBvString.length() != singlePrecType.getTotalSize()) { + if (bvNaNAsBigInt.signum() >= 0) { + bvAsBvString = "0" + bvAsBvString; + } + } + + // The bitvector is really a (known) NaN + assertThat(bvAsBvString).isIn(SINGLE_PRECISION_NANS_BITWISE); + + FloatingPointNumber fpNanValue = model.evaluate(fpNan); + // The FP is also a (known) NaN + String fpNanAsString = fpNanValue.toString(); + assertThat(fpNanAsString).isIn(SINGLE_PRECISION_NANS_BITWISE); + + // No solver uses the same bit representation for NaN in the FP number and bitvector + assertThat(fpNanAsString).isNotEqualTo(bvAsBvString); + } + } + } + + // Tests toIeeeBitvector() fallback == toIeeeBitvector() solver native for special numbers, + // some example numbers, and a variable for single FP precision type + @Test + public void floatingPointSinglePrecToIeeeBitvectorFallbackCompareWithNativeTest() + throws SolverException, InterruptedException { + requireBitvectors(); + requireNativeFPToBitvector(); + + FloatingPointType fpType = singlePrecType; + FloatingPointFormula varSingle = fpmgr.makeVariable("varSingle", fpType); + Set testSetOfFps = + ImmutableSet.of(nan, posInf, negInf, zero, negZero, one, varSingle); + + int fpTypeSize = fpType.getTotalSize(); + int i = 0; + for (FloatingPointFormula fpToTest : testSetOfFps) { + BitvectorFormula fallbackBv = bvmgr.makeVariable(fpTypeSize, "bv" + i++); + assertThat(bvmgr.getLength(fallbackBv)).isEqualTo(fpTypeSize); + BooleanFormula fpEqFallbackBv = fpmgr.bitwiseEqual(fpToTest, fallbackBv); + + BitvectorFormula nativeBv = fpmgr.toIeeeBitvector(fpToTest); + assertThat(bvmgr.getLength(nativeBv)).isEqualTo(fpTypeSize); + + BooleanFormula constraints = bmgr.and(fpEqFallbackBv, bvmgr.equal(nativeBv, fallbackBv)); + + assertThatFormula(constraints).isSatisfiable(); + } + } + + // Tests toIeeeBitvector() fallback == toIeeeBitvector() solver native for special numbers, + // some example numbers, and a variable for double FP precision type + @Test + public void floatingPointDoublePrecToIeeeBitvectorFallbackCompareWithNativeTest() + throws SolverException, InterruptedException { + requireBitvectors(); + requireNativeFPToBitvector(); + + FloatingPointType fpType = doublePrecType; + FloatingPointFormula varDouble = fpmgr.makeVariable("varDouble", fpType); + Set testSetOfFps = + ImmutableSet.of( + fpmgr.makeNaN(fpType), + fpmgr.makePlusInfinity(fpType), + fpmgr.makeMinusInfinity(fpType), + fpmgr.makeNumber(0.0, fpType), + fpmgr.makeNumber(-0.0, fpType), + fpmgr.makeNumber(1.0, fpType), + varDouble); + + int fpTypeSize = fpType.getTotalSize(); + int i = 0; + for (FloatingPointFormula fpToTest : testSetOfFps) { + BitvectorFormula fallbackBv = bvmgr.makeVariable(fpTypeSize, "bv" + i++); + assertThat(bvmgr.getLength(fallbackBv)).isEqualTo(fpTypeSize); + BooleanFormula fpEqFallbackBv = fpmgr.bitwiseEqual(fpToTest, fallbackBv); + + BitvectorFormula nativeBv = fpmgr.toIeeeBitvector(fpToTest); + assertThat(bvmgr.getLength(nativeBv)).isEqualTo(fpTypeSize); + + BooleanFormula constraints = bmgr.and(fpEqFallbackBv, bvmgr.equal(nativeBv, fallbackBv)); + + assertThatFormula(constraints).isSatisfiable(); + } + } + @Test public void specialDoubles() throws SolverException, InterruptedException { assertThatFormula(fpmgr.assignment(fpmgr.makeNumber(Double.NaN, singlePrecType), nan)) @@ -1089,7 +1610,7 @@ public void fpTraversalWithRoundingMode() { @Test public void fpIeeeConversionTypes() { - requireFPToBitvector(); + requireNativeFPToBitvector(); FloatingPointFormula var = fpmgr.makeVariable("var", singlePrecType); assertThat(mgr.getFormulaType(fpmgr.toIeeeBitvector(var))) @@ -1098,7 +1619,7 @@ public void fpIeeeConversionTypes() { @Test public void fpIeeeConversion() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); FloatingPointFormula var = fpmgr.makeVariable("var", singlePrecType); assertThatFormula( @@ -1109,7 +1630,7 @@ public void fpIeeeConversion() throws SolverException, InterruptedException { @Test public void ieeeFpConversion() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); BitvectorFormula var = bvmgr.makeBitvector(32, 123456789); assertThatFormula( @@ -1200,7 +1721,7 @@ public void checkIeeeBv2FpConversion64() throws SolverException, InterruptedExce @Test public void checkIeeeFp2BvConversion32() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); proveForAll( // makeBV(value.bits) == fromFP(makeFP(value.float)) @@ -1213,7 +1734,7 @@ public void checkIeeeFp2BvConversion32() throws SolverException, InterruptedExce @Test public void checkIeeeFp2BvConversion64() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); proveForAll( // makeBV(value.bits) == fromFP(makeFP(value.float)) @@ -1224,6 +1745,40 @@ public void checkIeeeFp2BvConversion64() throws SolverException, InterruptedExce fpmgr.toIeeeBitvector(fpmgr.makeNumber(pDouble, doublePrecType)))); } + // Equal to checkIeeeFp2BvConversion32, but with the fallback method of toIeeeBitvector() + @Test + public void checkIeeeFp2BvConversion32WithFallback() + throws SolverException, InterruptedException { + requireBitvectors(); + + proveForAll( + // makeBV(value.bits) == fromFP(makeFP(value.float)) + getListOfFloats(), + pFloat -> { + var bv = bvmgr.makeVariable(32, "bv"); + return bmgr.implication( + fpmgr.bitwiseEqual(fpmgr.makeNumber(pFloat, singlePrecType), bv), + bvmgr.equal(bvmgr.makeBitvector(32, Float.floatToRawIntBits(pFloat)), bv)); + }); + } + + // Equal to checkIeeeFp2BvConversion64, but with the fallback method of toIeeeBitvector() + @Test + public void checkIeeeFp2BvConversion64WithFallback() + throws SolverException, InterruptedException { + requireBitvectors(); + + proveForAll( + // makeBV(value.bits) == fromFP(makeFP(value.float)) + getListOfFloats(), + pDouble -> { + var bv = bvmgr.makeVariable(64, "bv"); + return bmgr.implication( + fpmgr.bitwiseEqual(fpmgr.makeNumber(pDouble, doublePrecType), bv), + bvmgr.equal(bvmgr.makeBitvector(64, Double.doubleToRawLongBits(pDouble)), bv)); + }); + } + private List getListOfFloats() { List flts = Lists.newArrayList( @@ -1455,7 +2010,7 @@ public void bitvectorToFloatingPointMantissaSignBitInterpretationSinglePrecision @Test public void floatingPointMantissaSignBitWithBitvectorInterpretationSinglePrecision() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); int bvSize32 = singlePrecType.getTotalSize(); BitvectorFormula bvNumber32 = bvmgr.makeBitvector(bvSize32, BigInteger.ZERO); @@ -1568,7 +2123,7 @@ public void bitvectorToFloatingPointMantissaSignBitInterpretationDoublePrecision @Test public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecision() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); int bvSize64 = doublePrecType.getTotalSize(); BitvectorFormula bvNumberSize64 = bvmgr.makeBitvector(bvSize64, BigInteger.ZERO); @@ -1637,6 +2192,31 @@ public void failOnInvalidString() { assertThrows(Exception.class, () -> fpmgr.makeNumber("a", singlePrecType)); } + @Test + public void failOnInvalidBvSizeInToIeeeFallback() { + FloatingPointType fpType = singlePrecType; + assertThrows( + IllegalArgumentException.class, + () -> + fpmgr.bitwiseEqual( + fpmgr.makeVariable("someName1", fpType), + bvmgr.makeVariable(fpType.getTotalSize() + 1, "someBv1"))); + assertThrows( + IllegalArgumentException.class, + () -> + fpmgr.bitwiseEqual( + fpmgr.makeVariable("someName2", fpType), + bvmgr.makeVariable(fpType.getTotalSize() - 1, "someBv2"))); + assertThrows( + IllegalArgumentException.class, + () -> + fpmgr.bitwiseEqual( + fpmgr.makeVariable("someName3", fpType), + bvmgr.makeVariable( + fpType.getExponentSize() + fpType.getMantissaSizeWithoutHiddenBit(), + "someBv3"))); + } + @Test public void fpFrom32BitPattern() throws SolverException, InterruptedException { proveForAll( diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index 509a7ea587..95f5ba0f01 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -366,13 +366,19 @@ protected final void requireBitvectorToInt() { } @SuppressWarnings("CheckReturnValue") - protected final void requireFPToBitvector() { + final void requireNativeFPToBitvector() { requireFloats(); + var someFP = fpmgr.makeNumber(0, getSinglePrecisionFloatingPointType()); try { - fpmgr.toIeeeBitvector(fpmgr.makeNumber(0, getSinglePrecisionFloatingPointType())); + fpmgr.toIeeeBitvector(someFP); } 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(); } diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java index 9f7ff57557..2c34ecd8de 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java @@ -12,6 +12,8 @@ import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.Truth.assertWithMessage; import static com.google.common.truth.TruthJUnit.assume; +import static org.junit.Assert.assertThrows; +import static org.sosy_lab.java_smt.api.FormulaType.getSinglePrecisionFloatingPointType; import com.google.common.base.Splitter; import com.google.common.collect.HashMultimap; @@ -27,7 +29,9 @@ import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.FloatingPointFormula; import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; import org.sosy_lab.java_smt.api.FunctionDeclaration; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.SolverException; @@ -121,6 +125,22 @@ public class SolverFormulaIOTest extends SolverBasedTest0.ParameterizedSolverBas (assert (let (($x35 (and (xor q (= (+ a b) c)) (>= a b)))) (let (($x9 (= a b))) (and (and (or $x35 u) q) (and $x9 $x35)))))\ """; + private static final String TO_IEEE_BV_DUMP_Z3 = + """ + (declare-fun someOtherBv () (_ BitVec 32)) + (declare-fun fpVar () (_ FloatingPoint 8 24)) + (assert (= (fp.to_ieee_bv fpVar) someOtherBv))\ + """; + + private static final String TO_IEEE_BV_DUMP_MATHSAT5 = + """ + (declare-fun fpVar () (_ FloatingPoint 8 24)) + (declare-fun someOtherBv () (_ BitVec 32)) + (assert (let ((.def_12 (fp.as_ieee_bv fpVar))) + (let ((.def_13 (= someOtherBv .def_12))) + .def_13)))\ + """; + private static final Collection ABDE = ImmutableSet.of("a", "b", "d", "e"); private static final Collection AQBCU = ImmutableSet.of("a", "q", "b", "c", "u"); private static final Collection QBCU = ImmutableSet.of("q", "b", "c", "u"); @@ -173,7 +193,7 @@ public void varDumpTest() { checkVariableIsDeclared(formDump, "|main::a|", "Bool"); checkVariableIsDeclared(formDump, "b", "Bool"); checkThatAssertIsInLastLine(formDump); - checkThatDumpIsParseable(formDump); + checkThatDumpIsParseableWithCurrentSolver(formDump); } @Test @@ -191,7 +211,7 @@ public void varWithSpaceDumpTest() { checkVariableIsDeclared(formDump, "|main a|", "Bool"); checkVariableIsDeclared(formDump, "b", "Bool"); checkThatAssertIsInLastLine(formDump); - checkThatDumpIsParseable(formDump); + checkThatDumpIsParseableWithCurrentSolver(formDump); } @Test @@ -223,7 +243,7 @@ public void varDumpTest2() { checkVariableIsDeclared(formDump, "b", "Bool"); // The serialization has to be parse-able. - checkThatDumpIsParseable(formDump); + checkThatDumpIsParseableWithCurrentSolver(formDump); } @Test @@ -242,7 +262,7 @@ public void valDumpTest() { String formDump = mgr.dumpFormula(valComp5).toString(); checkThatAssertIsInLastLine(formDump); - checkThatDumpIsParseable(formDump); + checkThatDumpIsParseableWithCurrentSolver(formDump); } @Test @@ -257,7 +277,7 @@ public void intsDumpTest() { // check that int variable is declared correctly + necessary assert that has to be there assertThat(formDump).contains("(declare-fun a () Int)"); checkThatAssertIsInLastLine(formDump); - checkThatDumpIsParseable(formDump); + checkThatDumpIsParseableWithCurrentSolver(formDump); } @Test @@ -273,7 +293,7 @@ public void bvDumpTest() { // check that int variable is declared correctly + necessary assert that has to be there checkVariableIsDeclared(formDump, "a", "(_ BitVec 8)"); checkThatAssertIsInLastLine(formDump); - checkThatDumpIsParseable(formDump); + checkThatDumpIsParseableWithCurrentSolver(formDump); } @Test @@ -292,7 +312,7 @@ public void funcsDumpTest() { // check that function is dumped correctly + necessary assert that has to be there assertThat(formDump).contains("(declare-fun fun_a (Int Int) Int)"); checkThatAssertIsInLastLine(formDump); - checkThatDumpIsParseable(formDump); + checkThatDumpIsParseableWithCurrentSolver(formDump); } @Test @@ -421,7 +441,7 @@ public void funDeclareTest() { // check if dumped formula fits our specification checkThatFunOnlyDeclaredOnce(formDump, ImmutableSet.of("fun_a", "fun_b")); checkThatAssertIsInLastLine(formDump); - checkThatDumpIsParseable(formDump); + checkThatDumpIsParseableWithCurrentSolver(formDump); } @Test @@ -441,7 +461,7 @@ public void funDeclareTest2() { // check if dumped formula fits our specification checkThatFunOnlyDeclaredOnce(formDump, ImmutableSet.of("fun_a")); checkThatAssertIsInLastLine(formDump); - checkThatDumpIsParseable(formDump); + checkThatDumpIsParseableWithCurrentSolver(formDump); } @Test @@ -464,7 +484,110 @@ public void funDeclareWithArrayTest() { // check if dumped formula fits our specification checkThatFunOnlyDeclaredOnce(formDump, ImmutableSet.of("idx", "arr")); checkThatAssertIsInLastLine(formDump); - checkThatDumpIsParseable(formDump); + checkThatDumpIsParseableWithCurrentSolver(formDump); + } + + // Tests that the output of the SMTLIB2 dump of the 2 versions of toIeeeBitvector() are + // distinct and that the correct SMTLIB2 keywords are used + @Test + public void floatingPointToIeeeBvSMTLIB2DumpTest() { + requireFloats(); + requireBitvectors(); + + FloatingPointType fpType = getSinglePrecisionFloatingPointType(); + FloatingPointFormula fp = fpmgr.makeVariable("fp", fpType); + BitvectorFormula someOtherBv = bvmgr.makeVariable(fpType.getTotalSize(), "someOtherBv"); + BitvectorFormula bvFromFpFallback = + bvmgr.makeVariable(fpType.getTotalSize(), "bvFromFpFallback"); + BooleanFormula fpToBvFallbackConstraint = fpmgr.bitwiseEqual(fp, bvFromFpFallback); + + String fallbackDump = + mgr.dumpFormula( + bmgr.and(fpToBvFallbackConstraint, bvmgr.equal(bvFromFpFallback, someOtherBv))) + .toString(); + assertThat(fallbackDump).contains("((_ to_fp 8 24) bvFromFpFallback)"); + assertThat(fallbackDump).doesNotContain("to_ieee_bv"); + + requireNativeFPToBitvector(); + BitvectorFormula bvFromFpNative = fpmgr.toIeeeBitvector(fp); + + String nativeDump = mgr.dumpFormula(bvmgr.equal(bvFromFpNative, someOtherBv)).toString(); + if (solverToUse() == Solvers.MATHSAT5) { + // MathSAT5 does not stick to the standards naming here. But to be fair, the standard says + // that this method is not a good idea and our "fallback" (i.e. output fallbackDump) is + // preferred. + assertThat(nativeDump).contains("fp.as_ieee_bv"); + } else { + assertThat(nativeDump).contains("fp.to_ieee_bv"); + } + assertThat(nativeDump).doesNotContain("to_fp"); + } + + // Tests that the output of the SMTLIB2 dump of our versions of toIeeeBitvector() is always + // parseable + @Test + public void fallbackFloatingPointToIeeeBvSMTLIB2DumpParseTest() { + requireFloats(); + requireBitvectors(); + + FloatingPointType fpType = getSinglePrecisionFloatingPointType(); + FloatingPointFormula fpVar = fpmgr.makeVariable("fpVar", fpType); + BitvectorFormula someOtherBv = bvmgr.makeVariable(fpType.getTotalSize(), "someOtherBv"); + BitvectorFormula bvFromFpFallback = + bvmgr.makeVariable(fpType.getTotalSize(), "bvFromFpFallback"); + BooleanFormula fpToBvFallbackConstraint = fpmgr.bitwiseEqual(fpVar, bvFromFpFallback); + + String fallbackDump = + mgr.dumpFormula( + bmgr.and(fpToBvFallbackConstraint, bvmgr.equal(bvFromFpFallback, someOtherBv))) + .toString(); + checkThatDumpIsParseableWithCurrentSolver(fallbackDump); + } + + // Tests the parseability of the output of the SMTLIB2 dump of the native version of the + // toIeeeBitvector() method + @Test + public void nativeFloatingPointToIeeeBvSMTLIB2DumpParseTest() { + requireFloats(); + requireBitvectors(); + requireNativeFPToBitvector(); + + FloatingPointType fpType = getSinglePrecisionFloatingPointType(); + FloatingPointFormula fpVar = fpmgr.makeVariable("fpVar", fpType); + BitvectorFormula someOtherBv = bvmgr.makeVariable(fpType.getTotalSize(), "someOtherBv"); + BitvectorFormula bvFromFpNative = fpmgr.toIeeeBitvector(fpVar); + + String nativeDump = mgr.dumpFormula(bvmgr.equal(bvFromFpNative, someOtherBv)).toString(); + System.out.println(nativeDump); + checkThatDumpIsParseableWithCurrentSolver(nativeDump); + } + + // Tests the parseability of the output of the SMTLIB2 dump of the native version of the + // toIeeeBitvector() method from Z3 + @Test + public void nativeFloatingPointToIeeeBvSMTLIB2DumpFromZ3ParseTest() { + requireFloats(); + requireBitvectors(); + + if (ImmutableSet.of(Solvers.Z3, Solvers.CVC4).contains(solverToUse())) { + checkThatDumpIsParseableWithCurrentSolver(TO_IEEE_BV_DUMP_Z3); + } else { + assertThatDumpThrowsWhenParsingWithCurrentSolver(TO_IEEE_BV_DUMP_Z3); + } + } + + // Tests the parseability of the output of the SMTLIB2 dump of the native version of the + // toIeeeBitvector() method from MathSAT5 + @Test + public void nativeFloatingPointToIeeeBvSMTLIB2DumpFromMathSAT5ParseTest() { + requireFloats(); + requireBitvectors(); + + if (ImmutableSet.of(Solvers.MATHSAT5, Solvers.CVC4).contains(solverToUse())) { + checkThatDumpIsParseableWithCurrentSolver(TO_IEEE_BV_DUMP_MATHSAT5); + } else { + assertThatDumpThrowsWhenParsingWithCurrentSolver(TO_IEEE_BV_DUMP_MATHSAT5); + } } private void compareParseWithOrgExprFirst( @@ -537,7 +660,7 @@ private void checkThatAssertIsInLastLine(String dump) { } @SuppressWarnings("CheckReturnValue") - private void checkThatDumpIsParseable(String dump) { + private void checkThatDumpIsParseableWithCurrentSolver(String dump) { try { requireParser(); mgr.parse(dump); @@ -546,6 +669,20 @@ private void checkThatDumpIsParseable(String dump) { } } + /** + * Asserts that parsing the given dump in the current solver throws a {@link + * IllegalArgumentException}. + */ + @SuppressWarnings("CheckReturnValue") + private void assertThatDumpThrowsWhenParsingWithCurrentSolver(String dump) { + try { + requireParser(); + assertThrows(IllegalArgumentException.class, () -> mgr.parse(dump)); + } catch (AssumptionViolatedException ave) { + // ignore, i.e., do not report test-case as skipped. + } + } + private BooleanFormula genBoolExpr() { BooleanFormula a = bmgr.makeVariable("a"); BooleanFormula b = bmgr.makeVariable("b"); diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 3e77c298df..4eddfe498d 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -618,7 +618,7 @@ public void floatMoreVisit() { public void fpToBvTest() { requireFloats(); requireBitvectors(); - requireFPToBitvector(); + requireNativeFPToBitvector(); var fpType = FormulaType.getFloatingPointTypeFromSizesWithoutHiddenBit(5, 10); var visitor =