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.h | |
parent | 012f1543af4aa65bf1d9ab9444c36c009fcfeb2b (diff) |
fixing slicer bugs.
Diffstat (limited to 'src/theory/bv/slicer.h')
-rw-r--r-- | src/theory/bv/slicer.h | 43 |
1 files changed, 30 insertions, 13 deletions
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index c4b3b06a1..b27b85e65 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -119,7 +119,7 @@ class UnionFind { class Node { Index d_bitwidth; TermId d_ch1, d_ch2; - TermId d_repr; + TermId d_repr; public: Node(Index b) : d_bitwidth(b), @@ -136,23 +136,18 @@ class UnionFind { Assert (i < 2); return i == 0? d_ch1 : d_ch2; } - Index getCutPoint(const UnionFind& uf) const { - Assert (d_ch1 != UndefinedId && d_ch2 != UndefinedId); - return uf.getNode(d_ch1).getBitwidth(); - } void setRepr(TermId id) { Assert (! hasChildren()); d_repr = id; } - void setChildren(TermId ch1, TermId ch2) { Assert (d_repr == UndefinedId && !hasChildren()); d_ch1 = ch1; d_ch2 = ch2; } - std::string debugPrint() const; + std::string debugPrint() const; }; - + /// map from TermId to the nodes that represent them std::vector<Node> d_nodes; /// a term is in this set if it is its own representative @@ -160,6 +155,32 @@ class UnionFind { void getDecomposition(const ExtractTerm& term, Decomposition& decomp); void handleCommonSlice(const Decomposition& d1, const Decomposition& d2, TermId common); + /// getter methods for the internal nodes + TermId getRepr(TermId id) const { + Assert (id < d_nodes.size()); + return d_nodes[id].getRepr(); + } + TermId getChild(TermId id, Index i) const { + Assert (id < d_nodes.size()); + return d_nodes[id].getChild(i); + } + Index getCutPoint(TermId id) const { + return getBitwidth(getChild(id, 1)); + } + bool hasChildren(TermId id) const { + Assert (id < d_nodes.size()); + return d_nodes[id].hasChildren(); + } + /// setter methods for the internal nodes + void setRepr(TermId id, TermId new_repr) { + Assert (id < d_nodes.size()); + d_nodes[id].setRepr(new_repr); + } + void setChildren(TermId id, TermId ch1, TermId ch2) { + Assert (id < d_nodes.size() && getBitwidth(id) == getBitwidth(ch1) + getBitwidth(ch2)); + d_nodes[id].setChildren(ch1, ch2); + } + public: UnionFind() @@ -176,11 +197,6 @@ public: void getNormalForm(const ExtractTerm& term, NormalForm& nf); void alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2); void ensureSlicing(const ExtractTerm& term); - - Node getNode(TermId id) const { - Assert (id < d_nodes.size()); - return d_nodes[id]; - } Index getBitwidth(TermId id) const { Assert (id < d_nodes.size()); return d_nodes[id].getBitwidth(); @@ -208,6 +224,7 @@ public: static void splitEqualities(TNode node, std::vector<Node>& equalities); }; + }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |