From e1f85a45ad88de60bbcdb91270b9c15f712e491d Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 25 Aug 2025 14:48:41 +0200 Subject: [PATCH 1/9] 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 2/9] 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 3/9] 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 4/9] 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 5/9] 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 6/9] 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 7/9] 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 8/9] 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 9/9] 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);