diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-11 18:54:38 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-11 18:54:38 +0000 |
commit | d54c761087af01874ea6674111888cb94ffa4ee6 (patch) | |
tree | 2f196940df9b488a1298ccfdee9bf1b54a70ccac /src | |
parent | e148b0a99917b21499b2f596aa22403559baf677 (diff) |
fixing bitvector bugs
* clauses shouldn't be erased when they could be a reason for outside propagation
* propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally
Diffstat (limited to 'src')
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 50 | ||||
-rw-r--r-- | src/theory/bv/bitblaster.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory.h | 21 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_eq.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 63 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 16 |
7 files changed, 113 insertions, 45 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 41c0c4ac9..2eadbdf22 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -31,19 +31,26 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA using namespace BVMinisat; -// purely debugging functions -void printDebug2 (BVMinisat::Lit l) { - std::cout<< (sign(l) ? "-" : "") << var(l) + 1 << std::endl; +namespace CVC4 { + +#define OUTPUT_TAG "bvminisat: [a=" << assumptions.size() << ",l=" << decisionLevel() << "] " + +std::ostream& operator << (std::ostream& out, const BVMinisat::Lit& l) { + out << (sign(l) ? "-" : "") << var(l) + 1; + return out; } -void printDebug2 (BVMinisat::Clause& c) { +std::ostream& operator << (std::ostream& out, const BVMinisat::Clause& c) { for (int i = 0; i < c.size(); i++) { - std::cout << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; + if (i > 0) { + out << " "; + } + out << c[i]; } - std::cout << std::endl; + return out; } - +} //================================================================================================= // Options: @@ -243,7 +250,8 @@ bool Solver::satisfied(const Clause& c) const { // void Solver::cancelUntil(int level) { if (decisionLevel() > level){ - for (int c = trail.size()-1; c >= trail_lim[level]; c--){ + Debug("bvminisat::explain") << OUTPUT_TAG << " backtracking to " << level << std::endl; + for (int c = trail.size()-1; c >= trail_lim[level]; c--){ Var x = var(trail[c]); assigns [x] = l_Undef; if (marker[x] == 2) marker[x] = 1; @@ -502,6 +510,7 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) trail.push_(p); if (decisionLevel() <= assumptions.size() && marker[var(p)] == 1) { if (notify) { + Debug("bvminisat::explain") << OUTPUT_TAG << "propagating " << p << std::endl; notify->notify(p); } } @@ -757,6 +766,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) if (assumption) { assert(decisionLevel() < assumptions.size()); analyzeFinal(p, conflict); + Debug("bvminisat::search") << OUTPUT_TAG << " conflict on assumptions " << std::endl; return l_False; } @@ -779,17 +789,24 @@ lbool Solver::search(int nof_conflicts, UIP uip) // NO CONFLICT if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){ // Reached bound on number of conflicts: + Debug("bvminisat::search") << OUTPUT_TAG << " restarting " << std::endl; progress_estimate = progressEstimate(); cancelUntil(assumptions.size()); return l_Undef; } // Simplify the set of problem clauses: - if (decisionLevel() == 0 && !simplify()) + if (decisionLevel() == 0 && !simplify()) { + Debug("bvminisat::search") << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl; return l_False; + } - if (learnts.size()-nAssigns() >= max_learnts) + // We can't erase clauses if there is unprocessed assumptions, there might be some + // propagationg we need to redu + if (decisionLevel() >= assumptions.size() && learnts.size()-nAssigns() >= max_learnts) { // Reduce the set of learnt clauses: + Debug("bvminisat::search") << OUTPUT_TAG << " cleaning up database" << std::endl; reduceDB(); + } Lit next = lit_Undef; while (decisionLevel() < assumptions.size()){ @@ -800,6 +817,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) newDecisionLevel(); }else if (value(p) == l_False){ analyzeFinal(~p, conflict); + Debug("bvminisat::search") << OUTPUT_TAG << " assumption false, we're unsat" << std::endl; return l_False; }else{ marker[var(p)] = 2; @@ -811,6 +829,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) if (next == lit_Undef){ if (only_bcp) { + Debug("bvminisat::search") << OUTPUT_TAG << " only bcp, skipping rest of the problem" << std::endl; return l_True; } @@ -818,9 +837,11 @@ lbool Solver::search(int nof_conflicts, UIP uip) decisions++; next = pickBranchLit(); - if (next == lit_Undef) + if (next == lit_Undef) { + Debug("bvminisat::search") << OUTPUT_TAG << " satisfiable" << std::endl; // Model found: return l_True; + } } // Increase decision level and enqueue 'next' @@ -930,11 +951,16 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) { vec<Lit> queue; queue.push(p); - __gnu_cxx::hash_set<Var> visited; + Debug("bvminisat::explain") << OUTPUT_TAG << "starting explain of " << p << std::endl; + + __gnu_cxx::hash_set<Var> visited; visited.insert(var(p)); while(queue.size() > 0) { Lit l = queue.last(); + + Debug("bvminisat::explain") << OUTPUT_TAG << "processing " << l << std::endl; + assert(value(l) == l_True); queue.pop(); if (reason(var(l)) == CRef_Undef) { diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index d512847d5..5bb906841 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -337,7 +337,7 @@ Bitblaster::Statistics::~Statistics() { } bool Bitblaster::MinisatNotify::notify(prop::SatLiteral lit) { - return d_bv->storePropagation(d_cnf->getNode(lit), TheoryBV::SUB_BITBLAST); + return d_bv->storePropagation(d_cnf->getNode(lit), SUB_BITBLAST); }; void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) { diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index a8813b7aa..f8c763e3f 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -30,6 +30,27 @@ namespace CVC4 { namespace theory { namespace bv { +enum SubTheory { + SUB_EQUALITY = 1, + SUB_BITBLAST = 2 +}; + +inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { + switch (subtheory) { + case SUB_BITBLAST: + out << "BITBLASTER"; + break; + case SUB_EQUALITY: + out << "EQUALITY"; + break; + default: + Unreachable(); + break; + } + return out; +} + + const bool d_useEqualityEngine = true; const bool d_useSatPropagation = true; diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index ff0fc2b1a..334a704e9 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -79,7 +79,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory: // propagation for (unsigned i = 0; i < assertions.size(); ++i) { TNode fact = assertions[i]; - if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, TheoryBV::SUB_BITBLAST)) { + if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_BITBLAST)) { // Some atoms have not been bit-blasted yet d_bitblaster->bbAtom(fact); // Assert to sat diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp index afb4a8b4a..cb08a1ad8 100644 --- a/src/theory/bv/bv_subtheory_eq.cpp +++ b/src/theory/bv/bv_subtheory_eq.cpp @@ -96,7 +96,7 @@ bool EqualitySolver::addAssertions(const std::vector<TNode>& assertions, Theory: TNode fact = assertions[i]; // Notify the equality engine - if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, TheoryBV::TheoryBV::SUB_EQUALITY) ) { + if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_EQUALITY) ) { bool negated = fact.getKind() == kind::NOT; TNode predicate = negated ? fact[0] : fact; if (predicate.getKind() == kind::EQUAL) { @@ -156,7 +156,7 @@ void EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) } bool EqualitySolver::storePropagation(TNode literal) { - return d_bv->storePropagation(literal, TheoryBV::SUB_EQUALITY); + return d_bv->storePropagation(literal, SUB_EQUALITY); } void EqualitySolver::conflict(TNode a, TNode b) { diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 66f443d50..208ffba6c 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -77,15 +77,25 @@ void TheoryBV::preRegisterTerm(TNode node) { d_equalitySolver.preRegister(node); } +void TheoryBV::sendConflict() { + Assert(d_conflict); + if (d_conflictNode.isNull()) { + return; + } else { + BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode; + d_out->conflict(d_conflictNode); + d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren()); + d_conflictNode = Node::null(); + } +} + void TheoryBV::check(Effort e) { BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; // if we are already in conflict just return the conflict - if (d_conflict) { - BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode; - d_out->conflict(d_conflictNode); - d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren()); + if (inConflict()) { + sendConflict(); return; } @@ -98,20 +108,18 @@ void TheoryBV::check(Effort e) BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; } - // sending assertions to the equality solver first - bool ok = d_equalitySolver.addAssertions(new_assertions, e); + if (!inConflict()) { + // sending assertions to the equality solver first + d_equalitySolver.addAssertions(new_assertions, e); + } - if (ok) { + if (!inConflict()) { // sending assertions to the bitblast solver - ok = d_bitblastSolver.addAssertions(new_assertions, e); + d_bitblastSolver.addAssertions(new_assertions, e); } - if (!ok) { - // output conflict - Assert (d_conflict); - BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode; - d_out->conflict(d_conflictNode); - d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren()); + if (inConflict()) { + sendConflict(); } } @@ -136,14 +144,20 @@ Node TheoryBV::getValue(TNode n) { void TheoryBV::propagate(Effort e) { BVDebug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl; - if (d_conflict) { + if (inConflict()) { return; } // go through stored propagations - for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { + bool ok = true; + for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; - d_out->propagate(literal); + ok = d_out->propagate(literal); + } + + if (!ok) { + BVDebug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl; + setConflict(); } } @@ -177,11 +191,11 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) { - Debug("bitvector") << indent() << "TheoryBV::storePropagation(" << literal << ")" << std::endl; + Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl; // If already in conflict, no more propagation if (d_conflict) { - Debug("bitvector") << indent() << "TheoryBV::storePropagation(" << literal << "): already in conflict" << std::endl; + Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl; return false; } @@ -190,6 +204,13 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) if (find != d_propagatedBy.end()) { return true; } else { + bool polarity = literal.getKind() != kind::NOT; + Node negatedLiteral = polarity ? literal.notNode() : (Node) literal[0]; + find = d_propagatedBy.find(negatedLiteral); + if (find != d_propagatedBy.end() && (*find).second != subtheory) { + // Safe to ignore this one, subtheory should produce a conflict + return true; + } d_propagatedBy[literal] = subtheory; } @@ -199,7 +220,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) // If asserted, we might be in conflict if (hasSatValue && !satValue) { - Debug("bitvector-prop") << indent() << "TheoryBV::storePropagation(" << literal << ") => conflict" << std::endl; + Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ") => conflict" << std::endl; std::vector<TNode> assumptions; Node negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode(); assumptions.push_back(negatedLiteral); @@ -209,7 +230,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) } // Nothing, just enqueue it for propagation and mark it as asserted already - Debug("bitvector-prop") << indent() << "TheoryBV::storePropagation(" << literal << ") => enqueuing for propagation" << std::endl; + Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ") => enqueuing for propagation" << std::endl; d_literalsToPropagate.push_back(literal); // No conflict diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index f79b7ab71..a2cf39049 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -91,11 +91,6 @@ private: /** Index of the next literal to propagate */ context::CDO<unsigned> d_literalsToPropagateIndex; - enum SubTheory { - SUB_EQUALITY = 1, - SUB_BITBLAST = 2 - }; - /** * Keeps a map from nodes to the subtheory that propagated it so that we can explain it * properly. @@ -127,12 +122,16 @@ private: return indentStr; } - void setConflict(Node conflict) { + void setConflict(Node conflict = Node::null()) { d_conflict = true; - d_conflictNode = conflict; + d_conflictNode = conflict; } - bool inConflict() { return d_conflict == true; } + bool inConflict() { + return d_conflict; + } + + void sendConflict(); friend class Bitblaster; friend class BitblastSolver; @@ -142,6 +141,7 @@ private: }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ + }/* CVC4 namespace */ #endif /* __CVC4__THEORY__BV__THEORY_BV_H */ |