using namespace CVC4::theory::bv;
using namespace std;
-void Base::decomposeNode(TNode node, std::vector<Node>& decomp) {
+void Base::decomposeNode(TNode node, std::vector<Node>& decomp) const {
Debug("bv-slicer") << "Base::decomposeNode " << node << "\n with base" << debugPrint() << endl;
Index low = 0;
* @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);
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];
return os.str();
}
-void SliceBlock::computeBlockBase(std::vector<RootId>& 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);
+ }
}
}
}
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()) {
}
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) {
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];
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;
void Slicer::computeCoarsestBase() {
Debug("bv-slicer") << "theory::bv::Slicer::computeCoarsestBase " << endl;
- std::vector<RootId> 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";
}
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);
}
std::vector<Node> a_decomp;
std::vector<Node> 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()) {
// 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;
<< 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;
#include "cvc4_private.h"
+
#include <vector>
#include <list>
#include <ext/hash_map>
+#include <math.h>
+
#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
class Base {
uint32_t d_size;
- CVC4::BitVector d_repr;
+ std::vector<uint32_t> 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
* @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<Node>& decomp);
+ void decomposeNode(TNode node, std::vector<Node>& 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;
class Slicer;
+typedef __gnu_cxx::hash_set<RootId> BlockIdSet;
+
class SliceBlock {
uint32_t d_bitwidth;
RootId d_rootId; /**< the id of the root term this block corresponds to */
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),
*
* @param queue other blocks that changed their base.
*/
- void computeBlockBase(std::vector<RootId>& queue);
+ void computeBlockBase(BlockIdSet& recompute);
void sliceBaseAt(Index i) {
d_base.sliceAt(i);
/* Indexed by Root Id */
SliceBlocks d_rootBlocks;
RootTermCache d_coreTermCache;
+
+
public:
Slicer();
void computeCoarsestBase();
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];
projects / cvc5.git / commitdiff