diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-14 19:46:22 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-14 19:46:22 +0000 |
commit | c1410887627654fad536492d52d3c80cd1082575 (patch) | |
tree | 2b6b832b920c981a0a4c51569fd4562b8c382e81 /src | |
parent | b849eeef09465da1100cd6a94beacc893849fb25 (diff) |
fixes for the hasTerm issues in the shared database under the decision heuristic
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/shared_terms_database.cpp | 18 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 2 |
2 files changed, 18 insertions, 2 deletions
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"); |