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

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 16ec0935c80f5bfb44e77cc4c4fd10ab1d5c7760..9b79b5c45b0f5e7abd422fb97b7f33f076619a17 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -3060,24 +3060,24 @@ const static std::
     unordered_map<RoundingMode, CVC4::RoundingMode, RoundingModeHashFunction>
         s_rmodes{
             {ROUND_NEAREST_TIES_TO_EVEN,
-             CVC4::RoundingMode::roundNearestTiesToEven},
-            {ROUND_TOWARD_POSITIVE, CVC4::RoundingMode::roundTowardPositive},
-            {ROUND_TOWARD_NEGATIVE, CVC4::RoundingMode::roundTowardNegative},
-            {ROUND_TOWARD_ZERO, CVC4::RoundingMode::roundTowardZero},
+             CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN},
+            {ROUND_TOWARD_POSITIVE, CVC4::RoundingMode::ROUND_TOWARD_POSITIVE},
+            {ROUND_TOWARD_NEGATIVE, CVC4::RoundingMode::ROUND_TOWARD_POSITIVE},
+            {ROUND_TOWARD_ZERO, CVC4::RoundingMode::ROUND_TOWARD_ZERO},
             {ROUND_NEAREST_TIES_TO_AWAY,
-             CVC4::RoundingMode::roundNearestTiesToAway},
+             CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY},
         };
 
 const static std::unordered_map<CVC4::RoundingMode,
                                 RoundingMode,
                                 CVC4::RoundingModeHashFunction>
     s_rmodes_internal{
-        {CVC4::RoundingMode::roundNearestTiesToEven,
+        {CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN,
          ROUND_NEAREST_TIES_TO_EVEN},
-        {CVC4::RoundingMode::roundTowardPositive, ROUND_TOWARD_POSITIVE},
-        {CVC4::RoundingMode::roundTowardNegative, ROUND_TOWARD_NEGATIVE},
-        {CVC4::RoundingMode::roundTowardZero, ROUND_TOWARD_ZERO},
-        {CVC4::RoundingMode::roundNearestTiesToAway,
+        {CVC4::RoundingMode::ROUND_TOWARD_POSITIVE, ROUND_TOWARD_POSITIVE},
+        {CVC4::RoundingMode::ROUND_TOWARD_POSITIVE, ROUND_TOWARD_NEGATIVE},
+        {CVC4::RoundingMode::ROUND_TOWARD_ZERO, ROUND_TOWARD_ZERO},
+        {CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY,
          ROUND_NEAREST_TIES_TO_AWAY},
     };
 

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 03b04469cc45e6f83a9f4369ff007a6e3ebf87e9..747873bee11fa781e03df3efec9bdabfea53a820 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -209,14 +209,14 @@ void Smt2Printer::toStream(std::ostream& out,
     }
     case kind::CONST_ROUNDINGMODE:
       switch (n.getConst<RoundingMode>()) {
-      case roundNearestTiesToEven : out << "roundNearestTiesToEven"; break;
-      case roundNearestTiesToAway : out << "roundNearestTiesToAway"; break;
-      case roundTowardPositive : out << "roundTowardPositive"; break;
-      case roundTowardNegative : out << "roundTowardNegative"; break;
-      case roundTowardZero : out << "roundTowardZero"; break;
-      default :
-        Unreachable() << "Invalid value of rounding mode constant ("
-                      << n.getConst<RoundingMode>() << ")";
+        case ROUND_NEAREST_TIES_TO_EVEN: out << "roundNearestTiesToEven"; break;
+        case ROUND_NEAREST_TIES_TO_AWAY: out << "roundNearestTiesToAway"; break;
+        case ROUND_TOWARD_POSITIVE: out << "roundTowardPositive"; break;
+        case ROUND_TOWARD_NEGATIVE: out << "roundTowardNegative"; break;
+        case ROUND_TOWARD_ZERO: out << "roundTowardZero"; break;
+        default:
+          Unreachable() << "Invalid value of rounding mode constant ("
+                        << n.getConst<RoundingMode>() << ")";
       }
       break;
     case kind::CONST_BOOLEAN:

diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index f7c58af7b9a9e4ed9e52bb072303755bb4090291..b8e6f381c932c120c734cf0bf59bf3ed2214f766 100644 (file)
--- 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 037b083f445b1ade79601790a9bbbfff14b7b10e..0b15486e2581ff62f18d36109dcc5eddb0f3b5a8 100644 (file)
--- 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 b56fa259c2542bebfb51937f2e202be90c55f837..78aba415bb6f62fcec984c0c87225f40d1984c82 100644 (file)
--- 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 59f643b95550ae3c1f64d6fc4237b23338d1d160..47266eda89896a89c082a6336607cae336ca21d2 100644 (file)
--- 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;

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index e5cc5460dbf91a87410d437bcad0de7bf6321c52..79fc1a36edcb724cefcfe01f5d664b44b7a98fb9 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -423,11 +423,11 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
   }
   else if (type.isRoundingMode())
   {
-    ops.push_back(nm->mkConst(RoundingMode::roundNearestTiesToAway));
-    ops.push_back(nm->mkConst(RoundingMode::roundNearestTiesToEven));
-    ops.push_back(nm->mkConst(RoundingMode::roundTowardNegative));
-    ops.push_back(nm->mkConst(RoundingMode::roundTowardPositive));
-    ops.push_back(nm->mkConst(RoundingMode::roundTowardZero));
+    ops.push_back(nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY));
+    ops.push_back(nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN));
+    ops.push_back(nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE));
+    ops.push_back(nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE));
+    ops.push_back(nm->mkConst(RoundingMode::ROUND_TOWARD_ZERO));
   }
   else if (type.isFloatingPoint())
   {

diff --git a/src/util/roundingmode.h b/src/util/roundingmode.h
index 245654a5349e5340627239c62679e3dedc2ceb6d..a1bda2988add7c18366d3c06fbaf317391426862 100644 (file)
--- a/src/util/roundingmode.h
+++ b/src/util/roundingmode.h
@@ -27,13 +27,14 @@ namespace CVC4 {
  */
 enum CVC4_PUBLIC RoundingMode
 {
-  roundNearestTiesToEven = FE_TONEAREST,
-  roundTowardPositive = FE_UPWARD,
-  roundTowardNegative = FE_DOWNWARD,
-  roundTowardZero = FE_TOWARDZERO,
+  ROUND_NEAREST_TIES_TO_EVEN = FE_TONEAREST,
+  ROUND_TOWARD_POSITIVE = FE_UPWARD,
+  ROUND_TOWARD_NEGATIVE = FE_DOWNWARD,
+  ROUND_TOWARD_ZERO = FE_TOWARDZERO,
   // Initializes this to the diagonalization of the 4 other values.
-  roundNearestTiesToAway = (((~FE_TONEAREST) & 0x1) | ((~FE_UPWARD) & 0x2)
-                            | ((~FE_DOWNWARD) & 0x4) | ((~FE_TOWARDZERO) & 0x8))
+  ROUND_NEAREST_TIES_TO_AWAY =
+      (((~FE_TONEAREST) & 0x1) | ((~FE_UPWARD) & 0x2) | ((~FE_DOWNWARD) & 0x4)
+       | ((~FE_TOWARDZERO) & 0x8))
 }; /* enum RoundingMode */
 
 /**

diff --git a/src/util/symfpu_literal.cpp b/src/util/symfpu_literal.cpp
index 46d3cbe4055cd15e960aa7ae0bac155d148acbf6..b916d62f92ea9ad79c61fe0f01ddc2a83433261c 100644 (file)
--- a/src/util/symfpu_literal.cpp
+++ b/src/util/symfpu_literal.cpp
@@ -400,11 +400,11 @@ wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(
 template class wrappedBitVector<true>;
 template class wrappedBitVector<false>;
 
-traits::rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; };
-traits::rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; };
-traits::rm traits::RTP(void) { return ::CVC4::roundTowardPositive; };
-traits::rm traits::RTN(void) { return ::CVC4::roundTowardNegative; };
-traits::rm traits::RTZ(void) { return ::CVC4::roundTowardZero; };
+traits::rm traits::RNE(void) { return ::CVC4::ROUND_NEAREST_TIES_TO_EVEN; };
+traits::rm traits::RNA(void) { return ::CVC4::ROUND_NEAREST_TIES_TO_AWAY; };
+traits::rm traits::RTP(void) { return ::CVC4::ROUND_TOWARD_POSITIVE; };
+traits::rm traits::RTN(void) { return ::CVC4::ROUND_TOWARD_NEGATIVE; };
+traits::rm traits::RTZ(void) { return ::CVC4::ROUND_TOWARD_ZERO; };
 // This is a literal back-end so props are actually bools
 // so these can be handled in the same way as the internal assertions above