diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-31 17:15:02 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-31 17:15:02 +0000 |
commit | e0ea9a22721a332be2a2354846ffdf5f72c6a6de (patch) | |
tree | 97f277ac1e6a203a3da3cfb5c41924bad86cc942 /src/theory/bv | |
parent | 48de3ac52d0fb8656b6e4e768c74be4be3b2a883 (diff) |
Fixed bug in bv: one more case where non-shared equality was getting propagated
Added a global push and pop around solving - fixes an assertion failure when
TNodes are still around in a CDHashMap at destruction time.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 33 |
1 files changed, 23 insertions, 10 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 79ab955aa..251650bf2 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -148,12 +148,13 @@ void TheoryBV::propagate(Effort e) { Node normalized = Rewriter::rewrite(literal); TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; - // check if it's a shared equality in the current context - if (atom.getKind() != kind::EQUAL || d_valuation.isSatLiteral(normalized) || - (d_sharedTermsSet.find(atom[0]) != d_sharedTermsSet.end() && - d_sharedTermsSet.find(atom[1]) != d_sharedTermsSet.end())) { - - bool satValue; + bool isSharedLiteral = (atom.getKind() == kind::EQUAL && + (d_sharedTermsSet.find(atom[0]) != d_sharedTermsSet.end() && + d_sharedTermsSet.find(atom[1]) != d_sharedTermsSet.end())); + + // Check if this is a SAT literal + if (d_valuation.isSatLiteral(normalized)) { + bool satValue = false; if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { // check if we already propagated the negation Node negLiteral = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal); @@ -166,11 +167,16 @@ void TheoryBV::propagate(Effort e) { setConflict(mkAnd(assumptions)); return; } - - BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << literal << std::endl; - d_out->propagate(literal); - d_alreadyPropagatedSet.insert(literal); + // If it's not a shared literal and hasn't already been set to true, we propagate the normalized version + // shared literals are handled below + if (!isSharedLiteral && !satValue) { + BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << normalized << std::endl; + d_out->propagate(normalized); + d_alreadyPropagatedSet.insert(normalized); + return; + } } else { + // Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl; Node negatedLiteral; std::vector<TNode> assumptions; @@ -181,9 +187,16 @@ void TheoryBV::propagate(Effort e) { return; } } + // Either it was not a SAT literal or it was but it is also shared - in that case we have to propagate the original literal (not the normalized one) + if (isSharedLiteral) { + BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << literal << std::endl; + d_out->propagate(literal); + d_alreadyPropagatedSet.insert(literal); + } } } + Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { switch(in.getKind()) { case kind::EQUAL: |