From b9b17625957d2e718dc2d071dff505d04ccad879 Mon Sep 17 00:00:00 2001 From: lianah Date: Sat, 23 Mar 2013 17:19:21 -0400 Subject: [PATCH] non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing) --- src/theory/bv/bv_inequality_graph.cpp | 64 +++++++++++++++++----- src/theory/bv/bv_inequality_graph.h | 3 +- src/theory/bv/bv_subtheory_inequality.cpp | 8 ++- src/theory/bv/theory_bv.cpp | 14 ++--- test/regress/regress0/bv/inequality04.smt2 | 2 +- 5 files changed, 68 insertions(+), 23 deletions(-) diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp index e29ce2014..53be803ca 100644 --- a/src/theory/bv/bv_inequality_graph.cpp +++ b/src/theory/bv/bv_inequality_graph.cpp @@ -28,6 +28,7 @@ const TermId CVC4::theory::bv::UndefinedTermId = -1; const ReasonId CVC4::theory::bv::UndefinedReasonId = -1; const ReasonId CVC4::theory::bv::AxiomReasonId = -2; + BitVector InequalityGraph::maxValue(unsigned bitwidth) { if (d_signed) { return BitVector(1, 0u).concat(~BitVector(bitwidth - 1, 0u)); @@ -78,7 +79,7 @@ TermId InequalityGraph::getMinValueId(unsigned bitwidth) { } bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) { - Debug("bv-inequality") << "InequlityGraph::addInequality " << a << " " << b << "\n"; + Debug("bv-inequality") << "InequlityGraph::addInequality " << a << " " << b << "strict: " << strict << "\n"; TermId id_a = registerTerm(a); TermId id_b = registerTerm(b); @@ -89,7 +90,17 @@ bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) BitVector b_val = getValue(id_b); unsigned bitwidth = utils::getSize(a); - BitVector diff = strict ? BitVector(bitwidth, 1u) : BitVector(bitwidth, 0u); + BitVector diff = strict ? BitVector(bitwidth, 1u) : BitVector(bitwidth, 0u); + + if (a_val + diff < a_val) { + // we have an overflow + std::vector conflict; + conflict.push_back(id_reason); + computeExplanation(UndefinedTermId, id_a, conflict); + setConflict(conflict); + return false; + } + if (a_val + diff <= b_val) { // the inequality is true in the current partial model // we still add the edge because it may not be true later (cardinality) @@ -117,7 +128,7 @@ bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) return computeValuesBFS(queue, id_a, seen); } -bool InequalityGraph::updateValue(const PQueueElement& el, TermId start, const TermIdSet& seen) { +bool InequalityGraph::updateValue(const PQueueElement& el, TermId start, const TermIdSet& seen, bool& changed) { TermId id = el.id; const BitVector& lower_bound = el.lower_bound; InequalityNode& ineqNode = getInequalityNode(id); @@ -138,7 +149,7 @@ bool InequalityGraph::updateValue(const PQueueElement& el, TermId start, const T // if not constant we can update the value if (ineqNode.getValue() < lower_bound) { // if we are updating the term we started with we must be in a cycle - if (seen.count(id)) { + if (seen.count(id) && id == start) { TermId parent = el.explanation.parent; ReasonId reason = el.explanation.reason; std::vector conflict; @@ -151,6 +162,7 @@ bool InequalityGraph::updateValue(const PQueueElement& el, TermId start, const T Debug("bv-inequality-internal") << "Updating " << getTermNode(id) << " from " << ineqNode.getValue() << "\n" << " to " << lower_bound << "\n"; + changed = true; ineqNode.setValue(lower_bound); setExplanation(id, el.explanation); } @@ -164,17 +176,28 @@ bool InequalityGraph::computeValuesBFS(BFSQueue& queue, TermId start, TermIdSet& const PQueueElement current = queue.top(); queue.pop(); - - if (!updateValue(current, start, seen)) { + Debug("bv-inequality-internal") << "InequalityGraph::computeValuesBFS proceessing " << getTermNode(current.id) << " " << current.toString() << "\n"; + bool updated_current = false; + if (!updateValue(current, start, seen, updated_current)) { return false; } - if (seen.count(current.id) && current.id != getMaxValueId(getBitwidth(current.id))) { + if (seen.count(current.id) && current.id == start) { + // we know what we didn't update start or we would have had a conflict Debug("bv-inequality-internal") << "InequalityGraph::computeValuesBFS equal cycle."; // this means we are in a cycle where all the values are forced to be equal + // TODO: make sure we collapse this cycle into one big node. + return computeValuesBFS(queue, start, seen); + } + + if (!updated_current && !(seen.count(current.id) == 0 && current.id == start)) { + // if we didn't update current we don't need to readd to the queue it's children + seen.insert(current.id); + Debug("bv-inequality-internal") << " unchanged " << getTermNode(current.id) << "\n"; return computeValuesBFS(queue, start, seen); } - seen.insert(current.id); + seen.insert(current.id); + const BitVector& current_value = getValue(current.id); unsigned size = getBitwidth(current.id); @@ -186,8 +209,19 @@ bool InequalityGraph::computeValuesBFS(BFSQueue& queue, TermId start, TermIdSet& TermId next = it->next; const BitVector increment = it->strict ? one : zero; const BitVector& next_lower_bound = current_value + increment; + if (next_lower_bound < current_value) { + // it means we have an overflow and hence a conflict + std::vector conflict; + conflict.push_back(it->reason); + computeExplanation(start, current.id, conflict); + Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n"; + setConflict(conflict); + return false; + } const BitVector& value = getValue(next); - queue.push(PQueueElement(next, value, next_lower_bound, Explanation(current.id, it->reason))); + PQueueElement el = PQueueElement(next, value, next_lower_bound, Explanation(current.id, it->reason)); + queue.push(el); + Debug("bv-inequality-internal") << " enqueue " << getTermNode(el.id) << " " << el.toString() << "\n"; } return computeValuesBFS(queue, start, seen); } @@ -209,16 +243,13 @@ void InequalityGraph::addEdge(TermId a, TermId b, bool strict, TermId reason) { } TermId InequalityGraph::registerTerm(TNode term) { - Debug("bv-inequality-internal") << "InequalityGraph::registerTerm " << term << "\n"; - - if (d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end()) { return d_termNodeToIdMap[term]; } // store in node mapping TermId id = d_termNodes.size(); - Debug("bv-inequality-internal") << " with id " << id << "\n"; + Debug("bv-inequality-internal") << "InequalityGraph::registerTerm " << term << " => id"<< id << "\n"; d_termNodes.push_back(term); d_termNodeToIdMap[term] = id; @@ -285,6 +316,13 @@ void InequalityGraph::getConflict(std::vector& conflict) { } } +std::string InequalityGraph::PQueueElement::toString() const { + ostringstream os; + os << "(id: " << id <<", value: " << value.toString(10) << ", lower_bound: " << lower_bound.toString(10) <<")"; + return os.str(); +} + + // bool InequalityGraph::initializeValues(TNode a, TNode b, bool strict, TermId reason_id) { // TermId id_a = registerTerm(a); // TermId id_b = registerTerm(b); diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 18bd75726..6eb88ec79 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -101,6 +101,7 @@ class InequalityGraph { bool operator< (const PQueueElement& other) const { return value > other.value; } + std::string toString() const; }; typedef __gnu_cxx::hash_map ReasonToIdMap; @@ -171,7 +172,7 @@ class InequalityGraph { * * @return */ - bool updateValue(const PQueueElement& el, TermId start, const TermIdSet& seen); + bool updateValue(const PQueueElement& el, TermId start, const TermIdSet& seen, bool& changed); /** * Update the current model starting with the start term. * diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 6b4b1a134..f856c9410 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -30,7 +30,13 @@ bool InequalitySolver::check(Theory::Effort e) { bool ok = true; while (!done() && ok) { TNode fact = get(); - + if (fact.getKind() == kind::EQUAL) { + TNode a = fact[0]; + TNode b = fact[1]; + ok = d_inequalityGraph.addInequality(a, b, false, fact); + if (ok) + ok = d_inequalityGraph.addInequality(b, a, false, fact); + } if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) { TNode a = fact[0][1]; TNode b = fact[0][0]; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index a794d63a3..bc8e39e67 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -122,15 +122,15 @@ void TheoryBV::check(Effort e) } Assert (!ok == inConflict()); - // if (!inConflict() && !d_coreSolver.isCoreTheory()) { - // ok = d_inequalitySolver.check(e); - // } - - Assert (!ok == inConflict()); if (!inConflict() && !d_coreSolver.isCoreTheory()) { - // if (!inConflict() && !d_inequalitySolver.isInequalityTheory()) { - ok = d_bitblastSolver.check(e); + ok = d_inequalitySolver.check(e); } + + Assert (!ok == inConflict()); + // if (!inConflict() && !d_coreSolver.isCoreTheory()) { + // if (!inConflict() && !d_inequalitySolver.isInequalityTheory()) { + // ok = d_bitblastSolver.check(e); + // } Assert (!ok == inConflict()); if (inConflict()) { diff --git a/test/regress/regress0/bv/inequality04.smt2 b/test/regress/regress0/bv/inequality04.smt2 index 7b5dbd7d5..35607eaef 100644 --- a/test/regress/regress0/bv/inequality04.smt2 +++ b/test/regress/regress0/bv/inequality04.smt2 @@ -12,7 +12,7 @@ (bvule v0 v1) (bvule v1 v2) (bvule v2 v0) - (bvule (_ bv4 16) v0) + (bvult (_ bv4 16) v0) (bvult v2 (_ bv5 16)) )) (check-sat) -- 2.30.2