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, 20 insertions, 16 deletions

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