diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-12-10 20:48:51 -0500 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-12-10 20:48:51 -0500 |
commit | 67af0bb961e42ab84c5f82245809ea12e2c12758 (patch) | |
tree | e2ac08edd8f3db204a712b87cf9532eb43f6b709 /src/theory/bv/slicer.cpp | |
parent | a8a471141d2fca4428b7c016ea4494d9925fc544 (diff) |
ported my bv-core branch from svn to git
Diffstat (limited to 'src/theory/bv/slicer.cpp')
-rw-r--r-- | src/theory/bv/slicer.cpp | 474 |
1 files changed, 474 insertions, 0 deletions
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp new file mode 100644 index 000000000..73cad53b8 --- /dev/null +++ b/src/theory/bv/slicer.cpp @@ -0,0 +1,474 @@ +/********************* */ +/*! \file slicer.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Bitvector theory. + ** + ** Bitvector theory. + **/ + +#include "theory/bv/slicer.h" +#include "util/integer.h" +#include "util/utility.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/rewriter.h" + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace std; + +void Base::decomposeNode(TNode node, std::vector<Node>& decomp) { + 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 + * + * @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); + + 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); + + if (i != 0) { + d_base.sliceAt(i - 1); + } + 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; +} + +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 << " "; + } + os << "}"; + return os.str(); +} + +void SliceBlock::computeBlockBase(std::vector<RootId>& queue) { + Debug("bv-slicer") << "SliceBlock::computeBlockBase for block" << d_rootId << endl; + Debug("bv-slicer") << this->debugPrint() << endl; + + // 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]; + const 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) { + if (new_cut_points.isCutPoint(i) && i != d_bitwidth - 1) { + 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); + + if (sp != Undefined) { + // if we do need to split something else split it + Debug("bv-slicer") <<" must split " << sp.debugPrint(); + Slice* slice = d_slicer->getSlice(sp); + Splinter* s = d_slicer->getSplinter(sp); + Index cutPoint = s->getLow() + i; + 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())); + + slice->addSplinter(new_bottom->getLow(), new_bottom); + 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; + queue.push_back(sp.term); + } + } + } + } + + Debug("bv-slicer") << "base computed: " << d_rootId << endl; + Debug("bv-slicer") << this->debugPrint() << endl; + Debug("bv-slicer") << "SliceBlock::computeBlockBase done. \n"; + +} + +std::string SliceBlock::debugPrint() { + 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; + } + return os.str(); +} + +Slicer::Slicer() + : d_simpleEqualities(), + d_roots(), + d_numRoots(0), + d_nodeRootMap(), + d_rootBlocks(), + d_coreTermCache() +{} + +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()); + + Debug("bv-slicer") << "Slicer::makeRoot " << n << " -> " << id << endl; + return id; +} + +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) { + unsigned size = 0; + for (int i = t1.getNumChildren(); i >= 0; --i) { + size = size + utils::getSize(t1[i]); + base1.sliceAt(size); + } + } + + Base base2(width); + if (t2.getKind() == kind::BITVECTOR_CONCAT) { + unsigned size = 0; + for (int i = t2.getNumChildren(); i >= 0; --i) { + size = size + utils::getSize(t2[i]); + base2.sliceAt(size); + } + } + + base1.sliceWith(base2); + if (base1 != Base(width)) { + // we split the equalities according to the base + int last = 0; + for (unsigned i = 1; i < utils::getSize(t1); ++i) { + if (base1.isCutPoint(i)) { + Node extract1 = Rewriter::rewrite(utils::mkExtract(t1, last, i - 1)); + Node extract2 = Rewriter::rewrite(utils::mkExtract(t2, last, i - 1)); + last = i; + 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); + } +} + +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(equalities[i]); + d_simpleEqualities.push_back(equalities[i]); + } +} + +void Slicer::registerSimpleEquality(TNode eq) { + Assert (eq.getKind() == kind::EQUAL); + Debug("bv-slicer") << "theory::bv::Slicer::registerSimpleEquality " << eq << endl; + TNode a = eq[0]; + TNode b = eq[1]; + + 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); + } + + 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 + granularity <= size) { + Splinter* s = new Splinter(size - 1, high + 1); + slice->addSplinter(high+1, s); + } + block_a->addSlice(slice); + return; + } + } + + 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); +} + +Slice* Slicer::makeSlice(TNode node) { + //Assert (d_sliceSet.find(node) == d_sliceSet.end()); + + 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]); + } + 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); + } + if (high != bitwidth - 1) { + Splinter* top_splinter = new Splinter(bitwidth - 1, high + 1); + slice->addSplinter(high+1, top_splinter); + } + return slice; +} + + +RootId Slicer::registerTerm(TNode node) { + if (node.getKind() == kind::BITVECTOR_EXTRACT ) { + node = node[0]; + Assert (isRootTerm(node)); + } + // 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) { + 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; + } + } + return d_coreTermCache[node]; +} + +bool Slicer::isRootTerm(TNode node) { + Kind kind = node.getKind(); + return kind != kind::BITVECTOR_EXTRACT && kind != kind::BITVECTOR_CONCAT; +} + +// Base Slicer::getBase(TNode node) { +// Assert (d_bases.find(node) != d_bases.end()); +// return d_bases[node]; +// } + +// 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; + std::vector<RootId> queue; + for (unsigned i = 0; i < d_rootBlocks.size(); ++i) { + SliceBlock* block = d_rootBlocks[i]; + block->computeBlockBase(queue); + } + + Debug("bv-slicer") << " processing queue of size " << queue.size() << endl; + while (!queue.empty()) { + // process split candidate + RootId current = queue.back(); + queue.pop_back(); + SliceBlock* block = d_rootBlocks[current]; + block->computeBlockBase(queue); + } + debugCheckBase(); +} + + +void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp) { + TNode root = node.getKind() == kind::BITVECTOR_EXTRACT ? node[0] : node; + Assert (isRootTerm(root)); + Base base = getSliceBlock(getRootId(root))->getBase(); + base.decomposeNode(node, decomp); +} + +void 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(); + SliceBlock::const_iterator it = block->begin(); + for (; it != block->end(); ++it) { + Slice* slice = *it; + Base diff_points = slice->getBase().diffCutPoints(block_base); + Assert (diff_points == Base(block->getBitwidth())); + 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); + Assert (splinter->getBitwidth() == other->getBitwidth()); + } + } + } + } +} + + + + + + |