From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 30 Mar 2022 22:16:46 +0000 (-0700)
Subject: Move cvc5::internal::context to cvc5::context. (#8451)
X-Git-Tag: cvc5-1.0.0~115
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=014ff8cdd6294f4b1375888c11dc8a1f3a5de0d4;p=cvc5.git

Move cvc5::internal::context to cvc5::context. (#8451)
---

diff --git a/src/base/check.h b/src/base/check.h
index be645f6fe..d8bdfa690 100644
--- a/src/base/check.h
+++ b/src/base/check.h
@@ -171,32 +171,33 @@ class AssertArgumentException : public Exception
 
 #define InternalError() CVC5_FATAL() << "Internal error detected "
 
-#define IllegalArgument(arg, msg...)      \
-  throw ::cvc5::internal::IllegalArgumentException( \
-      "",                                 \
-      #arg,                               \
-      __PRETTY_FUNCTION__,                \
-      ::cvc5::internal::IllegalArgumentException::formatVariadic(msg).c_str());
+#define IllegalArgument(arg, msg...)              \
+  throw cvc5::internal::IllegalArgumentException( \
+      "",                                         \
+      #arg,                                       \
+      __PRETTY_FUNCTION__,                        \
+      cvc5::internal::IllegalArgumentException::formatVariadic(msg).c_str());
 // This cannot use check argument directly as this forces
 // CheckArgument to use a va_list. This is unsupported in Swig.
-#define PrettyCheckArgument(cond, arg, msg...)                            \
-  do                                                                      \
-  {                                                                       \
-    if (__builtin_expect((!(cond)), false))                               \
-    {                                                                     \
-      throw ::cvc5::internal::IllegalArgumentException(                             \
-          #cond,                                                          \
-          #arg,                                                           \
-          __PRETTY_FUNCTION__,                                            \
-          ::cvc5::internal::IllegalArgumentException::formatVariadic(msg).c_str()); \
-    }                                                                     \
+#define PrettyCheckArgument(cond, arg, msg...)                          \
+  do                                                                    \
+  {                                                                     \
+    if (__builtin_expect((!(cond)), false))                             \
+    {                                                                   \
+      throw cvc5::internal::IllegalArgumentException(                   \
+          #cond,                                                        \
+          #arg,                                                         \
+          __PRETTY_FUNCTION__,                                          \
+          cvc5::internal::IllegalArgumentException::formatVariadic(msg) \
+              .c_str());                                                \
+    }                                                                   \
   } while (0)
 #define AlwaysAssertArgument(cond, arg, msg...)                         \
   do                                                                    \
   {                                                                     \
     if (__builtin_expect((!(cond)), false))                             \
     {                                                                   \
-      throw ::cvc5::internal::AssertArgumentException(                            \
+      throw cvc5::internal::AssertArgumentException(                    \
           #cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ##msg); \
     }                                                                   \
   } while (0)
diff --git a/src/base/exception.h b/src/base/exception.h
index 9d5ca7c1a..4cc3b3268 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -124,7 +124,7 @@ inline void CheckArgument(bool cond,
                           const char* tail CVC5_UNUSED)
 {
   if(__builtin_expect( ( !cond ), false )) {
-    throw ::cvc5::internal::IllegalArgumentException("", "", tail);
+    throw cvc5::internal::IllegalArgumentException("", "", tail);
   }
 }
 template <class T>
@@ -133,7 +133,7 @@ template <class T>
 inline void CheckArgument(bool cond, const T& arg CVC5_UNUSED)
 {
   if(__builtin_expect( ( !cond ), false )) {
-    throw ::cvc5::internal::IllegalArgumentException("", "", "");
+    throw cvc5::internal::IllegalArgumentException("", "", "");
   }
 }
 
diff --git a/src/base/map_util.h b/src/base/map_util.h
index e23c671b2..12ce241cf 100644
--- a/src/base/map_util.h
+++ b/src/base/map_util.h
@@ -16,8 +16,8 @@
  * Supports:
  * - std::map
  * - std::unordered_map
- * - cvc5::internal::context::CDHashmap
- * - cvc5::internal::context::CDInsertHashmap
+ * - context::CDHashmap
+ * - context::CDInsertHashmap
  * The ContainsKey function is also compatible with std::[unordered_]set.
  *
  * Currently implemented classes of functions:
diff --git a/src/base/output.h b/src/base/output.h
index 4f57ed450..0040ca65e 100644
--- a/src/base/output.h
+++ b/src/base/output.h
@@ -279,28 +279,39 @@ extern TraceC TraceChannel CVC5_EXPORT;
 
 #ifdef CVC5_MUZZLE
 
-#define Warning \
-  ::cvc5::internal::__cvc5_true() ? ::cvc5::internal::nullStream : ::cvc5::internal::WarningChannel
-#define WarningOnce \
-  ::cvc5::internal::__cvc5_true() ? ::cvc5::internal::nullStream : ::cvc5::internal::WarningChannel
-#define TraceIsOn ::cvc5::internal::__cvc5_true() ? false : ::cvc5::internal::TraceChannel.isOn
-#define Trace(tag) ::cvc5::internal::__cvc5_true() ? ::cvc5::internal::nullStream : ::cvc5::internal::TraceChannel()
+#define Warning                                              \
+  cvc5::internal::__cvc5_true() ? cvc5::internal::nullStream \
+                                : cvc5::internal::WarningChannel
+#define WarningOnce                                          \
+  cvc5::internal::__cvc5_true() ? cvc5::internal::nullStream \
+                                : cvc5::internal::WarningChannel
+#define TraceIsOn \
+  cvc5::internal::__cvc5_true() ? false : cvc5::internal::TraceChannel.isOn
+#define Trace(tag)                                           \
+  cvc5::internal::__cvc5_true() ? cvc5::internal::nullStream \
+                                : cvc5::internal::TraceChannel()
 
 #else /* CVC5_MUZZLE */
 
-#define Warning \
-  (!::cvc5::internal::WarningChannel.isOn()) ? ::cvc5::internal::nullStream : ::cvc5::internal::WarningChannel
-#define WarningOnce                                         \
-  (!::cvc5::internal::WarningChannel.isOn()                           \
-   || !::cvc5::internal::WarningChannel.warnOnce(__FILE__, __LINE__)) \
-      ? ::cvc5::internal::nullStream                                  \
-      : ::cvc5::internal::WarningChannel
+#define Warning                                                         \
+  (!cvc5::internal::WarningChannel.isOn()) ? cvc5::internal::nullStream \
+                                           : cvc5::internal::WarningChannel
+#define WarningOnce                                                 \
+  (!cvc5::internal::WarningChannel.isOn()                           \
+   || !cvc5::internal::WarningChannel.warnOnce(__FILE__, __LINE__)) \
+      ? cvc5::internal::nullStream                                  \
+      : cvc5::internal::WarningChannel
 #ifdef CVC5_TRACING
-#define TraceIsOn ::cvc5::internal::TraceChannel.isOn
-#define Trace(tag) !::cvc5::internal::TraceChannel.isOn(tag) ? ::cvc5::internal::nullStream : ::cvc5::internal::TraceChannel()
+#define TraceIsOn cvc5::internal::TraceChannel.isOn
+#define Trace(tag)                                                     \
+  !cvc5::internal::TraceChannel.isOn(tag) ? cvc5::internal::nullStream \
+                                          : cvc5::internal::TraceChannel()
 #else /* CVC5_TRACING */
-#define TraceIsOn ::cvc5::internal::__cvc5_true() ? false : ::cvc5::internal::TraceChannel.isOn
-#define Trace(tag) ::cvc5::internal::__cvc5_true() ? ::cvc5::internal::nullStream : ::cvc5::internal::TraceChannel()
+#define TraceIsOn \
+  cvc5::internal::__cvc5_true() ? false : cvc5::internal::TraceChannel.isOn
+#define Trace(tag)                                           \
+  cvc5::internal::__cvc5_true() ? cvc5::internal::nullStream \
+                                : cvc5::internal::TraceChannel()
 #endif /* CVC5_TRACING */
 
 #endif /* CVC5_MUZZLE */
diff --git a/src/base/versioninfo.cpp.in b/src/base/versioninfo.cpp.in
index dd8a2ac67..e84704b87 100644
--- a/src/base/versioninfo.cpp.in
+++ b/src/base/versioninfo.cpp.in
@@ -15,8 +15,8 @@
 
 #include "base/configuration.h"
 
-const bool ::cvc5::internal::Configuration::GIT_BUILD = @GIT_BUILD@;
-const bool ::cvc5::internal::Configuration::CVC5_IS_RELEASE = @CVC5_IS_RELEASE@;
-const char* const ::cvc5::internal::Configuration::CVC5_VERSION = "@CVC5_VERSION@";
-const char* const ::cvc5::internal::Configuration::CVC5_FULL_VERSION = "@CVC5_FULL_VERSION@";
-const char* const ::cvc5::internal::Configuration::CVC5_GIT_INFO = "@CVC5_GIT_INFO@";
+const bool cvc5::internal::Configuration::GIT_BUILD = @GIT_BUILD@;
+const bool cvc5::internal::Configuration::CVC5_IS_RELEASE = @CVC5_IS_RELEASE@;
+const char* const cvc5::internal::Configuration::CVC5_VERSION = "@CVC5_VERSION@";
+const char* const cvc5::internal::Configuration::CVC5_FULL_VERSION = "@CVC5_FULL_VERSION@";
+const char* const cvc5::internal::Configuration::CVC5_GIT_INFO = "@CVC5_GIT_INFO@";
diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 6a7f37896..553f1a6b4 100644
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -91,8 +91,7 @@
 #include "context/cdhashmap_forward.h"
 #include "context/context.h"
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 
 // Auxiliary class: almost the same as CDO (see cdo.h)
 
@@ -407,7 +406,6 @@ class CDHashMap : public ContextObj
 
 }; /* class CDHashMap<> */
 
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
 
 #endif /* CVC5__CONTEXT__CDHASHMAP_H */
diff --git a/src/context/cdhashmap_forward.h b/src/context/cdhashmap_forward.h
index a23180d4a..c48fe1a0f 100644
--- a/src/context/cdhashmap_forward.h
+++ b/src/context/cdhashmap_forward.h
@@ -28,12 +28,10 @@
 
 /// \cond internals
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 template <class Key, class Data, class HashFcn = std::hash<Key> >
 class CDHashMap;
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
 
 /// \endcond
 
diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h
index 789532c53..b84bae102 100644
--- a/src/context/cdhashset.h
+++ b/src/context/cdhashset.h
@@ -22,8 +22,7 @@
 #include "context/cdinsert_hashmap.h"
 #include "context/context.h"
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 
 template <class V, class HashFcn = std::hash<V>>
 class CDHashSet : protected CDInsertHashMap<V, bool, HashFcn>
@@ -151,7 +150,6 @@ public:
 
 }; /* class CDHashSet */
 
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
 
 #endif /* CVC5__CONTEXT__CDHASHSET_H */
diff --git a/src/context/cdhashset_forward.h b/src/context/cdhashset_forward.h
index 4e5068eb2..4f8b5e791 100644
--- a/src/context/cdhashset_forward.h
+++ b/src/context/cdhashset_forward.h
@@ -27,11 +27,9 @@
 
 #include <functional>
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 template <class V, class HashFcn = std::hash<V> >
 class CDHashSet;
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
 
 #endif /* CVC5__CONTEXT__CDSET_FORWARD_H */
diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h
index 308ca6de6..316a9fa5e 100644
--- a/src/context/cdinsert_hashmap.h
+++ b/src/context/cdinsert_hashmap.h
@@ -44,9 +44,7 @@
 
 #pragma once
 
-namespace cvc5::internal {
-namespace context {
-
+namespace cvc5::context {
 
 template <class Key, class Data, class HashFcn = std::hash<Key> >
 class InsertHashMap {
@@ -349,7 +347,8 @@ public:
 };/* class CDInsertHashMap<> */
 
 template <class Data, class HashFcn>
-class CDInsertHashMap<TNode, Data, HashFcn> : public ContextObj {
+class CDInsertHashMap<internal::TNode, Data, HashFcn> : public ContextObj
+{
   /* CDInsertHashMap is challenging to get working with TNode.
    * Consider using CDHashMap<TNode,...> instead.
    *
@@ -365,5 +364,4 @@ class CDInsertHashMap<TNode, Data, HashFcn> : public ContextObj {
                 "Cannot create a CDInsertHashMap with TNode keys");
 };
 
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
diff --git a/src/context/cdinsert_hashmap_forward.h b/src/context/cdinsert_hashmap_forward.h
index 3cf1b8698..124a6ecc8 100644
--- a/src/context/cdinsert_hashmap_forward.h
+++ b/src/context/cdinsert_hashmap_forward.h
@@ -28,11 +28,9 @@
 
 #include <functional>
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 template <class Key, class Data, class HashFcn = std::hash<Key> >
 class CDInsertHashMap;
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
 
 #endif /* CVC5__CONTEXT__CDINSERT_HASHMAP_FORWARD_H */
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index faed937ca..62794c7d6 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -30,8 +30,7 @@
 #include "context/context.h"
 #include "context/context_mm.h"
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 
 /**
  * Generic context-dependent dynamic array.  Note that for efficiency,
@@ -437,7 +436,6 @@ class CDList<T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj {
                 "Cannot create a CDList with a ContextMemoryAllocator.");
 };
 
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
 
 #endif /* CVC5__CONTEXT__CDLIST_H */
diff --git a/src/context/cdlist_forward.h b/src/context/cdlist_forward.h
index 685211e28..7e7a0b746 100644
--- a/src/context/cdlist_forward.h
+++ b/src/context/cdlist_forward.h
@@ -35,8 +35,7 @@
 
 /// \cond internals
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 
 template <class T>
 class DefaultCleanUp {
@@ -49,7 +48,6 @@ class CDList;
 
 /// \endcond
 
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
 
 #endif /* CVC5__CONTEXT__CDLIST_FORWARD_H */
diff --git a/src/context/cdmaybe.h b/src/context/cdmaybe.h
index 993bf6bd7..fb7c89001 100644
--- a/src/context/cdmaybe.h
+++ b/src/context/cdmaybe.h
@@ -24,8 +24,7 @@
 #include "context/cdo.h"
 #include "context/context.h"
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 
 class CDRaised {
 private:
@@ -73,5 +72,4 @@ public:
   }
 };/* class CDMaybe<T> */
 
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
diff --git a/src/context/cdo.h b/src/context/cdo.h
index f7fd4f763..cfc8c8a40 100644
--- a/src/context/cdo.h
+++ b/src/context/cdo.h
@@ -20,8 +20,7 @@
 
 #include "context/context.h"
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 
 /**
  * Most basic template for context-dependent objects.  Simply makes a copy
@@ -169,7 +168,6 @@ public:
 
 };/* class CDO */
 
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
 
 #endif /* CVC5__CONTEXT__CDO_H */
diff --git a/src/context/cdqueue.h b/src/context/cdqueue.h
index 6472fd5ca..7f380c03d 100644
--- a/src/context/cdqueue.h
+++ b/src/context/cdqueue.h
@@ -28,8 +28,7 @@
 #include "context/context.h"
 #include "context/cdlist.h"
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 
 template <class T, class CleanUp = DefaultCleanUp<T>, class Allocator = std::allocator<T> >
 class CDQueue;
@@ -155,7 +154,6 @@ public:
 
 };/* class CDQueue<> */
 
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
 
 #endif /* CVC5__CONTEXT__CDQUEUE_H */
diff --git a/src/context/cdtrail_queue.h b/src/context/cdtrail_queue.h
index bfb5f2a4f..a6427f9dd 100644
--- a/src/context/cdtrail_queue.h
+++ b/src/context/cdtrail_queue.h
@@ -25,8 +25,7 @@
 #include "context/cdlist.h"
 #include "context/cdo.h"
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 
 class Context;
 
@@ -89,7 +88,6 @@ public:
 
 };/* class CDTrailQueue<> */
 
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
 
 #endif /* CVC5__CONTEXT__CDTRAIL_QUEUE_H */
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 7a5d88252..129a4f961 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -20,9 +20,7 @@
 #include "base/check.h"
 #include "context/context.h"
 
-namespace cvc5::internal {
-namespace context {
-
+namespace cvc5::context {
 
 Context::Context() : d_pCNOpre(NULL), d_pCNOpost(NULL) {
   // Create new memory manager
@@ -347,5 +345,4 @@ void Scope::enqueueToGarbageCollect(ContextObj* obj) {
   d_garbage.push_back(obj);
 }
 
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
diff --git a/src/context/context.h b/src/context/context.h
index 1b73531f1..c227d97ea 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -28,8 +28,7 @@
 #include "base/output.h"
 #include "context/context_mm.h"
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 
 class Context;
 class Scope;
@@ -735,7 +734,6 @@ inline void Scope::addToChain(ContextObj* pContextObj)
   d_pContextObjList = pContextObj;
 }
 
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
 
 #endif /* CVC5__CONTEXT__CONTEXT_H */
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index 55660edb1..01fd23010 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -28,8 +28,7 @@
 #include "base/output.h"
 #include "context/context_mm.h"
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 
 #ifndef CVC5_DEBUG_CONTEXT_MEMORY_MANAGER
 
@@ -173,5 +172,4 @@ unsigned ContextMemoryManager::getMaxAllocationSize()
 
 #endif /* CVC5_DEBUG_CONTEXT_MEMORY_MANAGER */
 
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
diff --git a/src/context/context_mm.h b/src/context/context_mm.h
index 0fdb78045..742aab846 100644
--- a/src/context/context_mm.h
+++ b/src/context/context_mm.h
@@ -25,8 +25,7 @@
 #endif
 #include <vector>
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 
 #ifndef CVC5_DEBUG_CONTEXT_MEMORY_MANAGER
 
@@ -261,7 +260,6 @@ inline bool operator!=(const ContextMemoryAllocator<T>& a1,
   return a1.d_mm != a2.d_mm;
 }
 
-}  // namespace context
-}  // namespace cvc5::internal
+}  // namespace cvc5::context
 
 #endif /* CVC5__CONTEXT__CONTEXT_MM_H */
diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp
index cce1d6871..89e64afa6 100644
--- a/src/expr/kind_template.cpp
+++ b/src/expr/kind_template.cpp
@@ -50,7 +50,7 @@ std::ostream& operator<<(std::ostream& out, cvc5::internal::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::internal::Kind k)
+bool isAssociative(cvc5::internal::Kind k)
 {
   switch(k) {
   case kind::AND:
@@ -63,7 +63,7 @@ bool isAssociative(::cvc5::internal::Kind k)
   }
 }
 
-std::string kindToString(::cvc5::internal::Kind k) { return toString(k); }
+std::string kindToString(cvc5::internal::Kind k) { return toString(k); }
 
 }  // namespace kind
 
@@ -84,7 +84,7 @@ std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant)
 
 namespace theory {
 
-TheoryId kindToTheoryId(::cvc5::internal::Kind k)
+TheoryId kindToTheoryId(cvc5::internal::Kind k)
 {
   switch (k)
   {
@@ -99,7 +99,7 @@ ${kind_to_theory_id}
   throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
 }
 
-TheoryId typeConstantToTheoryId(::cvc5::internal::TypeConstant typeConstant)
+TheoryId typeConstantToTheoryId(cvc5::internal::TypeConstant typeConstant)
 {
   switch (typeConstant)
   {
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index ca7df0944..b3b511c9d 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -40,7 +40,7 @@ enum Kind_t
 
 // import Kind into the "cvc5" namespace but keep the individual kind
 // constants under kind::
-typedef ::cvc5::internal::kind::Kind_t Kind;
+typedef cvc5::internal::kind::Kind_t Kind;
 
 namespace kind {
 
@@ -68,12 +68,12 @@ std::ostream& operator<<(std::ostream&, cvc5::internal::Kind);
  * decide whether it's safe to modify big expressions by changing the grouping of
  * the arguments. */
 /* TODO: This could be generated. */
-bool isAssociative(::cvc5::internal::Kind k);
-std::string kindToString(::cvc5::internal::Kind k);
+bool isAssociative(cvc5::internal::Kind k);
+std::string kindToString(cvc5::internal::Kind k);
 
 struct KindHashFunction
 {
-  inline size_t operator()(::cvc5::internal::Kind k) const { return k; }
+  inline size_t operator()(cvc5::internal::Kind k) const { return k; }
 }; /* struct KindHashFunction */
 
 }  // namespace kind
@@ -101,9 +101,9 @@ std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant);
 
 namespace theory {
 
-::cvc5::internal::theory::TheoryId kindToTheoryId(::cvc5::internal::Kind k);
-::cvc5::internal::theory::TheoryId typeConstantToTheoryId(
-    ::cvc5::internal::TypeConstant typeConstant);
+cvc5::internal::theory::TheoryId kindToTheoryId(cvc5::internal::Kind k);
+cvc5::internal::theory::TheoryId typeConstantToTheoryId(
+    cvc5::internal::TypeConstant typeConstant);
 
 }  // namespace theory
 }  // namespace cvc5::internal
diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp
index 693b55930..91eef65c2 100644
--- a/src/expr/metakind_template.cpp
+++ b/src/expr/metakind_template.cpp
@@ -74,8 +74,8 @@ namespace metakind {
 template <Kind k, class T, bool pool>
 struct NodeValueConstCompare
 {
-  static bool compare(const ::cvc5::internal::expr::NodeValue* x,
-                      const ::cvc5::internal::expr::NodeValue* y)
+  static bool compare(const cvc5::internal::expr::NodeValue* x,
+                      const cvc5::internal::expr::NodeValue* y)
   {
     if (pool)
     {
@@ -96,13 +96,13 @@ struct NodeValueConstCompare
     return x->getConst<T>() == y->getConst<T>();
   }
 
-  static size_t constHash(const ::cvc5::internal::expr::NodeValue* nv)
+  static size_t constHash(const cvc5::internal::expr::NodeValue* nv)
   {
     return nv->getConst<T>().hash();
   }
 };
 
-size_t NodeValueCompare::constHash(const ::cvc5::internal::expr::NodeValue* nv)
+size_t NodeValueCompare::constHash(const cvc5::internal::expr::NodeValue* nv)
 {
   Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
 
@@ -111,13 +111,14 @@ size_t NodeValueCompare::constHash(const ::cvc5::internal::expr::NodeValue* nv)
 // clang-format off
     ${metakind_constHashes}
 // clang-format on
-default: Unhandled() << ::cvc5::internal::expr::NodeValue::dKindToKind(nv->d_kind);
+    default:
+      Unhandled() << cvc5::internal::expr::NodeValue::dKindToKind(nv->d_kind);
   }
 }
 
 template <bool pool>
-bool NodeValueCompare::compare(const ::cvc5::internal::expr::NodeValue* nv1,
-                               const ::cvc5::internal::expr::NodeValue* nv2)
+bool NodeValueCompare::compare(const cvc5::internal::expr::NodeValue* nv1,
+                               const cvc5::internal::expr::NodeValue* nv2)
 {
   if(nv1->d_kind != nv2->d_kind) {
     return false;
@@ -130,7 +131,8 @@ bool NodeValueCompare::compare(const ::cvc5::internal::expr::NodeValue* nv1,
 // clang-format off
 ${metakind_compares}
 // clang-format on
-default: Unhandled() << ::cvc5::internal::expr::NodeValue::dKindToKind(nv1->d_kind);
+default:
+  Unhandled() << cvc5::internal::expr::NodeValue::dKindToKind(nv1->d_kind);
     }
   }
 
@@ -138,9 +140,9 @@ default: Unhandled() << ::cvc5::internal::expr::NodeValue::dKindToKind(nv1->d_ki
     return false;
   }
 
-  ::cvc5::internal::expr::NodeValue::const_nv_iterator i = nv1->nv_begin();
-  ::cvc5::internal::expr::NodeValue::const_nv_iterator j = nv2->nv_begin();
-  ::cvc5::internal::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end();
+  cvc5::internal::expr::NodeValue::const_nv_iterator i = nv1->nv_begin();
+  cvc5::internal::expr::NodeValue::const_nv_iterator j = nv2->nv_begin();
+  cvc5::internal::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end();
 
   while(i != i_end) {
     if((*i) != (*j)) {
@@ -154,12 +156,14 @@ default: Unhandled() << ::cvc5::internal::expr::NodeValue::dKindToKind(nv1->d_ki
 }
 
 template bool NodeValueCompare::compare<true>(
-    const ::cvc5::internal::expr::NodeValue* nv1, const ::cvc5::internal::expr::NodeValue* nv2);
+    const cvc5::internal::expr::NodeValue* nv1,
+    const cvc5::internal::expr::NodeValue* nv2);
 template bool NodeValueCompare::compare<false>(
-    const ::cvc5::internal::expr::NodeValue* nv1, const ::cvc5::internal::expr::NodeValue* nv2);
+    const cvc5::internal::expr::NodeValue* nv1,
+    const cvc5::internal::expr::NodeValue* nv2);
 
 void nodeValueConstantToStream(std::ostream& out,
-                               const ::cvc5::internal::expr::NodeValue* nv)
+                               const cvc5::internal::expr::NodeValue* nv)
 {
   Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
 
@@ -168,7 +172,8 @@ void nodeValueConstantToStream(std::ostream& out,
 // clang-format off
 ${metakind_constPrinters}
 // clang-format on
-default: Unhandled() << ::cvc5::internal::expr::NodeValue::dKindToKind(nv->d_kind);
+default:
+  Unhandled() << cvc5::internal::expr::NodeValue::dKindToKind(nv->d_kind);
   }
 }
 
@@ -189,7 +194,7 @@ default: Unhandled() << ::cvc5::internal::expr::NodeValue::dKindToKind(nv->d_kin
  * This doesn't support "non-inlined" NodeValues, which shouldn't need this
  * kind of cleanup.
  */
-void deleteNodeValueConstant(::cvc5::internal::expr::NodeValue* nv)
+void deleteNodeValueConstant(cvc5::internal::expr::NodeValue* nv)
 {
   Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
 
@@ -198,14 +203,15 @@ void deleteNodeValueConstant(::cvc5::internal::expr::NodeValue* nv)
 // clang-format off
 ${metakind_constDeleters}
 // clang-format on
-default: Unhandled() << ::cvc5::internal::expr::NodeValue::dKindToKind(nv->d_kind);
+default:
+  Unhandled() << cvc5::internal::expr::NodeValue::dKindToKind(nv->d_kind);
   }
 }
 
 // re-enable the strict-aliasing warning
 # pragma GCC diagnostic warning "-Wstrict-aliasing"
 
-uint32_t getMinArityForKind(::cvc5::internal::Kind k)
+uint32_t getMinArityForKind(cvc5::internal::Kind k)
 {
   static const unsigned lbs[] = {
     0, /* NULL_EXPR */
@@ -219,7 +225,7 @@ ${metakind_lbchildren}
   return lbs[k];
 }
 
-uint32_t getMaxArityForKind(::cvc5::internal::Kind k)
+uint32_t getMaxArityForKind(cvc5::internal::Kind k)
 {
   static const unsigned ubs[] = {
     0, /* NULL_EXPR */
@@ -240,7 +246,7 @@ ${metakind_ubchildren}
  * example, since the kind of functions is just VARIABLE, it should map
  * VARIABLE to APPLY_UF.
  */
-Kind operatorToKind(::cvc5::internal::expr::NodeValue* nv)
+Kind operatorToKind(cvc5::internal::expr::NodeValue* nv)
 {
   if(nv->getKind() == kind::BUILTIN) {
     return nv->getConst<Kind>();
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index c9e6e4c36..6fcfcbcce 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -38,9 +38,9 @@ namespace metakind {
 
 struct NodeValueCompare {
   template <bool pool>
-  static bool compare(const ::cvc5::internal::expr::NodeValue* nv1,
-                      const ::cvc5::internal::expr::NodeValue* nv2);
-  static size_t constHash(const ::cvc5::internal::expr::NodeValue* nv);
+  static bool compare(const cvc5::internal::expr::NodeValue* nv1,
+                      const cvc5::internal::expr::NodeValue* nv2);
+  static size_t constHash(const cvc5::internal::expr::NodeValue* nv);
 };/* struct NodeValueCompare */
 
 /**
@@ -67,7 +67,7 @@ enum MetaKind_t {
  * @param nv the node value representing a constant node
  */
 void nodeValueConstantToStream(std::ostream& out,
-                               const ::cvc5::internal::expr::NodeValue* nv);
+                               const cvc5::internal::expr::NodeValue* nv);
 
 /**
  * Cleanup to be performed when a NodeValue zombie is collected, and
@@ -78,18 +78,18 @@ void nodeValueConstantToStream(std::ostream& out,
  * This doesn't support "non-inlined" NodeValues, which shouldn't need this
  * kind of cleanup.
  */
-void deleteNodeValueConstant(::cvc5::internal::expr::NodeValue* nv);
+void deleteNodeValueConstant(cvc5::internal::expr::NodeValue* nv);
 
 /** Return the minimum arity of the given kind. */
-uint32_t getMinArityForKind(::cvc5::internal::Kind k);
+uint32_t getMinArityForKind(cvc5::internal::Kind k);
 /** Return the maximum arity of the given kind. */
-uint32_t getMaxArityForKind(::cvc5::internal::Kind k);
+uint32_t getMaxArityForKind(cvc5::internal::Kind k);
 
 }  // namespace metakind
 
 // import MetaKind into the "cvc5::internal::kind" namespace but keep the
 // individual MetaKind constants under kind::metakind::
-typedef ::cvc5::internal::kind::metakind::MetaKind_t MetaKind;
+typedef cvc5::internal::kind::metakind::MetaKind_t MetaKind;
 
 /**
  * Get the metakind for a particular kind.
@@ -101,7 +101,7 @@ MetaKind metaKindOf(Kind k);
  * example, since the kind of functions is just VARIABLE, it should map
  * VARIABLE to APPLY_UF.
  */
-Kind operatorToKind(::cvc5::internal::expr::NodeValue* nv);
+Kind operatorToKind(cvc5::internal::expr::NodeValue* nv);
 
 }  // namespace kind
 
@@ -111,7 +111,8 @@ namespace expr {
 struct NodeValuePoolEq {
   bool operator()(const NodeValue* nv1, const NodeValue* nv2) const
   {
-    return ::cvc5::internal::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2);
+    return cvc5::internal::kind::metakind::NodeValueCompare::compare<true>(nv1,
+                                                                           nv2);
   }
 };
 
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 490e0adb1..d67e8f393 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -44,7 +44,7 @@ namespace expr {
 namespace kind {
   namespace metakind {
 
-  template < ::cvc5::internal::Kind k, class T, bool pool>
+  template <cvc5::internal::Kind k, class T, bool pool>
   struct NodeValueConstCompare;
 
   struct NodeValueCompare;
@@ -60,10 +60,10 @@ namespace expr {
 class NodeValue
 {
   template <bool>
-  friend class ::cvc5::internal::NodeTemplate;
-  friend class ::cvc5::internal::TypeNode;
-  friend class ::cvc5::internal::NodeBuilder;
-  friend class ::cvc5::internal::NodeManager;
+  friend class cvc5::internal::NodeTemplate;
+  friend class cvc5::internal::TypeNode;
+  friend class cvc5::internal::NodeBuilder;
+  friend class cvc5::internal::NodeManager;
 
   template <Kind k, class T, bool pool>
   friend struct kind::metakind::NodeValueConstCompare;
diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp
index 846254bf2..7d05a785b 100644
--- a/src/expr/symbol_manager.cpp
+++ b/src/expr/symbol_manager.cpp
@@ -20,7 +20,7 @@
 #include "context/cdlist.h"
 #include "context/cdo.h"
 
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5 {
 
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index f6153372a..a765da157 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -28,15 +28,15 @@
 
 namespace cvc5::internal {
 
-using ::cvc5::internal::context::CDHashMap;
-using ::cvc5::internal::context::CDHashSet;
-using ::cvc5::internal::context::Context;
-using ::std::copy;
-using ::std::endl;
-using ::std::ostream_iterator;
-using ::std::pair;
-using ::std::string;
-using ::std::vector;
+using context::CDHashMap;
+using context::CDHashSet;
+using context::Context;
+using std::copy;
+using std::endl;
+using std::ostream_iterator;
+using std::pair;
+using std::string;
+using std::vector;
 
 /** Overloaded type trie.
  *
diff --git a/src/preprocessing/learned_literal_manager.h b/src/preprocessing/learned_literal_manager.h
index 22d9fad91..001f79b8e 100644
--- a/src/preprocessing/learned_literal_manager.h
+++ b/src/preprocessing/learned_literal_manager.h
@@ -56,7 +56,7 @@ class LearnedLiteralManager : protected EnvObj
 
  private:
   /** Learned literal map */
-  typedef context::CDHashSet<Node> NodeSet;
+  using NodeSet = context::CDHashSet<Node>;
   /** Learned literals */
   NodeSet d_learnedLits;
 };
diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h
index 4b24d223d..82e9a4b17 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.h
+++ b/src/preprocessing/passes/unconstrained_simplifier.h
@@ -30,10 +30,10 @@
 #include "theory/substitutions.h"
 #include "util/statistics_stats.h"
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 class Context;
 }
+namespace cvc5::internal {
 namespace preprocessing {
 namespace passes {
 
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 4176ac03c..da1dd5582 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -133,8 +133,8 @@ class ScopedBool
 
 Solver::Solver(Env& env,
                cvc5::internal::prop::TheoryProxy* proxy,
-               cvc5::internal::context::Context* context,
-               cvc5::internal::context::UserContext* userContext,
+               context::Context* context,
+               context::UserContext* userContext,
                ProofNodeManager* pnm,
                bool enableIncremental)
     : EnvObj(env),
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index bb2167d0d..5704133f4 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -75,7 +75,7 @@ class Solver : protected EnvObj
   cvc5::internal::prop::TheoryProxy* d_proxy;
 
   /** The contexts from the SMT solver */
-  cvc5::internal::context::Context* d_context;
+  context::Context* d_context;
 
   /** The current assertion level (user) */
   int assertionLevel;
@@ -132,8 +132,8 @@ public:
     //
  Solver(Env& env,
         cvc5::internal::prop::TheoryProxy* proxy,
-        cvc5::internal::context::Context* context,
-        cvc5::internal::context::UserContext* userContext,
+        context::Context* context,
+        context::UserContext* userContext,
         ProofNodeManager* pnm,
         bool enableIncremental = false);
  virtual ~Solver();
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index fdbdb6ad8..cb9c034ad 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -50,7 +50,7 @@ class MinisatSatSolver : public CDCLTSatSolverInterface, protected EnvObj
   static void  toSatClause    (const Minisat::Clause& clause, SatClause& sat_clause);
   void initialize(context::Context* context,
                   TheoryProxy* theoryProxy,
-                  cvc5::internal::context::UserContext* userContext,
+                  context::UserContext* userContext,
                   ProofNodeManager* pnm) override;
 
   ClauseId addClause(SatClause& clause, bool removable) override;
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index c1e4a93b3..879fb51c6 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -49,8 +49,8 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of
 
 SimpSolver::SimpSolver(Env& env,
                        cvc5::internal::prop::TheoryProxy* proxy,
-                       cvc5::internal::context::Context* context,
-                       cvc5::internal::context::UserContext* userContext,
+                       context::Context* context,
+                       context::UserContext* userContext,
                        ProofNodeManager* pnm,
                        bool enableIncremental)
     : Solver(env, proxy, context, userContext, pnm, enableIncremental),
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index be795681b..79d37c3f4 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -44,8 +44,8 @@ class SimpSolver : public Solver {
     //
   SimpSolver(Env& env,
              cvc5::internal::prop::TheoryProxy* proxy,
-             cvc5::internal::context::Context* context,
-             cvc5::internal::context::UserContext* userContext,
+             context::Context* context,
+             context::UserContext* userContext,
              ProofNodeManager* pnm,
              bool enableIncremental = false);
   ~SimpSolver();
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 47b9b9f22..024273c2f 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -124,7 +124,7 @@ class CDCLTSatSolverInterface : public SatSolver
 
   virtual void initialize(context::Context* context,
                           prop::TheoryProxy* theoryProxy,
-                          cvc5::internal::context::UserContext* userContext,
+                          context::UserContext* userContext,
                           ProofNodeManager* pnm) = 0;
 
   virtual void push() = 0;
diff --git a/src/smt/env.h b/src/smt/env.h
index 155b16ec2..12f4cc5be 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -27,6 +27,11 @@
 #include "theory/theory_id.h"
 #include "util/statistics_registry.h"
 
+namespace cvc5::context {
+class Context;
+class UserContext;
+}  // namespace cvc5::context
+
 namespace cvc5::internal {
 
 class NodeManager;
@@ -39,11 +44,6 @@ enum class OutputTag;
 }
 using OutputTag = options::OutputTag;
 
-namespace context {
-class Context;
-class UserContext;
-}  // namespace context
-
 namespace smt {
 class PfManager;
 }
diff --git a/src/smt/env_obj.h b/src/smt/env_obj.h
index 5ad20f415..e5a6e152e 100644
--- a/src/smt/env_obj.h
+++ b/src/smt/env_obj.h
@@ -22,6 +22,12 @@
 #include <memory>
 
 #include "expr/node.h"
+
+namespace cvc5::context {
+class Context;
+class UserContext;
+}  // namespace cvc5::context
+
 namespace cvc5::internal {
 
 class Env;
@@ -30,10 +36,6 @@ class NodeManager;
 class Options;
 class StatisticsRegistry;
 
-namespace context {
-class Context;
-class UserContext;
-}  // namespace context
 namespace options {
 enum class OutputTag;
 }
diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 59264ee70..3babf40ae 100644
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -77,7 +77,7 @@ using namespace std;
 using namespace cvc5::internal::smt;
 using namespace cvc5::internal::preprocessing;
 using namespace cvc5::internal::prop;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::theory;
 
 namespace cvc5::internal {
@@ -140,11 +140,14 @@ Result SolverEngine::getStatusOfLastCommand() const
 {
   return d_state->getStatus();
 }
-context::UserContext* SolverEngine::getUserContext()
+UserContext* SolverEngine::getUserContext()
 {
   return d_env->getUserContext();
 }
-context::Context* SolverEngine::getContext() { return d_env->getContext(); }
+Context* SolverEngine::getContext()
+{
+  return d_env->getContext();
+}
 
 TheoryEngine* SolverEngine::getTheoryEngine()
 {
@@ -1159,7 +1162,7 @@ std::pair<Node, Node> SolverEngine::getSepHeapAndNilExpr(void)
 std::vector<Node> SolverEngine::getAssertionsInternal()
 {
   Assert(d_state->isFullyInited());
-  const context::CDList<Node>& al = d_asserts->getAssertionList();
+  const CDList<Node>& al = d_asserts->getAssertionList();
   std::vector<Node> res;
   for (const Node& n : al)
   {
@@ -1442,7 +1445,7 @@ void SolverEngine::checkUnsatCore()
 
 void SolverEngine::checkModel(bool hardFailure)
 {
-  const context::CDList<Node>& al = d_asserts->getAssertionList();
+  const CDList<Node>& al = d_asserts->getAssertionList();
   // we always enable the assertion list, so it is able to be checked
 
   TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index 5bdc3201b..bfcc45dce 100644
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -31,6 +31,11 @@
 #include "util/result.h"
 #include "util/synth_result.h"
 
+namespace cvc5::context {
+class Context;
+class UserContext;
+}  // namespace cvc5::context
+
 namespace cvc5 {
 
 class Solver;
@@ -54,15 +59,6 @@ struct InstantiationList;
 
 /* -------------------------------------------------------------------------- */
 
-/* -------------------------------------------------------------------------- */
-
-namespace context {
-class Context;
-class UserContext;
-}  // namespace context
-
-/* -------------------------------------------------------------------------- */
-
 namespace preprocessing {
 class PreprocessingPassContext;
 }
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 6f2866a1c..530fba94b 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -34,11 +34,8 @@ namespace cvc5::internal {
 namespace theory {
 namespace arith {
 
-
-ArithStaticLearner::ArithStaticLearner(context::Context* userContext) :
-  d_minMap(userContext),
-  d_maxMap(userContext),
-  d_statistics()
+ArithStaticLearner::ArithStaticLearner(context::Context* userContext)
+    : d_minMap(userContext), d_maxMap(userContext), d_statistics()
 {
 }
 
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index 703bdbfd9..f1cc8379d 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -26,10 +26,11 @@
 #include "theory/arith/delta_rational.h"
 #include "util/statistics_stats.h"
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 class Context;
 }
+
+namespace cvc5::internal {
 namespace theory {
 namespace arith {
 
@@ -44,29 +45,29 @@ private:
  CDNodeToMinMaxMap d_maxMap;
 
 public:
-  ArithStaticLearner(context::Context* userContext);
-  ~ArithStaticLearner();
-  void staticLearning(TNode n, NodeBuilder& learned);
-
-  void addBound(TNode n);
+ ArithStaticLearner(context::Context* userContext);
+ ~ArithStaticLearner();
+ void staticLearning(TNode n, NodeBuilder& learned);
 
- private:
-  void process(TNode n, NodeBuilder& learned, const TNodeSet& defTrue);
+ void addBound(TNode n);
 
-  void iteMinMax(TNode n, NodeBuilder& learned);
-  void iteConstant(TNode n, NodeBuilder& learned);
-
-  /**
-   * These fields are designed to be accessible to ArithStaticLearner methods.
-   */
-  class Statistics
-  {
-   public:
-    IntStat d_iteMinMaxApplications;
-    IntStat d_iteConstantApplications;
-
-    Statistics();
-  };
+private:
+ void process(TNode n, NodeBuilder& learned, const TNodeSet& defTrue);
+
+ void iteMinMax(TNode n, NodeBuilder& learned);
+ void iteConstant(TNode n, NodeBuilder& learned);
+
+ /**
+  * These fields are designed to be accessible to ArithStaticLearner methods.
+  */
+ class Statistics
+ {
+  public:
+   IntStat d_iteMinMaxApplications;
+   IntStat d_iteConstantApplications;
+
+   Statistics();
+ };
 
   Statistics d_statistics;
 
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index cf0ec4340..29c2d45cb 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -34,16 +34,16 @@
 #include "util/dense_map.h"
 #include "util/statistics_stats.h"
 
+namespace cvc5::context {
+class Context;
+class UserContext;
+}  // namespace cvc5::context
+
 namespace cvc5::internal {
 
 class ProofNodeManager;
 class EagerProofGenerator;
 
-namespace context {
-class Context;
-class UserContext;
-}
-
 namespace theory {
 struct EeSetupInfo;
 
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index c0ac9d07a..e925bba58 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -2019,12 +2019,12 @@ bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const {
   return v < d_varDatabases.size();
 }
 
-
-ConstraintDatabase::Watches::Watches(context::Context* satContext, context::Context* userContext):
-  d_constraintProofs(satContext),
-  d_canBePropagatedWatches(satContext),
-  d_assertionOrderWatches(satContext),
-  d_splitWatches(userContext)
+ConstraintDatabase::Watches::Watches(context::Context* satContext,
+                                     context::Context* userContext)
+    : d_constraintProofs(satContext),
+      d_canBePropagatedWatches(satContext),
+      d_assertionOrderWatches(satContext),
+      d_splitWatches(userContext)
 {}
 
 
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 7aaa3a8ba..1a31d0b51 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -94,14 +94,14 @@
 #include "theory/arith/delta_rational.h"
 #include "util/statistics_stats.h"
 
+namespace cvc5::context {
+class Context;
+}
 namespace cvc5::internal {
 
 class ProofNodeManager;
 class EagerProofGenerator;
 
-namespace context {
-class Context;
-}
 namespace theory {
 
 namespace arith {
@@ -152,7 +152,6 @@ enum ArithProofType
  */
 enum ConstraintType {LowerBound, Equality, UpperBound, Disequality};
 
-
 typedef context::CDList<ConstraintCP> CDConstraintList;
 
 typedef std::unordered_map<Node, ConstraintP> NodetoConstraintMap;
@@ -1034,13 +1033,14 @@ class ConstraintDatabase : protected EnvObj
    */
   CDConstraintList d_antecedents;
 
-  typedef context::CDList<ConstraintRule, Constraint::ConstraintRuleCleanup> ConstraintRuleList;
-  typedef context::CDList<ConstraintP, Constraint::CanBePropagatedCleanup> CBPList;
-  typedef context::CDList<ConstraintP, Constraint::AssertionOrderCleanup> AOList;
+  typedef context::CDList<ConstraintRule, Constraint::ConstraintRuleCleanup>
+      ConstraintRuleList;
+  typedef context::CDList<ConstraintP, Constraint::CanBePropagatedCleanup>
+      CBPList;
+  typedef context::CDList<ConstraintP, Constraint::AssertionOrderCleanup>
+      AOList;
   typedef context::CDList<ConstraintP, Constraint::SplitCleanup> SplitList;
 
-
-
   /**
    * The watch lists are collected together as they need to be garbage collected
    * carefully.
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 8f17d4e4d..e8dbd3dfc 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -31,10 +31,10 @@
 #include "util/rational.h"
 #include "util/statistics_stats.h"
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 class Context;
 }
+namespace cvc5::internal {
 namespace theory {
 namespace arith {
 
@@ -65,7 +65,6 @@ class DioSolver : protected EnvObj
    */
   context::CDO<size_t> d_nextInputConstraintToEnqueue;
 
-
   /**
    * We maintain a map from the variables associated with proofs to an input constraint.
    * These variables can then be used in polynomial manipulations.
@@ -109,7 +108,8 @@ class DioSolver : protected EnvObj
   // /** Compare by d_minimal. */
   // struct TrailMinimalCoefficientOrder {
   //   const context::CDList<Constraint>& d_trail;
-  //   TrailMinimalCoefficientOrder(const context::CDList<Constraint>& trail):
+  //   TrailMinimalCoefficientOrder(const context::CDList<Constraint>&
+  //   trail):
   //     d_trail(trail)
   //   {}
 
@@ -175,8 +175,7 @@ class DioSolver : protected EnvObj
    */
   context::CDQueue<TrailIndex> d_decompositionLemmaQueue;
 
-public:
-
+ public:
   /** Construct a Diophantine equation solver with the given context. */
  DioSolver(Env& env);
 
diff --git a/src/theory/arith/nl/coverings/proof_generator.cpp b/src/theory/arith/nl/coverings/proof_generator.cpp
index c7504b263..3dc132b7f 100644
--- a/src/theory/arith/nl/coverings/proof_generator.cpp
+++ b/src/theory/arith/nl/coverings/proof_generator.cpp
@@ -92,7 +92,7 @@ Node mkIRP(const Node& var,
 }  // namespace
 
 CoveringsProofGenerator::CoveringsProofGenerator(context::Context* ctx,
-                                     ProofNodeManager* pnm)
+                                                 ProofNodeManager* pnm)
     : d_pnm(pnm), d_proofs(pnm, ctx), d_current(nullptr)
 {
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index a643066f1..51f50e942 100644
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -25,12 +25,12 @@
 #include "expr/subs.h"
 #include "smt/env_obj.h"
 
-namespace cvc5::internal {
-
-namespace context {
+namespace cvc5::context {
 class Context;
 }
 
+namespace cvc5::internal {
+
 namespace theory {
 
 class TheoryModel;
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 58218a731..5b9afde81 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -27,20 +27,21 @@ namespace cvc5::internal {
 namespace theory {
 namespace arith {
 
-ArithVariables::ArithVariables(context::Context* c, DeltaComputeCallback deltaComputingFunc)
- : d_vars(),
-   d_safeAssignment(),
-   d_numberOfVariables(0),
-   d_pool(),
-   d_released(),
-   d_nodeToArithVarMap(),
-   d_boundsQueue(),
-   d_enqueueingBoundCounts(true),
-   d_lbRevertHistory(c, true, LowerBoundCleanUp(this)),
-   d_ubRevertHistory(c, true, UpperBoundCleanUp(this)),
-   d_deltaIsSafe(false),
-   d_delta(-1,1),
-   d_deltaComputingFunc(deltaComputingFunc)
+ArithVariables::ArithVariables(context::Context* c,
+                               DeltaComputeCallback deltaComputingFunc)
+    : d_vars(),
+      d_safeAssignment(),
+      d_numberOfVariables(0),
+      d_pool(),
+      d_released(),
+      d_nodeToArithVarMap(),
+      d_boundsQueue(),
+      d_enqueueingBoundCounts(true),
+      d_lbRevertHistory(c, true, LowerBoundCleanUp(this)),
+      d_ubRevertHistory(c, true, UpperBoundCleanUp(this)),
+      d_deltaIsSafe(false),
+      d_delta(-1, 1),
+      d_deltaComputingFunc(deltaComputingFunc)
 { }
 
 ArithVar ArithVariables::getNumberOfVariables() const {
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 05f3db6be..4375ee629 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -33,10 +33,10 @@
 #include "theory/arith/constraint_forward.h"
 #include "theory/arith/delta_rational.h"
 
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
 class Context;
 }
+namespace cvc5::internal {
 namespace theory {
 namespace arith {
 
@@ -235,25 +235,25 @@ private:
 
 
 public:
-
-  ArithVariables(context::Context* c, DeltaComputeCallback deltaComputation);
-
-  /**
-   * This sets the lower bound for a variable in the current context.
-   * This must be stronger the previous constraint.
-   */
-  void setLowerBoundConstraint(ConstraintP lb);
-
-  /**
-   * This sets the upper bound for a variable in the current context.
-   * This must be stronger the previous constraint.
-   */
-  void setUpperBoundConstraint(ConstraintP ub);
-
-  /** Returns the constraint for the upper bound of a variable. */
-  inline ConstraintP getUpperBoundConstraint(ArithVar x) const{
-    return d_vars[x].d_ub;
-  }
+ ArithVariables(context::Context* c, DeltaComputeCallback deltaComputation);
+
+ /**
+  * This sets the lower bound for a variable in the current context.
+  * This must be stronger the previous constraint.
+  */
+ void setLowerBoundConstraint(ConstraintP lb);
+
+ /**
+  * This sets the upper bound for a variable in the current context.
+  * This must be stronger the previous constraint.
+  */
+ void setUpperBoundConstraint(ConstraintP ub);
+
+ /** Returns the constraint for the upper bound of a variable. */
+ inline ConstraintP getUpperBoundConstraint(ArithVar x) const
+ {
+   return d_vars[x].d_ub;
+ }
   /** Returns the constraint for the lower bound of a variable. */
   inline ConstraintP getLowerBoundConstraint(ArithVar x) const{
     return d_vars[x].d_lb;
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 6e11f124d..bfbaa79c6 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -719,11 +719,10 @@ private:
   void branchVector(const std::vector<ArithVar>& lemmas);
 
   context::CDO<unsigned> d_cutCount;
-  context::CDHashSet<ArithVar, std::hash<ArithVar> > d_cutInContext;
+  context::CDHashSet<ArithVar, std::hash<ArithVar>> d_cutInContext;
 
   context::CDO<bool> d_likelyIntegerInfeasible;
 
-
   context::CDO<bool> d_guessedCoeffSet;
   ArithRatPairVec d_guessedCoeffs;
 
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 15db3e1fa..a911837cb 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -43,8 +43,7 @@ Info::~Info() {
   in_stores->deleteSelf();
 }
 
-ArrayInfo::ArrayInfo(context::Context* c,
-                     std::string statisticsPrefix)
+ArrayInfo::ArrayInfo(context::Context* c, std::string statisticsPrefix)
     : ct(c),
       info_map(),
       d_mergeInfoTimer(smtStatisticsRegistry().registerTimer(
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index a1136a272..fb5ecd841 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -56,33 +56,34 @@ bool inList(const CTNodeList* l, const TNode el);
 
 class Info {
 public:
-  context::CDO<bool> isNonLinear;
-  context::CDO<bool> rIntro1Applied;
-  context::CDO<TNode> modelRep;
-  context::CDO<TNode> constArr;
-  context::CDO<TNode> weakEquivPointer;
-  context::CDO<TNode> weakEquivIndex;
-  context::CDO<TNode> weakEquivSecondary;
-  context::CDO<TNode> weakEquivSecondaryReason;
-  CTNodeList* indices;
-  CTNodeList* stores;
-  CTNodeList* in_stores;
-
-  Info(context::Context* c);
-  ~Info();
-
-  /**
-   * prints the information
-   */
-  void print() const {
-    Assert(indices != NULL && stores != NULL && in_stores != NULL);
-    Trace("arrays-info")<<"  indices   ";
-    printList(indices);
-    Trace("arrays-info")<<"  stores ";
-    printList(stores);
-    Trace("arrays-info")<<"  in_stores ";
-    printList(in_stores);
-  }
+ context::CDO<bool> isNonLinear;
+ context::CDO<bool> rIntro1Applied;
+ context::CDO<TNode> modelRep;
+ context::CDO<TNode> constArr;
+ context::CDO<TNode> weakEquivPointer;
+ context::CDO<TNode> weakEquivIndex;
+ context::CDO<TNode> weakEquivSecondary;
+ context::CDO<TNode> weakEquivSecondaryReason;
+ CTNodeList* indices;
+ CTNodeList* stores;
+ CTNodeList* in_stores;
+
+ Info(context::Context* c);
+ ~Info();
+
+ /**
+  * prints the information
+  */
+ void print() const
+ {
+   Assert(indices != NULL && stores != NULL && in_stores != NULL);
+   Trace("arrays-info") << "  indices   ";
+   printList(indices);
+   Trace("arrays-info") << "  stores ";
+   printList(stores);
+   Trace("arrays-info") << "  in_stores ";
+   printList(in_stores);
+ }
 };/* class Info */
 
 typedef std::unordered_map<Node, Info*> CNodeInfoMap;
@@ -98,33 +99,33 @@ typedef std::unordered_map<Node, Info*> CNodeInfoMap;
  */
 class ArrayInfo {
 private:
-  context::Context* ct;
-  CNodeInfoMap info_map;
-
-  CTNodeList* emptyList;
-
-  /* == STATISTICS == */
-
-  /** time spent in preregisterTerm() */
-  TimerStat d_mergeInfoTimer;
-  AverageStat d_avgIndexListLength;
-  AverageStat d_avgStoresListLength;
-  AverageStat d_avgInStoresListLength;
-  IntStat d_listsCount;
-  IntStat d_callsMergeInfo;
-  IntStat d_maxList;
-  SizeStat<CNodeInfoMap> d_tableSize;
-
-  /**
-   * checks if a certain element is in the list l
-   * FIXME: better way to check for duplicates?
-   */
-
-  /**
-   * helper method that merges two lists into the first
-   * without adding duplicates
-   */
-  void mergeLists(CTNodeList* la, const CTNodeList* lb) const;
+ context::Context* ct;
+ CNodeInfoMap info_map;
+
+ CTNodeList* emptyList;
+
+ /* == STATISTICS == */
+
+ /** time spent in preregisterTerm() */
+ TimerStat d_mergeInfoTimer;
+ AverageStat d_avgIndexListLength;
+ AverageStat d_avgStoresListLength;
+ AverageStat d_avgInStoresListLength;
+ IntStat d_listsCount;
+ IntStat d_callsMergeInfo;
+ IntStat d_maxList;
+ SizeStat<CNodeInfoMap> d_tableSize;
+
+ /**
+  * checks if a certain element is in the list l
+  * FIXME: better way to check for duplicates?
+  */
+
+ /**
+  * helper method that merges two lists into the first
+  * without adding duplicates
+  */
+ void mergeLists(CTNodeList* la, const CTNodeList* lb) const;
 
 public:
   const Info* emptyInfo;
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 8752779fd..e82f30c01 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1190,7 +1190,8 @@ void TheoryArrays::postCheck(Effort level)
       && weakEquiv)
   {
     // Replay all array merges to update weak equivalence data structures
-    context::CDList<Node>::iterator it = d_arrayMerges.begin(), iend = d_arrayMerges.end();
+    context::CDList<Node>::iterator it = d_arrayMerges.begin(),
+                                    iend = d_arrayMerges.end();
     TNode a, b, eq;
     for (; it != iend; ++it) {
       eq = *it;
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 0b10859c6..05f58085b 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -371,7 +371,7 @@ class TheoryArrays : public Theory {
   using RowLemmaType = std::tuple<TNode, TNode, TNode, TNode>;
 
   context::CDQueue<RowLemmaType> d_RowQueue;
-  context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded;
+  context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction> d_RowAlreadyAdded;
 
   typedef context::CDHashSet<Node> CDNodeSet;
 
@@ -389,24 +389,29 @@ class TheoryArrays : public Theory {
   context::CDList<TNode> d_constReadsList;
   context::Context* d_constReadsContext;
   /** Helper class to keep d_constReadsContext in sync with satContext */
-  class ContextPopper : public context::ContextNotifyObj {
+  class ContextPopper : public context::ContextNotifyObj
+  {
     context::Context* d_satContext;
     context::Context* d_contextToPop;
-  protected:
-   void contextNotifyPop() override
-   {
-     if (d_contextToPop->getLevel() > d_satContext->getLevel())
-     {
-       d_contextToPop->pop();
-     }
+
+   protected:
+    void contextNotifyPop() override
+    {
+      if (d_contextToPop->getLevel() > d_satContext->getLevel())
+      {
+        d_contextToPop->pop();
+      }
     }
-  public:
+
+   public:
     ContextPopper(context::Context* context, context::Context* contextToPop)
-      :context::ContextNotifyObj(context), d_satContext(context),
-       d_contextToPop(contextToPop)
-    {}
+        : context::ContextNotifyObj(context),
+          d_satContext(context),
+          d_contextToPop(contextToPop)
+    {
+    }
 
-  };/* class ContextPopper */
+  }; /* class ContextPopper */
   ContextPopper d_contextPopper;
 
   // The decision requests we have for the core
diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h
index 866d3ae86..958dc7ead 100644
--- a/src/theory/arrays/union_find.h
+++ b/src/theory/arrays/union_find.h
@@ -26,18 +26,18 @@
 #include "expr/node.h"
 #include "context/cdo.h"
 
-namespace cvc5::internal {
-
-namespace context {
-  class Context;
-  }  // namespace context
+namespace cvc5::context {
+class Context;
+}
 
+namespace cvc5::internal {
 namespace theory {
 namespace arrays {
 
 // NodeType \in { Node, TNode }
 template <class NodeType, class NodeHash>
-class UnionFind : context::ContextNotifyObj {
+class UnionFind : context::ContextNotifyObj
+{
   /** Our underlying map type. */
   typedef std::unordered_map<NodeType, NodeType, NodeHash> MapType;
 
@@ -55,9 +55,9 @@ class UnionFind : context::ContextNotifyObj {
   context::CDO<size_t> d_offset;
 
  public:
-  UnionFind(context::Context* ctxt) :
-    context::ContextNotifyObj(ctxt),
-    d_offset(ctxt, 0) {
+  UnionFind(context::Context* ctxt)
+      : context::ContextNotifyObj(ctxt), d_offset(ctxt, 0)
+  {
   }
 
   /**
@@ -84,7 +84,7 @@ class UnionFind : context::ContextNotifyObj {
    */
   void notify();
 
-};/* class UnionFind<> */
+}; /* class UnionFind<> */
 
 template <class NodeType, class NodeHash>
 inline TNode UnionFind<NodeType, NodeHash>::debugFind(TNode n) const {
diff --git a/src/theory/atom_requests.cpp b/src/theory/atom_requests.cpp
index 0b9560982..db71ba7ef 100644
--- a/src/theory/atom_requests.cpp
+++ b/src/theory/atom_requests.cpp
@@ -21,9 +21,9 @@
 using namespace cvc5::internal;
 
 AtomRequests::AtomRequests(context::Context* context)
-: d_allRequests(context)
-, d_requests(context)
-, d_triggerToRequestMap(context)
+    : d_allRequests(context),
+      d_requests(context),
+      d_triggerToRequestMap(context)
 {}
 
 AtomRequests::element_index AtomRequests::getList(TNode trigger) const {
diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp
index 32257b5b0..c9c12d483 100644
--- a/src/theory/bags/bag_solver.cpp
+++ b/src/theory/bags/bag_solver.cpp
@@ -25,7 +25,7 @@
 #include "util/rational.h"
 
 using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
diff --git a/src/theory/bags/card_solver.cpp b/src/theory/bags/card_solver.cpp
index b8b874248..7c33f5699 100644
--- a/src/theory/bags/card_solver.cpp
+++ b/src/theory/bags/card_solver.cpp
@@ -26,7 +26,7 @@
 #include "util/rational.h"
 
 using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 2561e7b6d..2a019b980 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -120,8 +120,7 @@ BVSolverBitblast::BVSolverBitblast(Env& env,
       d_bbInputFacts(context()),
       d_assumptions(context()),
       d_assertions(context()),
-      d_epg(pnm ? new EagerProofGenerator(pnm, userContext(), "")
-                : nullptr),
+      d_epg(pnm ? new EagerProofGenerator(pnm, userContext(), "") : nullptr),
       d_factLiteralCache(context()),
       d_literalFactCache(context()),
       d_propagate(options().bv.bitvectorPropagate),
diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h
index ba3e3ea66..79b5c04ad 100644
--- a/src/theory/bv/int_blaster.h
+++ b/src/theory/bv/int_blaster.h
@@ -368,7 +368,6 @@ class IntBlaster : protected EnvObj
 
   /** an SolverEngine for context */
   context::Context* d_context;
-
 };
 
 }  // namespace cvc5::internal
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 798e8690b..39ca10868 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -39,7 +39,7 @@
 
 using namespace cvc5::internal;
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::theory;
 using namespace cvc5::internal::theory::datatypes;
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 8bbd179c7..6ff5261ff 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -43,7 +43,7 @@
 
 using namespace std;
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
@@ -680,9 +680,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
 }
 
 TheoryDatatypes::EqcInfo::EqcInfo(context::Context* c)
-    : d_inst(c, false),
-      d_constructor(c, Node::null()),
-      d_selectors(c, false)
+    : d_inst(c, false), d_constructor(c, Node::null()), d_selectors(c, false)
 {}
 
 bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 284c13c92..a54ea6275 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -78,14 +78,14 @@ private:
   class EqcInfo
   {
   public:
-    EqcInfo( context::Context* c );
-    ~EqcInfo(){}
-    //whether we have instantiatied this eqc
-    context::CDO< bool > d_inst;
-    //constructor equal to this eqc
-    context::CDO< Node > d_constructor;
-    //all selectors whose argument is this eqc
-    context::CDO< bool > d_selectors;
+   EqcInfo(context::Context* c);
+   ~EqcInfo() {}
+   // whether we have instantiatied this eqc
+   context::CDO<bool> d_inst;
+   // constructor equal to this eqc
+   context::CDO<Node> d_constructor;
+   // all selectors whose argument is this eqc
+   context::CDO<bool> d_selectors;
   };
   /** does eqc of n have a label (do we know its constructor)? */
   bool hasLabel( EqcInfo* eqc, Node n );
diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h
index 732cbb5ec..bcf956088 100644
--- a/src/theory/engine_output_channel.h
+++ b/src/theory/engine_output_channel.h
@@ -41,7 +41,7 @@ class Theory;
  */
 class EngineOutputChannel : public theory::OutputChannel
 {
-  friend class TheoryEngine;
+  friend class internal::TheoryEngine;
 
  public:
   EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory);
diff --git a/src/theory/fp/fp_word_blaster.cpp b/src/theory/fp/fp_word_blaster.cpp
index aead0414e..97ee04c3d 100644
--- a/src/theory/fp/fp_word_blaster.cpp
+++ b/src/theory/fp/fp_word_blaster.cpp
@@ -38,76 +38,81 @@
 #include "util/floatingpoint_literal_symfpu.h"
 
 namespace symfpu {
-using namespace ::cvc5::internal::theory::fp::symfpuSymbolic;
-
-#define CVC5_SYM_ITE_DFN(T)                                                \
-  template <>                                                              \
-  struct ite<symbolicProposition, T>                                       \
-  {                                                                        \
-    static const T iteOp(const symbolicProposition& _cond,                 \
-                         const T& _l,                                      \
-                         const T& _r)                                      \
-    {                                                                      \
-      ::cvc5::internal::NodeManager* nm = ::cvc5::internal::NodeManager::currentNM();          \
-                                                                           \
-      ::cvc5::internal::Node cond = _cond;                                           \
-      ::cvc5::internal::Node l = _l;                                                 \
-      ::cvc5::internal::Node r = _r;                                                 \
-                                                                           \
-      /* Handle some common symfpu idioms */                               \
-      if (cond.isConst())                                                  \
-      {                                                                    \
-        return (cond == nm->mkConst(::cvc5::internal::BitVector(1U, 1U))) ? l : r;   \
-      }                                                                    \
-      else                                                                 \
-      {                                                                    \
-        if (l.getKind() == ::cvc5::internal::kind::BITVECTOR_ITE)                    \
-        {                                                                  \
-          if (l[1] == r)                                                   \
-          {                                                                \
-            return nm->mkNode(                                             \
-                ::cvc5::internal::kind::BITVECTOR_ITE,                               \
-                nm->mkNode(::cvc5::internal::kind::BITVECTOR_AND,                    \
-                           cond,                                           \
-                           nm->mkNode(::cvc5::internal::kind::BITVECTOR_NOT, l[0])), \
-                l[2],                                                      \
-                r);                                                        \
-          }                                                                \
-          else if (l[2] == r)                                              \
-          {                                                                \
-            return nm->mkNode(                                             \
-                ::cvc5::internal::kind::BITVECTOR_ITE,                               \
-                nm->mkNode(::cvc5::internal::kind::BITVECTOR_AND, cond, l[0]),       \
-                l[1],                                                      \
-                r);                                                        \
-          }                                                                \
-        }                                                                  \
-        else if (r.getKind() == ::cvc5::internal::kind::BITVECTOR_ITE)               \
-        {                                                                  \
-          if (r[1] == l)                                                   \
-          {                                                                \
-            return nm->mkNode(                                             \
-                ::cvc5::internal::kind::BITVECTOR_ITE,                               \
-                nm->mkNode(::cvc5::internal::kind::BITVECTOR_AND,                    \
-                           nm->mkNode(::cvc5::internal::kind::BITVECTOR_NOT, cond),  \
-                           nm->mkNode(::cvc5::internal::kind::BITVECTOR_NOT, r[0])), \
-                r[2],                                                      \
-                l);                                                        \
-          }                                                                \
-          else if (r[2] == l)                                              \
-          {                                                                \
-            return nm->mkNode(                                             \
-                ::cvc5::internal::kind::BITVECTOR_ITE,                               \
-                nm->mkNode(::cvc5::internal::kind::BITVECTOR_AND,                    \
-                           nm->mkNode(::cvc5::internal::kind::BITVECTOR_NOT, cond),  \
-                           r[0]),                                          \
-                r[1],                                                      \
-                l);                                                        \
-          }                                                                \
-        }                                                                  \
-      }                                                                    \
-      return T(nm->mkNode(::cvc5::internal::kind::BITVECTOR_ITE, cond, l, r));       \
-    }                                                                      \
+using namespace cvc5::internal::theory::fp::symfpuSymbolic;
+
+#define CVC5_SYM_ITE_DFN(T)                                                  \
+  template <>                                                                \
+  struct ite<symbolicProposition, T>                                         \
+  {                                                                          \
+    static const T iteOp(const symbolicProposition& _cond,                   \
+                         const T& _l,                                        \
+                         const T& _r)                                        \
+    {                                                                        \
+      cvc5::internal::NodeManager* nm =                                      \
+          cvc5::internal::NodeManager::currentNM();                          \
+                                                                             \
+      cvc5::internal::Node cond = _cond;                                     \
+      cvc5::internal::Node l = _l;                                           \
+      cvc5::internal::Node r = _r;                                           \
+                                                                             \
+      /* Handle some common symfpu idioms */                                 \
+      if (cond.isConst())                                                    \
+      {                                                                      \
+        return (cond == nm->mkConst(cvc5::internal::BitVector(1U, 1U))) ? l  \
+                                                                        : r; \
+      }                                                                      \
+      else                                                                   \
+      {                                                                      \
+        if (l.getKind() == cvc5::internal::kind::BITVECTOR_ITE)              \
+        {                                                                    \
+          if (l[1] == r)                                                     \
+          {                                                                  \
+            return nm->mkNode(                                               \
+                cvc5::internal::kind::BITVECTOR_ITE,                         \
+                nm->mkNode(                                                  \
+                    cvc5::internal::kind::BITVECTOR_AND,                     \
+                    cond,                                                    \
+                    nm->mkNode(cvc5::internal::kind::BITVECTOR_NOT, l[0])),  \
+                l[2],                                                        \
+                r);                                                          \
+          }                                                                  \
+          else if (l[2] == r)                                                \
+          {                                                                  \
+            return nm->mkNode(                                               \
+                cvc5::internal::kind::BITVECTOR_ITE,                         \
+                nm->mkNode(cvc5::internal::kind::BITVECTOR_AND, cond, l[0]), \
+                l[1],                                                        \
+                r);                                                          \
+          }                                                                  \
+        }                                                                    \
+        else if (r.getKind() == cvc5::internal::kind::BITVECTOR_ITE)         \
+        {                                                                    \
+          if (r[1] == l)                                                     \
+          {                                                                  \
+            return nm->mkNode(                                               \
+                cvc5::internal::kind::BITVECTOR_ITE,                         \
+                nm->mkNode(                                                  \
+                    cvc5::internal::kind::BITVECTOR_AND,                     \
+                    nm->mkNode(cvc5::internal::kind::BITVECTOR_NOT, cond),   \
+                    nm->mkNode(cvc5::internal::kind::BITVECTOR_NOT, r[0])),  \
+                r[2],                                                        \
+                l);                                                          \
+          }                                                                  \
+          else if (r[2] == l)                                                \
+          {                                                                  \
+            return nm->mkNode(                                               \
+                cvc5::internal::kind::BITVECTOR_ITE,                         \
+                nm->mkNode(                                                  \
+                    cvc5::internal::kind::BITVECTOR_AND,                     \
+                    nm->mkNode(cvc5::internal::kind::BITVECTOR_NOT, cond),   \
+                    r[0]),                                                   \
+                r[1],                                                        \
+                l);                                                          \
+          }                                                                  \
+        }                                                                    \
+      }                                                                      \
+      return T(nm->mkNode(cvc5::internal::kind::BITVECTOR_ITE, cond, l, r)); \
+    }                                                                        \
   }
 
 // Can (unsurprisingly) only ITE things which contain Nodes
@@ -391,8 +396,9 @@ symbolicBitVector<true> symbolicBitVector<true>::maxValue(const bwt& w)
   symbolicBitVector<true> leadingZero(symbolicBitVector<true>::zero(1));
   symbolicBitVector<true> base(symbolicBitVector<true>::allOnes(w - 1));
 
-  return symbolicBitVector<true>(::cvc5::internal::NodeManager::currentNM()->mkNode(
-      ::cvc5::internal::kind::BITVECTOR_CONCAT, leadingZero, base));
+  return symbolicBitVector<true>(
+      cvc5::internal::NodeManager::currentNM()->mkNode(
+          cvc5::internal::kind::BITVECTOR_CONCAT, leadingZero, base));
 }
 
 template <>
@@ -407,8 +413,9 @@ symbolicBitVector<true> symbolicBitVector<true>::minValue(const bwt& w)
   symbolicBitVector<true> leadingOne(symbolicBitVector<true>::one(1));
   symbolicBitVector<true> base(symbolicBitVector<true>::zero(w - 1));
 
-  return symbolicBitVector<true>(::cvc5::internal::NodeManager::currentNM()->mkNode(
-      ::cvc5::internal::kind::BITVECTOR_CONCAT, leadingOne, base));
+  return symbolicBitVector<true>(
+      cvc5::internal::NodeManager::currentNM()->mkNode(
+          cvc5::internal::kind::BITVECTOR_CONCAT, leadingOne, base));
 }
 
 template <>
@@ -793,8 +800,8 @@ Node FpWordBlaster::rmToNode(const rm& r) const
 Node FpWordBlaster::propToNode(const prop& p) const
 {
   NodeManager* nm = NodeManager::currentNM();
-  Node value =
-      nm->mkNode(kind::EQUAL, p, nm->mkConst(::cvc5::internal::BitVector(1U, 1U)));
+  Node value = nm->mkNode(
+      kind::EQUAL, p, nm->mkConst(cvc5::internal::BitVector(1U, 1U)));
   return value;
 }
 Node FpWordBlaster::ubvToNode(const ubv& u) const { return u; }
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index ac6f1072c..d52fd4084 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -430,7 +430,8 @@ void TheoryFp::wordBlastAndEquateTerm(TNode node)
     NodeManager* nm = NodeManager::currentNM();
 
     handleLemma(
-        nm->mkNode(kind::EQUAL, addA, nm->mkConst(::cvc5::internal::BitVector(1U, 1U))),
+        nm->mkNode(
+            kind::EQUAL, addA, nm->mkConst(cvc5::internal::BitVector(1U, 1U))),
         InferenceId::FP_EQUATE_TERM);
 
     ++oldSize;
@@ -447,11 +448,12 @@ void TheoryFp::wordBlastAndEquateTerm(TNode node)
       NodeManager* nm = NodeManager::currentNM();
 
       handleLemma(
-          nm->mkNode(kind::EQUAL,
-                     node,
-                     nm->mkNode(kind::EQUAL,
-                                wordBlasted,
-                                nm->mkConst(::cvc5::internal::BitVector(1U, 1U)))),
+          nm->mkNode(
+              kind::EQUAL,
+              node,
+              nm->mkNode(kind::EQUAL,
+                         wordBlasted,
+                         nm->mkConst(cvc5::internal::BitVector(1U, 1U)))),
           InferenceId::FP_EQUATE_TERM);
     }
     else
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 007bbebb1..9ffc185fc 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -1076,275 +1076,280 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
   /**
    * Initialize the rewriter.
    */
-TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u)
-{
-  /* Set up the pre-rewrite dispatch table */
-  for (uint32_t i = 0; i < kind::LAST_KIND; ++i)
+  TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u)
   {
-    d_preRewriteTable[i] = rewrite::notFP;
-  }
+    /* Set up the pre-rewrite dispatch table */
+    for (uint32_t i = 0; i < kind::LAST_KIND; ++i)
+    {
+      d_preRewriteTable[i] = rewrite::notFP;
+    }
 
-  /******** Constants ********/
-  /* No rewriting possible for constants */
-  d_preRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
-  d_preRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
-
-  /******** Sorts(?) ********/
-  /* These kinds should only appear in types */
-  // d_preRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type;
-  d_preRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
-
-  /******** Operations ********/
-  d_preRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::compactAbs;
-  d_preRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation;
-  d_preRewriteTable[kind::FLOATINGPOINT_ADD] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_SUB] =
-      rewrite::convertSubtractionToAddition;
-  d_preRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
-  d_preRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
-  d_preRewriteTable[kind::FLOATINGPOINT_MIN_TOTAL] = rewrite::compactMinMax;
-  d_preRewriteTable[kind::FLOATINGPOINT_MAX_TOTAL] = rewrite::compactMinMax;
-
-  /******** Comparisons ********/
-  d_preRewriteTable[kind::FLOATINGPOINT_EQ] =
-      rewrite::then<rewrite::breakChain, rewrite::ieeeEqToEq>;
-  d_preRewriteTable[kind::FLOATINGPOINT_LEQ] =
-      rewrite::then<rewrite::breakChain, rewrite::leqId>;
-  d_preRewriteTable[kind::FLOATINGPOINT_LT] =
-      rewrite::then<rewrite::breakChain, rewrite::ltId>;
-  d_preRewriteTable[kind::FLOATINGPOINT_GEQ] =
-      rewrite::then<rewrite::breakChain, rewrite::geqToleq>;
-  d_preRewriteTable[kind::FLOATINGPOINT_GT] =
-      rewrite::then<rewrite::breakChain, rewrite::gtTolt>;
-
-  /******** Classifications ********/
-  d_preRewriteTable[kind::FLOATINGPOINT_IS_NORMAL] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_IS_SUBNORMAL] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_IS_ZERO] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_IS_INF] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_IS_NAN] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_IS_NEG] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity;
-
-  /******** Conversions ********/
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] = rewrite::identity;
-
-  /******** Variables ********/
-  d_preRewriteTable[kind::VARIABLE] = rewrite::variable;
-  d_preRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
-  d_preRewriteTable[kind::SKOLEM] = rewrite::variable;
-  d_preRewriteTable[kind::INST_CONSTANT] = rewrite::variable;
-
-  d_preRewriteTable[kind::EQUAL] = rewrite::equal;
-
-  /******** Components for bit-blasting ********/
-  d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_NAN] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_INF] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] =
-      rewrite::identity;
-  d_preRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity;
-
-  /* Set up the post-rewrite dispatch table */
-  for (uint32_t i = 0; i < kind::LAST_KIND; ++i)
-  {
-    d_postRewriteTable[i] = rewrite::notFP;
-  }
+    /******** Constants ********/
+    /* No rewriting possible for constants */
+    d_preRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
+    d_preRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
+
+    /******** Sorts(?) ********/
+    /* These kinds should only appear in types */
+    // d_preRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type;
+    d_preRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
+
+    /******** Operations ********/
+    d_preRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::compactAbs;
+    d_preRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation;
+    d_preRewriteTable[kind::FLOATINGPOINT_ADD] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_SUB] =
+        rewrite::convertSubtractionToAddition;
+    d_preRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
+    d_preRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
+    d_preRewriteTable[kind::FLOATINGPOINT_MIN_TOTAL] = rewrite::compactMinMax;
+    d_preRewriteTable[kind::FLOATINGPOINT_MAX_TOTAL] = rewrite::compactMinMax;
+
+    /******** Comparisons ********/
+    d_preRewriteTable[kind::FLOATINGPOINT_EQ] =
+        rewrite::then<rewrite::breakChain, rewrite::ieeeEqToEq>;
+    d_preRewriteTable[kind::FLOATINGPOINT_LEQ] =
+        rewrite::then<rewrite::breakChain, rewrite::leqId>;
+    d_preRewriteTable[kind::FLOATINGPOINT_LT] =
+        rewrite::then<rewrite::breakChain, rewrite::ltId>;
+    d_preRewriteTable[kind::FLOATINGPOINT_GEQ] =
+        rewrite::then<rewrite::breakChain, rewrite::geqToleq>;
+    d_preRewriteTable[kind::FLOATINGPOINT_GT] =
+        rewrite::then<rewrite::breakChain, rewrite::gtTolt>;
+
+    /******** Classifications ********/
+    d_preRewriteTable[kind::FLOATINGPOINT_IS_NORMAL] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_IS_SUBNORMAL] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_IS_ZERO] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_IS_INF] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_IS_NAN] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_IS_NEG] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity;
+
+    /******** Conversions ********/
+    d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] =
+        rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] = rewrite::identity;
+
+    /******** Variables ********/
+    d_preRewriteTable[kind::VARIABLE] = rewrite::variable;
+    d_preRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
+    d_preRewriteTable[kind::SKOLEM] = rewrite::variable;
+    d_preRewriteTable[kind::INST_CONSTANT] = rewrite::variable;
+
+    d_preRewriteTable[kind::EQUAL] = rewrite::equal;
+
+    /******** Components for bit-blasting ********/
+    d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_NAN] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_INF] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] =
+        rewrite::identity;
+    d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] =
+        rewrite::identity;
+    d_preRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity;
+
+    /* Set up the post-rewrite dispatch table */
+    for (uint32_t i = 0; i < kind::LAST_KIND; ++i)
+    {
+      d_postRewriteTable[i] = rewrite::notFP;
+    }
 
-  /******** Constants ********/
-  /* No rewriting possible for constants */
-  d_postRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
-  d_postRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
-
-  /******** Sorts(?) ********/
-  /* These kinds should only appear in types */
-  // d_postRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type;
-  d_postRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
-
-  /******** Operations ********/
-  d_postRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::compactAbs;
-  d_postRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation;
-  d_postRewriteTable[kind::FLOATINGPOINT_ADD] = rewrite::reorderBinaryOperation;
-  d_postRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_MULT] =
-      rewrite::reorderBinaryOperation;
-  d_postRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::reorderFMA;
-  d_postRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::compactRemainder;
-  d_postRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
-  d_postRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
-  d_postRewriteTable[kind::FLOATINGPOINT_MIN_TOTAL] = rewrite::compactMinMax;
-  d_postRewriteTable[kind::FLOATINGPOINT_MAX_TOTAL] = rewrite::compactMinMax;
-
-  /******** Comparisons ********/
-  d_postRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::leqId;
-  d_postRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::ltId;
-  d_postRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::identity;
-
-  /******** Classifications ********/
-  d_postRewriteTable[kind::FLOATINGPOINT_IS_NORMAL] =
-      rewrite::removeSignOperations;
-  d_postRewriteTable[kind::FLOATINGPOINT_IS_SUBNORMAL] =
-      rewrite::removeSignOperations;
-  d_postRewriteTable[kind::FLOATINGPOINT_IS_ZERO] =
-      rewrite::removeSignOperations;
-  d_postRewriteTable[kind::FLOATINGPOINT_IS_INF] =
-      rewrite::removeSignOperations;
-  d_postRewriteTable[kind::FLOATINGPOINT_IS_NAN] =
-      rewrite::removeSignOperations;
-  d_postRewriteTable[kind::FLOATINGPOINT_IS_NEG] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity;
-
-  /******** Conversions ********/
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] =
-      rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] =
-      rewrite::toFPSignedBV;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] = rewrite::identity;
-
-  /******** Variables ********/
-  d_postRewriteTable[kind::VARIABLE] = rewrite::variable;
-  d_postRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
-  d_postRewriteTable[kind::SKOLEM] = rewrite::variable;
-  d_postRewriteTable[kind::INST_CONSTANT] = rewrite::variable;
-
-  d_postRewriteTable[kind::EQUAL] = rewrite::equal;
-
-  /******** Components for bit-blasting ********/
-  d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_NAN] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_INF] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] =
-      rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] =
-      rewrite::identity;
-  d_postRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity;
-
-  /* Set up the post-rewrite constant fold table */
-  for (uint32_t i = 0; i < kind::LAST_KIND; ++i)
-  {
-    // Note that this is identity, not notFP
-    // Constant folding is called after post-rewrite
-    // So may have to deal with cases of things being
-    // re-written to non-floating-point sorts (i.e. true).
-    d_constantFoldTable[i] = rewrite::identity;
-  }
+    /******** Constants ********/
+    /* No rewriting possible for constants */
+    d_postRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
+    d_postRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
+
+    /******** Sorts(?) ********/
+    /* These kinds should only appear in types */
+    // d_postRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type;
+    d_postRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
+
+    /******** Operations ********/
+    d_postRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::compactAbs;
+    d_postRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation;
+    d_postRewriteTable[kind::FLOATINGPOINT_ADD] =
+        rewrite::reorderBinaryOperation;
+    d_postRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_MULT] =
+        rewrite::reorderBinaryOperation;
+    d_postRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::reorderFMA;
+    d_postRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::compactRemainder;
+    d_postRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
+    d_postRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
+    d_postRewriteTable[kind::FLOATINGPOINT_MIN_TOTAL] = rewrite::compactMinMax;
+    d_postRewriteTable[kind::FLOATINGPOINT_MAX_TOTAL] = rewrite::compactMinMax;
+
+    /******** Comparisons ********/
+    d_postRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::leqId;
+    d_postRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::ltId;
+    d_postRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::identity;
+
+    /******** Classifications ********/
+    d_postRewriteTable[kind::FLOATINGPOINT_IS_NORMAL] =
+        rewrite::removeSignOperations;
+    d_postRewriteTable[kind::FLOATINGPOINT_IS_SUBNORMAL] =
+        rewrite::removeSignOperations;
+    d_postRewriteTable[kind::FLOATINGPOINT_IS_ZERO] =
+        rewrite::removeSignOperations;
+    d_postRewriteTable[kind::FLOATINGPOINT_IS_INF] =
+        rewrite::removeSignOperations;
+    d_postRewriteTable[kind::FLOATINGPOINT_IS_NAN] =
+        rewrite::removeSignOperations;
+    d_postRewriteTable[kind::FLOATINGPOINT_IS_NEG] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity;
+
+    /******** Conversions ********/
+    d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] =
+        rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] =
+        rewrite::toFPSignedBV;
+    d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] = rewrite::identity;
+
+    /******** Variables ********/
+    d_postRewriteTable[kind::VARIABLE] = rewrite::variable;
+    d_postRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
+    d_postRewriteTable[kind::SKOLEM] = rewrite::variable;
+    d_postRewriteTable[kind::INST_CONSTANT] = rewrite::variable;
+
+    d_postRewriteTable[kind::EQUAL] = rewrite::equal;
+
+    /******** Components for bit-blasting ********/
+    d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_NAN] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_INF] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] =
+        rewrite::identity;
+    d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] =
+        rewrite::identity;
+    d_postRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity;
+
+    /* Set up the post-rewrite constant fold table */
+    for (uint32_t i = 0; i < kind::LAST_KIND; ++i)
+    {
+      // Note that this is identity, not notFP
+      // Constant folding is called after post-rewrite
+      // So may have to deal with cases of things being
+      // re-written to non-floating-point sorts (i.e. true).
+      d_constantFoldTable[i] = rewrite::identity;
+    }
 
-  /******** Constants ********/
-  /* Already folded! */
-  d_constantFoldTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
-  d_constantFoldTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
-
-  /******** Sorts(?) ********/
-  /* These kinds should only appear in types */
-  d_constantFoldTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
-
-  /******** Operations ********/
-  d_constantFoldTable[kind::FLOATINGPOINT_FP] = constantFold::fpLiteral;
-  d_constantFoldTable[kind::FLOATINGPOINT_ABS] = constantFold::abs;
-  d_constantFoldTable[kind::FLOATINGPOINT_NEG] = constantFold::neg;
-  d_constantFoldTable[kind::FLOATINGPOINT_ADD] = constantFold::add;
-  d_constantFoldTable[kind::FLOATINGPOINT_MULT] = constantFold::mult;
-  d_constantFoldTable[kind::FLOATINGPOINT_DIV] = constantFold::div;
-  d_constantFoldTable[kind::FLOATINGPOINT_FMA] = constantFold::fma;
-  d_constantFoldTable[kind::FLOATINGPOINT_SQRT] = constantFold::sqrt;
-  d_constantFoldTable[kind::FLOATINGPOINT_REM] = constantFold::rem;
-  d_constantFoldTable[kind::FLOATINGPOINT_RTI] = constantFold::rti;
-  d_constantFoldTable[kind::FLOATINGPOINT_MIN] = constantFold::min;
-  d_constantFoldTable[kind::FLOATINGPOINT_MAX] = constantFold::max;
-  d_constantFoldTable[kind::FLOATINGPOINT_MIN_TOTAL] = constantFold::minTotal;
-  d_constantFoldTable[kind::FLOATINGPOINT_MAX_TOTAL] = constantFold::maxTotal;
-
-  /******** Comparisons ********/
-  d_constantFoldTable[kind::FLOATINGPOINT_LEQ] = constantFold::leq;
-  d_constantFoldTable[kind::FLOATINGPOINT_LT] = constantFold::lt;
-
-  /******** Classifications ********/
-  d_constantFoldTable[kind::FLOATINGPOINT_IS_NORMAL] = constantFold::isNormal;
-  d_constantFoldTable[kind::FLOATINGPOINT_IS_SUBNORMAL] =
-      constantFold::isSubnormal;
-  d_constantFoldTable[kind::FLOATINGPOINT_IS_ZERO] = constantFold::isZero;
-  d_constantFoldTable[kind::FLOATINGPOINT_IS_INF] = constantFold::isInfinite;
-  d_constantFoldTable[kind::FLOATINGPOINT_IS_NAN] = constantFold::isNaN;
-  d_constantFoldTable[kind::FLOATINGPOINT_IS_NEG] = constantFold::isNegative;
-  d_constantFoldTable[kind::FLOATINGPOINT_IS_POS] = constantFold::isPositive;
-
-  /******** Conversions ********/
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] =
-      constantFold::convertFromIEEEBitVectorLiteral;
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] =
-      constantFold::constantConvert;
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] =
-      constantFold::convertFromRealLiteral;
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] =
-      constantFold::convertFromSBV;
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] =
-      constantFold::convertFromUBV;
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_UBV] = constantFold::convertToUBV;
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_SBV] = constantFold::convertToSBV;
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_REAL] =
-      constantFold::convertToReal;
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] =
-      constantFold::convertToUBVTotal;
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] =
-      constantFold::convertToSBVTotal;
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] =
-      constantFold::convertToRealTotal;
-
-  /******** Variables ********/
-  d_constantFoldTable[kind::VARIABLE] = rewrite::variable;
-  d_constantFoldTable[kind::BOUND_VARIABLE] = rewrite::variable;
-
-  d_constantFoldTable[kind::EQUAL] = constantFold::equal;
-
-  /******** Components for bit-blasting ********/
-  d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_NAN] =
-      constantFold::componentFlag;
-  d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_INF] =
-      constantFold::componentFlag;
-  d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_ZERO] =
-      constantFold::componentFlag;
-  d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_SIGN] =
-      constantFold::componentFlag;
-  d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] =
-      constantFold::componentExponent;
-  d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] =
-      constantFold::componentSignificand;
-  d_constantFoldTable[kind::ROUNDINGMODE_BITBLAST] =
-      constantFold::roundingModeBitBlast;
+    /******** Constants ********/
+    /* Already folded! */
+    d_constantFoldTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
+    d_constantFoldTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
+
+    /******** Sorts(?) ********/
+    /* These kinds should only appear in types */
+    d_constantFoldTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
+
+    /******** Operations ********/
+    d_constantFoldTable[kind::FLOATINGPOINT_FP] = constantFold::fpLiteral;
+    d_constantFoldTable[kind::FLOATINGPOINT_ABS] = constantFold::abs;
+    d_constantFoldTable[kind::FLOATINGPOINT_NEG] = constantFold::neg;
+    d_constantFoldTable[kind::FLOATINGPOINT_ADD] = constantFold::add;
+    d_constantFoldTable[kind::FLOATINGPOINT_MULT] = constantFold::mult;
+    d_constantFoldTable[kind::FLOATINGPOINT_DIV] = constantFold::div;
+    d_constantFoldTable[kind::FLOATINGPOINT_FMA] = constantFold::fma;
+    d_constantFoldTable[kind::FLOATINGPOINT_SQRT] = constantFold::sqrt;
+    d_constantFoldTable[kind::FLOATINGPOINT_REM] = constantFold::rem;
+    d_constantFoldTable[kind::FLOATINGPOINT_RTI] = constantFold::rti;
+    d_constantFoldTable[kind::FLOATINGPOINT_MIN] = constantFold::min;
+    d_constantFoldTable[kind::FLOATINGPOINT_MAX] = constantFold::max;
+    d_constantFoldTable[kind::FLOATINGPOINT_MIN_TOTAL] = constantFold::minTotal;
+    d_constantFoldTable[kind::FLOATINGPOINT_MAX_TOTAL] = constantFold::maxTotal;
+
+    /******** Comparisons ********/
+    d_constantFoldTable[kind::FLOATINGPOINT_LEQ] = constantFold::leq;
+    d_constantFoldTable[kind::FLOATINGPOINT_LT] = constantFold::lt;
+
+    /******** Classifications ********/
+    d_constantFoldTable[kind::FLOATINGPOINT_IS_NORMAL] = constantFold::isNormal;
+    d_constantFoldTable[kind::FLOATINGPOINT_IS_SUBNORMAL] =
+        constantFold::isSubnormal;
+    d_constantFoldTable[kind::FLOATINGPOINT_IS_ZERO] = constantFold::isZero;
+    d_constantFoldTable[kind::FLOATINGPOINT_IS_INF] = constantFold::isInfinite;
+    d_constantFoldTable[kind::FLOATINGPOINT_IS_NAN] = constantFold::isNaN;
+    d_constantFoldTable[kind::FLOATINGPOINT_IS_NEG] = constantFold::isNegative;
+    d_constantFoldTable[kind::FLOATINGPOINT_IS_POS] = constantFold::isPositive;
+
+    /******** Conversions ********/
+    d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] =
+        constantFold::convertFromIEEEBitVectorLiteral;
+    d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] =
+        constantFold::constantConvert;
+    d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] =
+        constantFold::convertFromRealLiteral;
+    d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] =
+        constantFold::convertFromSBV;
+    d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] =
+        constantFold::convertFromUBV;
+    d_constantFoldTable[kind::FLOATINGPOINT_TO_UBV] =
+        constantFold::convertToUBV;
+    d_constantFoldTable[kind::FLOATINGPOINT_TO_SBV] =
+        constantFold::convertToSBV;
+    d_constantFoldTable[kind::FLOATINGPOINT_TO_REAL] =
+        constantFold::convertToReal;
+    d_constantFoldTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] =
+        constantFold::convertToUBVTotal;
+    d_constantFoldTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] =
+        constantFold::convertToSBVTotal;
+    d_constantFoldTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] =
+        constantFold::convertToRealTotal;
+
+    /******** Variables ********/
+    d_constantFoldTable[kind::VARIABLE] = rewrite::variable;
+    d_constantFoldTable[kind::BOUND_VARIABLE] = rewrite::variable;
+
+    d_constantFoldTable[kind::EQUAL] = constantFold::equal;
+
+    /******** Components for bit-blasting ********/
+    d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_NAN] =
+        constantFold::componentFlag;
+    d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_INF] =
+        constantFold::componentFlag;
+    d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_ZERO] =
+        constantFold::componentFlag;
+    d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_SIGN] =
+        constantFold::componentFlag;
+    d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] =
+        constantFold::componentExponent;
+    d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] =
+        constantFold::componentSignificand;
+    d_constantFoldTable[kind::ROUNDINGMODE_BITBLAST] =
+        constantFold::roundingModeBitBlast;
 }
 
   /**
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 88012ff49..7dd27f980 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -27,7 +27,7 @@
 
 using namespace std;
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index 0b94bdc37..af2beff4b 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -27,7 +27,7 @@
 
 using namespace std;
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 32d1111b0..f2c10a9fa 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -29,7 +29,7 @@
 
 using namespace std;
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 9751518db..bee9ee597 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -157,9 +157,9 @@ void ConjectureGenerator::eqNotifyMerge(TNode t1, TNode t2)
   }
 }
 
-
-ConjectureGenerator::EqcInfo::EqcInfo( context::Context* c ) : d_rep( c, Node::null() ){
-
+ConjectureGenerator::EqcInfo::EqcInfo(context::Context* c)
+    : d_rep(c, Node::null())
+{
 }
 
 ConjectureGenerator::EqcInfo* ConjectureGenerator::getOrMakeEqcInfo( TNode n, bool doMake ) {
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index bf7eface5..473391380 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -274,9 +274,9 @@ class ConjectureGenerator : public QuantifiersModule
   NotifyClass d_notify;
   class EqcInfo{
   public:
-    EqcInfo( context::Context* c );
-    //representative
-    context::CDO< Node > d_rep;
+   EqcInfo(context::Context* c);
+   // representative
+   context::CDO<Node> d_rep;
   };
   /** get or make eqc info */
   EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 1993e81c7..964af97b6 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -25,7 +25,7 @@
 #include "theory/quantifiers/term_util.h"
 
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::theory::quantifiers::inst;
 
 namespace cvc5::internal {
diff --git a/src/theory/quantifiers/entailment_check.cpp b/src/theory/quantifiers/entailment_check.cpp
index d79f4a641..c73074361 100644
--- a/src/theory/quantifiers/entailment_check.cpp
+++ b/src/theory/quantifiers/entailment_check.cpp
@@ -19,7 +19,7 @@
 #include "theory/quantifiers/term_database.h"
 
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index ac58a4d9f..441786b5f 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -23,7 +23,7 @@
 
 using namespace std;
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index ab54e7c52..c36901413 100644
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -74,7 +74,7 @@ class EqualityQuery : public QuantifiersUtil
   /** Pointer to the model */
   FirstOrderModel* d_model;
   /** quantifiers equality inference */
-  context::CDO< unsigned > d_eqi_counter;
+  context::CDO<unsigned> d_eqi_counter;
   /** internal representatives */
   std::map< TypeNode, std::map< Node, Node > > d_int_rep;
   /** rep score */
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 57be2d8d4..53dbd67f6 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -25,7 +25,7 @@
 #include "theory/quantifiers/term_util.h"
 
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 43254103b..8a5705bcf 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -51,7 +51,8 @@ class BoundedIntegers : public QuantifiersModule
   typedef context::CDHashMap<Node, int> NodeIntMap;
   typedef context::CDHashMap<Node, Node> NodeNodeMap;
   typedef context::CDHashMap<int, bool> IntBoolMap;
-private:
+
+ private:
   //for determining bounds
   bool hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited );
   bool hasNonBoundVar( Node f, Node b );
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 27d49bc46..a69630a00 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -32,7 +32,7 @@
 #include "theory/rewriter.h"
 
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 0bf6b4a78..7c5cd90a5 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -26,7 +26,7 @@
 using namespace std;
 using namespace cvc5::internal;
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::theory;
 using namespace cvc5::internal::theory::quantifiers;
 
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 2c4db6ae7..ff61df74f 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -24,7 +24,7 @@
 #include "theory/quantifiers/term_database.h"
 
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp
index b56637f14..2a6fa4394 100644
--- a/src/theory/quantifiers/inst_match_trie.cpp
+++ b/src/theory/quantifiers/inst_match_trie.cpp
@@ -21,7 +21,7 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/uf/equality_engine_iterator.h"
 
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index edcc0efca..c946731d0 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -23,7 +23,7 @@
 #include "theory/quantifiers/term_util.h"
 
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/inst_strategy_pool.cpp b/src/theory/quantifiers/inst_strategy_pool.cpp
index a0c592765..c03823ea5 100644
--- a/src/theory/quantifiers/inst_strategy_pool.cpp
+++ b/src/theory/quantifiers/inst_strategy_pool.cpp
@@ -24,7 +24,7 @@
 #include "theory/quantifiers/term_tuple_enumerator.h"
 
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index a9cb1140a..958daa878 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -36,7 +36,7 @@
 #include "theory/rewriter.h"
 
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/quant_relevance.cpp b/src/theory/quantifiers/quant_relevance.cpp
index 0e146ce20..be658147d 100644
--- a/src/theory/quantifiers/quant_relevance.cpp
+++ b/src/theory/quantifiers/quant_relevance.cpp
@@ -17,7 +17,7 @@
 
 using namespace std;
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 3988da8c9..c69ffb6de 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -27,7 +27,7 @@
 
 using namespace std;
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h
index d4285f4e3..a61fcb485 100644
--- a/src/theory/quantifiers/quantifiers_modules.h
+++ b/src/theory/quantifiers/quantifiers_modules.h
@@ -47,7 +47,7 @@ namespace quantifiers {
  */
 class QuantifiersModules
 {
-  friend class ::cvc5::internal::theory::QuantifiersEngine;
+  friend class theory::QuantifiersEngine;
 
  public:
   QuantifiersModules();
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 4bf8e528e..c87667525 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -37,7 +37,7 @@
 
 using namespace std;
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index ac41dbbff..e5f888093 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -26,7 +26,7 @@
 
 using namespace std;
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index 6a82c60e2..d0994bf22 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -24,7 +24,7 @@
 
 using namespace std;
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 87d147e94..6b3d9fe10 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -31,7 +31,7 @@
 #include "theory/uf/equality_engine.h"
 
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 900adb6b1..b1252b787 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -24,7 +24,7 @@
 #include "theory/valuation.h"
 
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index bac943b15..be462e60b 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -57,7 +57,7 @@ class TermRegistry;
  */
 class QuantifiersEngine : protected EnvObj
 {
-  friend class ::cvc5::internal::TheoryEngine;
+  friend class internal::TheoryEngine;
   typedef context::CDHashMap<Node, bool> BoolMap;
   typedef context::CDHashSet<Node> NodeSet;
 
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index df161616a..48da252b3 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -922,9 +922,9 @@ void TheorySep::conflict(TNode a, TNode b) {
   d_im.conflictEqConstantMerge(a, b);
 }
 
-
-TheorySep::HeapAssertInfo::HeapAssertInfo( context::Context* c ) : d_pto(c), d_has_neg_pto(c,false) {
-
+TheorySep::HeapAssertInfo::HeapAssertInfo(context::Context* c)
+    : d_pto(c), d_has_neg_pto(c, false)
+{
 }
 
 TheorySep::HeapAssertInfo * TheorySep::getOrMakeEqcInfo( Node n, bool doMake ) {
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index f3371dd6a..a2ba94969 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -275,10 +275,10 @@ class TheorySep : public Theory {
 
   class HeapAssertInfo {
   public:
-    HeapAssertInfo( context::Context* c );
-    ~HeapAssertInfo(){}
-    context::CDO< Node > d_pto;
-    context::CDO< bool > d_has_neg_pto;
+   HeapAssertInfo(context::Context* c);
+   ~HeapAssertInfo() {}
+   context::CDO<Node> d_pto;
+   context::CDO<bool> d_has_neg_pto;
   };
   std::map< Node, HeapAssertInfo * > d_eqc_info;
   HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false );
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 28b84a161..398a21d73 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -100,10 +100,10 @@ class TheorySetsPrivate : protected EnvObj
   class EqcInfo
   {
   public:
-    EqcInfo( context::Context* c );
-    ~EqcInfo(){}
-    // singleton or emptyset equal to this eqc
-    context::CDO< Node > d_singleton;
+   EqcInfo(context::Context* c);
+   ~EqcInfo() {}
+   // singleton or emptyset equal to this eqc
+   context::CDO<Node> d_singleton;
   };
   /** information necessary for equivalence classes */
   std::map< Node, EqcInfo* > d_eqc_info;
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 6de70acc9..7802aa63a 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -35,7 +35,8 @@ namespace cvc5::internal {
 class Env;
 class TheoryEngine;
 
-class SharedTermsDatabase : public context::ContextNotifyObj {
+class SharedTermsDatabase : public context::ContextNotifyObj
+{
  public:
   /** A container for a list of shared terms */
   typedef std::vector<TNode> shared_terms_list;
diff --git a/src/theory/strings/array_core_solver.cpp b/src/theory/strings/array_core_solver.cpp
index bbaca6b06..cb0c37cf7 100644
--- a/src/theory/strings/array_core_solver.cpp
+++ b/src/theory/strings/array_core_solver.cpp
@@ -20,7 +20,7 @@
 #include "theory/strings/word.h"
 #include "util/rational.h"
 
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
diff --git a/src/theory/strings/array_solver.cpp b/src/theory/strings/array_solver.cpp
index b48300e81..0a2fab83d 100644
--- a/src/theory/strings/array_solver.cpp
+++ b/src/theory/strings/array_solver.cpp
@@ -21,7 +21,7 @@
 #include "theory/strings/word.h"
 #include "util/rational.h"
 
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 1955b2b63..9d75ececa 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -25,7 +25,7 @@
 #include "util/rational.h"
 
 using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 382105eb9..dcbb1a6bd 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -28,7 +28,7 @@
 #include "util/string.h"
 
 using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
@@ -2524,7 +2524,7 @@ void CoreSolver::checkNormalFormsDeq()
 {
   eq::EqualityEngine* ee = d_state.getEqualityEngine();
   std::map< Node, std::map< Node, bool > > processed;
-  
+
   const context::CDList<Node>& deqs = d_state.getDisequalityList();
 
   NodeManager* nm = NodeManager::currentNM();
diff --git a/src/theory/strings/eqc_info.cpp b/src/theory/strings/eqc_info.cpp
index 06b19272d..1c1d1384f 100644
--- a/src/theory/strings/eqc_info.cpp
+++ b/src/theory/strings/eqc_info.cpp
@@ -19,7 +19,7 @@
 #include "theory/strings/word.h"
 
 using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 40649e927..2324b5674 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -23,7 +23,7 @@
 #include "util/statistics_registry.h"
 
 using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 651431afa..fb6a9977f 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -23,7 +23,7 @@
 #include "util/rational.h"
 
 using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index faacc0402..6368d1e43 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -26,7 +26,7 @@
 #include "util/statistics_value.h"
 
 using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
@@ -51,7 +51,7 @@ RegExpSolver::RegExpSolver(Env& env,
       d_processed_memberships(context()),
       d_regexp_opr(env, tr.getSkolemCache())
 {
-  d_emptyString = NodeManager::currentNM()->mkConst(::cvc5::internal::String(""));
+  d_emptyString = NodeManager::currentNM()->mkConst(cvc5::internal::String(""));
   d_emptyRegexp = NodeManager::currentNM()->mkNode(REGEXP_NONE);
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 431564b82..be3025a7a 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -3574,7 +3574,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n)
   Node val;
   if (isPrefix)
   {
-    val = NodeManager::currentNM()->mkConstInt(::cvc5::internal::Rational(0));
+    val = NodeManager::currentNM()->mkConstInt(cvc5::internal::Rational(0));
   }
   else
   {
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 38672e63c..946671f7d 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -21,7 +21,7 @@
 #include "util/rational.h"
 
 using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp
index d0f5a70dd..e38c13bf4 100644
--- a/src/theory/strings/strings_fmf.cpp
+++ b/src/theory/strings/strings_fmf.cpp
@@ -18,7 +18,7 @@
 #include "util/rational.h"
 
 using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 5372b50cf..322c9b99e 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -29,7 +29,7 @@
 #include "util/string.h"
 
 using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 30abd1df3..0416be16c 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -33,7 +33,7 @@
 #include "theory/valuation.h"
 
 using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 134102db2..e72779b58 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -99,7 +99,7 @@ namespace eq {
 class Theory : protected EnvObj
 {
   friend class CarePairArgumentCallback;
-  friend class ::cvc5::internal::TheoryEngine;
+  friend class internal::TheoryEngine;
 
  protected:
   /** Name of this theory instance. Along with the TheoryId this should
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index aa10da4ac..959575ccd 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -335,7 +335,9 @@ void TheoryEngine::printAssertions(const char* tag) {
 
         if (d_logicInfo.isSharingEnabled()) {
           Trace(tag) << "Shared terms of " << theory->getId() << ": " << endl;
-          context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
+          context::CDList<TNode>::const_iterator
+              it = theory->shared_terms_begin(),
+              it_end = theory->shared_terms_end();
           for (unsigned i = 0; it != it_end; ++ it, ++i) {
               Trace(tag) << "[" << i << "]: " << (*it) << endl;
           }
@@ -1843,10 +1845,12 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
   for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
     Theory* theory = d_theoryTable[theoryId];
     if(theory && d_logicInfo.isTheoryEnabled(theoryId)) {
-      for(context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
-            it_end = theory->facts_end();
-          it != it_end;
-          ++it) {
+      for (context::CDList<Assertion>::const_iterator
+               it = theory->facts_begin(),
+               it_end = theory->facts_end();
+           it != it_end;
+           ++it)
+      {
         Node assertion = (*it).d_assertion;
         if (hasRelevantAssertions
             && relevantAssertions.find(assertion) == relevantAssertions.end())
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index c434a8e91..c6962d171 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -28,7 +28,7 @@
 
 using namespace std;
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 2119054a2..7ca737fa8 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -28,7 +28,7 @@
 
 using namespace std;
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index b193adfde..9898ba808 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -33,7 +33,7 @@
 
 using namespace std;
 using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
 
 namespace cvc5::internal {
 namespace theory {
@@ -46,15 +46,17 @@ typedef Region::RegionNodeInfo RegionNodeInfo;
 typedef RegionNodeInfo::DiseqList DiseqList;
 
 Region::Region(SortModel* cf, context::Context* c)
-  : d_cf( cf )
-  , d_testCliqueSize( c, 0 )
-  , d_splitsSize( c, 0 )
-  , d_testClique( c )
-  , d_splits( c )
-  , d_reps_size( c, 0 )
-  , d_total_diseq_external( c, 0 )
-  , d_total_diseq_internal( c, 0 )
-  , d_valid( c, true ) {}
+    : d_cf(cf),
+      d_testCliqueSize(c, 0),
+      d_splitsSize(c, 0),
+      d_testClique(c),
+      d_splits(c),
+      d_reps_size(c, 0),
+      d_total_diseq_external(c, 0),
+      d_total_diseq_internal(c, 0),
+      d_valid(c, true)
+{
+}
 
 Region::~Region() {
   for(iterator i = begin(), iend = end(); i != iend; ++i) {
diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index d5155141f..7aef63c29 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -69,14 +69,14 @@ class CardinalityExtension : protected EnvObj
         /** disequality list for node */
         class DiseqList {
         public:
-          DiseqList( context::Context* c )
-            : d_size( c, 0 ), d_disequalities( c ) {}
-          ~DiseqList(){}
-
-          void setDisequal( Node n, bool valid ){
-            Assert((!isSet(n)) || getDisequalityValue(n) != valid);
-            d_disequalities[ n ] = valid;
-            d_size = d_size + ( valid ? 1 : -1 );
+         DiseqList(context::Context* c) : d_size(c, 0), d_disequalities(c) {}
+         ~DiseqList() {}
+
+         void setDisequal(Node n, bool valid)
+         {
+           Assert((!isSet(n)) || getDisequalityValue(n) != valid);
+           d_disequalities[n] = valid;
+           d_size = d_size + (valid ? 1 : -1);
           }
           bool isSet(Node n) const {
             return d_disequalities.find(n) != d_disequalities.end();
@@ -93,13 +93,14 @@ class CardinalityExtension : protected EnvObj
           iterator end() { return d_disequalities.end(); }
 
         private:
-          context::CDO< int > d_size;
-          NodeBoolMap d_disequalities;
+         context::CDO<int> d_size;
+         NodeBoolMap d_disequalities;
         }; /* class DiseqList */
        public:
         /** constructor */
-        RegionNodeInfo( context::Context* c )
-          : d_internal(c), d_external(c), d_valid(c, true) {
+        RegionNodeInfo(context::Context* c)
+            : d_internal(c), d_external(c), d_valid(c, true)
+        {
           d_disequalities[0] = &d_internal;
           d_disequalities[1] = &d_external;
         }
@@ -123,7 +124,7 @@ class CardinalityExtension : protected EnvObj
        private:
         DiseqList d_internal;
         DiseqList d_external;
-        context::CDO< bool > d_valid;
+        context::CDO<bool> d_valid;
         DiseqList* d_disequalities[2];
       }; /* class RegionNodeInfo */
 
@@ -132,7 +133,7 @@ class CardinalityExtension : protected EnvObj
       SortModel* d_cf;
 
       context::CDO<size_t> d_testCliqueSize;
-      context::CDO< unsigned > d_splitsSize;
+      context::CDO<unsigned> d_splitsSize;
       //a postulated clique
       NodeBoolMap d_testClique;
       //disequalities needed for this clique to happen
@@ -140,19 +141,19 @@ class CardinalityExtension : protected EnvObj
       //number of valid representatives in this region
       context::CDO<size_t> d_reps_size;
       //total disequality size (external)
-      context::CDO< unsigned > d_total_diseq_external;
+      context::CDO<unsigned> d_total_diseq_external;
       //total disequality size (internal)
-      context::CDO< unsigned > d_total_diseq_internal;
+      context::CDO<unsigned> d_total_diseq_internal;
       /** set rep */
       void setRep( Node n, bool valid );
       //region node infomation
       std::map< Node, RegionNodeInfo* > d_nodes;
       //whether region is valid
-      context::CDO< bool > d_valid;
+      context::CDO<bool> d_valid;
 
      public:
       //constructor
-      Region( SortModel* cf, context::Context* c );
+      Region(SortModel* cf, context::Context* c);
       virtual ~Region();
 
       typedef std::map< Node, RegionNodeInfo* >::iterator iterator;
@@ -228,11 +229,11 @@ class CardinalityExtension : protected EnvObj
     /** the score for each node for splitting */
     NodeIntMap d_split_score;
     /** number of valid disequalities in d_disequalities */
-    context::CDO< unsigned > d_disequalities_index;
+    context::CDO<unsigned> d_disequalities_index;
     /** list of all disequalities */
     std::vector< Node > d_disequalities;
     /** number of representatives in all regions */
-    context::CDO< unsigned > d_reps;
+    context::CDO<unsigned> d_reps;
 
     /** get number of disequalities from node n to region ri */
     int getNumDisequalitiesToRegion( Node n, int ri );
@@ -268,7 +269,7 @@ class CardinalityExtension : protected EnvObj
     /** cardinality literals */
     std::map<uint32_t, Node> d_cardinality_literal;
     /** whether a positive cardinality constraint has been asserted */
-    context::CDO< bool > d_hasCard;
+    context::CDO<bool> d_hasCard;
     /** clique lemmas that have been asserted */
     std::map< int, std::vector< std::vector< Node > > > d_cliques;
     /** maximum negatively asserted cardinality */
@@ -276,7 +277,7 @@ class CardinalityExtension : protected EnvObj
     /** list of fresh representatives allocated */
     std::vector< Node > d_fresh_aloc_reps;
     /** whether we are initialized */
-    context::CDO< bool > d_initialized;
+    context::CDO<bool> d_initialized;
     /** simple check cardinality */
     void simpleCheckCardinality();
 
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 28da5abff..8d9e3e91d 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -53,8 +53,8 @@ class ProofEqEngine;
  * Class for keeping an incremental congruence closure over a set of terms. It provides
  * notifications via an EqualityEngineNotify object.
  */
-class EqualityEngine : public context::ContextNotifyObj, protected EnvObj {
-
+class EqualityEngine : public context::ContextNotifyObj, protected EnvObj
+{
   friend class EqClassesIterator;
   friend class EqClassIterator;
 
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index c236fbdc2..da89b04d5 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -50,7 +50,7 @@ namespace cvc5::internal {
 namespace theory {
 namespace uf {
 
-using namespace ::cvc5::internal::context;
+using namespace cvc5::context;
 
 SymmetryBreaker::Template::Template() :
   d_template(),
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index 191a7116e..082997d43 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -170,7 +170,7 @@ public:
 
 std::ostream& operator<<(
     std::ostream& out,
-    const ::cvc5::internal::theory::uf::SymmetryBreaker::Permutation& p);
+    const cvc5::internal::theory::uf::SymmetryBreaker::Permutation& p);
 
 }  // namespace cvc5::internal
 
diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h
index df4914fb5..f1e9a452d 100644
--- a/src/util/floatingpoint.h
+++ b/src/util/floatingpoint.h
@@ -508,7 +508,7 @@ struct FloatingPointToBVHashFunction
 {
   inline size_t operator()(const FloatingPointToBV& fptbv) const
   {
-    UnsignedHashFunction< ::cvc5::internal::BitVectorSize> f;
+    UnsignedHashFunction<cvc5::internal::BitVectorSize> f;
     return (key ^ 0x46504256) ^ f(fptbv.d_bv_size);
   }
 }; /* struct FloatingPointToBVHashFunction */
diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp
index b77184ff9..88605dce5 100644
--- a/src/util/floatingpoint_literal_symfpu.cpp
+++ b/src/util/floatingpoint_literal_symfpu.cpp
@@ -35,22 +35,22 @@
 
 namespace symfpu {
 
-#define CVC5_LIT_ITE_DFN(T)                                            \
-  template <>                                                          \
-  struct ite<::cvc5::internal::symfpuLiteral::Cvc5Prop, T>                       \
-  {                                                                    \
-    static const T& iteOp(const ::cvc5::internal::symfpuLiteral::Cvc5Prop& cond, \
-                          const T& l,                                  \
-                          const T& r)                                  \
-    {                                                                  \
-      return cond ? l : r;                                             \
-    }                                                                  \
+#define CVC5_LIT_ITE_DFN(T)                                                    \
+  template <>                                                                  \
+  struct ite<cvc5::internal::symfpuLiteral::Cvc5Prop, T>                       \
+  {                                                                            \
+    static const T& iteOp(const cvc5::internal::symfpuLiteral::Cvc5Prop& cond, \
+                          const T& l,                                          \
+                          const T& r)                                          \
+    {                                                                          \
+      return cond ? l : r;                                                     \
+    }                                                                          \
   }
 
-CVC5_LIT_ITE_DFN(::cvc5::internal::symfpuLiteral::traits::rm);
-CVC5_LIT_ITE_DFN(::cvc5::internal::symfpuLiteral::traits::prop);
-CVC5_LIT_ITE_DFN(::cvc5::internal::symfpuLiteral::traits::sbv);
-CVC5_LIT_ITE_DFN(::cvc5::internal::symfpuLiteral::traits::ubv);
+CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::rm);
+CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::prop);
+CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::sbv);
+CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::ubv);
 
 #undef CVC5_LIT_ITE_DFN
 }  // namespace symfpu
diff --git a/src/util/floatingpoint_literal_symfpu_traits.h b/src/util/floatingpoint_literal_symfpu_traits.h
index 6c35a3ba0..a82555e84 100644
--- a/src/util/floatingpoint_literal_symfpu_traits.h
+++ b/src/util/floatingpoint_literal_symfpu_traits.h
@@ -45,8 +45,8 @@ class wrappedBitVector;
 
 using Cvc5BitWidth = uint32_t;
 using Cvc5Prop = bool;
-using Cvc5RM = ::cvc5::internal::RoundingMode;
-using Cvc5FPSize = ::cvc5::internal::FloatingPointSize;
+using Cvc5RM = cvc5::internal::RoundingMode;
+using Cvc5FPSize = cvc5::internal::FloatingPointSize;
 using Cvc5UnsignedBitVector = wrappedBitVector<false>;
 using Cvc5SignedBitVector = wrappedBitVector<true>;
 
diff --git a/src/util/string.cpp b/src/util/string.cpp
index 1acca2964..00c8fb7a7 100644
--- a/src/util/string.cpp
+++ b/src/util/string.cpp
@@ -522,7 +522,7 @@ Rational String::toNumber() const
 
 namespace strings {
 
-size_t StringHashFunction::operator()(const ::cvc5::internal::String& s) const
+size_t StringHashFunction::operator()(const cvc5::internal::String& s) const
 {
   uint64_t ret = fnv1a::offsetBasis;
   for (unsigned c : s.d_str)
diff --git a/src/util/string.h b/src/util/string.h
index 6b3d59117..4cacbb8e1 100644
--- a/src/util/string.h
+++ b/src/util/string.h
@@ -273,7 +273,7 @@ namespace strings {
 
 struct StringHashFunction
 {
-  size_t operator()(const ::cvc5::internal::String& s) const;
+  size_t operator()(const cvc5::internal::String& s) const;
 }; /* struct StringHashFunction */
 
 }  // namespace strings
diff --git a/test/unit/base/map_util_black.cpp b/test/unit/base/map_util_black.cpp
index 051c30624..5ef8c747c 100644
--- a/test/unit/base/map_util_black.cpp
+++ b/test/unit/base/map_util_black.cpp
@@ -28,9 +28,9 @@
 
 namespace cvc5::internal {
 
-using context::CDHashMap;
-using context::CDInsertHashMap;
-using context::Context;
+using cvc5::context::CDHashMap;
+using cvc5::context::CDInsertHashMap;
+using cvc5::context::Context;
 
 namespace test {
 
diff --git a/test/unit/context/cdhashmap_black.cpp b/test/unit/context/cdhashmap_black.cpp
index 3a27252d1..fde9517d0 100644
--- a/test/unit/context/cdhashmap_black.cpp
+++ b/test/unit/context/cdhashmap_black.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Black box testing of context::CDMap<>.
+ * Black box testing of cvc5::context::CDMap<>.
  */
 
 #include <map>
@@ -23,8 +23,8 @@
 namespace cvc5::internal {
 namespace test {
 
-using context::CDHashMap;
-using context::Context;
+using cvc5::context::CDHashMap;
+using cvc5::context::Context;
 
 class TestContextBlackCDHashMap : public TestContext
 {
diff --git a/test/unit/context/cdhashmap_white.cpp b/test/unit/context/cdhashmap_white.cpp
index 3210fa5ef..038bc0138 100644
--- a/test/unit/context/cdhashmap_white.cpp
+++ b/test/unit/context/cdhashmap_white.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * White box testing of context::CDMap<>.
+ * White box testing of cvc5::context::CDMap<>.
  */
 
 #include "base/check.h"
diff --git a/test/unit/context/cdlist_black.cpp b/test/unit/context/cdlist_black.cpp
index 843e6b655..2772e1503 100644
--- a/test/unit/context/cdlist_black.cpp
+++ b/test/unit/context/cdlist_black.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Black box testing of context::CDList<>.
+ * Black box testing of cvc5::context::CDList<>.
  */
 
 #include <limits.h>
diff --git a/test/unit/context/cdo_black.cpp b/test/unit/context/cdo_black.cpp
index 57bd6150f..564d5f73e 100644
--- a/test/unit/context/cdo_black.cpp
+++ b/test/unit/context/cdo_black.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Black box testing of context::CDO<>.
+ * Black box testing of cvc5::context::CDO<>.
  */
 
 #include <iostream>
diff --git a/test/unit/context/context_black.cpp b/test/unit/context/context_black.cpp
index bde4c9d23..12efc52ca 100644
--- a/test/unit/context/context_black.cpp
+++ b/test/unit/context/context_black.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Black box testing of context::Context.
+ * Black box testing of cvc5::context::Context.
  */
 
 #include <iostream>
diff --git a/test/unit/context/context_mm_black.cpp b/test/unit/context/context_mm_black.cpp
index a539a6e28..8c9101be5 100644
--- a/test/unit/context/context_mm_black.cpp
+++ b/test/unit/context/context_mm_black.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Black box testing of context::ContextMemoryManager.
+ * Black box testing of cvc5::context::ContextMemoryManager.
  */
 
 #include <cstring>
diff --git a/test/unit/context/context_white.cpp b/test/unit/context/context_white.cpp
index f1c570c36..2fef425b3 100644
--- a/test/unit/context/context_white.cpp
+++ b/test/unit/context/context_white.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * White box testing of context::Context.
+ * White box testing of cvc5::context::Context.
  */
 
 #include "base/check.h"
diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp
index 4bb3d9bf2..29c6f123c 100644
--- a/test/unit/prop/cnf_stream_white.cpp
+++ b/test/unit/prop/cnf_stream_white.cpp
@@ -29,7 +29,7 @@
 
 namespace cvc5::internal {
 
-using namespace context;
+using namespace cvc5::context;
 using namespace prop;
 using namespace smt;
 using namespace theory;
@@ -109,7 +109,7 @@ class TestPropWhiteCnfStream : public TestSmt
     TestSmt::SetUp();
     d_theoryEngine = d_slvEngine->getTheoryEngine();
     d_satSolver.reset(new FakeSatSolver());
-    d_cnfContext.reset(new context::Context());
+    d_cnfContext.reset(new Context());
     d_cnfRegistrar.reset(new prop::NullRegistrar);
     d_cnfStream.reset(new prop::CnfStream(d_slvEngine->getEnv(),
                                           d_satSolver.get(),
diff --git a/test/unit/test_context.h b/test/unit/test_context.h
index 5e875cb52..455319c6b 100644
--- a/test/unit/test_context.h
+++ b/test/unit/test_context.h
@@ -25,8 +25,8 @@ namespace test {
 class TestContext : public TestInternal
 {
  protected:
-  void SetUp() override { d_context.reset(new context::Context()); }
-  std::unique_ptr<context::Context> d_context;
+  void SetUp() override { d_context.reset(new cvc5::context::Context()); }
+  std::unique_ptr<cvc5::context::Context> d_context;
 };
 
 }  // namespace test
diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp
index fa0fbbd73..0f643397d 100644
--- a/test/unit/theory/theory_engine_white.cpp
+++ b/test/unit/theory/theory_engine_white.cpp
@@ -37,7 +37,7 @@ namespace cvc5::internal {
 
 using namespace theory;
 using namespace expr;
-using namespace context;
+using namespace cvc5::context;
 using namespace kind;
 using namespace theory::bv;