Rename namespace CVC4 to CVC5. (#6249)

author: Aina Niemetz <aina.niemetz@gmail.com> 2021-03-31 15:23:17 -0700
committer: GitHub <noreply@github.com> 2021-03-31 22:23:17 +0000
commit: a1466978fbc328507406d4a121dab4d1a1047e1d (patch)
tree: 12b40f161bb4d7a6ee40c20c78a15d6cda3c1995 /src/expr
parent: f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff)
115 files changed, 427 insertions, 424 deletions
diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index 6d14ac40d..d50921598 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -26,7 +26,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 
 ArrayStoreAll::ArrayStoreAll(const TypeNode& type, const Node& value)
     : d_type(), d_value()
@@ -115,4 +115,4 @@ size_t ArrayStoreAllHashFunction::operator()(const ArrayStoreAll& asa) const {
          * NodeHashFunction()(asa.getValue());
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h
index dac967668..974f456ef 100644
--- a/src/expr/array_store_all.h
+++ b/src/expr/array_store_all.h
@@ -24,8 +24,7 @@
 #include <iosfwd>
 #include <memory>
 
-
-namespace CVC4 {
+namespace CVC5 {
 
 template <bool ref_count>
 class NodeTemplate;
@@ -70,6 +69,6 @@ struct ArrayStoreAllHashFunction
   size_t operator()(const ArrayStoreAll& asa) const;
 }; /* struct ArrayStoreAllHashFunction */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__ARRAY_STORE_ALL_H */
diff --git a/src/expr/ascription_type.cpp b/src/expr/ascription_type.cpp
index 6f50568f1..6fecb2978 100644
--- a/src/expr/ascription_type.cpp
+++ b/src/expr/ascription_type.cpp
@@ -18,7 +18,7 @@
 
 #include "expr/type_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 AscriptionType::AscriptionType(TypeNode t) : d_type(new TypeNode(t)) {}
 
@@ -55,4 +55,4 @@ std::ostream& operator<<(std::ostream& out, AscriptionType at)
   return out;
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h
index 66f376b18..5b0ff2b71 100644
--- a/src/expr/ascription_type.h
+++ b/src/expr/ascription_type.h
@@ -22,7 +22,7 @@
 #include <iosfwd>
 #include <memory>
 
-namespace CVC4 {
+namespace CVC5 {
 
 class TypeNode;
 
@@ -60,6 +60,6 @@ struct AscriptionTypeHashFunction
 /** An output routine for AscriptionTypes */
 std::ostream& operator<<(std::ostream& out, AscriptionType at);
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__ASCRIPTION_TYPE_H */
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 5973aab17..fe1bff897 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -22,7 +22,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 namespace attr {
 
@@ -114,6 +114,6 @@ void AttributeManager::deleteAttributes(const AttrIdVec& atids) {
   }
 }
 
-}/* CVC4::expr::attr namespace */
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
+}  // namespace attr
+}  // namespace expr
+}  // namespace CVC5
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 9a1f4682e..b3a3eb717 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -32,7 +32,7 @@
 #include "expr/attribute_internals.h"
 #undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 namespace attr {
 
@@ -218,7 +218,7 @@ public:
   void debugHook(int debugFlag);
 };
 
-}/* CVC4::expr::attr namespace */
+}  // namespace attr
 
 // MAPPING OF ATTRIBUTE KINDS TO TABLES IN THE ATTRIBUTE MANAGER ===============
 
@@ -318,7 +318,7 @@ struct getTable<std::string, false> {
   }
 };
 
-}/* CVC4::expr::attr namespace */
+}  // namespace attr
 
 // ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
 
@@ -540,9 +540,8 @@ void AttributeManager::reconstructTable(AttrHash<T>& table){
   d_inGarbageCollection = false;
 }
 
-
-}/* CVC4::expr::attr namespace */
-}/* CVC4::expr namespace */
+}  // namespace attr
+}  // namespace expr
 
 template <class AttrKind>
 inline typename AttrKind::value_type
@@ -622,6 +621,6 @@ NodeManager::setAttribute(TypeNode n, const AttrKind&,
   d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__ATTRIBUTE_H */
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index 271c34d3c..bbd5455be 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -25,7 +25,7 @@
 
 #include <unordered_map>
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 // ATTRIBUTE HASH FUNCTIONS ====================================================
@@ -54,7 +54,7 @@ struct AttrBoolHashFunction {
   }
 };/* struct AttrBoolHashFunction */
 
-}/* CVC4::expr::attr namespace */
+}  // namespace attr
 
 // ATTRIBUTE TYPE MAPPINGS =====================================================
 
@@ -131,7 +131,7 @@ struct KindValueToTableValueMapping<
   static T convertBack(const uint64_t& t) { return static_cast<T>(t); }
 };
 
-}/* CVC4::expr::attr namespace */
+}  // namespace attr
 
 // ATTRIBUTE HASH TABLES =======================================================
 
@@ -363,7 +363,7 @@ public:
   }
 };/* class AttrHash<bool> */
 
-}/* CVC4::expr::attr namespace */
+}  // namespace attr
 
 // ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ====================================
 
@@ -393,7 +393,7 @@ struct LastAttributeId {
   }
 };
 
-}/* CVC4::expr::attr namespace */
+}  // namespace attr
 
 // ATTRIBUTE DEFINITION ========================================================
 
@@ -511,7 +511,7 @@ template <class T, bool context_dep>
 const uint64_t Attribute<T, bool, context_dep>::s_id =
     Attribute<T, bool, context_dep>::registerAttribute();
 
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
+}  // namespace expr
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__ATTRIBUTE_INTERNALS_H */
diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h
index 247e0b1f1..f084baaa1 100644
--- a/src/expr/attribute_unique_id.h
+++ b/src/expr/attribute_unique_id.h
@@ -21,7 +21,7 @@
 
 // ATTRIBUTE IDs ============================================================
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 namespace attr {
 
@@ -59,8 +59,8 @@ public:
   AttrTableId getTableId() const{ return d_tableId; }
   uint64_t getWithinTypeId() const{ return d_withinTypeId; }
 
-};/* CVC4::expr::attr::AttributeUniqueId */
+}; /* CVC5::expr::attr::AttributeUniqueId */
 
-}/* CVC4::expr::attr namespace */
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
+}  // namespace attr
+}  // namespace expr
+}  // namespace CVC5
diff --git a/src/expr/bound_var_manager.cpp b/src/expr/bound_var_manager.cpp
index 36b824c31..ca257d313 100644
--- a/src/expr/bound_var_manager.cpp
+++ b/src/expr/bound_var_manager.cpp
@@ -16,7 +16,7 @@
 
 #include "expr/node_manager_attributes.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 BoundVarManager::BoundVarManager() : d_keepCacheVals(false) {}
 
@@ -53,4 +53,4 @@ Node BoundVarManager::getCacheValue(TNode cv, size_t i)
   return getCacheValue(cv, getCacheValue(i));
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h
index 16ff97cce..08705f6d2 100644
--- a/src/expr/bound_var_manager.h
+++ b/src/expr/bound_var_manager.h
@@ -22,7 +22,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * Bound variable manager.
@@ -98,6 +98,6 @@ class BoundVarManager
   std::unordered_set<Node, NodeHashFunction> d_cacheVals;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__BOUND_VAR_MANAGER_H */
diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp
index b1abee0d0..caf6b0841 100644
--- a/src/expr/buffered_proof_generator.cpp
+++ b/src/expr/buffered_proof_generator.cpp
@@ -17,7 +17,7 @@
 #include "expr/proof.h"
 #include "expr/proof_node_manager.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 BufferedProofGenerator::BufferedProofGenerator(context::Context* c,
                                                ProofNodeManager* pnm)
@@ -80,4 +80,4 @@ std::shared_ptr<ProofNode> BufferedProofGenerator::getProofFor(Node fact)
   return cdp.getProofFor(fact);
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h
index 4b46aa56a..db8e50274 100644
--- a/src/expr/buffered_proof_generator.h
+++ b/src/expr/buffered_proof_generator.h
@@ -20,7 +20,7 @@
 #include "context/cdhashmap.h"
 #include "expr/proof_generator.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofNodeManager;
 class ProofStep;
@@ -57,6 +57,6 @@ class BufferedProofGenerator : public ProofGenerator
   ProofNodeManager* d_pnm;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H */
diff --git a/src/expr/datatype_index.cpp b/src/expr/datatype_index.cpp
index 5f9d782ad..2459c86d8 100644
--- a/src/expr/datatype_index.cpp
+++ b/src/expr/datatype_index.cpp
@@ -20,7 +20,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 
 DatatypeIndexConstant::DatatypeIndexConstant(uint32_t index) : d_index(index) {}
 std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic)
