Rename namespace CVC4 to CVC5. (#6249)

26 files changed, 111 insertions, 115 deletions

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index ef1b3e8d5..84e7786e8 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -25,9 +25,9 @@
 #include "theory/valuation.h"
 
 using namespace std;
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -1114,4 +1114,4 @@ const std::vector<Node>& CardinalityExtension::getFiniteTypeMembers(
 
 }  // namespace sets
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h
index c353f86b8..47fa18d5b 100644
--- a/src/theory/sets/cardinality_extension.h
+++ b/src/theory/sets/cardinality_extension.h
@@ -25,7 +25,7 @@
 #include "theory/type_set.h"
 #include "theory/uf/equality_engine.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -412,6 +412,6 @@ class CardinalityExtension
 
 }  // namespace sets
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index 9e16bfb97..305059797 100644
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -18,9 +18,9 @@
 #include "theory/rewriter.h"
 
 using namespace std;
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -177,4 +177,4 @@ void InferenceManager::split(Node n, InferenceId id, int reqPol)
 
 }  // namespace sets
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h
index ce561f454..8e4614718 100644
--- a/src/theory/sets/inference_manager.h
+++ b/src/theory/sets/inference_manager.h
@@ -20,7 +20,7 @@
 #include "theory/inference_manager_buffered.h"
 #include "theory/sets/solver_state.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -100,6 +100,6 @@ class InferenceManager : public InferenceManagerBuffered
 
 }  // namespace sets
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__SETS__INFERENCE_MANAGER_H */
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 57120e42e..4ef22d68c 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -5,10 +5,10 @@
 #
 
 theory THEORY_SETS \
-    ::CVC4::theory::sets::TheorySets \
+    ::CVC5::theory::sets::TheorySets \
     "theory/sets/theory_sets.h"
 typechecker "theory/sets/theory_sets_type_rules.h"
-rewriter ::CVC4::theory::sets::TheorySetsRewriter \
+rewriter ::CVC5::theory::sets::TheorySetsRewriter \
     "theory/sets/theory_sets_rewriter.h"
 
 properties parametric
@@ -16,22 +16,22 @@ properties check presolve
 
 # constants
 constant EMPTYSET \
-    ::CVC4::EmptySet \
-    ::CVC4::EmptySetHashFunction \
+    ::CVC5::EmptySet \
+    ::CVC5::EmptySetHashFunction \
     "expr/emptyset.h" \
-    "the empty set constant; payload is an instance of the CVC4::EmptySet class"
+    "the empty set constant; payload is an instance of the CVC5::EmptySet class"
 
 # the type
 operator SET_TYPE 1 "set type, takes as parameter the type of the elements"
 cardinality SET_TYPE \
-    "::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
+    "::CVC5::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
     "theory/sets/theory_sets_type_rules.h"
 well-founded SET_TYPE \
-    "::CVC4::theory::sets::SetsProperties::isWellFounded(%TYPE%)" \
-    "::CVC4::theory::sets::SetsProperties::mkGroundTerm(%TYPE%)" \
+    "::CVC5::theory::sets::SetsProperties::isWellFounded(%TYPE%)" \
+    "::CVC5::theory::sets::SetsProperties::mkGroundTerm(%TYPE%)" \
     "theory/sets/theory_sets_type_rules.h"
 enumerator SET_TYPE \
-    "::CVC4::theory::sets::SetEnumerator" \
+    "::CVC5::theory::sets::SetEnumerator" \
     "theory/sets/theory_sets_type_enumerator.h"
 
 # operators
@@ -42,10 +42,10 @@ operator SUBSET         2  "subset predicate; first parameter a subset of second
 operator MEMBER         2  "set membership predicate; first parameter a member of second"
 
 constant SINGLETON_OP \
-	::CVC4::SingletonOp \
-	::CVC4::SingletonOpHashFunction \
+	::CVC5::SingletonOp \
+	::CVC5::SingletonOpHashFunction \
 	"theory/sets/singleton_op.h" \
-	"operator for singletons; payload is an instance of the CVC4::SingletonOp class"
+	"operator for singletons; payload is an instance of the CVC5::SingletonOp class"
 parameterized SINGLETON SINGLETON_OP 1  \
 "constructs a set of a single element. First parameter is a SingletonOp. Second is a term"
 
