diff options
author | lianah <lianahady@gmail.com> | 2013-01-25 17:31:45 -0500 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-01-25 17:31:45 -0500 |
commit | df01ef792cf9806782b12bc93ddaa139d75346c0 (patch) | |
tree | 1ebde531896cff825dc36ea6fe00867c7f3c4cde /src/theory/bv/slicer.cpp | |
parent | 683961cae0fabb44c2018b31a24168089cd692cf (diff) |
starting the slicer form scratch.
Diffstat (limited to 'src/theory/bv/slicer.cpp')
-rw-r--r-- | src/theory/bv/slicer.cpp | 708 |
1 files changed, 191 insertions, 517 deletions
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index 8eb7d6127..001427488 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -17,7 +17,6 @@ **/ #include "theory/bv/slicer.h" -#include "util/integer.h" #include "util/utility.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" @@ -27,582 +26,257 @@ using namespace CVC4::theory; using namespace CVC4::theory::bv; using namespace std; -void Base::decomposeNode(TNode node, std::vector<Node>& decomp) const { - Debug("bv-slicer") << "Base::decomposeNode " << node << "\n with base" << debugPrint() << endl; - - Index low = 0; - Index high = utils::getSize(node) - 1; - if (node.getKind() == kind::BITVECTOR_EXTRACT) { - low = utils::getExtractLow(node); - high = utils::getExtractHigh(node); - node = node[0]; - } - Index index = low; - for (Index i = low; i <= high; ++i) { - if (isCutPoint(i)) { - // make sure the extract is pushed down before concat - Node slice = Rewriter::rewrite(utils::mkExtract(node, i, index)); - index = i + 1; - decomp.push_back(slice); - Debug("bv-slicer") << slice <<" "; - } - } - Debug("bv-slicer") << endl; -} - -/** - * Adds a cutPoint at Index i and splits the corresponding Splinter +/** + * Base * - * @param i the index where the cut point will be introduced - * @param sp the splinter pointer corresponding to the splinter to be sliced - * @param low_splinter the resulting bottom part of the splinter - * @param top_splinter the resulting top part of the splinter */ -void Slice::split(Index i, SplinterPointer& sp, Splinter*& low_splinter, Splinter*& top_splinter) { - Debug("bv-slicer") << "Slice::split " << this->debugPrint() << "\n"; - Assert (!d_base.isCutPoint(i)); - d_base.sliceAt(i); - - Splinter* s = NULL; - Slice::const_iterator it = begin(); - bool lt, gt; - for (; it != end(); ++it) { - lt = (it->second)->getHigh() >= i; - gt = (it->second)->getLow() <= i; - if (gt && lt) { - s = it->second; - break; - } - } - - Assert (s != NULL); +Base::Base(uint32_t size) + : d_size(size), + d_repr((size-1)/32 + ((size-1) % 32 == 0? 0 : 1), 0) +{ + Assert (d_size > 0); +} - sp = s->getPointer(); - Index low = s->getLow(); - Index high = s->getHigh(); - // creating the two splinter fragments - low_splinter = new Splinter(i, low); - top_splinter = new Splinter(high, i+1); - addSplinter(low, low_splinter); - addSplinter(i+1, top_splinter); - Debug("bv-slicer") << " to " << this->debugPrint() << "\n"; -} - -void Slice::addSplinter(Index i, Splinter* sp) { - Assert (i == sp->getLow() && sp->getHigh() < d_bitwidth); +void Base::sliceAt(Index index) { + Index vector_index = index / 32; + Assert (vector_index < d_size - 1); + Index int_index = index % 32; + uint32_t bit_mask = utils::pow2(int_index); + d_repr[vector_index] = d_repr[vector_index] | bit_mask; +} - if (i != 0) { - d_base.sliceAt(i - 1); +void Base::sliceWith(const Base& other) { + Assert (d_size == other.d_size); + for (unsigned i = 0; i < d_repr.size(); ++i) { + d_repr[i] = d_repr[i] | other.d_repr[i]; } - // d_base.debugPrint(); - // free the memory associated with the previous splinter - if (d_splinters.find(i) != d_splinters.end()) { - delete d_splinters[i]; - } - d_splinters[i] = sp; } -bool Slice::isConsistent() { - // check that base is consistent with slicings - // and that the slicings are continous - std::map<Index, Splinter*>::const_iterator it = d_splinters.begin(); - Index prev = -1; - for (; it != d_splinters.end(); ++it) { - Index index = (*it).first; - Splinter* splinter = (*it).second; - if (index != 0 && !d_base.isCutPoint(index-1)) - return false; - if (index != splinter->getLow()) - return false; - if (prev + 1 != index) - return false; - prev = splinter->getHigh(); - } - if (prev != d_bitwidth - 1) - return false; +bool Base::isCutPoint (Index index) const { + // there is an implicit cut point at the end of the bv + if (index == d_size - 1) + return true; + + Index vector_index = index / 32; + Assert (vector_index < d_size - 1); + Index int_index = index % 32; + uint32_t bit_mask = utils::pow2(int_index); - for (unsigned i = 0; i < d_bitwidth - 1; ++i) { - if (d_base.isCutPoint(i) && d_splinters.find(i+1) == d_splinters.end()) - return false; - } - return true; + return (bit_mask & d_repr[vector_index]) != 0; } -std::string Slice::debugPrint() { - std::ostringstream os; - os << d_base.debugPrint(); - os << "{ "; - for (Slice::const_iterator it = begin(); it != end(); ++it) { - Splinter* s = (*it).second; - os << "[" << s->getLow() << ":" << s->getHigh() <<"]"; - Assert ((*it).first == s->getLow()); - Assert (s->getLow() == 0 || d_base.isCutPoint(s->getLow() - 1)); - SplinterPointer sp = s->getPointer(); - if (s->getPointer() != Undefined) { - os << "->" << sp.debugPrint(); - } - os << " "; +void Base::diffCutPoints(const Base& other, Base& res) const { + Assert (d_size == other.d_size && res.d_size == d_size); + for (unsigned i = 0; i < d_repr.size(); ++i) { + Assert (res.d_repr[i] == 0); + res.d_repr[i] = d_repr[i] ^ other.d_repr[i]; } - os << "}"; - return os.str(); } -void SliceBlock::computeBlockBase(BlockIdSet& changedSet) { - Debug("bv-slicer") << "SliceBlock::computeBlockBase for block" << d_rootId << endl; - Debug("bv-slicer") << this->debugPrint() << endl; - - ++(d_slicer->d_statistics.d_numBlockBaseComputations); - - Base new_cut_points(d_bitwidth); - - // at this point d_base has all the cut points in the individual slices - for (unsigned row = 0; row < d_block.size(); ++row) { - Slice* slice = d_block[row]; - new_cut_points.reset(); - slice->getBase().diffCutPoints(d_base, new_cut_points); - - if (! new_cut_points.isEmpty()) { - // use the cut points from the base to split the current slice - for (unsigned i = 0; i < d_bitwidth; ++i) { - const Base& base = slice->getBase(); // the base may have changed if splinters of the same slice are equal - - if (new_cut_points.isCutPoint(i) && i != d_bitwidth - 1 && ! base.isCutPoint(i) ) { - - Debug("bv-slicer") << " adding cut point at " << i << " for row " << row << endl; - // split this slice (this updates the slice's base) - Splinter* bottom, *top = NULL; - SplinterPointer sp; - - ++(d_slicer->d_statistics.d_numSplits); - slice->split(i, sp, bottom, top); - Assert (bottom != NULL && top != NULL); - Assert (i >= bottom->getLow()); - - if (sp != Undefined) { - unsigned delta = i - bottom->getLow(); - // if we do need to split something else split it now - Debug("bv-slicer") <<" must split " << sp.debugPrint(); - Slice* other_slice = d_slicer->getSlice(sp); - Splinter* s = d_slicer->getSplinter(sp); - Index cutPoint = s->getLow() + delta; - Splinter* new_bottom = new Splinter(cutPoint, s->getLow()); - Splinter* new_top = new Splinter(s->getHigh(), cutPoint + 1); - new_bottom->setPointer(SplinterPointer(d_rootId, row, bottom->getLow())); - new_top->setPointer(SplinterPointer(d_rootId, row, top->getLow())); - // note that this could modify the current splinter - other_slice->addSplinter(new_bottom->getLow(), new_bottom); - other_slice->addSplinter(new_top->getLow(), new_top); - - bottom->setPointer(SplinterPointer(sp.term, sp.row, new_bottom->getLow())); - top->setPointer(SplinterPointer(sp.term, sp.row, new_top->getLow())); - // update base for block - d_slicer->getSliceBlock(sp)->sliceBaseAt(cutPoint); - // add to queue of blocks that have changed base - Debug("bv-slicer") << " adding block to queue: " << sp.term << endl; - changedSet.insert(sp.term); - } - } - } - } +bool Base::isEmpty() const { + for (unsigned i = 0; i< d_repr.size(); ++i) { + if (d_repr[i] != 0) + return false; } - - Debug("bv-slicer") << "base computed: " << d_rootId << endl; - Debug("bv-slicer") << this->debugPrint() << endl; - Debug("bv-slicer") << "SliceBlock::computeBlockBase done. \n"; - + return true; } -std::string SliceBlock::debugPrint() { +std::string Base::debugPrint() const { std::ostringstream os; - os << "Width " << d_bitwidth << endl; - os << "Base " << d_base.debugPrint() << endl; - for (SliceBlock::const_iterator it = begin(); it!= end(); ++it) { - os << (*it)->debugPrint() << endl; + os << "["; + bool first = true; + for (unsigned i = 0; i < d_size - 1; ++i) { + if (isCutPoint(i)) { + if (first) + first = false; + else + os <<"| "; + + os << i ; + } } + os << "]"; return os.str(); } - -Slicer::Slicer() - : d_simpleEqualities(), - d_roots(), - d_numRoots(0), - d_nodeRootMap(), - d_rootBlocks(), - d_coreTermCache(), - d_statistics() -{} - -Slicer::Statistics::Statistics() : - d_numBlocks("TheoryBV::Slicer::NumBlocks", 0), - d_avgBlockSize("TheoryBV::Slicer::AvgBlockSize"), - d_avgBlockBitwitdh("TheoryBV::Slicer::AvgBlockBitwidth"), - d_numBlockBaseComputations("TheoryBV::Slicer::NumBlockBaseComputations", 0), - d_numSplits("TheoryBV::Slicer::NumSplits", 0), - d_numSimpleEqualities("TheoryBV::Slicer::NumSimpleEqualities", 0), - d_numSlices("TheoryBV::Slicer::NumSlices", 0) -{ - StatisticsRegistry::registerStat(&d_numBlocks); - StatisticsRegistry::registerStat(&d_avgBlockSize); - StatisticsRegistry::registerStat(&d_avgBlockBitwitdh); - StatisticsRegistry::registerStat(&d_numBlockBaseComputations); - StatisticsRegistry::registerStat(&d_numSplits); - StatisticsRegistry::registerStat(&d_numSimpleEqualities); - StatisticsRegistry::registerStat(&d_numSlices); -} - -Slicer::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numBlocks); - StatisticsRegistry::unregisterStat(&d_avgBlockSize); - StatisticsRegistry::unregisterStat(&d_avgBlockBitwitdh); - StatisticsRegistry::unregisterStat(&d_numBlockBaseComputations); - StatisticsRegistry::unregisterStat(&d_numSplits); - StatisticsRegistry::unregisterStat(&d_numSimpleEqualities); - StatisticsRegistry::unregisterStat(&d_numSlices); + + +/** + * UnionFind + * + */ +TermId UnionFind::addTerm(Index bitwidth) { + Node node(bitwidth); + d_nodes.push_back(node); + TermId id = d_nodes.size() - 1; + d_representatives.insert(id); + d_topLevelTerms.insert(id); } - -RootId Slicer::makeRoot(TNode n) { - Assert (n.getKind() != kind::BITVECTOR_EXTRACT && n.getKind() != kind::BITVECTOR_CONCAT); - if (d_nodeRootMap.find(n) != d_nodeRootMap.end()) { - return d_nodeRootMap[n]; - } - RootId id = d_roots.size(); - d_nodeRootMap[n] = id; - d_roots.push_back(n); - d_rootBlocks.push_back(new SliceBlock(id, utils::getSize(n), this)); - Assert (d_roots.size() == d_rootBlocks.size()); +void UnionFind::merge(TermId t1, TermId t2) { - Debug("bv-slicer") << "Slicer::makeRoot " << n << " -> " << id << endl; +} +TermId UnionFind::find(TermId id) { + Node node = getNode(id); + if (node.getRepr() != -1) + return find(node.getRepr()); return id; } +/** + * Splits the representative of the term between i-1 and i + * + * @param id the id of the term + * @param i the index we are splitting at + * + * @return + */ +void UnionFind::split(TermId id, Index i) { + id = find(id); + Node node = getNode(id); + Assert (i < node.getBitwidth()); -void Slicer::splitEqualities(TNode node, std::vector<Node>& equalities) { - Assert (node.getKind() == kind::EQUAL); - TNode t1 = node[0]; - TNode t2 = node[1]; - - uint32_t width = utils::getSize(t1); - - Base base1(width); - if (t1.getKind() == kind::BITVECTOR_CONCAT) { - int size = -1; - // no need to count the last child since the end cut point is implicit - for (int i = t1.getNumChildren() - 1; i >= 1 ; --i) { - size = size + utils::getSize(t1[i]); - base1.sliceAt(size); - } + if (i == 0 || i == node.getBitwidth()) { + // nothing to do + return; } - Base base2(width); - if (t2.getKind() == kind::BITVECTOR_CONCAT) { - unsigned size = -1; - for (int i = t2.getNumChildren() - 1; i >= 1; --i) { - size = size + utils::getSize(t2[i]); - base2.sliceAt(size); - } - } + if (!node.hasChildren()) { + // first time we split this term + TermId bottom_id = addTerm(i); + TermId top_id = addTerm(node.getBitwidth() - i); + node.addChildren(top_id, bottom_id); - base1.sliceWith(base2); - if (!base1.isEmpty()) { - // we split the equalities according to the base - int last = 0; - for (unsigned i = 0; i < utils::getSize(t1); ++i) { - if (base1.isCutPoint(i)) { - Node extract1 = Rewriter::rewrite(utils::mkExtract(t1, i, last)); - Node extract2 = Rewriter::rewrite(utils::mkExtract(t2, i, last)); - last = i + 1; - Assert (utils::getSize(extract1) == utils::getSize(extract2)); - equalities.push_back(utils::mkNode(kind::EQUAL, extract1, extract2)); - } - } } else { - // just return same equality - equalities.push_back(node); + Index cut = node.getCutPoint(); + if (i < cut ) + split(child1, i); + else + split(node.getChild(1), i - cut); } -} - -void Slicer::processEquality(TNode node) { - Assert (node.getKind() == kind::EQUAL); - Debug("bv-slicer") << "theory::bv::Slicer::processEquality " << node << endl; - // std::vector<Node> equalities; - // splitEqualities(node, equalities); - // for (unsigned i = 0; i < equalities.size(); ++i) { - // Debug("bv-slicer") << " splitEqualities " << node << endl; - registerSimpleEquality(node); - d_simpleEqualities.push_back(node); - // } } -void Slicer::registerSimpleEquality(TNode eq) { - Assert (eq.getKind() == kind::EQUAL); - ++(d_statistics.d_numSimpleEqualities); - - Debug("bv-slicer-eq") << "theory::bv::Slicer::registerSimpleEquality " << eq << endl; - TNode a = eq[0]; - TNode b = eq[1]; - - if (a == b) - return; - - RootId id_a = registerTerm(a); - RootId id_b = registerTerm(b); - - unsigned low_a = 0; - unsigned low_b = 0; - - if (a.getKind() == kind::BITVECTOR_EXTRACT) { - low_a = utils::getExtractLow(a); - } - - if (b.getKind() == kind::BITVECTOR_EXTRACT) { - low_b = utils::getExtractLow(b); +void UnionFind::getNormalForm(ExtractTerm term, NormalForm& nf) { + TermId id = find(term.id); + getDecomposition(term, nf.decomp); + // update nf base + Index count = 0; + for (unsigned i = 0; i < nf.decomp.size(); ++i) { + count += getBitwidth(nf.decomp[i]); + nf.base.sliceAt(count); } +} - if (id_a == id_b ) { - // we are in the special case a[i0:j0] = a[i1:j1] - Index high_a = utils::getExtractHigh(a); - Index high_b = utils::getExtractHigh(b); - - unsigned intersection_low = std::max(low_a, low_b); - unsigned intersection_high = std::min(high_a, high_b); - if (intersection_low <= intersection_high) { - // if the two extracts intersect - unsigned intersection_size = intersection_high - intersection_low + 1; - // gcd between overlapping area and difference - unsigned diff = low_a > low_b ? low_a - low_b : low_b - low_a; - unsigned granularity = gcd(intersection_size, diff); - SliceBlock* block_a = d_rootBlocks[id_a]; - Assert (a.getKind() == kind::BITVECTOR_EXTRACT); - unsigned size = utils::getSize(a[0]); - - Slice* slice = new Slice(size); - unsigned low = low_a > low_b ? low_b : low_a; - unsigned high = high_a > high_b ? high_a : high_b; - Splinter* prev_splinter = NULL; - // the row the new slice will be in - unsigned block_row = block_a->getSize(); - for (unsigned i = low; i <= high; i+=granularity) { - Splinter* s = new Splinter(i+ granularity-1, i); - slice->addSplinter(i, s); - // update splinter pointers to reflect entailed equalities - if (prev_splinter!= NULL) { - // the previous splinter will be equal to the current - prev_splinter->setPointer(SplinterPointer(id_a, block_row, i)); - } - prev_splinter = s; - } - // make sure to splinters for the extremities - if (low!= 0) { - Splinter* s = new Splinter(low -1 , 0); - slice->addSplinter(0, s); - } - if (high != size - 1) { - Splinter* s = new Splinter(size - 1, high + 1); - slice->addSplinter(high+1, s); - } - block_a->addSlice(slice); - d_rootBlocks[id_a] = block_a; - Debug("bv-slicer") << " updated block" << id_a << " to " << endl; - Debug("bv-slicer") << block_a->debugPrint() << endl; - return; - } +void UnionFind::getDecomposition(ExtractTerm term, Decomposition& decomp) { + // making sure the term is aligned + TermId id = find(term.id); + + Node node = getNode(id); + Assert (term.high < node.getBitwidth()); + // because we split the node, this must be the whole extract + if (!node.hasChildren()) { + Assert (term.high == node.getBitwidth() - 1 && + term.low == 0); + decomp.push_back(id); } + + Index cut = node.getCutPoint(); - Slice* slice_a = makeSlice(a); - Slice* slice_b = makeSlice(b); - - SliceBlock* block_a = d_rootBlocks[id_a]; - SliceBlock* block_b = d_rootBlocks[id_b]; - - uint32_t row_a = block_a->addSlice(slice_a); - uint32_t row_b = block_b->addSlice(slice_b); - - SplinterPointer sp_a = SplinterPointer(id_a, row_a, low_a); - SplinterPointer sp_b = SplinterPointer(id_b, row_b, low_b); - - slice_a->getSplinter(low_a)->setPointer(sp_b); - slice_b->getSplinter(low_b)->setPointer(sp_a); - Debug("bv-slicer") << " updated block" << id_a << " to " << endl; - Debug("bv-slicer") << block_a->debugPrint() << endl; - Debug("bv-slicer") << " updated block" <<id_b << " to " << endl; - Debug("bv-slicer") << block_b->debugPrint() << endl; -} - -Slice* Slicer::makeSlice(TNode node) { - //Assert (d_sliceSet.find(node) == d_sliceSet.end()); - ++(d_statistics.d_numSlices); - Index bitwidth = utils::getSize(node); - Index low = 0; - Index high = bitwidth -1; - if (node.getKind() == kind::BITVECTOR_EXTRACT) { - low = utils::getExtractLow(node); - high = utils::getExtractHigh(node); - bitwidth = utils::getSize(node[0]); + if (low < cut && high < cut) { + // the extract falls entirely on the low child + ExtractTerm child_ex(node.getChild(0), high, low); + getDecomposition(child_ex, decomp); } - Splinter* splinter = new Splinter(high, low); - Slice* slice = new Slice(bitwidth); - slice->addSplinter(low, splinter); - if (low != 0) { - Splinter* bottom_splinter = new Splinter(low-1, 0); - slice->addSplinter(0, bottom_splinter); + else if (low >= cut && high >= cut){ + // the extract falls entirely on the high child + ExtractTerm child_ex(node.getChild(1), high - cut, low - cut); + getDecomposition(child_ex, decomp); } - if (high != bitwidth - 1) { - Splinter* top_splinter = new Splinter(bitwidth - 1, high + 1); - slice->addSplinter(high+1, top_splinter); + else { + // the extract is split over the two children + ExtractTerm low_child(node.getChild(0), cut - 1, low); + getDecomposition(low_child, decomp); + ExtractTerm high_child(node.getChild(1), high, cut); + getDecomposition(high_child, decomp); } - return slice; } - -RootId Slicer::registerTerm(TNode node) { - if (node.getKind() == kind::BITVECTOR_EXTRACT ) { - node = node[0]; - Assert (isRootTerm(node)); +void UnionFind::alignSlicings(NormalForm& nf1, NormalForm& nf2) { + Assert (nf1.base.getBitwidth() == nf2.base.getBitwidth()); + // check if the two have + std::vector<TermId> intersection; + intersection(nf1.decomp, nf2.decomp, intersection); + for (unsigned i = 0; i < intersection.size(); ++i) { + TermId overlap = intersection[i]; + Index start1 = 0; + Decomposition& decomp1 = nf1.decomp; + for (unsigned j = 0; j < decomp1.size(); ++j) { + if (decomp1[j] == overlap) + break; + start1 += getSize(decomp1[j]); + } } - // setting up the data-structures for the root term - RootId id = makeRoot(node); - return id; -} - -bool Slicer::isCoreTerm(TNode node) { - if (d_coreTermCache.find(node) == d_coreTermCache.end()) { - Kind kind = node.getKind(); - if (kind != kind::BITVECTOR_EXTRACT && - kind != kind::BITVECTOR_CONCAT && - kind != kind::EQUAL && kind != kind::NOT && - node.getMetaKind() != kind::metakind::VARIABLE && - kind != kind::CONST_BITVECTOR) { - d_coreTermCache[node] = false; - return false; - } else { - // we need to recursively check whether the term is a root term or not - bool isCore = true; - for (unsigned i = 0; i < node.getNumChildren(); ++i) { - isCore = isCore && isCoreTerm(node[i]); - } - d_coreTermCache[node] = isCore; - return isCore; + + Base new_cuts1 = nf1.base.diffCutPoints(nf2.base); + Base new_cuts2 = nf2.base.diffCutPoints(nf1.base); + for (unsigned i = 0; i < new_cuts.base.getBitwidth(); ++i) { + if (new_cuts1.isCutPoint(i)) { + } } - return d_coreTermCache[node]; + } -bool Slicer::isRootTerm(TNode node) { - Kind kind = node.getKind(); - return kind != kind::BITVECTOR_EXTRACT && kind != kind::BITVECTOR_CONCAT; +void UnionFind::ensureSlicing(ExtractTerm& term) { + TermId id = find(term.id); + split(id, term.high); + split(id, term.low); + + } -// Base Slicer::getBase(TNode node) { -// Assert (d_bases.find(node) != d_bases.end()); -// return d_bases[node]; -// } +/** + * Slicer + * + */ -// void Slicer::updateBase(TNode node, const Base& base) { -// Assert (d_bases.find(node) != d_bases.end()); -// d_bases[node] = d_bases[node].bitwiseOr(base); -// } -void Slicer::computeCoarsestBase() { - Debug("bv-slicer") << "theory::bv::Slicer::computeCoarsestBase " << endl; - BlockIdSet changed_set; - for (unsigned i = 0; i < d_rootBlocks.size(); ++i) { - SliceBlock* block = d_rootBlocks[i]; - block->computeBlockBase(changed_set); - ++(d_statistics.d_numBlocks); - d_statistics.d_avgBlockSize.addEntry(block->getSize()); - d_statistics.d_avgBlockBitwitdh.addEntry(block->getBitwidth()); +void Slicer::registerTerm(TNode node) { + Index low = 0, high = utils::getSize(node); + TNode n = node; + if (node.getKind() == kind::BITVECTOR_EXTRACT) { + TNode n = node[0]; + high = utils::getExtractHigh(node); + low = utils::getExtractLow(node); } - - Debug("bv-slicer") << " processing changeSet of size " << changed_set.size() << endl; - while (!changed_set.empty()) { - // process split candidate - RootId current = *(changed_set.begin()); - changed_set.erase(current); - SliceBlock* block = d_rootBlocks[current]; - block->computeBlockBase(changed_set); + if (d_nodeToId.find(n) == d_nodeToId.end()) { + id = d_uf.addTerm(utils::getSize(n)); + d_nodeToId[n] = id; + d_idToNode[id] = n; } - Assert(debugCheckBase()); - std::cout << "Done computing coarsest base \n"; -} - + TermId id = d_nodeToId[n]; -void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp) { - Assert (node.getKind() != kind::BITVECTOR_CONCAT); - TNode root = node.getKind() == kind::BITVECTOR_EXTRACT ? node[0] : node; - Assert (isRootTerm(root)); - const Base& base = getSliceBlock(getRootId(root))->getBase(); - base.decomposeNode(node, decomp); + return ExtractTerm(id, high, low); } -bool Slicer::debugCheckBase() { - // check that all terms involved in equalities are properly sliced w.r.t. - // these equalities - for (unsigned i = 0; i < d_simpleEqualities.size(); ++i) { - TNode a = d_simpleEqualities[i][0]; - TNode b = d_simpleEqualities[i][1]; - std::vector<Node> a_decomp; - std::vector<Node> b_decomp; +void Slicer::processSimpleEquality(TNode eq) { + Assert (eq.getKind() == kind::EQUAL); + TNode a = eq[0]; + TNode b = eq[1]; + ExtractTerm a_ex= registerTerm(a); + ExtractTerm b_ex= registerTerm(b); + + NormalForm a_nf, b_nf; + d_uf.ensureSlicing(a_ex); + d_uf.ensureSlicing(b_ex); + + d_uf.getNormalForm(a_ex, a_nf); + d_uf.getNormalForm(b_ex, b_nf); - const Base& base_a = getSliceBlock(getRootId(a.getKind() == kind::BITVECTOR_EXTRACT ? a[0] : a))->getBase(); - const Base& base_b = getSliceBlock(getRootId(b.getKind() == kind::BITVECTOR_EXTRACT ? b[0] : b))->getBase(); - base_a.decomposeNode(a, a_decomp); - base_b.decomposeNode(b, b_decomp); - if (a_decomp.size() != b_decomp.size()) { - Debug("bv-slicer-check") << "Slicer::debugCheckBase different decomposition sizes for \n" - << a <<" and \n" - << b <<" \n"; - return false; - } - for (unsigned j = 0; j < a_decomp.size(); ++j) { - if (utils::getSize(a_decomp[j]) != utils::getSize(b_decomp[j])) { - Debug("bv-slicer-check") << "Slicer::debugCheckBase inconsistent decompositions \n"; - return false; - } - } - } - // iterate through blocks and check that the block base is the same as each slice base - for (unsigned i = 0; i < d_rootBlocks.size(); ++i) { - SliceBlock* block = d_rootBlocks[i]; - const Base& block_base = block->getBase(); - Base diff_points(block->getBitwidth()); - SliceBlock::const_iterator it = block->begin(); - for (; it != block->end(); ++it) { - Slice* slice = *it; - if (!slice->isConsistent()) { - Debug("bv-slicer-check") << "Slicer::debugCheckBase inconsistent slice: \n" - << slice->debugPrint() << "\n"; - return false; - } - - diff_points.reset(); - slice->getBase().diffCutPoints(block_base, diff_points); - if (!diff_points.isEmpty()) { - Debug("bv-slicer-check") << "Slicer::debugCheckBase slice missing cut points: \n" - << slice->debugPrint() - << "Block base: " << block->getBase().debugPrint() << endl; - return false; - } - Slice::const_iterator slice_it = slice->begin(); - for (; slice_it!= slice->end(); ++slice_it) { - Splinter* splinter = (*slice_it).second; - const SplinterPointer& sp = splinter->getPointer(); - if (sp != Undefined) { - Splinter* other = getSplinter(sp); - if (splinter->getBitwidth() != other->getBitwidth()) { - Debug("bv-slicer-check") << "Slicer::debugCheckBase inconsistent splinter pointer \n"; - return false; - } - } - } - } - } - return true; + d_uf.alignSlicings(a_nf, b_nf); } - - - +void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp) const { +} |