@@ -34,4 +34,4 @@ size_t DatatypeIndexConstantHashFunction::operator()(
   return IntegerHashFunction()(dic.getIndex());
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/datatype_index.h b/src/expr/datatype_index.h
index 6020759fb..08d33ca83 100644
--- a/src/expr/datatype_index.h
+++ b/src/expr/datatype_index.h
@@ -19,7 +19,7 @@
 
 #include <iosfwd>
 
-namespace CVC4 {
+namespace CVC5 {
 
 /* stores an index to Datatype residing in NodeManager */
 class DatatypeIndexConstant
@@ -64,6 +64,6 @@ struct DatatypeIndexConstantHashFunction
   size_t operator()(const DatatypeIndexConstant& dic) const;
 }; /* struct DatatypeIndexConstantHashFunction */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__DATATYPE_H */
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 162afd84a..35ad5ff4c 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -19,9 +19,9 @@
 #include "expr/node_algorithm.h"
 #include "expr/type_matcher.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 
 DType::DType(std::string name, bool isCo)
     : d_name(name),
@@ -954,4 +954,4 @@ std::ostream& operator<<(std::ostream& out, const DTypeIndexConstant& dic)
   return out << "index_" << dic.getIndex();
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index 18694bf64..5b6ec4a7d 100644
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -24,7 +24,7 @@
 #include "expr/node.h"
 #include "expr/type_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 // ----------------------- datatype attributes
 /**
@@ -696,6 +696,6 @@ struct DTypeIndexConstantHashFunction
 
 std::ostream& operator<<(std::ostream& os, const DType& dt);
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index d02435465..089d41637 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -18,10 +18,10 @@
 #include "expr/type_matcher.h"
 #include "options/datatypes_options.h"
 
-using namespace CVC4::kind;
-using namespace CVC4::theory;
+using namespace CVC5::kind;
+using namespace CVC5::theory;
 
-namespace CVC4 {
+namespace CVC5 {
 
 DTypeConstructor::DTypeConstructor(std::string name,
                                    unsigned weight)
@@ -693,4 +693,4 @@ std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor)
   return os;
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h
index dd9fc6a0b..245d461b0 100644
--- a/src/expr/dtype_cons.h
+++ b/src/expr/dtype_cons.h
@@ -24,7 +24,7 @@
 #include "expr/node.h"
 #include "expr/type_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * The Node-level representation of a constructor for a datatype, which
@@ -371,6 +371,6 @@ struct DTypeConstructorHashFunction
 
 std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor);
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp
index 522e6b4c1..a276c3734 100644
--- a/src/expr/dtype_selector.cpp
+++ b/src/expr/dtype_selector.cpp
@@ -16,9 +16,9 @@
 
 #include "options/set_language.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 
 DTypeSelector::DTypeSelector(std::string name, Node selector)
     : d_name(name), d_selector(selector), d_resolved(false)
@@ -83,4 +83,4 @@ std::ostream& operator<<(std::ostream& os, const DTypeSelector& arg)
   return os;
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/dtype_selector.h b/src/expr/dtype_selector.h
index b134c7f7d..7404c0c96 100644
--- a/src/expr/dtype_selector.h
+++ b/src/expr/dtype_selector.h
@@ -21,7 +21,7 @@
 #include "expr/node.h"
 #include "expr/type_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class DatatypeConstructorArg;
 class DType;
@@ -90,6 +90,6 @@ class DTypeSelector
 
 std::ostream& operator<<(std::ostream& os, const DTypeSelector& arg);
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/expr/emptybag.cpp b/src/expr/emptybag.cpp
index d23ccef09..0f7a3a73e 100644
--- a/src/expr/emptybag.cpp
+++ b/src/expr/emptybag.cpp
@@ -18,7 +18,7 @@
 
 #include "expr/type_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 std::ostream& operator<<(std::ostream& out, const EmptyBag& asa)
 {
@@ -64,4 +64,4 @@ bool EmptyBag::operator<=(const EmptyBag& es) const
 
 bool EmptyBag::operator>(const EmptyBag& es) const { return !(*this <= es); }
 bool EmptyBag::operator>=(const EmptyBag& es) const { return !(*this < es); }
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/emptybag.h b/src/expr/emptybag.h
index e9763108e..59060eaa8 100644
--- a/src/expr/emptybag.h
+++ b/src/expr/emptybag.h
@@ -20,7 +20,7 @@
 #include <iosfwd>
 #include <memory>
 
-namespace CVC4 {
+namespace CVC5 {
 
 class TypeNode;
 
@@ -58,6 +58,6 @@ struct EmptyBagHashFunction
   size_t operator()(const EmptyBag& es) const;
 }; /* struct EmptyBagHashFunction */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EMPTY_BAG_H */
diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp
index 97a986054..4a0bd4e51 100644
--- a/src/expr/emptyset.cpp
+++ b/src/expr/emptyset.cpp
@@ -21,7 +21,7 @@
 
 #include "expr/type_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 std::ostream& operator<<(std::ostream& out, const EmptySet& asa) {
   return out << "emptyset(" << asa.getType() << ')';
@@ -64,4 +64,4 @@ bool EmptySet::operator<=(const EmptySet& es) const
 
 bool EmptySet::operator>(const EmptySet& es) const { return !(*this <= es); }
 bool EmptySet::operator>=(const EmptySet& es) const { return !(*this < es); }
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h
index 1c441e519..febb4e111 100644
--- a/src/expr/emptyset.h
+++ b/src/expr/emptyset.h
@@ -23,7 +23,7 @@
 #include <iosfwd>
 #include <memory>
 
-namespace CVC4 {
+namespace CVC5 {
 
 class TypeNode;
 
@@ -60,6 +60,6 @@ struct EmptySetHashFunction
   size_t operator()(const EmptySet& es) const;
 }; /* struct EmptySetHashFunction */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EMPTY_SET_H */
diff --git a/src/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp
index 82ac83d33..4aec28b85 100644
--- a/src/expr/expr_iomanip.cpp
+++ b/src/expr/expr_iomanip.cpp
@@ -22,7 +22,7 @@
 #include "options/options.h"
 #include "options/expr_options.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc();
@@ -122,6 +122,5 @@ std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) {
   return out;
 }
 
-
-}/* namespace CVC4::expr */
-}/* namespace CVC4 */
+}  // namespace expr
+} // namespace CVC5
diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h
index 5306e2a2b..c40840cd4 100644
--- a/src/expr/expr_iomanip.h
+++ b/src/expr/expr_iomanip.h
@@ -21,7 +21,7 @@
 
 #include <iosfwd>
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 /**
@@ -171,8 +171,8 @@ std::ostream& operator<<(std::ostream& out, ExprDag d);
  */
 std::ostream& operator<<(std::ostream& out, ExprSetDepth sd);
 
-}/* namespace CVC4::expr */
+}  // namespace expr
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__EXPR_IOMANIP_H */
diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h
index d118b7077..e6f6f9ca0 100644
--- a/src/expr/kind_map.h
+++ b/src/expr/kind_map.h
@@ -25,7 +25,7 @@
 #include "base/check.h"
 #include "expr/kind.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /** A very simple bitmap for Kinds */
 class KindMap
@@ -51,6 +51,6 @@ class KindMap
   std::bitset<kind::LAST_KIND> d_bits;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__KIND_MAP_H */
diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp
index 0aff7a79b..cbe979642 100644
--- a/src/expr/kind_template.cpp
+++ b/src/expr/kind_template.cpp
@@ -19,12 +19,12 @@
 
 #include "expr/kind.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace kind {
 
-const char* toString(CVC4::Kind k)
+const char* toString(CVC5::Kind k)
 {
-  using namespace CVC4::kind;
+  using namespace CVC5::kind;
 
   switch (k)
   {
@@ -37,7 +37,7 @@ const char* toString(CVC4::Kind k)
   }
 }
 
-std::ostream& operator<<(std::ostream& out, CVC4::Kind k)
+std::ostream& operator<<(std::ostream& out, CVC5::Kind k)
 {
   out << toString(k);
   return out;
@@ -47,7 +47,8 @@ std::ostream& operator<<(std::ostream& out, CVC4::Kind k)
  * decide whether it's safe to modify big expressions by changing the grouping of
  * the arguments. */
 /* TODO: This could be generated. */
-bool isAssociative(::CVC4::Kind k) {
+bool isAssociative(::CVC5::Kind k)
+{
   switch(k) {
   case kind::AND:
   case kind::OR:
@@ -60,13 +61,14 @@ bool isAssociative(::CVC4::Kind k) {
   }
 }
 
-std::string kindToString(::CVC4::Kind k) {
+std::string kindToString(::CVC5::Kind k)
+{
   std::stringstream ss;
   ss << k;
   return ss.str();
 }
 
-}/* CVC4::kind namespace */
+}  // namespace kind
 
 std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
   switch(typeConstant) {
@@ -80,7 +82,8 @@ ${type_constant_descriptions}
 
 namespace theory {
 
-TheoryId kindToTheoryId(::CVC4::Kind k) {
+TheoryId kindToTheoryId(::CVC5::Kind k)
+{
   switch(k) {
   case kind::UNDEFINED_KIND:
   case kind::NULL_EXPR:
@@ -92,7 +95,7 @@ ${kind_to_theory_id}
   throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
 }
 
-TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant)
+TheoryId typeConstantToTheoryId(::CVC5::TypeConstant typeConstant)
 {
   switch (typeConstant)
   {
@@ -103,5 +106,5 @@ ${type_constant_to_theory_id}
       "", "k", __PRETTY_FUNCTION__, "bad type constant");
 }
 
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace theory
+}  // namespace CVC5
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index ccb7656a9..4661cfa15 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -24,7 +24,7 @@
 #include "base/exception.h"
 #include "theory/theory_id.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace kind {
 
 enum Kind_t
@@ -35,11 +35,11 @@ enum Kind_t
 
 }; /* enum Kind_t */
 
-}/* CVC4::kind namespace */
+}  // namespace kind
 
 // import Kind into the "CVC4" namespace but keep the individual kind
 // constants under kind::
-typedef ::CVC4::kind::Kind_t Kind;
+typedef ::CVC5::kind::Kind_t Kind;
 
 namespace kind {
 
@@ -52,7 +52,7 @@ namespace kind {
  * @param k The kind
  * @return The name of the kind
  */
-const char* toString(CVC4::Kind k);
+const char* toString(CVC5::Kind k);
 
 /**
  * Writes a kind name to a stream.
@@ -61,22 +61,20 @@ const char* toString(CVC4::Kind k);
  * @param k The kind to write to the stream
  * @return The stream
  */
-std::ostream& operator<<(std::ostream&, CVC4::Kind);
+std::ostream& operator<<(std::ostream&, CVC5::Kind);
 
 /** Returns true if the given kind is associative. This is used by ExprManager to
  * decide whether it's safe to modify big expressions by changing the grouping of
  * the arguments. */
 /* TODO: This could be generated. */
-bool isAssociative(::CVC4::Kind k);
-std::string kindToString(::CVC4::Kind k);
+bool isAssociative(::CVC5::Kind k);
+std::string kindToString(::CVC5::Kind k);
 
 struct KindHashFunction {
-  inline size_t operator()(::CVC4::Kind k) const {
-    return k;
-  }
+  inline size_t operator()(::CVC5::Kind k) const { return k; }
 };/* struct KindHashFunction */
 
-}/* CVC4::kind namespace */
+}  // namespace kind
 
 /**
  * The enumeration for the built-in atomic types.
@@ -99,11 +97,11 @@ std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant);
 
 namespace theory {
 
-::CVC4::theory::TheoryId kindToTheoryId(::CVC4::Kind k);
-::CVC4::theory::TheoryId typeConstantToTheoryId(
-    ::CVC4::TypeConstant typeConstant);
+::CVC5::theory::TheoryId kindToTheoryId(::CVC5::Kind k);
+::CVC5::theory::TheoryId typeConstantToTheoryId(
+    ::CVC5::TypeConstant typeConstant);
 
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace theory
+}  // namespace CVC5
 
 #endif /* CVC4__KIND_H */
diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index 3f333eeab..701cc55dc 100644
--- a/src/expr/lazy_proof.cpp
+++ b/src/expr/lazy_proof.cpp
@@ -18,9 +18,9 @@
 #include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 
 LazyCDProof::LazyCDProof(ProofNodeManager* pnm,
                          ProofGenerator* dpg,
@@ -228,4 +228,4 @@ bool LazyCDProof::hasGenerator(Node fact) const
   return it != d_gens.end();
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
index 989fd55dc..5c0de5c5b 100644
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -19,7 +19,7 @@
 
 #include "expr/proof.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofGenerator;
 class ProofNodeManager;
@@ -105,6 +105,6 @@ class LazyCDProof : public CDProof
   ProofGenerator* getGeneratorFor(Node fact, bool& isSym);
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__LAZY_PROOF_H */
diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index e6fba747e..3651e53e1 100644
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -21,7 +21,7 @@
 #include "expr/proof_node_manager.h"
 #include "options/proof_options.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm,
                                    bool cyclic,
@@ -317,4 +317,4 @@ ProofGenerator* LazyCDProofChain::getGeneratorForInternal(Node fact, bool& rec)
 
 std::string LazyCDProofChain::identify() const { return "LazyCDProofChain"; }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
index 4c21eea99..7482e3ca4 100644
--- a/src/expr/lazy_proof_chain.h
+++ b/src/expr/lazy_proof_chain.h
@@ -22,7 +22,7 @@
 #include "context/cdhashmap.h"
 #include "expr/proof_generator.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofNodeManager;
 
@@ -148,6 +148,6 @@ class LazyCDProofChain : public ProofGenerator
   ProofGenerator* d_defGen;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__LAZY_PROOF_CHAIN_H */
diff --git a/src/expr/match_trie.cpp b/src/expr/match_trie.cpp
index f2465e030..d3adeb50e 100644
--- a/src/expr/match_trie.cpp
+++ b/src/expr/match_trie.cpp
@@ -14,9 +14,9 @@
 
 #include "expr/match_trie.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 bool MatchTrie::getMatches(Node n, NotifyMatch* ntm)
@@ -196,4 +196,4 @@ void MatchTrie::clear()
 }
 
 }  // namespace expr
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/match_trie.h b/src/expr/match_trie.h
index 976b70fba..45ff0c0c7 100644
--- a/src/expr/match_trie.h
+++ b/src/expr/match_trie.h
@@ -22,7 +22,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 /** A virtual class for notifications regarding matches. */
@@ -77,6 +77,6 @@ class MatchTrie
 };
 
 }  // namespace expr
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */
diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp
index 6e76c0da3..2f147b8b4 100644
--- a/src/expr/metakind_template.cpp
+++ b/src/expr/metakind_template.cpp
@@ -19,7 +19,7 @@
 
 #include <iostream>
 
