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.

1 files changed, 77 insertions, 40 deletions

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);
   }