try foreach on CD datastructure

diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 47d112cd89c38eba337b72ae325a90b318838197..c57a315f57f07a89ac3912facdadc577d68c9306 100644 (file)
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -417,6 +417,7 @@ public:
     }
 
   };/* class CDList<>::const_iterator */
+  typedef const_iterator iterator;
 
   /**
    * Returns an iterator pointing to the first item in the list.

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 2cc182819d79f0a6da98112a52cd511fce41a4e0..42d417fc3feaa261f60bfe546bddb5a78f32c8fb 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1066,18 +1066,17 @@ void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
 (CDTNodeList* l, TNode S, bool polarity)
 {
-  for(typeof(l->begin()) i = l->begin(); i != l->end(); ++i) {
+  BOOST_FOREACH(TNode x, (*l) ) {
     Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
-                       << MEMBER(*i, d_eqEngine->getRepresentative(S))
+                       << MEMBER(x, d_eqEngine->getRepresentative(S))
                        << std::endl;
 
-    d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(*i),
+    d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x),
                               d_eqEngine->getRepresentative(S)));
 
     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
         !j.isFinished(); ++j) {
 
-      TNode x = (*i);
       TNode S = (*j);
       Node cur_atom = MEMBER(x, S);