-namespace CVC4 {
+namespace CVC5 {
 namespace kind {
 
 /**
@@ -41,31 +41,32 @@ ${metakind_kinds}
   return metaKinds[k + 1];
 }/* metaKindOf(k) */
 
-}/* CVC4::kind namespace */
+}  // namespace kind
 
 namespace expr {
 
 ${metakind_constantMaps}
 
-}/* CVC4::expr namespace */
+}  // namespace expr
 
 namespace kind {
 namespace metakind {
 
-size_t NodeValueCompare::constHash(const ::CVC4::expr::NodeValue* nv)
+size_t NodeValueCompare::constHash(const ::CVC5::expr::NodeValue* nv)
 {
   Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
 
   switch (nv->d_kind)
   {
 ${metakind_constHashes}
-    default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv->d_kind);
+default: Unhandled() << ::CVC5::expr::NodeValue::dKindToKind(nv->d_kind);
   }
 }
 
 template <bool pool>
-bool NodeValueCompare::compare(const ::CVC4::expr::NodeValue* nv1,
-                               const ::CVC4::expr::NodeValue* nv2) {
+bool NodeValueCompare::compare(const ::CVC5::expr::NodeValue* nv1,
+                               const ::CVC5::expr::NodeValue* nv2)
+{
   if(nv1->d_kind != nv2->d_kind) {
     return false;
   }
@@ -75,7 +76,7 @@ bool NodeValueCompare::compare(const ::CVC4::expr::NodeValue* nv1,
     switch (nv1->d_kind)
     {
 ${metakind_compares}
-      default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv1->d_kind);
+default: Unhandled() << ::CVC5::expr::NodeValue::dKindToKind(nv1->d_kind);
     }
   }
 
@@ -83,9 +84,9 @@ ${metakind_compares}
     return false;
   }
 
-  ::CVC4::expr::NodeValue::const_nv_iterator i = nv1->nv_begin();
-  ::CVC4::expr::NodeValue::const_nv_iterator j = nv2->nv_begin();
-  ::CVC4::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end();
+  ::CVC5::expr::NodeValue::const_nv_iterator i = nv1->nv_begin();
+  ::CVC5::expr::NodeValue::const_nv_iterator j = nv2->nv_begin();
+  ::CVC5::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end();
 
   while(i != i_end) {
     if((*i) != (*j)) {
@@ -98,19 +99,20 @@ ${metakind_compares}
   return true;
 }
 
-template bool NodeValueCompare::compare<true>(const ::CVC4::expr::NodeValue* nv1,
-                                              const ::CVC4::expr::NodeValue* nv2);
-template bool NodeValueCompare::compare<false>(const ::CVC4::expr::NodeValue* nv1,
-                                               const ::CVC4::expr::NodeValue* nv2);
+template bool NodeValueCompare::compare<true>(
+    const ::CVC5::expr::NodeValue* nv1, const ::CVC5::expr::NodeValue* nv2);
+template bool NodeValueCompare::compare<false>(
+    const ::CVC5::expr::NodeValue* nv1, const ::CVC5::expr::NodeValue* nv2);
 
 void NodeValueConstPrinter::toStream(std::ostream& out,
-                                            const ::CVC4::expr::NodeValue* nv) {
+                                     const ::CVC5::expr::NodeValue* nv)
+{
   Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
 
   switch (nv->d_kind)
   {
 ${metakind_constPrinters}
-    default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv->d_kind);
+default: Unhandled() << ::CVC5::expr::NodeValue::dKindToKind(nv->d_kind);
   }
 }
 
@@ -134,20 +136,21 @@ void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) {
  * 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)
+{
   Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
 
   switch (nv->d_kind)
   {
 ${metakind_constDeleters}
-    default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv->d_kind);
+default: Unhandled() << ::CVC5::expr::NodeValue::dKindToKind(nv->d_kind);
   }
 }
 
 // re-enable the strict-aliasing warning
 # pragma GCC diagnostic warning "-Wstrict-aliasing"
 
-uint32_t getMinArityForKind(::CVC4::Kind k)
+uint32_t getMinArityForKind(::CVC5::Kind k)
 {
   static const unsigned lbs[] = {
     0, /* NULL_EXPR */
@@ -159,7 +162,7 @@ ${metakind_lbchildren}
   return lbs[k];
 }
 
-uint32_t getMaxArityForKind(::CVC4::Kind k)
+uint32_t getMaxArityForKind(::CVC5::Kind k)
 {
   static const unsigned ubs[] = {
     0, /* NULL_EXPR */
@@ -177,7 +180,8 @@ ${metakind_ubchildren}
  * 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)
+{
   if(nv->getKind() == kind::BUILTIN) {
     return nv->getConst<Kind>();
   } else if(nv->getKind() == kind::LAMBDA) {
@@ -192,5 +196,5 @@ ${metakind_operatorKinds}
   };
 }
 
-}/* CVC4::kind namespace */
-}/* CVC4 namespace */
+}  // namespace kind
+}  // namespace CVC5
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 */
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 58531cba4..cc5162fef 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -92,9 +92,9 @@ function theory {
     echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
     exit 1
   elif ! expr "$2" : '\(::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
-  elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
+    echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC5::theory::foo)" >&2
+  elif ! expr "$2" : '\(::CVC5::theory::*\)' >/dev/null; then
+    echo "$kf:$lineno: warning: theory class not under ::CVC5::theory namespace" >&2
   fi
 }
 
@@ -226,7 +226,7 @@ template <> $2 const & Expr::getConst< $2 >() const;
 "
   getConst_implementations="${getConst_implementations}
 template <> $2 const & Expr::getConst() const {
-  PrettyCheckArgument(getKind() == ::CVC4::kind::$1, *this, \"Improper kind for getConst<$2>()\");
+  PrettyCheckArgument(getKind() == ::CVC5::kind::$1, *this, \"Improper kind for getConst<$2>()\");
   return d_node->getConst< $2 >();
 }
 "
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 55276549a..3b987746a 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -97,9 +97,9 @@ function theory {
     echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
     exit 1
   elif ! expr "$2" : '\(::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
-  elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
+    echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC5::theory::foo)" >&2
+  elif ! expr "$2" : '\(::CVC5::theory::*\)' >/dev/null; then
+    echo "$kf:$lineno: warning: theory class not under ::CVC5::theory namespace" >&2
   fi
 
   theory_id="$1"
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 9d2f0a475..b88a70c71 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -76,9 +76,9 @@ function theory {
     echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
     exit 1
   elif ! expr "$2" : '\(::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
-  elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
+    echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC5::theory::foo)" >&2
+  elif ! expr "$2" : '\(::CVC5::theory::*\)' >/dev/null; then
+    echo "$kf:$lineno: warning: theory class not under ::CVC5::theory namespace" >&2
   fi
 
   theory_class=$1
@@ -211,12 +211,12 @@ function constant {
       # tricky to specify the CONST payload, like "int const*"; in any
       # case, this warning gives too many false positives, so disable it
       if ! expr "$2" : '..* ..*' >/dev/null; then
-        echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::CVC4::Rational)" >&2
+        echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::CVC5::Rational)" >&2
       fi
     fi
   fi
   if ! expr "$3" : '\(::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC4::RationalHashFunction)" >&2
+    echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC5::RationalHashFunction)" >&2
   fi
 
   # Avoid including the same header multiple times
