diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-04-27 19:26:01 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-04-27 19:26:01 +0000 |
commit | 0168ec9f128246d1a6a0a34f7ee59aec109b7782 (patch) | |
tree | eae4e1fbe2970feb917c1e26b3b6036152ceca28 /src/theory/shared_terms_database.cpp | |
parent | f813ed144b0945334e03bfd769ea3c2cf8b75843 (diff) |
Fixed warning in decision_engine.h, minor tweak to caregraph function in
arrays, fixed bug with equalities between constants in shared terms database
Diffstat (limited to 'src/theory/shared_terms_database.cpp')
-rw-r--r-- | src/theory/shared_terms_database.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 24cbc165c..577e1b957 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -204,11 +204,9 @@ void SharedTermsDatabase::mergeSharedTerms(TNode a, TNode b) // Normalize the equality Node equality = left.eqNode(right); Node normalized = Rewriter::rewriteEquality(currentTheory, equality); - if (normalized.getKind() != kind::CONST_BOOLEAN) { + if (normalized.getKind() != kind::CONST_BOOLEAN || !normalized.getConst<bool>()) { // Notify client d_sharedNotify.notify(normalized, equality, currentTheory); - } else { - Assert(equality.getConst<bool>()); } } @@ -253,6 +251,7 @@ void SharedTermsDatabase::processSharedLiteral(TNode literal, TNode reason) if (negated) { Assert(!d_equalityEngine.areDisequal(atom[0], atom[1])); d_equalityEngine.addDisequality(atom[0], atom[1], reason); + // !!! need to send this out } else { Assert(!d_equalityEngine.areEqual(atom[0], atom[1])); |