diff options
Diffstat (limited to 'src/theory/shared_terms_database.cpp')
-rw-r--r-- | src/theory/shared_terms_database.cpp | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index b081e27ef..98ab3f10d 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -52,7 +52,7 @@ void SharedTermsDatabase::addEqualityToPropagate(TNode equality) { void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theories) { - Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " << term << ", " << Theory::setToString(theories) << ")" << std::endl; + Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " << term << ", " << Theory::setToString(theories) << ")" << std::endl; std::pair<TNode, TNode> search_pair(atom, term); SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair); @@ -64,18 +64,18 @@ void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theo d_termsToTheories[search_pair] = theories; } else { Assert(theories != (*find).second); - d_termsToTheories[search_pair] = Theory::setUnion(theories, (*find).second); + d_termsToTheories[search_pair] = Theory::setUnion(theories, (*find).second); } } SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::begin(TNode atom) const { Assert(hasSharedTerms(atom)); - return d_atomsToTerms.find(atom)->second.begin(); + return d_atomsToTerms.find(atom)->second.begin(); } SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::end(TNode atom) const { Assert(hasSharedTerms(atom)); - return d_atomsToTerms.find(atom)->second.end(); + return d_atomsToTerms.find(atom)->second.end(); } bool SharedTermsDatabase::hasSharedTerms(TNode atom) const { @@ -89,24 +89,24 @@ void SharedTermsDatabase::backtrack() { list.pop_back(); if (list.empty()) { d_atomsToTerms.erase(atom); - } + } } d_addedSharedTerms.resize(d_addedSharedTermsSize); } Theory::Set SharedTermsDatabase::getTheoriesToNotify(TNode atom, TNode term) const { - // Get the theories that share this term from this atom + // Get the theories that share this term from this atom std::pair<TNode, TNode> search_pair(atom, term); SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair); - Assert(find != d_termsToTheories.end()); - + Assert(find != d_termsToTheories.end()); + // Get the theories that were already notified Theory::Set alreadyNotified = 0; AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term); if (theoriesFind != d_alreadyNotifiedMap.end()) { alreadyNotified = (*theoriesFind).second; } - + // Return the ones that haven't been notified yet return Theory::setDifference((*find).second, alreadyNotified); } |