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_engine.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_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index bf74cd016..c61879b6d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -50,6 +50,7 @@ #include "theory/relevance_manager.h" #include "theory/rewriter.h" #include "theory/theory.h" +#include "theory/theory_id.h" #include "theory/theory_model.h" #include "theory/theory_traits.h" #include "theory/uf/equality_engine.h" @@ -308,12 +309,13 @@ void TheoryEngine::preRegister(TNode preprocessed) { Assert(!expr::hasFreeVar(preprocessed)); // Pre-register the terms in the atom - Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run( + theory::TheoryIdSet theories = NodeVisitor<PreRegisterVisitor>::run( d_preRegistrationVisitor, preprocessed); - theories = Theory::setRemove(THEORY_BOOL, theories); + theories = TheoryIdSetUtil::setRemove(THEORY_BOOL, theories); // Remove the top theory, if any more that means multiple theories were // involved - bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories); + bool multipleTheories = + TheoryIdSetUtil::setRemove(Theory::theoryOf(preprocessed), theories); if (Configuration::isAssertionBuild()) { TheoryId i; @@ -324,7 +326,7 @@ void TheoryEngine::preRegister(TNode preprocessed) { // even though arithmetic isn't actually involved. if (!options::finiteModelFind()) { - while ((i = Theory::setPop(theories)) != THEORY_LAST) + while ((i = TheoryIdSetUtil::setPop(theories)) != THEORY_LAST) { if (!d_logicInfo.isTheoryEnabled(i)) { @@ -1074,9 +1076,11 @@ void TheoryEngine::assertFact(TNode literal) SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom); for (; it != it_end; ++ it) { TNode term = *it; - Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term); + theory::TheoryIdSet theories = + d_sharedTerms.getTheoriesToNotify(atom, term); for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++ id) { - if (Theory::setContains(id, theories)) { + if (TheoryIdSetUtil::setContains(id, theories)) + { theoryOf(id)->addSharedTerm(term); } } |