RoundingMode: Rename enum values to conform to code style guidelines. (#5494)

4 files changed, 66 insertions, 67 deletions

diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index f7c58af7b..b8e6f381c 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -799,17 +799,17 @@ Node FpConverter::rmToNode(const rm &r) const
   Node value = nm->mkNode(
       kind::ITE,
       nm->mkNode(kind::EQUAL, transVar, RNE),
-      nm->mkConst(roundNearestTiesToEven),
+      nm->mkConst(ROUND_NEAREST_TIES_TO_EVEN),
       nm->mkNode(kind::ITE,
                  nm->mkNode(kind::EQUAL, transVar, RNA),
-                 nm->mkConst(roundNearestTiesToAway),
+                 nm->mkConst(ROUND_NEAREST_TIES_TO_AWAY),
                  nm->mkNode(kind::ITE,
                             nm->mkNode(kind::EQUAL, transVar, RTP),
-                            nm->mkConst(roundTowardPositive),
+                            nm->mkConst(ROUND_TOWARD_POSITIVE),
                             nm->mkNode(kind::ITE,
                                        nm->mkNode(kind::EQUAL, transVar, RTN),
-                                       nm->mkConst(roundTowardNegative),
-                                       nm->mkConst(roundTowardZero)))));
+                                       nm->mkConst(ROUND_TOWARD_NEGATIVE),
+                                       nm->mkConst(ROUND_TOWARD_ZERO)))));
   return value;
 }
 
