From: lianah Date: Fri, 25 Jan 2013 17:10:34 +0000 (-0500) Subject: minor changes trying to optimize the slicing code X-Git-Tag: cvc5-1.0.0~7361^2~56 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=683961cae0fabb44c2018b31a24168089cd692cf;p=cvc5.git minor changes trying to optimize the slicing code --- diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index e67c0b827..8eb7d6127 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -27,7 +27,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::bv; using namespace std; -void Base::decomposeNode(TNode node, std::vector& decomp) { +void Base::decomposeNode(TNode node, std::vector& decomp) const { Debug("bv-slicer") << "Base::decomposeNode " << node << "\n with base" << debugPrint() << endl; Index low = 0; @@ -59,7 +59,7 @@ void Base::decomposeNode(TNode node, std::vector& decomp) { * @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"; + Debug("bv-slicer") << "Slice::split " << this->debugPrint() << "\n"; Assert (!d_base.isCutPoint(i)); d_base.sliceAt(i); @@ -95,7 +95,7 @@ void Slice::addSplinter(Index i, Splinter* sp) { if (i != 0) { d_base.sliceAt(i - 1); } - d_base.debugPrint(); + // d_base.debugPrint(); // free the memory associated with the previous splinter if (d_splinters.find(i) != d_splinters.end()) { delete d_splinters[i]; @@ -148,49 +148,60 @@ std::string Slice::debugPrint() { return os.str(); } -void SliceBlock::computeBlockBase(std::vector& queue) { +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]; - Base base = slice->getBase(); - Base new_cut_points = base.diffCutPoints(d_base); - // use the cut points from the base to split the current slice - for (unsigned i = 0; i < d_bitwidth; ++i) { - 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; - 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); + 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()); - 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; - queue.push_back(sp.term); + 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); + } } } } @@ -218,9 +229,39 @@ Slicer::Slicer() d_numRoots(0), d_nodeRootMap(), d_rootBlocks(), - d_coreTermCache() + 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); +} + + RootId Slicer::makeRoot(TNode n) { Assert (n.getKind() != kind::BITVECTOR_EXTRACT && n.getKind() != kind::BITVECTOR_CONCAT); if (d_nodeRootMap.find(n) != d_nodeRootMap.end()) { @@ -263,7 +304,7 @@ void Slicer::splitEqualities(TNode node, std::vector& equalities) { } base1.sliceWith(base2); - if (base1 != Base(width)) { + if (!base1.isEmpty()) { // we split the equalities according to the base int last = 0; for (unsigned i = 0; i < utils::getSize(t1); ++i) { @@ -295,6 +336,8 @@ void Slicer::processEquality(TNode 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]; @@ -388,7 +431,7 @@ void Slicer::registerSimpleEquality(TNode eq) { 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; @@ -463,21 +506,25 @@ bool Slicer::isRootTerm(TNode node) { void Slicer::computeCoarsestBase() { Debug("bv-slicer") << "theory::bv::Slicer::computeCoarsestBase " << endl; - std::vector queue; + BlockIdSet changed_set; for (unsigned i = 0; i < d_rootBlocks.size(); ++i) { SliceBlock* block = d_rootBlocks[i]; - block->computeBlockBase(queue); + block->computeBlockBase(changed_set); + ++(d_statistics.d_numBlocks); + d_statistics.d_avgBlockSize.addEntry(block->getSize()); + d_statistics.d_avgBlockBitwitdh.addEntry(block->getBitwidth()); } - Debug("bv-slicer") << " processing queue of size " << queue.size() << endl; - while (!queue.empty()) { + Debug("bv-slicer") << " processing changeSet of size " << changed_set.size() << endl; + while (!changed_set.empty()) { // process split candidate - RootId current = queue.back(); - queue.pop_back(); + RootId current = *(changed_set.begin()); + changed_set.erase(current); SliceBlock* block = d_rootBlocks[current]; - block->computeBlockBase(queue); + block->computeBlockBase(changed_set); } Assert(debugCheckBase()); + std::cout << "Done computing coarsest base \n"; } @@ -485,7 +532,7 @@ void Slicer::getBaseDecomposition(TNode node, std::vector& decomp) { Assert (node.getKind() != kind::BITVECTOR_CONCAT); TNode root = node.getKind() == kind::BITVECTOR_EXTRACT ? node[0] : node; Assert (isRootTerm(root)); - Base base = getSliceBlock(getRootId(root))->getBase(); + const Base& base = getSliceBlock(getRootId(root))->getBase(); base.decomposeNode(node, decomp); } @@ -498,8 +545,8 @@ bool Slicer::debugCheckBase() { std::vector a_decomp; std::vector b_decomp; - Base base_a = getSliceBlock(getRootId(a.getKind() == kind::BITVECTOR_EXTRACT ? a[0] : a))->getBase(); - Base base_b = getSliceBlock(getRootId(b.getKind() == kind::BITVECTOR_EXTRACT ? b[0] : b))->getBase(); + 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()) { @@ -518,7 +565,8 @@ bool Slicer::debugCheckBase() { // 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]; - Base block_base = block->getBase(); + 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; @@ -527,8 +575,10 @@ bool Slicer::debugCheckBase() { << slice->debugPrint() << "\n"; return false; } - Base diff_points = slice->getBase().diffCutPoints(block_base); - if (diff_points != Base(block->getBitwidth())) { + + 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; diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index 4d430258d..16820801e 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -18,10 +18,15 @@ #include "cvc4_private.h" + #include #include #include +#include + #include "util/bitvector.h" +#include "util/statistics_registry.h" + #include "expr/node.h" #include "theory/bv/theory_bv_utils.h" #ifndef __CVC4__THEORY__BV__SLICER_BV_H @@ -39,19 +44,15 @@ typedef uint32_t Index; class Base { uint32_t d_size; - CVC4::BitVector d_repr; + std::vector d_repr; public: Base(uint32_t size) - : d_size(size) { - Assert (size > 0); - d_repr = BitVector(size - 1, 0u); + : d_size(size), + d_repr((size-1)/32 + ((size-1) % 32 == 0? 0 : 1), 0) + { + Assert (d_size > 0); } - Base(const BitVector& repr) - : d_size(repr.getSize() + 1), - d_repr(repr) { - Assert (d_size > 0); - } /** * Marks the base by adding a cut between index and index + 1 @@ -59,40 +60,74 @@ public: * @param index */ void sliceAt(Index index) { - Assert (index < d_size - 1); - d_repr = d_repr.setBit(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; } void sliceWith(const Base& other) { - Assert (d_size == other.d_size); - d_repr = d_repr | other.d_repr; + 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]; + } } - void decomposeNode(TNode node, std::vector& decomp); + void decomposeNode(TNode node, std::vector& decomp) const; - bool isCutPoint (Index index) { - Assert (index < d_size); - // the last cut point is implicit + bool isCutPoint (Index index) const { + // there is an implicit cut point at the end of the bv if (index == d_size - 1) - return true; - return d_repr.isBitSet(index); + 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); + + return (bit_mask & d_repr[vector_index]) != 0; } - Base diffCutPoints(const Base& other) const { - return Base(other.d_repr ^ d_repr); + void 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]; + } } - bool operator==(const Base& other) const { - return d_repr == other.d_repr; + bool isEmpty() const { + for (unsigned i = 0; i< d_repr.size(); ++i) { + if (d_repr[i] != 0) + return false; + } + return true; } - bool operator!=(const Base& other) const { - return !(*this == other); + + void reset() { + for (unsigned i = 0; i< d_repr.size(); ++i) { + d_repr[i] = 0; + } } - std::string debugPrint() { + + // bool operator==(const Base& other) const { + // Assert (d_size == other.d_size); + // for (unsigned i = 0; i < d_repr.size(); ++i) { + // if (d_repr[i] != other.d_repr[i]) + // return false; + // } + // return true; + // } + // bool operator!=(const Base& other) const { + // return !(*this == other); + // } + + std::string debugPrint() const { std::ostringstream os; os << "["; bool first = true; - for (Index i = 0; i < d_size - 1; ++i) { + for (unsigned i = 0; i < d_size - 1; ++i) { if (isCutPoint(i)) { if (first) first = false; @@ -229,6 +264,8 @@ public: class Slicer; +typedef __gnu_cxx::hash_set BlockIdSet; + class SliceBlock { uint32_t d_bitwidth; RootId d_rootId; /**< the id of the root term this block corresponds to */ @@ -236,10 +273,8 @@ class SliceBlock { Base d_base; /**< the base corresponding to this block containing all the cut points. Invariant: the base should contain all the cut-points in the slices*/ Slicer* d_slicer; // FIXME: more elegant way to do this - + public: - - SliceBlock(RootId rootId, uint32_t bitwidth, Slicer* slicer) : d_bitwidth(bitwidth), d_rootId(rootId), @@ -267,7 +302,7 @@ public: * * @param queue other blocks that changed their base. */ - void computeBlockBase(std::vector& queue); + void computeBlockBase(BlockIdSet& recompute); void sliceBaseAt(Index i) { d_base.sliceAt(i); @@ -311,6 +346,8 @@ class Slicer { /* Indexed by Root Id */ SliceBlocks d_rootBlocks; RootTermCache d_coreTermCache; + + public: Slicer(); void computeCoarsestBase(); @@ -342,8 +379,24 @@ private: RootId makeRoot(TNode n); Slice* makeSlice(TNode node); - bool debugCheckBase(); + bool debugCheckBase(); + + class Statistics { + public: + IntStat d_numBlocks; + AverageStat d_avgBlockSize; + AverageStat d_avgBlockBitwitdh; + IntStat d_numBlockBaseComputations; + IntStat d_numSplits; + IntStat d_numSimpleEqualities; + IntStat d_numSlices; + Statistics(); + ~Statistics(); + }; + public: + Statistics d_statistics; + Slice* getSlice(const SplinterPointer& sp) { Assert (sp != Undefined); SliceBlock* sb = d_rootBlocks[sp.term]; diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 565ec9704..73a13e1ad 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -37,6 +37,12 @@ namespace theory { namespace bv { namespace utils { +inline uint32_t pow2(uint32_t power) { + Assert (power < 32); + uint32_t one = 1; + return one << power; +} + inline unsigned getExtractHigh(TNode node) { return node.getOperator().getConst().high; }