diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-28 18:01:34 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-28 18:01:34 -0500 |
commit | 960147384b7953a352ca9c721f9b93bdac4ff178 (patch) | |
tree | 2bbc6df18d6cebbe94f9cce9732fcc6c6096e341 /src/theory/theory_id.cpp | |
parent | 48dfcfd271ff9fa04766e29fb82ba83290da1ad8 (diff) |
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.
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 |