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.h | |
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.h')
-rw-r--r-- | src/theory/theory_id.h | 48 |
1 files changed, 47 insertions, 1 deletions
diff --git a/src/theory/theory_id.h b/src/theory/theory_id.h index 005380352..452dd09a9 100644 --- a/src/theory/theory_id.h +++ b/src/theory/theory_id.h @@ -23,7 +23,6 @@ #include <iostream> namespace CVC4 { - namespace theory { /** @@ -58,6 +57,53 @@ std::ostream& operator<<(std::ostream& out, TheoryId theoryId); std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC; +/** + * A set of theories. Utilities for TheoryIdSet can be found below. + */ +typedef uint32_t TheoryIdSet; + +class TheoryIdSetUtil +{ + public: + /** A set of all theories */ + static const TheoryIdSet AllTheories = (1 << theory::THEORY_LAST) - 1; + + /** Pops a first theory off the set */ + static TheoryId setPop(TheoryIdSet& set); + + /** Returns the size of a set of theories */ + static size_t setSize(TheoryIdSet set); + + /** Returns the index size of a set of theories */ + static size_t setIndex(TheoryId id, TheoryIdSet set); + + /** Add the theory to the set. If no set specified, just returns a singleton + * set */ + static TheoryIdSet setInsert(TheoryId theory, TheoryIdSet set = 0); + + /** Add the theory to the set. If no set specified, just returns a singleton + * set */ + static TheoryIdSet setRemove(TheoryId theory, TheoryIdSet set = 0); + + /** Check if the set contains the theory */ + static bool setContains(TheoryId theory, TheoryIdSet set); + + /** Set complement of a */ + static TheoryIdSet setComplement(TheoryIdSet a); + + /** Set intersection of a and b */ + static TheoryIdSet setIntersection(TheoryIdSet a, TheoryIdSet b); + + /** Set union of a and b */ + static TheoryIdSet setUnion(TheoryIdSet a, TheoryIdSet b); + + /** Set difference of a and b */ + static TheoryIdSet setDifference(TheoryIdSet a, TheoryIdSet b); + + /** Convert theorySet to string (for debugging) */ + static std::string setToString(TheoryIdSet theorySet); +}; + } // namespace theory } // namespace CVC4 #endif |