@@ -233,13 +233,13 @@ $2 const& NodeValue::getConst< $2 >() const;
 template <>
 struct ConstantMap< $2 > {
   // typedef $theory_class OwningTheory;
-  enum { kind = ::CVC4::kind::$1 };
+  enum { kind = ::CVC5::kind::$1 };
 };/* ConstantMap< $2 > */
 
 template <>
-struct ConstantMapReverse< ::CVC4::kind::$1 > {
+struct ConstantMapReverse< ::CVC5::kind::$1 > {
   typedef $2 T;
-};/* ConstantMapReverse< ::CVC4::kind::$1 > */
+};/* ConstantMapReverse< ::CVC5::kind::$1 > */
   "
   metakind_constantMaps="${metakind_constantMaps}
 // The reinterpret_cast of d_children to \"$2 const*\"
@@ -250,7 +250,7 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > {
 
 template <>
 $2 const& NodeValue::getConst< $2 >() const {
-  AssertArgument(getKind() == ::CVC4::kind::$1, *this,
+  AssertArgument(getKind() == ::CVC5::kind::$1, *this,
                  \"Improper kind for getConst<$2>()\");
   // To support non-inlined CONSTANT-kinded NodeValues (those that are
   // \"constructed\" when initially checking them against the NodeManager
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 59d002631..fa2a8860c 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -26,7 +26,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 
 TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
                                                            std::string message)
@@ -110,4 +110,4 @@ bool NodeTemplate<ref_count>::isConst() const {
 template bool NodeTemplate<true>::isConst() const;
 template bool NodeTemplate<false>::isConst() const;
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/expr/node.h b/src/expr/node.h
index 9e485ae78..291c2e538 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -41,7 +41,7 @@
 #include "util/hash.h"
 #include "util/utility.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class TypeNode;
 class NodeManager;
@@ -138,16 +138,16 @@ class NodeValue;
   namespace attr {
     class AttributeManager;
     struct SmtAttributes;
-  }/* CVC4::expr::attr namespace */
+    }  // namespace attr
 
   class ExprSetDepth;
-}/* CVC4::expr namespace */
+  }  // namespace expr
 
 namespace kind {
   namespace metakind {
     struct NodeValueConstPrinter;
-  }/* CVC4::kind::metakind namespace */
-}/* CVC4::kind namespace */
+    }  // namespace metakind
+    }  // namespace kind
 
 // for hash_maps, hash_sets..
 struct NodeHashFunction {
@@ -199,10 +199,10 @@ class NodeTemplate {
   template <unsigned nchild_thresh>
   friend class NodeBuilder;
 
-  friend class ::CVC4::expr::attr::AttributeManager;
-  friend struct ::CVC4::expr::attr::SmtAttributes;
+  friend class ::CVC5::expr::attr::AttributeManager;
+  friend struct ::CVC5::expr::attr::SmtAttributes;
 
-  friend struct ::CVC4::kind::metakind::NodeValueConstPrinter;
+  friend struct ::CVC5::kind::metakind::NodeValueConstPrinter;
 
   /**
    * Assigns the expression value and does reference counting. No assumptions
@@ -951,12 +951,12 @@ std::ostream& operator<<(
   return out;
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 //#include "expr/attribute.h"
 #include "expr/node_manager.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 inline size_t NodeHashFunction::operator()(Node node) const {
   return node.getId();
@@ -986,7 +986,7 @@ template <class AttrKind>
 inline typename AttrKind::value_type NodeTemplate<ref_count>::
 getAttribute(const AttrKind&) const {
   Assert(NodeManager::currentNM() != NULL)
-      << "There is no current CVC4::NodeManager associated to this thread.\n"
+      << "There is no current CVC5::NodeManager associated to this thread.\n"
          "Perhaps a public-facing function is missing a NodeManagerScope ?";
 
   assertTNodeNotExpired();
@@ -999,7 +999,7 @@ template <class AttrKind>
 inline bool NodeTemplate<ref_count>::
 hasAttribute(const AttrKind&) const {
   Assert(NodeManager::currentNM() != NULL)
-      << "There is no current CVC4::NodeManager associated to this thread.\n"
+      << "There is no current CVC5::NodeManager associated to this thread.\n"
          "Perhaps a public-facing function is missing a NodeManagerScope ?";
 
   assertTNodeNotExpired();
@@ -1012,7 +1012,7 @@ template <class AttrKind>
 inline bool NodeTemplate<ref_count>::getAttribute(const AttrKind&,
                                                   typename AttrKind::value_type& ret) const {
   Assert(NodeManager::currentNM() != NULL)
-      << "There is no current CVC4::NodeManager associated to this thread.\n"
+      << "There is no current CVC5::NodeManager associated to this thread.\n"
          "Perhaps a public-facing function is missing a NodeManagerScope ?";
 
   assertTNodeNotExpired();
@@ -1025,7 +1025,7 @@ template <class AttrKind>
 inline void NodeTemplate<ref_count>::
 setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
   Assert(NodeManager::currentNM() != NULL)
-      << "There is no current CVC4::NodeManager associated to this thread.\n"
+      << "There is no current CVC5::NodeManager associated to this thread.\n"
          "Perhaps a public-facing function is missing a NodeManagerScope ?";
 
   assertTNodeNotExpired();
@@ -1225,7 +1225,7 @@ template <bool ref_count>
 NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const
 {
   Assert(NodeManager::currentNM() != NULL)
-      << "There is no current CVC4::NodeManager associated to this thread.\n"
+      << "There is no current CVC5::NodeManager associated to this thread.\n"
          "Perhaps a public-facing function is missing a NodeManagerScope ?";
 
   assertTNodeNotExpired();
@@ -1255,7 +1255,7 @@ template <bool ref_count>
 TypeNode NodeTemplate<ref_count>::getType(bool check) const
 {
   Assert(NodeManager::currentNM() != NULL)
-      << "There is no current CVC4::NodeManager associated to this thread.\n"
+      << "There is no current CVC5::NodeManager associated to this thread.\n"
          "Perhaps a public-facing function is missing a NodeManagerScope ?";
 
   assertTNodeNotExpired();
@@ -1491,6 +1491,6 @@ static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>&
 }
 #endif /* CVC4_DEBUG */
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__NODE_H */
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 1ec6c7f3a..318b7c85b 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -20,7 +20,7 @@
 #include "expr/attribute.h"
 #include "expr/dtype.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 bool hasSubterm(TNode n, TNode t, bool strict)
@@ -764,4 +764,4 @@ bool match(Node x,
 }
 
 }  // namespace expr
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index e7d71ce3a..ca1ee2e39 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -27,7 +27,7 @@
 #include "expr/node.h"
 #include "expr/type_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 /**
@@ -235,6 +235,6 @@ bool match(Node n1,
            std::unordered_map<Node, Node, NodeHashFunction>& subs);
 
 }  // namespace expr
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 91b378c5f..724e03451 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -160,14 +160,14 @@
 #include <memory>
 #include <vector>
 
-namespace CVC4 {
-  static const unsigned default_nchild_thresh = 10;
+namespace CVC5 {
+static const unsigned default_nchild_thresh = 10;
 
-  template <unsigned nchild_thresh>
-  class NodeBuilder;
+template <unsigned nchild_thresh>
+class NodeBuilder;
 
-  class NodeManager;
-}/* CVC4 namespace */
+class NodeManager;
+}  // namespace CVC5
 
 #include "base/check.h"
 #include "base/output.h"
@@ -175,7 +175,7 @@ namespace CVC4 {
 #include "expr/metakind.h"
 #include "expr/node_value.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 // Sometimes it's useful for debugging to output a NodeBuilder that
 // isn't yet a Node..
@@ -729,7 +729,7 @@ public:
 
 };/* class NodeBuilder<> */
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 // TODO: add templatized NodeTemplate<ref_count> to all above and
 // below inlines for 'const [T]Node&' arguments?  Technically a lot of
