diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-09 21:25:17 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-09 21:25:17 +0000 |
commit | 1ce0650dcf8ce30424b546deb540974cc510c215 (patch) | |
tree | 74a9985463234fc9adfed2de209c134ed7da359b /src/theory/shared_terms_database.cpp | |
parent | 690fb2843d9845e405fee54eb2d8023eebbd5b72 (diff) |
* simplifying equality engine interface
* notifications are now through the interface subclass instead of a template
* notifications include constants being merged
* changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed
* sat solver now has explicit methods to make true and false constants
* 0-level literals are removed from explanations of propagations
Diffstat (limited to 'src/theory/shared_terms_database.cpp')
-rw-r--r-- | src/theory/shared_terms_database.cpp | 49 |
1 files changed, 10 insertions, 39 deletions
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 577e1b957..4f5475e97 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -16,7 +16,6 @@ **/ #include "theory/shared_terms_database.h" -#include "theory/uf/equality_engine_impl.h" using namespace CVC4; using namespace theory; @@ -36,15 +35,8 @@ SharedTermsDatabase::SharedTermsDatabase(SharedTermsNotifyClass& notify, context 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); @@ -53,9 +45,9 @@ SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException) } } - void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theories) { 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); if (find == d_termsToTheories.end()) { @@ -243,23 +235,21 @@ 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); + d_equalityEngine.assertEquality(atom, false, reason); // !!! need to send this out } else { Assert(!d_equalityEngine.areEqual(atom[0], atom[1])); - d_equalityEngine.addEquality(atom[0], atom[1], reason); + d_equalityEngine.assertEquality(atom, true, reason); } } - static Node mkAnd(const std::vector<TNode>& conjunctions) { Assert(conjunctions.size() > 0); @@ -286,31 +276,12 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) { 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(); + if (literal.getKind() == kind::NOT) { + Assert(literal[0].getKind() == kind::EQUAL); + d_equalityEngine.explainEquality(literal[0][0], literal[0][1], false, assumptions); + } else { + Assert(literal.getKind() == kind::EQUAL); + d_equalityEngine.explainEquality(literal[0], literal[1], true, assumptions); } - d_equalityEngine.explainEquality(lhs, rhs, assumptions); + return mkAnd(assumptions); } |