From e6383effa630863bcc73abc1df985b1dad55db39 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Mon, 2 May 2011 19:09:11 +0000 Subject: updates for bitvectors --- src/theory/bv/slice_manager.h | 61 +++++++++++++++++++++++++------------------ 1 file changed, 35 insertions(+), 26 deletions(-) (limited to 'src/theory/bv/slice_manager.h') 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; } -- cgit v1.2.3