diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-09 14:23:19 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-09 14:23:19 +0000 |
commit | f1352c1aa3cfd119f9f8f595d50eacf531b1513b (patch) | |
tree | af2dfb36ac9804e00a6d8baa72f79e15e90fe665 | |
parent | 5b65d0f80d56731fd7d07f491973bad14a85566e (diff) |
fix for bug 415
-rw-r--r-- | src/theory/uf/equality_engine.h | 40 |
1 files changed, 23 insertions, 17 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 5d5e0f1f3..6d30900ee 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -840,37 +840,43 @@ public: class EqClassIterator { - Node d_rep; - eq::EqualityNode d_curr; - Node d_curr_node; const eq::EqualityEngine* d_ee; + /** Starting node */ + EqualityNodeId d_start; + + /** Current node */ + EqualityNodeId d_current; + public: - EqClassIterator(): d_ee(NULL){ } + EqClassIterator(): d_ee(NULL), d_start(null_id), d_current(null_id) { } EqClassIterator(Node eqc, const eq::EqualityEngine* ee) : d_ee(ee) { Assert( d_ee->getRepresentative(eqc) == eqc ); - d_rep = eqc; - d_curr_node = eqc; - d_curr = d_ee->getEqualityNode(eqc); + d_current = d_start = d_ee->getNodeId(eqc); } Node operator*() const { - return d_curr_node; + return d_ee->d_nodes[d_current]; } bool operator==(const EqClassIterator& i) const { - return d_ee == i.d_ee && d_curr_node == i.d_curr_node; + return d_ee == i.d_ee && d_current == i.d_current; } bool operator!=(const EqClassIterator& i) const { return !(*this == i); } EqClassIterator& operator++() { - Node next = d_ee->d_nodes[ d_curr.getNext() ]; - Assert( d_rep==d_ee->getRepresentative(next) ); - if (d_rep != next) { // we end when we have cycled back to the original representative - d_curr_node = next; - d_curr = d_ee->getEqualityNode(d_curr.getNext()); - } else { - d_curr_node = Node::null(); + Assert(!isFinished()); + + // Find the next one + do { + d_current = d_ee->getEqualityNode(d_current).getNext(); + } while (d_ee->d_isInternal[d_current]); + + Assert(d_start == d_ee->getEqualityNode(d_current).getFind()); + + if (d_current == d_start) { + // we end when we have cycled back to the original representative + d_current = null_id; } return *this; } @@ -880,7 +886,7 @@ public: return i; } bool isFinished() const { - return d_curr_node == Node::null(); + return d_current == null_id; } };/* class EqClassIterator */ |