diff options
author | Liana Hadarean <lianahady@gmail.com> | 2013-01-29 23:09:03 -0500 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2013-01-29 23:09:03 -0500 |
commit | 76a7010156d3dc696b25c32483467ec39b92f2ed (patch) | |
tree | d6c33846ae2d7de38556d9930c7a55a310fa756b /src/theory/bv/slicer.cpp | |
parent | 012f1543af4aa65bf1d9ab9444c36c009fcfeb2b (diff) |
fixing slicer bugs.
Diffstat (limited to 'src/theory/bv/slicer.cpp')
-rw-r--r-- | src/theory/bv/slicer.cpp | 50 |
1 files changed, 22 insertions, 28 deletions
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index c624b9c5e..80a52525d 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -207,17 +207,14 @@ void UnionFind::merge(TermId t1, TermId t2) { if (t1 == t2) return; - Node n1 = getNode(t1); - Node n2 = getNode(t2); - Assert (! n1.hasChildren() && ! n2.hasChildren()); - n1.setRepr(t2); + Assert (! hasChildren(t1) && ! hasChildren(t2)); + setRepr(t1, t2); d_representatives.erase(t1); } TermId UnionFind::find(TermId id) const { - Node node = getNode(id); - if (node.getRepr() != UndefinedId) - return find(node.getRepr()); + if (getRepr(id) != UndefinedId) + return find(getRepr(id)); return id; } /** @@ -231,27 +228,25 @@ TermId UnionFind::find(TermId id) const { void UnionFind::split(TermId id, Index i) { Debug("bv-slicer-uf") << "UnionFind::split " << id << " at " << i << endl; id = find(id); - Node node = getNode(id); - Debug("bv-slicer-uf") << " node: " << node.debugPrint() << endl; - Assert (i < node.getBitwidth()); + Debug("bv-slicer-uf") << " node: " << d_nodes[id].debugPrint() << endl; - if (i == 0 || i == node.getBitwidth()) { + if (i == 0 || i == getBitwidth(id)) { // nothing to do return; } - - if (!node.hasChildren()) { + Assert (i < getBitwidth(id)); + if (!hasChildren(id)) { // first time we split this term TermId bottom_id = addTerm(i); - TermId top_id = addTerm(node.getBitwidth() - i); - node.setChildren(top_id, bottom_id); + TermId top_id = addTerm(getBitwidth(id) - i); + setChildren(id, top_id, bottom_id); } else { - Index cut = node.getCutPoint(*this); + Index cut = getCutPoint(id); if (i < cut ) - split(node.getChild(0), i); + split(getChild(id, 1), i); else - split(node.getChild(1), i - cut); + split(getChild(id, 0), i - cut); } } @@ -271,32 +266,31 @@ void UnionFind::getDecomposition(const ExtractTerm& term, Decomposition& decomp) // making sure the term is aligned TermId id = find(term.id); - Node node = getNode(id); - Assert (term.high < node.getBitwidth()); + Assert (term.high < getBitwidth(id)); // because we split the node, this must be the whole extract - if (!node.hasChildren()) { - Assert (term.high == node.getBitwidth() - 1 && + if (!hasChildren(id)) { + Assert (term.high == getBitwidth(id) - 1 && term.low == 0); decomp.push_back(id); } - Index cut = node.getCutPoint(*this); + Index cut = getCutPoint(id); if (term.low < cut && term.high < cut) { // the extract falls entirely on the low child - ExtractTerm child_ex(node.getChild(0), term.high, term.low); + ExtractTerm child_ex(getChild(id, 0), term.high, term.low); getDecomposition(child_ex, decomp); } else if (term.low >= cut && term.high >= cut){ // the extract falls entirely on the high child - ExtractTerm child_ex(node.getChild(1), term.high - cut, term.low - cut); + ExtractTerm child_ex(getChild(id, 1), term.high - cut, term.low - cut); getDecomposition(child_ex, decomp); } else { // the extract is split over the two children - ExtractTerm low_child(node.getChild(0), cut - 1, term.low); + ExtractTerm low_child(getChild(id, 0), cut - 1, term.low); getDecomposition(low_child, decomp); - ExtractTerm high_child(node.getChild(1), term.high, cut); + ExtractTerm high_child(getChild(id, 1), term.high, cut); getDecomposition(high_child, decomp); } } @@ -397,7 +391,7 @@ void UnionFind::ensureSlicing(const ExtractTerm& term) { */ ExtractTerm Slicer::registerTerm(TNode node) { - Index low = 0, high = utils::getSize(node); + Index low = 0, high = utils::getSize(node) - 1; TNode n = node; if (node.getKind() == kind::BITVECTOR_EXTRACT) { n = node[0]; |