fixing and refactoring the equality iterator

2 files changed, 126 insertions, 77 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 3ca540ae2..90de8d0d2 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1770,6 +1770,110 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger
   return !d_done;
 }
 
+EqClassesIterator::EqClassesIterator() :
+    d_ee(NULL), d_it(0) {
+}
+
+EqClassesIterator::EqClassesIterator(const eq::EqualityEngine* ee)
+: d_ee(ee)
+{
+  Assert(d_ee->consistent());
+  d_it = 0;
+  // Go to the first non-internal node that is it's own representative
+  if(d_it < d_ee->d_nodesCount && (d_ee->d_isInternal[d_it] || d_ee->getEqualityNode(d_it).getFind() != d_it)) {
+    ++d_it;
+  }
+}
+
+Node EqClassesIterator::operator*() const {
+  return d_ee->d_nodes[d_it];
+}
+
+bool EqClassesIterator::operator==(const EqClassesIterator& i) const {
+  return d_ee == i.d_ee && d_it == i.d_it;
+}
+
+bool EqClassesIterator::operator!=(const EqClassesIterator& i) const {
+  return !(*this == i);
+}
+
+EqClassesIterator& EqClassesIterator::operator++() {
+  ++d_it;
+  while(d_it < d_ee->d_nodesCount && (d_ee->d_isInternal[d_it] || d_ee->getEqualityNode(d_it).getFind() != d_it)) {
+    ++d_it;
+  }
+  return *this;
+}
+
+EqClassesIterator EqClassesIterator::operator++(int) {
+  EqClassesIterator i = *this;
+  ++*this;
+  return i;
+}
+
+bool EqClassesIterator::isFinished() const {
+  return d_it >= d_ee->d_nodesCount;
+}
+
+EqClassIterator::EqClassIterator()
+: d_ee(NULL)
+, d_start(null_id)
+, d_current(null_id)
+{}
+
+EqClassIterator::EqClassIterator(Node eqc, const eq::EqualityEngine* ee)
+: d_ee(ee)
+{
+  Assert(d_ee->consistent());
+  d_current = d_start = d_ee->getNodeId(eqc);
+  Assert(d_start == d_ee->getEqualityNode(d_start).getFind());
+  Assert (!d_ee->d_isInternal[d_start]);
+}
+
+Node EqClassIterator::operator*() const {
+  return d_ee->d_nodes[d_current];
+}
+
+bool EqClassIterator::operator==(const EqClassIterator& i) const {
+  return d_ee == i.d_ee && d_current == i.d_current;
+}
+
+bool EqClassIterator::operator!=(const EqClassIterator& i) const {
+  return !(*this == i);
+}
+
+EqClassIterator& EqClassIterator::operator++() {
+  Assert(!isFinished());
+
+  Assert(d_start == d_ee->getEqualityNode(d_current).getFind());
+  Assert(!d_ee->d_isInternal[d_current]);
+
+  // 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());
+  Assert(!d_ee->d_isInternal[d_current]);
+
+  if(d_current == d_start) {
+    // we end when we have cycled back to the original representative
+    d_current = null_id;
+  }
+  return *this;
+}
+
+EqClassIterator EqClassIterator::operator++(int) {
+  EqClassIterator i = *this;
+  ++*this;
+  return i;
+}
+
+bool EqClassIterator::isFinished() const {
+  return d_current == null_id;
+}
+
+
 } // Namespace uf
 } // Namespace theory
 } // Namespace CVC4
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 2d477c744..166362951 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -796,96 +796,41 @@ public:
 
 };
 
+/**
+ * Iterator to iterate over the equivalence classes.
+ */
 class EqClassesIterator {
-
   const eq::EqualityEngine* d_ee;
   size_t d_it;
 public:
-
-  EqClassesIterator(): d_ee(NULL), d_it(0){ }
-  EqClassesIterator(const eq::EqualityEngine* ee) : d_ee(ee) {
-    d_it = 0;
-    // Go to the first non-internal node that is it's own representative
-    if (d_it < d_ee->d_nodesCount && (d_ee->d_isInternal[d_it] || d_ee->getRepresentative(d_ee->d_nodes[d_it]) != d_ee->d_nodes[d_it])) {
-      ++*this;
-    }
-  }
-  Node operator*() const {
-    return d_ee->d_nodes[d_it];
-  }
-  bool operator==(const EqClassesIterator& i) const {
-    return d_ee == i.d_ee && d_it == i.d_it;
-  }
-  bool operator!=(const EqClassesIterator& i) const {
-    return !(*this == i);
-  }
-  EqClassesIterator& operator++() {
-    ++d_it;
-    while (d_it<d_ee->d_nodesCount && (d_ee->d_isInternal[d_it] || d_ee->getRepresentative(d_ee->d_nodes[d_it]) != d_ee->d_nodes[d_it])) {
-      ++d_it;
-    }
-    return *this;
-  }
-  EqClassesIterator operator++(int) {
-    EqClassesIterator i = *this;
-    ++*this;
-    return i;
-  }
-  bool isFinished() const {
-    return d_it>=d_ee->d_nodesCount;
-  }
+  EqClassesIterator();
+  EqClassesIterator(const eq::EqualityEngine* ee);
+  Node operator*() const;
+  bool operator==(const EqClassesIterator& i) const;
+  bool operator!=(const EqClassesIterator& i) const;
+  EqClassesIterator& operator++();
+  EqClassesIterator operator++(int);
+  bool isFinished() const;
 };/* class EqClassesIterator */
 
+/**
+ * Iterator to iterate over the equivalence class members.
+ */
 class EqClassIterator {
-
   const eq::EqualityEngine* d_ee;
-
   /** Starting node */
   EqualityNodeId d_start;
-
   /** Current node */
   EqualityNodeId d_current;
-
 public:
-
-  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_current = d_start = d_ee->getNodeId(eqc);
-  }
-  Node operator*() const {
-    return d_ee->d_nodes[d_current];
-  }
-  bool operator==(const EqClassIterator& i) const {
-    return d_ee == i.d_ee && d_current == i.d_current;
-  }
-  bool operator!=(const EqClassIterator& i) const {
-    return !(*this == i);
-  }
-  EqClassIterator& operator++() {
-    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;
-  }
-  EqClassIterator operator++(int) {
-    EqClassIterator i = *this;
-    ++*this;
-    return i;
-  }
-  bool isFinished() const {
-    return d_current == null_id;
-  }
+  EqClassIterator();
+  EqClassIterator(Node eqc, const eq::EqualityEngine* ee);
+  Node operator*() const;
+  bool operator==(const EqClassIterator& i) const;
+  bool operator!=(const EqClassIterator& i) const;
+  EqClassIterator& operator++();
+  EqClassIterator operator++(int);
+  bool isFinished() const;
 };/* class EqClassIterator */
 
 } // Namespace eq