RoundingMode: Remove Kinds for specific rounding modes from FunctionDeclarationKind and treat them as atomic values instead

Author: daniel-raffler

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,
 

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: