diff options
Diffstat (limited to 'src/theory/shared_terms_database.cpp')
-rw-r--r-- | src/theory/shared_terms_database.cpp | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 7abc7f1e5..426458202 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -130,7 +130,7 @@ bool SharedTermsDatabase::propagateSharedEquality(TheoryId theory, TNode a, TNod return false; } - // Propagate away + // Propagate away Node equality = a.eqNode(b); if (value) { d_theoryEngine->assertToTheory(equality, theory, THEORY_BUILTIN); @@ -156,20 +156,20 @@ void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) { if (newlyNotified == 0) { return; } - + Debug("shared-terms-database") << "SharedTermsDatabase::markNotified(" << term << ")" << endl; // First update the set of notified theories for this term d_alreadyNotifiedMap[term] = Theory::setUnion(newlyNotified, alreadyNotified); // Mark the shared terms in the equality engine - theory::TheoryId currentTheory; + theory::TheoryId currentTheory; while ((currentTheory = Theory::setPop(newlyNotified)) != THEORY_LAST) { - d_equalityEngine.addTriggerTerm(term, currentTheory); + d_equalityEngine.addTriggerTerm(term, currentTheory); } - + // Check for any conflits - checkForConflict(); + checkForConflict(); } bool SharedTermsDatabase::areEqual(TNode a, TNode b) const { @@ -181,7 +181,7 @@ bool SharedTermsDatabase::areEqual(TNode a, TNode b) const { // since one (or both) of them is a constant, and the other is in the equality engine, they are not same return false; } -} +} bool SharedTermsDatabase::areDisequal(TNode a, TNode b) const { if (d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b)) { @@ -240,7 +240,7 @@ void SharedTermsDatabase::checkForConflict() { std::vector<TNode> assumptions; d_equalityEngine.explainEquality(d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions); Node conflict = mkAnd(assumptions); - d_theoryEngine->conflict(conflict, THEORY_BUILTIN); + d_theoryEngine->conflict(conflict, THEORY_BUILTIN); d_conflictLHS = d_conflictRHS = Node::null(); } } @@ -261,6 +261,9 @@ Node SharedTermsDatabase::explain(TNode literal) const { Assert(atom.getKind() == kind::EQUAL); std::vector<TNode> assumptions; d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); - return mkAnd(assumptions); + return mkAnd(assumptions); } +void SharedTermsDatabase::collectModelInfo( theory::TheoryModel* m, bool fullModel ){ + m->assertEqualityEngine( &d_equalityEngine ); +} |