diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-05-15 00:11:07 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-05-15 00:11:07 +0000 |
commit | 77ff33bc6be64f338f035bd9d077737f83280944 (patch) | |
tree | 3593a4f931ca107cdcb9b2e6891f7008f6d3be76 /src/theory/bv | |
parent | 5b5a421d79d12a31edde3902f2b8ddec6a3ca684 (diff) |
several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify and now term notify handles boolean constants; fixed bug 328
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 65 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 21 |
2 files changed, 60 insertions, 26 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index bbbfdc1ad..5ca1594ee 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -39,6 +39,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& : Theory(THEORY_BV, c, u, out, valuation, logicInfo), d_context(c), d_assertions(c), + d_bitblastQueue(c), d_bitblaster(new Bitblaster(c, this) ), d_alreadyPropagatedSet(c), d_sharedTermsSet(c), @@ -114,12 +115,13 @@ void TheoryBV::preRegisterTerm(TNode node) { return; } - if (node.getKind() == kind::EQUAL || - node.getKind() == kind::BITVECTOR_ULT || - node.getKind() == kind::BITVECTOR_ULE || - node.getKind() == kind::BITVECTOR_SLT || - node.getKind() == kind::BITVECTOR_SLE) { - d_bitblaster->bbAtom(node); + if ((node.getKind() == kind::EQUAL || + node.getKind() == kind::BITVECTOR_ULT || + node.getKind() == kind::BITVECTOR_ULE || + node.getKind() == kind::BITVECTOR_SLT || + node.getKind() == kind::BITVECTOR_SLE) && + !d_bitblaster->hasBBAtom(node)) { + d_bitblastQueue.push_back(node); } if (d_useEqualityEngine) { @@ -157,11 +159,21 @@ void TheoryBV::check(Effort e) return; } + // getting the new assertions + + std::vector<TNode> new_assertions; while (!done() && !d_conflict) { Assertion assertion = get(); TNode fact = assertion.assertion; - + new_assertions.push_back(fact); BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; + } + + // sending assertions to equality engine first + + for (unsigned i = 0; i < new_assertions.size(); ++i) { + TNode fact = new_assertions[i]; + TypeNode factType = fact[0].getType(); // Notify the equality engine if (d_useEqualityEngine && !d_conflict && !propagatedBy(fact, SUB_EQUALITY) ) { @@ -183,7 +195,24 @@ void TheoryBV::check(Effort e) } } - // Bit-blaster + // checking for a conflict + if (d_conflict) { + BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode; + d_out->conflict(d_conflictNode); + return; + } + } + + // bit-blasting atoms on queue + + for (unsigned i = 0; i < d_bitblastQueue.size(); ++i) { + d_bitblaster->bbAtom(d_bitblastQueue[i]); + // would be nice to clear the bitblastQueue? + } + + // bit-blaster propagation + for (unsigned i = 0; i < new_assertions.size(); ++i) { + TNode fact = new_assertions[i]; if (!d_conflict && !propagatedBy(fact, SUB_BITBLASTER)) { // Some atoms have not been bit-blasted yet d_bitblaster->bbAtom(fact); @@ -202,7 +231,7 @@ void TheoryBV::check(Effort e) // If in conflict, output the conflict if (d_conflict) { - BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode; + BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode; d_out->conflict(d_conflictNode); return; } @@ -242,7 +271,7 @@ Node TheoryBV::getValue(TNode n) { void TheoryBV::propagate(Effort e) { - BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate()" << std::endl; + BVDebug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl; if (d_conflict) { return; @@ -266,7 +295,7 @@ void TheoryBV::propagate(Effort e) { // check if we already propagated the negation Node negLiteral = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal); if (d_alreadyPropagatedSet.find(negLiteral) != d_alreadyPropagatedSet.end()) { - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict " << literal << " and its negation both propagated \n"; + Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict " << literal << " and its negation both propagated \n"; // we are in conflict std::vector<TNode> assumptions; explain(literal, assumptions); @@ -276,11 +305,11 @@ void TheoryBV::propagate(Effort e) { return; } - BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): " << literal << std::endl; + BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << literal << std::endl; d_out->propagate(literal); d_alreadyPropagatedSet.insert(literal); } else { - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl; + Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl; Node negatedLiteral; std::vector<TNode> assumptions; @@ -324,11 +353,11 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) { - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ")" << std::endl; + Debug("bitvector") << indent() << "TheoryBV::storePropagation(" << literal << ")" << std::endl; // If already in conflict, no more propagation if (d_conflict) { - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << "): already in conflict" << std::endl; + Debug("bitvector") << indent() << "TheoryBV::storePropagation(" << literal << "): already in conflict" << std::endl; return false; } @@ -346,7 +375,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) // If asserted, we might be in conflict if (hasSatValue && !satValue) { - Debug("bitvector-prop") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ") => conflict" << std::endl; + Debug("bitvector-prop") << indent() << "TheoryBV::storePropagation(" << literal << ") => conflict" << std::endl; std::vector<TNode> assumptions; Node negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode(); assumptions.push_back(negatedLiteral); @@ -357,7 +386,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) } // Nothing, just enqueue it for propagation and mark it as asserted already - Debug("bitvector-prop") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ") => enqueuing for propagation" << std::endl; + Debug("bitvector-prop") << indent() << "TheoryBV::storePropagation(" << literal << ") => enqueuing for propagation" << std::endl; d_literalsToPropagate.push_back(literal); // No conflict @@ -399,7 +428,7 @@ Node TheoryBV::explain(TNode node) { void TheoryBV::addSharedTerm(TNode t) { - Debug("bitvector::sharing") << spaces(getSatContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; + Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; d_sharedTermsSet.insert(t); if (!Options::current()->bitvectorEagerBitblast && d_useEqualityEngine) { d_equalityEngine.addTriggerTerm(t); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index e46d052f8..6ef9d18dd 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -42,12 +42,6 @@ namespace bv { /// forward declarations class Bitblaster; -static inline std::string spaces(int level) -{ - std::string indentStr(level, ' '); - return indentStr; -} - class TheoryBV : public Theory { @@ -61,7 +55,9 @@ private: /** Bitblaster */ Bitblaster* d_bitblaster; - + + context::CDList<TNode> d_bitblastQueue; + /** Context dependent set of atoms we already propagated */ context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet; context::CDHashSet<TNode, TNodeHashFunction> d_sharedTermsSet; @@ -119,7 +115,7 @@ private: if (value) { return d_bv.storePropagation(predicate, SUB_EQUALITY); } else { - return d_bv.storePropagation(predicate, SUB_EQUALITY); + return d_bv.storePropagation(predicate.notNode(), SUB_EQUALITY); } } @@ -134,6 +130,9 @@ private: bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { Debug("bitvector") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; + if (Theory::theoryOf(t1) == THEORY_BOOL) { + return d_bv.storePropagation(t1.iffNode(t2), SUB_EQUALITY); + } return d_bv.storePropagation(t1.eqNode(t2), SUB_EQUALITY); } }; @@ -190,6 +189,12 @@ private: friend class Bitblaster; + inline std::string indent() + { + std::string indentStr(getSatContext()->getLevel(), ' '); + return indentStr; + } + public: void propagate(Effort e); |