From: Tim King Date: Tue, 14 Aug 2012 17:50:57 +0000 (+0000) Subject: Switched a number of EqClassIterator operations to const as well as the internal... X-Git-Tag: cvc5-1.0.0~7873 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b43f87e90aec85a18b5b8c34f6111a9aacaa42ba;p=cvc5.git Switched a number of EqClassIterator operations to const as well as the internal EqualityEngine pointer. --- 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 */