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/theory/shared_terms_database.cpp | |
parent | b849eeef09465da1100cd6a94beacc893849fb25 (diff) |
fixes for the hasTerm issues in the shared database under the decision heuristic
Diffstat (limited to 'src/theory/shared_terms_database.cpp')
-rw-r--r-- | src/theory/shared_terms_database.cpp | 18 |
1 files changed, 16 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) |