1 files changed, 31 insertions, 29 deletions

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 42b7da248..ba1b47b4a 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -24,11 +24,11 @@
 #include "base/check.h"
 #include "expr/kind.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 namespace expr {
   class NodeValue;
-}/* CVC4::expr namespace */
+  }  // namespace expr
 
 namespace kind {
 namespace metakind {
@@ -74,16 +74,16 @@ struct ConstantMapReverse;
  */
 template <Kind k, bool pool>
 struct NodeValueConstCompare {
-  inline static bool compare(const ::CVC4::expr::NodeValue* x,
-                             const ::CVC4::expr::NodeValue* y);
-  inline static size_t constHash(const ::CVC4::expr::NodeValue* nv);
+  inline static bool compare(const ::CVC5::expr::NodeValue* x,
+                             const ::CVC5::expr::NodeValue* y);
+  inline static size_t constHash(const ::CVC5::expr::NodeValue* nv);
 };/* NodeValueConstCompare<k, pool> */
 
 struct NodeValueCompare {
   template <bool pool>
-  static bool compare(const ::CVC4::expr::NodeValue* nv1,
-                      const ::CVC4::expr::NodeValue* nv2);
-  static size_t constHash(const ::CVC4::expr::NodeValue* nv);
+  static bool compare(const ::CVC5::expr::NodeValue* nv1,
+                      const ::CVC5::expr::NodeValue* nv2);
+  static size_t constHash(const ::CVC5::expr::NodeValue* nv);
 };/* struct NodeValueCompare */
 
 /**
@@ -102,29 +102,29 @@ enum MetaKind_t {
   NULLARY_OPERATOR /**< nullary operator */
 };/* enum MetaKind_t */
 
-}/* CVC4::kind::metakind namespace */
+}  // namespace metakind
 
-// import MetaKind into the "CVC4::kind" namespace but keep the
+// import MetaKind into the "CVC5::kind" namespace but keep the
 // individual MetaKind constants under kind::metakind::
-typedef ::CVC4::kind::metakind::MetaKind_t MetaKind;
+typedef ::CVC5::kind::metakind::MetaKind_t MetaKind;
 
 /**
  * Get the metakind for a particular kind.
  */
 MetaKind metaKindOf(Kind k);
-}/* CVC4::kind namespace */
+}  // namespace kind
 
 namespace expr {
 
 // Comparison predicate
 struct NodeValuePoolEq {
   inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
-    return ::CVC4::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2);
+    return ::CVC5::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2);
   }
 };
 
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
+}  // namespace expr
+}  // namespace CVC5
 
 #include "expr/node_value.h"
 
@@ -134,18 +134,19 @@ ${metakind_includes}
 
 #ifdef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
 
-namespace CVC4 {
+namespace CVC5 {
 
 namespace expr {
 ${metakind_getConst_decls}
-}/* CVC4::expr namespace */
+}  // namespace expr
 
 namespace kind {
 namespace metakind {
 
 template <Kind k, bool pool>
-inline bool NodeValueConstCompare<k, pool>::compare(const ::CVC4::expr::NodeValue* x,
-                                                    const ::CVC4::expr::NodeValue* y) {
+inline bool NodeValueConstCompare<k, pool>::compare(
+    const ::CVC5::expr::NodeValue* x, const ::CVC5::expr::NodeValue* y)
+{
   typedef typename ConstantMapReverse<k>::T T;
   if(pool) {
     if(x->d_nchildren == 1) {
@@ -163,7 +164,9 @@ inline bool NodeValueConstCompare<k, pool>::compare(const ::CVC4::expr::NodeValu
 }
 
 template <Kind k, bool pool>
-inline size_t NodeValueConstCompare<k, pool>::constHash(const ::CVC4::expr::NodeValue* nv) {
+inline size_t NodeValueConstCompare<k, pool>::constHash(
+    const ::CVC5::expr::NodeValue* nv)
+{
   typedef typename ConstantMapReverse<k>::T T;
   return nv->getConst<T>().hash();
 }
@@ -171,8 +174,7 @@ inline size_t NodeValueConstCompare<k, pool>::constHash(const ::CVC4::expr::Node
 ${metakind_constantMaps_decls}
 
 struct NodeValueConstPrinter {
-  static void toStream(std::ostream& out,
-                              const ::CVC4::expr::NodeValue* nv);
+  static void toStream(std::ostream& out, const ::CVC5::expr::NodeValue* nv);
   static void toStream(std::ostream& out, TNode n);
 };
 
@@ -185,24 +187,24 @@ struct NodeValueConstPrinter {
  * This doesn't support "non-inlined" NodeValues, which shouldn't need this
  * kind of cleanup.
  */
-void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv);
+void deleteNodeValueConstant(::CVC5::expr::NodeValue* nv);
 
 /** Return the minimum arity of the given kind. */
-uint32_t getMinArityForKind(::CVC4::Kind k);
+uint32_t getMinArityForKind(::CVC5::Kind k);
 /** Return the maximum arity of the given kind. */
-uint32_t getMaxArityForKind(::CVC4::Kind k);
+uint32_t getMaxArityForKind(::CVC5::Kind k);
 
-}/* CVC4::kind::metakind namespace */
+}  // namespace metakind
 
 /**
  * Map a kind of the operator to the kind of the enclosing expression. For
  * example, since the kind of functions is just VARIABLE, it should map
  * VARIABLE to APPLY_UF.
  */
-Kind operatorToKind(::CVC4::expr::NodeValue* nv);
+Kind operatorToKind(::CVC5::expr::NodeValue* nv);
 
-}/* CVC4::kind namespace */
+}  // namespace kind
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */