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..3cfaf9fcb7 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -8,9 +8,10 @@ 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; @@ -48,10 +49,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 +80,62 @@ public FloatingPointRoundingMode fromRoundingModeFormula( return getFormulaCreator().getRoundingMode(extractInfo(pRoundingModeFormula)); } - protected FloatingPointFormula wrap(TFormulaInfo pTerm) { + /** + * @param pTerm the term to be wrapped in a {@link FloatingPointFormula}. + * @param pTypeForAssertions the {@link FloatingPointType} used to create pTerm. This argument is + * only used to verify the exponent and mantissa sizes of pTerm. + * @return input term pTerm in a {@link FloatingPointFormula}. + */ + protected FloatingPointFormula wrapFloatingPointAndAssertType( + TFormulaInfo pTerm, 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) + checkArgument( + type.equals(checkNotNull(pTypeForAssertions)), + "Floating-Point formula %s type %s is not equal to expected type %s", + pTerm, + type, + pTypeForAssertions); + + return getFormulaCreator().encapsulateFloatingPoint(pTerm); + } + + protected FloatingPointFormula wrapFloatingPoint(TFormulaInfo pTerm) { + FormulaType type = getFormulaCreator().getFormulaType(pTerm); + checkArgument( + type.isFloatingPointType(), + "Floating-Point formula %s has unexpected type: %s", + pTerm, + type); return getFormulaCreator().encapsulateFloatingPoint(pTerm); } @Override public FloatingPointFormula makeNumber(Rational n, FormulaType.FloatingPointType type) { - return wrap(makeNumberImpl(n.toString(), type, getDefaultRoundingMode())); + return wrapFloatingPointAndAssertType( + 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 wrapFloatingPointAndAssertType( + makeNumberImpl(n.toString(), type, getRoundingMode(pFloatingPointRoundingMode)), type); } @Override public FloatingPointFormula makeNumber(double n, FormulaType.FloatingPointType type) { - return wrap(makeNumberImpl(n, type, getDefaultRoundingMode())); + return wrapFloatingPointAndAssertType(makeNumberImpl(n, type, getDefaultRoundingMode()), type); } @Override public FloatingPointFormula makeNumber( double n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode) { - return wrap(makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode))); + return wrapFloatingPointAndAssertType( + makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode)), type); } protected abstract TFormulaInfo makeNumberImpl( @@ -106,13 +143,14 @@ protected abstract TFormulaInfo makeNumberImpl( @Override public FloatingPointFormula makeNumber(BigDecimal n, FormulaType.FloatingPointType type) { - return wrap(makeNumberImpl(n, type, getDefaultRoundingMode())); + return wrapFloatingPointAndAssertType(makeNumberImpl(n, type, getDefaultRoundingMode()), type); } @Override public FloatingPointFormula makeNumber( BigDecimal n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode) { - return wrap(makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode))); + return wrapFloatingPointAndAssertType( + makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode)), type); } protected TFormulaInfo makeNumberImpl( @@ -122,13 +160,14 @@ protected TFormulaInfo makeNumberImpl( @Override public FloatingPointFormula makeNumber(String n, FormulaType.FloatingPointType type) { - return wrap(makeNumberImpl(n, type, getDefaultRoundingMode())); + return wrapFloatingPointAndAssertType(makeNumberImpl(n, type, getDefaultRoundingMode()), type); } @Override public FloatingPointFormula makeNumber( String n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode) { - return wrap(makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode))); + return wrapFloatingPointAndAssertType( + makeNumberImpl(n, type, getRoundingMode(pFloatingPointRoundingMode)), type); } /** directly catch the most common special String constants. */ @@ -153,14 +192,14 @@ protected TFormulaInfo makeNumberImpl( @Override public FloatingPointFormula makeNumber( BigInteger exponent, BigInteger mantissa, Sign sign, FloatingPointType type) { - return wrap(makeNumberImpl(exponent, mantissa, sign, type)); + return wrapFloatingPointAndAssertType(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 +215,7 @@ protected abstract TFormulaInfo makeNumberAndRound( @Override public FloatingPointFormula makeVariable(String pVar, FormulaType.FloatingPointType pType) { checkVariableName(pVar); - return wrap(makeVariableImpl(pVar, pType)); + return wrapFloatingPointAndAssertType(makeVariableImpl(pVar, pType), pType); } protected abstract TFormulaInfo makeVariableImpl( @@ -184,21 +223,21 @@ protected abstract TFormulaInfo makeVariableImpl( @Override public FloatingPointFormula makePlusInfinity(FormulaType.FloatingPointType pType) { - return wrap(makePlusInfinityImpl(pType)); + return wrapFloatingPointAndAssertType(makePlusInfinityImpl(pType), pType); } protected abstract TFormulaInfo makePlusInfinityImpl(FormulaType.FloatingPointType pType); @Override public FloatingPointFormula makeMinusInfinity(FormulaType.FloatingPointType pType) { - return wrap(makeMinusInfinityImpl(pType)); + return wrapFloatingPointAndAssertType(makeMinusInfinityImpl(pType), pType); } protected abstract TFormulaInfo makeMinusInfinityImpl(FormulaType.FloatingPointType pType); @Override public FloatingPointFormula makeNaN(FormulaType.FloatingPointType pType) { - return wrap(makeNaNImpl(pType)); + return wrapFloatingPointAndAssertType(makeNaNImpl(pType), pType); } protected abstract TFormulaInfo makeNaNImpl(FormulaType.FloatingPointType pType); @@ -237,7 +276,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 wrapFloatingPointAndAssertType( + castFromImpl(extractInfo(pNumber), pSigned, pTargetType, getDefaultRoundingMode()), + pTargetType); } @Override @@ -246,9 +287,10 @@ public FloatingPointFormula castFrom( boolean signed, FloatingPointType targetType, FloatingPointRoundingMode pFloatingPointRoundingMode) { - return wrap( + return wrapFloatingPointAndAssertType( castFromImpl( - extractInfo(number), signed, targetType, getRoundingMode(pFloatingPointRoundingMode))); + extractInfo(number), signed, targetType, getRoundingMode(pFloatingPointRoundingMode)), + targetType); } protected abstract TFormulaInfo castFromImpl( @@ -261,14 +303,15 @@ 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 wrapFloatingPointAndAssertType( + fromIeeeBitvectorImpl(extractInfo(pNumber), pTargetType), pTargetType); } protected abstract TFormulaInfo fromIeeeBitvectorImpl( @@ -279,12 +322,40 @@ 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) { TFormulaInfo param1 = extractInfo(pNumber); - return wrap(negate(param1)); + return wrapFloatingPoint(negate(param1)); } protected abstract TFormulaInfo negate(TFormulaInfo pParam1); @@ -292,34 +363,35 @@ public FloatingPointFormula negate(FloatingPointFormula pNumber) { @Override public FloatingPointFormula abs(FloatingPointFormula pNumber) { TFormulaInfo param1 = extractInfo(pNumber); - return wrap(abs(param1)); + return wrapFloatingPoint(abs(param1)); } protected abstract TFormulaInfo abs(TFormulaInfo pParam1); @Override public FloatingPointFormula max(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2) { - return wrap(max(extractInfo(pNumber1), extractInfo(pNumber2))); + return wrapFloatingPoint(max(extractInfo(pNumber1), extractInfo(pNumber2))); } protected abstract TFormulaInfo max(TFormulaInfo pParam1, TFormulaInfo pParam2); @Override public FloatingPointFormula min(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2) { - return wrap(min(extractInfo(pNumber1), extractInfo(pNumber2))); + return wrapFloatingPoint(min(extractInfo(pNumber1), extractInfo(pNumber2))); } protected abstract TFormulaInfo min(TFormulaInfo pParam1, TFormulaInfo pParam2); @Override public FloatingPointFormula sqrt(FloatingPointFormula pNumber) { - return wrap(sqrt(extractInfo(pNumber), getDefaultRoundingMode())); + return wrapFloatingPoint(sqrt(extractInfo(pNumber), getDefaultRoundingMode())); } @Override public FloatingPointFormula sqrt( FloatingPointFormula number, FloatingPointRoundingMode pFloatingPointRoundingMode) { - return wrap(sqrt(extractInfo(number), getRoundingMode(pFloatingPointRoundingMode))); + return wrapFloatingPoint( + sqrt(extractInfo(number), getRoundingMode(pFloatingPointRoundingMode))); } protected abstract TFormulaInfo sqrt(TFormulaInfo pNumber, TFormulaInfo pRoundingMode); @@ -329,7 +401,7 @@ public FloatingPointFormula add(FloatingPointFormula pNumber1, FloatingPointForm TFormulaInfo param1 = extractInfo(pNumber1); TFormulaInfo param2 = extractInfo(pNumber2); - return wrap(add(param1, param2, getDefaultRoundingMode())); + return wrapFloatingPoint(add(param1, param2, getDefaultRoundingMode())); } @Override @@ -337,7 +409,7 @@ public FloatingPointFormula add( FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode) { - return wrap( + return wrapFloatingPoint( add( extractInfo(number1), extractInfo(number2), @@ -353,7 +425,7 @@ public FloatingPointFormula subtract( TFormulaInfo param1 = extractInfo(pNumber1); TFormulaInfo param2 = extractInfo(pNumber2); - return wrap(subtract(param1, param2, getDefaultRoundingMode())); + return wrapFloatingPoint(subtract(param1, param2, getDefaultRoundingMode())); } @Override @@ -364,7 +436,7 @@ public FloatingPointFormula subtract( TFormulaInfo param1 = extractInfo(number1); TFormulaInfo param2 = extractInfo(number2); - return wrap(subtract(param1, param2, getRoundingMode(pFloatingPointRoundingMode))); + return wrapFloatingPoint(subtract(param1, param2, getRoundingMode(pFloatingPointRoundingMode))); } protected abstract TFormulaInfo subtract( @@ -375,7 +447,7 @@ public FloatingPointFormula divide(FloatingPointFormula pNumber1, FloatingPointF TFormulaInfo param1 = extractInfo(pNumber1); TFormulaInfo param2 = extractInfo(pNumber2); - return wrap(divide(param1, param2, getDefaultRoundingMode())); + return wrapFloatingPoint(divide(param1, param2, getDefaultRoundingMode())); } @Override @@ -386,7 +458,7 @@ public FloatingPointFormula divide( TFormulaInfo param1 = extractInfo(number1); TFormulaInfo param2 = extractInfo(number2); - return wrap(divide(param1, param2, getRoundingMode(pFloatingPointRoundingMode))); + return wrapFloatingPoint(divide(param1, param2, getRoundingMode(pFloatingPointRoundingMode))); } protected abstract TFormulaInfo divide( @@ -398,7 +470,7 @@ public FloatingPointFormula multiply( TFormulaInfo param1 = extractInfo(pNumber1); TFormulaInfo param2 = extractInfo(pNumber2); - return wrap(multiply(param1, param2, getDefaultRoundingMode())); + return wrapFloatingPoint(multiply(param1, param2, getDefaultRoundingMode())); } @Override @@ -408,7 +480,7 @@ public FloatingPointFormula multiply( FloatingPointRoundingMode pFloatingPointRoundingMode) { TFormulaInfo param1 = extractInfo(number1); TFormulaInfo param2 = extractInfo(number2); - return wrap(multiply(param1, param2, getRoundingMode(pFloatingPointRoundingMode))); + return wrapFloatingPoint(multiply(param1, param2, getRoundingMode(pFloatingPointRoundingMode))); } protected abstract TFormulaInfo multiply( @@ -417,7 +489,7 @@ protected abstract TFormulaInfo multiply( @Override public FloatingPointFormula remainder( FloatingPointFormula number1, FloatingPointFormula number2) { - return wrap(remainder(extractInfo(number1), extractInfo(number2))); + return wrapFloatingPoint(remainder(extractInfo(number1), extractInfo(number2))); } protected abstract TFormulaInfo remainder(TFormulaInfo pParam1, TFormulaInfo pParam2); @@ -529,7 +601,7 @@ public BooleanFormula isNegative(FloatingPointFormula pNumber) { @Override public FloatingPointFormula round( FloatingPointFormula pFormula, FloatingPointRoundingMode pRoundingMode) { - return wrap(round(extractInfo(pFormula), pRoundingMode)); + return wrapFloatingPoint(round(extractInfo(pFormula), pRoundingMode)); } protected abstract TFormulaInfo round( diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java index 1bb109f98f..54272da4e8 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -445,9 +445,23 @@ private String sanitize(String formulaStr) { @Override public List parseAll(String formulaStr) throws IllegalArgumentException { - return parseAllImpl(sanitize(formulaStr)).stream() - .map(formulaCreator::encapsulateBoolean) - .collect(Collectors.toList()); + try { + return parseAllImpl(sanitize(formulaStr)).stream() + .map(formulaCreator::encapsulateBoolean) + .collect(Collectors.toList()); + } catch (IllegalArgumentException illegalArgumentException) { + if (illegalArgumentException.getMessage() != null + && (illegalArgumentException.getMessage().contains("to_ieee_bv") + || illegalArgumentException.getMessage().contains("as_ieee_bv"))) { + 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."; + throw new IllegalArgumentException( + illegalArgumentException.getMessage() + additionalMessage, illegalArgumentException); + } + throw illegalArgumentException; + } } protected abstract String dumpFormulaImpl(TFormulaInfo t) throws IOException; 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 84a528b48b..a1acde1d74 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/BitwuzlaFloatingPointManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java index caeb79267d..f6660918cc 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java @@ -25,17 +25,15 @@ public class BitwuzlaFloatingPointManager extends AbstractFloatingPointFormulaManager { - private final BitwuzlaFormulaCreator bitwuzlaCreator; + private final TermManager termManager; private final Term roundingMode; - // Keeps track of the temporary variables that are created for fp-to-bv casts - private static int counter = 0; - protected BitwuzlaFloatingPointManager( - BitwuzlaFormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode) { - super(pCreator); - bitwuzlaCreator = pCreator; + BitwuzlaFormulaCreator pCreator, + FloatingPointRoundingMode pFloatingPointRoundingMode, + BitwuzlaBitvectorFormulaManager pBvMgr) { + super(pCreator, pBvMgr); termManager = pCreator.getEnv(); roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode); } @@ -196,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++; - 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 6620e3ae0e..dfc1a59905 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -124,8 +124,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); } 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 ec74a57e2e..35b37b65d8 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 62a13120c7..fad1687749 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -41,8 +41,10 @@ public class CVC4FloatingPointFormulaManager private final Expr roundingMode; protected CVC4FloatingPointFormulaManager( - CVC4FormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode) { - super(pCreator); + 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 70f6c9d9b5..6293a02b6f 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 8f1d346920..25e3e36de0 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -35,8 +35,10 @@ public class CVC5FloatingPointFormulaManager private final Term roundingMode; protected CVC5FloatingPointFormulaManager( - CVC5FormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode) { - super(pCreator); + 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 40f5a9f5b1..f1b41fc73a 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 4316a7dbeb..122d9638aa 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 4161327d69..ac686509d5 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); @@ -478,7 +529,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); @@ -523,7 +574,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); @@ -569,6 +620,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)) @@ -1040,7 +1546,7 @@ public void fpTraversalWithRoundingMode() { @Test public void fpIeeeConversionTypes() { - requireFPToBitvector(); + requireNativeFPToBitvector(); FloatingPointFormula var = fpmgr.makeVariable("var", singlePrecType); assertThat(mgr.getFormulaType(fpmgr.toIeeeBitvector(var))) @@ -1049,7 +1555,7 @@ public void fpIeeeConversionTypes() { @Test public void fpIeeeConversion() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); FloatingPointFormula var = fpmgr.makeVariable("var", singlePrecType); assertThatFormula( @@ -1060,7 +1566,7 @@ public void fpIeeeConversion() throws SolverException, InterruptedException { @Test public void ieeeFpConversion() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); BitvectorFormula var = bvmgr.makeBitvector(32, 123456789); assertThatFormula( @@ -1151,7 +1657,7 @@ public void checkIeeeBv2FpConversion64() throws SolverException, InterruptedExce @Test public void checkIeeeFp2BvConversion32() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); proveForAll( // makeBV(value.bits) == fromFP(makeFP(value.float)) @@ -1164,7 +1670,7 @@ public void checkIeeeFp2BvConversion32() throws SolverException, InterruptedExce @Test public void checkIeeeFp2BvConversion64() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); proveForAll( // makeBV(value.bits) == fromFP(makeFP(value.float)) @@ -1175,6 +1681,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( @@ -1406,7 +1946,7 @@ public void bitvectorToFloatingPointMantissaSignBitInterpretationSinglePrecision @Test public void floatingPointMantissaSignBitWithBitvectorInterpretationSinglePrecision() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); int bvSize32 = singlePrecType.getTotalSize(); BitvectorFormula bvNumber32 = bvmgr.makeBitvector(bvSize32, BigInteger.ZERO); @@ -1519,7 +2059,7 @@ public void bitvectorToFloatingPointMantissaSignBitInterpretationDoublePrecision @Test public void floatingPointMantissaSignBitWithBitvectorInterpretationDoublePrecision() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); int bvSize64 = doublePrecType.getTotalSize(); BitvectorFormula bvNumberSize64 = bvmgr.makeBitvector(bvSize64, BigInteger.ZERO); @@ -1582,6 +2122,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 e28c6823c2..c0838d7393 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -257,18 +257,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..db83acd106 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,114 @@ 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 { + assertThrows( + IllegalArgumentException.class, + () -> checkThatDumpIsParseableWithCurrentSolver(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 { + assertThrows( + IllegalArgumentException.class, + () -> checkThatDumpIsParseableWithCurrentSolver(TO_IEEE_BV_DUMP_MATHSAT5)); + } } private void compareParseWithOrgExprFirst( @@ -525,7 +649,7 @@ private void checkThatAssertIsInLastLine(String dump) { } @SuppressWarnings("CheckReturnValue") - private void checkThatDumpIsParseable(String dump) { + private void checkThatDumpIsParseableWithCurrentSolver(String dump) { try { requireParser(); mgr.parse(dump); diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 25cfed2b87..cd37dd6757 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -616,10 +616,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 =