@@ -741,7 +741,7 @@ public:
 #include "expr/node_manager.h"
 #include "options/expr_options.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 template <unsigned nchild_thresh>
 void NodeBuilder<nchild_thresh>::clear(Kind k) {
@@ -1324,6 +1324,6 @@ std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& nb
   return out << *nb.d_nv;
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__NODE_BUILDER_H */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index a5329147b..370f0fb4c 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -35,9 +35,9 @@
 #include "util/resource_manager.h"
 
 using namespace std;
-using namespace CVC4::expr;
+using namespace CVC5::expr;
 
-namespace CVC4 {
+namespace CVC5 {
 
 thread_local NodeManager* NodeManager::s_current = NULL;
 
@@ -87,7 +87,7 @@ struct NVReclaim {
 
 namespace attr {
   struct LambdaBoundVarListTag { };
-}/* CVC4::attr namespace */
+  }  // namespace attr
 
 // attribute that stores the canonical bound variable list for function types
 typedef expr::Attribute<attr::LambdaBoundVarListTag, Node> LambdaBoundVarListAttr;
@@ -373,7 +373,7 @@ void NodeManager::reclaimZombies() {
       if(mk == kind::metakind::CONSTANT) {
         // Destroy (call the destructor for) the C++ type representing
         // the constant in this NodeValue.  This is needed for
-        // e.g. CVC4::Rational, since it has a gmp internal
+        // e.g. CVC5::Rational, since it has a gmp internal
         // representation that mallocs memory and should be cleaned
         // up.  (This won't delete a pointer value if used as a
         // constant, but then, you should probably use a smart-pointer
@@ -678,7 +678,7 @@ std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes(
             << "malformed selector in datatype post-resolution";
         // This next one's a "hard" check, performed in non-debug builds
         // as well; the other ones should all be guaranteed by the
-        // CVC4::DType class, but this actually needs to be checked.
+        // CVC5::DType class, but this actually needs to be checked.
         AlwaysAssert(!selectorType.getRangeType().isFunctionLike())
             << "cannot put function-like things in datatypes";
       }
@@ -1170,4 +1170,4 @@ Kind NodeManager::getKindForFunction(TNode fun)
   return kind::UNDEFINED_KIND;
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 52ce096d5..aeea179d4 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -35,7 +35,7 @@
 #include "expr/metakind.h"
 #include "expr/node_value.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 namespace api {
 class Solver;
@@ -51,10 +51,10 @@ namespace expr {
   namespace attr {
     class AttributeUniqueId;
     class AttributeManager;
-  }/* CVC4::expr::attr namespace */
+    }  // namespace attr
 
   class TypeChecker;
-}/* CVC4::expr namespace */
+  }  // namespace expr
 
 /**
  * An interface that an interested party can implement and then subscribe
@@ -163,7 +163,7 @@ class NodeManager
    * PLUS, are APPLYs of a PLUS operator to arguments.  This array
    * holds the set of operators for these things.  A PLUS operator is
    * a Node with kind "BUILTIN", and if you call
-   * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
+   * plusOperator->getConst<CVC5::Kind>(), you get kind::PLUS back.
    */
   Node d_operators[kind::LAST_KIND];
 
@@ -660,7 +660,7 @@ class NodeManager
   /**
    * Get the (singleton) operator of an OPERATOR-kinded kind.  The
    * returned node n will have kind BUILTIN, and calling
-   * n.getConst<CVC4::Kind>() will yield k.
+   * n.getConst<CVC5::Kind>() will yield k.
    */
   inline TNode operatorOf(Kind k) {
     AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k,
@@ -1203,7 +1203,7 @@ inline void NodeManager::poolRemove(expr::NodeValue* nv) {
   d_nodeValuePool.erase(nv);// FIXME multithreading
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
 #include "expr/metakind.h"
@@ -1211,7 +1211,7 @@ inline void NodeManager::poolRemove(expr::NodeValue* nv) {
 
 #include "expr/node_builder.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 // general expression-builders
 
@@ -1577,6 +1577,6 @@ NodeClass NodeManager::mkConstInternal(const T& val) {
   return NodeClass(nv);
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__NODE_MANAGER_H */
diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h
index 2add5a314..b7f6319eb 100644
--- a/src/expr/node_manager_attributes.h
+++ b/src/expr/node_manager_attributes.h
@@ -19,7 +19,7 @@
 
 #include "expr/attribute.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 // Definition of an attribute for the variable name.
@@ -29,12 +29,12 @@ namespace attr {
   struct SortArityTag { };
   struct TypeTag { };
   struct TypeCheckedTag { };
-}/* CVC4::expr::attr namespace */
+  }  // namespace attr
 
 typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
 typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
 typedef expr::Attribute<expr::attr::TypeTag, TypeNode> TypeAttr;
 typedef expr::Attribute<expr::attr::TypeCheckedTag, bool> TypeCheckedAttr;
 
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
+}  // namespace expr
+}  // namespace CVC5
diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h
index 475e0a122..831eace65 100644
--- a/src/expr/node_self_iterator.h
+++ b/src/expr/node_self_iterator.h
@@ -24,7 +24,7 @@
 #include "base/check.h"
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 class NodeSelfIterator : public std::iterator<std::input_iterator_tag, Node> {
@@ -122,7 +122,7 @@ inline bool NodeSelfIterator::operator!=(NodeSelfIterator i) const {
   return !(*this == i);
 }
 
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
+}  // namespace expr
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__NODE_SELF_ITERATOR_H */
diff --git a/src/expr/node_traversal.cpp b/src/expr/node_traversal.cpp
index f3b4c2ede..c7d3ab3f8 100644
--- a/src/expr/node_traversal.cpp
+++ b/src/expr/node_traversal.cpp
@@ -16,7 +16,7 @@
 
 #include <functional>
 
-namespace CVC4 {
+namespace CVC5 {
 
 NodeDfsIterator::NodeDfsIterator(TNode n,
                                  VisitOrder order,
@@ -156,4 +156,4 @@ NodeDfsIterator NodeDfsIterable::end() const
   return NodeDfsIterator(d_order);
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h
index 1f3b1f563..934ec6bd8 100644
--- a/src/expr/node_traversal.h
+++ b/src/expr/node_traversal.h
@@ -23,7 +23,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * Enum that represents an order in which nodes are visited.
@@ -144,6 +144,6 @@ class NodeDfsIterable
   std::function<bool(TNode)> d_skipIf;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif  // CVC4__EXPR__NODE_TRAVERSAL_H
diff --git a/src/expr/node_trie.cpp b/src/expr/node_trie.cpp
index f02035c43..195011c1f 100644
--- a/src/expr/node_trie.cpp
+++ b/src/expr/node_trie.cpp
@@ -14,7 +14,7 @@
 
 #include "expr/node_trie.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 
 template <bool ref_count>
@@ -92,4 +92,4 @@ template void NodeTemplateTrie<true>::debugPrint(const char* c,
                                                  unsigned depth) const;
 
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/node_trie.h b/src/expr/node_trie.h
index 81529f38e..f765105d3 100644
--- a/src/expr/node_trie.h
+++ b/src/expr/node_trie.h
@@ -20,7 +20,7 @@
 #include <map>
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 
 /** NodeTemplate trie class
@@ -107,6 +107,6 @@ typedef NodeTemplateTrie<true> NodeTrie;
 typedef NodeTemplateTrie<false> TNodeTrie;
 
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__NODE_TRIE_H */
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index dc682a9fb..027c15a0a 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -31,7 +31,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 string NodeValue::toString() const {
@@ -94,5 +94,5 @@ NodeValue::iterator<NodeTemplate<false> > operator+(
   return i + p;
 }
 
-} /* CVC4::expr namespace */
-} /* CVC4 namespace */
+}  // namespace expr
+}  // namespace CVC5
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index d6b6d3c45..ecc054a75 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -32,7 +32,7 @@
 #include "expr/kind.h"
 #include "options/language.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 template <bool ref_count> class NodeTemplate;
 class TypeNode;
@@ -45,15 +45,15 @@ namespace expr {
 
 namespace kind {
   namespace metakind {
-    template < ::CVC4::Kind k, bool pool >
-    struct NodeValueConstCompare;
+  template < ::CVC5::Kind k, bool pool>
+  struct NodeValueConstCompare;
 
-    struct NodeValueCompare;
-    struct NodeValueConstPrinter;
+  struct NodeValueCompare;
+  struct NodeValueConstPrinter;
 
-    void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv);
-  }/* CVC4::kind::metakind namespace */
-}/* CVC4::kind namespace */
+  void deleteNodeValueConstant(::CVC5::expr::NodeValue* nv);
+  }  // namespace metakind
+  }  // namespace kind
 
 namespace expr {
 
@@ -63,19 +63,19 @@ namespace expr {
 class NodeValue
 {
   template <bool>
-  friend class ::CVC4::NodeTemplate;
-  friend class ::CVC4::TypeNode;
+  friend class ::CVC5::NodeTemplate;
+  friend class ::CVC5::TypeNode;
   template <unsigned nchild_thresh>
-  friend class ::CVC4::NodeBuilder;
-  friend class ::CVC4::NodeManager;
+  friend class ::CVC5::NodeBuilder;
+  friend class ::CVC5::NodeManager;
 
   template <Kind k, bool pool>
-  friend struct ::CVC4::kind::metakind::NodeValueConstCompare;
+  friend struct ::CVC5::kind::metakind::NodeValueConstCompare;
 
-  friend struct ::CVC4::kind::metakind::NodeValueCompare;
-  friend struct ::CVC4::kind::metakind::NodeValueConstPrinter;
+  friend struct ::CVC5::kind::metakind::NodeValueCompare;
+  friend struct ::CVC5::kind::metakind::NodeValueConstPrinter;
 
-  friend void ::CVC4::kind::metakind::deleteNodeValueConstant(NodeValue* nv);
+  friend void ::CVC5::kind::metakind::deleteNodeValueConstant(NodeValue* nv);
 
   friend class RefCountGuard;
 
@@ -395,12 +395,12 @@ struct NodeValueIDEquality {
 
 inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
 
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
+}  // namespace expr
+}  // namespace CVC5
 
 #include "expr/node_manager.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 inline NodeValue::NodeValue(int) :
@@ -496,12 +496,12 @@ inline NodeValue* NodeValue::getChild(int i) const {
   return d_children[i];
 }
 
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
+}  // namespace expr
+}  // namespace CVC5
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 template <typename T>
@@ -517,7 +517,7 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
   return out;
 }
 
-}/* CVC4::expr namespace */
+}  // namespace expr
 
 #ifdef CVC4_DEBUG
 /**
@@ -545,6 +545,6 @@ static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue*
 }
 #endif /* CVC4_DEBUG */
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__NODE_VALUE_H */
diff --git a/src/expr/node_visitor.h b/src/expr/node_visitor.h
index dcf8e38e0..a3e24772a 100644
--- a/src/expr/node_visitor.h
+++ b/src/expr/node_visitor.h
@@ -22,7 +22,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * Traverses the nodes reverse-topologically (children before parents),
@@ -123,4 +123,4 @@ public:
 template <typename Visitor>
 thread_local bool NodeVisitor<Visitor>::s_inRun = false;
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
index e3c70590c..a55b3c69a 100644
--- a/src/expr/proof.cpp
+++ b/src/expr/proof.cpp
@@ -18,9 +18,9 @@
 #include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 
 CDProof::CDProof(ProofNodeManager* pnm,
                  context::Context* c,
@@ -455,4 +455,4 @@ Node CDProof::getSymmFact(TNode f)
 
 std::string CDProof::identify() const { return d_name; }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/proof.h b/src/expr/proof.h
index e676731ea..164880cea 100644
--- a/src/expr/proof.h
+++ b/src/expr/proof.h
@@ -24,7 +24,7 @@
 #include "expr/proof_generator.h"
 #include "expr/proof_step_buffer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofNode;
 class ProofNodeManager;
@@ -273,6 +273,6 @@ class CDProof : public ProofGenerator
   void notifyNewProof(Node expected);
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__PROOF_MANAGER_H */
diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp
index bcff07c30..b5955e991 100644
--- a/src/expr/proof_checker.cpp
+++ b/src/expr/proof_checker.cpp
@@ -19,9 +19,9 @@
 #include "options/proof_options.h"
 #include "smt/smt_statistics_registry.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 
 Node ProofRuleChecker::check(PfRule id,
                              const std::vector<Node>& children,
@@ -347,4 +347,4 @@ bool ProofChecker::isPedanticFailure(PfRule id,
   return false;
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
index a84f17c28..edb0fec3a 100644
--- a/src/expr/proof_checker.h
+++ b/src/expr/proof_checker.h
@@ -24,7 +24,7 @@
 #include "util/statistics_registry.h"
 #include "util/stats_histogram.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofChecker;
 class ProofNode;
@@ -202,6 +202,6 @@ class ProofChecker
                      bool enableOutput);
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__PROOF_CHECKER_H */
diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp
index e4a59c8f0..487c52bc6 100644
--- a/src/expr/proof_ensure_closed.cpp
+++ b/src/expr/proof_ensure_closed.cpp
@@ -22,7 +22,7 @@
 #include "options/proof_options.h"
 #include "options/smt_options.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * Ensure closed with respect to assumptions, internal version, which
@@ -179,4 +179,4 @@ void pfnEnsureClosedWrt(ProofNode* pn,
   ensureClosedWrtInternal(Node::null(), nullptr, pn, assumps, c, ctx, false);
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h
index dd137343a..40143f814 100644
--- a/src/expr/proof_ensure_closed.h
+++ b/src/expr/proof_ensure_closed.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofGenerator;
 class ProofNode;
@@ -67,6 +67,6 @@ void pfnEnsureClosedWrt(ProofNode* pn,
                         const std::vector<Node>& assumps,
                         const char* c,
                         const char* ctx);
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__PROOF_ENSURE_CLOSED_H */
diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
index 53bc54d7a..102435cea 100644
--- a/src/expr/proof_generator.cpp
+++ b/src/expr/proof_generator.cpp
@@ -21,7 +21,7 @@
 #include "expr/proof_node_algorithm.h"
 #include "options/smt_options.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 std::ostream& operator<<(std::ostream& out, CDPOverwrite opol)
 {
@@ -73,4 +73,4 @@ bool ProofGenerator::addProofTo(Node f,
   return false;
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h
index 497e89d7a..446cb2c83 100644
--- a/src/expr/proof_generator.h
+++ b/src/expr/proof_generator.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class CDProof;
 class ProofNode;
@@ -107,6 +107,6 @@ class ProofGenerator
   virtual std::string identify() const = 0;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__PROOF_GENERATOR_H */
diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp
index 755a37643..923bdeacd 100644
--- a/src/expr/proof_node.cpp
+++ b/src/expr/proof_node.cpp
@@ -17,7 +17,7 @@
 #include "expr/proof_node_algorithm.h"
 #include "expr/proof_node_to_sexpr.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 ProofNode::ProofNode(PfRule id,
                      const std::vector<std::shared_ptr<ProofNode>>& children,
@@ -81,4 +81,4 @@ std::ostream& operator<<(std::ostream& out, const ProofNode& pn)
   return out;
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h
index f7b323018..67600e2d0 100644
--- a/src/expr/proof_node.h
+++ b/src/expr/proof_node.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "expr/proof_rule.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofNodeManager;
 class ProofNode;
@@ -141,6 +141,6 @@ inline size_t ProofNodeHashFunction::operator()(
  */
 std::ostream& operator<<(std::ostream& out, const ProofNode& pn);
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__PROOF_NODE_H */
diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp
index 90b1e9030..142a9b37f 100644
--- a/src/expr/proof_node_algorithm.cpp
+++ b/src/expr/proof_node_algorithm.cpp
@@ -16,7 +16,7 @@
 
 #include "expr/proof_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump)
@@ -172,4 +172,4 @@ bool containsSubproof(ProofNode* pn,
 }
 
 }  // namespace expr
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h
index 9106bb36f..9266c7251 100644
--- a/src/expr/proof_node_algorithm.h
+++ b/src/expr/proof_node_algorithm.h
@@ -21,7 +21,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofNode;
 
@@ -70,6 +70,6 @@ bool containsSubproof(ProofNode* pn,
                       std::unordered_set<const ProofNode*>& visited);
 
 }  // namespace expr
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__PROOF_NODE_ALGORITHM_H */
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index a018db4c0..ceb9d4eac 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -23,9 +23,9 @@
 #include "options/proof_options.h"
 #include "theory/rewriter.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 
 ProofNodeManager::ProofNodeManager(ProofChecker* pc)
     : d_checker(pc)
@@ -356,4 +356,4 @@ bool ProofNodeManager::updateNodeInternal(
   return true;
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index 434cffe28..8e019818d 100644
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "expr/proof_rule.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofChecker;
 class ProofNode;
@@ -192,6 +192,6 @@ class ProofNodeManager
       bool needsCheck);
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__PROOF_NODE_H */
diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp
index c298dafe6..7468ecb5a 100644
--- a/src/expr/proof_node_to_sexpr.cpp
+++ b/src/expr/proof_node_to_sexpr.cpp
@@ -20,9 +20,9 @@
 #include "expr/proof_node.h"
 #include "options/proof_options.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 
 ProofNodeToSExpr::ProofNodeToSExpr()
 {
@@ -144,4 +144,4 @@ Node ProofNodeToSExpr::getOrMkNodeVariable(Node n)
   return var;
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h
index cf2e86263..8da094da2 100644
--- a/src/expr/proof_node_to_sexpr.h
+++ b/src/expr/proof_node_to_sexpr.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "expr/proof_rule.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofNode;
 
@@ -64,6 +64,6 @@ class ProofNodeToSExpr
   Node getOrMkNodeVariable(Node n);
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__PROOF_RULE_H */
diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp
index cacadc815..4c1883e93 100644
--- a/src/expr/proof_node_updater.cpp
+++ b/src/expr/proof_node_updater.cpp
@@ -19,7 +19,7 @@
 #include "expr/proof_node_algorithm.h"
 #include "expr/proof_node_manager.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {}
 ProofNodeUpdaterCallback::~ProofNodeUpdaterCallback() {}
@@ -261,4 +261,4 @@ void ProofNodeUpdater::setDebugFreeAssumptions(
   d_debugFreeAssumps = true;
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h
index 693168a25..5a22af61a 100644
--- a/src/expr/proof_node_updater.h
+++ b/src/expr/proof_node_updater.h
@@ -23,7 +23,7 @@
 #include "expr/node.h"
 #include "expr/proof_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class CDProof;
 class ProofNode;
@@ -155,6 +155,6 @@ class ProofNodeUpdater
   bool d_autoSym;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 579b06c76..1323520c3 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -16,7 +16,7 @@
 
 #include <iostream>
 
-namespace CVC4 {
+namespace CVC5 {
 
 const char* toString(PfRule id)
 {
@@ -210,4 +210,4 @@ size_t PfRuleHashFunction::operator()(PfRule id) const
   return static_cast<size_t>(id);
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index efa673409..95f97ae44 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -19,7 +19,7 @@
 
 #include <iosfwd>
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * An enumeration for proof rules. This enumeration is analogous to Kind for
@@ -1379,6 +1379,6 @@ struct PfRuleHashFunction
   size_t operator()(PfRule id) const;
 }; /* struct PfRuleHashFunction */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__PROOF_RULE_H */
diff --git a/src/expr/proof_set.h b/src/expr/proof_set.h
index a45a0f1f8..ccfac350a 100644
--- a/src/expr/proof_set.h
+++ b/src/expr/proof_set.h
@@ -23,7 +23,7 @@
 #include "context/context.h"
 #include "expr/proof_node_manager.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * A (context-dependent) set of proofs, which is used for memory
@@ -70,6 +70,6 @@ class CDProofSet
   std::string d_namePrefix;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__LAZY_PROOF_SET_H */
diff --git a/src/expr/proof_step_buffer.cpp b/src/expr/proof_step_buffer.cpp
index 51aa9f098..23f0f5997 100644
--- a/src/expr/proof_step_buffer.cpp
+++ b/src/expr/proof_step_buffer.cpp
@@ -16,9 +16,9 @@
 
 #include "expr/proof_checker.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 
 ProofStep::ProofStep() : d_rule(PfRule::UNKNOWN) {}
 ProofStep::ProofStep(PfRule r,
@@ -108,4 +108,4 @@ const std::vector<std::pair<Node, ProofStep>>& ProofStepBuffer::getSteps() const
 
 void ProofStepBuffer::clear() { d_steps.clear(); }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h
index 0b4b8552b..b78d1d605 100644
--- a/src/expr/proof_step_buffer.h
+++ b/src/expr/proof_step_buffer.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "expr/proof_rule.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofChecker;
 
@@ -92,6 +92,6 @@ class ProofStepBuffer
   std::vector<std::pair<Node, ProofStep>> d_steps;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__PROOF_STEP_BUFFER_H */
diff --git a/src/expr/record.cpp b/src/expr/record.cpp
index ed4e05567..affd2615c 100644
--- a/src/expr/record.cpp
+++ b/src/expr/record.cpp
@@ -19,11 +19,10 @@
 #include "base/check.h"
 #include "base/output.h"
 
-
-namespace CVC4 {
+namespace CVC5 {
 
 std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) {
   return out << "[" << t.getField() << "]";
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/expr/record.h b/src/expr/record.h
index a9201fca3..d4b41b9b9 100644
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -25,13 +25,13 @@
 #include <utility>
 
 // Forward Declarations
-namespace CVC4 {
+namespace CVC5 {
 // This forward delcartion is required to resolve a cicular dependency with
 // Record which is a referenced in a Kind file.
 class TypeNode;
-} /* namespace CVC4 */
+} // namespace CVC5
 
-namespace CVC4 {
+namespace CVC5 {
 
 // operators for record update
 class RecordUpdate
@@ -56,6 +56,6 @@ std::ostream& operator<<(std::ostream& out, const RecordUpdate& t);
 
 using Record = std::vector<std::pair<std::string, TypeNode>>;
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__RECORD_H */
diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp
index b02b68815..90b57f58d 100644
--- a/src/expr/sequence.cpp
+++ b/src/expr/sequence.cpp
@@ -22,7 +22,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 
 Sequence::Sequence(const TypeNode& t, const std::vector<Node>& s)
     : d_type(new TypeNode(t)), d_seq(s)
@@ -378,4 +378,4 @@ size_t SequenceHashFunction::operator()(const Sequence& s) const
   return ret;
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/sequence.h b/src/expr/sequence.h
index 1c0b1fbb9..461adb667 100644
--- a/src/expr/sequence.h
+++ b/src/expr/sequence.h
@@ -20,7 +20,7 @@
 #include <memory>
 #include <vector>
 
-namespace CVC4 {
+namespace CVC5 {
 
 template <bool ref_count>
 class NodeTemplate;
@@ -36,7 +36,7 @@ class Sequence
  public:
   /** constructors for Sequence
    *
-   * Internally, a CVC4::Sequence is represented by a vector of Nodes (d_seq),
+   * Internally, a CVC5::Sequence is represented by a vector of Nodes (d_seq),
    * where each Node in this vector must be a constant.
    */
   Sequence() = default;
@@ -173,6 +173,6 @@ struct SequenceHashFunction
 
 std::ostream& operator<<(std::ostream& os, const Sequence& s);
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__SEQUENCE_H */
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index c65180ed3..2b04c0755 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -18,9 +18,9 @@
 #include "expr/bound_var_manager.h"
 #include "expr/node_algorithm.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 
 // Attributes are global maps from Nodes to data. Thus, note that these could
 // be implemented as internal maps in SkolemManager.
@@ -298,4 +298,4 @@ Node SkolemManager::mkSkolemInternal(Node w,
   return k;
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 44a8f87c2..1078bc11f 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -21,7 +21,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofGenerator;
 
@@ -234,6 +234,6 @@ class SkolemManager
                  int flags = NodeManager::SKOLEM_DEFAULT);
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__PROOF_SKOLEM_CACHE_H */
diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp
index 0434cacf3..897c6fdba 100644
--- a/src/expr/subs.cpp
+++ b/src/expr/subs.cpp
@@ -18,7 +18,7 @@
 
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 bool Subs::empty() const { return d_vars.empty(); }
 
@@ -176,4 +176,4 @@ std::ostream& operator<<(std::ostream& out, const Subs& s)
   return out;
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/subs.h b/src/expr/subs.h
index 86c7d1758..c2854bf36 100644
--- a/src/expr/subs.h
+++ b/src/expr/subs.h
@@ -19,7 +19,7 @@
 #include <vector>
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * Helper substitution class. Stores a substitution in parallel vectors
@@ -80,6 +80,6 @@ class Subs
  */
 std::ostream& operator<<(std::ostream& out, const Subs& s);
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__SUBS_H */
diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp
index d2e845452..352dd157a 100644
--- a/src/expr/sygus_datatype.cpp
+++ b/src/expr/sygus_datatype.cpp
@@ -16,9 +16,9 @@
 
 #include <sstream>
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 
 SygusDatatype::SygusDatatype(const std::string& name) : d_dt(DType(name)) {}
 
@@ -99,4 +99,4 @@ const DType& SygusDatatype::getDatatype() const
 
 bool SygusDatatype::isInitialized() const { return d_dt.isSygus(); }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h
index 1350e9e57..f4635bdb3 100644
--- a/src/expr/sygus_datatype.h
+++ b/src/expr/sygus_datatype.h
@@ -24,7 +24,7 @@
 #include "expr/node.h"
 #include "expr/type_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /** Attribute true for variables that represent any constant */
 struct SygusAnyConstAttributeId
@@ -134,6 +134,6 @@ class SygusDatatype
   DType d_dt;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp
index 0fa2db1d4..1e99f4a68 100644
--- a/src/expr/symbol_manager.cpp
+++ b/src/expr/symbol_manager.cpp
@@ -19,9 +19,9 @@
 #include "context/cdlist.h"
 #include "context/cdo.h"
 
-using namespace CVC4::context;
+using namespace CVC5::context;
 
-namespace CVC4 {
+namespace CVC5 {
 
 // ---------------------------------------------- SymbolManager::Implementation
 
@@ -367,4 +367,4 @@ void SymbolManager::resetAssertions()
   d_symtabAllocated.resetAssertions();
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h
index 40ea44b34..6795ce3b3 100644
--- a/src/expr/symbol_manager.h
+++ b/src/expr/symbol_manager.h
@@ -25,7 +25,7 @@
 #include "cvc4_export.h"
 #include "expr/symbol_table.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * Symbol manager, which manages:
@@ -156,6 +156,6 @@ class CVC4_EXPORT SymbolManager
   bool d_globalDeclarations;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__SYMBOL_MANAGER_H */
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 3942f3775..774e2bb39 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -28,11 +28,11 @@
 #include "context/cdhashset.h"
 #include "context/context.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
-using ::CVC4::context::CDHashMap;
-using ::CVC4::context::CDHashSet;
-using ::CVC4::context::Context;
+using ::CVC5::context::CDHashMap;
+using ::CVC5::context::CDHashSet;
+using ::CVC5::context::Context;
 using ::std::copy;
 using ::std::endl;
 using ::std::ostream_iterator;
@@ -679,4 +679,4 @@ size_t SymbolTable::getLevel() const { return d_implementation->getLevel(); }
 void SymbolTable::reset() { d_implementation->reset(); }
 void SymbolTable::resetAssertions() { d_implementation->resetAssertions(); }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index 297917120..113dea704 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -26,7 +26,7 @@
 #include "base/exception.h"
 #include "cvc4_export.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 namespace api {
 class Solver;
@@ -210,6 +210,6 @@ class CVC4_EXPORT SymbolTable
   std::unique_ptr<Implementation> d_implementation;
 }; /* class SymbolTable */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__SYMBOL_TABLE_H */
diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/expr/tconv_seq_proof_generator.cpp
index e7fba5088..9b099de2d 100644
--- a/src/expr/tconv_seq_proof_generator.cpp
+++ b/src/expr/tconv_seq_proof_generator.cpp
@@ -18,7 +18,7 @@
 
 #include "expr/proof_node_manager.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 TConvSeqProofGenerator::TConvSeqProofGenerator(
     ProofNodeManager* pnm,
@@ -168,4 +168,4 @@ theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence(
 
 std::string TConvSeqProofGenerator::identify() const { return d_name; }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h
index e907ef09c..a5b1de101 100644
--- a/src/expr/tconv_seq_proof_generator.h
+++ b/src/expr/tconv_seq_proof_generator.h
@@ -22,7 +22,7 @@
 #include "expr/proof_generator.h"
 #include "theory/trust_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofNodeManager;
 
@@ -115,6 +115,6 @@ class TConvSeqProofGenerator : public ProofGenerator
   std::string d_name;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */
diff --git a/src/expr/term_canonize.cpp b/src/expr/term_canonize.cpp
index 72c59136b..97f3c2539 100644
--- a/src/expr/term_canonize.cpp
+++ b/src/expr/term_canonize.cpp
@@ -19,9 +19,9 @@
 // TODO #1216: move the code in this include
 #include "theory/quantifiers/term_util.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 TermCanonize::TermCanonize() : d_op_id_count(0), d_typ_id_count(0) {}
@@ -209,4 +209,4 @@ Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar)
 }
 
 }  // namespace expr
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/term_canonize.h b/src/expr/term_canonize.h
index 3eefb0c4a..f9f0fda24 100644
--- a/src/expr/term_canonize.h
+++ b/src/expr/term_canonize.h
@@ -20,7 +20,7 @@
 #include <map>
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 /** TermCanonize
@@ -100,6 +100,6 @@ class TermCanonize
 };
 
 }  // namespace expr
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__TERM_CANONIZE_H */
diff --git a/src/expr/term_context.cpp b/src/expr/term_context.cpp
index 2ade0943d..56c38a17c 100644
--- a/src/expr/term_context.cpp
+++ b/src/expr/term_context.cpp
@@ -14,7 +14,7 @@
 
 #include "expr/term_context.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 uint32_t TermContext::computeValueOp(TNode t, uint32_t tval) const
 {
@@ -132,4 +132,4 @@ void PolarityTermContext::getFlags(uint32_t val, bool& hasPol, bool& pol)
   pol = val == 2;
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/term_context.h b/src/expr/term_context.h
index 7b4dbe928..65cdbb23e 100644
--- a/src/expr/term_context.h
+++ b/src/expr/term_context.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * This is an abstract class for computing "term context identifiers". A term
@@ -163,6 +163,6 @@ class PolarityTermContext : public TermContext
   static void getFlags(uint32_t val, bool& hasPol, bool& pol);
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
diff --git a/src/expr/term_context_node.cpp b/src/expr/term_context_node.cpp
index 871193442..1afc599d2 100644
--- a/src/expr/term_context_node.cpp
+++ b/src/expr/term_context_node.cpp
@@ -16,7 +16,7 @@
 
 #include "expr/term_context.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 TCtxNode::TCtxNode(Node n, const TermContext* tctx)
     : d_node(n), d_val(tctx->initialValue()), d_tctx(tctx)
@@ -73,4 +73,4 @@ Node TCtxNode::decomposeNodeHash(Node h, uint32_t& val)
   return h[0];
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/term_context_node.h b/src/expr/term_context_node.h
index 15e7f9f1b..67d747557 100644
--- a/src/expr/term_context_node.h
+++ b/src/expr/term_context_node.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class TCtxStack;
 class TermContext;
@@ -74,6 +74,6 @@ class TCtxNode
   const TermContext* d_tctx;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
diff --git a/src/expr/term_context_stack.cpp b/src/expr/term_context_stack.cpp
index 07d7746ed..557683498 100644
--- a/src/expr/term_context_stack.cpp
+++ b/src/expr/term_context_stack.cpp
@@ -16,7 +16,7 @@
 
 #include "expr/term_context.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 TCtxStack::TCtxStack(const TermContext* tctx) : d_tctx(tctx) {}
 
@@ -75,4 +75,4 @@ TCtxNode TCtxStack::getCurrentNode() const
   return TCtxNode(curr.first, curr.second, d_tctx);
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/term_context_stack.h b/src/expr/term_context_stack.h
index f40f5f6b2..34c474a52 100644
--- a/src/expr/term_context_stack.h
+++ b/src/expr/term_context_stack.h
@@ -19,7 +19,7 @@
 
 #include "expr/term_context_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * A stack for term-context-sensitive terms. Its main advantage is that
@@ -68,6 +68,6 @@ class TCtxStack
   const TermContext* d_tctx;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__TERM_CONTEXT_STACK_H */
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
index 470b8c9f8..bfdf4d188 100644
--- a/src/expr/term_conversion_proof_generator.cpp
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -21,9 +21,9 @@
 #include "expr/term_context.h"
 #include "expr/term_context_stack.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 
 std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol)
 {
@@ -588,4 +588,4 @@ std::string TConvProofGenerator::toStringDebug() const
   return ss.str();
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h
index acff2ded1..734ef103e 100644
--- a/src/expr/term_conversion_proof_generator.h
+++ b/src/expr/term_conversion_proof_generator.h
@@ -21,7 +21,7 @@
 #include "expr/lazy_proof.h"
 #include "expr/proof_generator.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofNodeManager;
 class TermContext;
@@ -242,6 +242,6 @@ class TConvProofGenerator : public ProofGenerator
   std::string toStringDebug() const;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h
index 0ca2fb806..b502d8013 100644
--- a/src/expr/type_checker.h
+++ b/src/expr/type_checker.h
@@ -22,7 +22,7 @@
 #ifndef CVC4__EXPR__TYPE_CHECKER_H
 #define CVC4__EXPR__TYPE_CHECKER_H
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 class TypeChecker {
@@ -35,7 +35,7 @@ public:
 
 };/* class TypeChecker */
 
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
+}  // namespace expr
+}  // namespace CVC5
 
 #endif /* CVC4__EXPR__TYPE_CHECKER_H */
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 527f98384..07dca77e2 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -23,7 +23,7 @@
 
 ${typechecker_includes}
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check)
@@ -71,5 +71,5 @@ ${construles}
 
 }/* TypeChecker::computeIsConst */
 
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
+}  // namespace expr
+}  // namespace CVC5
diff --git a/src/expr/type_checker_util.h b/src/expr/type_checker_util.h
index 5f227423b..1ca23d374 100644
--- a/src/expr/type_checker_util.h
+++ b/src/expr/type_checker_util.h
@@ -26,7 +26,7 @@
 #include "expr/node_manager.h"
 #include "expr/type_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace expr {
 
 /** Type check returns the builtin operator sort */
@@ -202,4 +202,4 @@ class SimpleTypeRuleVar
 };
 
 }  // namespace expr
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/type_matcher.cpp b/src/expr/type_matcher.cpp
index b71a4b515..76d256157 100644
--- a/src/expr/type_matcher.cpp
+++ b/src/expr/type_matcher.cpp
@@ -14,7 +14,7 @@
 
 #include "type_matcher.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 TypeMatcher::TypeMatcher(TypeNode dt)
 {
@@ -125,4 +125,4 @@ void TypeMatcher::getMatches(std::vector<TypeNode>& types) const
   }
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/expr/type_matcher.h b/src/expr/type_matcher.h
index 98c3ce865..651054313 100644
--- a/src/expr/type_matcher.h
+++ b/src/expr/type_matcher.h
@@ -21,7 +21,7 @@
 
 #include "expr/type_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * This class is used for inferring the parameters of an instantiated
@@ -68,6 +68,6 @@ class TypeMatcher
   void addTypes(const std::vector<TypeNode>& types);
 }; /* class TypeMatcher */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__MATCHER_H */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 8d474ca5f..f73bde3eb 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -25,7 +25,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 
 TypeNode TypeNode::s_null( &expr::NodeValue::null() );
 
@@ -499,7 +499,7 @@ TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){
 
 TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
   Assert(NodeManager::currentNM() != NULL)
-      << "There is no current CVC4::NodeManager associated to this thread.\n"
+      << "There is no current CVC5::NodeManager associated to this thread.\n"
          "Perhaps a public-facing function is missing a NodeManagerScope ?";
 
   Assert(!t0.isNull());
@@ -717,4 +717,4 @@ TypeNode TypeNode::getBagElementType() const
   return (*this)[0];
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index baff528ff..7b752c3e5 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -32,14 +32,14 @@
 #include "expr/metakind.h"
 #include "util/cardinality.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class NodeManager;
 class DType;
 
 namespace expr {
   class NodeValue;
-}/* CVC4::expr namespace */
+  }  // namespace expr
 
 /**
  * Encapsulation of an NodeValue pointer for Types. The reference count is
@@ -749,11 +749,11 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
 
 typedef TypeNode::HashFunction TypeNodeHashFunction;
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #include "expr/node_manager.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 inline TypeNode
 TypeNode::substitute(const TypeNode& type,
@@ -860,7 +860,7 @@ template <class AttrKind>
 inline typename AttrKind::value_type TypeNode::
 getAttribute(const AttrKind&) const {
   Assert(NodeManager::currentNM() != NULL)
-      << "There is no current CVC4::NodeManager associated to this thread.\n"
+      << "There is no current CVC5::NodeManager associated to this thread.\n"
          "Perhaps a public-facing function is missing a NodeManagerScope ?";
   return NodeManager::currentNM()->getAttribute(d_nv, AttrKind());
 }
@@ -869,7 +869,7 @@ template <class AttrKind>
 inline bool TypeNode::
 hasAttribute(const AttrKind&) const {
   Assert(NodeManager::currentNM() != NULL)
-      << "There is no current CVC4::NodeManager associated to this thread.\n"
+      << "There is no current CVC5::NodeManager associated to this thread.\n"
          "Perhaps a public-facing function is missing a NodeManagerScope ?";
   return NodeManager::currentNM()->hasAttribute(d_nv, AttrKind());
 }
@@ -877,7 +877,7 @@ hasAttribute(const AttrKind&) const {
 template <class AttrKind>
 inline bool TypeNode::getAttribute(const AttrKind&, typename AttrKind::value_type& ret) const {
   Assert(NodeManager::currentNM() != NULL)
-      << "There is no current CVC4::NodeManager associated to this thread.\n"
+      << "There is no current CVC5::NodeManager associated to this thread.\n"
          "Perhaps a public-facing function is missing a NodeManagerScope ?";
   return NodeManager::currentNM()->getAttribute(d_nv, AttrKind(), ret);
 }
@@ -886,7 +886,7 @@ template <class AttrKind>
 inline void TypeNode::
 setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
   Assert(NodeManager::currentNM() != NULL)
-      << "There is no current CVC4::NodeManager associated to this thread.\n"
+      << "There is no current CVC5::NodeManager associated to this thread.\n"
          "Perhaps a public-facing function is missing a NodeManagerScope ?";
   NodeManager::currentNM()->setAttribute(d_nv, AttrKind(), value);
 }
@@ -1069,6 +1069,6 @@ static void __attribute__((used)) debugPrintRawTypeNode(const TypeNode& n) {
 }
 #endif /* CVC4_DEBUG */
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__NODE_H */
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
index c0f9fb844..abf5e6173 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -29,7 +29,7 @@
 
 ${type_properties_includes}
 
-namespace CVC4 {
+namespace CVC5 {
 namespace kind {
 
 /**
@@ -113,7 +113,7 @@ ${type_groundterms}
   }
 } /* mkGroundTerm(TypeNode) */
 
-}/* CVC4::kind namespace */
-}/* CVC4 namespace */
+}  // namespace kind
+}  // namespace CVC5
 
 #endif /* CVC4__TYPE_PROPERTIES_H */
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
index b2d5a2b12..9d8b12264 100644
--- a/src/expr/uninterpreted_constant.cpp
+++ b/src/expr/uninterpreted_constant.cpp
@@ -26,7 +26,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 
 UninterpretedConstant::UninterpretedConstant(const TypeNode& type,
                                              Integer index)
@@ -95,4 +95,4 @@ size_t UninterpretedConstantHashFunction::operator()(
          * IntegerHashFunction()(uc.getIndex());
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h
index e7c0f9830..00ad68212 100644
--- a/src/expr/uninterpreted_constant.h
+++ b/src/expr/uninterpreted_constant.h
@@ -24,7 +24,7 @@
 
 #include "util/integer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class TypeNode;
 
@@ -60,6 +60,6 @@ struct UninterpretedConstantHashFunction
   size_t operator()(const UninterpretedConstant& uc) const;
 }; /* struct UninterpretedConstantHashFunction */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__UNINTERPRETED_CONSTANT_H */
author	Aina Niemetz <aina.niemetz@gmail.com>	2021-03-31 15:23:17 -0700
committer	GitHub <noreply@github.com>	2021-03-31 22:23:17 +0000
commit	a1466978fbc328507406d4a121dab4d1a1047e1d (patch)
tree	12b40f161bb4d7a6ee40c20c78a15d6cda3c1995 /src/expr
parent	f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff)