Updates to theory preprocess equality (#5776)

[cvc5.git] / src / theory / theory_id.cpp

diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp
index 2c87458efc194bb601865dcb3ab236f16ad81c74..e9111db8c164d021879d943579285dc6fdc10907 100644 (file)
--- a/src/theory/theory_id.cpp
+++ b/src/theory/theory_id.cpp
@@ -2,10 +2,10 @@
 /*! \file theory_id.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Tim King, Dejan Jovanovic
+ **   Andrew Reynolds, Aina Niemetz, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
@@ -17,6 +17,9 @@
 
 #include "theory/theory_id.h"
 
+#include "base/check.h"
+#include "lib/ffs.h"
+
 namespace CVC4 {
 namespace theory {
 
@@ -40,6 +43,7 @@ std::ostream& operator<<(std::ostream& out, TheoryId theoryId)
     case THEORY_SAT_SOLVER: out << "THEORY_SAT_SOLVER"; break;
     case THEORY_SEP: out << "THEORY_SEP"; break;
     case THEORY_SETS: out << "THEORY_SETS"; break;
+    case THEORY_BAGS: out << "THEORY_BAGS"; break;
     case THEORY_STRINGS: out << "THEORY_STRINGS"; break;
     case THEORY_QUANTIFIERS: out << "THEORY_QUANTIFIERS"; break;
 
@@ -62,6 +66,7 @@ std::string getStatsPrefix(TheoryId theoryId)
     case THEORY_DATATYPES: return "theory::datatypes"; break;
     case THEORY_SEP: return "theory::sep"; break;
     case THEORY_SETS: return "theory::sets"; break;
+    case THEORY_BAGS: return "theory::bags"; break;
     case THEORY_STRINGS: return "theory::strings"; break;
     case THEORY_QUANTIFIERS: return "theory::quantifiers"; break;
 
@@ -70,5 +75,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