From: Liana Hadarean Date: Mon, 25 Mar 2013 03:38:33 +0000 (-0400) Subject: added support for disequalities in the inequality solver X-Git-Tag: cvc5-1.0.0~7361^2~18 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=147f93cc140b1cf2a5957cbe95eccfc92e4d90b0;p=cvc5.git added support for disequalities in the inequality solver --- diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp index 704f99039..4bd315872 100644 --- a/src/theory/bv/bv_inequality_graph.cpp +++ b/src/theory/bv/bv_inequality_graph.cpp @@ -261,9 +261,27 @@ void InequalityGraph::addEdge(TermId a, TermId b, bool strict, TermId reason) { d_undoStackIndex = d_undoStackIndex + 1; } +void InequalityGraph::initializeModelValue(TNode node) { + TermId id = getTermId(node); + Assert (!hasModelValue(id)); + bool isConst = node.getKind() == kind::CONST_BITVECTOR; + unsigned size = utils::getSize(node); + BitVector value = isConst? node.getConst() : BitVector(size, 0u); + setModelValue(id, ModelValue(value, UndefinedTermId, UndefinedReasonId)); +} + +bool InequalityGraph::isRegistered(TNode term) const { + return d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end(); +} + TermId InequalityGraph::registerTerm(TNode term) { if (d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end()) { - return d_termNodeToIdMap[term]; + TermId id = d_termNodeToIdMap[term]; + if (!hasModelValue(id)) { + // we could have backtracked and + initializeModelValue(term); + } + return id; } // store in node mapping @@ -275,21 +293,17 @@ TermId InequalityGraph::registerTerm(TNode term) { // create InequalityNode unsigned size = utils::getSize(term); + bool isConst = term.getKind() == kind::CONST_BITVECTOR; - BitVector value = isConst? term.getConst() : BitVector(size, 0u); - InequalityNode ineq = InequalityNode(id, size, isConst); - setModelValue(id, ModelValue(value, UndefinedTermId, UndefinedReasonId)); - + Assert (d_ineqNodes.size() == id); d_ineqNodes.push_back(ineq); Assert (d_ineqEdges.size() == id); d_ineqEdges.push_back(Edges()); - // add the default edges min <= term <= max - // addEdge(getMinValueId(size), id, false, AxiomReasonId); - // addEdge(id, getMaxValueId(size), false, AxiomReasonId); + initializeModelValue(term); return id; } @@ -314,6 +328,11 @@ TNode InequalityGraph::getTermNode(TermId id) const { return d_termNodes[id]; } +TermId InequalityGraph::getTermId(TNode node) const { + Assert (d_termNodeToIdMap.find(node) != d_termNodeToIdMap.end()); + return d_termNodeToIdMap.find(node)->second; +} + void InequalityGraph::setConflict(const std::vector& conflict) { Assert (!d_inConflict); d_inConflict = true; @@ -351,8 +370,8 @@ bool InequalityGraph::hasModelValue(TermId id) const { } BitVector InequalityGraph::getValue(TermId id) const { - Assert (hasModelValue(id)); - BitVector res = (*(d_modelValues.find(id))).second.value; + Assert (hasModelValue(id)); + BitVector res = (*(d_modelValues.find(id))).second.value; return res; } @@ -361,6 +380,66 @@ bool InequalityGraph::hasReason(TermId id) const { return mv.reason != UndefinedReasonId; } +bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) { + Debug("bv-inequality") << "InequalityGraph::addDisequality " << reason << "\n"; + d_disequalities.push_back(reason); + + if (!isRegistered(a) || !isRegistered(b)) { + splitDisequality(reason); + return true; + } + TermId id_a = getTermId(a); + TermId id_b = getTermId(b); + if (!hasModelValue(id_a)) { + initializeModelValue(a); + } + if (!hasModelValue(id_b)) { + initializeModelValue(b); + } + const BitVector& val_a = getValue(id_a); + const BitVector& val_b = getValue(id_b); + if (val_a == val_b) { + if (a.getKind() == kind::CONST_BITVECTOR) { + // then we know b cannot be smaller than the assigned value so we try to make it larger + return addInequality(a, b, true, reason); + } + if (b.getKind() == kind::CONST_BITVECTOR) { + return addInequality(b, a, true, reason); + } + // if none of the terms are constants just add the lemma + splitDisequality(reason); + } else { + Debug("bv-inequality-internal") << "Disequal: " << a << " => " << val_a.toString(10) << "\n" + << " " << b << " => " << val_b.toString(10) << "\n"; + } + return true; +} + +void InequalityGraph::splitDisequality(TNode diseq) { + Debug("bv-inequality-internal")<<"InequalityGraph::splitDisequality " << diseq <<"\n"; + Assert (diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL); + TNode a = diseq[0][0]; + TNode b = diseq[0][1]; + Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b); + Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a); + Node split = utils::mkNode(kind::OR, a_lt_b, b_lt_a); + Node lemma = utils::mkNode(kind::IMPLIES, diseq, split); + if (d_lemmasAdded.find(lemma) == d_lemmasAdded.end()) { + d_lemmaQueue.push_back(lemma); + } +} + +void InequalityGraph::getNewLemmas(std::vector& new_lemmas) { + for (unsigned i = d_lemmaIndex; i < d_lemmaQueue.size(); ++i) { + TNode lemma = d_lemmaQueue[i]; + if (d_lemmasAdded.find(lemma) == d_lemmasAdded.end()) { + new_lemmas.push_back(lemma); + d_lemmasAdded.insert(lemma); + } + d_lemmaIndex = d_lemmaIndex + 1; + } +} + std::string InequalityGraph::PQueueElement::toString() const { ostringstream os; os << "(id: " << id << ", lower_bound: " << lower_bound.toString(10) <<", old_value: " << model_value.value.toString(10) << ")"; diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 57e59f6f5..1335eff93 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -111,7 +111,7 @@ class InequalityGraph : public context::ContextNotifyObj{ typedef __gnu_cxx::hash_set TermIdSet; typedef std::priority_queue BFSQueue; - + typedef __gnu_cxx::hash_set TNodeSet; std::vector d_ineqNodes; std::vector< Edges > d_ineqEdges; @@ -125,7 +125,8 @@ class InequalityGraph : public context::ContextNotifyObj{ std::vector d_conflict; bool d_signed; - context::CDHashMap d_modelValues; + context::CDHashMap d_modelValues; + void initializeModelValue(TNode node); void setModelValue(TermId term, const ModelValue& mv); ModelValue getModelValue(TermId term) const; bool hasModelValue(TermId id) const; @@ -142,7 +143,8 @@ class InequalityGraph : public context::ContextNotifyObj{ TermId registerTerm(TNode term); TNode getTermNode(TermId id) const; TermId getTermId(TNode node) const; - + bool isRegistered(TNode term) const; + ReasonId registerReason(TNode reason); TNode getReasonNode(ReasonId id) const; @@ -152,10 +154,6 @@ class InequalityGraph : public context::ContextNotifyObj{ const InequalityNode& getInequalityNode(TermId id) const { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; } unsigned getBitwidth(TermId id) const { return getInequalityNode(id).getBitwidth(); } bool isConst(TermId id) const { return getInequalityNode(id).isConstant(); } - // BitVector maxValue(unsigned bitwidth); - // BitVector minValue(unsigned bitwidth); - // TermId getMaxValueId(unsigned bitwidth); - // TermId getMinValueId(unsigned bitwidth); BitVector getValue(TermId id) const; @@ -191,7 +189,18 @@ class InequalityGraph : public context::ContextNotifyObj{ * @param explanation */ void computeExplanation(TermId from, TermId to, std::vector& explanation); + void splitDisequality(TNode diseq); + /** + Disequality reasoning + */ + + /*** The currently asserted disequalities */ + context::CDQueue d_disequalities; + context::CDQueue d_lemmaQueue; + context::CDO d_lemmaIndex; + TNodeSet d_lemmasAdded; + /** Backtracking mechanisms **/ std::vector > d_undoStack; context::CDO d_undoStackIndex; @@ -213,6 +222,10 @@ public: d_conflict(), d_signed(s), d_modelValues(c), + d_disequalities(c), + d_lemmaQueue(c), + d_lemmaIndex(c, 0), + d_lemmasAdded(), d_undoStack(), d_undoStackIndex(c) {} @@ -227,9 +240,11 @@ public: * @return */ bool addInequality(TNode a, TNode b, bool strict, TNode reason); + bool addDisequality(TNode a, TNode b, TNode reason); bool areLessThan(TNode a, TNode b); void getConflict(std::vector& conflict); virtual ~InequalityGraph() throw(AssertionException) {} + void getNewLemmas(std::vector& new_lemmas); }; } diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index f856c9410..6b9842e8f 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -27,15 +27,21 @@ using namespace CVC4::theory::bv; using namespace CVC4::theory::bv::utils; bool InequalitySolver::check(Theory::Effort e) { + Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n"; bool ok = true; while (!done() && ok) { TNode fact = get(); + Debug("bv-subtheory-inequality") << " "<< fact <<"\n"; 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); + } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL) { + TNode a = fact[0][0]; + TNode b = fact[0][1]; + ok = d_inequalityGraph.addDisequality(a, b, fact); } if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) { TNode a = fact[0][1]; @@ -61,6 +67,12 @@ bool InequalitySolver::check(Theory::Effort e) { d_bv->setConflict(utils::mkConjunction(conflict)); return false; } + // send out any lemmas + std::vector lemmas; + d_inequalityGraph.getNewLemmas(lemmas); + for(unsigned i = 0; i < lemmas.size(); ++i) { + d_bv->lemma(lemmas[i]); + } return true; } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 13a475d3d..54260deb9 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -137,6 +137,8 @@ private: void sendConflict(); + void lemma(TNode node) { d_out->lemma(node); } + friend class Bitblaster; friend class BitblastSolver; friend class EqualitySolver;