Replace Theory::Set with TheoryIdSet (#4959)

This makes it so that equality_engine.h does not include theory.h. This is a bad dependency since Theory contains EqualityEngine.

This dependency between equality engine and theory was due to the use of a helper (Theory::Set) for representing sets of theories that is inlined into Theory. This PR moves this definition and utilities to theory_id.h.

It fixes the resulting include dependencies which are broken by changing the include theory.h -> theory_id.h in equality_engine.h.

This avoids a circular dependency in the includes between Theory -> InferenceManager -> ProofEqualityEngine -> EqualityEngine -> Theory.

20 files changed, 392 insertions, 232 deletions

diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index d46346fd8..242d895fc 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -27,6 +27,7 @@
 #include "theory/arith/arithvar.h"
 #include "theory/arith/constraint_forward.h"
 #include "theory/arith/partial_model.h"
+#include "theory/ee_setup_info.h"
 #include "theory/uf/equality_engine.h"
 #include "util/dense_map.h"
 #include "util/statistics_registry.h"
diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h
index 9fc2e1156..9511f2779 100644
--- a/src/theory/model_manager.h
+++ b/src/theory/model_manager.h
@@ -19,6 +19,7 @@
 
 #include <memory>
 
+#include "theory/logic_info.h"
 #include "theory/theory_model.h"
 #include "theory/theory_model_builder.h"
 
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 4e1ef6d7f..bdf6d0607 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -17,6 +17,7 @@
 #ifndef CVC4__FIRST_ORDER_MODEL_H
 #define CVC4__FIRST_ORDER_MODEL_H
 
+#include "context/cdlist.h"
 #include "expr/attribute.h"
 #include "theory/theory_model.h"
 #include "theory/uf/theory_uf_model.h"
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 4aa866d27..08410943f 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -18,6 +18,7 @@
 #include "expr/emptyset.h"
 #include "expr/node_algorithm.h"
 #include "options/sets_options.h"
+#include "smt/logic_exception.h"
 #include "theory/sets/normal_form.h"
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 99584b167..a196d0ed0 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -50,9 +50,13 @@ void SharedTermsDatabase::addEqualityToPropagate(TNode equality) {
   checkForConflict();
 }
 
-
-void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theories) {
-  Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " << term << ", " << Theory::setToString(theories) << ")" << std::endl;
+void SharedTermsDatabase::addSharedTerm(TNode atom,
+                                        TNode term,
+                                        TheoryIdSet theories)
+{
+  Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", "
+                    << term << ", " << TheoryIdSetUtil::setToString(theories)
+                    << ")" << std::endl;
 
   std::pair<TNode, TNode> search_pair(atom, term);
   SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair);
@@ -64,7 +68,8 @@ void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theo
     d_termsToTheories[search_pair] = theories;
   } else {
     Assert(theories != (*find).second);
-    d_termsToTheories[search_pair] = Theory::setUnion(theories, (*find).second);
+    d_termsToTheories[search_pair] =
+        TheoryIdSetUtil::setUnion(theories, (*find).second);
   }
 }
 
@@ -94,25 +99,27 @@ void SharedTermsDatabase::backtrack() {
   d_addedSharedTerms.resize(d_addedSharedTermsSize);
 }
 
-Theory::Set SharedTermsDatabase::getTheoriesToNotify(TNode atom, TNode term) const {
+TheoryIdSet SharedTermsDatabase::getTheoriesToNotify(TNode atom,
+                                                     TNode term) const
+{
   // Get the theories that share this term from this atom
   std::pair<TNode, TNode> search_pair(atom, term);
   SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair);
   Assert(find != d_termsToTheories.end());
 
   // Get the theories that were already notified
-  Theory::Set alreadyNotified = 0;
+  TheoryIdSet alreadyNotified = 0;
   AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
   if (theoriesFind != d_alreadyNotifiedMap.end()) {
     alreadyNotified = (*theoriesFind).second;
   }
 
   // Return the ones that haven't been notified yet
-  return Theory::setDifference((*find).second, alreadyNotified);
+  return TheoryIdSetUtil::setDifference((*find).second, alreadyNotified);
 }
 
