RoundingMode: Fix visitors for rounding mode formulas

Author: daniel-raffler

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);

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> R visit(FormulaVisitor<R> 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));
+    }
+  }
 }

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> R visit(FormulaVisitor<R> 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(

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> R visit(FormulaVisitor<R> 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;