diff options
author | Tim King <taking@cs.nyu.edu> | 2018-07-25 16:13:18 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-25 16:13:18 -0700 |
commit | d01aea38d45c8242a39be95c5c634182c6b3a902 (patch) | |
tree | 108bb7d90b6dd0bc4c93b73bf1c2606da42875d9 /src | |
parent | aae5e18cb1bc8a6774fa4293cc0b5016fab7c46e (diff) |
Removing support for CDHashMap::iterator's postfix increment. (#2208)
Diffstat (limited to 'src')
-rw-r--r-- | src/context/cdhashmap.h | 24 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 14 | ||||
-rw-r--r-- | 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 ); |