diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index 16a04dcb17..1c64123eaf 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -299,12 +299,49 @@ 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 total size of the {@link FloatingPointFormula}s {@link + * FloatingPointType}. 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 #toIeeeBitvector(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 with the given {@link BitvectorFormula}, + * conforming to the IEEE 754-2008 floating-point format. The size m of the given {@link + * BitvectorFormula} has to be equal to the sum of the sizes of the exponent eb and mantissa sb + * (including the hidden bit) 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), with eb + * being the {@link FloatingPointFormula}s exponent bit size, sb being its mantissa with the + * hidden bit, and eb + sb equal to the bit size of the used {@link BitvectorFormula} parameter, + * illustrated in SMTLIB2 as: + * + *

(= ((_ to_fp eb sb) bitvectorFormulaSetToBeEqualToFpNumber) fpNumber) + * + *

Example usage in SMTLIB2, asserting the equality of the 2 parameters: + * + *

(declare-fun bitvectorFormulaSetToBeEqualToFpNumber () (_ BitVec m)) + * + *

(assert (= ((_ to_fp eb sb) bitvectorFormulaSetToBeEqualToFpNumber) fpNumber)) + * + *

Note: SMTLIB2 output of this method uses the SMTLIB2 keyword 'to_fp' as described above. + * + * @param fpNumber the {@link FloatingPointFormula} to be converted into an IEEE bitvector. + * @param bitvectorFormulaSetToBeEqualToFpNumber 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) bitvectorFormulaSetToBeEqualToFpNumber) fpNumber). + */ + BooleanFormula toIeeeBitvector( + FloatingPointFormula fpNumber, BitvectorFormula bitvectorFormulaSetToBeEqualToFpNumber); + 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 e80bb6a3fe..1240abe0bc 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,68 @@ 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) { + checkArgument( + type.equals(pTypeForAssertions), + "Floating-Point formula %s type %s is not equal to expected type %s", + pTerm, + type, + pTypeForAssertions); + } else { + checkArgument( + type.isFloatingPointType(), + "Floating-Point formula %s has unexpected type: %s", + 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 +150,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 +166,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. */ @@ -153,14 +197,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); } @@ -176,7 +220,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( @@ -184,21 +228,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); @@ -237,7 +281,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 @@ -248,7 +294,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( @@ -261,14 +308,14 @@ 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( () -> String.format( "The total size %s of type %s has to match the size %s of type %s.", pTargetType.getTotalSize(), pTargetType, bvType.getSize(), bvType))); - return wrap(fromIeeeBitvectorImpl(extractInfo(pNumber), pTargetType)); + return wrap(fromIeeeBitvectorImpl(extractInfo(pNumber), pTargetType), pTargetType); } protected abstract TFormulaInfo fromIeeeBitvectorImpl( @@ -279,7 +326,35 @@ 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 toIeeeBitvector( + FloatingPointFormula fpNumber, BitvectorFormula bitvectorFormulaSetToBeEqualToFpNumber) { + FormulaType.FloatingPointType fpType = + (FloatingPointType) getFormulaCreator().getFormulaType(fpNumber); + checkArgument( + fpType.getTotalSize() == bvMgr.getLength(bitvectorFormulaSetToBeEqualToFpNumber), + "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", + bitvectorFormulaSetToBeEqualToFpNumber, + bvMgr.getLength(bitvectorFormulaSetToBeEqualToFpNumber), + fpNumber, + fpType.getTotalSize()); + + FloatingPointFormula fromIeeeBitvector = + fromIeeeBitvector(bitvectorFormulaSetToBeEqualToFpNumber, 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, fpNumber); + } @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 1bb109f98f..b0139a1368 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -366,22 +366,27 @@ protected TFormulaInfo parseImpl(String formulaStr) throws IllegalArgumentExcept @ForOverride protected List parseAllImpl(String formulaStr) throws IllegalArgumentException { - // The fallback implementation splits the input into declarations and assertions, - // and parses each assertion separately, - // which is not very efficient, but it works for simple cases and is better than nothing - List tokens = Tokenizer.tokenize(formulaStr); - - List declarationTokens = - tokens.stream().filter(Tokenizer::isDeclarationToken).collect(Collectors.toList()); - List definitionTokens = - tokens.stream().filter(Tokenizer::isDefinitionToken).collect(Collectors.toList()); - List assertTokens = - tokens.stream().filter(Tokenizer::isAssertToken).collect(Collectors.toList()); - String definitions = - Joiner.on("").join(declarationTokens) + Joiner.on("").join(definitionTokens); - - return Collections3.transformedImmutableListCopy( - assertTokens, assertion -> parseImpl(definitions + assertion)); + try { + // The fallback implementation splits the input into declarations and assertions, + // and parses each assertion separately, + // which is not very efficient, but it works for simple cases and is better than nothing + List tokens = Tokenizer.tokenize(formulaStr); + + List declarationTokens = + tokens.stream().filter(Tokenizer::isDeclarationToken).collect(Collectors.toList()); + List definitionTokens = + tokens.stream().filter(Tokenizer::isDefinitionToken).collect(Collectors.toList()); + List assertTokens = + tokens.stream().filter(Tokenizer::isAssertToken).collect(Collectors.toList()); + String definitions = + Joiner.on("").join(declarationTokens) + Joiner.on("").join(definitionTokens); + + return Collections3.transformedImmutableListCopy( + assertTokens, assertion -> parseImpl(definitions + assertion)); + + } catch (IllegalArgumentException illegalArgumentException) { + throw throwIllegalArgumentExceptionWithBetterErrorMessage(illegalArgumentException); + } } /** @@ -811,4 +816,29 @@ public final String unescape(String pVar) { } return pVar; // unchanged } + + /** + * 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 b14646b6f1..ec156c11f2 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java @@ -166,10 +166,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..fa0688d796 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 toIeeeBitvector( + FloatingPointFormula fpNumber, BitvectorFormula bitvectorFormulaSetToBeEqualToFpNumber) { + debugging.assertThreadLocal(); + debugging.assertFormulaInContext(fpNumber); + debugging.assertFormulaInContext(bitvectorFormulaSetToBeEqualToFpNumber); + BooleanFormula res = delegate.toIeeeBitvector(fpNumber, bitvectorFormulaSetToBeEqualToFpNumber); + 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..dc43c6e667 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 toIeeeBitvector( + FloatingPointFormula fpNumber, BitvectorFormula bitvectorFormulaSetToBeEqualToFpNumber) { + stats.fpOperations.getAndIncrement(); + return delegate.toIeeeBitvector(fpNumber, bitvectorFormulaSetToBeEqualToFpNumber); + } + @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..c3a930ac84 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 toIeeeBitvector( + FloatingPointFormula fpNumber, BitvectorFormula bitvectorFormulaSetToBeEqualToFpNumber) { + synchronized (sync) { + return delegate.toIeeeBitvector(fpNumber, bitvectorFormulaSetToBeEqualToFpNumber); + } + } + @Override public FloatingPointFormula round( FloatingPointFormula pFormula, FloatingPointRoundingMode pRoundingMode) { diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java index e7247fff72..961b0260ad 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java @@ -29,7 +29,6 @@ import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Bitwuzla; -import org.sosy_lab.java_smt.solvers.bitwuzla.api.Kind; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Option; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Options; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Result; @@ -103,9 +102,6 @@ public void popImpl() { @CanIgnoreReturnValue protected int addConstraint0(BooleanFormula constraint) { Term formula = creator.extractInfo(constraint); - for (Term t : creator.getConstraintsForTerm(formula)) { - formula = creator.getEnv().mk_term(Kind.AND, formula, t); - } env.assert_formula(formula); var label = BitwuzlaAbstractProver.ID_GENERATOR.getFreshId(); @@ -202,7 +198,6 @@ public Optional> unsatCoreOverAssumptions( for (BooleanFormula formula : assumptions) { Term term = creator.extractInfo(formula); newAssumptions.add(term); - newAssumptions.addAll(creator.getConstraintsForTerm(term)); } Result result = env.check_sat(new Vector_Term(newAssumptions)); 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 39964a3ff3..905f626389 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java @@ -10,7 +10,6 @@ import java.math.BigDecimal; import java.math.BigInteger; -import org.sosy_lab.common.UniqueIdGenerator; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.FloatingPointFormula; import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign; @@ -26,17 +25,15 @@ 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 final UniqueIdGenerator counter = new UniqueIdGenerator(); - BitwuzlaFloatingPointManager( - BitwuzlaFormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode) { - super(pCreator); - bitwuzlaCreator = pCreator; + BitwuzlaFormulaCreator pCreator, + FloatingPointRoundingMode pFloatingPointRoundingMode, + BitwuzlaBitvectorFormulaManager pBvMgr) { + super(pCreator, pBvMgr); termManager = pCreator.getEnv(); roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode); } @@ -197,48 +194,6 @@ protected Term fromIeeeBitvectorImpl(Term pNumber, FloatingPointType pTargetType pTargetType.getMantissaSizeWithHiddenBit()); } - @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.getFreshId(); - 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; - } - @Override protected Term negate(Term pParam1) { return termManager.mk_term(Kind.FP_NEG, pParam1); 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 b72074d427..079c242068 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -9,7 +9,6 @@ package org.sosy_lab.java_smt.solvers.bitwuzla; import static com.google.common.base.Preconditions.checkArgument; -import static org.sosy_lab.common.collect.Collections3.transformedImmutableSetCopy; import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointTypeFromSizesWithHiddenBit; import com.google.common.base.Preconditions; @@ -17,18 +16,11 @@ import com.google.common.collect.ImmutableList; import com.google.common.collect.Table; import java.math.BigInteger; -import java.util.ArrayDeque; import java.util.ArrayList; -import java.util.Collection; -import java.util.Deque; -import java.util.HashMap; import java.util.Iterator; -import java.util.LinkedHashSet; import java.util.List; -import java.util.Map; import java.util.Map.Entry; import java.util.Optional; -import java.util.Set; import org.sosy_lab.java_smt.api.ArrayFormula; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -63,22 +55,6 @@ class BitwuzlaFormulaCreator extends FormulaCreator formulaCache = HashBasedTable.create(); - /** - * This mapping stores symbols and their constraints, such as from fp-to-bv casts with their - * defining equation. - * - *

Bitwuzla does not support casts from floating-point to bitvector natively. The reason given - * is that the value is undefined for NaN and that the SMT-LIB standard also does not include such - * an operation. We try to work around this limitation by introducing a fresh variable - * __CAST_FROM_BV_XXXfor the result and then adding the constraint - * fp.to_fp(__CAST_FROM_BV_XXX) = <float-term> as a side-condition. This is also what - * is recommended by the SMT-LIB2 standard. The map variableCasts is used to store - * these side-conditions so that they can later be added as assertions. The keys of the map are - * the newly introduced variable symbols and the values are the defining equations as mentioned - * above. - */ - private final Map constraintsForVariables = new HashMap<>(); - BitwuzlaFormulaCreator(TermManager pTermManager) { super(pTermManager, pTermManager.mk_bool_sort(), null, null, null, null); } @@ -123,8 +99,6 @@ public Sort getArrayType(Sort indexType, Sort elementType) { @Override protected FloatingPointFormula encapsulateFloatingPoint(Term pTerm) { - assert getFormulaType(pTerm).isFloatingPointType() - : String.format("%s is no FP, but %s (%s)", pTerm, pTerm.sort(), getFormulaType(pTerm)); return new BitwuzlaFloatingPointFormula(pTerm); } @@ -603,37 +577,6 @@ public Object convertValue(Term term) { throw new AssertionError("Unknown value type."); } - /** Add a constraint that is pushed onto the prover stack whenever the variable is used. */ - public void addConstraintForVariable(String variable, Term constraint) { - constraintsForVariables.put(variable, constraint); - } - - /** - * Returns a set of additional constraints (side-conditions) that are needed to use some variables - * from the given term, such as utility variables from casts. - * - *

Bitwuzla does not support fp-to-bv conversion natively. We have to use side-conditions as a - * workaround. When a term containing fp-to-bv casts is added to the assertion stack these - * side-conditions need to be collected by calling this method and then also adding them to the - * assertion stack. - */ - public Collection getConstraintsForTerm(Term pTerm) { - final Set usedConstraintVariables = new LinkedHashSet<>(); - final Deque waitlist = new ArrayDeque<>(extractVariablesAndUFs(pTerm, false).keySet()); - while (!waitlist.isEmpty()) { - String current = waitlist.pop(); - if (constraintsForVariables.containsKey(current)) { // ignore variables without constraints - if (usedConstraintVariables.add(current)) { - // if we found a new variable with constraint, get transitive variables from constraint - Term constraint = constraintsForVariables.get(current); - waitlist.addAll(extractVariablesAndUFs(constraint, false).keySet()); - } - } - } - - return transformedImmutableSetCopy(usedConstraintVariables, constraintsForVariables::get); - } - @Override protected FloatingPointRoundingMode getRoundingMode(Term term) { checkArgument(term.sort().is_rm(), "Term '%s' is not of rounding mode sort.", term); diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java index c384dd5545..03eed94a12 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java @@ -230,9 +230,6 @@ public String dumpFormulaImpl(Term pTerm) { return "(assert " + pTerm + ")"; } Bitwuzla bitwuzla = new Bitwuzla(creator.getEnv()); - for (Term t : creator.getConstraintsForTerm(pTerm)) { - bitwuzla.assert_formula(t); - } bitwuzla.assert_formula(pTerm); return bitwuzla.print_formula(); } 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 2af48115d8..dd37c15fa0 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 97c0528cd7..cdeec44cd7 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 6bb9882a89..7e55eaa2ab 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -261,8 +261,6 @@ assert getFormulaType(pTerm).isBitvectorType() @Override protected FloatingPointFormula encapsulateFloatingPoint(Expr pTerm) { - assert getFormulaType(pTerm).isFloatingPointType() - : String.format("%s is no FP, but %s (%s)", 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 b5bd086812..8fb387f007 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 a5f9e2f91a..d6c382762e 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 4f0004b6cd..b12ffa8017 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() - : String.format("%s is no FP, but %s (%s)", 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 1302f2d0d5..7cab9889a5 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 c4a10604b1..9526e1fae7 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -302,7 +302,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 02b8dfcd7d..a7e7a84620 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 b455aa3c17..d2f317b7e6 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 900aebec4e..6678029211 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -363,7 +363,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 18cbdb246d..79dcd9bb21 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java @@ -187,7 +187,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 36c6d5a8a8..3d91cd8844 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 2dc6da4ddf..fc5a676c5d 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java @@ -369,7 +369,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 04c37f5c28..4c2fda23f4 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,461 @@ 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.toIeeeBitvector(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.toIeeeBitvector(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 + @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.toIeeeBitvector(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: + case Z3_WITH_INTERPOLATION: + if (specialFpNumAsBv.equals(SINGLE_PRECISION_POSITIVE_ZERO_BITWISE)) { + assertThat(fpAsString).isEqualTo(SINGLE_PRECISION_NEGATIVE_ZERO_BITWISE); + break; + } + // $FALL-THROUGH$ + case MATHSAT5: + if (specialFpNumAsBv.equals(SINGLE_PRECISION_NEGATIVE_ZERO_BITWISE)) { + assertThat(fpAsString).isEqualTo(SINGLE_PRECISION_POSITIVE_ZERO_BITWISE); + break; + } + // $FALL-THROUGH$ + default: + assertThat(fpAsString).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.toIeeeBitvector(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.toIeeeBitvector(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.toIeeeBitvector(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.toIeeeBitvector(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.toIeeeBitvector(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 +1595,7 @@ public void fpTraversalWithRoundingMode() { @Test public void fpIeeeConversionTypes() { - requireFPToBitvector(); + requireNativeFPToBitvector(); FloatingPointFormula var = fpmgr.makeVariable("var", singlePrecType); assertThat(mgr.getFormulaType(fpmgr.toIeeeBitvector(var))) @@ -1098,7 +1604,7 @@ public void fpIeeeConversionTypes() { @Test public void fpIeeeConversion() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); FloatingPointFormula var = fpmgr.makeVariable("var", singlePrecType); assertThatFormula( @@ -1109,7 +1615,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 +1706,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 +1719,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 +1730,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.toIeeeBitvector(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.toIeeeBitvector(fpmgr.makeNumber(pDouble, doublePrecType), bv), + bvmgr.equal(bvmgr.makeBitvector(64, Double.doubleToRawLongBits(pDouble)), bv)); + }); + } + private List getListOfFloats() { List flts = Lists.newArrayList( @@ -1455,7 +1995,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 +2108,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 +2177,31 @@ public void failOnInvalidString() { assertThrows(Exception.class, () -> fpmgr.makeNumber("a", singlePrecType)); } + @Test + public void failOnInvalidBvSizeInToIeeeFallback() { + FloatingPointType fpType = singlePrecType; + assertThrows( + IllegalArgumentException.class, + () -> + fpmgr.toIeeeBitvector( + fpmgr.makeVariable("someName1", fpType), + bvmgr.makeVariable(fpType.getTotalSize() + 1, "someBv1"))); + assertThrows( + IllegalArgumentException.class, + () -> + fpmgr.toIeeeBitvector( + fpmgr.makeVariable("someName2", fpType), + bvmgr.makeVariable(fpType.getTotalSize() - 1, "someBv2"))); + assertThrows( + IllegalArgumentException.class, + () -> + fpmgr.toIeeeBitvector( + 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 19b49c604b..6b8f0f3951 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -254,18 +254,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/SolverFormulaIOTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java index 94a3ab6461..f0423905d9 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; @@ -109,6 +113,19 @@ 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))\n" + + "(declare-fun fpVar () (_ FloatingPoint 8 24))\n" + + "(assert (= (fp.to_ieee_bv fpVar) someOtherBv))"; + + private static final String TO_IEEE_BV_DUMP_MATHSAT5 = + "(declare-fun fpVar () (_ FloatingPoint " + + "8 24))\n" + + "(declare-fun someOtherBv () (_ BitVec 32))\n" + + "(assert (let ((.def_12 (fp.as_ieee_bv fpVar)))\n" + + "(let ((.def_13 (= someOtherBv .def_12)))\n" + + ".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"); @@ -161,7 +178,7 @@ public void varDumpTest() { checkVariableIsDeclared(formDump, "|main::a|", "Bool"); checkVariableIsDeclared(formDump, "b", "Bool"); checkThatAssertIsInLastLine(formDump); - checkThatDumpIsParseable(formDump); + checkThatDumpIsParseableWithCurrentSolver(formDump); } @Test @@ -179,7 +196,7 @@ public void varWithSpaceDumpTest() { checkVariableIsDeclared(formDump, "|main a|", "Bool"); checkVariableIsDeclared(formDump, "b", "Bool"); checkThatAssertIsInLastLine(formDump); - checkThatDumpIsParseable(formDump); + checkThatDumpIsParseableWithCurrentSolver(formDump); } @Test @@ -211,7 +228,7 @@ public void varDumpTest2() { checkVariableIsDeclared(formDump, "b", "Bool"); // The serialization has to be parse-able. - checkThatDumpIsParseable(formDump); + checkThatDumpIsParseableWithCurrentSolver(formDump); } @Test @@ -230,7 +247,7 @@ public void valDumpTest() { String formDump = mgr.dumpFormula(valComp5).toString(); checkThatAssertIsInLastLine(formDump); - checkThatDumpIsParseable(formDump); + checkThatDumpIsParseableWithCurrentSolver(formDump); } @Test @@ -245,7 +262,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 @@ -261,7 +278,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 @@ -280,7 +297,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 @@ -409,7 +426,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 @@ -429,7 +446,7 @@ public void funDeclareTest2() { // check if dumped formula fits our specification checkThatFunOnlyDeclaredOnce(formDump, ImmutableSet.of("fun_a")); checkThatAssertIsInLastLine(formDump); - checkThatDumpIsParseable(formDump); + checkThatDumpIsParseableWithCurrentSolver(formDump); } @Test @@ -452,7 +469,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.toIeeeBitvector(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.toIeeeBitvector(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( @@ -525,7 +645,7 @@ private void checkThatAssertIsInLastLine(String dump) { } @SuppressWarnings("CheckReturnValue") - private void checkThatDumpIsParseable(String dump) { + private void checkThatDumpIsParseableWithCurrentSolver(String dump) { try { requireParser(); mgr.parse(dump); @@ -534,6 +654,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 bf85fb6e1e..51bf0986a1 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -618,10 +618,7 @@ public void floatMoreVisit() { public void fpToBvTest() { requireFloats(); requireBitvectors(); - assume() - .withMessage("FP-to-BV conversion not available for CVC4 and CVC5") - .that(solverToUse()) - .isNoneOf(Solvers.CVC4, Solvers.CVC5); + requireNativeFPToBitvector(); var fpType = FormulaType.getFloatingPointTypeFromSizesWithoutHiddenBit(5, 10); var visitor =