diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-14 15:13:05 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-14 15:13:05 +0000 |
commit | 4c49dd9bcc859a07bebf969ee126ee2f4ffa2384 (patch) | |
tree | ed8d169dcc089b5d3dd7b195ac6cc1b077a3559a /src/theory/term_registration_visitor.cpp | |
parent | 39c17191ad88a50bfffdbbc5ed8b493ad99b3fb5 (diff) |
fixing up preregistration again
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 46 |
1 files changed, 17 insertions, 29 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 75426cba4..0f8822e72 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -40,21 +40,17 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { return false; } - Theory::Set theories; - TheoryId currentTheoryId = Theory::theoryOf(current); TheoryId parentTheoryId = Theory::theoryOf(parent); - // Remember the theories interested in this term - d_theories[parent] = theories = Theory::setInsert(currentTheoryId, d_theories[parent]); - // Check if there are multiple of those - d_multipleTheories = d_multipleTheories || Theory::setRemove(parentTheoryId, theories); + d_theories = Theory::setInsert(currentTheoryId, d_theories); + d_theories = Theory::setInsert(parentTheoryId, d_theories); - theories = (*find).second; - if (Theory::setContains(currentTheoryId, theories)) { + Theory::Set visitedTheories = (*find).second; + if (Theory::setContains(currentTheoryId, visitedTheories)) { // The current theory has already visited it, so now it depends on the parent - Debug("register::internal") << (Theory::setContains(parentTheoryId, theories) ? "2:true" : "2:false") << std::endl; - return Theory::setContains(parentTheoryId, theories); + Debug("register::internal") << (Theory::setContains(parentTheoryId, visitedTheories) ? "2:true" : "2:false") << std::endl; + return Theory::setContains(parentTheoryId, visitedTheories); } else { // If the current theory is not registered, it still needs to be visited Debug("register::internal") << "3:false" << std::endl; @@ -64,8 +60,6 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { void PreRegisterVisitor::visit(TNode current, TNode parent) { - Theory::Set theories; - Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl; if (Debug.isOn("register::internal")) { Debug("register::internal") << toString() << std::endl; @@ -75,24 +69,21 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { TheoryId currentTheoryId = Theory::theoryOf(current); TheoryId parentTheoryId = Theory::theoryOf(parent); - // Remember the theories interested in this term - d_theories[parent] = theories = Theory::setInsert(currentTheoryId, d_theories[parent]); - // If there are theories other than the parent itself, we are in multi-theory case - d_multipleTheories = d_multipleTheories || Theory::setRemove(parentTheoryId, theories); - - theories = d_visited[current]; - Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(theories) << std::endl; - if (!Theory::setContains(currentTheoryId, theories)) { - d_visited[current] = theories = Theory::setInsert(currentTheoryId, theories); + 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); + d_visited[current] = visitedTheories; d_engine->theoryOf(currentTheoryId)->preRegisterTerm(current); Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl; } - if (!Theory::setContains(parentTheoryId, theories)) { - d_visited[current] = theories = Theory::setInsert(parentTheoryId, theories); + if (!Theory::setContains(parentTheoryId, visitedTheories)) { + visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories); + d_visited[current] = visitedTheories; d_engine->theoryOf(parentTheoryId)->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(theories) << std::endl; + Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl; Assert(d_visited.find(current) != d_visited.end()); Assert(alreadyVisited(current, parent)); @@ -103,11 +94,8 @@ void PreRegisterVisitor::start(TNode node) { } bool PreRegisterVisitor::done(TNode node) { -// <<<<<<< .working -// d_engine->markActive(d_theories[node]); -// ======= -// >>>>>>> .merge-right.r3396 - return d_multipleTheories; + // We have multiple theories if removing the node theory from others is non-empty + return Theory::setRemove(Theory::theoryOf(node), d_theories); } std::string SharedTermsVisitor::toString() const { |