From d01aea38d45c8242a39be95c5c634182c6b3a902 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 25 Jul 2018 16:13:18 -0700
Subject: [PATCH] Removing support for CDHashMap::iterator's postfix increment.
 (#2208)

---
 src/context/cdhashmap.h              | 24 +-----------------------
 src/theory/sets/theory_sets_rels.cpp | 14 ++++++++------
 src/theory/sets/theory_sets_rels.h   |  4 +++-
 3 files changed, 12 insertions(+), 30 deletions(-)

diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index f58bb6509..83a8f22c4 100644
--- 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 1637695e2..29cd492c7 100644
--- 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 e2807112d..a95948bc7 100644
--- 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 );
-- 
2.30.2