diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
commit | d01d291be3213368985f28d0072905c4f033d5ff (patch) | |
tree | 8524a2b6a00c012221ecca9266c3ab9fb11989ed /src/theory/shared_terms_database.cpp | |
parent | 889853e225687dfef36b15ca1dccf74682e0fd66 (diff) |
merge from arrays-clark branch
Diffstat (limited to 'src/theory/shared_terms_database.cpp')
-rw-r--r-- | src/theory/shared_terms_database.cpp | 226 |
1 files changed, 224 insertions, 2 deletions
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 1687f3480..24cbc165c 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -16,9 +16,43 @@ **/ #include "theory/shared_terms_database.h" +#include "theory/uf/equality_engine_impl.h" using namespace CVC4; -using namespace CVC4::theory; +using namespace theory; + +SharedTermsDatabase::SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context) + : ContextNotifyObj(context), + d_context(context), + d_statSharedTerms("theory::shared_terms", 0), + d_addedSharedTermsSize(context, 0), + d_termsToTheories(context), + d_alreadyNotifiedMap(context), + d_sharedNotify(notify), + d_termToNotifyList(context), + d_allocatedNLSize(0), + d_allocatedNLNext(context, 0), + d_EENotify(*this), + d_equalityEngine(d_EENotify, context, "SharedTermsDatabase") +{ + StatisticsRegistry::registerStat(&d_statSharedTerms); + NodeManager* nm = NodeManager::currentNM(); + d_true = nm->mkConst<bool>(true); + d_false = nm->mkConst<bool>(false); + d_equalityEngine.addTerm(d_true); + d_equalityEngine.addTerm(d_false); + d_equalityEngine.addTriggerEquality(d_true, d_false, d_false); +} + + +SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException) +{ + StatisticsRegistry::unregisterStat(&d_statSharedTerms); + for (unsigned i = 0; i < d_allocatedNLSize; ++i) { + d_allocatedNL[i]->deleteSelf(); + } +} + void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theories) { Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " << term << ", " << Theory::setToString(theories) << ")" << std::endl; @@ -30,6 +64,9 @@ void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theo d_addedSharedTerms.push_back(atom); d_addedSharedTermsSize = d_addedSharedTermsSize + 1; d_termsToTheories[search_pair] = theories; + if (!d_equalityEngine.hasTerm(term)) { + d_equalityEngine.addTriggerTerm(term); + } } else { Assert(theories != (*find).second); d_termsToTheories[search_pair] = Theory::setUnion(theories, (*find).second); @@ -79,6 +116,7 @@ Theory::Set SharedTermsDatabase::getTheoriesToNotify(TNode atom, TNode term) con return Theory::setDifference((*find).second, alreadyNotified); } + Theory::Set SharedTermsDatabase::getNotifiedTheories(TNode term) const { // Get the theories that were already notified AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term); @@ -89,7 +127,191 @@ Theory::Set SharedTermsDatabase::getNotifiedTheories(TNode term) const { } } + +SharedTermsDatabase::NotifyList* SharedTermsDatabase::getNewNotifyList() +{ + NotifyList* retval; + if (d_allocatedNLSize == d_allocatedNLNext) { + retval = new (true) NotifyList(d_context); + d_allocatedNL.push_back(retval); + d_allocatedNLNext = ++d_allocatedNLSize; + } + else { + retval = d_allocatedNL[d_allocatedNLNext]; + d_allocatedNLNext = d_allocatedNLNext + 1; + } + Assert(retval->empty()); + return retval; +} + + +void SharedTermsDatabase::mergeSharedTerms(TNode a, TNode b) +{ + // Note: a is the new representative + + NotifyList* pnlLeft = NULL; + NotifyList* pnlRight = NULL; + + TermToNotifyList::iterator it = d_termToNotifyList.find(a); + if (it == d_termToNotifyList.end()) { + pnlLeft = getNewNotifyList(); + d_termToNotifyList[a] = pnlLeft; + } + else { + pnlLeft = (*it).second; + } + it = d_termToNotifyList.find(b); + if (it != d_termToNotifyList.end()) { + pnlRight = (*it).second; + } + + // Get theories interested in EC for lhs + Theory::Set lhsSet = getNotifiedTheories(a); + Theory::Set rhsSet = getNotifiedTheories(b); + NotifyList::iterator nit; + TNode left, right; + + for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) { + + if (Theory::setContains(currentTheory, rhsSet)) { + right = b; + } + else if (pnlRight != NULL && + ((nit = pnlRight->end()) != pnlRight->end())) { + right = (*nit).second; + } + else { + // no match for right: continue + continue; + } + + if (Theory::setContains(currentTheory, lhsSet)) { + left = a; + } + else if ((nit = pnlLeft->find(currentTheory)) != pnlLeft->end()) { + left = (*nit).second; + } + else { + // no match for left: insert right into left + (*pnlLeft)[currentTheory] = right; + continue; + } + + // New shared equality: notify the client + + // TODO: add propagation of disequalities? + + // Normalize the equality + Node equality = left.eqNode(right); + Node normalized = Rewriter::rewriteEquality(currentTheory, equality); + if (normalized.getKind() != kind::CONST_BOOLEAN) { + // Notify client + d_sharedNotify.notify(normalized, equality, currentTheory); + } else { + Assert(equality.getConst<bool>()); + } + } + +} + + void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) { - d_alreadyNotifiedMap[term] = Theory::setUnion(theories, d_alreadyNotifiedMap[term]); + Theory::Set alreadyNotified = d_alreadyNotifiedMap[term]; + Theory::Set newlyNotified = Theory::setDifference(theories, alreadyNotified); + if (newlyNotified != 0) { + TNode rep = d_equalityEngine.getRepresentative(term); + if (rep != term) { + TermToNotifyList::iterator it = d_termToNotifyList.find(rep); + Assert(it != d_termToNotifyList.end()); + NotifyList* pnl = (*it).second; + for (TheoryId theory = THEORY_FIRST; theory != THEORY_LAST; ++ theory) { + if (Theory::setContains(theory, newlyNotified) && + pnl->find(theory) == pnl->end()) { + (*pnl)[theory] = term; + } + } + } + } + d_alreadyNotifiedMap[term] = Theory::setUnion(newlyNotified, alreadyNotified); +} + + +bool SharedTermsDatabase::areEqual(TNode a, TNode b) { + return d_equalityEngine.areEqual(a,b); +} + + +bool SharedTermsDatabase::areDisequal(TNode a, TNode b) { + return d_equalityEngine.areDisequal(a,b); +} + + +void SharedTermsDatabase::processSharedLiteral(TNode literal, TNode reason) +{ + bool negated = literal.getKind() == kind::NOT; + TNode atom = negated ? literal[0] : literal; + if (negated) { + Assert(!d_equalityEngine.areDisequal(atom[0], atom[1])); + d_equalityEngine.addDisequality(atom[0], atom[1], reason); + } + else { + Assert(!d_equalityEngine.areEqual(atom[0], atom[1])); + d_equalityEngine.addEquality(atom[0], atom[1], reason); + } } + +static Node mkAnd(const std::vector<TNode>& conjunctions) { + Assert(conjunctions.size() > 0); + + std::set<TNode> all; + all.insert(conjunctions.begin(), conjunctions.end()); + + if (all.size() == 1) { + // All the same, or just one + return conjunctions[0]; + } + + NodeBuilder<> conjunction(kind::AND); + std::set<TNode>::const_iterator it = all.begin(); + std::set<TNode>::const_iterator it_end = all.end(); + while (it != it_end) { + conjunction << *it; + ++ it; + } + + return conjunction; +}/* mkAnd() */ + + +Node SharedTermsDatabase::explain(TNode literal) +{ + std::vector<TNode> assumptions; + explain(literal, assumptions); + return mkAnd(assumptions); +} + + +void SharedTermsDatabase::explain(TNode literal, std::vector<TNode>& assumptions) { + TNode lhs, rhs; + switch (literal.getKind()) { + case kind::EQUAL: + lhs = literal[0]; + rhs = literal[1]; + break; + case kind::NOT: + if (literal[0].getKind() == kind::EQUAL) { + // Disequalities + d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions); + return; + } + case kind::CONST_BOOLEAN: + // we get to explain true = false, since we set false to be the trigger of this + lhs = d_true; + rhs = d_false; + break; + default: + Unreachable(); + } + d_equalityEngine.explainEquality(lhs, rhs, assumptions); +} |