diff options
author | Liana Hadarean <lianahady@gmail.com> | 2013-03-24 23:38:33 -0400 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2013-03-24 23:38:33 -0400 |
commit | 147f93cc140b1cf2a5957cbe95eccfc92e4d90b0 (patch) | |
tree | 985ec319875036d27079763865a4d15cc29018f0 /src/theory/bv/bv_inequality_graph.cpp | |
parent | ab19f7ee3cd09d9e9bbf3a75f54989e132442ccf (diff) |
added support for disequalities in the inequality solver
Diffstat (limited to 'src/theory/bv/bv_inequality_graph.cpp')
-rw-r--r-- | src/theory/bv/bv_inequality_graph.cpp | 99 |
1 files changed, 89 insertions, 10 deletions
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>() : 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>() : 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<ReasonId>& 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<TNode>& 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) << ")"; |