diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index 62bb3afbe4..89f6d8437f 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java @@ -2,12 +2,13 @@ // 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; +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; @@ -34,6 +35,19 @@ */ 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)}. + */ + @SuppressWarnings("unused") + 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/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 ead8fc04af..d932fbc629 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointRoundingModeFormula.java +++ b/src/org/sosy_lab/java_smt/api/FloatingPointRoundingModeFormula.java @@ -11,8 +11,15 @@ 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. + * + *

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/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 diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java index 2421eca80c..02f1b7281f 100644 --- a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java +++ b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java @@ -261,21 +261,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/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 47c847afe2..e2572ab820 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,18 @@ private TFormulaInfo getRoundingMode(FloatingPointRoundingMode pFloatingPointRou return roundingModes.computeIfAbsent(pFloatingPointRoundingMode, this::getRoundingModeImpl); } + @Override + public FloatingPointRoundingModeFormula makeRoundingMode( + FloatingPointRoundingMode pRoundingMode) { + 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 748fdd7b3b..1e1ed943f4 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,16 @@ public final TType getRegexType() { return regexType; } + public FloatingPointRoundingMode getRoundingMode(FloatingPointRoundingModeFormula f) { + return getRoundingMode(extractInfo(f)); + } + + @SuppressWarnings("unused") + 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) { @@ -160,6 +171,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..84a528b48b 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,23 @@ 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 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 415b7cb00f..5f1b58b7aa 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,20 @@ class StatisticsFloatingPointFormulaManager implements FloatingPointFormulaManag stats = checkNotNull(pStats); } + @Override + public FloatingPointRoundingModeFormula makeRoundingMode( + FloatingPointRoundingMode pRoundingMode) { + stats.fpOperations.getAndIncrement(); + 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 3d922f71a8..4dd8354be5 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,22 @@ class SynchronizedFloatingPointFormulaManager implements FloatingPointFormulaMan sync = checkNotNull(pSync); } + @Override + public FloatingPointRoundingModeFormula makeRoundingMode( + FloatingPointRoundingMode pRoundingMode) { + synchronized (sync) { + return delegate.makeRoundingMode(pRoundingMode); + } + } + + @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 f946331319..1809f4f8ff 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( @@ -584,7 +594,7 @@ public Object convertValue(Term term) { return term.to_bool(); } if (sort.is_rm()) { - return term.to_rm(); + return getRoundingMode(term); } if (sort.is_bv()) { return new BigInteger(term.to_bv(), 2); @@ -627,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 3c4712fb3a..1de5ad6614 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; @@ -41,6 +42,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 +267,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( @@ -323,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, getRoundingMode(f)); } else if (type.isString()) { return visitor.visitConstant(formula, f.getConstString()); } else if (type.isArray()) { @@ -614,6 +625,9 @@ public Object convertValue(Expr expForType, Expr value) { } else if (valueType.isFloatingPoint()) { return convertFloatingPoint(value); + } else if (valueType.isRoundingMode()) { + return getRoundingMode(value); + } else if (valueType.isString()) { return unescapeUnicodeForSmtlib(value.getConstString().toString()); @@ -649,4 +663,27 @@ private FloatingPointNumber convertFloatingPoint(Expr fpExpr) { expWidth, mantWidth); } + + @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; + } 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 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 54761f9a1e..6d948cb969 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( @@ -399,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, f.getRoundingModeValue()); + return visitor.visitConstant(formula, getRoundingMode(f)); } else if (f.isConstArray()) { Term constant = f.getConstArrayBase(); @@ -819,6 +830,9 @@ public Object convertValue(Term expForType, Term value) { } else if (value.isFloatingPointValue()) { return convertFloatingPoint(value); + } else if (value.isRoundingModeValue()) { + return getRoundingMode(value); + } else if (value.isBooleanValue()) { return value.getBooleanValue(); @@ -848,6 +862,31 @@ private FloatingPointNumber convertFloatingPoint(Term value) throws CVC5ApiExcep return FloatingPointNumber.of(bits, expWidth, mantWidth); } + @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 e) { + throw new IllegalArgumentException( + String.format("Failure trying to get the rounding mode of Term '%s'.", pTerm), e); + } + } + 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 a96aa8f4ee..cde933a5dc 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -75,7 +75,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; @@ -109,6 +108,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; @@ -131,6 +134,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; @@ -295,6 +300,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( @@ -337,6 +348,8 @@ 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))) { + 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))) { @@ -376,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)); @@ -528,22 +557,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; 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); 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 332ddfa474..0f9fdc558c 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -48,6 +48,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; @@ -367,6 +368,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() @@ -411,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); @@ -498,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); @@ -505,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 @@ -803,16 +837,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: diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index f8579710cf..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 @@ -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,67 @@ public void floatingPointType() { .isEqualTo(type.getMantissaSize()); } + @Test + public void roundingModeVisitor() { + FloatingPointFormula variable = + fpmgr.makeVariable("a", FormulaType.getSinglePrecisionFloatingPointType()); + FloatingPointFormula original = + fpmgr.sqrt(variable, 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 substituted = + (FloatingPointFormula) + mgr.visit( + fpmgr.sqrt(variable, 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).hasSize(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(original).isEqualTo(substituted); + } + } + @Test public void negative() throws SolverException, InterruptedException { for (double d : new double[] {-1, -2, -0.0, Double.NEGATIVE_INFINITY}) { @@ -785,6 +852,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; + } + assertThat(fpmgr.fromRoundingModeFormula(fpmgr.makeRoundingMode(rm))).isEqualTo(rm); + } + } + @Test public void round() throws SolverException, InterruptedException { requireIntegers();