From f8c88fa4b7b9b2d59f48d0e33f1344196a06f5da Mon Sep 17 00:00:00 2001 From: lianah Date: Thu, 10 Jan 2013 20:44:58 -0500 Subject: [PATCH] fixed most bugs and added paranoid assertions --- src/theory/bv/bv_subtheory_core.cpp | 1 + src/theory/bv/slicer.cpp | 93 ++++++++++++++++++++++++----- src/theory/bv/slicer.h | 7 ++- src/theory/bv/theory_bv.cpp | 31 +++++----- src/util/utility.h | 5 +- 5 files changed, 102 insertions(+), 35 deletions(-) diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 8343ac3a6..1e74f86f2 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -110,6 +110,7 @@ bool CoreSolver::decomposeFact(TNode fact) { TNode b = eq[1]; std::vector a_decomp; std::vector b_decomp; + d_slicer->getBaseDecomposition(a, a_decomp); d_slicer->getBaseDecomposition(b, b_decomp); diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index e49976572..1dbb48eed 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -103,6 +103,32 @@ void Slice::addSplinter(Index i, Splinter* sp) { d_splinters[i] = sp; } +bool Slice::isConsistent() { + // check that base is consistent with slicings + // and that the slicings are continous + std::map::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; + + 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; +} + std::string Slice::debugPrint() { std::ostringstream os; os << d_base.debugPrint(); @@ -129,11 +155,13 @@ void SliceBlock::computeBlockBase(std::vector& queue) { // 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 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) { + 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; @@ -143,7 +171,7 @@ void SliceBlock::computeBlockBase(std::vector& queue) { Assert (i >= bottom->getLow()); if (sp != Undefined) { unsigned delta = i - bottom->getLow(); - // if we do need to split something else split it + // 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); @@ -152,7 +180,7 @@ void SliceBlock::computeBlockBase(std::vector& queue) { 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); @@ -267,7 +295,7 @@ void Slicer::processEquality(TNode node) { void Slicer::registerSimpleEquality(TNode eq) { Assert (eq.getKind() == kind::EQUAL); - Debug("bv-slicer") << "theory::bv::Slicer::registerSimpleEquality " << eq << endl; + Debug("bv-slicer-eq") << "theory::bv::Slicer::registerSimpleEquality " << eq << endl; TNode a = eq[0]; TNode b = eq[1]; @@ -311,7 +339,7 @@ void Slicer::registerSimpleEquality(TNode eq) { 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) { + 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 @@ -326,7 +354,7 @@ void Slicer::registerSimpleEquality(TNode eq) { Splinter* s = new Splinter(low -1 , 0); slice->addSplinter(0, s); } - if (high + granularity <= size) { + if (high + granularity < size) { Splinter* s = new Splinter(size - 1, high + 1); slice->addSplinter(high+1, s); } @@ -447,13 +475,9 @@ void Slicer::computeCoarsestBase() { SliceBlock* block = d_rootBlocks[current]; block->computeBlockBase(queue); } - debugCheckBase(); + Assert(debugCheckBase()); } -// void Slicer::getExtractOverBase(TNode node, std::vector& decomp) { - -// } - void Slicer::getBaseDecomposition(TNode node, std::vector& decomp) { Assert (node.getKind() != kind::BITVECTOR_CONCAT); @@ -463,7 +487,32 @@ void Slicer::getBaseDecomposition(TNode node, std::vector& decomp) { base.decomposeNode(node, decomp); } -void Slicer::debugCheckBase() { +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 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(); + 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]; @@ -471,19 +520,33 @@ void Slicer::debugCheckBase() { 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; + } Base diff_points = slice->getBase().diffCutPoints(block_base); - Assert (diff_points == Base(block->getBitwidth())); + if (diff_points != Base(block->getBitwidth())) { + 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); - Assert (splinter->getBitwidth() == other->getBitwidth()); + if (splinter->getBitwidth() != other->getBitwidth()) { + Debug("bv-slicer-check") << "Slicer::debugCheckBase inconsistent splinter pointer \n"; + return false; + } } } } } + return true; } diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index fa9b65ce1..4d430258d 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -70,7 +70,7 @@ public: void decomposeNode(TNode node, std::vector& decomp); - bool isCutPoint(Index index) { + bool isCutPoint (Index index) { Assert (index < d_size); // the last cut point is implicit if (index == d_size - 1) @@ -223,7 +223,8 @@ public: std::map::const_iterator end() { return d_splinters.end(); } - std::string debugPrint(); + std::string debugPrint(); + bool isConsistent(); }; class Slicer; @@ -341,7 +342,7 @@ private: RootId makeRoot(TNode n); Slice* makeSlice(TNode node); - void debugCheckBase(); + bool debugCheckBase(); public: Slice* getSlice(const SplinterPointer& sp) { Assert (sp != Undefined); diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index bb16e00ce..5af5b2d23 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -127,23 +127,24 @@ void TheoryBV::check(Effort e) // FIXME: this is not quite correct as it does not take into account cardinality constraints - if (d_coreSolver.isCoreTheory()) { + //if (d_coreSolver.isCoreTheory()) { // paranoid check to make sure results of bit-blaster agree with slicer for core theory - if (inConflict()) { - d_conflict = false; - d_bitblastSolver.addAssertions(new_assertions, Theory::EFFORT_FULL); - Assert (inConflict()); - } else { - d_bitblastSolver.addAssertions(new_assertions, Theory::EFFORT_FULL); - Assert (!inConflict()); - } + // if (inConflict()) { + // d_conflict = false; + // d_bitblastSolver.addAssertions(new_assertions, Theory::EFFORT_FULL); + // Assert (inConflict()); + // } else { + // d_bitblastSolver.addAssertions(new_assertions, Theory::EFFORT_FULL); + // Assert (!inConflict()); + // } + //} + //else { + + if (!inConflict() && !d_coreSolver.isCoreTheory()) { + // sending assertions to the bitblast solver if it's not just core theory + d_bitblastSolver.addAssertions(new_assertions, e); } - else { - if (!inConflict()) { - // sending assertions to the bitblast solver - d_bitblastSolver.addAssertions(new_assertions, e); - } - } + if (inConflict()) { sendConflict(); } diff --git a/src/util/utility.h b/src/util/utility.h index 72213764f..2084ccafb 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -70,8 +70,9 @@ inline InputIterator find_if_unique(InputIterator first, InputIterator last, Pre template inline T gcd(T a, T b) { while (b != 0) { - a = b; - b = a % b; + T t = b; + b = a % t; + a = t; } return a; } -- 2.30.2