diff options
author | Tim King <taking@cs.nyu.edu> | 2012-05-15 21:20:56 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-05-15 21:20:56 +0000 |
commit | 7871d62e49f8ae6ad02793c2bd47b2b31e83ed64 (patch) | |
tree | 7f623ca3dd1040db2ca0bba3f2b8969ec27e5d15 /src/theory/term_registration_visitor.cpp | |
parent | 49c07e26bae748fae3bdc2dadc742a3036e39b3f (diff) |
Fix to shared terms visitor.
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 7d82dee8e..4a2a5f135 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -179,36 +179,30 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { bool useType = current != parent && currentTheoryId != parentTheoryId; - unsigned newTheoriesCount = 0; 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); - newTheoriesCount ++; Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl; } if (!Theory::setContains(parentTheoryId, visitedTheories)) { visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories); - newTheoriesCount ++; Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } if (useType) { TheoryId typeTheoryId = Theory::theoryOf(current.getType()); if (!Theory::setContains(typeTheoryId, visitedTheories)) { visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories); - newTheoriesCount ++; 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; // Record the new theories that we visited - if (newTheoriesCount > 0) { - d_visited[current] = visitedTheories; - } + d_visited[current] = visitedTheories; // If there is more than two theories and a new one has been added notify the shared terms database - if (newTheoriesCount > 1) { + if (Theory::setDifference(visitedTheories, Theory::setInsert(currentTheoryId))) { d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories); } |