Rename namespace CVC5 to cvc5. (#6258)

author: Aina Niemetz <aina.niemetz@gmail.com> 2021-04-01 09:56:14 -0700
committer: GitHub <noreply@github.com> 2021-04-01 16:56:14 +0000
commit: 05a53a2ac405bcd18a84024247145f161809c3b0 (patch)
tree: 34241c0a82f79d717ddbfbb0c294f9a09c7edb0c /src/expr
parent: afaf4413775ff7d6054a5893f1397ad908e0773c (diff)
115 files changed, 357 insertions, 357 deletions
diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index d50921598..b92ba8607 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -26,7 +26,7 @@
 
 using namespace std;
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h
index 974f456ef..65385b0c4 100644
--- a/src/expr/array_store_all.h
+++ b/src/expr/array_store_all.h
@@ -24,7 +24,7 @@
 #include <iosfwd>
 #include <memory>
 
-namespace CVC5 {
+namespace cvc5 {
 
 template <bool ref_count>
 class NodeTemplate;
@@ -69,6 +69,6 @@ struct ArrayStoreAllHashFunction
   size_t operator()(const ArrayStoreAll& asa) const;
 }; /* struct ArrayStoreAllHashFunction */
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__ARRAY_STORE_ALL_H */
diff --git a/src/expr/ascription_type.cpp b/src/expr/ascription_type.cpp
index 6fecb2978..83254f5a5 100644
--- a/src/expr/ascription_type.cpp
+++ b/src/expr/ascription_type.cpp
@@ -18,7 +18,7 @@
 
 #include "expr/type_node.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h
index 5b0ff2b71..b216a0fa1 100644
--- a/src/expr/ascription_type.h
+++ b/src/expr/ascription_type.h
@@ -22,7 +22,7 @@
 #include <iosfwd>
 #include <memory>
 
-namespace CVC5 {
+namespace cvc5 {
 
 class TypeNode;
 
@@ -60,6 +60,6 @@ struct AscriptionTypeHashFunction
 /** An output routine for AscriptionTypes */
 std::ostream& operator<<(std::ostream& out, AscriptionType at);
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__ASCRIPTION_TYPE_H */
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index fe1bff897..062f0a2d2 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -22,7 +22,7 @@
 
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace expr {
 namespace attr {
 
@@ -116,4 +116,4 @@ void AttributeManager::deleteAttributes(const AttrIdVec& atids) {
 
 }  // namespace attr
 }  // namespace expr
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index b3a3eb717..6156ccc2d 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 CVC5 {
+namespace cvc5 {
 namespace expr {
 namespace attr {
 
@@ -621,6 +621,6 @@ NodeManager::setAttribute(TypeNode n, const AttrKind&,
   d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__ATTRIBUTE_H */
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index bbd5455be..db3e57675 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -25,7 +25,7 @@
 
 #include <unordered_map>
 
-namespace CVC5 {
+namespace cvc5 {
 namespace expr {
 
 // ATTRIBUTE HASH FUNCTIONS ====================================================
@@ -512,6 +512,6 @@ const uint64_t Attribute<T, bool, context_dep>::s_id =
     Attribute<T, bool, context_dep>::registerAttribute();
 
 }  // namespace expr
-}  // namespace CVC5
+}  // 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 f084baaa1..b475a700d 100644
--- a/src/expr/attribute_unique_id.h
+++ b/src/expr/attribute_unique_id.h
@@ -21,7 +21,7 @@
 
 // ATTRIBUTE IDs ============================================================
 
-namespace CVC5 {
+namespace cvc5 {
 namespace expr {
 namespace attr {
 
@@ -59,8 +59,8 @@ public:
   AttrTableId getTableId() const{ return d_tableId; }
   uint64_t getWithinTypeId() const{ return d_withinTypeId; }
 
-}; /* CVC5::expr::attr::AttributeUniqueId */
+}; /* cvc5::expr::attr::AttributeUniqueId */
 
 }  // namespace attr
 }  // namespace expr
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/bound_var_manager.cpp b/src/expr/bound_var_manager.cpp
index ca257d313..e97e559a8 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 CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h
index 08705f6d2..ebd107737 100644
--- a/src/expr/bound_var_manager.h
+++ b/src/expr/bound_var_manager.h
@@ -22,7 +22,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 /**
  * Bound variable manager.
@@ -98,6 +98,6 @@ class BoundVarManager
   std::unordered_set<Node, NodeHashFunction> d_cacheVals;
 };
 
-}  // namespace CVC5
+}  // 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 caf6b0841..40820ea20 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 CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h
index db8e50274..7399b3741 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 CVC5 {
+namespace cvc5 {
 
 class ProofNodeManager;
 class ProofStep;
@@ -57,6 +57,6 @@ class BufferedProofGenerator : public ProofGenerator
   ProofNodeManager* d_pnm;
 };
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H */
diff --git a/src/expr/datatype_index.cpp b/src/expr/datatype_index.cpp
index 2459c86d8..6f530529a 100644
--- a/src/expr/datatype_index.cpp
+++ b/src/expr/datatype_index.cpp
@@ -20,7 +20,7 @@
 
 using namespace std;
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/datatype_index.h b/src/expr/datatype_index.h
index 08d33ca83..a239c387b 100644
--- a/src/expr/datatype_index.h
+++ b/src/expr/datatype_index.h
@@ -19,7 +19,7 @@
 
 #include <iosfwd>
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__DATATYPE_H */
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 35ad5ff4c..3302be018 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 CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index 5b6ec4a7d..524702bdd 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 CVC5 {
+namespace cvc5 {
 
 // ----------------------- datatype attributes
 /**
@@ -696,6 +696,6 @@ struct DTypeIndexConstantHashFunction
 
 std::ostream& operator<<(std::ostream& os, const DType& dt);
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index 089d41637..59b870897 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 CVC5::kind;
-using namespace CVC5::theory;
+using namespace cvc5::kind;
+using namespace cvc5::theory;
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h
index 245d461b0..d444d9261 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 CVC5 {
+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 CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp
index a276c3734..d6a3b4469 100644
--- a/src/expr/dtype_selector.cpp
+++ b/src/expr/dtype_selector.cpp
@@ -16,9 +16,9 @@
 
 #include "options/set_language.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/dtype_selector.h b/src/expr/dtype_selector.h
index 7404c0c96..d45bcf8c5 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 CVC5 {
+namespace cvc5 {
 
 class DatatypeConstructorArg;
 class DType;
@@ -90,6 +90,6 @@ class DTypeSelector
 
 std::ostream& operator<<(std::ostream& os, const DTypeSelector& arg);
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/expr/emptybag.cpp b/src/expr/emptybag.cpp
index 0f7a3a73e..d45612a9c 100644
--- a/src/expr/emptybag.cpp
+++ b/src/expr/emptybag.cpp
@@ -18,7 +18,7 @@
 
 #include "expr/type_node.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/emptybag.h b/src/expr/emptybag.h
index 59060eaa8..f45bd9e96 100644
--- a/src/expr/emptybag.h
+++ b/src/expr/emptybag.h
@@ -20,7 +20,7 @@
 #include <iosfwd>
 #include <memory>
 
-namespace CVC5 {
+namespace cvc5 {
 
 class TypeNode;
 
@@ -58,6 +58,6 @@ struct EmptyBagHashFunction
   size_t operator()(const EmptyBag& es) const;
 }; /* struct EmptyBagHashFunction */
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EMPTY_BAG_H */
diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp
index 4a0bd4e51..4d6604a63 100644
--- a/src/expr/emptyset.cpp
+++ b/src/expr/emptyset.cpp
@@ -21,7 +21,7 @@
 
 #include "expr/type_node.h"
 
-namespace CVC5 {
+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); }
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h
index febb4e111..aa6d5e143 100644
--- a/src/expr/emptyset.h
+++ b/src/expr/emptyset.h
@@ -23,7 +23,7 @@
 #include <iosfwd>
 #include <memory>
 
-namespace CVC5 {
+namespace cvc5 {
 
 class TypeNode;
 
@@ -60,6 +60,6 @@ struct EmptySetHashFunction
   size_t operator()(const EmptySet& es) const;
 }; /* struct EmptySetHashFunction */
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EMPTY_SET_H */
diff --git a/src/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp
index 4aec28b85..4417ccb5c 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 CVC5 {
+namespace cvc5 {
 namespace expr {
 
 const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc();
@@ -123,4 +123,4 @@ std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) {
 }
 
 }  // namespace expr
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h
index c40840cd4..674d4c6fd 100644
--- a/src/expr/expr_iomanip.h
+++ b/src/expr/expr_iomanip.h
@@ -21,7 +21,7 @@
 
 #include <iosfwd>
 
-namespace CVC5 {
+namespace cvc5 {
 namespace expr {
 
 /**
@@ -173,6 +173,6 @@ std::ostream& operator<<(std::ostream& out, ExprSetDepth sd);
 
 }  // namespace expr
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__EXPR_IOMANIP_H */
diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h
index e6f6f9ca0..0716ff4d0 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 CVC5 {
+namespace cvc5 {
 
 /** A very simple bitmap for Kinds */
 class KindMap
@@ -51,6 +51,6 @@ class KindMap
   std::bitset<kind::LAST_KIND> d_bits;
 };
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__KIND_MAP_H */
diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp
index cbe979642..d9f913ddf 100644
--- a/src/expr/kind_template.cpp
+++ b/src/expr/kind_template.cpp
@@ -19,12 +19,12 @@
 
 #include "expr/kind.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace kind {
 
-const char* toString(CVC5::Kind k)
+const char* toString(cvc5::Kind k)
 {
-  using namespace CVC5::kind;
+  using namespace cvc5::kind;
 
   switch (k)
   {
@@ -37,7 +37,7 @@ const char* toString(CVC5::Kind k)
   }
 }
 
-std::ostream& operator<<(std::ostream& out, CVC5::Kind k)
+std::ostream& operator<<(std::ostream& out, cvc5::Kind k)
 {
   out << toString(k);
   return out;
@@ -47,7 +47,7 @@ std::ostream& operator<<(std::ostream& out, CVC5::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(::CVC5::Kind k)
+bool isAssociative(::cvc5::Kind k)
 {
   switch(k) {
   case kind::AND:
@@ -61,7 +61,7 @@ bool isAssociative(::CVC5::Kind k)
   }
 }
 
-std::string kindToString(::CVC5::Kind k)
+std::string kindToString(::cvc5::Kind k)
 {
   std::stringstream ss;
   ss << k;
@@ -82,7 +82,7 @@ ${type_constant_descriptions}
 
 namespace theory {
 
-TheoryId kindToTheoryId(::CVC5::Kind k)
+TheoryId kindToTheoryId(::cvc5::Kind k)
 {
   switch(k) {
   case kind::UNDEFINED_KIND:
@@ -95,7 +95,7 @@ ${kind_to_theory_id}
   throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
 }
 
-TheoryId typeConstantToTheoryId(::CVC5::TypeConstant typeConstant)
+TheoryId typeConstantToTheoryId(::cvc5::TypeConstant typeConstant)
 {
   switch (typeConstant)
   {
@@ -107,4 +107,4 @@ ${type_constant_to_theory_id}
 }
 
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 4661cfa15..484e8c273 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 CVC5 {
+namespace cvc5 {
 namespace kind {
 
 enum Kind_t
@@ -39,7 +39,7 @@ enum Kind_t
 
 // import Kind into the "CVC4" namespace but keep the individual kind
 // constants under kind::
-typedef ::CVC5::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(CVC5::Kind k);
+const char* toString(cvc5::Kind k);
 
 /**
  * Writes a kind name to a stream.
@@ -61,17 +61,17 @@ const char* toString(CVC5::Kind k);
  * @param k The kind to write to the stream
  * @return The stream
  */
-std::ostream& operator<<(std::ostream&, CVC5::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(::CVC5::Kind k);
-std::string kindToString(::CVC5::Kind k);
+bool isAssociative(::cvc5::Kind k);
+std::string kindToString(::cvc5::Kind k);
 
 struct KindHashFunction {
-  inline size_t operator()(::CVC5::Kind k) const { return k; }
+  inline size_t operator()(::cvc5::Kind k) const { return k; }
 };/* struct KindHashFunction */
 
 }  // namespace kind
@@ -97,11 +97,11 @@ std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant);
 
 namespace theory {
 
-::CVC5::theory::TheoryId kindToTheoryId(::CVC5::Kind k);
-::CVC5::theory::TheoryId typeConstantToTheoryId(
-    ::CVC5::TypeConstant typeConstant);
+::cvc5::theory::TheoryId kindToTheoryId(::cvc5::Kind k);
+::cvc5::theory::TheoryId typeConstantToTheoryId(
+    ::cvc5::TypeConstant typeConstant);
 
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__KIND_H */
diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index 701cc55dc..95ce1406c 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 CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 
 LazyCDProof::LazyCDProof(ProofNodeManager* pnm,
                          ProofGenerator* dpg,
@@ -228,4 +228,4 @@ bool LazyCDProof::hasGenerator(Node fact) const
   return it != d_gens.end();
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
index 5c0de5c5b..3ab0ca49e 100644
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -19,7 +19,7 @@
 
 #include "expr/proof.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class ProofGenerator;
 class ProofNodeManager;
@@ -105,6 +105,6 @@ class LazyCDProof : public CDProof
   ProofGenerator* getGeneratorFor(Node fact, bool& isSym);
 };
 
-}  // namespace CVC5
+}  // 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 3651e53e1..7f14adc38 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 CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
index 7482e3ca4..41488c821 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 CVC5 {
+namespace cvc5 {
 
 class ProofNodeManager;
 
@@ -148,6 +148,6 @@ class LazyCDProofChain : public ProofGenerator
   ProofGenerator* d_defGen;
 };
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__LAZY_PROOF_CHAIN_H */
diff --git a/src/expr/match_trie.cpp b/src/expr/match_trie.cpp
index d3adeb50e..b014339ad 100644
--- a/src/expr/match_trie.cpp
+++ b/src/expr/match_trie.cpp
@@ -14,9 +14,9 @@
 
 #include "expr/match_trie.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace expr {
 
 bool MatchTrie::getMatches(Node n, NotifyMatch* ntm)
@@ -196,4 +196,4 @@ void MatchTrie::clear()
 }
 
 }  // namespace expr
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/match_trie.h b/src/expr/match_trie.h
index 45ff0c0c7..70ce549e1 100644
--- a/src/expr/match_trie.h
+++ b/src/expr/match_trie.h
@@ -22,7 +22,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace expr {
 
 /** A virtual class for notifications regarding matches. */
@@ -77,6 +77,6 @@ class MatchTrie
 };
 
 }  // namespace expr
-}  // namespace CVC5
+}  // 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 2f147b8b4..52502cbcd 100644
--- a/src/expr/metakind_template.cpp
+++ b/src/expr/metakind_template.cpp
@@ -19,7 +19,7 @@
 
 #include <iostream>
 
-namespace CVC5 {
+namespace cvc5 {
 namespace kind {
 
 /**
@@ -52,20 +52,20 @@ ${metakind_constantMaps}
 namespace kind {
 namespace metakind {
 
-size_t NodeValueCompare::constHash(const ::CVC5::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() << ::CVC5::expr::NodeValue::dKindToKind(nv->d_kind);
+default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv->d_kind);
   }
 }
 
 template <bool pool>
-bool NodeValueCompare::compare(const ::CVC5::expr::NodeValue* nv1,
-                               const ::CVC5::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;
@@ -76,7 +76,7 @@ bool NodeValueCompare::compare(const ::CVC5::expr::NodeValue* nv1,
     switch (nv1->d_kind)
     {
 ${metakind_compares}
-default: Unhandled() << ::CVC5::expr::NodeValue::dKindToKind(nv1->d_kind);
+default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv1->d_kind);
     }
   }
 
@@ -84,9 +84,9 @@ default: Unhandled() << ::CVC5::expr::NodeValue::dKindToKind(nv1->d_kind);
     return false;
   }
 
-  ::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();
+  ::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)) {
@@ -100,19 +100,19 @@ default: Unhandled() << ::CVC5::expr::NodeValue::dKindToKind(nv1->d_kind);
 }
 
 template bool NodeValueCompare::compare<true>(
-    const ::CVC5::expr::NodeValue* nv1, const ::CVC5::expr::NodeValue* nv2);
+    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);
+    const ::cvc5::expr::NodeValue* nv1, const ::cvc5::expr::NodeValue* nv2);
 
 void NodeValueConstPrinter::toStream(std::ostream& out,
-                                     const ::CVC5::expr::NodeValue* nv)
+                                     const ::cvc5::expr::NodeValue* nv)
 {
   Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
 
   switch (nv->d_kind)
   {
 ${metakind_constPrinters}
-default: Unhandled() << ::CVC5::expr::NodeValue::dKindToKind(nv->d_kind);
+default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv->d_kind);
   }
 }
 
@@ -136,21 +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(::CVC5::expr::NodeValue* nv)
+void deleteNodeValueConstant(::cvc5::expr::NodeValue* nv)
 {
   Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
 
   switch (nv->d_kind)
   {
 ${metakind_constDeleters}
-default: Unhandled() << ::CVC5::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(::CVC5::Kind k)
+uint32_t getMinArityForKind(::cvc5::Kind k)
 {
   static const unsigned lbs[] = {
     0, /* NULL_EXPR */
@@ -162,7 +162,7 @@ ${metakind_lbchildren}
   return lbs[k];
 }
 
-uint32_t getMaxArityForKind(::CVC5::Kind k)
+uint32_t getMaxArityForKind(::cvc5::Kind k)
 {
   static const unsigned ubs[] = {
     0, /* NULL_EXPR */
@@ -180,7 +180,7 @@ ${metakind_ubchildren}
  * example, since the kind of functions is just VARIABLE, it should map
  * VARIABLE to APPLY_UF.
  */
-Kind operatorToKind(::CVC5::expr::NodeValue* nv)
+Kind operatorToKind(::cvc5::expr::NodeValue* nv)
 {
   if(nv->getKind() == kind::BUILTIN) {
     return nv->getConst<Kind>();
@@ -197,4 +197,4 @@ ${metakind_operatorKinds}
 }
 
 }  // namespace kind
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index ba1b47b4a..5c78d87d3 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -24,7 +24,7 @@
 #include "base/check.h"
 #include "expr/kind.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 namespace expr {
   class NodeValue;
@@ -74,16 +74,16 @@ struct ConstantMapReverse;
  */
 template <Kind k, bool pool>
 struct NodeValueConstCompare {
-  inline static bool compare(const ::CVC5::expr::NodeValue* x,
-                             const ::CVC5::expr::NodeValue* y);
-  inline static size_t constHash(const ::CVC5::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 ::CVC5::expr::NodeValue* nv1,
-                      const ::CVC5::expr::NodeValue* nv2);
-  static size_t constHash(const ::CVC5::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 */
 
 /**
@@ -104,9 +104,9 @@ enum MetaKind_t {
 
 }  // namespace metakind
 
-// import MetaKind into the "CVC5::kind" namespace but keep the
+// import MetaKind into the "cvc5::kind" namespace but keep the
 // individual MetaKind constants under kind::metakind::
-typedef ::CVC5::kind::metakind::MetaKind_t MetaKind;
+typedef ::cvc5::kind::metakind::MetaKind_t MetaKind;
 
 /**
  * Get the metakind for a particular kind.
@@ -119,12 +119,12 @@ namespace expr {
 // Comparison predicate
 struct NodeValuePoolEq {
   inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
-    return ::CVC5::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2);
+    return ::cvc5::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2);
   }
 };
 
 }  // namespace expr
-}  // namespace CVC5
+}  // namespace cvc5
 
 #include "expr/node_value.h"
 
@@ -134,7 +134,7 @@ ${metakind_includes}
 
 #ifdef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
 
-namespace CVC5 {
+namespace cvc5 {
 
 namespace expr {
 ${metakind_getConst_decls}
@@ -145,7 +145,7 @@ namespace metakind {
 
 template <Kind k, bool pool>
 inline bool NodeValueConstCompare<k, pool>::compare(
-    const ::CVC5::expr::NodeValue* x, const ::CVC5::expr::NodeValue* y)
+    const ::cvc5::expr::NodeValue* x, const ::cvc5::expr::NodeValue* y)
 {
   typedef typename ConstantMapReverse<k>::T T;
   if(pool) {
@@ -165,7 +165,7 @@ inline bool NodeValueConstCompare<k, pool>::compare(
 
 template <Kind k, bool pool>
 inline size_t NodeValueConstCompare<k, pool>::constHash(
-    const ::CVC5::expr::NodeValue* nv)
+    const ::cvc5::expr::NodeValue* nv)
 {
   typedef typename ConstantMapReverse<k>::T T;
   return nv->getConst<T>().hash();
@@ -174,7 +174,7 @@ inline size_t NodeValueConstCompare<k, pool>::constHash(
 ${metakind_constantMaps_decls}
 
 struct NodeValueConstPrinter {
-  static void toStream(std::ostream& out, const ::CVC5::expr::NodeValue* nv);
+  static void toStream(std::ostream& out, const ::cvc5::expr::NodeValue* nv);
   static void toStream(std::ostream& out, TNode n);
 };
 
@@ -187,12 +187,12 @@ struct NodeValueConstPrinter {
  * This doesn't support "non-inlined" NodeValues, which shouldn't need this
  * kind of cleanup.
  */
-void deleteNodeValueConstant(::CVC5::expr::NodeValue* nv);
+void deleteNodeValueConstant(::cvc5::expr::NodeValue* nv);
 
 /** Return the minimum arity of the given kind. */
-uint32_t getMinArityForKind(::CVC5::Kind k);
+uint32_t getMinArityForKind(::cvc5::Kind k);
 /** Return the maximum arity of the given kind. */
-uint32_t getMaxArityForKind(::CVC5::Kind k);
+uint32_t getMaxArityForKind(::cvc5::Kind k);
 
 }  // namespace metakind
 
@@ -201,10 +201,10 @@ uint32_t getMaxArityForKind(::CVC5::Kind k);
  * example, since the kind of functions is just VARIABLE, it should map
  * VARIABLE to APPLY_UF.
  */
-Kind operatorToKind(::CVC5::expr::NodeValue* nv);
+Kind operatorToKind(::cvc5::expr::NodeValue* nv);
 
 }  // namespace kind
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index cc5162fef..c5ff67a43 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., ::CVC5::theory::foo)" >&2
-  elif ! expr "$2" : '\(::CVC5::theory::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class not under ::CVC5::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() == ::CVC5::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 3b987746a..289789a9e 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., ::CVC5::theory::foo)" >&2
-  elif ! expr "$2" : '\(::CVC5::theory::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class not under ::CVC5::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 b88a70c71..7c0d110fb 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., ::CVC5::theory::foo)" >&2
-  elif ! expr "$2" : '\(::CVC5::theory::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class not under ::CVC5::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., ::CVC5::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., ::CVC5::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 = ::CVC5::kind::$1 };
+  enum { kind = ::cvc5::kind::$1 };
 };/* ConstantMap< $2 > */
 
 template <>
-struct ConstantMapReverse< ::CVC5::kind::$1 > {
+struct ConstantMapReverse< ::cvc5::kind::$1 > {
   typedef $2 T;
-};/* ConstantMapReverse< ::CVC5::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< ::CVC5::kind::$1 > {
 
 template <>
 $2 const& NodeValue::getConst< $2 >() const {
-  AssertArgument(getKind() == ::CVC5::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 fa2a8860c..90d29f1eb 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -26,7 +26,7 @@
 
 using namespace std;
 
-namespace CVC5 {
+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;
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/node.h b/src/expr/node.h
index 291c2e538..29bfaa157 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -41,7 +41,7 @@
 #include "util/hash.h"
 #include "util/utility.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class TypeNode;
 class NodeManager;
@@ -199,10 +199,10 @@ class NodeTemplate {
   template <unsigned nchild_thresh>
   friend class NodeBuilder;
 
-  friend class ::CVC5::expr::attr::AttributeManager;
-  friend struct ::CVC5::expr::attr::SmtAttributes;
+  friend class ::cvc5::expr::attr::AttributeManager;
+  friend struct ::cvc5::expr::attr::SmtAttributes;
 
-  friend struct ::CVC5::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;
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 //#include "expr/attribute.h"
 #include "expr/node_manager.h"
 
-namespace CVC5 {
+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 CVC5::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 CVC5::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 CVC5::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 CVC5::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 CVC5::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 CVC5::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 */
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__NODE_H */
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 318b7c85b..bcf74a944 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 CVC5 {
+namespace cvc5 {
 namespace expr {
 
 bool hasSubterm(TNode n, TNode t, bool strict)
@@ -764,4 +764,4 @@ bool match(Node x,
 }
 
 }  // namespace expr
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index ca1ee2e39..7ae56e5ba 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 CVC5 {
+namespace cvc5 {
 namespace expr {
 
 /**
@@ -235,6 +235,6 @@ bool match(Node n1,
            std::unordered_map<Node, Node, NodeHashFunction>& subs);
 
 }  // namespace expr
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 724e03451..eaf5b040d 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -160,14 +160,14 @@
 #include <memory>
 #include <vector>
 
-namespace CVC5 {
+namespace cvc5 {
 static const unsigned default_nchild_thresh = 10;
 
 template <unsigned nchild_thresh>
 class NodeBuilder;
 
 class NodeManager;
-}  // namespace CVC5
+}  // namespace cvc5
 
 #include "base/check.h"
 #include "base/output.h"
@@ -175,7 +175,7 @@ class NodeManager;
 #include "expr/metakind.h"
 #include "expr/node_value.h"
 
-namespace CVC5 {
+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<> */
 
-}  // namespace CVC5
+}  // 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 CVC5 {
+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;
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__NODE_BUILDER_H */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 370f0fb4c..6d2d150f5 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 CVC5::expr;
+using namespace cvc5::expr;
 
-namespace CVC5 {
+namespace cvc5 {
 
 thread_local NodeManager* NodeManager::s_current = NULL;
 
@@ -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. CVC5::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
-        // CVC5::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;
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index aeea179d4..857bcc25f 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 CVC5 {
+namespace cvc5 {
 
 namespace api {
 class Solver;
@@ -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<CVC5::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<CVC5::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
 }
 
-}  // namespace CVC5
+}  // 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 CVC5 {
+namespace cvc5 {
 
 // general expression-builders
 
@@ -1577,6 +1577,6 @@ NodeClass NodeManager::mkConstInternal(const T& val) {
   return NodeClass(nv);
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__NODE_MANAGER_H */
diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h
index b7f6319eb..c88df3cee 100644
--- a/src/expr/node_manager_attributes.h
+++ b/src/expr/node_manager_attributes.h
@@ -19,7 +19,7 @@
 
 #include "expr/attribute.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace expr {
 
 // Definition of an attribute for the variable name.
@@ -37,4 +37,4 @@ typedef expr::Attribute<expr::attr::TypeTag, TypeNode> TypeAttr;
 typedef expr::Attribute<expr::attr::TypeCheckedTag, bool> TypeCheckedAttr;
 
 }  // namespace expr
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h
index 831eace65..d8558de97 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 CVC5 {
+namespace cvc5 {
 namespace expr {
 
 class NodeSelfIterator : public std::iterator<std::input_iterator_tag, Node> {
@@ -123,6 +123,6 @@ inline bool NodeSelfIterator::operator!=(NodeSelfIterator i) const {
 }
 
 }  // namespace expr
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__NODE_SELF_ITERATOR_H */
diff --git a/src/expr/node_traversal.cpp b/src/expr/node_traversal.cpp
index c7d3ab3f8..01140a806 100644
--- a/src/expr/node_traversal.cpp
+++ b/src/expr/node_traversal.cpp
@@ -16,7 +16,7 @@
 
 #include <functional>
 
-namespace CVC5 {
+namespace cvc5 {
 
 NodeDfsIterator::NodeDfsIterator(TNode n,
                                  VisitOrder order,
@@ -156,4 +156,4 @@ NodeDfsIterator NodeDfsIterable::end() const
   return NodeDfsIterator(d_order);
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h
index 934ec6bd8..015bcec06 100644
--- a/src/expr/node_traversal.h
+++ b/src/expr/node_traversal.h
@@ -23,7 +23,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
 
 #endif  // CVC4__EXPR__NODE_TRAVERSAL_H
diff --git a/src/expr/node_trie.cpp b/src/expr/node_trie.cpp
index 195011c1f..5af1cef01 100644
--- a/src/expr/node_trie.cpp
+++ b/src/expr/node_trie.cpp
@@ -14,7 +14,7 @@
 
 #include "expr/node_trie.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/node_trie.h b/src/expr/node_trie.h
index f765105d3..2f42b6a52 100644
--- a/src/expr/node_trie.h
+++ b/src/expr/node_trie.h
@@ -20,7 +20,7 @@
 #include <map>
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 /** NodeTemplate trie class
@@ -107,6 +107,6 @@ typedef NodeTemplateTrie<true> NodeTrie;
 typedef NodeTemplateTrie<false> TNodeTrie;
 
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__NODE_TRIE_H */
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 027c15a0a..7b3e413f7 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -31,7 +31,7 @@
 
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace expr {
 
 string NodeValue::toString() const {
@@ -95,4 +95,4 @@ NodeValue::iterator<NodeTemplate<false> > operator+(
 }
 
 }  // namespace expr
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index ecc054a75..3815ea5be 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 CVC5 {
+namespace cvc5 {
 
 template <bool ref_count> class NodeTemplate;
 class TypeNode;
@@ -45,13 +45,13 @@ namespace expr {
 
 namespace kind {
   namespace metakind {
-  template < ::CVC5::Kind k, bool pool>
+  template < ::cvc5::Kind k, bool pool>
   struct NodeValueConstCompare;
 
   struct NodeValueCompare;
   struct NodeValueConstPrinter;
 
-  void deleteNodeValueConstant(::CVC5::expr::NodeValue* nv);
+  void deleteNodeValueConstant(::cvc5::expr::NodeValue* nv);
   }  // namespace metakind
   }  // namespace kind
 
@@ -63,19 +63,19 @@ namespace expr {
 class NodeValue
 {
   template <bool>
-  friend class ::CVC5::NodeTemplate;
-  friend class ::CVC5::TypeNode;
+  friend class ::cvc5::NodeTemplate;
+  friend class ::cvc5::TypeNode;
   template <unsigned nchild_thresh>
-  friend class ::CVC5::NodeBuilder;
-  friend class ::CVC5::NodeManager;
+  friend class ::cvc5::NodeBuilder;
+  friend class ::cvc5::NodeManager;
 
   template <Kind k, bool pool>
-  friend struct ::CVC5::kind::metakind::NodeValueConstCompare;
+  friend struct ::cvc5::kind::metakind::NodeValueConstCompare;
 
-  friend struct ::CVC5::kind::metakind::NodeValueCompare;
-  friend struct ::CVC5::kind::metakind::NodeValueConstPrinter;
+  friend struct ::cvc5::kind::metakind::NodeValueCompare;
+  friend struct ::cvc5::kind::metakind::NodeValueConstPrinter;
 
-  friend void ::CVC5::kind::metakind::deleteNodeValueConstant(NodeValue* nv);
+  friend void ::cvc5::kind::metakind::deleteNodeValueConstant(NodeValue* nv);
 
   friend class RefCountGuard;
 
@@ -396,11 +396,11 @@ struct NodeValueIDEquality {
 inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
 
 }  // namespace expr
-}  // namespace CVC5
+}  // namespace cvc5
 
 #include "expr/node_manager.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace expr {
 
 inline NodeValue::NodeValue(int) :
@@ -497,11 +497,11 @@ inline NodeValue* NodeValue::getChild(int i) const {
 }
 
 }  // namespace expr
-}  // namespace CVC5
+}  // namespace cvc5
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace expr {
 
 template <typename T>
@@ -545,6 +545,6 @@ static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue*
 }
 #endif /* CVC4_DEBUG */
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__NODE_VALUE_H */
diff --git a/src/expr/node_visitor.h b/src/expr/node_visitor.h
index a3e24772a..9816e37e8 100644
--- a/src/expr/node_visitor.h
+++ b/src/expr/node_visitor.h
@@ -22,7 +22,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+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;
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
index a55b3c69a..c0ba27a64 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 CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/proof.h b/src/expr/proof.h
index 164880cea..af859df93 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 CVC5 {
+namespace cvc5 {
 
 class ProofNode;
 class ProofNodeManager;
@@ -273,6 +273,6 @@ class CDProof : public ProofGenerator
   void notifyNewProof(Node expected);
 };
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__PROOF_MANAGER_H */
diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp
index b5955e991..ca1b96f1e 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 CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 
 Node ProofRuleChecker::check(PfRule id,
                              const std::vector<Node>& children,
@@ -347,4 +347,4 @@ bool ProofChecker::isPedanticFailure(PfRule id,
   return false;
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
index edb0fec3a..99f9f3ec8 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 CVC5 {
+namespace cvc5 {
 
 class ProofChecker;
 class ProofNode;
@@ -202,6 +202,6 @@ class ProofChecker
                      bool enableOutput);
 };
 
-}  // namespace CVC5
+}  // 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 487c52bc6..6947cfd44 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 CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h
index 40143f814..d610147d4 100644
--- a/src/expr/proof_ensure_closed.h
+++ b/src/expr/proof_ensure_closed.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__PROOF_ENSURE_CLOSED_H */
diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
index 102435cea..a315ba2cd 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 CVC5 {
+namespace cvc5 {
 
 std::ostream& operator<<(std::ostream& out, CDPOverwrite opol)
 {
@@ -73,4 +73,4 @@ bool ProofGenerator::addProofTo(Node f,
   return false;
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h
index 446cb2c83..76a2c9b3b 100644
--- a/src/expr/proof_generator.h
+++ b/src/expr/proof_generator.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class CDProof;
 class ProofNode;
@@ -107,6 +107,6 @@ class ProofGenerator
   virtual std::string identify() const = 0;
 };
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__PROOF_GENERATOR_H */
diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp
index 923bdeacd..f7ad65844 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 CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h
index 67600e2d0..13c7f2878 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 CVC5 {
+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 CVC5
+}  // 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 142a9b37f..f307b78b9 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 CVC5 {
+namespace cvc5 {
 namespace expr {
 
 void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump)
@@ -172,4 +172,4 @@ bool containsSubproof(ProofNode* pn,
 }
 
 }  // namespace expr
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h
index 9266c7251..01faa8a40 100644
--- a/src/expr/proof_node_algorithm.h
+++ b/src/expr/proof_node_algorithm.h
@@ -21,7 +21,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class ProofNode;
 
@@ -70,6 +70,6 @@ bool containsSubproof(ProofNode* pn,
                       std::unordered_set<const ProofNode*>& visited);
 
 }  // namespace expr
-}  // namespace CVC5
+}  // 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 ceb9d4eac..036c50947 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 CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 
 ProofNodeManager::ProofNodeManager(ProofChecker* pc)
     : d_checker(pc)
@@ -356,4 +356,4 @@ bool ProofNodeManager::updateNodeInternal(
   return true;
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index 8e019818d..54d398545 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 CVC5 {
+namespace cvc5 {
 
 class ProofChecker;
 class ProofNode;
@@ -192,6 +192,6 @@ class ProofNodeManager
       bool needsCheck);
 };
 
-}  // namespace CVC5
+}  // 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 7468ecb5a..b53ce368d 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 CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 
 ProofNodeToSExpr::ProofNodeToSExpr()
 {
@@ -144,4 +144,4 @@ Node ProofNodeToSExpr::getOrMkNodeVariable(Node n)
   return var;
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h
index 8da094da2..bbbde39f6 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 CVC5 {
+namespace cvc5 {
 
 class ProofNode;
 
@@ -64,6 +64,6 @@ class ProofNodeToSExpr
   Node getOrMkNodeVariable(Node n);
 };
 
-}  // namespace CVC5
+}  // 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 4c1883e93..933e5b999 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 CVC5 {
+namespace cvc5 {
 
 ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {}
 ProofNodeUpdaterCallback::~ProofNodeUpdaterCallback() {}
@@ -261,4 +261,4 @@ void ProofNodeUpdater::setDebugFreeAssumptions(
   d_debugFreeAssumps = true;
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h
index 5a22af61a..8e30f14d2 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 CVC5 {
+namespace cvc5 {
 
 class CDProof;
 class ProofNode;
@@ -155,6 +155,6 @@ class ProofNodeUpdater
   bool d_autoSym;
 };
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 1323520c3..8141a017c 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -16,7 +16,7 @@
 
 #include <iostream>
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 95f97ae44..7e0fc31fe 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -19,7 +19,7 @@
 
 #include <iosfwd>
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__PROOF_RULE_H */
diff --git a/src/expr/proof_set.h b/src/expr/proof_set.h
index ccfac350a..0509ed9d4 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 CVC5 {
+namespace cvc5 {
 
 /**
  * A (context-dependent) set of proofs, which is used for memory
@@ -70,6 +70,6 @@ class CDProofSet
   std::string d_namePrefix;
 };
 
-}  // namespace CVC5
+}  // 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 23f0f5997..4ecee9130 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 CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h
index b78d1d605..99a7608ff 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 CVC5 {
+namespace cvc5 {
 
 class ProofChecker;
 
@@ -92,6 +92,6 @@ class ProofStepBuffer
   std::vector<std::pair<Node, ProofStep>> d_steps;
 };
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__PROOF_STEP_BUFFER_H */
diff --git a/src/expr/record.cpp b/src/expr/record.cpp
index affd2615c..367315d84 100644
--- a/src/expr/record.cpp
+++ b/src/expr/record.cpp
@@ -19,10 +19,10 @@
 #include "base/check.h"
 #include "base/output.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) {
   return out << "[" << t.getField() << "]";
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/record.h b/src/expr/record.h
index d4b41b9b9..436b5b269 100644
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -25,13 +25,13 @@
 #include <utility>
 
 // Forward Declarations
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
 
-namespace CVC5 {
+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>>;
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__RECORD_H */
diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp
index 90b57f58d..df40c8534 100644
--- a/src/expr/sequence.cpp
+++ b/src/expr/sequence.cpp
@@ -22,7 +22,7 @@
 
 using namespace std;
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/sequence.h b/src/expr/sequence.h
index 461adb667..e42851f58 100644
--- a/src/expr/sequence.h
+++ b/src/expr/sequence.h
@@ -20,7 +20,7 @@
 #include <memory>
 #include <vector>
 
-namespace CVC5 {
+namespace cvc5 {
 
 template <bool ref_count>
 class NodeTemplate;
@@ -36,7 +36,7 @@ class Sequence
  public:
   /** constructors for Sequence
    *
-   * Internally, a CVC5::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 CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__SEQUENCE_H */
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index 2b04c0755..31c0b55cd 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 CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 1078bc11f..9955c0e15 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -21,7 +21,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class ProofGenerator;
 
@@ -234,6 +234,6 @@ class SkolemManager
                  int flags = NodeManager::SKOLEM_DEFAULT);
 };
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__PROOF_SKOLEM_CACHE_H */
diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp
index 897c6fdba..c2138499b 100644
--- a/src/expr/subs.cpp
+++ b/src/expr/subs.cpp
@@ -18,7 +18,7 @@
 
 #include "theory/rewriter.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/subs.h b/src/expr/subs.h
index c2854bf36..fdb8e4551 100644
--- a/src/expr/subs.h
+++ b/src/expr/subs.h
@@ -19,7 +19,7 @@
 #include <vector>
 #include "expr/node.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__SUBS_H */
diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp
index 352dd157a..929c8a97c 100644
--- a/src/expr/sygus_datatype.cpp
+++ b/src/expr/sygus_datatype.cpp
@@ -16,9 +16,9 @@
 
 #include <sstream>
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h
index f4635bdb3..e5d1de740 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 CVC5 {
+namespace cvc5 {
 
 /** Attribute true for variables that represent any constant */
 struct SygusAnyConstAttributeId
@@ -134,6 +134,6 @@ class SygusDatatype
   DType d_dt;
 };
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp
index 1e99f4a68..9610e443d 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 CVC5::context;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 
 // ---------------------------------------------- SymbolManager::Implementation
 
@@ -367,4 +367,4 @@ void SymbolManager::resetAssertions()
   d_symtabAllocated.resetAssertions();
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h
index 6795ce3b3..0a9248f78 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 CVC5 {
+namespace cvc5 {
 
 /**
  * Symbol manager, which manages:
@@ -156,6 +156,6 @@ class CVC4_EXPORT SymbolManager
   bool d_globalDeclarations;
 };
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__SYMBOL_MANAGER_H */
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 774e2bb39..1c513fea4 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 CVC5 {
+namespace cvc5 {
 
-using ::CVC5::context::CDHashMap;
-using ::CVC5::context::CDHashSet;
-using ::CVC5::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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index 113dea704..fbb1969dd 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 CVC5 {
+namespace cvc5 {
 
 namespace api {
 class Solver;
@@ -210,6 +210,6 @@ class CVC4_EXPORT SymbolTable
   std::unique_ptr<Implementation> d_implementation;
 }; /* class SymbolTable */
 
-}  // namespace CVC5
+}  // 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 9b099de2d..d51e07e83 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 CVC5 {
+namespace cvc5 {
 
 TConvSeqProofGenerator::TConvSeqProofGenerator(
     ProofNodeManager* pnm,
@@ -168,4 +168,4 @@ theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence(
 
 std::string TConvSeqProofGenerator::identify() const { return d_name; }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h
index a5b1de101..151cd511d 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 CVC5 {
+namespace cvc5 {
 
 class ProofNodeManager;
 
@@ -115,6 +115,6 @@ class TConvSeqProofGenerator : public ProofGenerator
   std::string d_name;
 };
 
-}  // namespace CVC5
+}  // 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 97f3c2539..11a992d16 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 CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/term_canonize.h b/src/expr/term_canonize.h
index f9f0fda24..f15bb2df0 100644
--- a/src/expr/term_canonize.h
+++ b/src/expr/term_canonize.h
@@ -20,7 +20,7 @@
 #include <map>
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace expr {
 
 /** TermCanonize
@@ -100,6 +100,6 @@ class TermCanonize
 };
 
 }  // namespace expr
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__EXPR__TERM_CANONIZE_H */
diff --git a/src/expr/term_context.cpp b/src/expr/term_context.cpp
index 56c38a17c..883fa3e08 100644
--- a/src/expr/term_context.cpp
+++ b/src/expr/term_context.cpp
@@ -14,7 +14,7 @@
 
 #include "expr/term_context.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/term_context.h b/src/expr/term_context.h
index 65cdbb23e..062104fc2 100644
--- a/src/expr/term_context.h
+++ b/src/expr/term_context.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+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 CVC5
+}  // 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 1afc599d2..564459d37 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 CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/term_context_node.h b/src/expr/term_context_node.h
index 67d747557..5af435a56 100644
--- a/src/expr/term_context_node.h
+++ b/src/expr/term_context_node.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class TCtxStack;
 class TermContext;
@@ -74,6 +74,6 @@ class TCtxNode
   const TermContext* d_tctx;
 };
 
-}  // namespace CVC5
+}  // 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 557683498..8a0fd91c9 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 CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/src/expr/term_context_stack.h b/src/expr/term_context_stack.h
index 34c474a52..0042091ed 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 CVC5 {
+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 CVC5
+}  // 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 bfdf4d188..df4708f74 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 CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 
 std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol)
 {
@@ -588,4 +588,4 @@ std::string TConvProofGenerator::toStringDebug() const
   return ss.str();
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h
index 734ef103e..e1f2b90e8 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 CVC5 {
+namespace cvc5 {
 
 class ProofNodeManager;
 class TermContext;
@@ -242,6 +242,6 @@ class TConvProofGenerator : public ProofGenerator
   std::string toStringDebug() const;
 };
 
-}  // namespace CVC5
+}  // 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 b502d8013..fee02de75 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 CVC5 {
+namespace cvc5 {
 namespace expr {
 
 class TypeChecker {
@@ -36,6 +36,6 @@ public:
 };/* class TypeChecker */
 
 }  // namespace expr
-}  // namespace CVC5
+}  // 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 07dca77e2..d99d5e82d 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -23,7 +23,7 @@
 
 ${typechecker_includes}
 
-namespace CVC5 {
+namespace cvc5 {
 namespace expr {
 
 TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check)
@@ -72,4 +72,4 @@ ${construles}
 }/* TypeChecker::computeIsConst */
 
 }  // namespace expr
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/type_checker_util.h b/src/expr/type_checker_util.h
index 1ca23d374..207c242b8 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 CVC5 {
+namespace cvc5 {
 namespace expr {
 
 /** Type check returns the builtin operator sort */
@@ -202,4 +202,4 @@ class SimpleTypeRuleVar
 };
 
 }  // namespace expr
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/type_matcher.cpp b/src/expr/type_matcher.cpp
index 76d256157..9389ce4b8 100644
--- a/src/expr/type_matcher.cpp
+++ b/src/expr/type_matcher.cpp
@@ -14,7 +14,7 @@
 
 #include "type_matcher.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 TypeMatcher::TypeMatcher(TypeNode dt)
 {
@@ -125,4 +125,4 @@ void TypeMatcher::getMatches(std::vector<TypeNode>& types) const
   }
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/type_matcher.h b/src/expr/type_matcher.h
index 651054313..a75bb7b8b 100644
--- a/src/expr/type_matcher.h
+++ b/src/expr/type_matcher.h
@@ -21,7 +21,7 @@
 
 #include "expr/type_node.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__MATCHER_H */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index f73bde3eb..cbade1220 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -25,7 +25,7 @@
 
 using namespace std;
 
-namespace CVC5 {
+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 CVC5::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];
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 7b752c3e5..98515be2a 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -32,7 +32,7 @@
 #include "expr/metakind.h"
 #include "util/cardinality.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class NodeManager;
 class DType;
@@ -749,11 +749,11 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
 
 typedef TypeNode::HashFunction TypeNodeHashFunction;
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #include "expr/node_manager.h"
 
-namespace CVC5 {
+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 CVC5::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 CVC5::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 CVC5::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 CVC5::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 */
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__NODE_H */
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
index abf5e6173..ce2696c5b 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -29,7 +29,7 @@
 
 ${type_properties_includes}
 
-namespace CVC5 {
+namespace cvc5 {
 namespace kind {
 
 /**
@@ -114,6 +114,6 @@ ${type_groundterms}
 } /* mkGroundTerm(TypeNode) */
 
 }  // namespace kind
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__TYPE_PROPERTIES_H */
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
index 9d8b12264..bd934e391 100644
--- a/src/expr/uninterpreted_constant.cpp
+++ b/src/expr/uninterpreted_constant.cpp
@@ -26,7 +26,7 @@
 
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 
 UninterpretedConstant::UninterpretedConstant(const TypeNode& type,
                                              Integer index)
@@ -95,4 +95,4 @@ size_t UninterpretedConstantHashFunction::operator()(
          * IntegerHashFunction()(uc.getIndex());
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h
index 00ad68212..94d7f85ed 100644
--- a/src/expr/uninterpreted_constant.h
+++ b/src/expr/uninterpreted_constant.h
@@ -24,7 +24,7 @@
 
 #include "util/integer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class TypeNode;
 
@@ -60,6 +60,6 @@ struct UninterpretedConstantHashFunction
   size_t operator()(const UninterpretedConstant& uc) const;
 }; /* struct UninterpretedConstantHashFunction */
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__UNINTERPRETED_CONSTANT_H */
author	Aina Niemetz <aina.niemetz@gmail.com>	2021-04-01 09:56:14 -0700
committer	GitHub <noreply@github.com>	2021-04-01 16:56:14 +0000
commit	05a53a2ac405bcd18a84024247145f161809c3b0 (patch)
tree	34241c0a82f79d717ddbfbb0c294f9a09c7edb0c /src/expr
parent	afaf4413775ff7d6054a5893f1397ad908e0773c (diff)