@@ -85,30 +85,30 @@ operator TCLOSURE      1  "set transitive closure"
 operator JOIN_IMAGE	   2  "set join image"
 operator IDEN 	   	   1  "set identity"
 
-typerule UNION          ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
-typerule INTERSECTION   ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
-typerule SETMINUS       ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
-typerule SUBSET         ::CVC4::theory::sets::SubsetTypeRule
-typerule MEMBER         ::CVC4::theory::sets::MemberTypeRule
+typerule UNION          ::CVC5::theory::sets::SetsBinaryOperatorTypeRule
+typerule INTERSECTION   ::CVC5::theory::sets::SetsBinaryOperatorTypeRule
+typerule SETMINUS       ::CVC5::theory::sets::SetsBinaryOperatorTypeRule
+typerule SUBSET         ::CVC5::theory::sets::SubsetTypeRule
+typerule MEMBER         ::CVC5::theory::sets::MemberTypeRule
 typerule SINGLETON_OP   "SimpleTypeRule<RBuiltinOperator>"
-typerule SINGLETON      ::CVC4::theory::sets::SingletonTypeRule
-typerule EMPTYSET       ::CVC4::theory::sets::EmptySetTypeRule
-typerule INSERT         ::CVC4::theory::sets::InsertTypeRule
-typerule CARD           ::CVC4::theory::sets::CardTypeRule
-typerule COMPLEMENT     ::CVC4::theory::sets::ComplementTypeRule
-typerule UNIVERSE_SET   ::CVC4::theory::sets::UniverseSetTypeRule
-typerule COMPREHENSION  ::CVC4::theory::sets::ComprehensionTypeRule
-typerule CHOOSE         ::CVC4::theory::sets::ChooseTypeRule
-typerule IS_SINGLETON   ::CVC4::theory::sets::IsSingletonTypeRule
+typerule SINGLETON      ::CVC5::theory::sets::SingletonTypeRule
+typerule EMPTYSET       ::CVC5::theory::sets::EmptySetTypeRule
+typerule INSERT         ::CVC5::theory::sets::InsertTypeRule
+typerule CARD           ::CVC5::theory::sets::CardTypeRule
+typerule COMPLEMENT     ::CVC5::theory::sets::ComplementTypeRule
+typerule UNIVERSE_SET   ::CVC5::theory::sets::UniverseSetTypeRule
+typerule COMPREHENSION  ::CVC5::theory::sets::ComprehensionTypeRule
+typerule CHOOSE         ::CVC5::theory::sets::ChooseTypeRule
+typerule IS_SINGLETON   ::CVC5::theory::sets::IsSingletonTypeRule
 
-typerule JOIN 			::CVC4::theory::sets::RelBinaryOperatorTypeRule
-typerule PRODUCT 		::CVC4::theory::sets::RelBinaryOperatorTypeRule
-typerule TRANSPOSE 		::CVC4::theory::sets::RelTransposeTypeRule
-typerule TCLOSURE 	    ::CVC4::theory::sets::RelTransClosureTypeRule
-typerule JOIN_IMAGE	    ::CVC4::theory::sets::JoinImageTypeRule
-typerule IDEN 			::CVC4::theory::sets::RelIdenTypeRule
+typerule JOIN 			::CVC5::theory::sets::RelBinaryOperatorTypeRule
+typerule PRODUCT 		::CVC5::theory::sets::RelBinaryOperatorTypeRule
+typerule TRANSPOSE 		::CVC5::theory::sets::RelTransposeTypeRule
+typerule TCLOSURE 	    ::CVC5::theory::sets::RelTransClosureTypeRule
+typerule JOIN_IMAGE	    ::CVC5::theory::sets::JoinImageTypeRule
+typerule IDEN 			::CVC5::theory::sets::RelIdenTypeRule
 
-construle UNION         ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
-construle SINGLETON     ::CVC4::theory::sets::SingletonTypeRule
+construle UNION         ::CVC5::theory::sets::SetsBinaryOperatorTypeRule
+construle SINGLETON     ::CVC5::theory::sets::SingletonTypeRule
 
 endtheory
diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h
index 4033a6b44..197f31903 100644
--- a/src/theory/sets/normal_form.h
+++ b/src/theory/sets/normal_form.h
@@ -19,7 +19,7 @@
 #ifndef CVC4__THEORY__SETS__NORMAL_FORM_H
 #define CVC4__THEORY__SETS__NORMAL_FORM_H
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -158,6 +158,6 @@ class NormalForm {
 };
 }
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h
index a85e2d27c..eb3477f5a 100644
--- a/src/theory/sets/rels_utils.h
+++ b/src/theory/sets/rels_utils.h
@@ -21,7 +21,7 @@
 #include "expr/dtype_cons.h"
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -95,9 +95,9 @@ public:
         kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), a, b);
   }     
     
-};             
-}/* CVC4::theory::sets namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+};
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/sets/singleton_op.cpp b/src/theory/sets/singleton_op.cpp
index 5ef863fe8..4e76d35e4 100644
--- a/src/theory/sets/singleton_op.cpp
+++ b/src/theory/sets/singleton_op.cpp
@@ -18,7 +18,7 @@
 
 #include "expr/type_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 std::ostream& operator<<(std::ostream& out, const SingletonOp& op)
 {
@@ -47,4 +47,4 @@ bool SingletonOp::operator==(const SingletonOp& op) const
   return getType() == op.getType();
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/sets/singleton_op.h b/src/theory/sets/singleton_op.h
index 7d7bb85b6..d17f8255e 100644
--- a/src/theory/sets/singleton_op.h
+++ b/src/theory/sets/singleton_op.h
@@ -19,7 +19,7 @@
 
 #include <memory>
 
-namespace CVC4 {
+namespace CVC5 {
 
 class TypeNode;
 
@@ -58,6 +58,6 @@ struct SingletonOpHashFunction
   size_t operator()(const SingletonOp& op) const;
 }; /* struct SingletonOpHashFunction */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__SINGLETON_OP_H */
diff --git a/src/theory/sets/skolem_cache.cpp b/src/theory/sets/skolem_cache.cpp
index 1deb28688..3c0f33caf 100644
--- a/src/theory/sets/skolem_cache.cpp
+++ b/src/theory/sets/skolem_cache.cpp
@@ -16,9 +16,9 @@
 
 #include "theory/rewriter.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -61,4 +61,4 @@ bool SkolemCache::isSkolem(Node n) const
 
 }  // namespace sets
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/sets/skolem_cache.h b/src/theory/sets/skolem_cache.h
index a4997baf0..42369c7a9 100644
--- a/src/theory/sets/skolem_cache.h
+++ b/src/theory/sets/skolem_cache.h
@@ -22,7 +22,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -78,6 +78,6 @@ class SkolemCache
 
 }  // namespace sets
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */
diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
index 43f8a7d17..ff604f838 100644
--- a/src/theory/sets/solver_state.cpp
+++ b/src/theory/sets/solver_state.cpp
@@ -19,9 +19,9 @@
 #include "theory/sets/theory_sets_private.h"
 
 using namespace std;
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -595,4 +595,4 @@ bool SolverState::merge(TNode t1,
 
 }  // namespace sets
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h
index 06ae41c9a..431aa019d 100644
--- a/src/theory/sets/solver_state.h
+++ b/src/theory/sets/solver_state.h
@@ -24,7 +24,7 @@
 #include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -268,6 +268,6 @@ class SolverState : public TheoryState
 
 }  // namespace sets
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H */
diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp
index e32255eab..6dc18591c 100644
--- a/src/theory/sets/term_registry.cpp
+++ b/src/theory/sets/term_registry.cpp
@@ -17,9 +17,9 @@
 #include "expr/emptyset.h"
 
 using namespace std;
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -151,4 +151,4 @@ void TermRegistry::debugPrintSet(Node s, const char* c) const
 
 }  // namespace sets
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/sets/term_registry.h b/src/theory/sets/term_registry.h
index 204b14504..913473ff0 100644
--- a/src/theory/sets/term_registry.h
+++ b/src/theory/sets/term_registry.h
@@ -25,7 +25,7 @@
 #include "theory/sets/skolem_cache.h"
 #include "theory/sets/solver_state.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -89,6 +89,6 @@ class TermRegistry
 
 }  // namespace sets
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__SETS__TERM_REGISTRY_H */
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index f3ad57535..1530da809 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -22,9 +22,9 @@
 #include "theory/theory_model.h"
 #include "theory/trust_substitutions.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -236,6 +236,6 @@ void TheorySets::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
   d_theory.eqNotifyDisequal(t1, t2, reason);
 }
 
