diff options
Diffstat (limited to 'src/theory/theory_id.cpp')
-rw-r--r-- | src/theory/theory_id.cpp | 87 |
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 |