From: Liana Hadarean Date: Thu, 10 Jan 2013 19:30:23 +0000 (-0500) Subject: minor bug fixes X-Git-Tag: cvc5-1.0.0~7361^2~59 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=590e7f438dacbee1c349f431316e918de43e5a8e;p=cvc5.git minor bug fixes --- diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index 51775f72a..e49976572 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -29,6 +29,7 @@ using namespace std; void Base::decomposeNode(TNode node, std::vector& 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) { @@ -237,7 +238,7 @@ void Slicer::splitEqualities(TNode node, std::vector& equalities) { if (base1 != Base(width)) { // we split the equalities according to the base int last = 0; - for (unsigned i = 1; i < utils::getSize(t1); ++i) { + 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)); @@ -255,13 +256,13 @@ void Slicer::splitEqualities(TNode node, std::vector& equalities) { void Slicer::processEquality(TNode node) { Assert (node.getKind() == kind::EQUAL); Debug("bv-slicer") << "theory::bv::Slicer::processEquality " << node << endl; - std::vector 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]); - } + // std::vector 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) { @@ -269,7 +270,10 @@ void Slicer::registerSimpleEquality(TNode eq) { Debug("bv-slicer") << "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); @@ -284,7 +288,7 @@ void Slicer::registerSimpleEquality(TNode eq) { low_b = utils::getExtractLow(b); } - if (id_a == id_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); @@ -446,50 +450,17 @@ void Slicer::computeCoarsestBase() { debugCheckBase(); } -void Slicer::getExtractOverBase(TNode node, std::vector& decomp) { +// void Slicer::getExtractOverBase(TNode node, std::vector& decomp) { -} +// } + void Slicer::getBaseDecomposition(TNode node, std::vector& decomp) { - if (node.getKind() == kind::BITVECTOR_CONCAT) { - for (unsigned i = 0; i < node.getNumChildren(); ++i) { - TNode root = node[i].getKind() == kind::BITVECTOR_EXTRACT ? node[i][0] : node[i]; - Assert (isRootTerm(root)); - Base base = getSliceBlock(getRootId(root))->getBase(); - std::vector decomp_i; - base.decomposeNode(node[i], decomp_i); - // TODO: add check for extract and finish this code here - - if (node[i].getKind() == kind::BITVECTOR_EXTRACT) { - unsigned low = utils::getExtractLow(node[i]); - unsigned high = utils::getExtractHigh(node[i]); - unsigned size = 0; - bool add = false; - for (int i = decomp_i.size() - 1; i >= 0; --i) { - int size_i = utils::getSize(decomp_i[i]); - if (low > size + size_i - 1 && !add) { - add = true; - Node first = utils::mkExtract(decomp_i[i], size + size_i -1, low - size); - decomp.push_back(first); - } - if (high < size + size_i - 1 && add) { - add = false; - Node last = utils::mkExtract(decomp_i[i], size + size_i - 1, high - size); - decomp.push_back(last); - } - if(add) { - decomp.push_back(decomp_i[i]); - } - size += size_i; - } - } - } - } else { - TNode root = node.getKind() == kind::BITVECTOR_EXTRACT ? node[0] : node; - Assert (isRootTerm(root)); - Base base = getSliceBlock(getRootId(root))->getBase(); - base.decomposeNode(node, 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(); + base.decomposeNode(node, decomp); } void Slicer::debugCheckBase() { diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index cb4636fef..fa9b65ce1 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -303,7 +303,7 @@ typedef std::vector Splinters; typedef std::vector SliceBlocks; class Slicer { - std::vector d_simpleEqualities; /**< equalities of the form a[i0:j0] = b[i1:j1] */ + std::vector d_simpleEqualities; /**< equalities of the form a[i0:j0] = b[i1:j1] */ Roots d_roots; uint32_t d_numRoots; NodeRootIdMap d_nodeRootMap; @@ -323,9 +323,10 @@ public: */ void processEquality(TNode node); bool isCoreTerm(TNode node); + static void splitEqualities(TNode node, std::vector& equalities); private: void registerSimpleEquality(TNode node); - void splitEqualities(TNode node, std::vector& equalities); + TNode addSimpleTerm(TNode t); bool isRootTerm(TNode node); diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index d537b8e60..bb16e00ce 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -210,6 +210,13 @@ Node TheoryBV::ppRewrite(TNode t) Node result = RewriteRule::run(t); return Rewriter::rewrite(result); } + + if (t.getKind() == kind::EQUAL) { + std::vector equalities; + Slicer::splitEqualities(t, equalities); + return utils::mkAnd(equalities); + } + return t; }