From c1410887627654fad536492d52d3c80cd1082575 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Thu, 14 Jun 2012 19:46:22 +0000 Subject: fixes for the hasTerm issues in the shared database under the decision heuristic --- src/theory/shared_terms_database.cpp | 18 ++++++++++++++++-- src/theory/theory_engine.cpp | 2 ++ 2 files changed, 18 insertions(+), 2 deletions(-) (limited to 'src/theory') diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index c1266ee6d..7abc7f1e5 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -173,11 +173,25 @@ void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) { } bool SharedTermsDatabase::areEqual(TNode a, TNode b) const { - return d_equalityEngine.areEqual(a,b); + if (d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b)) { + return d_equalityEngine.areEqual(a,b); + } else { + Assert(d_equalityEngine.hasTerm(a) || a.isConst()); + Assert(d_equalityEngine.hasTerm(b) || b.isConst()); + // 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 { - return d_equalityEngine.areDisequal(a,b,false); + if (d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b)) { + return d_equalityEngine.areDisequal(a,b,false); + } else { + Assert(d_equalityEngine.hasTerm(a) || a.isConst()); + Assert(d_equalityEngine.hasTerm(b) || b.isConst()); + // one (or both) are in the equality engine + return false; + } } void SharedTermsDatabase::assertEquality(TNode equality, bool polarity, TNode reason) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 060d48230..557acae95 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -390,6 +390,8 @@ void TheoryEngine::combineTheories() { Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << std::endl; + Assert(d_sharedTerms.isShared(carePair.a) || carePair.a.isConst()); + Assert(d_sharedTerms.isShared(carePair.b) || carePair.b.isConst()); Assert(!d_sharedTerms.areEqual(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); Assert(!d_sharedTerms.areDisequal(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); -- cgit v1.2.3