diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/shared_terms_database.cpp | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
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); } |