From: Liana Hadarean Date: Tue, 15 May 2012 00:11:07 +0000 (+0000) Subject: several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify and now... X-Git-Tag: cvc5-1.0.0~8179 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=77ff33bc6be64f338f035bd9d077737f83280944;p=cvc5.git several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify and now term notify handles boolean constants; fixed bug 328 --- diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index d53507def..41c0c4ac9 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -101,6 +101,7 @@ Solver::Solver(CVC4::context::Context* c) : , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0) , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) + , need_to_propagate(false) , only_bcp(false) , clause_added(false) , ok (true) @@ -187,13 +188,12 @@ bool Solver::addClause_(vec& ps) else if (ps.size() == 1){ uncheckedEnqueue(ps[0]); return ok = (propagate() == CRef_Undef); - }else{ + } else { CRef cr = ca.alloc(ps, false); clauses.push(cr); attachClause(cr); } - - return true; + return ok; } void Solver::attachClause(CRef cr) { @@ -514,8 +514,8 @@ void Solver::popAssumption() { } lbool Solver::assertAssumption(Lit p, bool propagate) { - - assert(marker[var(p)] == 1); + + // assert(marker[var(p)] == 1); if (decisionLevel() > assumptions.size()) { cancelUntil(assumptions.size()); @@ -759,7 +759,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) analyzeFinal(p, conflict); return l_False; } - + varDecayActivity(); claDecayActivity(); @@ -927,7 +927,6 @@ lbool Solver::solve_() // void Solver::explain(Lit p, std::vector& explanation) { - vec queue; queue.push(p); diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index ae5efd81e..ea8e98c4c 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -190,6 +190,7 @@ public: marker[var] = 1; } + bool need_to_propagate; // true if we added new clauses, set to true in propagation bool only_bcp; // solving mode in which only boolean constraint propagation is done void setOnlyBCP (bool val) { only_bcp = val;} void explain(Lit l, std::vector& explanation); 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 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 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 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 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 d_bitblastQueue; + /** Context dependent set of atoms we already propagated */ context::CDHashSet d_alreadyPropagatedSet; context::CDHashSet 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);