1 files changed, 87 insertions, 0 deletions
diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp
index 2c87458ef..a801e4abb 100644
--- a/src/theory/theory_id.cpp
+++ b/src/theory/theory_id.cpp
@@ -17,6 +17,9 @@
 
 #include "theory/theory_id.h"
 
+#include "base/check.h"
+#include "lib/ffs.h"
+
 namespace CVC4 {
 namespace theory {
 
@@ -70,5 +73,89 @@ std::string getStatsPrefix(TheoryId theoryId)
   return "unknown";
 }
 
+TheoryId TheoryIdSetUtil::setPop(TheoryIdSet& set)
+{
+  uint32_t i = ffs(set);  // Find First Set (bit)
+  if (i == 0)
+  {
+    return THEORY_LAST;
+  }
+  TheoryId id = static_cast<TheoryId>(i - 1);
+  set = setRemove(id, set);
+  return id;
+}
+
+size_t TheoryIdSetUtil::setSize(TheoryIdSet set)
+{
+  size_t count = 0;
+  while (setPop(set) != THEORY_LAST)
+  {
+    ++count;
+  }
+  return count;
+}
+
+size_t TheoryIdSetUtil::setIndex(TheoryId id, TheoryIdSet set)
+{
+  Assert(setContains(id, set));
+  size_t count = 0;
+  while (setPop(set) != id)
+  {
+    ++count;
+  }
+  return count;
+}
+
+TheoryIdSet TheoryIdSetUtil::setInsert(TheoryId theory, TheoryIdSet set)
+{
+  return set | (1 << theory);
+}
+
+TheoryIdSet TheoryIdSetUtil::setRemove(TheoryId theory, TheoryIdSet set)
+{
+  return setDifference(set, setInsert(theory));
+}
+
+bool TheoryIdSetUtil::setContains(TheoryId theory, TheoryIdSet set)
+{
+  return set & (1 << theory);
+}
+
+TheoryIdSet TheoryIdSetUtil::setComplement(TheoryIdSet a)
+{
+  return (~a) & AllTheories;
+}
+
+TheoryIdSet TheoryIdSetUtil::setIntersection(TheoryIdSet a, TheoryIdSet b)
+{
+  return a & b;
+}
+
+TheoryIdSet TheoryIdSetUtil::setUnion(TheoryIdSet a, TheoryIdSet b)
+{
+  return a | b;
+}
+
+TheoryIdSet TheoryIdSetUtil::setDifference(TheoryIdSet a, TheoryIdSet b)
+{
+  return (~b) & a;
+}
+
+std::string TheoryIdSetUtil::setToString(TheoryIdSet theorySet)
+{
+  std::stringstream ss;
+  ss << "[";
+  for (unsigned theoryId = 0; theoryId < THEORY_LAST; ++theoryId)
+  {
+    TheoryId tid = static_cast<TheoryId>(theoryId);
+    if (setContains(tid, theorySet))
+    {
+      ss << tid << " ";
+    }
+  }
+  ss << "]";
+  return ss.str();
+}
+
 }  // namespace theory
 }  // namespace CVC4