@@ -877,19 +877,19 @@ Node FpConverter::convert(TNode node)
             /******** Constants ********/
             switch (current.getConst<RoundingMode>())
             {
-              case roundNearestTiesToEven:
+              case ROUND_NEAREST_TIES_TO_EVEN:
                 d_rmMap.insert(current, traits::RNE());
                 break;
-              case roundNearestTiesToAway:
+              case ROUND_NEAREST_TIES_TO_AWAY:
                 d_rmMap.insert(current, traits::RNA());
                 break;
-              case roundTowardPositive:
+              case ROUND_TOWARD_POSITIVE:
                 d_rmMap.insert(current, traits::RTP());
                 break;
-              case roundTowardNegative:
+              case ROUND_TOWARD_NEGATIVE:
                 d_rmMap.insert(current, traits::RTN());
                 break;
-              case roundTowardZero:
+              case ROUND_TOWARD_ZERO:
                 d_rmMap.insert(current, traits::RTZ());
                 break;
               default: Unreachable() << "Unknown rounding mode"; break;
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 037b083f4..0b15486e2 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -589,7 +589,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
           nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
                      nm->mkConst(FloatingPointToFPReal(
                          concrete[0].getType().getConst<FloatingPointSize>())),
-                     nm->mkConst(roundTowardPositive),
+                     nm->mkConst(ROUND_TOWARD_POSITIVE),
                      abstractValue));
 
       Node bg = nm->mkNode(
@@ -606,7 +606,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
           nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
                      nm->mkConst(FloatingPointToFPReal(
                          concrete[0].getType().getConst<FloatingPointSize>())),
-                     nm->mkConst(roundTowardNegative),
+                     nm->mkConst(ROUND_TOWARD_NEGATIVE),
                      abstractValue));
 
       Node bl = nm->mkNode(
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index b56fa259c..78aba415b 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -946,23 +946,23 @@ namespace constantFold {
     RoundingMode arg0(node[0].getConst<RoundingMode>());
     switch (arg0)
     {
-      case roundNearestTiesToEven:
+      case ROUND_NEAREST_TIES_TO_EVEN:
         value = symfpuSymbolic::traits::RNE().getConst<BitVector>();
         break;
 
-      case roundNearestTiesToAway:
+      case ROUND_NEAREST_TIES_TO_AWAY:
         value = symfpuSymbolic::traits::RNA().getConst<BitVector>();
         break;
 
-      case roundTowardPositive:
+      case ROUND_TOWARD_POSITIVE:
         value = symfpuSymbolic::traits::RTP().getConst<BitVector>();
         break;
 
-      case roundTowardNegative:
+      case ROUND_TOWARD_NEGATIVE:
         value = symfpuSymbolic::traits::RTN().getConst<BitVector>();
         break;
 
-      case roundTowardZero:
+      case ROUND_TOWARD_ZERO:
         value = symfpuSymbolic::traits::RTZ().getConst<BitVector>();
         break;
 
@@ -1343,58 +1343,65 @@ TheoryFpRewriter::TheoryFpRewriter()
         }
       }
 
-      if (allChildrenConst) {
-	RewriteStatus rs = REWRITE_DONE;    // This is a bit messy because
-        Node rn = res.d_node;  // RewriteResponse is too functional..
+      if (allChildrenConst)
+      {
+        RewriteStatus rs = REWRITE_DONE;  // This is a bit messy because
+        Node rn = res.d_node;             // RewriteResponse is too functional..
 
-        if (apartFromRoundingMode) {
+        if (apartFromRoundingMode)
+        {
           if (!(res.d_node.getKind() == kind::EQUAL)
               &&  // Avoid infinite recursion...
               !(res.d_node.getKind() == kind::ROUNDINGMODE_BITBLAST))
-          {  // Don't eliminate the bit-blast
+          {
+            // Don't eliminate the bit-blast
             // We are close to being able to constant fold this
             // and in many cases the rounding mode really doesn't matter.
             // So we can try brute forcing our way through them.
 
-            NodeManager *nm = NodeManager::currentNM();
+            NodeManager* nm = NodeManager::currentNM();
 
-	    Node RNE(nm->mkConst(roundNearestTiesToEven));
-	    Node RNA(nm->mkConst(roundNearestTiesToAway));
-	    Node RTZ(nm->mkConst(roundTowardPositive));
-	    Node RTN(nm->mkConst(roundTowardNegative));
-	    Node RTP(nm->mkConst(roundTowardZero));
+            Node rne(nm->mkConst(ROUND_NEAREST_TIES_TO_EVEN));
+            Node rna(nm->mkConst(ROUND_NEAREST_TIES_TO_AWAY));
+            Node rtz(nm->mkConst(ROUND_TOWARD_POSITIVE));
+            Node rtn(nm->mkConst(ROUND_TOWARD_NEGATIVE));
+            Node rtp(nm->mkConst(ROUND_TOWARD_ZERO));
 
-            TNode RM(res.d_node[0]);
+            TNode rm(res.d_node[0]);
 
-            Node wRNE(res.d_node.substitute(RM, TNode(RNE)));
-            Node wRNA(res.d_node.substitute(RM, TNode(RNA)));
-            Node wRTZ(res.d_node.substitute(RM, TNode(RTZ)));
-            Node wRTN(res.d_node.substitute(RM, TNode(RTN)));
-            Node wRTP(res.d_node.substitute(RM, TNode(RTP)));
+            Node w_rne(res.d_node.substitute(rm, TNode(rne)));
+            Node w_rna(res.d_node.substitute(rm, TNode(rna)));
+            Node w_rtz(res.d_node.substitute(rm, TNode(rtz)));
+            Node w_rtn(res.d_node.substitute(rm, TNode(rtn)));
+            Node w_rtp(res.d_node.substitute(rm, TNode(rtp)));
 
             rs = REWRITE_AGAIN_FULL;
-	    rn = nm->mkNode(kind::ITE,
-			    nm->mkNode(kind::EQUAL, RM, RNE),
-			    wRNE,
-			    nm->mkNode(kind::ITE,
-				       nm->mkNode(kind::EQUAL, RM, RNA),
-				       wRNA,
-				       nm->mkNode(kind::ITE,
-						  nm->mkNode(kind::EQUAL, RM, RTZ),
-						  wRTZ,
-						  nm->mkNode(kind::ITE,
-							     nm->mkNode(kind::EQUAL, RM, RTN),
-							     wRTN,
-							     wRTP))));
-	  }
-	} else {
+            rn = nm->mkNode(
+                kind::ITE,
+                nm->mkNode(kind::EQUAL, rm, rne),
+                w_rne,
+                nm->mkNode(
+                    kind::ITE,
+                    nm->mkNode(kind::EQUAL, rm, rna),
+                    w_rna,
+                    nm->mkNode(kind::ITE,
+                               nm->mkNode(kind::EQUAL, rm, rtz),
+                               w_rtz,
+                               nm->mkNode(kind::ITE,
+                                          nm->mkNode(kind::EQUAL, rm, rtn),
+                                          w_rtn,
+                                          w_rtp))));
+          }
+        }
+        else
+        {
           RewriteResponse tmp =
               d_constantFoldTable[res.d_node.getKind()](res.d_node, false);
           rs = tmp.d_status;
           rn = tmp.d_node;
         }
 
-	RewriteResponse constRes(rs,rn);
+        RewriteResponse constRes(rs, rn);
 
         if (constRes.d_node != res.d_node)
         {
diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h
index 59f643b95..47266eda8 100644
--- a/src/theory/fp/type_enumerator.h
+++ b/src/theory/fp/type_enumerator.h
@@ -86,8 +86,10 @@ class RoundingModeEnumerator
  public:
   RoundingModeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
       : TypeEnumeratorBase<RoundingModeEnumerator>(type),
-        d_rm(roundNearestTiesToEven),
-        d_enumerationComplete(false) {}
+        d_rm(ROUND_NEAREST_TIES_TO_EVEN),
+        d_enumerationComplete(false)
+  {
+  }
 
   /** Throws NoMoreValuesException if the enumeration is complete. */
   Node operator*() override {
@@ -99,21 +101,11 @@ class RoundingModeEnumerator
 
   RoundingModeEnumerator& operator++() override {
     switch (d_rm) {
-      case roundNearestTiesToEven:
-        d_rm = roundTowardPositive;
-        break;
-      case roundTowardPositive:
-        d_rm = roundTowardNegative;
-        break;
-      case roundTowardNegative:
-        d_rm = roundTowardZero;
-        break;
-      case roundTowardZero:
-        d_rm = roundNearestTiesToAway;
-        break;
-      case roundNearestTiesToAway:
-        d_enumerationComplete = true;
-        break;
+      case ROUND_NEAREST_TIES_TO_EVEN: d_rm = ROUND_TOWARD_POSITIVE; break;
+      case ROUND_TOWARD_POSITIVE: d_rm = ROUND_TOWARD_NEGATIVE; break;
+      case ROUND_TOWARD_NEGATIVE: d_rm = ROUND_TOWARD_ZERO; break;
+      case ROUND_TOWARD_ZERO: d_rm = ROUND_NEAREST_TIES_TO_AWAY; break;
+      case ROUND_NEAREST_TIES_TO_AWAY: d_enumerationComplete = true; break;
       default: Unreachable() << "Unknown rounding mode?"; break;
     }
     return *this;