diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-05-02 19:09:11 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-05-02 19:09:11 +0000 |
commit | e6383effa630863bcc73abc1df985b1dad55db39 (patch) | |
tree | cdc42f8a0290c15cc87f0265ce2fb4664ab4fb14 /src/theory/bv/theory_bv.cpp | |
parent | e5206966df456dbb9cad97809d6e10f2bca13b2e (diff) |
updates for bitvectors
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 137 |
1 files changed, 93 insertions, 44 deletions
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<TNode> 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<TNode> 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<TNode> assumptions; - Node lhsNormalized = d_eqEngine.normalize(equality[0], assumptions); - Node rhsNormalized = d_eqEngine.normalize(equality[1], assumptions); + std::set<TNode> 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<TNode> reasons; - d_eqEngine.getExplanation(node[0], node[1], reasons); - std::set<TNode> 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<TNode> >& vec = d_normalization[equality]->assumptions; + std::set<TNode> 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; } |