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, 10 insertions, 6 deletions

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