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/term_registration_visitor.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/term_registration_visitor.cpp')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 117 |
1 files changed, 77 insertions, 40 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index bf7cab4e3..b076e72a3 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -26,7 +26,8 @@ std::string PreRegisterVisitor::toString() const { std::stringstream ss; TNodeToTheorySetMap::const_iterator it = d_visited.begin(); for (; it != d_visited.end(); ++ it) { - ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl; + ss << (*it).first << ": " << TheoryIdSetUtil::setToString((*it).second) + << std::endl; } return ss.str(); } @@ -50,8 +51,8 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { TheoryId currentTheoryId = Theory::theoryOf(current); TheoryId parentTheoryId = Theory::theoryOf(parent); - d_theories = Theory::setInsert(currentTheoryId, d_theories); - d_theories = Theory::setInsert(parentTheoryId, d_theories); + d_theories = TheoryIdSetUtil::setInsert(currentTheoryId, d_theories); + d_theories = TheoryIdSetUtil::setInsert(parentTheoryId, d_theories); // Should we use the theory of the type bool useType = false; @@ -78,19 +79,21 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { TNodeToTheorySetMap::iterator find = d_visited.find(current); if (find == d_visited.end()) { if (useType) { - d_theories = Theory::setInsert(typeTheoryId, d_theories); + d_theories = TheoryIdSetUtil::setInsert(typeTheoryId, d_theories); } return false; } - Theory::Set visitedTheories = (*find).second; - if (Theory::setContains(currentTheoryId, visitedTheories)) { + TheoryIdSet visitedTheories = (*find).second; + if (TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories)) + { // The current theory has already visited it, so now it depends on the parent and the type - if (Theory::setContains(parentTheoryId, visitedTheories)) { + if (TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories)) + { if (useType) { TheoryId typeTheoryId2 = Theory::theoryOf(current.getType()); - d_theories = Theory::setInsert(typeTheoryId2, d_theories); - return Theory::setContains(typeTheoryId2, visitedTheories); + d_theories = TheoryIdSetUtil::setInsert(typeTheoryId2, d_theories); + return TheoryIdSetUtil::setContains(typeTheoryId2, visitedTheories); } else { return true; } @@ -133,33 +136,45 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { } } } - - Theory::Set visitedTheories = d_visited[current]; - Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl; - if (!Theory::setContains(currentTheoryId, visitedTheories)) { - visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories); + + TheoryIdSet visitedTheories = d_visited[current]; + Debug("register::internal") + << "PreRegisterVisitor::visit(" << current << "," << parent + << "): previously registered with " + << TheoryIdSetUtil::setToString(visitedTheories) << std::endl; + if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories)) + { + visitedTheories = + TheoryIdSetUtil::setInsert(currentTheoryId, visitedTheories); d_visited[current] = visitedTheories; Theory* th = d_engine->theoryOf(currentTheoryId); th->preRegisterTerm(current); Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl; } - if (!Theory::setContains(parentTheoryId, visitedTheories)) { - visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories); + if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories)) + { + visitedTheories = + TheoryIdSetUtil::setInsert(parentTheoryId, visitedTheories); d_visited[current] = visitedTheories; Theory* th = d_engine->theoryOf(parentTheoryId); th->preRegisterTerm(current); Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } if (useType) { - if (!Theory::setContains(typeTheoryId, visitedTheories)) { - visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories); + if (!TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories)) + { + visitedTheories = + TheoryIdSetUtil::setInsert(typeTheoryId, visitedTheories); d_visited[current] = visitedTheories; Theory* th = d_engine->theoryOf(typeTheoryId); th->preRegisterTerm(current); Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } } - Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl; + Debug("register::internal") + << "PreRegisterVisitor::visit(" << current << "," << parent + << "): now registered with " + << TheoryIdSetUtil::setToString(visitedTheories) << std::endl; Assert(d_visited.find(current) != d_visited.end()); Assert(alreadyVisited(current, parent)); @@ -169,7 +184,8 @@ std::string SharedTermsVisitor::toString() const { std::stringstream ss; TNodeVisitedMap::const_iterator it = d_visited.begin(); for (; it != d_visited.end(); ++ it) { - ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl; + ss << (*it).first << ": " << TheoryIdSetUtil::setToString((*it).second) + << std::endl; } return ss.str(); } @@ -197,7 +213,7 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { return false; } - Theory::Set theories = (*find).second; + TheoryIdSet theories = (*find).second; TheoryId currentTheoryId = Theory::theoryOf(current); TheoryId parentTheoryId = Theory::theoryOf(parent); @@ -239,16 +255,23 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { } } - if (Theory::setContains(currentTheoryId, theories)) { - if (Theory::setContains(parentTheoryId, theories)) { - if (useType) { - return Theory::setContains(typeTheoryId, theories); - } else { - return true; - } - } else { - return false; + if (TheoryIdSetUtil::setContains(currentTheoryId, theories)) + { + if (TheoryIdSetUtil::setContains(parentTheoryId, theories)) + { + if (useType) + { + return TheoryIdSetUtil::setContains(typeTheoryId, theories); } + else + { + return true; + } + } + else + { + return false; + } } else { return false; } @@ -286,29 +309,43 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { } } - Theory::Set visitedTheories = d_visited[current]; - Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl; - if (!Theory::setContains(currentTheoryId, visitedTheories)) { - visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories); + TheoryIdSet visitedTheories = d_visited[current]; + Debug("register::internal") + << "SharedTermsVisitor::visit(" << current << "," << parent + << "): previously registered with " + << TheoryIdSetUtil::setToString(visitedTheories) << std::endl; + if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories)) + { + visitedTheories = + TheoryIdSetUtil::setInsert(currentTheoryId, visitedTheories); Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl; } - if (!Theory::setContains(parentTheoryId, visitedTheories)) { - visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories); + if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories)) + { + visitedTheories = + TheoryIdSetUtil::setInsert(parentTheoryId, visitedTheories); Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } if (useType) { - if (!Theory::setContains(typeTheoryId, visitedTheories)) { - visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories); + if (!TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories)) + { + visitedTheories = + TheoryIdSetUtil::setInsert(typeTheoryId, visitedTheories); Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << typeTheoryId << std::endl; } } - Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl; + Debug("register::internal") + << "SharedTermsVisitor::visit(" << current << "," << parent + << "): now registered with " + << TheoryIdSetUtil::setToString(visitedTheories) << std::endl; // Record the new theories that we visited d_visited[current] = visitedTheories; // If there is more than two theories and a new one has been added notify the shared terms database - if (Theory::setDifference(visitedTheories, Theory::setInsert(currentTheoryId))) { + if (TheoryIdSetUtil::setDifference( + visitedTheories, TheoryIdSetUtil::setInsert(currentTheoryId))) + { d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories); } |