From 6a91ebf8f6f5808058c6b8b30bb4904442c9e155 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 13 Aug 2025 19:43:28 +0200 Subject: [PATCH 01/39] Remove workaround for toIeeeBitvector() in Bitwuzla as the extra constraint is not handed to the user --- .../java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java index 6ccc1c31ae..3baef6cd14 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java @@ -172,7 +172,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( From 5c864962adb053254b31c619650262b5fc9a4963 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 13 Aug 2025 19:44:25 +0200 Subject: [PATCH 02/39] Add fallback for toIeeeBitvector() based on the SMTLIB2 standards suggestion + add helper to get mantissa and exponent sizes for FPs (not finished for all solvers) --- .../api/FloatingPointFormulaManager.java | 29 +++++++- .../AbstractFloatingPointFormulaManager.java | 72 +++++++++++++++++-- .../DebuggingFloatingPointFormulaManager.java | 12 ++++ ...StatisticsFloatingPointFormulaManager.java | 8 +++ ...nchronizedFloatingPointFormulaManager.java | 9 +++ .../BitwuzlaFloatingPointManager.java | 64 ++++------------- .../cvc4/CVC4FloatingPointFormulaManager.java | 16 ++++- .../solvers/cvc4/CVC4SolverContext.java | 3 +- .../cvc5/CVC5FloatingPointFormulaManager.java | 16 ++++- .../solvers/cvc5/CVC5SolverContext.java | 2 +- .../Mathsat5FloatingPointFormulaManager.java | 16 ++++- .../mathsat5/Mathsat5SolverContext.java | 3 +- .../z3/Z3FloatingPointFormulaManager.java | 16 ++++- .../java_smt/solvers/z3/Z3SolverContext.java | 2 +- 14 files changed, 201 insertions(+), 67 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index 62bb3afbe4..a25e20144c 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -15,6 +15,7 @@ import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign; import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; +import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula; /** * Floating point operations. @@ -285,11 +286,35 @@ FloatingPointFormula castFrom( /** * Create a formula that produces a representation of the given floating-point value as a - * bitvector conforming to the IEEE format. The size of the resulting bitvector is the sum of the - * sizes of the exponent and mantissa of the input formula plus 1 (for the sign bit). + * bitvector conforming to the IEEE 754-2008 format. The size of the resulting bitvector is the + * sum of the sizes of the exponent and mantissa of the input formula plus 1 (for the sign bit). */ BitvectorFormula toIeeeBitvector(FloatingPointFormula number); + /** + * Create a formula that produces a representation of the given floating-point value as a + * bitvector conforming to the IEEE 754-2008 format. The size of the resulting bitvector is the + * sum of the sizes of the exponent and mantissa of the input formula plus 1 (for the sign bit). + * This implementation can be used independently of {@link + * #toIeeeBitvector(FloatingPointFormula)}, as it does not rely on an SMT solvers support for + * {@link #toIeeeBitvector(FloatingPointFormula)}. Behavior for special FP values (NaN, Inf, etc.) + * is not defined. In case you want to define how to handle those values, please use TODO This + * method is based on a suggestion in the SMTLib2 standard ( source) implementation: + * + *

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

(assert (= ((_ to_fp eb sb) b) f)) + * + * @param number the {@link FloatingPointFormula} to be converted into an IEEE bitvector. + * @param bitvectorConstantName the name of the returned {@link BitvectorFormula}. + * @return {@link BitvectorFormulaAndBooleanFormula} consisting of the transformed input + * floating-point as a {@link BitvectorFormula} and the additional constraint as {@link + * BooleanFormula}. + */ + BitvectorFormulaAndBooleanFormula toIeeeBitvector( + FloatingPointFormula number, String bitvectorConstantName); + 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 47c847afe2..2691f275cc 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -8,9 +8,9 @@ package org.sosy_lab.java_smt.basicimpl; +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; @@ -45,10 +45,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(); @@ -145,7 +149,7 @@ protected abstract TFormulaInfo makeNumberImpl( BigInteger exponent, BigInteger mantissa, Sign sign, FloatingPointType type); protected static boolean isNegativeZero(Double pN) { - Preconditions.checkNotNull(pN); + checkNotNull(pN); return Double.valueOf("-0.0").equals(pN); } @@ -256,7 +260,43 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula pNumber) { return getFormulaCreator().encapsulateBitvector(toIeeeBitvectorImpl(extractInfo(pNumber))); } - protected abstract TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber); + protected TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber) { + throw new UnsupportedOperationException( + "The chosen solver does not support transforming " + + "FloatingPointFormula to IEEE bitvectors. Try using "); // TODO: finish + } + + @Override + public BitvectorFormulaAndBooleanFormula toIeeeBitvector( + FloatingPointFormula f, String bitvectorConstantName) { + + int mantissaSize = getMantissaSize(f); + int exponentSize = getExponentSize(f); + BitvectorFormula bvFormula = + bvMgr.makeVariable(mantissaSize + exponentSize, bitvectorConstantName); + + FloatingPointFormula fromIeeeBitvector = + fromIeeeBitvector( + bvFormula, FloatingPointType.getFloatingPointType(exponentSize, mantissaSize)); + + // assignment() allows a value to be NaN etc. + // Note: All fp.to_* functions are unspecified for NaN and infinity input values! + BooleanFormula additionalConstraint = assignment(fromIeeeBitvector, f); + + return BitvectorFormulaAndBooleanFormula.of(bvFormula, additionalConstraint); + } + + protected int getMantissaSize(FloatingPointFormula f) { + return getMantissaSizeImpl(extractInfo(f)); + } + + protected abstract int getMantissaSizeImpl(TFormulaInfo f); + + protected int getExponentSize(FloatingPointFormula f) { + return getExponentSizeImpl(extractInfo(f)); + } + + protected abstract int getExponentSizeImpl(TFormulaInfo f); @Override public FloatingPointFormula negate(FloatingPointFormula pNumber) { @@ -519,4 +559,28 @@ protected static String getBvRepresentation(BigInteger integer, int size) { } return String.copyValueOf(values); } + + public static class BitvectorFormulaAndBooleanFormula { + private final BitvectorFormula bitvectorFormula; + private final BooleanFormula booleanFormula; + + private BitvectorFormulaAndBooleanFormula( + BitvectorFormula pBitvectorFormula, BooleanFormula pBooleanFormula) { + bitvectorFormula = checkNotNull(pBitvectorFormula); + booleanFormula = checkNotNull(pBooleanFormula); + } + + protected static BitvectorFormulaAndBooleanFormula of( + BitvectorFormula pBitvectorFormula, BooleanFormula pBooleanFormula) { + return new BitvectorFormulaAndBooleanFormula(pBitvectorFormula, pBooleanFormula); + } + + public BitvectorFormula getBitvectorFormula() { + return bitvectorFormula; + } + + public BooleanFormula getBooleanFormula() { + return booleanFormula; + } + } } diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java index 74b1677375..8bd8d1df03 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java @@ -20,6 +20,7 @@ import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; +import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula; public class DebuggingFloatingPointFormulaManager implements FloatingPointFormulaManager { private final FloatingPointFormulaManager delegate; @@ -206,6 +207,17 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula number) { return result; } + @Override + public BitvectorFormulaAndBooleanFormula toIeeeBitvector( + FloatingPointFormula number, String bitvectorConstantName) { + debugging.assertThreadLocal(); + debugging.assertFormulaInContext(number); + BitvectorFormulaAndBooleanFormula res = delegate.toIeeeBitvector(number, bitvectorConstantName); + debugging.addFormulaTerm(res.getBitvectorFormula()); + debugging.addFormulaTerm(res.getBooleanFormula()); + return res; + } + @Override public 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 415b7cb00f..666a5ac1af 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java @@ -22,6 +22,7 @@ import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; +import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula; class StatisticsFloatingPointFormulaManager implements FloatingPointFormulaManager { @@ -166,6 +167,13 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula pNumber) { return delegate.toIeeeBitvector(pNumber); } + @Override + public BitvectorFormulaAndBooleanFormula toIeeeBitvector( + FloatingPointFormula number, String bitvectorConstantName) { + stats.fpOperations.getAndIncrement(); + return delegate.toIeeeBitvector(number, bitvectorConstantName); + } + @Override public 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 3d922f71a8..5fb2d34bd4 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java @@ -23,6 +23,7 @@ import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula; class SynchronizedFloatingPointFormulaManager implements FloatingPointFormulaManager { @@ -186,6 +187,14 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula pNumber) { } } + @Override + public BitvectorFormulaAndBooleanFormula toIeeeBitvector( + FloatingPointFormula number, String bitvectorConstantName) { + synchronized (sync) { + return delegate.toIeeeBitvector(number, bitvectorConstantName); + } + } + @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 cb03e5aa6d..d0db5a1dc5 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.getTermManager(); roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode); } @@ -148,6 +146,16 @@ protected Term castToImpl( } } + @Override + protected int getMantissaSizeImpl(Term fp) { + return fp.sort().fp_sig_size(); + } + + @Override + protected int getExponentSizeImpl(Term fp) { + return fp.sort().fp_exp_size(); + } + @Override protected Term castFromImpl( Term pNumber, boolean pSigned, FloatingPointType pTargetType, Term pRoundingMode) { @@ -186,48 +194,6 @@ protected Term fromIeeeBitvectorImpl(Term pNumber, FloatingPointType pTargetType pTargetType.getMantissaSize() + 1); } - @Override - protected Term toIeeeBitvectorImpl(Term pNumber) { - int sizeExp = pNumber.sort().fp_exp_size(); - int sizeSig = pNumber.sort().fp_sig_size(); - - Sort bvSort = termManager.mk_bv_sort(sizeExp + sizeSig); - - // The following code creates a new variable that is returned as result. - // Additionally, we track constraints about the equality of the new variable and the FP number, - // which is added onto the prover stack whenever the new variable is used as assertion. - - // TODO This internal implementation is a technical dept and should be removed. - // The additional constraints are not transparent in all cases, e.g., when visiting a - // formula, creating a model, or transferring the assertions onto another prover stack. - // A better way would be a direct implementation of this in Bitwuzla, without interfering - // with JavaSMT. - - // Note that NaN is handled as a special case in this method. This is not strictly necessary, - // but if we just use "fpTerm = to_fp(bvVar)" the NaN will be given a random payload (and - // sign). Since NaN payloads are not preserved here anyway we might as well pick a canonical - // representation, e.g., which is "0 11111111 10000000000000000000000" for single precision. - String nanRepr = "0" + "1".repeat(sizeExp + 1) + "0".repeat(sizeSig - 2); - Term bvNaN = termManager.mk_bv_value(bvSort, nanRepr); - - // TODO creating our own utility variables might eb unexpected from the user. - // We might need to exclude such variables in models and formula traversal. - String newVariable = "__JAVASMT__CAST_FROM_BV_" + counter++; - Term bvVar = termManager.mk_const(bvSort, newVariable); - Term equal = - termManager.mk_term( - Kind.ITE, - termManager.mk_term(Kind.FP_IS_NAN, pNumber), - termManager.mk_term(Kind.EQUAL, bvVar, bvNaN), - termManager.mk_term( - Kind.EQUAL, - termManager.mk_term(Kind.FP_TO_FP_FROM_BV, bvVar, sizeExp, sizeSig), - pNumber)); - - bitwuzlaCreator.addConstraintForVariable(newVariable, equal); - return bvVar; - } - @Override protected Term negate(Term pParam1) { return termManager.mk_term(Kind.FP_NEG, pParam1); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java index 248f6a55a8..b83769b8b2 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); } @@ -385,4 +387,14 @@ protected Expr toIeeeBitvectorImpl(Expr pNumber) { protected Expr round(Expr pFormula, FloatingPointRoundingMode pRoundingMode) { return exprManager.mkExpr(Kind.FLOATINGPOINT_RTI, getRoundingModeImpl(pRoundingMode), pFormula); } + + @Override + protected int getMantissaSizeImpl(Expr f) { + throw new UnsupportedOperationException("implement me"); + } + + @Override + protected int getExponentSizeImpl(Expr f) { + throw new UnsupportedOperationException("implement me"); + } } 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 883a8a1f8a..c646ac5914 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); @@ -445,4 +447,14 @@ protected Term toIeeeBitvectorImpl(Term pNumber) { protected Term round(Term pFormula, FloatingPointRoundingMode pRoundingMode) { return termManager.mkTerm(Kind.FLOATINGPOINT_RTI, getRoundingModeImpl(pRoundingMode), pFormula); } + + @Override + protected int getMantissaSizeImpl(Term f) { + throw new UnsupportedOperationException("implement me"); + } + + @Override + protected int getExponentSizeImpl(Term f) { + throw new UnsupportedOperationException("implement me"); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java index 97e0d269b2..c4f0967b45 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java @@ -150,7 +150,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); 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 d994620231..21176cf8ef 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); @@ -223,6 +225,16 @@ protected Long toIeeeBitvectorImpl(Long pNumber) { return Mathsat5NativeApi.msat_make_fp_as_ieeebv(mathsatEnv, pNumber); } + @Override + protected int getMantissaSizeImpl(Long f) { + throw new UnsupportedOperationException("implement me"); + } + + @Override + protected int getExponentSizeImpl(Long f) { + throw new UnsupportedOperationException("implement me"); + } + @Override protected Long negate(Long pNumber) { return msat_make_fp_neg(mathsatEnv, pNumber); diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java index 8ca17b8a2a..f169a2ffcb 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java @@ -192,7 +192,8 @@ public static Mathsat5SolverContext create( Mathsat5BitvectorFormulaManager bitvectorTheory = new Mathsat5BitvectorFormulaManager(creator, booleanTheory); Mathsat5FloatingPointFormulaManager floatingPointTheory = - new Mathsat5FloatingPointFormulaManager(creator, pFloatingPointRoundingMode); + new Mathsat5FloatingPointFormulaManager( + creator, pFloatingPointRoundingMode, bitvectorTheory); Mathsat5ArrayFormulaManager arrayTheory = new Mathsat5ArrayFormulaManager(creator); Mathsat5EnumerationFormulaManager enumerationTheory = new Mathsat5EnumerationFormulaManager(creator); diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java index 84ed3dc559..6a591c9198 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java @@ -26,8 +26,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); } @@ -314,4 +316,14 @@ protected Long isNegative(Long pParam) { protected Long round(Long pFormula, FloatingPointRoundingMode pRoundingMode) { return Native.mkFpaRoundToIntegral(z3context, getRoundingModeImpl(pRoundingMode), pFormula); } + + @Override + protected int getMantissaSizeImpl(Long f) { + throw new UnsupportedOperationException("implement me"); + } + + @Override + protected int getExponentSizeImpl(Long f) { + throw new UnsupportedOperationException("implement me"); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java index 7d408faf11..52f57369e6 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java @@ -186,7 +186,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); From 06e365f0cd9abe79566fee234a6e9e5049e88aca Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 31 Aug 2025 20:15:16 +0200 Subject: [PATCH 03/39] Add extended toIeeeBitvector() fallback implementation with the option of user defined results for special FP numbers --- .../api/FloatingPointFormulaManager.java | 36 +++++++++++++++++-- .../AbstractFloatingPointFormulaManager.java | 33 +++++++++++++++-- .../DebuggingFloatingPointFormulaManager.java | 20 +++++++++++ ...StatisticsFloatingPointFormulaManager.java | 9 +++++ ...nchronizedFloatingPointFormulaManager.java | 11 ++++++ 5 files changed, 105 insertions(+), 4 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index a25e20144c..051623ebb2 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -12,6 +12,7 @@ import java.math.BigDecimal; import java.math.BigInteger; +import java.util.Map; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign; import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; @@ -298,8 +299,9 @@ FloatingPointFormula castFrom( * This implementation can be used independently of {@link * #toIeeeBitvector(FloatingPointFormula)}, as it does not rely on an SMT solvers support for * {@link #toIeeeBitvector(FloatingPointFormula)}. Behavior for special FP values (NaN, Inf, etc.) - * is not defined. In case you want to define how to handle those values, please use TODO This - * method is based on a suggestion in the SMTLib2 standard ( source) implementation: * *

(declare-fun b () (_ BitVec m)) @@ -315,6 +317,36 @@ FloatingPointFormula castFrom( BitvectorFormulaAndBooleanFormula toIeeeBitvector( FloatingPointFormula number, String bitvectorConstantName); + /** + * Create a formula that produces a representation of the given floating-point value as a + * bitvector conforming to the IEEE 754-2008 format. The size of the resulting bitvector is the + * sum of the sizes of the exponent and mantissa of the input formula plus 1 (for the sign bit). + * This implementation can be used independently of {@link + * #toIeeeBitvector(FloatingPointFormula)}, as it does not rely on an SMT solvers support for + * {@link #toIeeeBitvector(FloatingPointFormula)}. Behavior for special FP values (NaN, Inf, etc.) + * can be defined using the specialFPConstantHandling parameter. This method is based on a + * suggestion in the SMTLib2 standard ( source) implementation: + * + *

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

(assert (= ((_ to_fp eb sb) b) f)) + * + * @param number the {@link FloatingPointFormula} to be converted into an IEEE bitvector. + * @param bitvectorConstantName the name of the returned {@link BitvectorFormula}. + * @param specialFPConstantHandling a {@link Map} defining the returned {@link BitvectorFormula} + * for special {@link FloatingPointFormula} constant values like Nan. For an empty {@link + * Map}, or missing mappings, this method behaves like {@link + * #toIeeeBitvector(FloatingPointFormula, String)}. + * @return {@link BitvectorFormulaAndBooleanFormula} consisting of the transformed input + * floating-point as a {@link BitvectorFormula} and the additional constraint as {@link + * BooleanFormula}. + */ + BitvectorFormulaAndBooleanFormula toIeeeBitvector( + FloatingPointFormula number, + String bitvectorConstantName, + Map specialFPConstantHandling); + FloatingPointFormula round(FloatingPointFormula formula, FloatingPointRoundingMode roundingMode); // ----------------- Arithmetic relations, return type NumeralFormula ----------------- diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 2691f275cc..6c4b771a5e 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -15,6 +15,7 @@ import java.math.BigInteger; import java.util.HashMap; import java.util.Map; +import java.util.Map.Entry; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -47,12 +48,16 @@ public abstract class AbstractFloatingPointFormulaManager bvMgr; + private final AbstractBooleanFormulaManager bMgr; + protected AbstractFloatingPointFormulaManager( FormulaCreator pCreator, - AbstractBitvectorFormulaManager pBvMgr) { + AbstractBitvectorFormulaManager pBvMgr, + AbstractBooleanFormulaManager pBMgr) { super(pCreator); roundingModes = new HashMap<>(); bvMgr = pBvMgr; + bMgr = pBMgr; } protected abstract TFormulaInfo getDefaultRoundingMode(); @@ -280,12 +285,36 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( bvFormula, FloatingPointType.getFloatingPointType(exponentSize, mantissaSize)); // assignment() allows a value to be NaN etc. - // Note: All fp.to_* functions are unspecified for NaN and infinity input values! + // Note: All fp.to_* functions are unspecified for NaN and infinity input values in the + // standard, what solvers return might be distinct. BooleanFormula additionalConstraint = assignment(fromIeeeBitvector, f); return BitvectorFormulaAndBooleanFormula.of(bvFormula, additionalConstraint); } + @Override + public BitvectorFormulaAndBooleanFormula toIeeeBitvector( + FloatingPointFormula f, + String bitvectorConstantName, + Map specialFPConstantHandling) { + + BitvectorFormulaAndBooleanFormula toIeeeBvAndConstraint = + toIeeeBitvector(f, bitvectorConstantName); + + BitvectorFormula toIeeeBv = toIeeeBvAndConstraint.getBitvectorFormula(); + for (Entry entry : + specialFPConstantHandling.entrySet()) { + FloatingPointFormula fpConst = entry.getKey(); + // TODO: can we check that fpConst is a special number here? + BooleanFormula assumption = assignment(fpConst, f); + // TODO: do we want to enforce the size of the BV? Decide and put into JavaDoc! + toIeeeBv = bMgr.ifThenElse(assumption, entry.getValue(), toIeeeBv); + } + + return BitvectorFormulaAndBooleanFormula.of( + toIeeeBv, toIeeeBvAndConstraint.getBooleanFormula()); + } + protected int getMantissaSize(FloatingPointFormula f) { return getMantissaSizeImpl(extractInfo(f)); } 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 8bd8d1df03..644d575497 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java @@ -10,6 +10,7 @@ import java.math.BigDecimal; import java.math.BigInteger; +import java.util.Map; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -218,6 +219,25 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( return res; } + @Override + public BitvectorFormulaAndBooleanFormula toIeeeBitvector( + FloatingPointFormula number, + String bitvectorConstantName, + Map specialFPConstantHandling) { + debugging.assertThreadLocal(); + debugging.assertFormulaInContext(number); + specialFPConstantHandling.forEach( + (key, value) -> { + debugging.assertFormulaInContext(key); + debugging.assertFormulaInContext(value); + }); + BitvectorFormulaAndBooleanFormula res = + delegate.toIeeeBitvector(number, bitvectorConstantName, specialFPConstantHandling); + debugging.addFormulaTerm(res.getBitvectorFormula()); + debugging.addFormulaTerm(res.getBooleanFormula()); + return res; + } + @Override public FloatingPointFormula round( FloatingPointFormula formula, FloatingPointRoundingMode roundingMode) { 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 666a5ac1af..80441e2d01 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java @@ -12,6 +12,7 @@ import java.math.BigDecimal; import java.math.BigInteger; +import java.util.Map; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -174,6 +175,14 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( return delegate.toIeeeBitvector(number, bitvectorConstantName); } + @Override + public BitvectorFormulaAndBooleanFormula toIeeeBitvector( + FloatingPointFormula number, + String bitvectorConstantName, + Map specialFPConstantHandling) { + return delegate.toIeeeBitvector(number, bitvectorConstantName, specialFPConstantHandling); + } + @Override public FloatingPointFormula round( FloatingPointFormula pFormula, FloatingPointRoundingMode pRoundingMode) { 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 5fb2d34bd4..d589a119c3 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java @@ -12,6 +12,7 @@ import java.math.BigDecimal; import java.math.BigInteger; +import java.util.Map; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -195,6 +196,16 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( } } + @Override + public BitvectorFormulaAndBooleanFormula toIeeeBitvector( + FloatingPointFormula number, + String bitvectorConstantName, + Map specialFPConstantHandling) { + synchronized (sync) { + return delegate.toIeeeBitvector(number, bitvectorConstantName, specialFPConstantHandling); + } + } + @Override public FloatingPointFormula round( FloatingPointFormula pFormula, FloatingPointRoundingMode pRoundingMode) { From d00e5348936d62f1c02aed054fffffa2036aace0 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 31 Aug 2025 20:15:49 +0200 Subject: [PATCH 04/39] Add bool manager to all FP managers for new toIeeeBitvector() impl --- .../solvers/bitwuzla/BitwuzlaFloatingPointManager.java | 5 +++-- .../java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java | 3 ++- .../solvers/cvc4/CVC4FloatingPointFormulaManager.java | 5 +++-- .../sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java | 3 ++- .../solvers/cvc5/CVC5FloatingPointFormulaManager.java | 5 +++-- .../sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java | 3 ++- .../mathsat5/Mathsat5FloatingPointFormulaManager.java | 5 +++-- .../java_smt/solvers/mathsat5/Mathsat5SolverContext.java | 2 +- .../java_smt/solvers/z3/Z3FloatingPointFormulaManager.java | 5 +++-- src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java | 3 ++- 10 files changed, 24 insertions(+), 15 deletions(-) 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 d0db5a1dc5..1e87dd1258 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java @@ -32,8 +32,9 @@ public class BitwuzlaFloatingPointManager protected BitwuzlaFloatingPointManager( BitwuzlaFormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode, - BitwuzlaBitvectorFormulaManager pBvMgr) { - super(pCreator, pBvMgr); + BitwuzlaBitvectorFormulaManager pBvMgr, + BitwuzlaBooleanFormulaManager pBmgr) { + super(pCreator, pBvMgr, pBmgr); termManager = pCreator.getTermManager(); roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode); } 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 3baef6cd14..77110ba71e 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java @@ -172,7 +172,8 @@ public static BitwuzlaSolverContext create( BitwuzlaQuantifiedFormulaManager quantifierTheory = new BitwuzlaQuantifiedFormulaManager(creator); BitwuzlaFloatingPointManager floatingPointTheory = - new BitwuzlaFloatingPointManager(creator, pFloatingPointRoundingMode, bitvectorTheory); + new BitwuzlaFloatingPointManager( + creator, pFloatingPointRoundingMode, bitvectorTheory, booleanTheory); BitwuzlaArrayFormulaManager arrayTheory = new BitwuzlaArrayFormulaManager(creator); BitwuzlaFormulaManager manager = new BitwuzlaFormulaManager( diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java index b83769b8b2..6d000dbe3d 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -43,8 +43,9 @@ public class CVC4FloatingPointFormulaManager protected CVC4FloatingPointFormulaManager( CVC4FormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode, - CVC4BitvectorFormulaManager pBvFormulaManager) { - super(pCreator, pBvFormulaManager); + CVC4BitvectorFormulaManager pBvFormulaManager, + CVC4BooleanFormulaManager pBoolFormulaManager) { + super(pCreator, pBvFormulaManager, pBoolFormulaManager); exprManager = pCreator.getEnv(); roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode); } 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 8fb387f007..6dff64284d 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java @@ -81,7 +81,8 @@ public static SolverContext create( CVC4FloatingPointFormulaManager fpTheory; if (Configuration.isBuiltWithSymFPU()) { fpTheory = - new CVC4FloatingPointFormulaManager(creator, pFloatingPointRoundingMode, bitvectorTheory); + new CVC4FloatingPointFormulaManager( + creator, pFloatingPointRoundingMode, bitvectorTheory, booleanTheory); } else { fpTheory = null; pLogger.log(Level.INFO, "CVC4 was built without support for FloatingPoint theory"); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java index c646ac5914..3aa8c06aaf 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -37,8 +37,9 @@ public class CVC5FloatingPointFormulaManager protected CVC5FloatingPointFormulaManager( CVC5FormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode, - CVC5BitvectorFormulaManager pBvFormulaManager) { - super(pCreator, pBvFormulaManager); + CVC5BitvectorFormulaManager pBvFormulaManager, + CVC5BooleanFormulaManager pBoolFormulaManager) { + super(pCreator, pBvFormulaManager, pBoolFormulaManager); termManager = pCreator.getEnv(); solver = pCreator.getSolver(); roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode); 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 c4f0967b45..696334c8ee 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java @@ -150,7 +150,8 @@ public static SolverContext create( CVC5BitvectorFormulaManager bitvectorTheory = new CVC5BitvectorFormulaManager(pCreator, booleanTheory); CVC5FloatingPointFormulaManager fpTheory = - new CVC5FloatingPointFormulaManager(pCreator, pFloatingPointRoundingMode, bitvectorTheory); + new CVC5FloatingPointFormulaManager( + pCreator, pFloatingPointRoundingMode, bitvectorTheory, booleanTheory); CVC5QuantifiedFormulaManager qfTheory = new CVC5QuantifiedFormulaManager(pCreator); CVC5ArrayFormulaManager arrayTheory = new CVC5ArrayFormulaManager(pCreator); CVC5SLFormulaManager slTheory = new CVC5SLFormulaManager(pCreator); diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java index 21176cf8ef..85f3b6a52d 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java @@ -63,8 +63,9 @@ class Mathsat5FloatingPointFormulaManager Mathsat5FloatingPointFormulaManager( Mathsat5FormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode, - Mathsat5BitvectorFormulaManager pBvFormulaManager) { - super(pCreator, pBvFormulaManager); + Mathsat5BitvectorFormulaManager pBvFormulaManager, + Mathsat5BooleanFormulaManager pBoolFormulaManager) { + super(pCreator, pBvFormulaManager, pBoolFormulaManager); mathsatEnv = pCreator.getEnv(); roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode); 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 f169a2ffcb..aaec8987bf 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java @@ -193,7 +193,7 @@ public static Mathsat5SolverContext create( new Mathsat5BitvectorFormulaManager(creator, booleanTheory); Mathsat5FloatingPointFormulaManager floatingPointTheory = new Mathsat5FloatingPointFormulaManager( - creator, pFloatingPointRoundingMode, bitvectorTheory); + creator, pFloatingPointRoundingMode, bitvectorTheory, booleanTheory); Mathsat5ArrayFormulaManager arrayTheory = new Mathsat5ArrayFormulaManager(creator); Mathsat5EnumerationFormulaManager enumerationTheory = new Mathsat5EnumerationFormulaManager(creator); diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java index 6a591c9198..46ec7426b5 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java @@ -28,8 +28,9 @@ class Z3FloatingPointFormulaManager Z3FloatingPointFormulaManager( Z3FormulaCreator creator, FloatingPointRoundingMode pFloatingPointRoundingMode, - Z3BitvectorFormulaManager pBvFormulaManager) { - super(creator, pBvFormulaManager); + Z3BitvectorFormulaManager pBvFormulaManager, + Z3BooleanFormulaManager pBoolFormulaManager) { + super(creator, pBvFormulaManager, pBoolFormulaManager); z3context = creator.getEnv(); roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode); } 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 52f57369e6..80f9bd6904 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java @@ -186,7 +186,8 @@ public static synchronized Z3SolverContext create( Z3BitvectorFormulaManager bitvectorTheory = new Z3BitvectorFormulaManager(creator, booleanTheory); Z3FloatingPointFormulaManager floatingPointTheory = - new Z3FloatingPointFormulaManager(creator, pFloatingPointRoundingMode, bitvectorTheory); + new Z3FloatingPointFormulaManager( + creator, pFloatingPointRoundingMode, bitvectorTheory, booleanTheory); Z3QuantifiedFormulaManager quantifierManager = new Z3QuantifiedFormulaManager(creator); Z3ArrayFormulaManager arrayManager = new Z3ArrayFormulaManager(creator); Z3StringFormulaManager stringTheory = new Z3StringFormulaManager(creator); From bc5a5e32ef964fdbac7a19457370d687cae8e2fa Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 31 Aug 2025 20:18:47 +0200 Subject: [PATCH 05/39] Simplify toIeeeBitvector() fallback implementation --- .../AbstractFloatingPointFormulaManager.java | 26 ++++++++----------- 1 file changed, 11 insertions(+), 15 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 6c4b771a5e..4e5a5c616e 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -11,6 +11,7 @@ import static com.google.common.base.Preconditions.checkNotNull; import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName; +import com.google.common.collect.ImmutableMap; import java.math.BigDecimal; import java.math.BigInteger; import java.util.HashMap; @@ -274,6 +275,14 @@ protected TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber) { @Override public BitvectorFormulaAndBooleanFormula toIeeeBitvector( FloatingPointFormula f, String bitvectorConstantName) { + return toIeeeBitvector(f, bitvectorConstantName, ImmutableMap.of()); + } + + @Override + public BitvectorFormulaAndBooleanFormula toIeeeBitvector( + FloatingPointFormula f, + String bitvectorConstantName, + Map specialFPConstantHandling) { int mantissaSize = getMantissaSize(f); int exponentSize = getExponentSize(f); @@ -289,19 +298,7 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( // standard, what solvers return might be distinct. BooleanFormula additionalConstraint = assignment(fromIeeeBitvector, f); - return BitvectorFormulaAndBooleanFormula.of(bvFormula, additionalConstraint); - } - - @Override - public BitvectorFormulaAndBooleanFormula toIeeeBitvector( - FloatingPointFormula f, - String bitvectorConstantName, - Map specialFPConstantHandling) { - - BitvectorFormulaAndBooleanFormula toIeeeBvAndConstraint = - toIeeeBitvector(f, bitvectorConstantName); - - BitvectorFormula toIeeeBv = toIeeeBvAndConstraint.getBitvectorFormula(); + BitvectorFormula toIeeeBv = bvFormula; for (Entry entry : specialFPConstantHandling.entrySet()) { FloatingPointFormula fpConst = entry.getKey(); @@ -311,8 +308,7 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( toIeeeBv = bMgr.ifThenElse(assumption, entry.getValue(), toIeeeBv); } - return BitvectorFormulaAndBooleanFormula.of( - toIeeeBv, toIeeeBvAndConstraint.getBooleanFormula()); + return BitvectorFormulaAndBooleanFormula.of(toIeeeBv, additionalConstraint); } protected int getMantissaSize(FloatingPointFormula f) { From 6e6ec7e600f1ead037574ef5d437a560ad421843 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 31 Aug 2025 20:43:48 +0200 Subject: [PATCH 06/39] Add CVC4 implementation for getMantissaSize() and getExponentSize() --- .../solvers/cvc4/CVC4FloatingPointFormulaManager.java | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) 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 6d000dbe3d..51985c8be7 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -8,6 +8,8 @@ package org.sosy_lab.java_smt.solvers.cvc4; +import static com.google.common.base.Preconditions.checkArgument; + import com.google.common.collect.ImmutableList; import edu.stanford.CVC4.BitVector; import edu.stanford.CVC4.BitVectorExtract; @@ -391,11 +393,15 @@ protected Expr round(Expr pFormula, FloatingPointRoundingMode pRoundingMode) { @Override protected int getMantissaSizeImpl(Expr f) { - throw new UnsupportedOperationException("implement me"); + Type type = f.getType(); + checkArgument(type.isFloatingPoint()); + return (int) ((edu.stanford.CVC4.FloatingPointType) type).getSignificandSize(); } @Override protected int getExponentSizeImpl(Expr f) { - throw new UnsupportedOperationException("implement me"); + Type type = f.getType(); + checkArgument(type.isFloatingPoint()); + return (int) ((edu.stanford.CVC4.FloatingPointType) type).getExponentSize(); } } From f584f6bc36615ac6e9fee807816957cada6bf891 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 31 Aug 2025 20:43:53 +0200 Subject: [PATCH 07/39] Add CVC5 implementation for getMantissaSize() and getExponentSize() --- .../solvers/cvc5/CVC5FloatingPointFormulaManager.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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 3aa8c06aaf..b464130134 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -451,11 +451,13 @@ protected Term round(Term pFormula, FloatingPointRoundingMode pRoundingMode) { @Override protected int getMantissaSizeImpl(Term f) { - throw new UnsupportedOperationException("implement me"); + Sort sort = f.getSort(); + return sort.getFloatingPointSignificandSize(); } @Override protected int getExponentSizeImpl(Term f) { - throw new UnsupportedOperationException("implement me"); + Sort sort = f.getSort(); + return sort.getFloatingPointExponentSize(); } } From 9df8f217483e56fb3149f40c48f8d6ed8aa5ad02 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 31 Aug 2025 20:43:59 +0200 Subject: [PATCH 08/39] Add Mathsat5 implementation for getMantissaSize() and getExponentSize() --- .../mathsat5/Mathsat5FloatingPointFormulaManager.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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 85f3b6a52d..9b7d12a1f8 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java @@ -8,6 +8,8 @@ package org.sosy_lab.java_smt.solvers.mathsat5; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_fp_type_exp_width; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_fp_type_mant_width; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_equal; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_abs; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_bits_number; @@ -228,12 +230,12 @@ protected Long toIeeeBitvectorImpl(Long pNumber) { @Override protected int getMantissaSizeImpl(Long f) { - throw new UnsupportedOperationException("implement me"); + return msat_get_fp_type_mant_width(mathsatEnv, msat_term_get_type(f)); } @Override protected int getExponentSizeImpl(Long f) { - throw new UnsupportedOperationException("implement me"); + return msat_get_fp_type_exp_width(mathsatEnv, msat_term_get_type(f)); } @Override From 105e7f27c25b3964bcf68064f379811f047d4daa Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 31 Aug 2025 20:44:03 +0200 Subject: [PATCH 09/39] Add Z3 implementation for getMantissaSize() and getExponentSize() --- .../java_smt/solvers/z3/Z3FloatingPointFormulaManager.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 46ec7426b5..848ef2c15f 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java @@ -320,11 +320,11 @@ protected Long round(Long pFormula, FloatingPointRoundingMode pRoundingMode) { @Override protected int getMantissaSizeImpl(Long f) { - throw new UnsupportedOperationException("implement me"); + return Native.fpaGetEbits(z3context, Native.getSort(z3context, f)); } @Override protected int getExponentSizeImpl(Long f) { - throw new UnsupportedOperationException("implement me"); + return Native.fpaGetSbits(z3context, Native.getSort(z3context, f)); } } From 4ec71076955da3d68032dd734d2b7c116b311873 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 11:09:08 +0200 Subject: [PATCH 10/39] Add internal API to retrieve the width of a BV and implement it for all BV capable solvers --- .../basicimpl/AbstractBitvectorFormulaManager.java | 6 ++++++ .../bitwuzla/BitwuzlaBitvectorFormulaManager.java | 5 +++++ .../boolector/BoolectorBitvectorFormulaManager.java | 6 ++++++ .../solvers/cvc4/CVC4BitvectorFormulaManager.java | 9 +++++++++ .../solvers/cvc5/CVC5BitvectorFormulaManager.java | 5 +++++ .../mathsat5/Mathsat5BitvectorFormulaManager.java | 7 +++++++ .../princess/PrincessBitvectorFormulaManager.java | 5 +++++ .../solvers/yices2/Yices2BitvectorFormulaManager.java | 7 +++++++ .../java_smt/solvers/z3/Z3BitvectorFormulaManager.java | 5 +++++ 9 files changed, 55 insertions(+) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java index 46455c4829..8b8a1a58cf 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java @@ -439,4 +439,10 @@ protected TFormulaInfo distinctImpl(List pBits) { } return bmgr.andImpl(lst); } + + protected final int getBitvectorWidth(BitvectorFormula bitvector) { + return getBitvectorWidthImpl(extractInfo(bitvector)); + } + + protected abstract int getBitvectorWidthImpl(TFormulaInfo bitvector); } diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBitvectorFormulaManager.java index e99b5cbe16..d83b2208a3 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBitvectorFormulaManager.java @@ -203,4 +203,9 @@ protected Term extend(Term pNumber, int pExtensionBits, boolean pSigned) { return termManager.mk_term(Kind.BV_ZERO_EXTEND, pNumber, pExtensionBits); } } + + @Override + protected int getBitvectorWidthImpl(Term pNumber) { + return pNumber.sort().bv_size(); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java index b44c9af19d..23e5fa58ea 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java @@ -12,6 +12,7 @@ import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_and; import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_concat; import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_eq; +import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_get_width; import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_mul; import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_neg; import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_not; @@ -235,4 +236,9 @@ public Long extend(Long bitVec, int extensionBits, boolean signed) { return boolector_uext(btor, bitVec, extensionBits); } } + + @Override + protected int getBitvectorWidthImpl(Long bitvector) { + return boolector_get_width(btor, bitvector); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java index 89f672ab9e..b59db60b30 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java @@ -8,6 +8,8 @@ package org.sosy_lab.java_smt.solvers.cvc4; +import static com.google.common.base.Preconditions.checkArgument; + import edu.stanford.CVC4.BitVector; import edu.stanford.CVC4.BitVectorExtract; import edu.stanford.CVC4.BitVectorRotateLeft; @@ -259,4 +261,11 @@ protected Expr distinctImpl(List pParam) { pParam.forEach(param::add); return exprManager.mkExpr(Kind.DISTINCT, param); } + + @Override + protected int getBitvectorWidthImpl(Expr bitvector) { + Type type = bitvector.getType(); + checkArgument(type.isBitVector()); + return (int) ((edu.stanford.CVC4.BitVectorType) type).getSize(); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java index 83a9fae343..f47d654678 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java @@ -298,4 +298,9 @@ protected Term toIntegerFormulaImpl(Term pBv, boolean pSigned) { protected Term distinctImpl(List pParam) { return termManager.mkTerm(Kind.DISTINCT, pParam.toArray(new Term[0])); } + + @Override + protected int getBitvectorWidthImpl(Term bitvector) { + return bitvector.getSort().getBitVectorSize(); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5BitvectorFormulaManager.java index 5ccde4d21f..4adcbc6d27 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5BitvectorFormulaManager.java @@ -8,6 +8,7 @@ package org.sosy_lab.java_smt.solvers.mathsat5; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_bv_type_size; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_bv_and; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_bv_ashr; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_bv_concat; @@ -41,6 +42,7 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_int_from_ubv; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_int_to_bv; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_term_ite; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_get_type; import java.math.BigInteger; import java.util.function.Function; @@ -78,6 +80,11 @@ public Long extend(Long pNumber, int pExtensionBits, boolean pSigned) { } } + @Override + protected int getBitvectorWidthImpl(Long bitvector) { + return msat_get_bv_type_size(mathsatEnv, msat_term_get_type(bitvector)); + } + @Override public Long makeBitvectorImpl(int pLength, long pI) { int i = (int) pI; diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java index 4ea9cf3191..d6a5dc5376 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java @@ -200,4 +200,9 @@ protected IExpression extend(IExpression pNumber, int pExtensionBits, boolean pS return ModuloArithmetic$.MODULE$.zero_extend(pExtensionBits, (ITerm) pNumber); } } + + @Override + protected int getBitvectorWidthImpl(IExpression bitvector) { + return bitvector.length(); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java index 3df71f8a8a..6cabc088a6 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java @@ -34,11 +34,13 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bvsmod; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bvsrem; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bvsub; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bvtype_size; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bvxor2; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_parse_bvbin; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_rotate_left; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_rotate_right; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_sign_extend; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_of_term; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_zero_extend; import com.google.common.base.Preconditions; @@ -227,6 +229,11 @@ protected Integer extend(Integer pNumber, int pExtensionBits, boolean pSigned) { } } + @Override + protected int getBitvectorWidthImpl(Integer bitvector) { + return yices_bvtype_size(yices_type_of_term(bitvector)); + } + @Override protected Integer makeBitvectorImpl(int pLength, Integer pFormula) { throw new UnsupportedOperationException( diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3BitvectorFormulaManager.java index 940a58918d..969efe4539 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3BitvectorFormulaManager.java @@ -202,4 +202,9 @@ public Long greaterOrEquals(Long pNumber1, Long pNumber2, boolean signed) { protected Long distinctImpl(List pBits) { return Native.mkDistinct(z3context, pBits.size(), Longs.toArray(pBits)); } + + @Override + protected int getBitvectorWidthImpl(Long bitvector) { + return Native.getBvSortSize(z3context, Native.getSort(z3context, bitvector)); + } } From 97c1fe4a50bbf30900afa9e9a3c8e3b62124a85a Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 11:09:32 +0200 Subject: [PATCH 11/39] Add test for FP special number identity for equal precisions --- .../test/FloatingPointFormulaManagerTest.java | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 74390241cf..573b45a63f 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -73,6 +73,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 = FormulaType.getFloatingPointType(23, 42); From fdaabcc4459d87545d4af8d9442fd502eff87f9e Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 11:10:18 +0200 Subject: [PATCH 12/39] Add preconditions for FP toIeeeBitvector() method special number mappings and add it to JavaDoc --- .../api/FloatingPointFormulaManager.java | 10 ++++-- .../AbstractFloatingPointFormulaManager.java | 36 +++++++++++++++++-- 2 files changed, 40 insertions(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index 051623ebb2..4c36ed7f62 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -335,9 +335,13 @@ BitvectorFormulaAndBooleanFormula toIeeeBitvector( * @param number the {@link FloatingPointFormula} to be converted into an IEEE bitvector. * @param bitvectorConstantName the name of the returned {@link BitvectorFormula}. * @param specialFPConstantHandling a {@link Map} defining the returned {@link BitvectorFormula} - * for special {@link FloatingPointFormula} constant values like Nan. For an empty {@link - * Map}, or missing mappings, this method behaves like {@link - * #toIeeeBitvector(FloatingPointFormula, String)}. + * for special {@link FloatingPointFormula} constant numbers. You are only allowed to specify + * a mapping for special FP numbers with more than one well-defined bitvector representation, + * i.e. NaN and +/- Infinity. The width of the mapped bitvector values has to match the + * expected width of the bitvector return value. The {@link FloatingPointType}, i.e. + * precision, of the key FP numbers has to match the {@link FloatingPointType} of the + * parameter {@code number}. For an empty {@link Map}, or missing mappings, this method + * behaves like {@link #toIeeeBitvector(FloatingPointFormula, String)}. * @return {@link BitvectorFormulaAndBooleanFormula} consisting of the transformed input * floating-point as a {@link BitvectorFormula} and the additional constraint as {@link * BooleanFormula}. diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 4e5a5c616e..9ed60f5eb6 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -8,15 +8,18 @@ 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.collect.ImmutableMap; +import com.google.common.collect.ImmutableSet; import java.math.BigDecimal; import java.math.BigInteger; import java.util.HashMap; import java.util.Map; import java.util.Map.Entry; +import java.util.Set; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -298,14 +301,41 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( // standard, what solvers return might be distinct. BooleanFormula additionalConstraint = assignment(fromIeeeBitvector, f); + // Build special numbers so that we can compare them in the map + FloatingPointType precision = + FloatingPointType.getFloatingPointType(exponentSize, mantissaSize); + Set specialNumbers = + ImmutableSet.of( + makeNaN(precision), makePlusInfinity(precision), makeMinusInfinity(precision)); + BitvectorFormula toIeeeBv = bvFormula; for (Entry entry : specialFPConstantHandling.entrySet()) { FloatingPointFormula fpConst = entry.getKey(); - // TODO: can we check that fpConst is a special number here? + + // We check that FP const special numbers are used (info from SMTLib2-standard) + // NaN has multiple possible definitions. + // +/- Infinity each has 2; e.g., +infinity for sort (_ FloatingPoint 2 3) is represented + // equivalently by (_ +oo 2 3) and (fp #b0 #b11 #b00). + // -0 only has one representation; i.e. (_ -zero 3 2) abbreviates (fp #b1 #b000 #b0), and + // is therefore disallowed. + // This automatically checks the correct precision as well! + checkArgument( + specialNumbers.contains(fpConst), + "You are only allowed to specify a mapping for special FP numbers with more than one" + + " well-defined bitvector representation, i.e. NaN and +/- Infinity. Their precision" + + " has to match the precision of the formula to be represented as bitvector."); + + BitvectorFormula bvTerm = entry.getValue(); + checkArgument( + bvMgr.getBitvectorWidth(bvTerm) == bvMgr.getBitvectorWidth(bvFormula), + "The size of the bitvector terms used as mapped values needs to be equal to the size of" + + " the bitvector returned by this method"); + BooleanFormula assumption = assignment(fpConst, f); - // TODO: do we want to enforce the size of the BV? Decide and put into JavaDoc! - toIeeeBv = bMgr.ifThenElse(assumption, entry.getValue(), toIeeeBv); + toIeeeBv = bMgr.ifThenElse(assumption, bvTerm, toIeeeBv); + // TODO: add tests for this and the other method, find out typical returns and add tests, + // then add to doc. } return BitvectorFormulaAndBooleanFormula.of(toIeeeBv, additionalConstraint); From 3ecd1338a68725507cdcfc99e0af2c47d90aa774 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 17:21:58 +0200 Subject: [PATCH 13/39] Add native Mathsat test for mantissa not including the sign bit with BV transformation and width comparison --- .../Mathsat5AbstractNativeApiTest.java | 39 +++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java index bd277cf91a..129b2669a8 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java @@ -35,6 +35,7 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_repr; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_to_smtlib2_ext; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_to_smtlib2_term; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_type_equals; import org.junit.After; import org.junit.Ignore; @@ -79,6 +80,44 @@ public void fpMantWidth() { assertThat(msat_get_fp_type_mant_width(env, type)).isEqualTo(23); } + /* + * MathSAT5, compared to all other solvers and the standard, does not expect the sign bit to be + * included in the mantissa! + */ + @Test + public void fpMantissaDoesNotIncludeSignBit() { + int totalBVSize = 32; + long bvNumber = msat_make_bv_number(env, "42", totalBVSize, 10); + long bvType = msat_term_get_type(bvNumber); + assertThat(msat_get_bv_type_size(env, bvType)).isEqualTo(totalBVSize); + assertThat(msat_get_bv_type_size(env, msat_term_get_type(bvNumber))).isEqualTo(totalBVSize); + + int exponent = 8; + int mantissaWithoutSign = 23; // excluding sign bit + long fpSinglePrecType = msat_get_fp_type(env, exponent, mantissaWithoutSign); + assertThat(msat_get_fp_type_mant_width(env, fpSinglePrecType)).isEqualTo(mantissaWithoutSign); + assertThat(msat_get_fp_type_exp_width(env, fpSinglePrecType)).isEqualTo(exponent); + // total size is exp + man + 1 + assertThat( + msat_get_fp_type_mant_width(env, fpSinglePrecType) + + msat_get_fp_type_exp_width(env, fpSinglePrecType) + + 1) + .isEqualTo(totalBVSize); + + long bvToFpSinglePrec = + Mathsat5NativeApi.msat_make_fp_from_ieeebv(env, exponent, mantissaWithoutSign, bvNumber); + assertThat(msat_type_equals(msat_term_get_type(bvToFpSinglePrec), fpSinglePrecType)).isTrue(); + assertThat(msat_get_fp_type_mant_width(env, msat_term_get_type(bvToFpSinglePrec))) + .isEqualTo(mantissaWithoutSign); + assertThat(msat_get_fp_type_exp_width(env, msat_term_get_type(bvToFpSinglePrec))) + .isEqualTo(exponent); + + long bvToFpSinglePrecToBv = Mathsat5NativeApi.msat_make_fp_as_ieeebv(env, bvToFpSinglePrec); + assertThat(msat_type_equals(msat_term_get_type(bvToFpSinglePrecToBv), bvType)).isTrue(); + assertThat(msat_get_bv_type_size(env, msat_term_get_type(bvToFpSinglePrecToBv))) + .isEqualTo(totalBVSize); + } + @Test public void fpExpWidthIllegal() { long type = msat_get_integer_type(env); From 52dbeb568a60ae3506695a3a2117ca7a02a47b22 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 18:09:17 +0200 Subject: [PATCH 14/39] Add tests for FP toIeeeBitvector() fallback (without custom special number mapping) and a test for FP size/mantissa/exponent in relation to BV width for toIeeeBitvector() --- .../test/FloatingPointFormulaManagerTest.java | 202 +++++++++++++++++- .../java_smt/test/SolverBasedTest0.java | 19 +- 2 files changed, 212 insertions(+), 9 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 573b45a63f..ce125f5fdd 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -15,6 +15,7 @@ import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; import com.google.common.collect.ImmutableSet; import com.google.common.collect.Lists; import java.math.BigDecimal; @@ -41,6 +42,7 @@ import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula; public class FloatingPointFormulaManagerTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { @@ -434,7 +436,7 @@ public void specialValueFunctionsFrom64Bits() throws SolverException, Interrupte @Test public void specialValueFunctionsFrom32Bits2() throws SolverException, InterruptedException { requireBitvectors(); - requireFPToBitvector(); + requireNativeFPToBitvector(); final FloatingPointFormula x = fpmgr.makeVariable("x32", singlePrecType); final BitvectorFormula signBit = bvmgr.extract(fpmgr.toIeeeBitvector(x), 31, 31); @@ -479,7 +481,7 @@ public void specialValueFunctionsFrom32Bits2() throws SolverException, Interrupt @Test public void specialValueFunctionsFrom64Bits2() throws SolverException, InterruptedException { requireBitvectors(); - requireFPToBitvector(); + requireNativeFPToBitvector(); final FloatingPointFormula x = fpmgr.makeVariable("x64", doublePrecType); final BitvectorFormula signBit = bvmgr.extract(fpmgr.toIeeeBitvector(x), 63, 63); @@ -525,6 +527,192 @@ public void specialValueFunctionsFrom64Bits2() throws SolverException, Interrupt bmgr.and(bmgr.not(fpmgr.isNaN(x)), bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1)))); } + // Same as specialValueFunctionsFrom32Bits2, but with fallback toIeeeBitvector() implementation. + @Test + public void specialValueFunctionsFrom32Bits2ToIeeeFallback() + throws SolverException, InterruptedException { + requireBitvectors(); + + final FloatingPointFormula x = fpmgr.makeVariable("x32", singlePrecType); + BitvectorFormulaAndBooleanFormula xToIeeeAndAddConstraint = + fpmgr.toIeeeBitvector(x, "bvConst_x"); + BitvectorFormula xToIeee = xToIeeeAndAddConstraint.getBitvectorFormula(); + final BitvectorFormula signBit = bvmgr.extract(xToIeee, 31, 31); + final BitvectorFormula exponent = bvmgr.extract(xToIeee, 30, 23); + final BitvectorFormula mantissa = bvmgr.extract(xToIeee, 22, 0); + final BooleanFormula additionalConstraint = xToIeeeAndAddConstraint.getBooleanFormula(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isInfinity(x), + bmgr.or( + bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x7f80_0000L)), + bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0xff80_0000L)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isZero(x), + bmgr.or( + bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x0000_0000)), + bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x8000_0000L)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isNormal(x), + bmgr.and( + bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0))), + bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1))))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isSubnormal(x), + bmgr.and( + bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0)), + bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0))))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isNaN(x), + bmgr.and( + bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1)), + bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0))))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isNegative(x), + bmgr.and( + bmgr.not(fpmgr.isNaN(x)), + bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1)))))) + .isTautological(); + } + + // Same as specialValueFunctionsFrom64Bits2, but with fallback toIeeeBitvector() implementation. + @Test + public void specialValueFunctionsFrom64Bits2ToIeeeFallback() + throws SolverException, InterruptedException { + requireBitvectors(); + + final FloatingPointFormula x = fpmgr.makeVariable("x64", doublePrecType); + BitvectorFormulaAndBooleanFormula xToIeeeAndAddConstraint = + fpmgr.toIeeeBitvector(x, "bvConst_x"); + BitvectorFormula xToIeee = xToIeeeAndAddConstraint.getBitvectorFormula(); + final BitvectorFormula signBit = bvmgr.extract(xToIeee, 63, 63); + final BitvectorFormula exponent = bvmgr.extract(xToIeee, 62, 52); + final BitvectorFormula mantissa = bvmgr.extract(xToIeee, 51, 0); + final BooleanFormula additionalConstraint = xToIeeeAndAddConstraint.getBooleanFormula(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isInfinity(x), + bmgr.or( + bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x7ff0_0000_0000_0000L)), + bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0xfff0_0000_0000_0000L)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isZero(x), + bmgr.or( + bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x0000_0000_0000_0000L)), + bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x8000_0000_0000_0000L)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isNormal(x), + bmgr.and( + bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0))), + bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, -1))))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isSubnormal(x), + bmgr.and( + bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0)), + bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(52, 0))))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isNaN(x), + bmgr.and( + bvmgr.equal(exponent, bvmgr.makeBitvector(11, -1)), + bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(52, 0))))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + additionalConstraint, + bmgr.equivalence( + fpmgr.isNegative(x), + bmgr.and( + bmgr.not(fpmgr.isNaN(x)), + bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1)))))) + .isTautological(); + } + + @Test + public void floatingPointSinglePrecisionSizeWithBvTransformationTest() { + requireBitvectors(); + int fpSinglePrecSize = 32; + var bv32 = bvmgr.makeBitvector(fpSinglePrecSize, 0); + assertThat(bvmgr.getLength(bv32)).isEqualTo(fpSinglePrecSize); + + requireFloats(); + var singlePrec = FormulaType.getSinglePrecisionFloatingPointType(); + var fpSinglePrec = fpmgr.makeNumber(0.0, singlePrec); + // Sizes of the type and the actual term should match + assertThat(fpmgr.getExponentSize(fpSinglePrec)).isEqualTo(8); + assertThat(fpmgr.getMantissaSize(fpSinglePrec)).isEqualTo(24); + assertThat(singlePrec.getExponentSize()).isEqualTo(8); + assertThat(singlePrec.getMantissaSize()).isEqualTo(24); + assertThat(singlePrec.getExponentSize() + singlePrec.getMantissaSize()) + .isEqualTo(fpSinglePrecSize); + assertThat(singlePrec.getTotalSize()) + .isEqualTo(singlePrec.getExponentSize() + singlePrec.getMantissaSize()); + + assertThat(bvmgr.getLength(fpmgr.toIeeeBitvector(fpSinglePrec, "dummy1").getBitvectorFormula())) + .isEqualTo(fpSinglePrecSize); + assertThat( + bvmgr.getLength( + fpmgr + .toIeeeBitvector(fpSinglePrec, "dummy2", ImmutableMap.of()) + .getBitvectorFormula())) + .isEqualTo(fpSinglePrecSize); + + if (solverSupportsNativeFPToBitvector()) { + assertThat(bvmgr.getLength(fpmgr.toIeeeBitvector(fpSinglePrec))).isEqualTo(fpSinglePrecSize); + } + } + @Test public void specialDoubles() throws SolverException, InterruptedException { assertThatFormula(fpmgr.assignment(fpmgr.makeNumber(Double.NaN, singlePrecType), nan)) @@ -982,7 +1170,7 @@ public void fpTraversalWithRoundingMode() { @Test public void fpIeeeConversionTypes() { - requireFPToBitvector(); + requireNativeFPToBitvector(); FloatingPointFormula var = fpmgr.makeVariable("var", singlePrecType); assertThat(mgr.getFormulaType(fpmgr.toIeeeBitvector(var))) @@ -991,7 +1179,7 @@ public void fpIeeeConversionTypes() { @Test public void fpIeeeConversion() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); FloatingPointFormula var = fpmgr.makeVariable("var", singlePrecType); assertThatFormula( @@ -1002,7 +1190,7 @@ public void fpIeeeConversion() throws SolverException, InterruptedException { @Test public void ieeeFpConversion() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); BitvectorFormula var = bvmgr.makeBitvector(32, 123456789); assertThatFormula( @@ -1072,7 +1260,7 @@ public void checkIeeeBv2FpConversion64() throws SolverException, InterruptedExce @Test public void checkIeeeFp2BvConversion32() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); proveForAll( // makeBV(value.bits) == fromFP(makeFP(value.float)) @@ -1085,7 +1273,7 @@ public void checkIeeeFp2BvConversion32() throws SolverException, InterruptedExce @Test public void checkIeeeFp2BvConversion64() throws SolverException, InterruptedException { - requireFPToBitvector(); + requireNativeFPToBitvector(); proveForAll( // makeBV(value.bits) == fromFP(makeFP(value.float)) diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index e96c7b39f1..fcea391cf9 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -242,18 +242,33 @@ 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(); } } + 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() From 353b12c81e1523274ddaca640ae8ac423470a7fd Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 18:11:50 +0200 Subject: [PATCH 15/39] Add public API to get exponent and mantissa size in FloatingPointFormulaManager (based on solver return) --- .../java_smt/api/FloatingPointFormulaManager.java | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index 4c36ed7f62..7dc24c3d82 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -528,4 +528,15 @@ FloatingPointFormula multiply( * */ BooleanFormula isNegative(FloatingPointFormula number); + + /** + * Returns the size of the mantissa (also called a coefficient or significant), including the + * sign bit, for the given {@link FloatingPointFormula}. + */ + int getMantissaSize(FloatingPointFormula number); + + /** + * Returns the size of the exponent for the given {@link FloatingPointFormula}. + */ + int getExponentSize(FloatingPointFormula number); } From 6c554d0a592cba05c940a89e8333857ed1777e94 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 18:12:09 +0200 Subject: [PATCH 16/39] Add note about mantissa und sign bit in FloatingPointNumber.java --- src/org/sosy_lab/java_smt/api/FloatingPointNumber.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index fe3c14b1ca..a9b2513aad 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -23,6 +23,7 @@ @AutoValue public abstract class FloatingPointNumber { + // Mantissas do not include the sign bit public static final int SINGLE_PRECISION_EXPONENT_SIZE = 8; public static final int SINGLE_PRECISION_MANTISSA_SIZE = 23; public static final int DOUBLE_PRECISION_EXPONENT_SIZE = 11; From 9603aa689b5c774374713c8885da9d83029cc83a Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 18:13:00 +0200 Subject: [PATCH 17/39] Remove accidental double implementation of bitvector width getter --- .../basicimpl/AbstractBitvectorFormulaManager.java | 6 ------ .../bitwuzla/BitwuzlaBitvectorFormulaManager.java | 5 ----- .../boolector/BoolectorBitvectorFormulaManager.java | 6 ------ .../solvers/cvc4/CVC4BitvectorFormulaManager.java | 9 --------- .../solvers/cvc5/CVC5BitvectorFormulaManager.java | 5 ----- .../mathsat5/Mathsat5BitvectorFormulaManager.java | 7 ------- .../princess/PrincessBitvectorFormulaManager.java | 5 ----- .../solvers/yices2/Yices2BitvectorFormulaManager.java | 7 ------- .../java_smt/solvers/z3/Z3BitvectorFormulaManager.java | 5 ----- 9 files changed, 55 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java index 8b8a1a58cf..46455c4829 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java @@ -439,10 +439,4 @@ protected TFormulaInfo distinctImpl(List pBits) { } return bmgr.andImpl(lst); } - - protected final int getBitvectorWidth(BitvectorFormula bitvector) { - return getBitvectorWidthImpl(extractInfo(bitvector)); - } - - protected abstract int getBitvectorWidthImpl(TFormulaInfo bitvector); } diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBitvectorFormulaManager.java index d83b2208a3..e99b5cbe16 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBitvectorFormulaManager.java @@ -203,9 +203,4 @@ protected Term extend(Term pNumber, int pExtensionBits, boolean pSigned) { return termManager.mk_term(Kind.BV_ZERO_EXTEND, pNumber, pExtensionBits); } } - - @Override - protected int getBitvectorWidthImpl(Term pNumber) { - return pNumber.sort().bv_size(); - } } diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java index 23e5fa58ea..b44c9af19d 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java @@ -12,7 +12,6 @@ import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_and; import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_concat; import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_eq; -import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_get_width; import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_mul; import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_neg; import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_not; @@ -236,9 +235,4 @@ public Long extend(Long bitVec, int extensionBits, boolean signed) { return boolector_uext(btor, bitVec, extensionBits); } } - - @Override - protected int getBitvectorWidthImpl(Long bitvector) { - return boolector_get_width(btor, bitvector); - } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java index b59db60b30..89f672ab9e 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java @@ -8,8 +8,6 @@ package org.sosy_lab.java_smt.solvers.cvc4; -import static com.google.common.base.Preconditions.checkArgument; - import edu.stanford.CVC4.BitVector; import edu.stanford.CVC4.BitVectorExtract; import edu.stanford.CVC4.BitVectorRotateLeft; @@ -261,11 +259,4 @@ protected Expr distinctImpl(List pParam) { pParam.forEach(param::add); return exprManager.mkExpr(Kind.DISTINCT, param); } - - @Override - protected int getBitvectorWidthImpl(Expr bitvector) { - Type type = bitvector.getType(); - checkArgument(type.isBitVector()); - return (int) ((edu.stanford.CVC4.BitVectorType) type).getSize(); - } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java index f47d654678..83a9fae343 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java @@ -298,9 +298,4 @@ protected Term toIntegerFormulaImpl(Term pBv, boolean pSigned) { protected Term distinctImpl(List pParam) { return termManager.mkTerm(Kind.DISTINCT, pParam.toArray(new Term[0])); } - - @Override - protected int getBitvectorWidthImpl(Term bitvector) { - return bitvector.getSort().getBitVectorSize(); - } } diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5BitvectorFormulaManager.java index 4adcbc6d27..5ccde4d21f 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5BitvectorFormulaManager.java @@ -8,7 +8,6 @@ package org.sosy_lab.java_smt.solvers.mathsat5; -import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_bv_type_size; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_bv_and; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_bv_ashr; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_bv_concat; @@ -42,7 +41,6 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_int_from_ubv; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_int_to_bv; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_term_ite; -import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_get_type; import java.math.BigInteger; import java.util.function.Function; @@ -80,11 +78,6 @@ public Long extend(Long pNumber, int pExtensionBits, boolean pSigned) { } } - @Override - protected int getBitvectorWidthImpl(Long bitvector) { - return msat_get_bv_type_size(mathsatEnv, msat_term_get_type(bitvector)); - } - @Override public Long makeBitvectorImpl(int pLength, long pI) { int i = (int) pI; diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java index d6a5dc5376..4ea9cf3191 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java @@ -200,9 +200,4 @@ protected IExpression extend(IExpression pNumber, int pExtensionBits, boolean pS return ModuloArithmetic$.MODULE$.zero_extend(pExtensionBits, (ITerm) pNumber); } } - - @Override - protected int getBitvectorWidthImpl(IExpression bitvector) { - return bitvector.length(); - } } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java index 6cabc088a6..3df71f8a8a 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java @@ -34,13 +34,11 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bvsmod; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bvsrem; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bvsub; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bvtype_size; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bvxor2; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_parse_bvbin; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_rotate_left; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_rotate_right; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_sign_extend; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_of_term; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_zero_extend; import com.google.common.base.Preconditions; @@ -229,11 +227,6 @@ protected Integer extend(Integer pNumber, int pExtensionBits, boolean pSigned) { } } - @Override - protected int getBitvectorWidthImpl(Integer bitvector) { - return yices_bvtype_size(yices_type_of_term(bitvector)); - } - @Override protected Integer makeBitvectorImpl(int pLength, Integer pFormula) { throw new UnsupportedOperationException( diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3BitvectorFormulaManager.java index 969efe4539..940a58918d 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3BitvectorFormulaManager.java @@ -202,9 +202,4 @@ public Long greaterOrEquals(Long pNumber1, Long pNumber2, boolean signed) { protected Long distinctImpl(List pBits) { return Native.mkDistinct(z3context, pBits.size(), Longs.toArray(pBits)); } - - @Override - protected int getBitvectorWidthImpl(Long bitvector) { - return Native.getBvSortSize(z3context, Native.getSort(z3context, bitvector)); - } } From 1f09a650ea67d34f115510b2298944ea20126581 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 18:14:14 +0200 Subject: [PATCH 18/39] Use existing BV size getter + make size getters for FP public + extend text for native toIeeeBitvector() in AbstractFloatingPointFormulaManager --- .../AbstractFloatingPointFormulaManager.java | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 9ed60f5eb6..27e25edfa3 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -272,7 +272,10 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula pNumber) { protected TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber) { throw new UnsupportedOperationException( "The chosen solver does not support transforming " - + "FloatingPointFormula to IEEE bitvectors. Try using "); // TODO: finish + + "FloatingPointFormula to IEEE bitvectors. Try using the fallback " + + "methods toIeeeBitvector" + + "(FloatingPointFormula, String) and/or " + + "toIeeeBitvector(FloatingPointFormula, String, Map)"); } @Override @@ -292,9 +295,10 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( BitvectorFormula bvFormula = bvMgr.makeVariable(mantissaSize + exponentSize, bitvectorConstantName); + // When building new Fp types, we don't include the sign bit FloatingPointFormula fromIeeeBitvector = fromIeeeBitvector( - bvFormula, FloatingPointType.getFloatingPointType(exponentSize, mantissaSize)); + bvFormula, FloatingPointType.getFloatingPointType(exponentSize, mantissaSize - 1)); // assignment() allows a value to be NaN etc. // Note: All fp.to_* functions are unspecified for NaN and infinity input values in the @@ -328,7 +332,7 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( BitvectorFormula bvTerm = entry.getValue(); checkArgument( - bvMgr.getBitvectorWidth(bvTerm) == bvMgr.getBitvectorWidth(bvFormula), + bvMgr.getLength(bvTerm) == bvMgr.getLength(bvFormula), "The size of the bitvector terms used as mapped values needs to be equal to the size of" + " the bitvector returned by this method"); @@ -341,13 +345,15 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( return BitvectorFormulaAndBooleanFormula.of(toIeeeBv, additionalConstraint); } - protected int getMantissaSize(FloatingPointFormula f) { + @Override + public int getMantissaSize(FloatingPointFormula f) { return getMantissaSizeImpl(extractInfo(f)); } protected abstract int getMantissaSizeImpl(TFormulaInfo f); - protected int getExponentSize(FloatingPointFormula f) { + @Override + public int getExponentSize(FloatingPointFormula f) { return getExponentSizeImpl(extractInfo(f)); } From 43ee2a0a59879baa5ad84bda0a8916c00d6c9e2b Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 18:14:46 +0200 Subject: [PATCH 19/39] Extend delegate FloatingPointManagers with FP size methods --- .../DebuggingFloatingPointFormulaManager.java | 14 ++++++++++++++ .../StatisticsFloatingPointFormulaManager.java | 12 ++++++++++++ .../SynchronizedFloatingPointFormulaManager.java | 14 ++++++++++++++ 3 files changed, 40 insertions(+) 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 644d575497..1293288dfb 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java @@ -523,4 +523,18 @@ public BooleanFormula isNegative(FloatingPointFormula number) { debugging.addFormulaTerm(result); return result; } + + @Override + public int getMantissaSize(FloatingPointFormula number) { + debugging.assertThreadLocal(); + debugging.assertFormulaInContext(number); + return delegate.getMantissaSize(number); + } + + @Override + public int getExponentSize(FloatingPointFormula number) { + debugging.assertThreadLocal(); + debugging.assertFormulaInContext(number); + return delegate.getExponentSize(number); + } } diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java index 80441e2d01..28e439062a 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java @@ -369,4 +369,16 @@ public BooleanFormula isNegative(FloatingPointFormula pNumber) { stats.fpOperations.getAndIncrement(); return delegate.isNegative(pNumber); } + + @Override + public int getMantissaSize(FloatingPointFormula pNumber) { + stats.fpOperations.getAndIncrement(); + return delegate.getMantissaSize(pNumber); + } + + @Override + public int getExponentSize(FloatingPointFormula pNumber) { + stats.fpOperations.getAndIncrement(); + return delegate.getExponentSize(pNumber); + } } diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java index d589a119c3..42dc3ebbd0 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java @@ -420,4 +420,18 @@ public BooleanFormula isNegative(FloatingPointFormula pNumber) { return delegate.isNegative(pNumber); } } + + @Override + public int getMantissaSize(FloatingPointFormula pNumber) { + synchronized (sync) { + return delegate.getMantissaSize(pNumber); + } + } + + @Override + public int getExponentSize(FloatingPointFormula pNumber) { + synchronized (sync) { + return delegate.getExponentSize(pNumber); + } + } } From a27cc7ece18692d6678852fecaa38c7ddd39b12e Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:36:08 +0200 Subject: [PATCH 20/39] Rename new FloatingPointFormulaManager method getMantissaSize() to getMantissaSizeWithSignBit() + --- .../java_smt/api/FloatingPointFormulaManager.java | 13 ++++++------- .../AbstractFloatingPointFormulaManager.java | 4 ++-- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index 7dc24c3d82..391a78210b 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -101,7 +101,8 @@ default FloatingPointFormula makeNumber(FloatingPointNumber number) { number.getExponent(), number.getMantissa(), number.getMathSign(), - getFloatingPointType(number.getExponentSize(), number.getMantissaSize())); + getFloatingPointType( + number.getExponentSize(), number.getMantissaSize())); } /** @@ -530,13 +531,11 @@ FloatingPointFormula multiply( BooleanFormula isNegative(FloatingPointFormula number); /** - * Returns the size of the mantissa (also called a coefficient or significant), including the - * sign bit, for the given {@link FloatingPointFormula}. + * Returns the size of the mantissa (also called a coefficient or significant), including the sign + * bit, for the given {@link FloatingPointFormula}. */ - int getMantissaSize(FloatingPointFormula number); + int getMantissaSizeWithSignBit(FloatingPointFormula number); - /** - * Returns the size of the exponent for the given {@link FloatingPointFormula}. - */ + /** Returns the size of the exponent for the given {@link FloatingPointFormula}. */ int getExponentSize(FloatingPointFormula number); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 27e25edfa3..5a27eaa4b7 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -290,7 +290,7 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( String bitvectorConstantName, Map specialFPConstantHandling) { - int mantissaSize = getMantissaSize(f); + int mantissaSize = getMantissaSizeWithSignBit(f); int exponentSize = getExponentSize(f); BitvectorFormula bvFormula = bvMgr.makeVariable(mantissaSize + exponentSize, bitvectorConstantName); @@ -346,7 +346,7 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( } @Override - public int getMantissaSize(FloatingPointFormula f) { + public int getMantissaSizeWithSignBit(FloatingPointFormula f) { return getMantissaSizeImpl(extractInfo(f)); } From de90781ce232de0ae490ee397cdf546786a8d2c5 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:37:43 +0200 Subject: [PATCH 21/39] Add JavaDoc to FormulaType.FloatingPointType and add methods to get the type/mantissa with/without sign bit and add sign bit to toString and toSMTLIBString representations --- .../sosy_lab/java_smt/api/FormulaType.java | 86 +++++++++++++++++-- 1 file changed, 80 insertions(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index d5beea79cc..a6a705a8f6 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -205,14 +205,61 @@ public String toSMTLIBString() { } } - public static FloatingPointType getFloatingPointType(int exponentSize, int mantissaSize) { - return new FloatingPointType(exponentSize, mantissaSize); + /** + * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes. + * The mantissa size is expected to not include the sign bit. + * + * @param exponentSize size of the exponent for the base of the floating-point + * @param mantissaSizeWithoutSignBit size of the mantissa (also called a coefficient or + * significant), excluding the sign bit. + * @return the newly constructed {@link FloatingPointType}. + */ + // TODO: mark as soon to be deprecated + public static FloatingPointType getFloatingPointType( + int exponentSize, int mantissaSizeWithoutSignBit) { + return new FloatingPointType(exponentSize, mantissaSizeWithoutSignBit); + } + + /** + * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes. + * The mantissa size is expected to not include the sign bit. + * + * @param exponentSize size of the exponent for the base of the floating-point + * @param mantissaSizeWithoutSignBit size of the mantissa (also called a coefficient or + * significant), excluding the sign bit. + * @return the newly constructed {@link FloatingPointType}. + */ + public static FloatingPointType getFloatingPointTypeWithoutSignBit( + int exponentSize, int mantissaSizeWithoutSignBit) { + return new FloatingPointType(exponentSize, mantissaSizeWithoutSignBit); + } + + /** + * Constructs a new IEEE-754 {@link FloatingPointType} with the given exponent and mantissa sizes. + * The mantissa size is expected to not include the sign bit. + * + * @param exponentSize size of the exponent for the base of the floating-point + * @param mantissaSizeWithSignBit size of the mantissa (also called a coefficient or significant), + * including the sign bit. + * @return the newly constructed {@link FloatingPointType}. + */ + public static FloatingPointType getFloatingPointTypeWithSignBit( + int exponentSize, int mantissaSizeWithSignBit) { + return new FloatingPointType(exponentSize, mantissaSizeWithSignBit); } + /** + * @return single precision {@link FloatingPointType} with exponent sized 8, and mantissa sized 24 + * (including the sign bit). + */ public static FloatingPointType getSinglePrecisionFloatingPointType() { return FloatingPointType.SINGLE_PRECISION_FP_TYPE; } + /** + * @return double precision {@link FloatingPointType} with exponent sized 11, and mantissa sized + * 53 (including the sign bit). + */ public static FloatingPointType getDoublePrecisionFloatingPointType() { return FloatingPointType.DOUBLE_PRECISION_FP_TYPE; } @@ -226,6 +273,8 @@ public static final class FloatingPointType extends FormulaType"; + return "FloatingPoint"; } @Override public String toSMTLIBString() { - return "(_ FloatingPoint " + exponentSize + " " + mantissaSize + ")"; + return "(_ FloatingPoint " + exponentSize + " " + getMantissaSizeWithSignBit() + ")"; } } @@ -478,7 +552,7 @@ public static FormulaType fromString(String t) { } else if (t.startsWith("FloatingPoint<")) { // FloatingPoint List exman = Splitter.on(',').limit(2).splitToList(t.substring(14, t.length() - 1)); - return FormulaType.getFloatingPointType( + return FormulaType.getFloatingPointTypeWithoutSignBit( Integer.parseInt(exman.get(0).substring(4)), Integer.parseInt(exman.get(1).substring(5))); } else if (t.startsWith("Bitvector<")) { // Bitvector<32> From b652b7fa048da0dd1402faffc571dc8b63b18afc Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:39:27 +0200 Subject: [PATCH 22/39] Add JavaDoc to FloatingPointNumber and add methods to get the mantissa with/without sign bit and use those as far as possible to make the code unambiguous for mantissas --- .../java_smt/api/FloatingPointNumber.java | 49 ++++++++++++++----- 1 file changed, 36 insertions(+), 13 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java index a9b2513aad..6c750e3701 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -81,8 +81,29 @@ public final boolean getSign() { public abstract int getExponentSize(); + /** + * Returns the size of the mantissa (also called a coefficient or significant), excluding the sign + * bit. + */ + // TODO: mark as soon to be deprecated public abstract int getMantissaSize(); + /** + * Returns the size of the mantissa (also called a coefficient or significant), excluding the sign + * bit. + */ + public int getMantissaSizeWithoutSignBit() { + return getMantissaSize(); + } + + /** + * Returns the size of the mantissa (also called a coefficient or significant), including the sign + * bit. + */ + public int getMantissaSizeWithSignBit() { + return getMantissaSize() + 1; + } + /** * Get a floating-point number with the given sign, exponent, and mantissa. * @@ -93,7 +114,7 @@ public final boolean getSign() { * @param mantissa the mantissa of the floating-point number, given as unsigned (not negative) * number without hidden bit * @param exponentSize the (maximum) size of the exponent in bits - * @param mantissaSize the (maximum) size of the mantissa in bits + * @param mantissaSize the (maximum) size of the mantissa in bits (excluding the sign bit) * @see #of(Sign, BigInteger, BigInteger, int, int) */ @Deprecated( @@ -120,7 +141,7 @@ public static FloatingPointNumber of( * @param mantissa the mantissa of the floating-point number, given as unsigned (not negative) * number without hidden bit * @param exponentSize the (maximum) size of the exponent in bits - * @param mantissaSize the (maximum) size of the mantissa in bits + * @param mantissaSize the (maximum) size of the mantissa in bits (excluding the sign bit) */ public static FloatingPointNumber of( Sign sign, BigInteger exponent, BigInteger mantissa, int exponentSize, int mantissaSize) { @@ -137,7 +158,7 @@ public static FloatingPointNumber of( * @param bits the bit-representation of the floating-point number, consisting of sign bit, * exponent (without bias) and mantissa (without hidden bit) in this exact ordering * @param exponentSize the size of the exponent in bits - * @param mantissaSize the size of the mantissa in bits + * @param mantissaSize the size of the mantissa in bits (excluding the sign bit) */ public static FloatingPointNumber of(String bits, int exponentSize, int mantissaSize) { Preconditions.checkArgument(0 < exponentSize); @@ -160,24 +181,26 @@ public static FloatingPointNumber of(String bits, int exponentSize, int mantissa /** * Returns true if this floating-point number is an IEEE-754-2008 single precision type with 32 - * bits length consisting of an 8 bit exponent, a 23 bit mantissa and a single sign bit. + * bits length consisting of an 8 bit exponent, a 24 bit mantissa (including the sign bit). * * @return true for IEEE-754 single precision type, false otherwise. */ public boolean isIEEE754SinglePrecision() { + // Mantissa does not include the sign bit return getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE - && getMantissaSize() == SINGLE_PRECISION_MANTISSA_SIZE; + && getMantissaSizeWithoutSignBit() == SINGLE_PRECISION_MANTISSA_SIZE; } /** * Returns true if this floating-point number is an IEEE-754-2008 double precision type with 64 - * bits length consisting of an 11 bit exponent, a 52 bit mantissa and a single sign bit. + * bits length consisting of an 11 bit exponent, a 53 bit mantissa (including the sign bit). * * @return true for IEEE-754 double precision type, false otherwise. */ public boolean isIEEE754DoublePrecision() { + // Mantissa does not include the sign bit return getExponentSize() == DOUBLE_PRECISION_EXPONENT_SIZE - && getMantissaSize() == DOUBLE_PRECISION_MANTISSA_SIZE; + && getMantissaSizeWithoutSignBit() == DOUBLE_PRECISION_MANTISSA_SIZE; } /** compute a representation as Java-based float value, if possible. */ @@ -205,18 +228,18 @@ public double doubleValue() { } private BitSet getBits() { - var mantissaSize = getMantissaSize(); + var mantissaSizeWithoutSign = getMantissaSizeWithoutSignBit(); var exponentSize = getExponentSize(); var mantissa = getMantissa(); var exponent = getExponent(); - var bits = new BitSet(1 + exponentSize + mantissaSize); + var bits = new BitSet(exponentSize + mantissaSizeWithoutSign + 1); if (getMathSign().isNegative()) { - bits.set(exponentSize + mantissaSize); // if negative, set first bit to 1 + bits.set(exponentSize + mantissaSizeWithoutSign); // if negative, set first bit to 1 } for (int i = 0; i < exponentSize; i++) { - bits.set(mantissaSize + i, exponent.testBit(i)); + bits.set(mantissaSizeWithoutSign + i, exponent.testBit(i)); } - for (int i = 0; i < mantissaSize; i++) { + for (int i = 0; i < mantissaSizeWithoutSign; i++) { bits.set(i, mantissa.testBit(i)); } return bits; @@ -228,7 +251,7 @@ private BitSet getBits() { */ @Override public final String toString() { - var length = 1 + getExponentSize() + getMantissaSize(); + var length = getExponentSize() + getMantissaSizeWithSignBit(); var str = new StringBuilder(length); var bits = getBits(); for (int i = 0; i < length; i++) { From 11926f1aa9b3943afbbe616098795fd0d5a79b69 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:40:10 +0200 Subject: [PATCH 23/39] Add suppression of return value to test method checking native FP to IEEE BV method availability --- src/org/sosy_lab/java_smt/test/SolverBasedTest0.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index fcea391cf9..85cd1c1574 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -259,6 +259,7 @@ protected final void requireNativeFPToBitvector() { } } + @SuppressWarnings("CheckReturnValue") protected final boolean solverSupportsNativeFPToBitvector() { requireFloats(); try { From 17227ac0fe066b42f0fc3112f97a9b9a3bde6468 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:41:07 +0200 Subject: [PATCH 24/39] Extend FP tests with new mantissa API to be unambiguous about the sign bit and add some assertions for mantissa/exponent --- .../test/FloatingPointFormulaManagerTest.java | 75 +++++++++++++------ 1 file changed, 53 insertions(+), 22 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index ce125f5fdd..06ac5be9b0 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -103,7 +103,7 @@ public void testSpecialNumberIdentity() { @Test public void floatingPointType() { - FloatingPointType type = FormulaType.getFloatingPointType(23, 42); + FloatingPointType type = FormulaType.getFloatingPointTypeWithoutSignBit(23, 42); FloatingPointFormula var = fpmgr.makeVariable("x", type); FloatingPointType result = (FloatingPointType) mgr.getFormulaType(var); @@ -111,8 +111,8 @@ public void floatingPointType() { .that(result.getExponentSize()) .isEqualTo(type.getExponentSize()); assertWithMessage("mantissa size") - .that(result.getMantissaSize()) - .isEqualTo(type.getMantissaSize()); + .that(result.getMantissaSizeWithSignBit()) + .isEqualTo(type.getMantissaSizeWithSignBit()); } @Test @@ -286,7 +286,7 @@ public void fpRemainderNormal() throws SolverException, InterruptedException { for (FloatingPointType prec : new FloatingPointType[] { - singlePrecType, doublePrecType, FormulaType.getFloatingPointType(5, 6), + singlePrecType, doublePrecType, FormulaType.getFloatingPointTypeWithoutSignBit(5, 6), }) { final FloatingPointFormula numFive = fpmgr.makeNumber(5, prec); @@ -310,7 +310,7 @@ public void fpRemainderSpecial() throws SolverException, InterruptedException { for (FloatingPointType prec : new FloatingPointType[] { - singlePrecType, doublePrecType, FormulaType.getFloatingPointType(5, 6), + singlePrecType, doublePrecType, FormulaType.getFloatingPointTypeWithoutSignBit(5, 6), }) { final FloatingPointFormula num = fpmgr.makeNumber(42, prec); @@ -691,13 +691,13 @@ public void floatingPointSinglePrecisionSizeWithBvTransformationTest() { var fpSinglePrec = fpmgr.makeNumber(0.0, singlePrec); // Sizes of the type and the actual term should match assertThat(fpmgr.getExponentSize(fpSinglePrec)).isEqualTo(8); - assertThat(fpmgr.getMantissaSize(fpSinglePrec)).isEqualTo(24); + assertThat(fpmgr.getMantissaSizeWithSignBit(fpSinglePrec)).isEqualTo(24); assertThat(singlePrec.getExponentSize()).isEqualTo(8); - assertThat(singlePrec.getMantissaSize()).isEqualTo(24); - assertThat(singlePrec.getExponentSize() + singlePrec.getMantissaSize()) + assertThat(singlePrec.getMantissaSizeWithSignBit()).isEqualTo(24); + assertThat(singlePrec.getExponentSize() + singlePrec.getMantissaSizeWithSignBit()) .isEqualTo(fpSinglePrecSize); assertThat(singlePrec.getTotalSize()) - .isEqualTo(singlePrec.getExponentSize() + singlePrec.getMantissaSize()); + .isEqualTo(singlePrec.getExponentSize() + singlePrec.getMantissaSizeWithSignBit()); assertThat(bvmgr.getLength(fpmgr.toIeeeBitvector(fpSinglePrec, "dummy1").getBitvectorFormula())) .isEqualTo(fpSinglePrecSize); @@ -750,7 +750,7 @@ public void numberConstants() throws SolverException, InterruptedException { checkEqualityOfNumberConstantsFor(3.4028234663852886e+38, doublePrecType); // check unequality for large types - FloatingPointType nearDouble = FormulaType.getFloatingPointType(12, 52); + FloatingPointType nearDouble = FormulaType.getFloatingPointTypeWithoutSignBit(12, 52); FloatingPointFormula h1 = fpmgr.makeNumber(BigDecimal.TEN.pow(309).multiply(BigDecimal.valueOf(1.0001)), nearDouble); FloatingPointFormula h2 = @@ -758,7 +758,7 @@ public void numberConstants() throws SolverException, InterruptedException { assertThatFormula(fpmgr.equalWithFPSemantics(h1, h2)).isUnsatisfiable(); // check equality for short types - FloatingPointType smallType = FormulaType.getFloatingPointType(4, 4); + FloatingPointType smallType = FormulaType.getFloatingPointTypeWithoutSignBit(4, 4); FloatingPointFormula i1 = fpmgr.makeNumber(BigDecimal.TEN.pow(50).multiply(BigDecimal.valueOf(1.001)), smallType); FloatingPointFormula i2 = @@ -787,7 +787,7 @@ public void numberConstants() throws SolverException, InterruptedException { assertThatFormula(fpmgr.isNegative(ni2)).isTautological(); // check equality for short types - FloatingPointType smallType2 = FormulaType.getFloatingPointType(4, 4); + FloatingPointType smallType2 = FormulaType.getFloatingPointTypeWithoutSignBit(4, 4); FloatingPointFormula j1 = fpmgr.makeNumber(BigDecimal.TEN.pow(500).multiply(BigDecimal.valueOf(1.001)), smallType2); FloatingPointFormula j2 = @@ -818,7 +818,7 @@ public void numberConstants() throws SolverException, InterruptedException { // Z3 supports at least FloatingPointType(15, 112). Larger types seem to be rounded. if (!ImmutableSet.of(Solvers.Z3, Solvers.CVC4).contains(solver)) { // check unequality for very large types - FloatingPointType largeType = FormulaType.getFloatingPointType(100, 100); + FloatingPointType largeType = FormulaType.getFloatingPointTypeWithoutSignBit(100, 100); FloatingPointFormula k1 = fpmgr.makeNumber(BigDecimal.TEN.pow(200).multiply(BigDecimal.valueOf(1.001)), largeType); FloatingPointFormula k2 = @@ -855,7 +855,7 @@ public void numberConstantsNearInf() throws SolverException, InterruptedExceptio private void checkNearInf(int mantissa, int exponent, long value) throws SolverException, InterruptedException { - FloatingPointType type = FormulaType.getFloatingPointType(exponent, mantissa); + FloatingPointType type = FormulaType.getFloatingPointTypeWithoutSignBit(exponent, mantissa); FloatingPointFormula fp1 = fpmgr.makeNumber(BigDecimal.valueOf(value), type); assertThatFormula(fpmgr.isInfinity(fp1)).isTautological(); FloatingPointFormula fp2 = fpmgr.makeNumber(BigDecimal.valueOf(value - 1), type); @@ -890,7 +890,7 @@ public void numberConstantsNearMinusInf() throws SolverException, InterruptedExc private void checkNearMinusInf(int mantissa, int exponent, long value) throws SolverException, InterruptedException { - FloatingPointType type = FormulaType.getFloatingPointType(exponent, mantissa); + FloatingPointType type = FormulaType.getFloatingPointTypeWithoutSignBit(exponent, mantissa); FloatingPointFormula fp1 = fpmgr.makeNumber(BigDecimal.valueOf(value), type); assertThatFormula(fpmgr.isInfinity(fp1)).isTautological(); FloatingPointFormula fp2 = fpmgr.makeNumber(BigDecimal.valueOf(value + 1), type); @@ -1429,9 +1429,16 @@ public void fpModelValue() throws SolverException, InterruptedException { Float.MIN_VALUE, Float.MIN_NORMAL, }) { - FloatingPointNumber fiveValue = model.evaluate(fpmgr.makeNumber(f, singlePrecType)); - assertThat(fiveValue.floatValue()).isEqualTo(f); - assertThat(fiveValue.doubleValue()).isEqualTo((double) f); + var constFpNum = fpmgr.makeNumber(f, singlePrecType); + assertThat(fpmgr.getMantissaSizeWithSignBit(constFpNum)) + .isEqualTo(singlePrecType.getMantissaSizeWithSignBit()); + FloatingPointNumber fpValue = model.evaluate(constFpNum); + assertThat(fpValue.getMantissaSizeWithSignBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithSignBit()); + assertThat(fpValue.getMantissaSizeWithoutSignBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithSignBit() - 1); + assertThat(fpValue.floatValue()).isEqualTo(f); + assertThat(fpValue.doubleValue()).isEqualTo((double) f); } } } @@ -1480,16 +1487,28 @@ public void fpFrom32BitPattern() throws SolverException, InterruptedException { final FloatingPointFormula fpFromBv = fpmgr.makeNumber( BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, singlePrecType); + assertThat(fpmgr.getMantissaSizeWithSignBit(fpFromBv) + fpmgr.getExponentSize(fpFromBv)) + .isEqualTo(singlePrecType.getTotalSize()); final FloatingPointNumber fpNumber = FloatingPointNumber.of( sign, BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), singlePrecType.getExponentSize(), - singlePrecType.getMantissaSize()); + singlePrecType.getMantissaSizeWithoutSignBit()); + assertThat(fpNumber.getMantissaSizeWithSignBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithSignBit()); + assertThat(fpNumber.getMantissaSizeWithoutSignBit()) + .isEqualTo(singlePrecType.getMantissaSizeWithSignBit() - 1); final FloatingPointFormula fp1 = fpmgr.makeNumber(fpNumber); + assertThat(fpmgr.getMantissaSizeWithSignBit(fp1) + fpmgr.getExponentSize(fp1)) + .isEqualTo(singlePrecType.getTotalSize()); final FloatingPointFormula fp2 = fpmgr.makeNumber(pFloat, singlePrecType); - return bmgr.and(fpmgr.assignment(fpFromBv, fp1), fpmgr.assignment(fpFromBv, fp2)); + assertThat(fpmgr.getMantissaSizeWithSignBit(fp2) + fpmgr.getExponentSize(fp2)) + .isEqualTo(singlePrecType.getTotalSize()); + final BooleanFormula assignment1 = fpmgr.assignment(fpFromBv, fp1); + final BooleanFormula assignment2 = fpmgr.assignment(fpFromBv, fp2); + return bmgr.and(assignment1, assignment2); }); } @@ -1506,16 +1525,28 @@ public void fpFrom64BitPattern() throws SolverException, InterruptedException { final FloatingPointFormula fpFromBv = fpmgr.makeNumber( BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), sign, doublePrecType); + assertThat(fpmgr.getMantissaSizeWithSignBit(fpFromBv) + fpmgr.getExponentSize(fpFromBv)) + .isEqualTo(doublePrecType.getTotalSize()); final FloatingPointNumber fpNumber = FloatingPointNumber.of( sign, BigInteger.valueOf(exponent), BigInteger.valueOf(mantissa), doublePrecType.getExponentSize(), - doublePrecType.getMantissaSize()); + doublePrecType.getMantissaSizeWithoutSignBit()); + assertThat(fpNumber.getMantissaSizeWithSignBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithSignBit()); + assertThat(fpNumber.getMantissaSizeWithoutSignBit()) + .isEqualTo(doublePrecType.getMantissaSizeWithSignBit() - 1); final FloatingPointFormula fp1 = fpmgr.makeNumber(fpNumber); + assertThat(fpmgr.getMantissaSizeWithSignBit(fp1) + fpmgr.getExponentSize(fp1)) + .isEqualTo(doublePrecType.getTotalSize()); final FloatingPointFormula fp2 = fpmgr.makeNumber(pDouble, doublePrecType); - return bmgr.and(fpmgr.assignment(fpFromBv, fp1), fpmgr.assignment(fpFromBv, fp2)); + assertThat(fpmgr.getMantissaSizeWithSignBit(fp2) + fpmgr.getExponentSize(fp2)) + .isEqualTo(doublePrecType.getTotalSize()); + final BooleanFormula assignment1 = fpmgr.assignment(fpFromBv, fp1); + final BooleanFormula assignment2 = fpmgr.assignment(fpFromBv, fp2); + return bmgr.and(assignment1, assignment2); }); } From 31ffd6833fd52fe15f06b2df21efd146123fecee Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:41:33 +0200 Subject: [PATCH 25/39] Extend FloatingPointFormulaManager with new mantissa API to be unambiguous about the sign bit --- .../sosy_lab/java_smt/api/FloatingPointFormulaManager.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index 391a78210b..91a9d7d6bc 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -8,7 +8,7 @@ package org.sosy_lab.java_smt.api; -import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointType; +import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointTypeWithoutSignBit; import java.math.BigDecimal; import java.math.BigInteger; @@ -101,8 +101,8 @@ default FloatingPointFormula makeNumber(FloatingPointNumber number) { number.getExponent(), number.getMantissa(), number.getMathSign(), - getFloatingPointType( - number.getExponentSize(), number.getMantissaSize())); + getFloatingPointTypeWithoutSignBit( + number.getExponentSize(), number.getMantissaSizeWithoutSignBit())); } /** From 3cc3a9940944619fb4942710c1d12e7aa4d5f96d Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:42:18 +0200 Subject: [PATCH 26/39] Rename getMantissaSize() in FloatingPointFormulaManager delegates with new mantissa API --- .../debugging/DebuggingFloatingPointFormulaManager.java | 4 ++-- .../statistics/StatisticsFloatingPointFormulaManager.java | 4 ++-- .../synchronize/SynchronizedFloatingPointFormulaManager.java | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) 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 1293288dfb..cc0ca778a1 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java @@ -525,10 +525,10 @@ public BooleanFormula isNegative(FloatingPointFormula number) { } @Override - public int getMantissaSize(FloatingPointFormula number) { + public int getMantissaSizeWithSignBit(FloatingPointFormula number) { debugging.assertThreadLocal(); debugging.assertFormulaInContext(number); - return delegate.getMantissaSize(number); + return delegate.getMantissaSizeWithSignBit(number); } @Override 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 28e439062a..e0756d53f8 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java @@ -371,9 +371,9 @@ public BooleanFormula isNegative(FloatingPointFormula pNumber) { } @Override - public int getMantissaSize(FloatingPointFormula pNumber) { + public int getMantissaSizeWithSignBit(FloatingPointFormula pNumber) { stats.fpOperations.getAndIncrement(); - return delegate.getMantissaSize(pNumber); + return delegate.getMantissaSizeWithSignBit(pNumber); } @Override 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 42dc3ebbd0..4b7b7b3a63 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java @@ -422,9 +422,9 @@ public BooleanFormula isNegative(FloatingPointFormula pNumber) { } @Override - public int getMantissaSize(FloatingPointFormula pNumber) { + public int getMantissaSizeWithSignBit(FloatingPointFormula pNumber) { synchronized (sync) { - return delegate.getMantissaSize(pNumber); + return delegate.getMantissaSizeWithSignBit(pNumber); } } From cd3a9c1db5d662f17abf19cb3446a06bd7746ed7 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:43:00 +0200 Subject: [PATCH 27/39] Update Bitwuzla with new unambiguous FP mantissa size getters --- .../solvers/bitwuzla/BitwuzlaFloatingPointManager.java | 10 +++++----- .../solvers/bitwuzla/BitwuzlaFormulaCreator.java | 6 +++--- 2 files changed, 8 insertions(+), 8 deletions(-) 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 1e87dd1258..a68dcc25fe 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java @@ -83,7 +83,7 @@ protected Term makeNumberImpl( Sort expSort = termManager.mk_bv_sort(type.getExponentSize()); Term expTerm = termManager.mk_bv_value(expSort, exponent.toString(2)); - Sort mantissaSort = termManager.mk_bv_sort(type.getMantissaSize()); + Sort mantissaSort = termManager.mk_bv_sort(type.getMantissaSizeWithoutSignBit()); Term mantissaTerm = termManager.mk_bv_value(mantissaSort, mantissa.toString(2)); return termManager.mk_fp_value(signTerm, expTerm, mantissaTerm); @@ -133,7 +133,7 @@ protected Term castToImpl( pRoundingMode, pNumber, targetType.getExponentSize(), - targetType.getMantissaSize() + 1); + targetType.getMantissaSizeWithSignBit()); } else if (pTargetType.isBitvectorType()) { FormulaType.BitvectorType targetType = (FormulaType.BitvectorType) pTargetType; if (pSigned) { @@ -170,14 +170,14 @@ protected Term castFromImpl( roundingMode, pNumber, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithSignBit()); } else { return termManager.mk_term( Kind.FP_TO_FP_FROM_UBV, roundingMode, pNumber, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithSignBit()); } } else { @@ -192,7 +192,7 @@ protected Term fromIeeeBitvectorImpl(Term pNumber, FloatingPointType pTargetType Kind.FP_TO_FP_FROM_BV, pNumber, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithSignBit()); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index f946331319..fd5c82d284 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -102,7 +102,7 @@ assert getFormulaType(pTerm).isBitvectorType() // system instead use bitwuzla_mk_fp_value_from_real somehow or convert myself @Override public Sort getFloatingPointType(FloatingPointType type) { - return termManager.mk_fp_sort(type.getExponentSize(), type.getMantissaSize() + 1); + return termManager.mk_fp_sort(type.getExponentSize(), type.getMantissaSizeWithSignBit()); } @Override @@ -171,7 +171,7 @@ public FormulaType bitwuzlaSortToType(Sort pSort) { if (pSort.is_fp()) { int exponent = pSort.fp_exp_size(); int mantissa = pSort.fp_sig_size() - 1; - return FormulaType.getFloatingPointType(exponent, mantissa); + return FormulaType.getFloatingPointTypeWithoutSignBit(exponent, mantissa); } else if (pSort.is_bv()) { return FormulaType.getBitvectorTypeWithSize(pSort.bv_size()); } else if (pSort.is_array()) { @@ -380,7 +380,7 @@ public FormulaType getFormulaType(T pFormula) { } int exp = sort.fp_exp_size(); int man = sort.fp_sig_size() - 1; - return (FormulaType) FormulaType.getFloatingPointType(exp, man); + return (FormulaType) FormulaType.getFloatingPointTypeWithoutSignBit(exp, man); } else if (sort.is_rm()) { return (FormulaType) FormulaType.FloatingPointRoundingModeType; } From 2fbe5bd8f846f539c97dd2267db189b922cc8bfc Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:43:05 +0200 Subject: [PATCH 28/39] Update CVC4 with new unambiguous FP mantissa size getters --- .../cvc4/CVC4FloatingPointFormulaManager.java | 45 +++++++------------ .../solvers/cvc4/CVC4FormulaCreator.java | 6 +-- 2 files changed, 18 insertions(+), 33 deletions(-) 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 51985c8be7..de1a901b9b 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -12,13 +12,13 @@ import com.google.common.collect.ImmutableList; import edu.stanford.CVC4.BitVector; -import edu.stanford.CVC4.BitVectorExtract; import edu.stanford.CVC4.Expr; import edu.stanford.CVC4.ExprManager; import edu.stanford.CVC4.FloatingPoint; import edu.stanford.CVC4.FloatingPointConvertSort; import edu.stanford.CVC4.FloatingPointSize; import edu.stanford.CVC4.FloatingPointToFPFloatingPoint; +import edu.stanford.CVC4.FloatingPointToFPIEEEBitVector; import edu.stanford.CVC4.FloatingPointToFPSignedBitVector; import edu.stanford.CVC4.FloatingPointToFPUnsignedBitVector; import edu.stanford.CVC4.FloatingPointToSBV; @@ -57,8 +57,8 @@ protected CVC4FloatingPointFormulaManager( private static FloatingPointSize getFPSize(FloatingPointType pType) { long pExponentSize = pType.getExponentSize(); - long pMantissaSize = pType.getMantissaSize(); - return new FloatingPointSize(pExponentSize, pMantissaSize + 1); // plus sign bit + long pMantissaSize = pType.getMantissaSizeWithSignBit(); + return new FloatingPointSize(pExponentSize, pMantissaSize); } @Override @@ -94,11 +94,11 @@ protected Expr makeNumberImpl( BigInteger exponent, BigInteger mantissa, Sign sign, FloatingPointType type) { final String signStr = sign.isNegative() ? "1" : "0"; final String exponentStr = getBvRepresentation(exponent, type.getExponentSize()); - final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSize()); + final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSizeWithoutSignBit()); final String bitvecStr = signStr + exponentStr + mantissaStr; final BitVector bitVector = new BitVector(bitvecStr, 2); final FloatingPoint fp = - new FloatingPoint(type.getExponentSize(), type.getMantissaSize() + 1, bitVector); + new FloatingPoint(type.getExponentSize(), type.getMantissaSizeWithSignBit(), bitVector); return exprManager.mkConst(fp); } @@ -114,7 +114,7 @@ protected Expr makeNumberAndRound(String pN, FloatingPointType pType, Expr pRoun final Rational rat = toRational(pN); final BigInteger upperBound = - getBiggestNumberBeforeInf(pType.getMantissaSize(), pType.getExponentSize()); + getBiggestNumberBeforeInf(pType.getMantissaSizeWithSignBit(), pType.getExponentSize()); if (rat.greater(Rational.fromDecimal(upperBound.negate().toString())) && rat.less(Rational.fromDecimal(upperBound.toString()))) { @@ -223,7 +223,7 @@ protected Expr castFromImpl( } else if (formulaType.isBitvectorType()) { long pExponentSize = pTargetType.getExponentSize(); - long pMantissaSize = pTargetType.getMantissaSize(); + long pMantissaSize = pTargetType.getMantissaSizeWithSignBit(); FloatingPointSize fpSize = new FloatingPointSize(pExponentSize, pMantissaSize + 1); FloatingPointConvertSort fpConvert = new FloatingPointConvertSort(fpSize); final Expr op; @@ -363,27 +363,10 @@ protected Expr isNegative(Expr pParam) { @Override protected Expr fromIeeeBitvectorImpl(Expr bitvector, FloatingPointType pTargetType) { - int mantissaSize = pTargetType.getMantissaSize(); - int exponentSize = pTargetType.getExponentSize(); - int size = pTargetType.getTotalSize(); - assert size == mantissaSize + exponentSize + 1; - - Expr signExtract = exprManager.mkConst(new BitVectorExtract(size - 1, size - 1)); - Expr exponentExtract = exprManager.mkConst(new BitVectorExtract(size - 2, mantissaSize)); - Expr mantissaExtract = exprManager.mkConst(new BitVectorExtract(mantissaSize - 1, 0)); - - Expr sign = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, signExtract, bitvector); - Expr exponent = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, exponentExtract, bitvector); - Expr mantissa = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, mantissaExtract, bitvector); - - return exprManager.mkExpr(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa); - } - - @Override - protected Expr toIeeeBitvectorImpl(Expr pNumber) { - // TODO possible work-around: use a tmp-variable "TMP" and add an - // additional constraint "pNumer == fromIeeeBitvectorImpl(TMP)" for it in all use-cases. - throw new UnsupportedOperationException("FP to IEEE-BV is not supported"); + // This is just named weird, but the CVC4 doc say this is IEEE BV -> FP + FloatingPointConvertSort fpConvertSort = new FloatingPointConvertSort(getFPSize(pTargetType)); + Expr op = exprManager.mkConst(new FloatingPointToFPIEEEBitVector(fpConvertSort)); + return exprManager.mkExpr(op, bitvector); } @Override @@ -395,13 +378,15 @@ protected Expr round(Expr pFormula, FloatingPointRoundingMode pRoundingMode) { protected int getMantissaSizeImpl(Expr f) { Type type = f.getType(); checkArgument(type.isFloatingPoint()); - return (int) ((edu.stanford.CVC4.FloatingPointType) type).getSignificandSize(); + edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(type); + return (int) fpType.getSignificandSize(); } @Override protected int getExponentSizeImpl(Expr f) { Type type = f.getType(); checkArgument(type.isFloatingPoint()); - return (int) ((edu.stanford.CVC4.FloatingPointType) type).getExponentSize(); + edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(type); + return (int) fpType.getExponentSize(); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java index 23e7328956..1dac46d603 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -114,7 +114,7 @@ public Type getBitvectorType(int pBitwidth) { @Override public Type getFloatingPointType(FloatingPointType pType) { return exprManager.mkFloatingPointType( - pType.getExponentSize(), pType.getMantissaSize() + 1); // plus sign bit + pType.getExponentSize(), pType.getMantissaSizeWithSignBit()); } @Override @@ -154,7 +154,7 @@ public FormulaType getFormulaType(T pFormula) { t.isFloatingPoint(), "FloatingPointFormula with actual type %s: %s", t, pFormula); edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(t); return (FormulaType) - FormulaType.getFloatingPointType( + FormulaType.getFloatingPointTypeWithoutSignBit( (int) fpType.getExponentSize(), (int) fpType.getSignificandSize() - 1); // without sign bit @@ -182,7 +182,7 @@ private FormulaType getFormulaTypeFromTermType(Type t) { return FormulaType.getBitvectorTypeWithSize((int) new BitVectorType(t).getSize()); } else if (t.isFloatingPoint()) { edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(t); - return FormulaType.getFloatingPointType( + return FormulaType.getFloatingPointTypeWithoutSignBit( (int) fpType.getExponentSize(), (int) fpType.getSignificandSize() - 1); // without sign bit } else if (t.isRoundingMode()) { From b789362d143d30cc041048918f0c0cabc046cdec Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:43:09 +0200 Subject: [PATCH 29/39] Update CVC5 with new unambiguous FP mantissa size getters --- .../cvc5/CVC5FloatingPointFormulaManager.java | 69 +++++++------------ .../solvers/cvc5/CVC5FormulaCreator.java | 9 +-- 2 files changed, 30 insertions(+), 48 deletions(-) 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 b464130134..a678e7c499 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -81,7 +81,7 @@ protected Term makeNumberImpl( return termManager.mkFloatingPoint( termManager.mkBitVector(1, sign == Sign.NEGATIVE ? 1 : 0), termManager.mkBitVector(type.getExponentSize(), exponent.toString(16), 16), - termManager.mkBitVector(type.getMantissaSize(), mantissa.toString(16), 16)); + termManager.mkBitVector(type.getMantissaSizeWithoutSignBit(), mantissa.toString(16), 16)); } catch (CVC5ApiException e) { throw new IllegalArgumentException("You tried creating a invalid bitvector", e); @@ -93,7 +93,7 @@ protected Term makeNumberAndRound(String pN, FloatingPointType pType, Term pRoun try { if (isNegativeZero(Double.valueOf(pN))) { return termManager.mkFloatingPointNegZero( - pType.getExponentSize(), pType.getMantissaSize() + 1); + pType.getExponentSize(), pType.getMantissaSizeWithSignBit()); } } catch (CVC5ApiException | NumberFormatException e) { // ignore and fallback to floating point from rational numbers @@ -105,7 +105,7 @@ protected Term makeNumberAndRound(String pN, FloatingPointType pType, Term pRoun termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_REAL, pType.getExponentSize(), - pType.getMantissaSize() + 1); + pType.getMantissaSizeWithSignBit()); Term term = termManager.mkTerm(realToFp, pRoundingMode, termManager.mkReal(rationalValue.toString())); // simplification removes the cast from real to fp and return a bit-precise fp-number. @@ -114,8 +114,8 @@ protected Term makeNumberAndRound(String pN, FloatingPointType pType, Term pRoun throw new IllegalArgumentException( "You tried creating a invalid floating point with exponent size " + pType.getExponentSize() - + ", mantissa size " - + pType.getMantissaSize() + + ", mantissa size (including sign bit)" + + pType.getMantissaSizeWithSignBit() + " and value " + pN + ".", @@ -155,13 +155,13 @@ protected Term makeVariableImpl(String varName, FloatingPointType pType) { protected Term makePlusInfinityImpl(FloatingPointType pType) { try { return termManager.mkFloatingPointPosInf( - pType.getExponentSize(), pType.getMantissaSize() + 1); + pType.getExponentSize(), pType.getMantissaSizeWithSignBit()); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid positive floating point +infinity with exponent size " + pType.getExponentSize() + " and mantissa size " - + pType.getMantissaSize() + + pType.getMantissaSizeWithSignBit() + ".", e); } @@ -171,13 +171,13 @@ protected Term makePlusInfinityImpl(FloatingPointType pType) { protected Term makeMinusInfinityImpl(FloatingPointType pType) { try { return termManager.mkFloatingPointNegInf( - pType.getExponentSize(), pType.getMantissaSize() + 1); + pType.getExponentSize(), pType.getMantissaSizeWithSignBit()); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid negative floating point -infinity with exponent size " + pType.getExponentSize() + " and mantissa size " - + pType.getMantissaSize() + + pType.getMantissaSizeWithSignBit() + ".", e); } @@ -186,13 +186,14 @@ protected Term makeMinusInfinityImpl(FloatingPointType pType) { @Override protected Term makeNaNImpl(FloatingPointType pType) { try { - return termManager.mkFloatingPointNaN(pType.getExponentSize(), pType.getMantissaSize() + 1); + return termManager.mkFloatingPointNaN( + pType.getExponentSize(), pType.getMantissaSizeWithSignBit()); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid NaN with exponent size " + pType.getExponentSize() + " and mantissa size " - + pType.getMantissaSize() + + pType.getMantissaSizeWithSignBit() + ".", e); } @@ -208,7 +209,7 @@ protected Term castToImpl( termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_FP, ((FloatingPointType) pTargetType).getExponentSize(), - ((FloatingPointType) pTargetType).getMantissaSize() + 1); + ((FloatingPointType) pTargetType).getMantissaSizeWithSignBit()); return termManager.mkTerm(fpToFp, pRoundingMode, pNumber); } else if (pTargetType.isBitvectorType()) { @@ -249,7 +250,7 @@ protected Term castFromImpl( termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_REAL, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithSignBit()); return termManager.mkTerm(realToFp, pRoundingMode, pNumber); @@ -259,14 +260,14 @@ protected Term castFromImpl( termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_SBV, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithSignBit()); return termManager.mkTerm(realToSBv, pRoundingMode, pNumber); } else { Op realToUBv = termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_UBV, pTargetType.getExponentSize(), - pTargetType.getMantissaSize() + 1); + pTargetType.getMantissaSizeWithSignBit()); return termManager.mkTerm(realToUBv, pRoundingMode, pNumber); } @@ -281,7 +282,7 @@ protected Term castFromImpl( + " into a FloatingPoint with exponent size " + pTargetType.getExponentSize() + " and mantissa size " - + pTargetType.getMantissaSize() + + pTargetType.getMantissaSizeWithSignBit() + ".", e); } @@ -412,36 +413,16 @@ protected Term isNegative(Term pParam) { @Override protected Term fromIeeeBitvectorImpl(Term bitvector, FloatingPointType pTargetType) { - int mantissaSize = pTargetType.getMantissaSize(); - int exponentSize = pTargetType.getExponentSize(); - int size = pTargetType.getTotalSize(); - assert size == mantissaSize + exponentSize + 1; - - Op signExtract; - Op exponentExtract; - Op mantissaExtract; try { - signExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 1, size - 1); - exponentExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 2, mantissaSize); - mantissaExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, mantissaSize - 1, 0); - } catch (CVC5ApiException e) { - throw new IllegalArgumentException( - "You tried creating a invalid bitvector extract in term " + bitvector + ".", e); + return termManager.mkTerm( + termManager.mkOp( + Kind.FLOATINGPOINT_TO_FP_FROM_IEEE_BV, + pTargetType.getExponentSize(), + pTargetType.getMantissaSizeWithSignBit()), + bitvector); + } catch (CVC5ApiException pE) { + throw new RuntimeException(pE); } - - Term sign = termManager.mkTerm(signExtract, bitvector); - Term exponent = termManager.mkTerm(exponentExtract, bitvector); - Term mantissa = termManager.mkTerm(mantissaExtract, bitvector); - - return termManager.mkTerm(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa); - } - - @Override - protected Term toIeeeBitvectorImpl(Term pNumber) { - // TODO possible work-around: use a tmp-variable "TMP" and add an - // additional constraint "pNumer == fromIeeeBitvectorImpl(TMP)" for it in all use-cases. - // --> This has to be done on user-side, not in JavaSMT. - throw new UnsupportedOperationException("FP to IEEE-BV is not supported"); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java index 946b6be069..381daa2a29 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -142,14 +142,15 @@ public Sort getBitvectorType(int pBitwidth) { public Sort getFloatingPointType(FloatingPointType pType) { try { // plus sign bit - return termManager.mkFloatingPointSort(pType.getExponentSize(), pType.getMantissaSize() + 1); + return termManager.mkFloatingPointSort( + pType.getExponentSize(), pType.getMantissaSizeWithSignBit()); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "Cannot create floatingpoint sort with exponent size " + pType.getExponentSize() + " and mantissa " - + pType.getMantissaSize() - + " (plus sign bit).", + + pType.getMantissaSizeWithSignBit() + + " (including sign bit).", e); } } @@ -223,7 +224,7 @@ private FormulaType getFormulaTypeFromTermType(Sort sort) { return FormulaType.getBitvectorTypeWithSize(sort.getBitVectorSize()); } else if (sort.isFloatingPoint()) { // CVC5 wants the sign bit as part of the mantissa. We add that manually in creation. - return FormulaType.getFloatingPointType( + return FormulaType.getFloatingPointTypeWithoutSignBit( sort.getFloatingPointExponentSize(), sort.getFloatingPointSignificandSize() - 1); } else if (sort.isRoundingMode()) { return FormulaType.FloatingPointRoundingModeType; From 2fc661c045f66b432e0a6b85493c73e023073bcd Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:43:16 +0200 Subject: [PATCH 30/39] Update MathSAT5 with new unambiguous FP mantissa size getters --- .../Mathsat5FloatingPointFormulaManager.java | 51 ++++++++++++++----- .../mathsat5/Mathsat5FormulaCreator.java | 17 ++++--- 2 files changed, 49 insertions(+), 19 deletions(-) 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 9b7d12a1f8..6c42a178a3 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java @@ -107,27 +107,41 @@ protected Long makeNumberImpl( BigInteger exponent, BigInteger mantissa, Sign sign, FloatingPointType type) { final String signStr = sign.isNegative() ? "1" : "0"; final String exponentStr = getBvRepresentation(exponent, type.getExponentSize()); - final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSize()); + // MathSAT5 expects the mantissa to not include the sign bit + final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSizeWithSignBit() - 1); final String bitvecForm = signStr + exponentStr + mantissaStr; final BigInteger bitvecValue = new BigInteger(bitvecForm, 2); return msat_make_fp_bits_number( - mathsatEnv, bitvecValue.toString(), type.getExponentSize(), type.getMantissaSize()); + mathsatEnv, + bitvecValue.toString(), + type.getExponentSize(), + type.getMantissaSizeWithSignBit() - 1); } @Override protected Long makeNumberAndRound(String pN, FloatingPointType pType, Long pRoundingMode) { try { if (isNegativeZero(Double.valueOf(pN))) { + // MathSAT5 expects the mantissa to not include the sign bit return msat_make_fp_neg( mathsatEnv, msat_make_fp_rat_number( - mathsatEnv, "0", pType.getExponentSize(), pType.getMantissaSize(), pRoundingMode)); + mathsatEnv, + "0", + pType.getExponentSize(), + pType.getMantissaSizeWithSignBit() - 1, + pRoundingMode)); } } catch (NumberFormatException e) { // ignore and fallback to floating point from rational numbers } + // MathSAT5 expects the mantissa to not include the sign bit return msat_make_fp_rat_number( - mathsatEnv, pN, pType.getExponentSize(), pType.getMantissaSize(), pRoundingMode); + mathsatEnv, + pN, + pType.getExponentSize(), + pType.getMantissaSizeWithoutSignBit(), + pRoundingMode); } @Override @@ -137,17 +151,23 @@ protected Long makeVariableImpl(String var, FloatingPointType type) { @Override protected Long makePlusInfinityImpl(FloatingPointType type) { - return msat_make_fp_plus_inf(mathsatEnv, type.getExponentSize(), type.getMantissaSize()); + // MathSAT5 expects the mantissa to not include the sign bit + return msat_make_fp_plus_inf( + mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithSignBit() - 1); } @Override protected Long makeMinusInfinityImpl(FloatingPointType type) { - return msat_make_fp_minus_inf(mathsatEnv, type.getExponentSize(), type.getMantissaSize()); + // MathSAT5 expects the mantissa to not include the sign bit + return msat_make_fp_minus_inf( + mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithSignBit() - 1); } @Override protected Long makeNaNImpl(FloatingPointType type) { - return msat_make_fp_nan(mathsatEnv, type.getExponentSize(), type.getMantissaSize()); + // MathSAT5 expects the mantissa to not include the sign bit + return msat_make_fp_nan( + mathsatEnv, type.getExponentSize(), type.getMantissaSizeWithSignBit() - 1); } @Override @@ -155,10 +175,11 @@ protected Long castToImpl( Long pNumber, boolean pSigned, FormulaType pTargetType, Long pRoundingMode) { if (pTargetType.isFloatingPointType()) { FormulaType.FloatingPointType targetType = (FormulaType.FloatingPointType) pTargetType; + // MathSAT5 expects the mantissa to not include the sign bit return msat_make_fp_cast( mathsatEnv, targetType.getExponentSize(), - targetType.getMantissaSize(), + targetType.getMantissaSizeWithSignBit() - 1, pRoundingMode, pNumber); @@ -184,18 +205,19 @@ protected Long castFromImpl( return castToImpl(pNumber, pSigned, pTargetType, pRoundingMode); } else if (formulaType.isBitvectorType()) { + // MathSAT5 expects the mantissa to not include the sign bit if (pSigned) { return msat_make_fp_from_sbv( mathsatEnv, pTargetType.getExponentSize(), - pTargetType.getMantissaSize(), + pTargetType.getMantissaSizeWithSignBit() - 1, pRoundingMode, pNumber); } else { return msat_make_fp_from_ubv( mathsatEnv, pTargetType.getExponentSize(), - pTargetType.getMantissaSize(), + pTargetType.getMantissaSizeWithSignBit() - 1, pRoundingMode, pNumber); } @@ -219,8 +241,12 @@ private Long genericCast(Long pNumber, FormulaType pTargetType) { @Override protected Long fromIeeeBitvectorImpl(Long pNumber, FloatingPointType pTargetType) { + // MathSAT5 expects the mantissa to not include the sign bit return Mathsat5NativeApi.msat_make_fp_from_ieeebv( - mathsatEnv, pTargetType.getExponentSize(), pTargetType.getMantissaSize(), pNumber); + mathsatEnv, + pTargetType.getExponentSize(), + pTargetType.getMantissaSizeWithSignBit() - 1, + pNumber); } @Override @@ -230,7 +256,8 @@ protected Long toIeeeBitvectorImpl(Long pNumber) { @Override protected int getMantissaSizeImpl(Long f) { - return msat_get_fp_type_mant_width(mathsatEnv, msat_term_get_type(f)); + // The mantissa includes the sign bit according to the SMTLib2 standard, but MathSAT does not. + return msat_get_fp_type_mant_width(mathsatEnv, msat_term_get_type(f)) + 1; } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java index ff35694c4a..d39b2f7d3b 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -213,7 +213,7 @@ private FormulaType getFormulaTypeFromTermType(Long type) { } else if (msat_is_bv_type(env, type)) { return FormulaType.getBitvectorTypeWithSize(msat_get_bv_type_size(env, type)); } else if (msat_is_fp_type(env, type)) { - return FormulaType.getFloatingPointType( + return FormulaType.getFloatingPointTypeWithoutSignBit( msat_get_fp_type_exp_width(env, type), msat_get_fp_type_mant_width(env, type)); } else if (msat_is_fp_roundingmode_type(env, type)) { return FormulaType.FloatingPointRoundingModeType; @@ -241,7 +241,9 @@ public Long getBitvectorType(int pBitwidth) { @Override public Long getFloatingPointType(FloatingPointType pType) { - return msat_get_fp_type(getEnv(), pType.getExponentSize(), pType.getMantissaSize()); + // MathSAT5 automatically adds 1 to the mantissa, as it expects it to be without it. + return msat_get_fp_type( + getEnv(), pType.getExponentSize(), pType.getMantissaSizeWithSignBit() - 1); } @SuppressWarnings("unchecked") @@ -575,13 +577,14 @@ private FloatingPointNumber parseFloatingPoint(String lTermRepresentation) { BigInteger bits = new BigInteger(matcher.group(1)); int expWidth = Integer.parseInt(matcher.group(2)); - int mantWidth = Integer.parseInt(matcher.group(3)); + // The term representation in MathSAT5 does not include the sign bit + int mantWidthWithoutSignBit = Integer.parseInt(matcher.group(3)); - Sign sign = Sign.of(bits.testBit(expWidth + mantWidth)); - BigInteger exponent = extractBitsFrom(bits, mantWidth, expWidth); - BigInteger mantissa = extractBitsFrom(bits, 0, mantWidth); + Sign sign = Sign.of(bits.testBit(expWidth + mantWidthWithoutSignBit)); + BigInteger exponent = extractBitsFrom(bits, mantWidthWithoutSignBit, expWidth); + BigInteger mantissa = extractBitsFrom(bits, 0, mantWidthWithoutSignBit); - return FloatingPointNumber.of(sign, exponent, mantissa, expWidth, mantWidth); + return FloatingPointNumber.of(sign, exponent, mantissa, expWidth, mantWidthWithoutSignBit); } /** From 7b2b1de402631a211a79fc28051ea7b7179120e0 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:43:22 +0200 Subject: [PATCH 31/39] Update Z3 with new unambiguous FP mantissa size getters --- .../z3/Z3FloatingPointFormulaManager.java | 8 ++++--- .../java_smt/solvers/z3/Z3FormulaCreator.java | 21 ++++++++++++------- 2 files changed, 18 insertions(+), 11 deletions(-) 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 848ef2c15f..a992d5ee6d 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java @@ -20,7 +20,8 @@ class Z3FloatingPointFormulaManager extends AbstractFloatingPointFormulaManager { - private static final FloatingPointType highPrec = FormulaType.getFloatingPointType(15, 112); + private static final FloatingPointType highPrec = + FormulaType.getFloatingPointTypeWithoutSignBit(15, 112); private final long z3context; private final long roundingMode; @@ -81,7 +82,8 @@ protected Long makeNumberImpl( final long signSort = getFormulaCreator().getBitvectorType(1); final long expoSort = getFormulaCreator().getBitvectorType(type.getExponentSize()); - final long mantSort = getFormulaCreator().getBitvectorType(type.getMantissaSize()); + final long mantSort = + getFormulaCreator().getBitvectorType(type.getMantissaSizeWithoutSignBit()); final long signBv = Native.mkNumeral(z3context, sign.isNegative() ? "1" : "0", signSort); Native.incRef(z3context, signBv); @@ -102,7 +104,7 @@ protected Long makeNumberAndRound(String pN, FloatingPointType pType, Long pRoun // Z3 does not allow specifying a rounding mode for numerals, // so we create it first with a high precision and then round it down explicitly. if (pType.getExponentSize() <= highPrec.getExponentSize() - || pType.getMantissaSize() <= highPrec.getMantissaSize()) { + || pType.getMantissaSizeWithSignBit() <= highPrec.getMantissaSizeWithSignBit()) { long highPrecNumber = Native.mkNumeral(z3context, pN, mkFpaSort(highPrec)); Native.incRef(z3context, highPrecNumber); long smallPrecNumber = diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java index bde94b3e5f..890b5d8eac 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -241,7 +241,7 @@ public FormulaType getFormulaTypeFromSort(Long pSort) { return FormulaType.getArrayType( getFormulaTypeFromSort(domainSort), getFormulaTypeFromSort(rangeSort)); case Z3_FLOATING_POINT_SORT: - return FormulaType.getFloatingPointType( + return FormulaType.getFloatingPointTypeWithoutSignBit( Native.fpaGetEbits(z3context, pSort), Native.fpaGetSbits(z3context, pSort) - 1); case Z3_ROUNDING_MODE_SORT: return FormulaType.FloatingPointRoundingModeType; @@ -420,7 +420,8 @@ public Long getBitvectorType(int pBitwidth) { @Override public Long getFloatingPointType(FormulaType.FloatingPointType type) { - long fpSort = Native.mkFpaSort(getEnv(), type.getExponentSize(), type.getMantissaSize() + 1); + long fpSort = + Native.mkFpaSort(getEnv(), type.getExponentSize(), type.getMantissaSizeWithSignBit()); Native.incRef(getEnv(), Native.sortToAst(getEnv(), fpSort)); return fpSort; } @@ -967,7 +968,7 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p expo, mant, pType.getExponentSize(), - pType.getMantissaSize()); + pType.getMantissaSizeWithSignBit()); } else if (Native.fpaIsNumeralInf(environment, pValue)) { // Floating Point Inf uses: @@ -976,9 +977,11 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p // - "00..00" as mantissa. String sign = getSign(pValue).isNegative() ? "1" : "0"; return FloatingPointNumber.of( - sign + "1".repeat(pType.getExponentSize()) + "0".repeat(pType.getMantissaSize()), + sign + + "1".repeat(pType.getExponentSize()) + + "0".repeat(pType.getMantissaSizeWithSignBit()), pType.getExponentSize(), - pType.getMantissaSize()); + pType.getMantissaSizeWithSignBit()); } else if (Native.fpaIsNumeralNan(environment, pValue)) { // TODO We are underspecified here and choose several bits on our own. @@ -988,9 +991,11 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p // - "11..11" as exponent, // - an unspecified mantissa (we choose all "1"). return FloatingPointNumber.of( - "0" + "1".repeat(pType.getExponentSize()) + "1".repeat(pType.getMantissaSize()), + "0" + + "1".repeat(pType.getExponentSize()) + + "1".repeat(pType.getMantissaSizeWithSignBit()), pType.getExponentSize(), - pType.getMantissaSize()); + pType.getMantissaSizeWithSignBit()); } else { Sign sign = getSign(pValue); @@ -1003,7 +1008,7 @@ private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long p new BigInteger(exponent), new BigInteger(mantissa), pType.getExponentSize(), - pType.getMantissaSize()); + pType.getMantissaSizeWithSignBit()); } } From dbacf94074c396d25df6413edd6b296254e2f8a3 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 1 Sep 2025 19:43:31 +0200 Subject: [PATCH 32/39] Update SolverVisitorTest with new unambiguous FP mantissa size getters --- src/org/sosy_lab/java_smt/test/SolverVisitorTest.java | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 56b0200874..bd072cd759 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -477,13 +477,14 @@ public void floatConstantVisit() { Integer.toBinaryString(Float.floatToRawIntBits(entry.getKey().floatValue())), 32, '0')); - checkFloatConstant(FormulaType.getFloatingPointType(5, 10), entry.getKey(), entry.getValue()); + checkFloatConstant( + FormulaType.getFloatingPointTypeWithoutSignBit(5, 10), entry.getKey(), entry.getValue()); } } private void checkFloatConstant(FloatingPointType prec, double value, String bits) { FloatingPointNumber fp = - FloatingPointNumber.of(bits, prec.getExponentSize(), prec.getMantissaSize()); + FloatingPointNumber.of(bits, prec.getExponentSize(), prec.getMantissaSizeWithSignBit()); ConstantsVisitor visitor = new ConstantsVisitor(); mgr.visit(fpmgr.makeNumber(value, prec), visitor); @@ -580,7 +581,7 @@ public void fpToBvTest() { .that(solverToUse()) .isNoneOf(Solvers.CVC4, Solvers.CVC5); - var fpType = FormulaType.getFloatingPointType(5, 10); + var fpType = FormulaType.getFloatingPointTypeWithoutSignBit(5, 10); var visitor = new DefaultFormulaVisitor() { @Override From 2d278901dde1dc1a300261652b991f6edd8a4abe Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 08:24:08 +0200 Subject: [PATCH 33/39] Use mantissa size without sign bit when building special numbers to check against in FP toIeeeBitvector() --- .../java_smt/basicimpl/AbstractFloatingPointFormulaManager.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 5a27eaa4b7..1d59d347fb 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -307,7 +307,7 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( // Build special numbers so that we can compare them in the map FloatingPointType precision = - FloatingPointType.getFloatingPointType(exponentSize, mantissaSize); + FloatingPointType.getFloatingPointType(exponentSize, mantissaSize - 1); Set specialNumbers = ImmutableSet.of( makeNaN(precision), makePlusInfinity(precision), makeMinusInfinity(precision)); From 15efd20b5a621f4fa4f6af4f0aa6e75cfda3d4ae Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 08:52:02 +0200 Subject: [PATCH 34/39] Fix off-by-one FP mantissa bug when casting BV to FP --- .../java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 de1a901b9b..24163e9ea0 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -224,7 +224,7 @@ protected Expr castFromImpl( } else if (formulaType.isBitvectorType()) { long pExponentSize = pTargetType.getExponentSize(); long pMantissaSize = pTargetType.getMantissaSizeWithSignBit(); - FloatingPointSize fpSize = new FloatingPointSize(pExponentSize, pMantissaSize + 1); + FloatingPointSize fpSize = new FloatingPointSize(pExponentSize, pMantissaSize); FloatingPointConvertSort fpConvert = new FloatingPointConvertSort(fpSize); final Expr op; if (pSigned) { From ba26c93089551bdbe6509f781a3014ca0165512b Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 08:52:52 +0200 Subject: [PATCH 35/39] Extend FP tests with new tests for toIeeeBitvector() fallback testing the re-mapping of special values --- .../test/FloatingPointFormulaManagerTest.java | 154 ++++++++++++++++++ 1 file changed, 154 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 06ac5be9b0..00b1af6168 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -679,6 +679,160 @@ public void specialValueFunctionsFrom64Bits2ToIeeeFallback() .isTautological(); } + // Same as specialValueFunctionsFrom32Bits2, but with fallback toIeeeBitvector() implementation + // with mapped special numbers. + @Test + public void specialValueFunctionsFrom32Bits2ToIeeeFallbackAlternatives() + throws SolverException, InterruptedException { + requireBitvectors(); + + final FloatingPointFormula x = fpmgr.makeVariable("x32", singlePrecType); + var nanBv = bvmgr.makeBitvector(32, 0x0110_0000L); + var negInfBv = bvmgr.makeBitvector(32, 0x7f80_0000L); + var posInfBv = bvmgr.makeBitvector(32, 0xff80_0000L); + BitvectorFormulaAndBooleanFormula xToIeeeAndAddConstraint = + fpmgr.toIeeeBitvector( + x, + "bvConst_x", + ImmutableMap.of( + fpmgr.makePlusInfinity(singlePrecType), + posInfBv, + fpmgr.makeMinusInfinity(singlePrecType), + negInfBv, + fpmgr.makeNaN(singlePrecType), + nanBv)); + BitvectorFormula xToIeee = xToIeeeAndAddConstraint.getBitvectorFormula(); + final BitvectorFormula signBit = bvmgr.extract(xToIeee, 31, 31); + final BitvectorFormula exponent = bvmgr.extract(xToIeee, 30, 23); + final BitvectorFormula mantissa = bvmgr.extract(xToIeee, 22, 0); + final BooleanFormula additionalConstraint = xToIeeeAndAddConstraint.getBooleanFormula(); + + assertThatFormula( + bmgr.implication( + bmgr.and(additionalConstraint, bmgr.not(fpmgr.isNegative(x)), fpmgr.isInfinity(x)), + bvmgr.equal(xToIeee, posInfBv))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + bmgr.and(fpmgr.isNegative(x), fpmgr.isInfinity(x), additionalConstraint), + bvmgr.equal(xToIeee, negInfBv))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + bmgr.and(fpmgr.isNaN(x), additionalConstraint), bvmgr.equal(xToIeee, nanBv))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + bmgr.and(fpmgr.isZero(x), additionalConstraint), + bmgr.or( + bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x0000_0000)), + bvmgr.equal(xToIeee, bvmgr.makeBitvector(32, 0x8000_0000L))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + bmgr.and(fpmgr.isNormal(x), additionalConstraint), + bmgr.and( + bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0))), + bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + bmgr.and(fpmgr.isSubnormal(x), additionalConstraint), + bmgr.and( + bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0)), + bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + bmgr.and(fpmgr.isNegative(x), bmgr.not(fpmgr.isInfinity(x)), additionalConstraint), + bmgr.and( + bmgr.not(fpmgr.isNaN(x)), bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1))))) + .isTautological(); + } + + // Same as specialValueFunctionsFrom64Bits2, but with fallback toIeeeBitvector() implementation + // with redefinitions for special values. + @Test + public void specialValueFunctionsFrom64Bits2ToIeeeFallbackAlternatives() + throws SolverException, InterruptedException { + requireBitvectors(); + + final FloatingPointFormula x = fpmgr.makeVariable("x64", doublePrecType); + var nanBv = bvmgr.makeBitvector(64, 0x0111_1000_0000_0000L); + var negInfBv = bvmgr.makeBitvector(64, 0x0000_0000_0000_0001L); + var posInfBv = bvmgr.makeBitvector(64, 0x0000_0000_0000_0000L); + BitvectorFormulaAndBooleanFormula xToIeeeAndAddConstraint = + fpmgr.toIeeeBitvector( + x, + "bvConst_x", + ImmutableMap.of( + fpmgr.makePlusInfinity(doublePrecType), + posInfBv, + fpmgr.makeMinusInfinity(doublePrecType), + negInfBv, + fpmgr.makeNaN(doublePrecType), + nanBv)); + BitvectorFormula xToIeee = xToIeeeAndAddConstraint.getBitvectorFormula(); + final BitvectorFormula signBit = bvmgr.extract(xToIeee, 63, 63); + final BitvectorFormula exponent = bvmgr.extract(xToIeee, 62, 52); + final BitvectorFormula mantissa = bvmgr.extract(xToIeee, 51, 0); + final BooleanFormula additionalConstraint = xToIeeeAndAddConstraint.getBooleanFormula(); + + assertThatFormula( + bmgr.implication( + bmgr.and(bmgr.not(fpmgr.isNegative(x)), fpmgr.isInfinity(x), additionalConstraint), + bvmgr.equal(xToIeee, posInfBv))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + bmgr.and(fpmgr.isNegative(x), fpmgr.isInfinity(x), additionalConstraint), + bvmgr.equal(xToIeee, negInfBv))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + bmgr.and(fpmgr.isNaN(x), additionalConstraint), bvmgr.equal(xToIeee, nanBv))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + bmgr.and(fpmgr.isZero(x), additionalConstraint), + bmgr.or( + bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x0000_0000_0000_0000L)), + bvmgr.equal(xToIeee, bvmgr.makeBitvector(64, 0x8000_0000_0000_0000L))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + bmgr.and(fpmgr.isNormal(x), additionalConstraint), + bmgr.and( + bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0))), + bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, -1)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + bmgr.and(fpmgr.isSubnormal(x), additionalConstraint), + bmgr.and( + bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0)), + bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(52, 0)))))) + .isTautological(); + + assertThatFormula( + bmgr.implication( + bmgr.and(fpmgr.isNegative(x), bmgr.not(fpmgr.isInfinity(x)), additionalConstraint), + bmgr.and( + bmgr.not(fpmgr.isNaN(x)), bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1))))) + .isTautological(); + } + @Test public void floatingPointSinglePrecisionSizeWithBvTransformationTest() { requireBitvectors(); From 9c72a5b166e78f4e5e3dfab034e840fe5d35195e Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 09:07:28 +0200 Subject: [PATCH 36/39] Remove done TODO --- .../java_smt/basicimpl/AbstractFloatingPointFormulaManager.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 1d59d347fb..e9c99a92a2 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -338,8 +338,6 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( BooleanFormula assumption = assignment(fpConst, f); toIeeeBv = bMgr.ifThenElse(assumption, bvTerm, toIeeeBv); - // TODO: add tests for this and the other method, find out typical returns and add tests, - // then add to doc. } return BitvectorFormulaAndBooleanFormula.of(toIeeeBv, additionalConstraint); From 85a5b4e00a4fb9828a136b13bd52c27bae6a23c7 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 09:39:36 +0200 Subject: [PATCH 37/39] Rename internal method getMantissaSizeImpl() to getMantissaSizeWithSignBitImpl() to reduce ambiguity + improve name of variable --- .../AbstractFloatingPointFormulaManager.java | 13 +++++++------ .../bitwuzla/BitwuzlaFloatingPointManager.java | 2 +- .../cvc4/CVC4FloatingPointFormulaManager.java | 2 +- .../cvc5/CVC5FloatingPointFormulaManager.java | 2 +- .../Mathsat5FloatingPointFormulaManager.java | 2 +- .../solvers/z3/Z3FloatingPointFormulaManager.java | 2 +- 6 files changed, 12 insertions(+), 11 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index e9c99a92a2..09fb9b03b5 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -290,15 +290,16 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( String bitvectorConstantName, Map specialFPConstantHandling) { - int mantissaSize = getMantissaSizeWithSignBit(f); + int mantissaSizeWithSignBit = getMantissaSizeWithSignBit(f); int exponentSize = getExponentSize(f); BitvectorFormula bvFormula = - bvMgr.makeVariable(mantissaSize + exponentSize, bitvectorConstantName); + bvMgr.makeVariable(mantissaSizeWithSignBit + exponentSize, bitvectorConstantName); // When building new Fp types, we don't include the sign bit FloatingPointFormula fromIeeeBitvector = fromIeeeBitvector( - bvFormula, FloatingPointType.getFloatingPointType(exponentSize, mantissaSize - 1)); + bvFormula, + FloatingPointType.getFloatingPointType(exponentSize, mantissaSizeWithSignBit - 1)); // assignment() allows a value to be NaN etc. // Note: All fp.to_* functions are unspecified for NaN and infinity input values in the @@ -307,7 +308,7 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( // Build special numbers so that we can compare them in the map FloatingPointType precision = - FloatingPointType.getFloatingPointType(exponentSize, mantissaSize - 1); + FloatingPointType.getFloatingPointType(exponentSize, mantissaSizeWithSignBit - 1); Set specialNumbers = ImmutableSet.of( makeNaN(precision), makePlusInfinity(precision), makeMinusInfinity(precision)); @@ -345,10 +346,10 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( @Override public int getMantissaSizeWithSignBit(FloatingPointFormula f) { - return getMantissaSizeImpl(extractInfo(f)); + return getMantissaSizeWithSignBitImpl(extractInfo(f)); } - protected abstract int getMantissaSizeImpl(TFormulaInfo f); + protected abstract int getMantissaSizeWithSignBitImpl(TFormulaInfo f); @Override public int getExponentSize(FloatingPointFormula f) { 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 a68dcc25fe..f5ee0f07f7 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java @@ -148,7 +148,7 @@ protected Term castToImpl( } @Override - protected int getMantissaSizeImpl(Term fp) { + protected int getMantissaSizeWithSignBitImpl(Term fp) { return fp.sort().fp_sig_size(); } 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 24163e9ea0..b62f959500 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -375,7 +375,7 @@ protected Expr round(Expr pFormula, FloatingPointRoundingMode pRoundingMode) { } @Override - protected int getMantissaSizeImpl(Expr f) { + protected int getMantissaSizeWithSignBitImpl(Expr f) { Type type = f.getType(); checkArgument(type.isFloatingPoint()); edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(type); 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 a678e7c499..f226e74da6 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -431,7 +431,7 @@ protected Term round(Term pFormula, FloatingPointRoundingMode pRoundingMode) { } @Override - protected int getMantissaSizeImpl(Term f) { + protected int getMantissaSizeWithSignBitImpl(Term f) { Sort sort = f.getSort(); return sort.getFloatingPointSignificandSize(); } 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 6c42a178a3..2eb6eb2750 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java @@ -255,7 +255,7 @@ protected Long toIeeeBitvectorImpl(Long pNumber) { } @Override - protected int getMantissaSizeImpl(Long f) { + protected int getMantissaSizeWithSignBitImpl(Long f) { // The mantissa includes the sign bit according to the SMTLib2 standard, but MathSAT does not. return msat_get_fp_type_mant_width(mathsatEnv, msat_term_get_type(f)) + 1; } 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 a992d5ee6d..d7714c401f 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java @@ -321,7 +321,7 @@ protected Long round(Long pFormula, FloatingPointRoundingMode pRoundingMode) { } @Override - protected int getMantissaSizeImpl(Long f) { + protected int getMantissaSizeWithSignBitImpl(Long f) { return Native.fpaGetEbits(z3context, Native.getSort(z3context, f)); } From edf028d7cbcb1d145c97868750522e087dc09b1a Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 10:38:43 +0200 Subject: [PATCH 38/39] Apply checkstyle and ECJ suggestions --- src/org/sosy_lab/java_smt/api/FormulaType.java | 2 +- .../basicimpl/AbstractFloatingPointFormulaManager.java | 10 ++++++---- .../solvers/cvc5/CVC5FloatingPointFormulaManager.java | 4 ++-- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index a6a705a8f6..da62759ba3 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -287,7 +287,7 @@ public boolean isFloatingPointType() { return true; } - /** Returns the size of the exponent */ + /** Returns the size of the exponent. */ public int getExponentSize() { return exponentSize; } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 09fb9b03b5..7f50e334d3 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -10,6 +10,7 @@ import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; +import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointType; import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName; import com.google.common.collect.ImmutableMap; @@ -269,6 +270,7 @@ public BitvectorFormula toIeeeBitvector(FloatingPointFormula pNumber) { return getFormulaCreator().encapsulateBitvector(toIeeeBitvectorImpl(extractInfo(pNumber))); } + @SuppressWarnings("unused") protected TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber) { throw new UnsupportedOperationException( "The chosen solver does not support transforming " @@ -299,7 +301,7 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( FloatingPointFormula fromIeeeBitvector = fromIeeeBitvector( bvFormula, - FloatingPointType.getFloatingPointType(exponentSize, mantissaSizeWithSignBit - 1)); + getFloatingPointType(exponentSize, mantissaSizeWithSignBit - 1)); // assignment() allows a value to be NaN etc. // Note: All fp.to_* functions are unspecified for NaN and infinity input values in the @@ -308,7 +310,7 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( // Build special numbers so that we can compare them in the map FloatingPointType precision = - FloatingPointType.getFloatingPointType(exponentSize, mantissaSizeWithSignBit - 1); + getFloatingPointType(exponentSize, mantissaSizeWithSignBit - 1); Set specialNumbers = ImmutableSet.of( makeNaN(precision), makePlusInfinity(precision), makeMinusInfinity(precision)); @@ -620,7 +622,7 @@ protected static String getBvRepresentation(BigInteger integer, int size) { return String.copyValueOf(values); } - public static class BitvectorFormulaAndBooleanFormula { + public static final class BitvectorFormulaAndBooleanFormula { private final BitvectorFormula bitvectorFormula; private final BooleanFormula booleanFormula; @@ -630,7 +632,7 @@ private BitvectorFormulaAndBooleanFormula( booleanFormula = checkNotNull(pBooleanFormula); } - protected static BitvectorFormulaAndBooleanFormula of( + private static BitvectorFormulaAndBooleanFormula of( BitvectorFormula pBitvectorFormula, BooleanFormula pBooleanFormula) { return new BitvectorFormulaAndBooleanFormula(pBitvectorFormula, pBooleanFormula); } 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 f226e74da6..ca4c2f339a 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -412,14 +412,14 @@ protected Term isNegative(Term pParam) { } @Override - protected Term fromIeeeBitvectorImpl(Term bitvector, FloatingPointType pTargetType) { + protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetType) { try { return termManager.mkTerm( termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_IEEE_BV, pTargetType.getExponentSize(), pTargetType.getMantissaSizeWithSignBit()), - bitvector); + pBitvector); } catch (CVC5ApiException pE) { throw new RuntimeException(pE); } From 567e120f010d9c01955ae93216223419ecf21a0f Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 2 Sep 2025 13:05:13 +0200 Subject: [PATCH 39/39] Use type information for FP exponent and mantissa in toIeeeBitvector() instead of new implementation --- .../AbstractFloatingPointFormulaManager.java | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 7f50e334d3..2653558406 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -292,16 +292,17 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( String bitvectorConstantName, Map specialFPConstantHandling) { - int mantissaSizeWithSignBit = getMantissaSizeWithSignBit(f); - int exponentSize = getExponentSize(f); + FormulaType.FloatingPointType fpType = + (FloatingPointType) getFormulaCreator().getFormulaType(f); + int mantissaSizeWithSignBit = fpType.getMantissaSizeWithSignBit(); + int exponentSize = fpType.getExponentSize(); BitvectorFormula bvFormula = bvMgr.makeVariable(mantissaSizeWithSignBit + exponentSize, bitvectorConstantName); // When building new Fp types, we don't include the sign bit FloatingPointFormula fromIeeeBitvector = fromIeeeBitvector( - bvFormula, - getFloatingPointType(exponentSize, mantissaSizeWithSignBit - 1)); + bvFormula, getFloatingPointType(exponentSize, mantissaSizeWithSignBit - 1)); // assignment() allows a value to be NaN etc. // Note: All fp.to_* functions are unspecified for NaN and infinity input values in the @@ -309,8 +310,7 @@ public BitvectorFormulaAndBooleanFormula toIeeeBitvector( BooleanFormula additionalConstraint = assignment(fromIeeeBitvector, f); // Build special numbers so that we can compare them in the map - FloatingPointType precision = - getFloatingPointType(exponentSize, mantissaSizeWithSignBit - 1); + FloatingPointType precision = getFloatingPointType(exponentSize, mantissaSizeWithSignBit - 1); Set specialNumbers = ImmutableSet.of( makeNaN(precision), makePlusInfinity(precision), makeMinusInfinity(precision));