-}/* CVC4::theory::sets namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC5
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 56b0d6290..4dc5d8a0d 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -29,7 +29,7 @@
 #include "theory/theory_eq_notify.h"
 #include "theory/uf/equality_engine.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -118,8 +118,8 @@ class TheorySets : public Theory
   NotifyClass d_notify;
 }; /* class TheorySets */
 
-}/* CVC4::theory::sets namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__SETS__THEORY_SETS_H */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index da2958c5c..285eac473 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -29,9 +29,9 @@
 #include "util/result.h"
 
 using namespace std;
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -1372,4 +1372,4 @@ void TheorySetsPrivate::presolve() { d_state.reset(); }
 
 }  // namespace sets
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 329fbfc17..a822d06e7 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -31,7 +31,7 @@
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -234,9 +234,8 @@ class TheorySetsPrivate {
   std::map<Node, Node> d_isSingletonNodes;
 };/* class TheorySetsPrivate */
 
-
-}/* CVC4::theory::sets namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H */
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 3570aa9d8..a160e0afd 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -19,9 +19,9 @@
 #include "theory/sets/theory_sets.h"
 
 using namespace std;
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -1333,4 +1333,4 @@ void TheorySetsRels::check(Theory::Effort level)
   }
 }
 }
-}
+}  // namespace CVC5
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index 6820c6f15..93913d4f5 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -28,7 +28,7 @@
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -183,11 +183,8 @@ private:
   bool isRel( Node n ) {return n.getType().isSet() && n.getType().getSetElementType().isTuple();}
 };
 
-
-}/* CVC4::theory::sets namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC5
 
 #endif /* SRC_THEORY_SETS_THEORY_SETS_RELS_H_ */
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 6eef046e6..935eb548d 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -22,9 +22,9 @@
 #include "theory/sets/normal_form.h"
 #include "theory/sets/rels_utils.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -540,6 +540,6 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
   return RewriteResponse(REWRITE_DONE, node);
 }
 
-}/* CVC4::theory::sets namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC5
diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h
index eeecf06a7..739a5f885 100644
--- a/src/theory/sets/theory_sets_rewriter.h
+++ b/src/theory/sets/theory_sets_rewriter.h
@@ -21,7 +21,7 @@
 
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -77,8 +77,8 @@ private:
   bool checkConstantMembership(TNode elementTerm, TNode setTerm);
 }; /* class TheorySetsRewriter */
 
-}/* CVC4::theory::sets namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H */
diff --git a/src/theory/sets/theory_sets_type_enumerator.cpp b/src/theory/sets/theory_sets_type_enumerator.cpp
index ceb87d8ec..30e279be7 100644
--- a/src/theory/sets/theory_sets_type_enumerator.cpp
+++ b/src/theory/sets/theory_sets_type_enumerator.cpp
@@ -16,7 +16,7 @@
 
 #include "theory/sets/theory_sets_type_enumerator.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -130,4 +130,4 @@ bool SetEnumerator::isFinished()
 
 }  // namespace sets
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h
index 4aaf07035..32aca5f79 100644
--- a/src/theory/sets/theory_sets_type_enumerator.h
+++ b/src/theory/sets/theory_sets_type_enumerator.h
@@ -26,7 +26,7 @@
 #include "theory/sets/normal_form.h"
 #include "theory/type_enumerator.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -68,6 +68,6 @@ class SetEnumerator : public TypeEnumeratorBase<SetEnumerator>
 
 }  // namespace sets
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__SETS__TYPE_ENUMERATOR_H */
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 9f7875e18..54791ac31 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -23,7 +23,7 @@
 
 #include "theory/sets/normal_form.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace sets {
 
@@ -390,7 +390,7 @@ struct JoinImageTypeRule {
       throw TypeCheckingExceptionPrivate(
           n, " JoinImage cardinality constraint must be a constant");
     }
-    CVC4::Rational r(INT_MAX);
+    CVC5::Rational r(INT_MAX);
     if (n[1].getConst<Rational>() > r) {
       throw TypeCheckingExceptionPrivate(
           n, " JoinImage Exceeded INT_MAX in cardinality constraint");
@@ -442,8 +442,8 @@ struct SetsProperties {
   }
 };/* struct SetsProperties */
 
-}/* CVC4::theory::sets namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */