Skip to content

Commit d181f60

Browse files
kfriedbergerkfriedberger
committed
extend API with method for retrieving RoundingMode from the corresponding formula.
1 parent 8d98bd1 commit d181f60

14 files changed

+171
-54
lines changed

‎src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
// an API wrapper for a collection of SMT solvers:
33
// https://github.com/sosy-lab/java-smt
44
//
5-
// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
5+
// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
66
//
77
// SPDX-License-Identifier: Apache-2.0
88

@@ -37,6 +37,13 @@ public interface FloatingPointFormulaManager {
3737
/** Creates a formula for the given floating point rounding mode. */
3838
FloatingPointRoundingModeFormula makeRoundingMode(FloatingPointRoundingMode pRoundingMode);
3939

40+
/**
41+
* Converts a rounding mode formula to the corresponding enum value. This method is the inverse of
42+
* {@link #makeRoundingMode(FloatingPointRoundingMode)}.
43+
*/
44+
FloatingPointRoundingMode fromRoundingModeFormula(
45+
FloatingPointRoundingModeFormula pRoundingModeFormula);
46+
4047
/**
4148
* Creates a floating point formula representing the given double value with the specified type.
4249
*/

‎src/org/sosy_lab/java_smt/api/FloatingPointRoundingMode.java‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,13 +2,17 @@
22
// an API wrapper for a collection of SMT solvers:
33
// https://github.com/sosy-lab/java-smt
44
//
5-
// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
5+
// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
66
//
77
// SPDX-License-Identifier: Apache-2.0
88

99
package org.sosy_lab.java_smt.api;
1010

11-
/** Possible floating point rounding modes. */
11+
/**
12+
* Represents the various rounding modes that can be applied when converting or manipulating
13+
* floating-point values and formulas. These modes define how results are rounded when an exact
14+
* representation is not possible due to precision limits of the target format.
15+
*/
1216
public enum FloatingPointRoundingMode {
1317
NEAREST_TIES_TO_EVEN,
1418
NEAREST_TIES_AWAY,

‎src/org/sosy_lab/java_smt/api/FloatingPointRoundingModeFormula.java‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,10 @@
1616
* <p>Rounding mode formulas are used by floating-point formulas to select the rounding mode for the
1717
* operation. Use {@link FloatingPointFormulaManager#makeRoundingMode(FloatingPointRoundingMode)} to
1818
* wrap a {@link org.sosy_lab.java_smt.api.FloatingPointRoundingMode} value inside a new formula.
19+
*
20+
* <p>This class is rarely used in the API but necessary to support visitor traversal of formulas
21+
* with certain floating-point operations, where JavaSMT provides the rounding mode as Formula-based
22+
* argument.
1923
*/
2024
@Immutable
2125
public interface FloatingPointRoundingModeFormula extends Formula {}

‎src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,12 @@ public FloatingPointRoundingModeFormula makeRoundingMode(
6767
return getFormulaCreator().encapsulateRoundingMode(getRoundingMode(pRoundingMode));
6868
}
6969

70+
@Override
71+
public FloatingPointRoundingMode fromRoundingModeFormula(
72+
FloatingPointRoundingModeFormula pRoundingModeFormula) {
73+
return getFormulaCreator().getRoundingMode(extractInfo(pRoundingModeFormula));
74+
}
75+
7076
protected FloatingPointFormula wrap(TFormulaInfo pTerm) {
7177
return getFormulaCreator().encapsulateFloatingPoint(pTerm);
7278
}

‎src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@
3131
import org.sosy_lab.java_smt.api.BooleanFormula;
3232
import org.sosy_lab.java_smt.api.EnumerationFormula;
3333
import org.sosy_lab.java_smt.api.FloatingPointFormula;
34+
import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
3435
import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula;
3536
import org.sosy_lab.java_smt.api.Formula;
3637
import org.sosy_lab.java_smt.api.FormulaType;
@@ -134,6 +135,15 @@ public final TType getRegexType() {
134135
return regexType;
135136
}
136137

138+
public FloatingPointRoundingMode getRoundingMode(FloatingPointRoundingModeFormula f) {
139+
return getRoundingMode(extractInfo(f));
140+
}
141+
142+
protected FloatingPointRoundingMode getRoundingMode(TFormulaInfo f) {
143+
throw new UnsupportedOperationException(
144+
"Floating point rounding modes are not supported by this solver.");
145+
}
146+
137147
public abstract TFormulaInfo makeVariable(TType type, String varName);
138148

139149
public BooleanFormula encapsulateBoolean(TFormulaInfo pTerm) {

‎src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFloatingPointFormulaManager.java‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,14 @@ public FloatingPointRoundingModeFormula makeRoundingMode(
4141
return result;
4242
}
4343

44+
@Override
45+
public FloatingPointRoundingMode fromRoundingModeFormula(
46+
FloatingPointRoundingModeFormula pRoundingModeFormula) {
47+
debugging.assertThreadLocal();
48+
debugging.assertFormulaInContext(pRoundingModeFormula);
49+
return delegate.fromRoundingModeFormula(pRoundingModeFormula);
50+
}
51+
4452
@Override
4553
public FloatingPointFormula makeNumber(double n, FloatingPointType type) {
4654
debugging.assertThreadLocal();

‎src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,13 @@ public FloatingPointRoundingModeFormula makeRoundingMode(
4242
return delegate.makeRoundingMode(pRoundingMode);
4343
}
4444

45+
@Override
46+
public FloatingPointRoundingMode fromRoundingModeFormula(
47+
FloatingPointRoundingModeFormula pRoundingModeFormula) {
48+
stats.fpOperations.getAndIncrement();
49+
return delegate.fromRoundingModeFormula(pRoundingModeFormula);
50+
}
51+
4552
@Override
4653
public FloatingPointFormula makeNumber(double pN, FloatingPointType pType) {
4754
stats.fpOperations.getAndIncrement();

‎src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,14 @@ public FloatingPointRoundingModeFormula makeRoundingMode(
4444
}
4545
}
4646

47+
@Override
48+
public FloatingPointRoundingMode fromRoundingModeFormula(
49+
FloatingPointRoundingModeFormula pRoundingModeFormula) {
50+
synchronized (sync) {
51+
return delegate.fromRoundingModeFormula(pRoundingModeFormula);
52+
}
53+
}
54+
4755
@Override
4856
public FloatingPointFormula makeNumber(double pN, FloatingPointType pType) {
4957
synchronized (sync) {

‎src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java‎

Lines changed: 20 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -594,19 +594,7 @@ public Object convertValue(Term term) {
594594
return term.to_bool();
595595
}
596596
if (sort.is_rm()) {
597-
if (term.is_rm_value_rna()) {
598-
return FloatingPointRoundingMode.NEAREST_TIES_AWAY;
599-
} else if (term.is_rm_value_rne()) {
600-
return FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN;
601-
} else if (term.is_rm_value_rtn()) {
602-
return FloatingPointRoundingMode.TOWARD_NEGATIVE;
603-
} else if (term.is_rm_value_rtp()) {
604-
return FloatingPointRoundingMode.TOWARD_POSITIVE;
605-
} else if (term.is_rm_value_rtz()) {
606-
return FloatingPointRoundingMode.TOWARD_ZERO;
607-
} else {
608-
throw new IllegalArgumentException(String.format("Unknown rounding mode: %s", term));
609-
}
597+
return getRoundingMode(term);
610598
}
611599
if (sort.is_bv()) {
612600
return new BigInteger(term.to_bv(), 2);
@@ -649,4 +637,23 @@ public Collection<Term> getConstraintsForTerm(Term pTerm) {
649637

650638
return transformedImmutableSetCopy(usedConstraintVariables, constraintsForVariables::get);
651639
}
640+
641+
@Override
642+
protected FloatingPointRoundingMode getRoundingMode(Term term) {
643+
checkArgument(term.sort().is_rm(), "Term '%s' is not of rounding mode sort.", term);
644+
if (term.is_rm_value_rna()) {
645+
return FloatingPointRoundingMode.NEAREST_TIES_AWAY;
646+
} else if (term.is_rm_value_rne()) {
647+
return FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN;
648+
} else if (term.is_rm_value_rtn()) {
649+
return FloatingPointRoundingMode.TOWARD_NEGATIVE;
650+
} else if (term.is_rm_value_rtp()) {
651+
return FloatingPointRoundingMode.TOWARD_POSITIVE;
652+
} else if (term.is_rm_value_rtz()) {
653+
return FloatingPointRoundingMode.TOWARD_ZERO;
654+
} else {
655+
throw new IllegalArgumentException(
656+
String.format("Unknown rounding mode in Term '%s'.", term));
657+
}
658+
}
652659
}

‎src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java‎

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -335,7 +335,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Expr f) {
335335
} else if (type.isFloatingPoint()) {
336336
return visitor.visitConstant(formula, convertFloatingPoint(f));
337337
} else if (type.isRoundingMode()) {
338-
return visitor.visitConstant(formula, convertRoundingMode(f));
338+
return visitor.visitConstant(formula, getRoundingMode(f));
339339
} else if (type.isString()) {
340340
return visitor.visitConstant(formula, f.getConstString());
341341
} else if (type.isArray()) {
@@ -626,7 +626,7 @@ public Object convertValue(Expr expForType, Expr value) {
626626
return convertFloatingPoint(value);
627627

628628
} else if (valueType.isRoundingMode()) {
629-
return convertRoundingMode(value);
629+
return getRoundingMode(value);
630630

631631
} else if (valueType.isString()) {
632632
return unescapeUnicodeForSmtlib(value.getConstString().toString());
@@ -664,7 +664,12 @@ private FloatingPointNumber convertFloatingPoint(Expr fpExpr) {
664664
mantWidth);
665665
}
666666

667-
private FloatingPointRoundingMode convertRoundingMode(Expr pExpr) {
667+
@Override
668+
protected FloatingPointRoundingMode getRoundingMode(Expr pExpr) {
669+
checkArgument(
670+
pExpr.isConst() && pExpr.getType().isRoundingMode(),
671+
"Expected a constant rounding mode, but got: %s",
672+
pExpr);
668673
RoundingMode rm = pExpr.getConstRoundingMode();
669674
if (rm.equals(RoundingMode.roundNearestTiesToAway)) {
670675
return FloatingPointRoundingMode.NEAREST_TIES_AWAY;
@@ -677,7 +682,8 @@ private FloatingPointRoundingMode convertRoundingMode(Expr pExpr) {
677682
} else if (rm.equals(RoundingMode.roundTowardZero)) {
678683
return FloatingPointRoundingMode.TOWARD_ZERO;
679684
} else {
680-
throw new IllegalArgumentException(String.format("Unknown rounding mode: %s", pExpr));
685+
throw new IllegalArgumentException(
686+
String.format("Unknown rounding mode in Term '%s'.", pExpr));
681687
}
682688
}
683689
}

0 commit comments

Comments
 (0)