Removing support for CDHashMap::iterator's postfix increment. (#2208)

diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index f58bb65093f73fa2d95769fd1ea1049f12adc007..83a8f22c40dcb0cbcd5e03d166e7976f69afa15e 100644 (file)
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -425,29 +425,7 @@ public:
       return *this;
     }
 
-    // Postfix increment: requires a Proxy object to hold the
-    // intermediate value for dereferencing
-    class Proxy {
-      const std::pair<const Key, Data>* d_pair;
-
-    public:
-
-      Proxy(const std::pair<const Key, Data>& p) : d_pair(&p) {}
-
-      const std::pair<const Key, Data>& operator*() const {
-        return *d_pair;
-      }
-    };/* class CDHashMap<>::iterator::Proxy */
-
-    // Actual postfix increment: returns Proxy with the old value.
-    // Now, an expression like *i++ will return the current *i, and
-    // then advance the iterator.  However, don't try to use
-    // Proxy for anything else.
-    const Proxy operator++(int) {
-      Proxy e(*(*this));
-      ++(*this);
-      return e;
-    }
+    // Postfix increment is not yet supported.
   };/* class CDHashMap<>::iterator */
 
   typedef iterator const_iterator;

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 1637695e20176a6cea338d6abf5bb7afc109a3fe..29cd492c75634c04468a2a9aa767f78578826c06 100644 (file)
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -1705,14 +1705,16 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti
     return conjunction;
   }/* mkAnd() */
 
-  void TheorySetsRels::printNodeMap(char* fst, char* snd, NodeMap map) {
-    NodeMap::iterator map_it    = map.begin();
-    while(map_it != map.end()) {
-      Trace("rels-debug") << fst << " "<< (*map_it).first << " " << snd << " " << (*map_it).second<< std::endl;
-      map_it++;
+  void TheorySetsRels::printNodeMap(const char* fst,
+                                    const char* snd,
+                                    const NodeMap& map)
+  {
+    for (const auto& key_data : map)
+    {
+      Trace("rels-debug") << fst << " " << key_data.first << " " << snd << " "
+                          << key_data.second << std::endl;
     }
   }
-
 }
 }
 }

diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index e2807112d063e7241c4c1aa471ddcbda0b416e45..a95948bc70783c35dd524092695633e13b86596d 100644 (file)
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -187,7 +187,9 @@ private:
   bool exists( std::vector<Node>&, Node );
   Node mkAnd( std::vector< TNode >& assumptions );
   inline void addToMembershipDB( Node, Node, Node  );
-  void printNodeMap(char* fst, char* snd, NodeMap map);
+  static void printNodeMap(const char* fst,
+                           const char* snd,
+                           const NodeMap& map);
   inline Node constructPair(Node tc_rep, Node a, Node b);
   void addToMap( std::map< Node, std::vector<Node> >&, Node, Node );
   bool safelyAddToMap( std::map< Node, std::vector<Node> >&, Node, Node );