-
-Theory::Set SharedTermsDatabase::getNotifiedTheories(TNode term) const {
+TheoryIdSet SharedTermsDatabase::getNotifiedTheories(TNode term) const
+{
   // Get the theories that were already notified
   AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
   if (theoriesFind != d_alreadyNotifiedMap.end()) {
@@ -142,15 +149,16 @@ bool SharedTermsDatabase::propagateSharedEquality(TheoryId theory, TNode a, TNod
   return true;
 }
 
-void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) {
-
+void SharedTermsDatabase::markNotified(TNode term, TheoryIdSet theories)
+{
   // Find out if there are any new theories that were notified about this term
-  Theory::Set alreadyNotified = 0;
+  TheoryIdSet alreadyNotified = 0;
   AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
   if (theoriesFind != d_alreadyNotifiedMap.end()) {
     alreadyNotified = (*theoriesFind).second;
   }
-  Theory::Set newlyNotified = Theory::setDifference(theories, alreadyNotified);
+  TheoryIdSet newlyNotified =
+      TheoryIdSetUtil::setDifference(theories, alreadyNotified);
 
   // If no new theories were notified, we are done
   if (newlyNotified == 0) {
@@ -160,11 +168,14 @@ void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) {
   Debug("shared-terms-database") << "SharedTermsDatabase::markNotified(" << term << ")" << endl;
 
   // First update the set of notified theories for this term
-  d_alreadyNotifiedMap[term] = Theory::setUnion(newlyNotified, alreadyNotified);
+  d_alreadyNotifiedMap[term] =
+      TheoryIdSetUtil::setUnion(newlyNotified, alreadyNotified);
 
   // Mark the shared terms in the equality engine
   theory::TheoryId currentTheory;
-  while ((currentTheory = Theory::setPop(newlyNotified)) != THEORY_LAST) {
+  while ((currentTheory = TheoryIdSetUtil::setPop(newlyNotified))
+         != THEORY_LAST)
+  {
     d_equalityEngine.addTriggerTerm(term, currentTheory);
   }
 
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 05ce88d99..ca4f6c183 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -21,7 +21,7 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
-#include "theory/theory.h"
+#include "theory/theory_id.h"
 #include "theory/uf/equality_engine.h"
 #include "util/statistics_registry.h"
 
@@ -57,11 +57,15 @@ private:
   context::CDO<unsigned> d_addedSharedTermsSize;
 
   /** A map from atoms and subterms to the theories that use it */
-  typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap;
+  typedef context::CDHashMap<std::pair<Node, TNode>,
+                             theory::TheoryIdSet,
+                             TNodePairHashFunction>
+      SharedTermsTheoriesMap;
   SharedTermsTheoriesMap d_termsToTheories;
 
   /** Map from term to theories that have already been notified about the shared term */
-  typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap;
+  typedef context::CDHashMap<TNode, theory::TheoryIdSet, TNodeHashFunction>
+      AlreadyNotifiedMap;
   AlreadyNotifiedMap d_alreadyNotifiedMap;
 
   /** The registered equalities for propagation */
@@ -178,12 +182,12 @@ public:
    * Add a shared term to the database. The shared term is a subterm of the atom and
    * should be associated with the given theory.
    */
-  void addSharedTerm(TNode atom, TNode term, theory::Theory::Set theories);
+  void addSharedTerm(TNode atom, TNode term, theory::TheoryIdSet theories);
 
   /**
    * Mark that the given theories have been notified of the given shared term.
    */
-  void markNotified(TNode term, theory::Theory::Set theories);
+  void markNotified(TNode term, theory::TheoryIdSet theories);
 
   /**
    * Returns true if the atom contains any shared terms, false otherwise.
@@ -203,12 +207,12 @@ public:
   /**
    * Get the theories that share the term in a given atom (and have not yet been notified).
    */
-  theory::Theory::Set getTheoriesToNotify(TNode atom, TNode term) const;
+  theory::TheoryIdSet getTheoriesToNotify(TNode atom, TNode term) const;
 
   /**
    * Get the theories that share the term and have been notified already.
    */
-  theory::Theory::Set getNotifiedTheories(TNode term) const;
+  theory::TheoryIdSet getNotifiedTheories(TNode term) const;
 
   /**
    * Returns true if the term is currently registered as shared with some theory.
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
index fc27b847b..d9a67748d 100644
--- a/src/theory/strings/solver_state.h
+++ b/src/theory/strings/solver_state.h
@@ -19,12 +19,14 @@
 
 #include <map>
 
+#include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "theory/strings/eqc_info.h"
 #include "theory/theory_model.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/valuation.h"
-#include "theory/strings/eqc_info.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index bf7cab4e3..b076e72a3 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -26,7 +26,8 @@ std::string PreRegisterVisitor::toString() const {
   std::stringstream ss;
   TNodeToTheorySetMap::const_iterator it = d_visited.begin();
   for (; it != d_visited.end(); ++ it) {
-    ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl;
+    ss << (*it).first << ": " << TheoryIdSetUtil::setToString((*it).second)
+       << std::endl;
   }
   return ss.str();
 }
@@ -50,8 +51,8 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
   TheoryId currentTheoryId = Theory::theoryOf(current);
   TheoryId parentTheoryId = Theory::theoryOf(parent);
 
-  d_theories = Theory::setInsert(currentTheoryId, d_theories);
-  d_theories = Theory::setInsert(parentTheoryId, d_theories);
+  d_theories = TheoryIdSetUtil::setInsert(currentTheoryId, d_theories);
+  d_theories = TheoryIdSetUtil::setInsert(parentTheoryId, d_theories);
 
   // Should we use the theory of the type
   bool useType = false;
@@ -78,19 +79,21 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
   TNodeToTheorySetMap::iterator find = d_visited.find(current);
   if (find == d_visited.end()) {
     if (useType) {
-      d_theories = Theory::setInsert(typeTheoryId, d_theories);
+      d_theories = TheoryIdSetUtil::setInsert(typeTheoryId, d_theories);
     }
     return false;
   }
 
-  Theory::Set visitedTheories = (*find).second;
-  if (Theory::setContains(currentTheoryId, visitedTheories)) {
+  TheoryIdSet visitedTheories = (*find).second;
+  if (TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
+  {
     // The current theory has already visited it, so now it depends on the parent and the type
-    if (Theory::setContains(parentTheoryId, visitedTheories)) {
+    if (TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
+    {
       if (useType) {
         TheoryId typeTheoryId2 = Theory::theoryOf(current.getType());
-        d_theories = Theory::setInsert(typeTheoryId2, d_theories);
-        return Theory::setContains(typeTheoryId2, visitedTheories);
+        d_theories = TheoryIdSetUtil::setInsert(typeTheoryId2, d_theories);
+        return TheoryIdSetUtil::setContains(typeTheoryId2, visitedTheories);
       } else {
         return true;
       }
@@ -133,33 +136,45 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
       }
     }
   }
-  
-  Theory::Set visitedTheories = d_visited[current];
-  Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
-  if (!Theory::setContains(currentTheoryId, visitedTheories)) {
-    visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories);
+
+  TheoryIdSet visitedTheories = d_visited[current];
+  Debug("register::internal")
+      << "PreRegisterVisitor::visit(" << current << "," << parent
+      << "): previously registered with "
+      << TheoryIdSetUtil::setToString(visitedTheories) << std::endl;
+  if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
+  {
+    visitedTheories =
+        TheoryIdSetUtil::setInsert(currentTheoryId, visitedTheories);
     d_visited[current] = visitedTheories;
     Theory* th = d_engine->theoryOf(currentTheoryId);
     th->preRegisterTerm(current);
     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
   }
-  if (!Theory::setContains(parentTheoryId, visitedTheories)) {
-    visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories);
+  if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
+  {
+    visitedTheories =
+        TheoryIdSetUtil::setInsert(parentTheoryId, visitedTheories);
     d_visited[current] = visitedTheories;
     Theory* th = d_engine->theoryOf(parentTheoryId);
     th->preRegisterTerm(current);
     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
   }
   if (useType) {
-    if (!Theory::setContains(typeTheoryId, visitedTheories)) {
-      visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
+    if (!TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories))
+    {
+      visitedTheories =
+          TheoryIdSetUtil::setInsert(typeTheoryId, visitedTheories);
       d_visited[current] = visitedTheories;
       Theory* th = d_engine->theoryOf(typeTheoryId);
       th->preRegisterTerm(current);
       Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
     }
   }
-  Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl;
+  Debug("register::internal")
+      << "PreRegisterVisitor::visit(" << current << "," << parent
+      << "): now registered with "
+      << TheoryIdSetUtil::setToString(visitedTheories) << std::endl;
 
   Assert(d_visited.find(current) != d_visited.end());
   Assert(alreadyVisited(current, parent));
@@ -169,7 +184,8 @@ std::string SharedTermsVisitor::toString() const {
   std::stringstream ss;
   TNodeVisitedMap::const_iterator it = d_visited.begin();
   for (; it != d_visited.end(); ++ it) {
-    ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl;
+    ss << (*it).first << ": " << TheoryIdSetUtil::setToString((*it).second)
+       << std::endl;
   }
   return ss.str();
 }
@@ -197,7 +213,7 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
     return false;
   }
 
-  Theory::Set theories = (*find).second;
+  TheoryIdSet theories = (*find).second;
 
   TheoryId currentTheoryId = Theory::theoryOf(current);
   TheoryId parentTheoryId  = Theory::theoryOf(parent);
@@ -239,16 +255,23 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
     }
   }
 
-  if (Theory::setContains(currentTheoryId, theories)) {
-      if (Theory::setContains(parentTheoryId, theories)) {
-        if (useType) {
-          return Theory::setContains(typeTheoryId, theories);
-        } else {
-          return true;
-        }
-      } else {
-        return false;
+  if (TheoryIdSetUtil::setContains(currentTheoryId, theories))
+  {
+    if (TheoryIdSetUtil::setContains(parentTheoryId, theories))
+    {
+      if (useType)
+      {
+        return TheoryIdSetUtil::setContains(typeTheoryId, theories);
       }
+      else
+      {
+        return true;
+      }
+    }
+    else
+    {
+      return false;
+    }
   } else {
     return false;
   }
@@ -286,29 +309,43 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) {
     }
   }
 
-  Theory::Set visitedTheories = d_visited[current];
-  Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
-  if (!Theory::setContains(currentTheoryId, visitedTheories)) {
-    visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories);
+  TheoryIdSet visitedTheories = d_visited[current];
+  Debug("register::internal")
+      << "SharedTermsVisitor::visit(" << current << "," << parent
+      << "): previously registered with "
+      << TheoryIdSetUtil::setToString(visitedTheories) << std::endl;
+  if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
+  {
+    visitedTheories =
+        TheoryIdSetUtil::setInsert(currentTheoryId, visitedTheories);
     Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
   }
-  if (!Theory::setContains(parentTheoryId, visitedTheories)) {
-    visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories);
+  if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
+  {
+    visitedTheories =
+        TheoryIdSetUtil::setInsert(parentTheoryId, visitedTheories);
     Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
   }
   if (useType) {
-    if (!Theory::setContains(typeTheoryId, visitedTheories)) {
-      visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
+    if (!TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories))
+    {
+      visitedTheories =
+          TheoryIdSetUtil::setInsert(typeTheoryId, visitedTheories);
       Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << typeTheoryId << std::endl;
     }
   }
-  Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl;
+  Debug("register::internal")
+      << "SharedTermsVisitor::visit(" << current << "," << parent
+      << "): now registered with "
+      << TheoryIdSetUtil::setToString(visitedTheories) << std::endl;
 
   // Record the new theories that we visited
   d_visited[current] = visitedTheories;
 
   // If there is more than two theories and a new one has been added notify the shared terms database
-  if (Theory::setDifference(visitedTheories, Theory::setInsert(currentTheoryId))) {
+  if (TheoryIdSetUtil::setDifference(
+          visitedTheories, TheoryIdSetUtil::setInsert(currentTheoryId)))
+  {
     d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories);
   }
 
diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h
index 6c6696f64..9772a6e34 100644
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -42,7 +42,8 @@ class PreRegisterVisitor {
   /** The engine */
   TheoryEngine* d_engine;
 
-  typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeToTheorySetMap;
+  typedef context::CDHashMap<TNode, theory::TheoryIdSet, TNodeHashFunction>
+      TNodeToTheorySetMap;
 
   /**
    * Map from terms to the theories that have already had this term pre-registered.
@@ -52,43 +53,43 @@ class PreRegisterVisitor {
   /**
    * A set of all theories in the term
    */
-  theory::Theory::Set d_theories;
+  theory::TheoryIdSet d_theories;
 
   /**
    * String representation of the visited map, for debugging purposes.
    */
   std::string toString() const;
 
-public:
-
+ public:
   /** Returned set tells us which theories there are */
-  typedef theory::Theory::Set return_type;
-  
+  typedef theory::TheoryIdSet return_type;
+
   PreRegisterVisitor(TheoryEngine* engine, context::Context* context)
-  : d_engine(engine)
-  , d_visited(context)
-  , d_theories(0)
-  {}
+      : d_engine(engine), d_visited(context), d_theories(0)
+  {
+  }
 
   /**
-   * Returns true is current has already been pre-registered with both current and parent theories.
+   * Returns true is current has already been pre-registered with both current
+   * and parent theories.
    */
   bool alreadyVisited(TNode current, TNode parent);
-  
+
   /**
-   * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
+   * Pre-registeres current with any of the current and parent theories that
+   * haven't seen the term yet.
    */
   void visit(TNode current, TNode parent);
-  
+
   /**
    * Marks the node as the starting literal.
    */
-  void start(TNode node) { }
+  void start(TNode node) {}
 
   /**
    * Notifies the engine of all the theories used.
    */
-  theory::Theory::Set done(TNode node) { return d_theories; }
+  theory::TheoryIdSet done(TNode node) { return d_theories; }
 };
 
 
@@ -105,7 +106,8 @@ class SharedTermsVisitor {
   /**
    * Cache from preprocessing of atoms.
    */
-  typedef std::unordered_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
+  typedef std::unordered_map<TNode, theory::TheoryIdSet, TNodeHashFunction>
+      TNodeVisitedMap;
   TNodeVisitedMap d_visited;
 
   /**
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 29a3a0998..c5fcf362c 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -30,7 +30,6 @@
 #include "context/cdo.h"
 #include "context/context.h"
 #include "expr/node.h"
-#include "lib/ffs.h"
 #include "options/options.h"
 #include "options/theory_options.h"
 #include "smt/command.h"
@@ -799,84 +798,6 @@ class Theory {
                     << " doesn't support Theory::setUserAttribute interface";
   }
 
-  /** A set of theories */
-  typedef uint32_t Set;
-
-  /** A set of all theories */
-  static const Set AllTheories = (1 << theory::THEORY_LAST) - 1;
-
-  /** Pops a first theory off the set */
-  static inline TheoryId setPop(Set& set) {
-    uint32_t i = ffs(set); // Find First Set (bit)
-    if (i == 0) { return THEORY_LAST; }
-    TheoryId id = (TheoryId)(i-1);
-    set = setRemove(id, set);
-    return id;
-  }
-
-  /** Returns the size of a set of theories */
-  static inline size_t setSize(Set set) {
-    size_t count = 0;
-    while (setPop(set) != THEORY_LAST) {
-      ++ count;
-    }
-    return count;
-  }
-
-  /** Returns the index size of a set of theories */
-  static inline size_t setIndex(TheoryId id, Set set) {
-    Assert(setContains(id, set));
-    size_t count = 0;
-    while (setPop(set) != id) {
-      ++ count;
-    }
-    return count;
-  }
-
-  /** Add the theory to the set. If no set specified, just returns a singleton set */
-  static inline Set setInsert(TheoryId theory, Set set = 0) {
-    return set | (1 << theory);
-  }
-
-  /** Add the theory to the set. If no set specified, just returns a singleton set */
-  static inline Set setRemove(TheoryId theory, Set set = 0) {
-    return setDifference(set, setInsert(theory));
-  }
-
-  /** Check if the set contains the theory */
-  static inline bool setContains(TheoryId theory, Set set) {
-    return set & (1 << theory);
-  }
-
-  static inline Set setComplement(Set a) {
-    return (~a) & AllTheories;
-  }
-
-  static inline Set setIntersection(Set a, Set b) {
-    return a & b;
-  }
-
-  static inline Set setUnion(Set a, Set b) {
-    return a | b;
-  }
-
-  /** a - b  */
-  static inline Set setDifference(Set a, Set b) {
-    return (~b) & a;
-  }
-
-  static inline std::string setToString(theory::Theory::Set theorySet) {
-    std::stringstream ss;
-    ss << "[";
-    for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
-      if (theory::Theory::setContains((theory::TheoryId)theoryId, theorySet)) {
-        ss << (theory::TheoryId) theoryId << " ";
-      }
-    }
-    ss << "]";
-    return ss.str();
-  }
-
   typedef context::CDList<Assertion>::const_iterator assertions_iterator;
 
   /**
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index bf74cd016..c61879b6d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -50,6 +50,7 @@
 #include "theory/relevance_manager.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_id.h"
 #include "theory/theory_model.h"
 #include "theory/theory_traits.h"
 #include "theory/uf/equality_engine.h"
@@ -308,12 +309,13 @@ void TheoryEngine::preRegister(TNode preprocessed) {
       Assert(!expr::hasFreeVar(preprocessed));
 
       // Pre-register the terms in the atom
-      Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(
+      theory::TheoryIdSet theories = NodeVisitor<PreRegisterVisitor>::run(
           d_preRegistrationVisitor, preprocessed);
-      theories = Theory::setRemove(THEORY_BOOL, theories);
+      theories = TheoryIdSetUtil::setRemove(THEORY_BOOL, theories);
       // Remove the top theory, if any more that means multiple theories were
       // involved
-      bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories);
+      bool multipleTheories =
+          TheoryIdSetUtil::setRemove(Theory::theoryOf(preprocessed), theories);
       if (Configuration::isAssertionBuild())
       {
         TheoryId i;
@@ -324,7 +326,7 @@ void TheoryEngine::preRegister(TNode preprocessed) {
         // even though arithmetic isn't actually involved.
         if (!options::finiteModelFind())
         {
-          while ((i = Theory::setPop(theories)) != THEORY_LAST)
+          while ((i = TheoryIdSetUtil::setPop(theories)) != THEORY_LAST)
           {
             if (!d_logicInfo.isTheoryEnabled(i))
             {
@@ -1074,9 +1076,11 @@ void TheoryEngine::assertFact(TNode literal)
       SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom);
       for (; it != it_end; ++ it) {
         TNode term = *it;
-        Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term);
+        theory::TheoryIdSet theories =
+            d_sharedTerms.getTheoriesToNotify(atom, term);
         for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++ id) {
-          if (Theory::setContains(id, theories)) {
+          if (TheoryIdSetUtil::setContains(id, theories))
+          {
             theoryOf(id)->addSharedTerm(term);
           }
         }
diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp
index 2c87458ef..a801e4abb 100644
--- a/src/theory/theory_id.cpp
+++ b/src/theory/theory_id.cpp
@@ -17,6 +17,9 @@
 
 #include "theory/theory_id.h"
 
+#include "base/check.h"
+#include "lib/ffs.h"
+
 namespace CVC4 {
 namespace theory {
 
@@ -70,5 +73,89 @@ std::string getStatsPrefix(TheoryId theoryId)
   return "unknown";
 }
 
+TheoryId TheoryIdSetUtil::setPop(TheoryIdSet& set)
+{
+  uint32_t i = ffs(set);  // Find First Set (bit)
+  if (i == 0)
+  {
+    return THEORY_LAST;
+  }
+  TheoryId id = static_cast<TheoryId>(i - 1);
+  set = setRemove(id, set);
+  return id;
+}
+
+size_t TheoryIdSetUtil::setSize(TheoryIdSet set)
+{
+  size_t count = 0;
+  while (setPop(set) != THEORY_LAST)
+  {
+    ++count;
+  }
+  return count;
+}
+
+size_t TheoryIdSetUtil::setIndex(TheoryId id, TheoryIdSet set)
+{
+  Assert(setContains(id, set));
+  size_t count = 0;
+  while (setPop(set) != id)
+  {
+    ++count;
+  }
+  return count;
+}
+
+TheoryIdSet TheoryIdSetUtil::setInsert(TheoryId theory, TheoryIdSet set)
+{
+  return set | (1 << theory);
+}
+
+TheoryIdSet TheoryIdSetUtil::setRemove(TheoryId theory, TheoryIdSet set)
+{
+  return setDifference(set, setInsert(theory));
+}
+
+bool TheoryIdSetUtil::setContains(TheoryId theory, TheoryIdSet set)
+{
+  return set & (1 << theory);
+}
+
+TheoryIdSet TheoryIdSetUtil::setComplement(TheoryIdSet a)
+{
+  return (~a) & AllTheories;
+}
+
+TheoryIdSet TheoryIdSetUtil::setIntersection(TheoryIdSet a, TheoryIdSet b)
+{
+  return a & b;
+}
+
+TheoryIdSet TheoryIdSetUtil::setUnion(TheoryIdSet a, TheoryIdSet b)
+{
+  return a | b;
+}
+
+TheoryIdSet TheoryIdSetUtil::setDifference(TheoryIdSet a, TheoryIdSet b)
+{
+  return (~b) & a;
+}
+
+std::string TheoryIdSetUtil::setToString(TheoryIdSet theorySet)
+{
+  std::stringstream ss;
+  ss << "[";
+  for (unsigned theoryId = 0; theoryId < THEORY_LAST; ++theoryId)
+  {
+    TheoryId tid = static_cast<TheoryId>(theoryId);
+    if (setContains(tid, theorySet))
+    {
+      ss << tid << " ";
+    }
+  }
+  ss << "]";
+  return ss.str();
+}
+
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/theory_id.h b/src/theory/theory_id.h
index 005380352..452dd09a9 100644
--- a/src/theory/theory_id.h
+++ b/src/theory/theory_id.h
@@ -23,7 +23,6 @@
 #include <iostream>
 
 namespace CVC4 {
-
 namespace theory {
 
 /**
@@ -58,6 +57,53 @@ std::ostream& operator<<(std::ostream& out, TheoryId theoryId);
 
 std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC;
 
+/**
+ * A set of theories. Utilities for TheoryIdSet can be found below.
+ */
+typedef uint32_t TheoryIdSet;
+
+class TheoryIdSetUtil
+{
+ public:
+  /** A set of all theories */
+  static const TheoryIdSet AllTheories = (1 << theory::THEORY_LAST) - 1;
+
+  /** Pops a first theory off the set */
+  static TheoryId setPop(TheoryIdSet& set);
+
+  /** Returns the size of a set of theories */
+  static size_t setSize(TheoryIdSet set);
+
+  /** Returns the index size of a set of theories */
+  static size_t setIndex(TheoryId id, TheoryIdSet set);
+
+  /** Add the theory to the set. If no set specified, just returns a singleton
+   * set */
+  static TheoryIdSet setInsert(TheoryId theory, TheoryIdSet set = 0);
+
+  /** Add the theory to the set. If no set specified, just returns a singleton
+   * set */
+  static TheoryIdSet setRemove(TheoryId theory, TheoryIdSet set = 0);
+
+  /** Check if the set contains the theory */
+  static bool setContains(TheoryId theory, TheoryIdSet set);
+
+  /** Set complement of a */
+  static TheoryIdSet setComplement(TheoryIdSet a);
+
+  /** Set intersection of a and b */
+  static TheoryIdSet setIntersection(TheoryIdSet a, TheoryIdSet b);
+
+  /** Set union of a and b */
+  static TheoryIdSet setUnion(TheoryIdSet a, TheoryIdSet b);
+
+  /** Set difference of a and b */
+  static TheoryIdSet setDifference(TheoryIdSet a, TheoryIdSet b);
+
+  /** Convert theorySet to string (for debugging) */
+  static std::string setToString(TheoryIdSet theorySet);
+};
+
 }  // namespace theory
 }  // namespace CVC4
 #endif
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 869e9100e..da9f28d01 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -16,6 +16,7 @@
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
+#include "options/theory_options.h"
 #include "options/uf_options.h"
 #include "smt/smt_engine.h"
 
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index c31f208a0..aea3463c8 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -21,6 +21,7 @@
 #include <unordered_set>
 
 #include "smt/model.h"
+#include "theory/ee_setup_info.h"
 #include "theory/rep_set.h"
 #include "theory/substitutions.h"
 #include "theory/type_enumerator.h"
diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index 898ca7dbc..32e2d1a90 100644
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -23,6 +23,9 @@
 #include "theory/theory_model.h"
 
 namespace CVC4 {
+
+class TheoryEngine;
+
 namespace theory {
 
 /** TheoryEngineModelBuilder class
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 7bb857425..dd142edf4 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -17,6 +17,8 @@
 
 #include "theory/uf/equality_engine.h"
 
+#include "options/smt_options.h"
+#include "proof/proof_manager.h"
 #include "smt/smt_statistics_registry.h"
 
 namespace CVC4 {
@@ -386,13 +388,13 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
       // Non-Boolean constants are trigger terms for all tags
       EqualityNodeId tId = getNodeId(t);
       // Setup the new set
-      Theory::Set newSetTags = 0;
+      TheoryIdSet newSetTags = 0;
       EqualityNodeId newSetTriggers[THEORY_LAST];
       unsigned newSetTriggersSize = THEORY_LAST;
       for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST;
            ++currentTheory)
       {
-        newSetTags = Theory::setInsert(currentTheory, newSetTags);
+        newSetTags = TheoryIdSetUtil::setInsert(currentTheory, newSetTags);
         newSetTriggers[currentTheory] = tId;
       }
       // Add it to the list for backtracking
@@ -534,17 +536,17 @@ bool EqualityEngine::assertEquality(TNode eq,
       TriggerTermSet& aTriggerTerms = getTriggerTermSet(aTriggerRef);
       TriggerTermSet& bTriggerTerms = getTriggerTermSet(bTriggerRef);
       // Go through and notify the shared dis-equalities
-      Theory::Set aTags = aTriggerTerms.d_tags;
-      Theory::Set bTags = bTriggerTerms.d_tags;
-      TheoryId aTag = Theory::setPop(aTags);
-      TheoryId bTag = Theory::setPop(bTags);
+      TheoryIdSet aTags = aTriggerTerms.d_tags;
+      TheoryIdSet bTags = bTriggerTerms.d_tags;
+      TheoryId aTag = TheoryIdSetUtil::setPop(aTags);
+      TheoryId bTag = TheoryIdSetUtil::setPop(bTags);
       int a_i = 0, b_i = 0;
       while (aTag != THEORY_LAST && bTag != THEORY_LAST) {
         if (aTag < bTag) {
-          aTag = Theory::setPop(aTags);
+          aTag = TheoryIdSetUtil::setPop(aTags);
           ++ a_i;
         } else if (aTag > bTag) {
-          bTag = Theory::setPop(bTags);
+          bTag = TheoryIdSetUtil::setPop(bTags);
           ++ b_i;
         } else {
           // Same tags, notify
@@ -567,8 +569,8 @@ bool EqualityEngine::assertEquality(TNode eq,
             }
           }
           // Pop the next tags
-          aTag = Theory::setPop(aTags);
-          bTag = Theory::setPop(bTags);
+          aTag = TheoryIdSetUtil::setPop(aTags);
+          bTag = TheoryIdSetUtil::setPop(bTags);
         }
       }
     }
@@ -618,12 +620,12 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
 
   // Trigger set of class 1
   TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id];
-  Theory::Set class1Tags = class1triggerRef == null_set_id
+  TheoryIdSet class1Tags = class1triggerRef == null_set_id
                                ? 0
                                : getTriggerTermSet(class1triggerRef).d_tags;
   // Trigger set of class 2
   TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id];
-  Theory::Set class2Tags = class2triggerRef == null_set_id
+  TheoryIdSet class2Tags = class2triggerRef == null_set_id
                                ? 0
                                : getTriggerTermSet(class2triggerRef).d_tags;
 
@@ -633,8 +635,10 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
   TaggedEqualitiesSet class1disequalitiesToNotify;
 
   // Individual tags
-  Theory::Set class1OnlyTags = Theory::setDifference(class1Tags, class2Tags);
-  Theory::Set class2OnlyTags = Theory::setDifference(class2Tags, class1Tags);
+  TheoryIdSet class1OnlyTags =
+      TheoryIdSetUtil::setDifference(class1Tags, class2Tags);
+  TheoryIdSet class2OnlyTags =
+      TheoryIdSetUtil::setDifference(class2Tags, class1Tags);
 
   // Only get disequalities if they are not both constant
   if (!class1isConstant || !class2isConstant) {
@@ -760,17 +764,17 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
       TriggerTermSet& class2triggers = getTriggerTermSet(class2triggerRef);
 
       // Initialize the merged set
-      Theory::Set newSetTags =
-          Theory::setUnion(class1triggers.d_tags, class2triggers.d_tags);
+      TheoryIdSet newSetTags = TheoryIdSetUtil::setUnion(class1triggers.d_tags,
+                                                         class2triggers.d_tags);
       EqualityNodeId newSetTriggers[THEORY_LAST];
       unsigned newSetTriggersSize = 0;
 
       int i1 = 0;
       int i2 = 0;
-      Theory::Set tags1 = class1triggers.d_tags;
-      Theory::Set tags2 = class2triggers.d_tags;
-      TheoryId tag1 = Theory::setPop(tags1);
-      TheoryId tag2 = Theory::setPop(tags2);
+      TheoryIdSet tags1 = class1triggers.d_tags;
+      TheoryIdSet tags2 = class2triggers.d_tags;
+      TheoryId tag1 = TheoryIdSetUtil::setPop(tags1);
+      TheoryId tag2 = TheoryIdSetUtil::setPop(tags2);
 
       // Comparing the THEORY_LAST is OK because all other theories are
       // smaller, and will therefore be preferred
@@ -780,12 +784,12 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
           // copy tag1
           newSetTriggers[newSetTriggersSize++] =
               class1triggers.d_triggers[i1++];
-          tag1 = Theory::setPop(tags1);
+          tag1 = TheoryIdSetUtil::setPop(tags1);
         } else if (tag1 > tag2) {
           // copy tag2
           newSetTriggers[newSetTriggersSize++] =
               class2triggers.d_triggers[i2++];
-          tag2 = Theory::setPop(tags2);
+          tag2 = TheoryIdSetUtil::setPop(tags2);
         } else {
           // copy tag1
           EqualityNodeId tag1id = newSetTriggers[newSetTriggersSize++] =
@@ -798,8 +802,8 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
             }
           }
           // Next tags
-          tag1 = Theory::setPop(tags1);
-          tag2 = Theory::setPop(tags2);
+          tag1 = TheoryIdSetUtil::setPop(tags1);
+          tag2 = TheoryIdSetUtil::setPop(tags2);
         }
       }
 
@@ -1252,6 +1256,7 @@ void EqualityEngine::explainPredicate(TNode p, bool polarity,
 
 void EqualityEngine::explainLit(TNode lit, std::vector<TNode>& assumptions)
 {
+  Assert(lit.getKind() != kind::AND);
   bool polarity = lit.getKind() != kind::NOT;
   TNode atom = polarity ? lit : lit[0];
   std::vector<TNode> tassumptions;
@@ -1281,6 +1286,7 @@ void EqualityEngine::explainLit(TNode lit, std::vector<TNode>& assumptions)
     if (std::find(assumptions.begin(), assumptions.end(), a)
         == assumptions.end())
     {
+      Assert(!a.isNull());
       assumptions.push_back(a);
     }
   }
@@ -1288,13 +1294,13 @@ void EqualityEngine::explainLit(TNode lit, std::vector<TNode>& assumptions)
 
 Node EqualityEngine::mkExplainLit(TNode lit)
 {
+  Assert(lit.getKind() != kind::AND);
   std::vector<TNode> assumptions;
   explainLit(lit, assumptions);
   Node ret;
-  NodeManager* nm = NodeManager::currentNM();
   if (assumptions.empty())
   {
-    ret = nm->mkConst(true);
+    ret = NodeManager::currentNM()->mkConst(true);
   }
   else if (assumptions.size() == 1)
   {
@@ -1302,7 +1308,7 @@ Node EqualityEngine::mkExplainLit(TNode lit)
   }
   else
   {
-    ret = nm->mkNode(kind::AND, assumptions);
+    ret = NodeManager::currentNM()->mkNode(kind::AND, assumptions);
   }
   return ret;
 }
@@ -2267,11 +2273,11 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
     // uselists that have been asserted to false. All the representatives appearing on the other
     // side of such disequalities, that have the tag on, are put in a set.
     TaggedEqualitiesSet disequalitiesToNotify;
-    Theory::Set tags = Theory::setInsert(tag);
+    TheoryIdSet tags = TheoryIdSetUtil::setInsert(tag);
     getDisequalities(!d_isConstant[classId], classId, tags, disequalitiesToNotify);
 
     // Trigger data
-    Theory::Set newSetTags;
+    TheoryIdSet newSetTags;
     EqualityNodeId newSetTriggers[THEORY_LAST];
     unsigned newSetTriggersSize;
 
@@ -2280,23 +2286,23 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
       // Get the existing set
       TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef);
       // Initialize the new set for copy/insert
-      newSetTags = Theory::setInsert(tag, triggerSet.d_tags);
+      newSetTags = TheoryIdSetUtil::setInsert(tag, triggerSet.d_tags);
       newSetTriggersSize = 0;
       // Copy into to new one, and insert the new tag/id
       unsigned i = 0;
-      Theory::Set tags2 = newSetTags;
+      TheoryIdSet tags2 = newSetTags;
       TheoryId current;
-      while ((current = Theory::setPop(tags2)) != THEORY_LAST)
+      while ((current = TheoryIdSetUtil::setPop(tags2)) != THEORY_LAST)
       {
         // Remove from the tags
-        tags2 = Theory::setRemove(current, tags2);
+        tags2 = TheoryIdSetUtil::setRemove(current, tags2);
         // Insert the id into the triggers
         newSetTriggers[newSetTriggersSize++] =
             current == tag ? eqNodeId : triggerSet.d_triggers[i++];
       }
     } else {
       // Setup a singleton
-      newSetTags = Theory::setInsert(tag);
+      newSetTags = TheoryIdSetUtil::setInsert(tag);
       newSetTriggers[0] = eqNodeId;
       newSetTriggersSize = 1;
     }
@@ -2326,8 +2332,9 @@ TNode EqualityEngine::getTriggerTermRepresentative(TNode t, TheoryId tag) const
   EqualityNodeId classId = getEqualityNode(t).getFind();
   const TriggerTermSet& triggerSet = getTriggerTermSet(d_nodeIndividualTrigger[classId]);
   unsigned i = 0;
-  Theory::Set tags = triggerSet.d_tags;
-  while (Theory::setPop(tags) != tag) {
+  TheoryIdSet tags = triggerSet.d_tags;
+  while (TheoryIdSetUtil::setPop(tags) != tag)
+  {
     ++ i;
   }
   return d_nodes[triggerSet.d_triggers[i]];
@@ -2381,7 +2388,11 @@ void EqualityEngine::getUseListTerms(TNode t, std::set<TNode>& output) {
   }
 }
 
-EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet(Theory::Set newSetTags, EqualityNodeId* newSetTriggers, unsigned newSetTriggersSize) {
+EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet(
+    TheoryIdSet newSetTags,
+    EqualityNodeId* newSetTriggers,
+    unsigned newSetTriggersSize)
+{
   // Size of the required set
   size_t size = sizeof(TriggerTermSet) + newSetTriggersSize*sizeof(EqualityNodeId);
   // Align the size
@@ -2429,7 +2440,7 @@ bool EqualityEngine::hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId
   }
   Assert(d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end())
       << "We propagated but there is no proof";
-  bool result = Theory::setContains(tag, (*it).second);
+  bool result = TheoryIdSetUtil::setContains(tag, (*it).second);
   Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => " << (result ? "true" : "false") << std::endl;
   return result;
 }
@@ -2446,12 +2457,12 @@ void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhs
   EqualityPair pair2(rhsId, lhsId);
 
   // Store the fact that we've propagated this already
-  Theory::Set notified = 0;
+  TheoryIdSet notified = 0;
   PropagatedDisequalitiesMap::const_iterator find = d_propagatedDisequalities.find(pair1);
   if (find == d_propagatedDisequalities.end()) {
-    notified = Theory::setInsert(tag);
+    notified = TheoryIdSetUtil::setInsert(tag);
   } else {
-    notified = Theory::setInsert(tag, (*find).second);
+    notified = TheoryIdSetUtil::setInsert(tag, (*find).second);
   }
   d_propagatedDisequalities[pair1] = notified;
   d_propagatedDisequalities[pair2] = notified;
@@ -2493,12 +2504,16 @@ void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhs
   }
 }
 
-void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classId, Theory::Set inputTags, TaggedEqualitiesSet& out) {
+void EqualityEngine::getDisequalities(bool allowConstants,
+                                      EqualityNodeId classId,
+                                      TheoryIdSet inputTags,
+                                      TaggedEqualitiesSet& out)
+{
   // Must be empty on input
   Assert(out.size() == 0);
   // The class we are looking for, shouldn't have any of the tags we are looking for already set
   Assert(d_nodeIndividualTrigger[classId] == null_set_id
-         || Theory::setIntersection(
+         || TheoryIdSetUtil::setIntersection(
                 getTriggerTermSet(d_nodeIndividualTrigger[classId]).d_tags,
                 inputTags)
                 == 0);
@@ -2556,8 +2571,8 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI
             // Tags of the other gey
             TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef);
             // We only care if there are things in inputTags that is also in toCompareTags
-            Theory::Set commonTags =
-                Theory::setIntersection(inputTags, toCompareTriggerSet.d_tags);
+            TheoryIdSet commonTags = TheoryIdSetUtil::setIntersection(
+                inputTags, toCompareTriggerSet.d_tags);
             if (commonTags) {
               out.push_back(TaggedEquality(funId, toCompareTriggerSetRef, lhs));
             }
@@ -2573,8 +2588,11 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI
 
 }
 
-bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify) {
-
+bool EqualityEngine::propagateTriggerTermDisequalities(
+    TheoryIdSet tags,
+    TriggerTermSetRef triggerSetRef,
+    const TaggedEqualitiesSet& disequalitiesToNotify)
+{
   // No tags, no food
   if (!tags) {
     return !d_done;
@@ -2592,8 +2610,8 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger
     const TaggedEquality& disequalityInfo = *it;
     const TriggerTermSet& disequalityTriggerSet =
         getTriggerTermSet(disequalityInfo.d_triggerSetRef);
-    Theory::Set commonTags =
-        Theory::setIntersection(disequalityTriggerSet.d_tags, tags);
+    TheoryIdSet commonTags =
+        TheoryIdSetUtil::setIntersection(disequalityTriggerSet.d_tags, tags);
     Assert(commonTags);
     // This is the actual function
     const FunctionApplication& fun =
@@ -2608,7 +2626,10 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger
     }
     // Go through the tags, and add the disequalities
     TheoryId currentTag;
-    while (!d_done && ((currentTag = Theory::setPop(commonTags)) != THEORY_LAST)) {
+    while (
+        !d_done
+        && ((currentTag = TheoryIdSetUtil::setPop(commonTags)) != THEORY_LAST))
+    {
       // Get the tag representative
       EqualityNodeId tagRep = disequalityTriggerSet.getTrigger(currentTag);
       EqualityNodeId myRep = triggerSet.getTrigger(currentTag);
@@ -2636,6 +2657,16 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger
   return !d_done;
 }
 
+TheoryIdSet EqualityEngine::TriggerTermSet::hasTrigger(TheoryId tag) const
+{
+  return TheoryIdSetUtil::setContains(tag, d_tags);
+}
+
+EqualityNodeId EqualityEngine::TriggerTermSet::getTrigger(TheoryId tag) const
+{
+  return d_triggers[TheoryIdSetUtil::setIndex(tag, d_tags)];
+}
+
 } // Namespace uf
 } // Namespace theory
 } // Namespace CVC4
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 91dae2509..19a10eba8 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -32,7 +32,7 @@
 #include "expr/kind_map.h"
 #include "expr/node.h"
 #include "theory/rewriter.h"
-#include "theory/theory.h"
+#include "theory/theory_id.h"
 #include "theory/uf/eq_proof.h"
 #include "theory/uf/equality_engine_iterator.h"
 #include "theory/uf/equality_engine_notify.h"
@@ -500,18 +500,13 @@ private:
   /** Set of trigger terms */
   struct TriggerTermSet {
     /** Set of theories in this set */
-    Theory::Set d_tags;
+    TheoryIdSet d_tags;
     /** The trigger terms */
     EqualityNodeId d_triggers[0];
     /** Returns the theory tags */
-    Theory::Set hasTrigger(TheoryId tag) const
-    {
-      return Theory::setContains(tag, d_tags);
-    }
+    TheoryIdSet hasTrigger(TheoryId tag) const;
     /** Returns a trigger by tag */
-    EqualityNodeId getTrigger(TheoryId tag) const {
-      return d_triggers[Theory::setIndex(tag, d_tags)];
-    }
+    EqualityNodeId getTrigger(TheoryId tag) const;
   };/* struct EqualityEngine::TriggerTermSet */
 
   /** Are the constants triggers */
@@ -535,7 +530,9 @@ private:
   static const TriggerTermSetRef null_set_id = (TriggerTermSetRef)(-1);
 
   /** Create new trigger term set based on the internally set information */
-  TriggerTermSetRef newTriggerTermSet(Theory::Set newSetTags, EqualityNodeId* newSetTriggers, unsigned newSetTriggersSize);
+  TriggerTermSetRef newTriggerTermSet(TheoryIdSet newSetTags,
+                                      EqualityNodeId* newSetTriggers,
+                                      unsigned newSetTriggersSize);
 
   /** Get the trigger set give a reference */
   TriggerTermSet& getTriggerTermSet(TriggerTermSetRef ref) {
@@ -607,7 +604,9 @@ private:
   /**
    * Map from equalities to the tags that have received the notification.
    */
-  typedef context::CDHashMap<EqualityPair, Theory::Set, EqualityPairHashFunction> PropagatedDisequalitiesMap;
+  typedef context::
+      CDHashMap<EqualityPair, TheoryIdSet, EqualityPairHashFunction>
+          PropagatedDisequalitiesMap;
   PropagatedDisequalitiesMap d_propagatedDisequalities;
 
   /**
@@ -659,14 +658,19 @@ private:
    * @param inputTags the tags to filter the equalities
    * @param out the output equalities, as described above
    */
-  void getDisequalities(bool allowConstants, EqualityNodeId classId, Theory::Set inputTags, TaggedEqualitiesSet& out);
+  void getDisequalities(bool allowConstants,
+                        EqualityNodeId classId,
+                        TheoryIdSet inputTags,
+                        TaggedEqualitiesSet& out);
 
   /**
    * Propagates the remembered disequalities with given tags the original triggers for those tags,
    * and the set of disequalities produced by above.
    */
-  bool propagateTriggerTermDisequalities(Theory::Set tags,
-    TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify);
+  bool propagateTriggerTermDisequalities(
+      TheoryIdSet tags,
+      TriggerTermSetRef triggerSetRef,
+      const TaggedEqualitiesSet& disequalitiesToNotify);
 
   /** Name of the equality engine */
   std::string d_name;
@@ -792,8 +796,8 @@ private:
    */
   void explainLit(TNode lit, std::vector<TNode>& assumptions);
   /**
-   * Explain literal, return the conjunction. This method relies on the above
-   * method.
+   * Explain literal, return the explanation as a conjunction. This method
+   * relies on the above method.
    */
   Node mkExplainLit(TNode lit);
   //--------------------------- end standard safe explanation methods
diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h
index dc37808c9..25cb3623b 100644
--- a/src/theory/uf/ho_extension.h
+++ b/src/theory/uf/ho_extension.h
@@ -22,6 +22,7 @@
 #include "context/cdo.h"
 #include "expr/node.h"
 #include "theory/theory_model.h"
+#include "theory/theory_state.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index 2ee379509..b71f72c53 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -21,6 +21,7 @@
 #include <vector>
 
 #include "context/cdhashmap.h"
+#include "context/cdhashset.h"
 #include "expr/lazy_proof.h"
 #include "expr/node.h"
 #include "expr/proof_node.h"