From b43f87e90aec85a18b5b8c34f6111a9aacaa42ba Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Tue, 14 Aug 2012 17:50:57 +0000
Subject: [PATCH] Switched a number of EqClassIterator operations to const as
 well as the internal EqualityEngine pointer.

---
 src/theory/uf/equality_engine.h | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 0b461131e..7f216d634 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -789,26 +789,26 @@ public:
 
 class EqClassesIterator {
 
-  eq::EqualityEngine* d_ee;
+  const eq::EqualityEngine* d_ee;
   size_t d_it;
 
 public:
 
   EqClassesIterator(): d_ee(NULL), d_it(0){ }
-  EqClassesIterator(eq::EqualityEngine* ee) : d_ee(ee) {
+  EqClassesIterator(const eq::EqualityEngine* ee) : d_ee(ee) {
     d_it = 0;
     if ( d_it < d_ee->d_nodesCount &&
          d_ee->getRepresentative(d_ee->d_nodes[d_it]) != d_ee->d_nodes[d_it] ) {
       ++*this;
     }
   }
-  Node operator*() {
+  Node operator*() const {
     return d_ee->d_nodes[d_it];
   }
-  bool operator==(const EqClassesIterator& i) {
+  bool operator==(const EqClassesIterator& i) const {
     return d_ee == i.d_ee && d_it == i.d_it;
   }
-  bool operator!=(const EqClassesIterator& i) {
+  bool operator!=(const EqClassesIterator& i) const {
     return !(*this == i);
   }
   EqClassesIterator& operator++() {
@@ -826,7 +826,7 @@ public:
     ++*this;
     return i;
   }
-  bool isFinished() {
+  bool isFinished() const {
     return d_it>=d_ee->d_nodesCount;
   }
 };/* class EqClassesIterator */
@@ -836,24 +836,24 @@ class EqClassIterator {
   Node d_rep;
   eq::EqualityNode d_curr;
   Node d_curr_node;
-  eq::EqualityEngine* d_ee;
+  const eq::EqualityEngine* d_ee;
 
 public:
 
   EqClassIterator(): d_ee(NULL){ }
-  EqClassIterator(Node eqc, eq::EqualityEngine* ee) : d_ee(ee) {
+  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);
   }
-  Node operator*() {
+  Node operator*() const {
     return d_curr_node;
   }
-  bool operator==(const EqClassIterator& i) {
+  bool operator==(const EqClassIterator& i) const {
     return d_ee == i.d_ee && d_curr_node == i.d_curr_node;
   }
-  bool operator!=(const EqClassIterator& i) {
+  bool operator!=(const EqClassIterator& i) const {
     return !(*this == i);
   }
   EqClassIterator& operator++() {
@@ -872,7 +872,7 @@ public:
     ++*this;
     return i;
   }
-  bool isFinished() {
+  bool isFinished() const {
     return d_curr_node == Node::null();
   }
 };/* class EqClassIterator */
-- 
2.30.2