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, 47 insertions, 1 deletions

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