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.

4 files changed, 103 insertions, 66 deletions

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"