From e1f85a45ad88de60bbcdb91270b9c15f712e491d Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 25 Aug 2025 14:48:41 +0200 Subject: [PATCH 01/13] RoundingMode: Add new method makeRoundingMode() to the FloatingPointFormulaManager --- .../java_smt/api/FloatingPointFormulaManager.java | 3 +++ .../api/FloatingPointRoundingModeFormula.java | 7 +++++-- .../AbstractFloatingPointFormulaManager.java | 7 +++++++ .../sosy_lab/java_smt/basicimpl/FormulaCreator.java | 8 ++++++++ .../DebuggingFloatingPointFormulaManager.java | 10 ++++++++++ .../StatisticsFloatingPointFormulaManager.java | 8 ++++++++ .../SynchronizedFloatingPointFormulaManager.java | 9 +++++++++ .../solvers/bitwuzla/BitwuzlaFormulaCreator.java | 10 ++++++++++ .../java_smt/solvers/cvc4/CVC4FormulaCreator.java | 11 +++++++++++ .../java_smt/solvers/cvc5/CVC5FormulaCreator.java | 11 +++++++++++ .../solvers/mathsat5/Mathsat5FormulaCreator.java | 8 ++++++++ .../java_smt/solvers/z3/Z3FormulaCreator.java | 8 ++++++++ 12 files changed, 98 insertions(+), 2 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..63b6802f83 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -34,6 +34,9 @@ */ public interface FloatingPointFormulaManager { + /** Creates a formula for the given floating point rounding mode */ + FloatingPointRoundingModeFormula makeRoundingMode(FloatingPointRoundingMode pRoundingMode); + /** * Creates a floating point formula representing the given double value with the specified type. */ diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointRoundingModeFormula.java b/src/org/sosy_lab/java_smt/api/FloatingPointRoundingModeFormula.java index ead8fc04af..b9fb69fd73 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointRoundingModeFormula.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointRoundingModeFormula.java @@ -11,8 +11,11 @@ import com.google.errorprone.annotations.Immutable; /** - * Formula representing a rounding mode for floating-point operations. This is currently unused by - * the API but necessary for traversal of formulas with such terms. + * Formula representing a rounding mode for floating-point operations. + * + *

Rounding mode formulas are used by floating-point formulas to select the rounding mode for the + * operation. Use {@link FloatingPointFormulaManager#makeRoundingMode(FloatingPointRoundingMode)} to + * wrap a {@link org.sosy_lab.java_smt.api.FloatingPointRoundingMode} value inside a new formula. */ @Immutable public interface FloatingPointRoundingModeFormula extends Formula {} diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 47c847afe2..a653948bb3 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -22,6 +22,7 @@ import org.sosy_lab.java_smt.api.FloatingPointFormulaManager; import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign; import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; +import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula; 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; @@ -60,6 +61,12 @@ private TFormulaInfo getRoundingMode(FloatingPointRoundingMode pFloatingPointRou return roundingModes.computeIfAbsent(pFloatingPointRoundingMode, this::getRoundingModeImpl); } + @Override + public FloatingPointRoundingModeFormula makeRoundingMode( + FloatingPointRoundingMode pRoundingMode) { + return getFormulaCreator().encapsulateRoundingMode(getRoundingMode(pRoundingMode)); + } + protected FloatingPointFormula wrap(TFormulaInfo pTerm) { return getFormulaCreator().encapsulateFloatingPoint(pTerm); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java index 748fdd7b3b..cf383fde5a 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java @@ -160,6 +160,14 @@ protected FloatingPointFormula encapsulateFloatingPoint(TFormulaInfo pTerm) { return new FloatingPointFormulaImpl<>(pTerm); } + protected FloatingPointRoundingModeFormula encapsulateRoundingMode(TFormulaInfo pTerm) { + checkArgument( + getFormulaType(pTerm).isFloatingPointRoundingModeType(), + "Floatingpoint rounding mode formula has unexpected type: %s", + getFormulaType(pTerm)); + return new FloatingPointRoundingModeFormulaImpl<>(pTerm); + } + protected ArrayFormula encapsulateArray( TFormulaInfo pTerm, FormulaType pIndexType, FormulaType pElementType) { checkArgument( 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..817fb05ff1 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java @@ -17,6 +17,7 @@ import org.sosy_lab.java_smt.api.FloatingPointFormulaManager; import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign; import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; +import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula; 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; @@ -31,6 +32,15 @@ public class DebuggingFloatingPointFormulaManager implements FloatingPointFormul debugging = pDebugging; } + @Override + public FloatingPointRoundingModeFormula makeRoundingMode( + FloatingPointRoundingMode pRoundingMode) { + debugging.assertThreadLocal(); + FloatingPointRoundingModeFormula result = delegate.makeRoundingMode(pRoundingMode); + debugging.addFormulaTerm(result); + return result; + } + @Override public FloatingPointFormula makeNumber(double n, FloatingPointType type) { debugging.assertThreadLocal(); 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..f1669369c8 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java @@ -19,6 +19,7 @@ import org.sosy_lab.java_smt.api.FloatingPointFormulaManager; import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign; import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; +import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula; 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; @@ -34,6 +35,13 @@ class StatisticsFloatingPointFormulaManager implements FloatingPointFormulaManag stats = checkNotNull(pStats); } + @Override + public FloatingPointRoundingModeFormula makeRoundingMode( + FloatingPointRoundingMode pRoundingMode) { + stats.fpOperations.getAndIncrement(); + return delegate.makeRoundingMode(pRoundingMode); + } + @Override public FloatingPointFormula makeNumber(double pN, FloatingPointType pType) { stats.fpOperations.getAndIncrement(); 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..f0e1049c75 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java @@ -19,6 +19,7 @@ import org.sosy_lab.java_smt.api.FloatingPointFormulaManager; import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign; import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; +import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula; 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; @@ -35,6 +36,14 @@ class SynchronizedFloatingPointFormulaManager implements FloatingPointFormulaMan sync = checkNotNull(pSync); } + @Override + public FloatingPointRoundingModeFormula makeRoundingMode( + FloatingPointRoundingMode pRoundingMode) { + synchronized (sync) { + return delegate.makeRoundingMode(pRoundingMode); + } + } + @Override public FloatingPointFormula makeNumber(double pN, FloatingPointType pType) { synchronized (sync) { 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..75ec715e0f 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -33,6 +33,8 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.FloatingPointFormula; import org.sosy_lab.java_smt.api.FloatingPointNumber; +import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; +import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; @@ -131,6 +133,14 @@ assert getFormulaType(pTerm).isFloatingPointType() return new BitwuzlaFloatingPointFormula(pTerm); } + @Override + protected FloatingPointRoundingModeFormula encapsulateRoundingMode(Term pTerm) { + assert getFormulaType(pTerm).isFloatingPointRoundingModeType() + : String.format( + "%s is no FP rounding mode, but %s (%s)", pTerm, pTerm.sort(), getFormulaType(pTerm)); + return new BitwuzlaFloatingPointRoundingModeFormula(pTerm); + } + @Override @SuppressWarnings("MethodTypeParameterName") protected ArrayFormula encapsulateArray( 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..14cb8a3b5b 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -41,6 +41,8 @@ import org.sosy_lab.java_smt.api.FloatingPointFormula; import org.sosy_lab.java_smt.api.FloatingPointNumber; import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign; +import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; +import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; @@ -264,6 +266,15 @@ assert getFormulaType(pTerm).isFloatingPointType() return new CVC4FloatingPointFormula(pTerm); } + @Override + protected FloatingPointRoundingModeFormula encapsulateRoundingMode(Expr pTerm) { + assert getFormulaType(pTerm).isFloatingPointRoundingModeType() + : String.format( + "%s is no FP rounding mode, but %s (%s)", + pTerm, pTerm.getType(), getFormulaType(pTerm)); + return new CVC4FloatingPointRoundingModeFormula(pTerm); + } + @Override @SuppressWarnings("MethodTypeParameterName") protected ArrayFormula encapsulateArray( 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..f31e7bf027 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -44,6 +44,8 @@ import org.sosy_lab.java_smt.api.EnumerationFormula; import org.sosy_lab.java_smt.api.FloatingPointFormula; import org.sosy_lab.java_smt.api.FloatingPointNumber; +import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; +import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; @@ -315,6 +317,15 @@ assert getFormulaType(pTerm).isFloatingPointType() return new CVC5FloatingPointFormula(pTerm); } + @Override + protected FloatingPointRoundingModeFormula encapsulateRoundingMode(Term pTerm) { + assert getFormulaType(pTerm).isFloatingPointRoundingModeType() + : String.format( + "%s is no FP rounding mode, but %s (%s)", + pTerm, pTerm.getSort(), getFormulaType(pTerm)); + return new CVC5FloatingPointRoundingModeFormula(pTerm); + } + @Override @SuppressWarnings("MethodTypeParameterName") protected ArrayFormula encapsulateArray( 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..94eade2f53 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -127,6 +127,8 @@ import org.sosy_lab.java_smt.api.FloatingPointFormula; import org.sosy_lab.java_smt.api.FloatingPointNumber; import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign; +import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; +import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; @@ -291,6 +293,12 @@ protected FloatingPointFormula encapsulateFloatingPoint(Long pTerm) { return new Mathsat5FloatingPointFormula(pTerm); } + @Override + protected FloatingPointRoundingModeFormula encapsulateRoundingMode(Long pTerm) { + assert getFormulaType(pTerm).isFloatingPointRoundingModeType(); + return new Mathsat5FloatingPointRoundingModeFormula(pTerm); + } + @Override @SuppressWarnings("MethodTypeParameterName") protected ArrayFormula encapsulateArray( 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..cb7c8f769d 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -47,6 +47,7 @@ import org.sosy_lab.java_smt.api.FloatingPointNumber; import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign; import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; +import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; @@ -366,6 +367,13 @@ protected FloatingPointFormula encapsulateFloatingPoint(Long pTerm) { return storePhantomReference(new Z3FloatingPointFormula(getEnv(), pTerm), pTerm); } + @Override + protected FloatingPointRoundingModeFormula encapsulateRoundingMode(Long pTerm) { + assert getFormulaType(pTerm).isFloatingPointRoundingModeType(); + cleanupReferences(); + return storePhantomReference(new Z3FloatingPointRoundingModeFormula(getEnv(), pTerm), pTerm); + } + @Override protected StringFormula encapsulateString(Long pTerm) { assert getFormulaType(pTerm).isStringType() From 310cbf0da8794a4851bfbe68100c652d88dc99a2 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 25 Aug 2025 14:49:22 +0200 Subject: [PATCH 02/13] RoundingMode: Fix visitors for rounding mode formulas --- .../bitwuzla/BitwuzlaFormulaCreator.java | 14 ++++++++- .../solvers/cvc4/CVC4FormulaCreator.java | 24 ++++++++++++-- .../solvers/cvc5/CVC5FormulaCreator.java | 23 +++++++++++++- .../mathsat5/Mathsat5FormulaCreator.java | 31 +++++++++---------- 4 files changed, 71 insertions(+), 21 deletions(-) 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 75ec715e0f..f9fa6e30e7 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -594,7 +594,19 @@ public Object convertValue(Term term) { return term.to_bool(); } if (sort.is_rm()) { - return term.to_rm(); + if (term.is_rm_value_rna()) { + return FloatingPointRoundingMode.NEAREST_TIES_AWAY; + } else if (term.is_rm_value_rne()) { + return FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN; + } else if (term.is_rm_value_rtn()) { + return FloatingPointRoundingMode.TOWARD_NEGATIVE; + } else if (term.is_rm_value_rtp()) { + return FloatingPointRoundingMode.TOWARD_POSITIVE; + } else if (term.is_rm_value_rtz()) { + return FloatingPointRoundingMode.TOWARD_ZERO; + } else { + throw new IllegalArgumentException(String.format("Unknown rounding mode: %s", term)); + } } if (sort.is_bv()) { return new BigInteger(term.to_bv(), 2); 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 14cb8a3b5b..875cce7bef 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -26,6 +26,7 @@ import edu.stanford.CVC4.Integer; import edu.stanford.CVC4.Kind; import edu.stanford.CVC4.Rational; +import edu.stanford.CVC4.RoundingMode; import edu.stanford.CVC4.Type; import edu.stanford.CVC4.vectorExpr; import edu.stanford.CVC4.vectorType; @@ -334,8 +335,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Expr f) { } else if (type.isFloatingPoint()) { return visitor.visitConstant(formula, convertFloatingPoint(f)); } else if (type.isRoundingMode()) { - // TODO is this correct? - return visitor.visitConstant(formula, f.getConstRoundingMode()); + return visitor.visitConstant(formula, convertRoundingMode(f)); } else if (type.isString()) { return visitor.visitConstant(formula, f.getConstString()); } else if (type.isArray()) { @@ -624,6 +624,9 @@ public Object convertValue(Expr expForType, Expr value) { } else if (valueType.isFloatingPoint()) { return convertFloatingPoint(value); + } else if (valueType.isRoundingMode()) { + return convertRoundingMode(value); + } else if (valueType.isString()) { return unescapeUnicodeForSmtlib(value.getConstString().toString()); @@ -659,4 +662,21 @@ private FloatingPointNumber convertFloatingPoint(Expr fpExpr) { expWidth, mantWidth); } + + private FloatingPointRoundingMode convertRoundingMode(Expr pExpr) { + RoundingMode rm = pExpr.getConstRoundingMode(); + if (rm.equals(RoundingMode.roundNearestTiesToAway)) { + return FloatingPointRoundingMode.NEAREST_TIES_AWAY; + } else if (rm.equals(RoundingMode.roundNearestTiesToEven)) { + return FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN; + } else if (rm.equals(RoundingMode.roundTowardNegative)) { + return FloatingPointRoundingMode.TOWARD_NEGATIVE; + } else if (rm.equals(RoundingMode.roundTowardPositive)) { + return FloatingPointRoundingMode.TOWARD_POSITIVE; + } else if (rm.equals(RoundingMode.roundTowardZero)) { + return FloatingPointRoundingMode.TOWARD_ZERO; + } else { + throw new IllegalArgumentException(String.format("Unknown rounding mode: %s", pExpr)); + } + } } 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 f31e7bf027..f326da1590 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -27,6 +27,7 @@ import io.github.cvc5.Kind; import io.github.cvc5.Op; import io.github.cvc5.Pair; +import io.github.cvc5.RoundingMode; import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; @@ -410,7 +411,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { return visitor.visitConstant(formula, convertFloatingPoint(f)); } else if (f.isRoundingModeValue()) { - return visitor.visitConstant(formula, f.getRoundingModeValue()); + return visitor.visitConstant(formula, convertRoundingMode(f)); } else if (f.isConstArray()) { Term constant = f.getConstArrayBase(); @@ -827,6 +828,9 @@ public Object convertValue(Term expForType, Term value) { } else if (value.isFloatingPointValue()) { return convertFloatingPoint(value); + } else if (value.isRoundingModeValue()) { + return convertRoundingMode(value); + } else if (value.isBooleanValue()) { return value.getBooleanValue(); @@ -856,6 +860,23 @@ private FloatingPointNumber convertFloatingPoint(Term value) throws CVC5ApiExcep return FloatingPointNumber.of(bits, expWidth, mantWidth); } + private FloatingPointRoundingMode convertRoundingMode(Term pTerm) throws CVC5ApiException { + RoundingMode rm = pTerm.getRoundingModeValue(); + if (rm.equals(RoundingMode.ROUND_NEAREST_TIES_TO_AWAY)) { + return FloatingPointRoundingMode.NEAREST_TIES_AWAY; + } else if (rm.equals(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN)) { + return FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN; + } else if (rm.equals(RoundingMode.ROUND_TOWARD_NEGATIVE)) { + return FloatingPointRoundingMode.TOWARD_NEGATIVE; + } else if (rm.equals(RoundingMode.ROUND_TOWARD_POSITIVE)) { + return FloatingPointRoundingMode.TOWARD_POSITIVE; + } else if (rm.equals(RoundingMode.ROUND_TOWARD_ZERO)) { + return FloatingPointRoundingMode.TOWARD_ZERO; + } else { + throw new IllegalArgumentException(String.format("Unknown rounding mode: %s", pTerm)); + } + } + private Term accessVariablesCache(String name, Sort sort) { Term existingVar = variablesCache.get(name, sort.toString()); Preconditions.checkNotNull( 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 94eade2f53..c2c9f01389 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -71,7 +71,6 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_OR; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_PLUS; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_TIMES; -import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_UNKNOWN; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_decl_get_arg_type; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_decl_get_name; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_decl_get_tag; @@ -341,6 +340,20 @@ public R visit(FormulaVisitor visitor, Formula formula, final Long f) { return visitor.visitConstant(formula, true); } else if (msat_term_is_false(environment, f)) { return visitor.visitConstant(formula, false); + } else if (msat_is_fp_roundingmode_type(environment, msat_term_get_type(f))) { + long decl = msat_term_get_decl(f); + switch (msat_decl_get_name(decl)) { + case "`fprounding_even`": + return visitor.visitConstant(formula, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + case "`fprounding_plus_inf`": + return visitor.visitConstant(formula, FloatingPointRoundingMode.TOWARD_POSITIVE); + case "`fprounding_minus_inf`": + return visitor.visitConstant(formula, FloatingPointRoundingMode.TOWARD_NEGATIVE); + case "`fprounding_zero`": + return visitor.visitConstant(formula, FloatingPointRoundingMode.TOWARD_ZERO); + default: + throw new IllegalArgumentException("Unknown rounding mode " + msat_decl_get_name(decl)); + } } else if (msat_term_is_constant(environment, f)) { return visitor.visitFreeVariable(formula, msat_term_repr(f)); } else if (msat_is_enum_type(environment, msat_term_get_type(f))) { @@ -524,22 +537,6 @@ private FunctionDeclarationKind getDeclarationKind(long pF) { return FunctionDeclarationKind.FP_IS_SUBNORMAL; case MSAT_TAG_FP_ISNORMAL: return FunctionDeclarationKind.FP_IS_NORMAL; - - case MSAT_TAG_UNKNOWN: - switch (msat_decl_get_name(decl)) { - case "`fprounding_even`": - return FunctionDeclarationKind.FP_ROUND_EVEN; - case "`fprounding_plus_inf`": - return FunctionDeclarationKind.FP_ROUND_POSITIVE; - case "`fprounding_minus_inf`": - return FunctionDeclarationKind.FP_ROUND_NEGATIVE; - case "`fprounding_zero`": - return FunctionDeclarationKind.FP_ROUND_ZERO; - - default: - return FunctionDeclarationKind.OTHER; - } - case MSAT_TAG_FLOOR: return FunctionDeclarationKind.FLOOR; From f92009275e18d24706bbbb8d9f6f78d2cb85e18f Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 25 Aug 2025 15:42:49 +0200 Subject: [PATCH 03/13] RoundingMode: Added missing . to JavaDoc --- src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index 63b6802f83..5820a8593e 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -34,7 +34,7 @@ */ public interface FloatingPointFormulaManager { - /** Creates a formula for the given floating point rounding mode */ + /** Creates a formula for the given floating point rounding mode. */ FloatingPointRoundingModeFormula makeRoundingMode(FloatingPointRoundingMode pRoundingMode); /** From 508ff5cd27f03991ee057d020312ed13b51c8920 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 25 Aug 2025 20:24:53 +0200 Subject: [PATCH 04/13] RoundingMode: Remove Kinds for specific rounding modes from FunctionDeclarationKind and treat them as atomic values instead --- .../java_smt/api/FunctionDeclarationKind.java | 15 --------------- .../java_smt/solvers/z3/Z3FormulaCreator.java | 10 ---------- 2 files changed, 25 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java index a203fa1f2d..bb8a3929ba 100644 --- a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java +++ b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java @@ -252,21 +252,6 @@ public enum FunctionDeclarationKind { /** Equal over floating points. */ FP_EQ, - /** Rounding over floating points. */ - FP_ROUND_EVEN, - - /** Rounding over floating points. */ - FP_ROUND_AWAY, - - /** Rounding over floating points. */ - FP_ROUND_POSITIVE, - - /** Rounding over floating points. */ - FP_ROUND_NEGATIVE, - - /** Rounding over floating points. */ - FP_ROUND_ZERO, - /** Rounding over floating points. */ FP_ROUND_TO_INTEGRAL, 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 cb7c8f769d..f38c6837aa 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -799,16 +799,6 @@ private FunctionDeclarationKind getDeclarationKind(long f) { return FunctionDeclarationKind.FP_GT; case Z3_OP_FPA_EQ: return FunctionDeclarationKind.FP_EQ; - case Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: - return FunctionDeclarationKind.FP_ROUND_EVEN; - case Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: - return FunctionDeclarationKind.FP_ROUND_AWAY; - case Z3_OP_FPA_RM_TOWARD_POSITIVE: - return FunctionDeclarationKind.FP_ROUND_POSITIVE; - case Z3_OP_FPA_RM_TOWARD_NEGATIVE: - return FunctionDeclarationKind.FP_ROUND_NEGATIVE; - case Z3_OP_FPA_RM_TOWARD_ZERO: - return FunctionDeclarationKind.FP_ROUND_ZERO; case Z3_OP_FPA_ROUND_TO_INTEGRAL: return FunctionDeclarationKind.FP_ROUND_TO_INTEGRAL; case Z3_OP_FPA_TO_FP_UNSIGNED: From b1b1574b72cf917b9adca7d91a2ef19291485e18 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 30 Aug 2025 15:09:04 +0200 Subject: [PATCH 05/13] RoundingMode: Add a test for visitors on rounding mode formulas --- .../test/FloatingPointFormulaManagerTest.java | 66 +++++++++++++++++++ 1 file changed, 66 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..55db51c200 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -32,15 +32,21 @@ import org.sosy_lab.java_smt.api.FloatingPointNumber; import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign; import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; +import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula; +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.api.FunctionDeclaration; +import org.sosy_lab.java_smt.api.FunctionDeclarationKind; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.Model.ValueAssignment; import org.sosy_lab.java_smt.api.NumeralFormula; import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.visitors.FormulaVisitor; public class FloatingPointFormulaManagerTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { @@ -87,6 +93,66 @@ public void floatingPointType() { .isEqualTo(type.getMantissaSize()); } + @Test + public void roundingModeVisitor() { + FloatingPointFormula var = + fpmgr.makeVariable("a", FloatingPointType.getSinglePrecisionFloatingPointType()); + FloatingPointFormula f = fpmgr.sqrt(var, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + + for (FloatingPointRoundingMode rm : FloatingPointRoundingMode.values()) { + if (solver == Solvers.MATHSAT5 && rm == FloatingPointRoundingMode.NEAREST_TIES_AWAY) { + // SKIP MathSAT does not support rounding mode "nearest-ties-away" + continue; + } + // Build a term with a different rounding mode, then replace it in the visitor + FloatingPointFormula g = + (FloatingPointFormula) + mgr.visit( + fpmgr.sqrt(var, rm), + new FormulaVisitor() { + @Override + public Formula visitFreeVariable(Formula f, String name) { + return f; + } + + @Override + public Formula visitConstant(Formula f, Object value) { + assertThat(f).isInstanceOf(FloatingPointRoundingModeFormula.class); + assertThat(value).isInstanceOf(FloatingPointRoundingMode.class); + assertThat(value).isEqualTo(rm); + + // Return the default rounding mode + return fpmgr.makeRoundingMode(FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + } + + @Override + public Formula visitFunction( + Formula f, List args, FunctionDeclaration functionDeclaration) { + assertThat(functionDeclaration.getKind()) + .isEqualTo(FunctionDeclarationKind.FP_SQRT); + assertThat(args.size()).isEqualTo(2); + return mgr.makeApplication( + functionDeclaration, + mgr.visit(args.get(0), this), + mgr.visit(args.get(1), this)); + } + + @Override + public Formula visitQuantifier( + BooleanFormula f, + Quantifier quantifier, + List boundVariables, + BooleanFormula body) { + throw new IllegalArgumentException( + String.format("Unexpected quantifier %s", quantifier)); + } + }); + + // Check that after the substitution the rounding mode is the default again + assertThat(f).isEqualTo(g); + } + } + @Test public void negative() throws SolverException, InterruptedException { for (double d : new double[] {-1, -2, -0.0, Double.NEGATIVE_INFINITY}) { From c42fef467f9877270432f18ac80f0747229ebd31 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 30 Aug 2025 21:21:24 +0200 Subject: [PATCH 06/13] RoundingMode: Use MathSAT API instead of matching the symbol name --- .../mathsat5/Mathsat5FormulaCreator.java | 27 ++++++++++--------- .../solvers/mathsat5/Mathsat5NativeApi.java | 8 ++++++ 2 files changed, 23 insertions(+), 12 deletions(-) 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 c2c9f01389..276cb236b8 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -104,6 +104,10 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_get_type; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_constant; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_false; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_fp_roundingmode_minus_inf; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_fp_roundingmode_nearest_even; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_fp_roundingmode_plus_inf; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_fp_roundingmode_zero; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_number; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_true; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_uf; @@ -341,18 +345,17 @@ public R visit(FormulaVisitor visitor, Formula formula, final Long f) { } else if (msat_term_is_false(environment, f)) { return visitor.visitConstant(formula, false); } else if (msat_is_fp_roundingmode_type(environment, msat_term_get_type(f))) { - long decl = msat_term_get_decl(f); - switch (msat_decl_get_name(decl)) { - case "`fprounding_even`": - return visitor.visitConstant(formula, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); - case "`fprounding_plus_inf`": - return visitor.visitConstant(formula, FloatingPointRoundingMode.TOWARD_POSITIVE); - case "`fprounding_minus_inf`": - return visitor.visitConstant(formula, FloatingPointRoundingMode.TOWARD_NEGATIVE); - case "`fprounding_zero`": - return visitor.visitConstant(formula, FloatingPointRoundingMode.TOWARD_ZERO); - default: - throw new IllegalArgumentException("Unknown rounding mode " + msat_decl_get_name(decl)); + if (msat_term_is_fp_roundingmode_nearest_even(environment, f)) { + return visitor.visitConstant(formula, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + } else if (msat_term_is_fp_roundingmode_plus_inf(environment, f)) { + return visitor.visitConstant(formula, FloatingPointRoundingMode.TOWARD_POSITIVE); + } else if (msat_term_is_fp_roundingmode_minus_inf(environment, f)) { + return visitor.visitConstant(formula, FloatingPointRoundingMode.TOWARD_NEGATIVE); + } else if (msat_term_is_fp_roundingmode_zero(environment, f)) { + return visitor.visitConstant(formula, FloatingPointRoundingMode.TOWARD_ZERO); + } else { + throw new IllegalArgumentException( + "Unknown rounding mode " + msat_decl_get_name(msat_term_get_decl(f))); } } else if (msat_term_is_constant(environment, f)) { return visitor.visitFreeVariable(formula, msat_term_repr(f)); diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java index f0862ddaf8..aa8556f983 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java @@ -652,6 +652,14 @@ public static native long msat_simplify( public static native boolean msat_term_is_bv_comp(long e, long t); + public static native boolean msat_term_is_fp_roundingmode_nearest_even(long e, long t); + + public static native boolean msat_term_is_fp_roundingmode_zero(long e, long t); + + public static native boolean msat_term_is_fp_roundingmode_plus_inf(long e, long t); + + public static native boolean msat_term_is_fp_roundingmode_minus_inf(long e, long t); + public static native boolean msat_term_is_quantifier(long e, long t); public static native boolean msat_term_is_forall(long e, long t); From e06058afc44aff72b510914e848260c9fbe10d51 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 30 Aug 2025 23:50:42 +0200 Subject: [PATCH 07/13] RoundingMode: Apply error-prone patch --- .../sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 55db51c200..5b8e6e8235 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -130,7 +130,7 @@ public Formula visitFunction( Formula f, List args, FunctionDeclaration functionDeclaration) { assertThat(functionDeclaration.getKind()) .isEqualTo(FunctionDeclarationKind.FP_SQRT); - assertThat(args.size()).isEqualTo(2); + assertThat(args).hasSize(2); return mgr.makeApplication( functionDeclaration, mgr.visit(args.get(0), this), From 766e762c738f3c62e79ddaf6760efe073141416e Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 30 Aug 2025 23:53:27 +0200 Subject: [PATCH 08/13] RoundingMode: Rename variables to avoid shadowing --- .../test/FloatingPointFormulaManagerTest.java | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 5b8e6e8235..51463b0a35 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -95,9 +95,10 @@ public void floatingPointType() { @Test public void roundingModeVisitor() { - FloatingPointFormula var = + FloatingPointFormula variable = fpmgr.makeVariable("a", FloatingPointType.getSinglePrecisionFloatingPointType()); - FloatingPointFormula f = fpmgr.sqrt(var, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + FloatingPointFormula original = + fpmgr.sqrt(variable, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); for (FloatingPointRoundingMode rm : FloatingPointRoundingMode.values()) { if (solver == Solvers.MATHSAT5 && rm == FloatingPointRoundingMode.NEAREST_TIES_AWAY) { @@ -105,10 +106,10 @@ public void roundingModeVisitor() { continue; } // Build a term with a different rounding mode, then replace it in the visitor - FloatingPointFormula g = + FloatingPointFormula substituted = (FloatingPointFormula) mgr.visit( - fpmgr.sqrt(var, rm), + fpmgr.sqrt(variable, rm), new FormulaVisitor() { @Override public Formula visitFreeVariable(Formula f, String name) { @@ -149,7 +150,7 @@ public Formula visitQuantifier( }); // Check that after the substitution the rounding mode is the default again - assertThat(f).isEqualTo(g); + assertThat(original).isEqualTo(substituted); } } From b14542ad5fb04fedbfdadedb3e3c11c64cfa0f5c Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 30 Aug 2025 23:54:37 +0200 Subject: [PATCH 09/13] RoundingMode: Fix checkstyle issue --- .../sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 51463b0a35..3f87193507 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -96,7 +96,7 @@ public void floatingPointType() { @Test public void roundingModeVisitor() { FloatingPointFormula variable = - fpmgr.makeVariable("a", FloatingPointType.getSinglePrecisionFloatingPointType()); + fpmgr.makeVariable("a", FormulaType.getSinglePrecisionFloatingPointType()); FloatingPointFormula original = fpmgr.sqrt(variable, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); From d181f60946f6e0c8f1dbf78a0963f8384f991a28 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 4 Nov 2025 23:18:47 +0100 Subject: [PATCH 10/13] extend API with method for retrieving RoundingMode from the corresponding formula. --- .../api/FloatingPointFormulaManager.java | 9 +++- .../api/FloatingPointRoundingMode.java | 8 +++- .../api/FloatingPointRoundingModeFormula.java | 4 ++ .../AbstractFloatingPointFormulaManager.java | 6 +++ .../java_smt/basicimpl/FormulaCreator.java | 10 +++++ .../DebuggingFloatingPointFormulaManager.java | 8 ++++ ...StatisticsFloatingPointFormulaManager.java | 7 ++++ ...nchronizedFloatingPointFormulaManager.java | 8 ++++ .../bitwuzla/BitwuzlaFormulaCreator.java | 33 +++++++++------ .../solvers/cvc4/CVC4FormulaCreator.java | 14 +++++-- .../solvers/cvc5/CVC5FormulaCreator.java | 41 +++++++++++-------- .../mathsat5/Mathsat5FormulaCreator.java | 29 +++++++------ .../java_smt/solvers/z3/Z3FormulaCreator.java | 36 +++++++++++++--- .../test/FloatingPointFormulaManagerTest.java | 12 ++++++ 14 files changed, 171 insertions(+), 54 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index 5820a8593e..e3765f1854 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2020 Dirk Beyer +// SPDX-FileCopyrightText: 2025 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 @@ -37,6 +37,13 @@ public interface FloatingPointFormulaManager { /** Creates a formula for the given floating point rounding mode. */ FloatingPointRoundingModeFormula makeRoundingMode(FloatingPointRoundingMode pRoundingMode); + /** + * Converts a rounding mode formula to the corresponding enum value. This method is the inverse of + * {@link #makeRoundingMode(FloatingPointRoundingMode)}. + */ + FloatingPointRoundingMode fromRoundingModeFormula( + FloatingPointRoundingModeFormula pRoundingModeFormula); + /** * Creates a floating point formula representing the given double value with the specified type. */ diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointRoundingMode.java b/src/org/sosy_lab/java_smt/api/FloatingPointRoundingMode.java index 6208682afa..1698d711e1 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointRoundingMode.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointRoundingMode.java @@ -2,13 +2,17 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2020 Dirk Beyer +// SPDX-FileCopyrightText: 2025 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 package org.sosy_lab.java_smt.api; -/** Possible floating point rounding modes. */ +/** + * Represents the various rounding modes that can be applied when converting or manipulating + * floating-point values and formulas. These modes define how results are rounded when an exact + * representation is not possible due to precision limits of the target format. + */ public enum FloatingPointRoundingMode { NEAREST_TIES_TO_EVEN, NEAREST_TIES_AWAY, diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointRoundingModeFormula.java b/src/org/sosy_lab/java_smt/api/FloatingPointRoundingModeFormula.java index b9fb69fd73..d932fbc629 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointRoundingModeFormula.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointRoundingModeFormula.java @@ -16,6 +16,10 @@ *

Rounding mode formulas are used by floating-point formulas to select the rounding mode for the * operation. Use {@link FloatingPointFormulaManager#makeRoundingMode(FloatingPointRoundingMode)} to * wrap a {@link org.sosy_lab.java_smt.api.FloatingPointRoundingMode} value inside a new formula. + * + *

This class is rarely used in the API but necessary to support visitor traversal of formulas + * with certain floating-point operations, where JavaSMT provides the rounding mode as Formula-based + * argument. */ @Immutable public interface FloatingPointRoundingModeFormula extends Formula {} diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index a653948bb3..e2572ab820 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -67,6 +67,12 @@ public FloatingPointRoundingModeFormula makeRoundingMode( return getFormulaCreator().encapsulateRoundingMode(getRoundingMode(pRoundingMode)); } + @Override + public FloatingPointRoundingMode fromRoundingModeFormula( + FloatingPointRoundingModeFormula pRoundingModeFormula) { + return getFormulaCreator().getRoundingMode(extractInfo(pRoundingModeFormula)); + } + protected FloatingPointFormula wrap(TFormulaInfo pTerm) { return getFormulaCreator().encapsulateFloatingPoint(pTerm); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java index cf383fde5a..44498ee4ec 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java @@ -31,6 +31,7 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.EnumerationFormula; import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; @@ -134,6 +135,15 @@ public final TType getRegexType() { return regexType; } + public FloatingPointRoundingMode getRoundingMode(FloatingPointRoundingModeFormula f) { + return getRoundingMode(extractInfo(f)); + } + + protected FloatingPointRoundingMode getRoundingMode(TFormulaInfo f) { + throw new UnsupportedOperationException( + "Floating point rounding modes are not supported by this solver."); + } + public abstract TFormulaInfo makeVariable(TType type, String varName); public BooleanFormula encapsulateBoolean(TFormulaInfo pTerm) { diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java index 817fb05ff1..84a528b48b 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java @@ -41,6 +41,14 @@ public FloatingPointRoundingModeFormula makeRoundingMode( return result; } + @Override + public FloatingPointRoundingMode fromRoundingModeFormula( + FloatingPointRoundingModeFormula pRoundingModeFormula) { + debugging.assertThreadLocal(); + debugging.assertFormulaInContext(pRoundingModeFormula); + return delegate.fromRoundingModeFormula(pRoundingModeFormula); + } + @Override public FloatingPointFormula makeNumber(double n, FloatingPointType type) { debugging.assertThreadLocal(); 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 f1669369c8..5f1b58b7aa 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java @@ -42,6 +42,13 @@ public FloatingPointRoundingModeFormula makeRoundingMode( return delegate.makeRoundingMode(pRoundingMode); } + @Override + public FloatingPointRoundingMode fromRoundingModeFormula( + FloatingPointRoundingModeFormula pRoundingModeFormula) { + stats.fpOperations.getAndIncrement(); + return delegate.fromRoundingModeFormula(pRoundingModeFormula); + } + @Override public FloatingPointFormula makeNumber(double pN, FloatingPointType pType) { stats.fpOperations.getAndIncrement(); 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 f0e1049c75..4dd8354be5 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java @@ -44,6 +44,14 @@ public FloatingPointRoundingModeFormula makeRoundingMode( } } + @Override + public FloatingPointRoundingMode fromRoundingModeFormula( + FloatingPointRoundingModeFormula pRoundingModeFormula) { + synchronized (sync) { + return delegate.fromRoundingModeFormula(pRoundingModeFormula); + } + } + @Override public FloatingPointFormula makeNumber(double pN, FloatingPointType pType) { synchronized (sync) { 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 f9fa6e30e7..1809f4f8ff 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -594,19 +594,7 @@ public Object convertValue(Term term) { return term.to_bool(); } if (sort.is_rm()) { - if (term.is_rm_value_rna()) { - return FloatingPointRoundingMode.NEAREST_TIES_AWAY; - } else if (term.is_rm_value_rne()) { - return FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN; - } else if (term.is_rm_value_rtn()) { - return FloatingPointRoundingMode.TOWARD_NEGATIVE; - } else if (term.is_rm_value_rtp()) { - return FloatingPointRoundingMode.TOWARD_POSITIVE; - } else if (term.is_rm_value_rtz()) { - return FloatingPointRoundingMode.TOWARD_ZERO; - } else { - throw new IllegalArgumentException(String.format("Unknown rounding mode: %s", term)); - } + return getRoundingMode(term); } if (sort.is_bv()) { return new BigInteger(term.to_bv(), 2); @@ -649,4 +637,23 @@ public Collection getConstraintsForTerm(Term pTerm) { return transformedImmutableSetCopy(usedConstraintVariables, constraintsForVariables::get); } + + @Override + protected FloatingPointRoundingMode getRoundingMode(Term term) { + checkArgument(term.sort().is_rm(), "Term '%s' is not of rounding mode sort.", term); + if (term.is_rm_value_rna()) { + return FloatingPointRoundingMode.NEAREST_TIES_AWAY; + } else if (term.is_rm_value_rne()) { + return FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN; + } else if (term.is_rm_value_rtn()) { + return FloatingPointRoundingMode.TOWARD_NEGATIVE; + } else if (term.is_rm_value_rtp()) { + return FloatingPointRoundingMode.TOWARD_POSITIVE; + } else if (term.is_rm_value_rtz()) { + return FloatingPointRoundingMode.TOWARD_ZERO; + } else { + throw new IllegalArgumentException( + String.format("Unknown rounding mode in Term '%s'.", term)); + } + } } 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 f07d91b748..1de5ad6614 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -335,7 +335,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Expr f) { } else if (type.isFloatingPoint()) { return visitor.visitConstant(formula, convertFloatingPoint(f)); } else if (type.isRoundingMode()) { - return visitor.visitConstant(formula, convertRoundingMode(f)); + return visitor.visitConstant(formula, getRoundingMode(f)); } else if (type.isString()) { return visitor.visitConstant(formula, f.getConstString()); } else if (type.isArray()) { @@ -626,7 +626,7 @@ public Object convertValue(Expr expForType, Expr value) { return convertFloatingPoint(value); } else if (valueType.isRoundingMode()) { - return convertRoundingMode(value); + return getRoundingMode(value); } else if (valueType.isString()) { return unescapeUnicodeForSmtlib(value.getConstString().toString()); @@ -664,7 +664,12 @@ private FloatingPointNumber convertFloatingPoint(Expr fpExpr) { mantWidth); } - private FloatingPointRoundingMode convertRoundingMode(Expr pExpr) { + @Override + protected FloatingPointRoundingMode getRoundingMode(Expr pExpr) { + checkArgument( + pExpr.isConst() && pExpr.getType().isRoundingMode(), + "Expected a constant rounding mode, but got: %s", + pExpr); RoundingMode rm = pExpr.getConstRoundingMode(); if (rm.equals(RoundingMode.roundNearestTiesToAway)) { return FloatingPointRoundingMode.NEAREST_TIES_AWAY; @@ -677,7 +682,8 @@ private FloatingPointRoundingMode convertRoundingMode(Expr pExpr) { } else if (rm.equals(RoundingMode.roundTowardZero)) { return FloatingPointRoundingMode.TOWARD_ZERO; } else { - throw new IllegalArgumentException(String.format("Unknown rounding mode: %s", pExpr)); + throw new IllegalArgumentException( + String.format("Unknown rounding mode in Term '%s'.", pExpr)); } } } 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 13aa32844a..afe52bb978 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -27,7 +27,6 @@ import io.github.cvc5.Kind; import io.github.cvc5.Op; import io.github.cvc5.Pair; -import io.github.cvc5.RoundingMode; import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; @@ -411,7 +410,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { return visitor.visitConstant(formula, convertFloatingPoint(f)); } else if (f.isRoundingModeValue()) { - return visitor.visitConstant(formula, convertRoundingMode(f)); + return visitor.visitConstant(formula, getRoundingMode(f)); } else if (f.isConstArray()) { Term constant = f.getConstArrayBase(); @@ -832,7 +831,7 @@ public Object convertValue(Term expForType, Term value) { return convertFloatingPoint(value); } else if (value.isRoundingModeValue()) { - return convertRoundingMode(value); + return getRoundingMode(value); } else if (value.isBooleanValue()) { return value.getBooleanValue(); @@ -863,20 +862,28 @@ private FloatingPointNumber convertFloatingPoint(Term value) throws CVC5ApiExcep return FloatingPointNumber.of(bits, expWidth, mantWidth); } - private FloatingPointRoundingMode convertRoundingMode(Term pTerm) throws CVC5ApiException { - RoundingMode rm = pTerm.getRoundingModeValue(); - if (rm.equals(RoundingMode.ROUND_NEAREST_TIES_TO_AWAY)) { - return FloatingPointRoundingMode.NEAREST_TIES_AWAY; - } else if (rm.equals(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN)) { - return FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN; - } else if (rm.equals(RoundingMode.ROUND_TOWARD_NEGATIVE)) { - return FloatingPointRoundingMode.TOWARD_NEGATIVE; - } else if (rm.equals(RoundingMode.ROUND_TOWARD_POSITIVE)) { - return FloatingPointRoundingMode.TOWARD_POSITIVE; - } else if (rm.equals(RoundingMode.ROUND_TOWARD_ZERO)) { - return FloatingPointRoundingMode.TOWARD_ZERO; - } else { - throw new IllegalArgumentException(String.format("Unknown rounding mode: %s", pTerm)); + @Override + public FloatingPointRoundingMode getRoundingMode(Term pTerm) { + checkArgument(pTerm.isRoundingModeValue(), "Term '%s' is not a rounding mode.", pTerm); + try { + switch (pTerm.getRoundingModeValue()) { + case ROUND_NEAREST_TIES_TO_AWAY: + return FloatingPointRoundingMode.NEAREST_TIES_AWAY; + case ROUND_NEAREST_TIES_TO_EVEN: + return FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN; + case ROUND_TOWARD_NEGATIVE: + return FloatingPointRoundingMode.TOWARD_NEGATIVE; + case ROUND_TOWARD_POSITIVE: + return FloatingPointRoundingMode.TOWARD_POSITIVE; + case ROUND_TOWARD_ZERO: + return FloatingPointRoundingMode.TOWARD_ZERO; + default: + throw new IllegalArgumentException( + String.format("Unknown rounding mode in Term '%s'.", pTerm)); + } + } catch (CVC5ApiException pE) { + throw new IllegalArgumentException( + String.format("Failure trying to get the rounding mode of Term '%s'.", pTerm), pE); } } 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 9f35e82dc9..cde933a5dc 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -349,18 +349,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Long f) { } else if (msat_term_is_false(environment, f)) { return visitor.visitConstant(formula, false); } else if (msat_is_fp_roundingmode_type(environment, msat_term_get_type(f))) { - if (msat_term_is_fp_roundingmode_nearest_even(environment, f)) { - return visitor.visitConstant(formula, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); - } else if (msat_term_is_fp_roundingmode_plus_inf(environment, f)) { - return visitor.visitConstant(formula, FloatingPointRoundingMode.TOWARD_POSITIVE); - } else if (msat_term_is_fp_roundingmode_minus_inf(environment, f)) { - return visitor.visitConstant(formula, FloatingPointRoundingMode.TOWARD_NEGATIVE); - } else if (msat_term_is_fp_roundingmode_zero(environment, f)) { - return visitor.visitConstant(formula, FloatingPointRoundingMode.TOWARD_ZERO); - } else { - throw new IllegalArgumentException( - "Unknown rounding mode " + msat_decl_get_name(msat_term_get_decl(f))); - } + return visitor.visitConstant(formula, getRoundingMode(f)); } else if (msat_term_is_constant(environment, f)) { return visitor.visitFreeVariable(formula, msat_term_repr(f)); } else if (msat_is_enum_type(environment, msat_term_get_type(f))) { @@ -400,6 +389,22 @@ public R visit(FormulaVisitor visitor, Formula formula, final Long f) { } } + @Override + protected FloatingPointRoundingMode getRoundingMode(Long f) { + if (msat_term_is_fp_roundingmode_nearest_even(environment, f)) { + return FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN; + } else if (msat_term_is_fp_roundingmode_plus_inf(environment, f)) { + return FloatingPointRoundingMode.TOWARD_POSITIVE; + } else if (msat_term_is_fp_roundingmode_minus_inf(environment, f)) { + return FloatingPointRoundingMode.TOWARD_NEGATIVE; + } else if (msat_term_is_fp_roundingmode_zero(environment, f)) { + return FloatingPointRoundingMode.TOWARD_ZERO; + } else { + throw new IllegalArgumentException( + String.format("Unknown rounding mode in Term '%s'.", msat_term_repr(f))); + } + } + String getName(long term) { if (msat_term_is_uf(environment, term)) { return msat_decl_get_name(msat_term_get_decl(term)); 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 978c76c482..0f9fdc558c 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -419,6 +419,32 @@ public Long getArrayType(Long pIndexType, Long pElementType) { return allocatedArraySort; } + @Override + protected FloatingPointRoundingMode getRoundingMode(Long f) { + checkArgument( + Native.getSortKind(environment, Native.getSort(environment, f)) + == Z3_sort_kind.Z3_ROUNDING_MODE_SORT.toInt(), + "Expected a floating point rounding mode, but got %s", + Native.astToString(environment, f)); + + int roundingModeOp = Native.getDeclKind(environment, Native.getAppDecl(environment, f)); + switch (Z3_decl_kind.fromInt(roundingModeOp)) { + case Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: + return FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN; + case Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: + return FloatingPointRoundingMode.NEAREST_TIES_AWAY; + case Z3_OP_FPA_RM_TOWARD_POSITIVE: + return FloatingPointRoundingMode.TOWARD_POSITIVE; + case Z3_OP_FPA_RM_TOWARD_NEGATIVE: + return FloatingPointRoundingMode.TOWARD_NEGATIVE; + case Z3_OP_FPA_RM_TOWARD_ZERO: + return FloatingPointRoundingMode.TOWARD_ZERO; + default: + throw new IllegalArgumentException( + "Cannot get rounding mode for Z3 operator: " + roundingModeOp); + } + } + @Override public Long getBitvectorType(int pBitwidth) { checkArgument(pBitwidth > 0, "Cannot use bitvector type with size %s", pBitwidth); @@ -506,6 +532,7 @@ public R visit(FormulaVisitor visitor, final Formula formula, final Long if (arity == 0) { // constants Object value = Z3_CONSTANTS.get(declKind); + int sortKind = Native.getSortKind(environment, Native.getSort(environment, f)); if (value != null) { return visitor.visitConstant(formula, value); @@ -513,15 +540,14 @@ public R visit(FormulaVisitor visitor, final Formula formula, final Long return visitor.visitConstant(formula, convertValue(f)); // Rounding mode - } else if (declKind == Z3_decl_kind.Z3_OP_FPA_NUM.toInt() - || Native.getSortKind(environment, Native.getSort(environment, f)) - == Z3_sort_kind.Z3_ROUNDING_MODE_SORT.toInt()) { + } else if (declKind == Z3_decl_kind.Z3_OP_FPA_NUM.toInt()) { return visitor.visitConstant(formula, convertValue(f)); + } else if (sortKind == Z3_sort_kind.Z3_ROUNDING_MODE_SORT.toInt()) { + return visitor.visitConstant(formula, getRoundingMode(f)); // string constant } else if (declKind == Z3_decl_kind.Z3_OP_INTERNAL.toInt() - && Native.getSortKind(environment, Native.getSort(environment, f)) - == Z3_sort_kind.Z3_SEQ_SORT.toInt()) { + && sortKind == Z3_sort_kind.Z3_SEQ_SORT.toInt()) { return visitor.visitConstant(formula, convertValue(f)); // Free variable diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 4636426e2e..3ae8251e63 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -11,6 +11,7 @@ import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.Truth.assertWithMessage; import static com.google.common.truth.TruthJUnit.assume; +import static org.junit.Assert.assertEquals; import static org.junit.Assert.assertThrows; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; @@ -852,6 +853,17 @@ private void assertEqualsAsFormula(FloatingPointFormula f1, FloatingPointFormula assertThatFormula(fpmgr.assignment(f1, f2)).isTautological(); } + @Test + public void roundingModeMapping() { + for (FloatingPointRoundingMode rm : FloatingPointRoundingMode.values()) { + if (solver == Solvers.MATHSAT5 && rm == FloatingPointRoundingMode.NEAREST_TIES_AWAY) { + // SKIP MathSAT does not support rounding mode "nearest-ties-away" + continue; + } + assertEquals(rm, fpmgr.fromRoundingModeFormula(fpmgr.makeRoundingMode(rm))); + } + } + @Test public void round() throws SolverException, InterruptedException { requireIntegers(); From de7a870eab54056a4349a4839553a4a157c36d52 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 4 Nov 2025 23:39:55 +0100 Subject: [PATCH 11/13] make API backward-compatible. --- .../java_smt/api/FloatingPointFormulaManager.java | 7 +++++-- src/org/sosy_lab/java_smt/api/FormulaManager.java | 10 ++++++++++ 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index e3765f1854..25ddff9a96 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -8,6 +8,7 @@ package org.sosy_lab.java_smt.api; +import static org.sosy_lab.java_smt.api.FormulaManager.API_METHOD_NOT_IMPLEMENTED; import static org.sosy_lab.java_smt.api.FormulaType.getFloatingPointType; import java.math.BigDecimal; @@ -41,8 +42,10 @@ public interface FloatingPointFormulaManager { * Converts a rounding mode formula to the corresponding enum value. This method is the inverse of * {@link #makeRoundingMode(FloatingPointRoundingMode)}. */ - FloatingPointRoundingMode fromRoundingModeFormula( - FloatingPointRoundingModeFormula pRoundingModeFormula); + default FloatingPointRoundingMode fromRoundingModeFormula( + FloatingPointRoundingModeFormula pRoundingModeFormula) { + throw new UnsupportedOperationException(API_METHOD_NOT_IMPLEMENTED); + } /** * Creates a floating point formula representing the given double value with the specified type. diff --git a/src/org/sosy_lab/java_smt/api/FormulaManager.java b/src/org/sosy_lab/java_smt/api/FormulaManager.java index fd3127a009..1dcefec063 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FormulaManager.java @@ -20,6 +20,16 @@ /** FormulaManager class contains all operations which can be performed on formulas. */ public interface FormulaManager { + /** + * Standardized message for not implemented API methods. + * + *

This constant can be used in {@link UnsupportedOperationException} to indicate that a + * certain method is not implemented by some subclass. We recommend using this constant in API + * extensions where the default implementation throws an exception. + */ + String API_METHOD_NOT_IMPLEMENTED = + "The requested method is not implemented in the current implementation of this interface."; + /** * Returns the Integer-Theory. Because most SAT-solvers support automatic casting between Integer- * and Rational-Theory, the Integer- and the RationalFormulaManager both return the same Formulas From 76c4ead4eee030cd098d8177d5a850eb604dc5c0 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 4 Nov 2025 23:44:45 +0100 Subject: [PATCH 12/13] fix CI warnings. --- src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java | 1 + .../sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java | 4 ++-- .../java_smt/test/FloatingPointFormulaManagerTest.java | 5 ++--- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java index 44498ee4ec..1e1ed943f4 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java @@ -139,6 +139,7 @@ public FloatingPointRoundingMode getRoundingMode(FloatingPointRoundingModeFormul return getRoundingMode(extractInfo(f)); } + @SuppressWarnings("unused") protected FloatingPointRoundingMode getRoundingMode(TFormulaInfo f) { throw new UnsupportedOperationException( "Floating point rounding modes are not supported by this solver."); 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 afe52bb978..6d948cb969 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -881,9 +881,9 @@ public FloatingPointRoundingMode getRoundingMode(Term pTerm) { throw new IllegalArgumentException( String.format("Unknown rounding mode in Term '%s'.", pTerm)); } - } catch (CVC5ApiException pE) { + } catch (CVC5ApiException e) { throw new IllegalArgumentException( - String.format("Failure trying to get the rounding mode of Term '%s'.", pTerm), pE); + String.format("Failure trying to get the rounding mode of Term '%s'.", pTerm), e); } } diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 3ae8251e63..3dd541d780 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2020 Dirk Beyer +// SPDX-FileCopyrightText: 2025 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 @@ -11,7 +11,6 @@ import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.Truth.assertWithMessage; import static com.google.common.truth.TruthJUnit.assume; -import static org.junit.Assert.assertEquals; import static org.junit.Assert.assertThrows; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; @@ -860,7 +859,7 @@ public void roundingModeMapping() { // SKIP MathSAT does not support rounding mode "nearest-ties-away" continue; } - assertEquals(rm, fpmgr.fromRoundingModeFormula(fpmgr.makeRoundingMode(rm))); + assertThat(fpmgr.fromRoundingModeFormula(fpmgr.makeRoundingMode(rm))).isEqualTo(rm); } } From 2fb264328be1e3dc34dc03b4bbb1794acf343e4e Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 4 Nov 2025 23:52:55 +0100 Subject: [PATCH 13/13] fix CI warnings. --- src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index 25ddff9a96..89f6d8437f 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -42,6 +42,7 @@ public interface FloatingPointFormulaManager { * Converts a rounding mode formula to the corresponding enum value. This method is the inverse of * {@link #makeRoundingMode(FloatingPointRoundingMode)}. */ + @SuppressWarnings("unused") default FloatingPointRoundingMode fromRoundingModeFormula( FloatingPointRoundingModeFormula pRoundingModeFormula) { throw new UnsupportedOperationException(API_METHOD_NOT_IMPLEMENTED);