From e6383effa630863bcc73abc1df985b1dad55db39 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Mon, 2 May 2011 19:09:11 +0000 Subject: [PATCH] updates for bitvectors --- src/theory/bv/cd_set_collection.h | 4 +- src/theory/bv/equality_engine.h | 2 +- src/theory/bv/slice_manager.h | 61 +++++++------ src/theory/bv/theory_bv.cpp | 137 ++++++++++++++++++++---------- src/theory/bv/theory_bv.h | 32 ++++++- src/theory/bv/theory_bv_utils.h | 9 +- 6 files changed, 162 insertions(+), 83 deletions(-) diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h index 217ebadcd..30e4e47ec 100644 --- a/src/theory/bv/cd_set_collection.h +++ b/src/theory/bv/cd_set_collection.h @@ -252,7 +252,7 @@ public: backtrack(); Assert(isValid(set)); - const_value_reference candidate_value; + const_value_reference candidate_value = value_type(); bool candidate_found = false; // Find the biggest node smaleer than value (it must exist) @@ -279,7 +279,7 @@ public: backtrack(); Assert(isValid(set)); - const_value_reference candidate_value; + const_value_reference candidate_value = value_type(); bool candidate_found = false; // Find the smallest node bigger than value (it must exist) diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h index 0450c4535..31a4bfd27 100644 --- a/src/theory/bv/equality_engine.h +++ b/src/theory/bv/equality_engine.h @@ -812,7 +812,7 @@ Node EqualityEngine::normalizeWit if (node != result) { std::vector equalities; getExplanation(result, node, equalities); - assumptions.insert(equalities.begin(), equalities.end()); + utils::getConjuncts(equalities, assumptions); } // If asked, substitute the children with their representatives diff --git a/src/theory/bv/slice_manager.h b/src/theory/bv/slice_manager.h index 78ed4f265..4fb11f105 100644 --- a/src/theory/bv/slice_manager.h +++ b/src/theory/bv/slice_manager.h @@ -301,18 +301,20 @@ bool SliceManager::sliceAndSolve(std::vector& lhs, std::v // We slice constants immediately if (sizeDifference > 0 && lhsTerm.getKind() == kind::CONST_BITVECTOR) { - BitVector low = lhsTerm.getConst().extract(utils::getSize(rhsTerm) - 1, 0); - BitVector high = lhsTerm.getConst().extract(utils::getSize(lhsTerm) - 1, utils::getSize(rhsTerm)); - lhs.push_back(utils::mkConst(low)); - lhs.push_back(utils::mkConst(high)); + Node low = utils::mkConst(lhsTerm.getConst().extract(sizeDifference - 1, 0)); + Node high = utils::mkConst(lhsTerm.getConst().extract(utils::getSize(lhsTerm) - 1, sizeDifference)); + d_equalityEngine.addTerm(low); d_equalityEngine.addTerm(high); + lhs.push_back(low); + lhs.push_back(high); rhs.push_back(rhsTerm); continue; } if (sizeDifference < 0 && rhsTerm.getKind() == kind::CONST_BITVECTOR) { - BitVector low = rhsTerm.getConst().extract(utils::getSize(lhsTerm) - 1, 0); - BitVector high = rhsTerm.getConst().extract(utils::getSize(rhsTerm) - 1, utils::getSize(lhsTerm)); - rhs.push_back(utils::mkConst(low)); - rhs.push_back(utils::mkConst(high)); + Node low = utils::mkConst(rhsTerm.getConst().extract(-sizeDifference - 1, 0)); + Node high = utils::mkConst(rhsTerm.getConst().extract(utils::getSize(rhsTerm) - 1, -sizeDifference)); + d_equalityEngine.addTerm(low); d_equalityEngine.addTerm(high); + rhs.push_back(low); + rhs.push_back(high); lhs.push_back(lhsTerm); continue; } @@ -418,7 +420,7 @@ bool SliceManager::sliceAndSolve(std::vector& lhs, std::v std::vector explanation; d_equalityEngine.getExplanation(lhsTerm, lhsTermRepresentative, explanation); std::set additionalAssumptions(assumptions); - additionalAssumptions.insert(explanation.begin(), explanation.end()); + utils::getConjuncts(explanation, additionalAssumptions); bool ok = solveEquality(lhsTermRepresentative, concat, additionalAssumptions); if (!ok) return false; } else { @@ -438,7 +440,7 @@ bool SliceManager::sliceAndSolve(std::vector& lhs, std::v std::vector explanation; d_equalityEngine.getExplanation(rhsTerm, rhsTermRepresentative, explanation); std::set additionalAssumptions(assumptions); - additionalAssumptions.insert(explanation.begin(), explanation.end()); + utils::getConjuncts(explanation, additionalAssumptions); bool ok = solveEquality(rhsTermRepresentative, concat, additionalAssumptions); if (!ok) return false; } else { @@ -509,6 +511,8 @@ bool SliceManager::addSlice(Node node, unsigned slicePoint) { TNode nodeBase = baseTerm(node); + Assert(nodeBase.getKind() != kind::CONST_BITVECTOR); + set_reference sliceSet; slicing_map::iterator find = d_nodeSlicing.find(nodeBase); if (find == d_nodeSlicing.end()) { @@ -550,7 +554,7 @@ bool SliceManager::addSlice(Node node, unsigned slicePoint) { std::set assumptions; std::vector equalities; d_equalityEngine.getExplanation(nodeSlice, nodeSliceRepresentative, equalities); - assumptions.insert(equalities.begin(), equalities.end()); + utils::getConjuncts(equalities, assumptions); ok = solveEquality(nodeSliceRepresentative, concat, assumptions); } @@ -592,23 +596,32 @@ inline bool SliceManager::slice(TNode node, std::vector& Assert(d_setCollection.size(nodeSliceSet) >= 2); BVDebug("slicing") << "SliceManager::slice(" << node << "): current: " << d_setCollection.toString(nodeSliceSet) << std::endl; - std::vector slicePoints; - if (low + 1 < high) { - d_setCollection.getElements(nodeSliceSet, low + 1, high - 1, slicePoints); - } - + // Go through all the points i_0 <= low < i_1 < ... < i_{n-1} < high <= i_n from the slice set // and generate the slices [i_0:low-1][low:i_1-1] [i_1:i2] ... [i_{n-1}:high-1][high:i_n-1]. They are in reverse order, // as they should be - size_t i_0 = low == 0 ? 0 : d_setCollection.prev(nodeSliceSet, low + 1); - BVDebug("slicing") << "SliceManager::slice(" << node << "): i_0: " << i_0 << std::endl; + + // The high bound already in the slicing size_t i_n = high == utils::getSize(nodeBase) ? high: d_setCollection.next(nodeSliceSet, high - 1); - BVDebug("slicing") << "SliceManager::slice(" << node << "): i_n: " << i_n << std::endl; - - // Add the new points to the slice set (they might be there already) + BVDebug("slicing") << "SliceManager::slice(" << node << "): i_n: " << i_n << std::endl; + // Add the new point to the slice set (they might be there already) if (high < i_n) { if (!addSlice(nodeBase, high)) return false; } + // The low bound already in the slicing (slicing might have changed after adding high) + size_t i_0 = low == 0 ? 0 : d_setCollection.prev(nodeSliceSet, low + 1); + BVDebug("slicing") << "SliceManager::slice(" << node << "): i_0: " << i_0 << std::endl; + // Add the new points to the slice set (they might be there already) + if (i_0 < low) { + if (!addSlice(nodeBase, low)) return false; + } + + // Get the slice points + std::vector slicePoints; + if (low + 1 < high) { + d_setCollection.getElements(nodeSliceSet, low + 1, high - 1, slicePoints); + } + // Construct the actuall slicing if (slicePoints.size() > 0) { BVDebug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, slicePoints[0] - 1, low) << std::endl; @@ -622,11 +635,7 @@ inline bool SliceManager::slice(TNode node, std::vector& } else { sliced.push_back(utils::mkExtract(nodeBase, high - 1, low)); } - // Add the new points to the slice set (they might be there already) - if (i_0 < low) { - if (!addSlice(nodeBase, low)) return false; - } - + return true; } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 314e6b714..7a8ebb85c 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -46,9 +46,8 @@ void TheoryBV::preRegisterTerm(TNode node) { d_eqEngine.addTerm(node[1][i]); } } - size_t triggerId = d_eqEngine.addTrigger(node[0], node[1]); - Assert(triggerId == d_triggers.size()); - d_triggers.push_back(node); + + d_normalization[node] = new Normalization(d_context, node); } } @@ -56,6 +55,10 @@ void TheoryBV::check(Effort e) { BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; + // Normalization iterators + NormalizationMap::iterator it = d_normalization.begin(); + NormalizationMap::iterator it_end = d_normalization.end(); + // Get all the assertions std::vector assertionsList; while (!done()) { @@ -65,6 +68,8 @@ void TheoryBV::check(Effort e) { assertionsList.push_back(assertion); } + bool normalizeEqualities = false; + for (unsigned i = 0; i < assertionsList.size(); ++ i) { TNode assertion = assertionsList[i]; @@ -77,27 +82,23 @@ void TheoryBV::check(Effort e) { // Slice and solve the equality bool ok = d_sliceManager.solveEquality(assertion[0], assertion[1]); if (!ok) return; + // Normalize all equalities + normalizeEqualities = true; + it = d_normalization.begin(); + it = d_normalization.end(); break; } case kind::NOT: { - // We need to check this as the equality trigger might have been true when we made it - TNode equality = assertion[0]; - - // Assumptions - std::set assumptions; - Node lhsNormalized = d_eqEngine.normalize(equality[0], assumptions); - Node rhsNormalized = d_eqEngine.normalize(equality[1], assumptions); - - BVDebug("bitvector") << "TheoryBV::check(" << e << "): normalizes to " << lhsNormalized << " = " << rhsNormalized << std::endl; - - // No need to slice the equality, the whole thing *should* be deduced - if (lhsNormalized == rhsNormalized) { - BVDebug("bitvector") << "TheoryBV::check(" << e << "): conflict with " << utils::setToString(assumptions) << std::endl; - assumptions.insert(assertion); - d_out->conflict(mkConjunction(assumptions)); - return; - } else { - d_disequalities.push_back(assertion); + if (!normalizeEqualities) { + // We still need to check this dis-equality, as it might have been pre-registered just now + // so we didn't have a chance to propagate + it = d_normalization.find(assertion[0]); + if (it->second->assumptions.size() == 1) { + // Just normalize this equality + normalizeEqualities = true; + it_end = it; + it_end ++; + } } break; } @@ -106,28 +107,70 @@ void TheoryBV::check(Effort e) { } } - if (fullEffort(e)) { + if (normalizeEqualities) { - BVDebug("bitvector") << "TheoryBV::check(" << e << "): checking dis-equalities" << std::endl; + BVDebug("bitvector") << "Checking for propagations" << std::endl; + + NormalizationMap::iterator it = d_normalization.begin(); + NormalizationMap::iterator it_end = d_normalization.end(); + for(; it != it_end; ++ it) { - for (unsigned i = 0, i_end = d_disequalities.size(); i < i_end; ++ i) { - - BVDebug("bitvector") << "TheoryBV::check(" << e << "): checking " << d_disequalities[i] << std::endl; + TNode equality = it->first; + BVDebug("bitvector") << "Checking " << equality << std::endl; + Normalization& normalization = *it->second; + + // If asserted, we don't care + if (d_assertions.find(equality) != d_assertions.end()) continue; - TNode equality = d_disequalities[i][0]; // Assumptions - std::set assumptions; - Node lhsNormalized = d_eqEngine.normalize(equality[0], assumptions); - Node rhsNormalized = d_eqEngine.normalize(equality[1], assumptions); + std::set assumptions; + TNode lhs = normalization.equalities.back()[0]; + TNode rhs = normalization.equalities.back()[1]; + // If already satisfied, do nothing + if (lhs == rhs) continue; + + Node lhsNormalized = d_eqEngine.normalize(lhs, assumptions); + Node rhsNormalized = d_eqEngine.normalize(rhs, assumptions); + + if (lhsNormalized == lhs && rhsNormalized == rhs) continue; + + normalization.equalities.push_back(lhsNormalized.eqNode(rhsNormalized)); + normalization.assumptions.push_back(assumptions); + + BVDebug("bitvector") << "Adding normalization " << lhsNormalized.eqNode(rhsNormalized) << std::endl; + BVDebug("bitvector") << " assumptions " << setToString(assumptions) << std::endl; + BVDebug("bitvector") << "TheoryBV::check(" << e << "): normalizes to " << lhsNormalized << " = " << rhsNormalized << std::endl; - // No need to slice the equality, the whole thing *should* be deduced - if (lhsNormalized == rhsNormalized) { - BVDebug("bitvector") << "TheoryBV::check(" << e << "): conflict with " << utils::setToString(assumptions) << std::endl; - assumptions.insert(d_disequalities[i]); - d_out->conflict(mkConjunction(assumptions)); - return; + // If both are equal we can propagate + bool propagate = lhsNormalized == rhsNormalized; + // otherwise if both are constants, we propagate negation (if not already there) + bool propagateNegation = !propagate && + lhsNormalized.getKind() == kind::CONST_BITVECTOR && rhsNormalized.getKind() == kind::CONST_BITVECTOR + && d_assertions.find(equality.notNode()) == d_assertions.end(); + ; + if (propagate || propagateNegation) { + Node implied = propagate ? Node(equality) : equality.notNode() ; + Node impliedNegated = propagate ? equality.notNode() : Node(equality) ; + // If the negation of what's implied has been asserted, we are in conflict + if (d_assertions.find(impliedNegated) != d_assertions.end()) { + BVDebug("bitvector") << "TheoryBV::check(" << e << "): conflict with " << utils::setToString(assumptions) << std::endl; + // Construct the assumptions + for (unsigned i = 0; i < normalization.assumptions.size(); ++ i) { + assumptions.insert(normalization.assumptions[i].begin(), normalization.assumptions[i].end()); + } + // Make the conflict + assumptions.insert(impliedNegated); + d_out->conflict(mkConjunction(assumptions)); + return; + } + // Otherwise we propagate the implication + else { + BVDebug("bitvector") << "TheoryBV::check(" << e << "): propagating " << implied << std::endl; + d_out->propagate(implied); + d_assertions.insert(implied); + } } } } @@ -138,6 +181,8 @@ bool TheoryBV::triggerEquality(size_t triggerId) { Assert(triggerId < d_triggers.size()); BVDebug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << "): " << d_triggers[triggerId] << std::endl; + return true; + TNode equality = d_triggers[triggerId]; // If we have just asserted this equality ignore it @@ -181,13 +226,17 @@ Node TheoryBV::getValue(TNode n) { void TheoryBV::explain(TNode node) { BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl; - if(node.getKind() == kind::EQUAL) { - std::vector reasons; - d_eqEngine.getExplanation(node[0], node[1], reasons); - std::set simpleReasons; - utils::getConjuncts(reasons, simpleReasons); - d_out->explanation(utils::mkConjunction(simpleReasons)); - return; + + TNode equality = node.getKind() == kind::NOT ? node[0] : node; + Assert(equality.getKind() == kind::EQUAL); + + context::CDList< set >& vec = d_normalization[equality]->assumptions; + std::set assumptions; + for (unsigned i = 0; i < vec.size(); ++ i) { + BVDebug("bitvector") << "Adding normalization " << d_normalization[equality]->equalities[i] << std::endl; + BVDebug("bitvector") << " assumptions " << setToString(d_normalization[equality]->assumptions[i]) << std::endl; + assumptions.insert(vec[i].begin(), vec[i].end()); } - Unreachable(); + d_out->explanation(utils::mkConjunction(assumptions)); + return; } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 748352321..8c2b59efa 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -24,6 +24,7 @@ #include "theory/theory.h" #include "context/context.h" #include "context/cdset.h" +#include "context/cdlist.h" #include "theory/bv/equality_engine.h" #include "theory/bv/slice_manager.h" @@ -82,7 +83,6 @@ public: private: - /** Equality reasoning engine */ BvEqualityEngine d_eqEngine; @@ -91,6 +91,9 @@ private: /** Equality triggers indexed by ids from the equality manager */ std::vector d_triggers; + + /** The context we are using */ + context::Context* d_context; /** The asserted stuff */ context::CDSet d_assertions; @@ -98,13 +101,36 @@ private: /** Asserted dis-equalities */ context::CDList d_disequalities; + struct Normalization { + context::CDList equalities; + context::CDList< std::set > assumptions; + Normalization(context::Context* c, TNode eq) + : equalities(c), assumptions(c) { + equalities.push_back(eq); + assumptions.push_back(std::set()); + } + }; + + /** Map from equalities to their noramlization information */ + typedef __gnu_cxx::hash_map NormalizationMap; + NormalizationMap d_normalization; + /** Called by the equality managere on triggers */ bool triggerEquality(size_t triggerId); + Node d_true; + public: - TheoryBV(context::Context* c, OutputChannel& out, Valuation valuation) : - Theory(THEORY_BV, c, out, valuation), d_eqEngine(*this, c, "theory::bv::EqualityEngine"), d_sliceManager(*this, c), d_assertions(c), d_disequalities(c) { + TheoryBV(context::Context* c, OutputChannel& out, Valuation valuation) + : Theory(THEORY_BV, c, out, valuation), + d_eqEngine(*this, c, "theory::bv::EqualityEngine"), + d_sliceManager(*this, c), + d_context(c), + d_assertions(c), + d_disequalities(c) + { + d_true = utils::mkTrue(); } BvEqualityEngine& getEqualityEngine() { diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 80751fe4c..a3135f077 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -106,7 +106,6 @@ inline void getConjuncts(std::vector& nodes, std::set& conjuncts) } } - inline Node mkConjunction(const std::set nodes) { std::set expandedNodes; @@ -115,12 +114,8 @@ inline Node mkConjunction(const std::set nodes) { while (it != it_end) { TNode current = *it; if (current != mkTrue()) { - Assert(current != mkFalse()); - if (current.getKind() == kind::AND) { - getConjuncts(current, expandedNodes); - } else { - expandedNodes.insert(current); - } + Assert(current.getKind() == kind::EQUAL || (current.getKind() == kind::NOT && current[0].getKind() == kind::EQUAL)); + expandedNodes.insert(current); } ++ it; } -- 2.30.2