diff options
author | lianah <lianahady@gmail.com> | 2013-01-30 20:02:47 -0500 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-01-30 20:02:47 -0500 |
commit | 6875e78dc08bd345061e38c0fabb0efd2ceff41d (patch) | |
tree | b00f837fd1e3140da24887028dbac6d0de844580 /src/theory/bv/slicer.h | |
parent | 76a7010156d3dc696b25c32483467ec39b92f2ed (diff) |
fixed some more bugs
Diffstat (limited to 'src/theory/bv/slicer.h')
-rw-r--r-- | src/theory/bv/slicer.h | 31 |
1 files changed, 19 insertions, 12 deletions
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index b27b85e65..c7451c288 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -60,6 +60,11 @@ public: bool isEmpty() const; std::string debugPrint() const; Index getBitwidth() const { return d_size; } + void clear() { + for (unsigned i = 0; i < d_repr.size(); ++i) { + d_repr[i] = 0; + } + } bool operator==(const Base& other) const { if (other.getBitwidth() != getBitwidth()) return false; @@ -110,40 +115,41 @@ struct NormalForm { * * @return */ - TermId getTerm(Index i, const UnionFind& uf) const; - std::string debugPrint(const UnionFind& uf) const; + std::pair<TermId, Index> getTerm(Index i, const UnionFind& uf) const; + std::string debugPrint(const UnionFind& uf) const; + void clear() { base.clear(); decomp.clear(); } }; class UnionFind { class Node { Index d_bitwidth; - TermId d_ch1, d_ch2; + TermId d_ch1, d_ch0; TermId d_repr; public: Node(Index b) : d_bitwidth(b), d_ch1(UndefinedId), - d_ch2(UndefinedId), + d_ch0(UndefinedId), d_repr(UndefinedId) {} TermId getRepr() const { return d_repr; } Index getBitwidth() const { return d_bitwidth; } - bool hasChildren() const { return d_ch1 != UndefinedId && d_ch2 != UndefinedId; } + bool hasChildren() const { return d_ch1 != UndefinedId && d_ch0 != UndefinedId; } TermId getChild(Index i) const { Assert (i < 2); - return i == 0? d_ch1 : d_ch2; + return i == 0? d_ch0 : d_ch1; } void setRepr(TermId id) { Assert (! hasChildren()); d_repr = id; } - void setChildren(TermId ch1, TermId ch2) { + void setChildren(TermId ch1, TermId ch0) { Assert (d_repr == UndefinedId && !hasChildren()); d_ch1 = ch1; - d_ch2 = ch2; + d_ch0 = ch0; } std::string debugPrint() const; }; @@ -165,7 +171,7 @@ class UnionFind { return d_nodes[id].getChild(i); } Index getCutPoint(TermId id) const { - return getBitwidth(getChild(id, 1)); + return getBitwidth(getChild(id, 0)); } bool hasChildren(TermId id) const { Assert (id < d_nodes.size()); @@ -176,9 +182,9 @@ class UnionFind { 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); + void setChildren(TermId id, TermId ch1, TermId ch0) { + Assert (id < d_nodes.size() && getBitwidth(id) == getBitwidth(ch1) + getBitwidth(ch0)); + d_nodes[id].setChildren(ch1, ch0); } @@ -201,6 +207,7 @@ public: Assert (id < d_nodes.size()); return d_nodes[id].getBitwidth(); } + std::string debugPrint(TermId id); }; |