+/********************* */
+/*! \file theory_id.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** 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.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
#include "theory/theory_id.h"
+#include "base/check.h"
+#include "lib/ffs.h"
+
namespace CVC4 {
namespace theory {
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;
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;
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