diff options
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 79 |
1 files changed, 0 insertions, 79 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 29a3a0998..c5fcf362c 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -30,7 +30,6 @@ #include "context/cdo.h" #include "context/context.h" #include "expr/node.h" -#include "lib/ffs.h" #include "options/options.h" #include "options/theory_options.h" #include "smt/command.h" @@ -799,84 +798,6 @@ class Theory { << " doesn't support Theory::setUserAttribute interface"; } - /** A set of theories */ - typedef uint32_t Set; - - /** A set of all theories */ - static const Set AllTheories = (1 << theory::THEORY_LAST) - 1; - - /** Pops a first theory off the set */ - static inline TheoryId setPop(Set& set) { - uint32_t i = ffs(set); // Find First Set (bit) - if (i == 0) { return THEORY_LAST; } - TheoryId id = (TheoryId)(i-1); - set = setRemove(id, set); - return id; - } - - /** Returns the size of a set of theories */ - static inline size_t setSize(Set set) { - size_t count = 0; - while (setPop(set) != THEORY_LAST) { - ++ count; - } - return count; - } - - /** Returns the index size of a set of theories */ - static inline size_t setIndex(TheoryId id, Set set) { - Assert(setContains(id, set)); - size_t count = 0; - while (setPop(set) != id) { - ++ count; - } - return count; - } - - /** Add the theory to the set. If no set specified, just returns a singleton set */ - static inline Set setInsert(TheoryId theory, Set set = 0) { - return set | (1 << theory); - } - - /** Add the theory to the set. If no set specified, just returns a singleton set */ - static inline Set setRemove(TheoryId theory, Set set = 0) { - return setDifference(set, setInsert(theory)); - } - - /** Check if the set contains the theory */ - static inline bool setContains(TheoryId theory, Set set) { - return set & (1 << theory); - } - - static inline Set setComplement(Set a) { - return (~a) & AllTheories; - } - - static inline Set setIntersection(Set a, Set b) { - return a & b; - } - - static inline Set setUnion(Set a, Set b) { - return a | b; - } - - /** a - b */ - static inline Set setDifference(Set a, Set b) { - return (~b) & a; - } - - static inline std::string setToString(theory::Theory::Set theorySet) { - std::stringstream ss; - ss << "["; - for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { - if (theory::Theory::setContains((theory::TheoryId)theoryId, theorySet)) { - ss << (theory::TheoryId) theoryId << " "; - } - } - ss << "]"; - return ss.str(); - } - typedef context::CDList<Assertion>::const_iterator assertions_iterator; /** |