CVC3  2.4.1
cdmap.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file cdmap.h
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Thu May 15 15:55:09 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__include__cdmap_h_
22 #define _cvc3__include__cdmap_h_
23 
24 #include <iterator>
25 #include "context.h"
26 
27 namespace CVC3 {
28 
29 ///////////////////////////////////////////////////////////////////////////////
30 // //
31 // Class: CDMap (Context Dependent Map) //
32 // Author: Sergey Berezin //
33 // Created: Thu May 15 15:55:09 2003 //
34 // Description: Generic templated class for a map which must be saved //
35 // and restored as contexts are pushed and popped. Requires //
36 // that operator= be defined for the data class, and //
37 // operator== for the key class. In addition, a hash<Key> //
38 // template specialization must be defined, or a hash class //
39 // explicitly provided in the template. //
40 // //
41 ///////////////////////////////////////////////////////////////////////////////
42 
43 // Auxiliary class: almost the same as CDO (see cdo.h), but on
44 // setNull() call it erases itself from the map.
45 
46 template <class Key, class Data, class HashFcn = std::hash<Key> > class CDMap;
47 
48 template <class Key, class Data, class HashFcn = std::hash<Key> >
49 class CDOmap :public ContextObj {
50  Key d_key;
51  Data d_data;
52  bool d_inMap; // whether the data must be in the map
54 
55  // Doubly-linked list for keeping track of elements in order of insertion
58 
60  { return new(cmm) CDOmap<Key, Data, HashFcn>(*this); }
61 
62  virtual void restoreData(ContextObj* data) {
64  if(p->d_inMap) { d_data = p->d_data; d_inMap = true; }
65  else setNull();
66  }
67  virtual void setNull(void) {
68  // Erase itself from the map and put itself into trash. We cannot
69  // "delete this" here, because it will break context operations in
70  // a non-trivial way.
71  if(d_cdmap->d_map.count(d_key) > 0) {
72  d_cdmap->d_map.erase(d_key);
73  d_cdmap->d_trash.push_back(this);
74  }
75  d_prev->d_next = d_next;
76  d_next->d_prev = d_prev;
77  if (d_cdmap->d_first == this) {
78  d_cdmap->d_first = d_next;
79  if (d_next == this) {
80  d_cdmap->d_first = NULL;
81  }
82  }
83  }
84 
85 public:
87  const Key& key, const Data& data, int scope = -1)
88  : ContextObj(context), d_key(key), d_inMap(false), d_cdmap(cdmap) {
89  set(data, scope);
90  IF_DEBUG(setName("CDOmap");)
91  CDOmap<Key, Data, HashFcn>*& first = d_cdmap->d_first;
92  if (first == NULL) {
93  first = d_next = d_prev = this;
94  }
95  else {
96  d_prev = first->d_prev;
97  d_next = first;
98  d_prev->d_next = first->d_prev = this;
99  }
100  }
101  ~CDOmap() {}
102  void set(const Data& data, int scope=-1) {
103  makeCurrent(scope); d_data = data; d_inMap = true;
104  }
105  const Key& getKey() const { return d_key; }
106  const Data& get() const { return d_data; }
107  operator Data() { return get(); }
108  CDOmap<Key, Data, HashFcn>& operator=(const Data& data) { set(data); return *this; }
110  if (d_next == d_cdmap->d_first) return NULL;
111  else return d_next;
112  }
113 }; // end of class CDOmap
114 
115 // Dummy subclass of ContextObj to serve as our data class
116 class CDMapData : public ContextObj {
118  { return new(cmm) CDMapData(*this); }
119  void restoreData(ContextObj* data) { }
120  void setNull(void) { }
121  public:
122  CDMapData(Context* context): ContextObj(context) { }
123  CDMapData(const ContextObj& co): ContextObj(co) { }
124 };
125 
126 // The actual class CDMap
127 template <class Key, class Data, class HashFcn>
128 class CDMap: public ContextObj {
129  friend class CDOmap<Key, Data, HashFcn>;
130  private:
132  // The vector of CDOmap objects to be destroyed
133  std::vector<CDOmap<Key, Data, HashFcn>*> d_trash;
136 
137  // Nothing to save; the elements take care of themselves
139  { return new(cmm) CDMapData(*this); }
140  // Similarly, nothing to restore
141  virtual void restoreData(ContextObj* data) { }
142 
143  // Destroy stale CDOmap objects from trash
144  void emptyTrash() {
145  for(typename std::vector<CDOmap<Key, Data, HashFcn>*>::iterator
146  i=d_trash.begin(), iend=d_trash.end(); i!=iend; ++i) {
147  delete *i;
148  free(*i);
149  }
150  d_trash.clear();
151  }
152 
153  virtual void setNull(void) {
154  // Delete all the elements and clear the map
155  for(typename std::hash_map<Key,CDOmap<Key, Data, HashFcn>*,HashFcn>::iterator
156  i=d_map.begin(), iend=d_map.end();
157  i!=iend; ++i) {
158  delete (*i).second;
159  free((*i).second);
160  }
161  d_map.clear();
162  emptyTrash();
163  }
164 public:
165  CDMap(Context* context, int scope = -1)
166  : ContextObj(context), d_first(NULL), d_context(context) {
167  IF_DEBUG(setName("CDMap")); ;
168  }
169  ~CDMap() { setNull(); }
170  // The usual operators of map
171  size_t size() const { return d_map.size(); }
172  size_t count(const Key& k) const { return d_map.count(k); }
173 
175 
176  // If a key is not present, a new object is created and inserted
178  emptyTrash();
179  typename std::hash_map<Key,CDOmap<Key, Data, HashFcn>*,HashFcn>::iterator i(d_map.find(k));
181  if(i == d_map.end()) { // Create new object
182  obj = new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, Data());
183  d_map[k] = obj;
184  } else {
185  obj = (*i).second;
186  }
187  return *obj;
188  }
189 
190  void insert(const Key& k, const Data& d, int scope = -1) {
191  emptyTrash();
192  typename std::hash_map<Key,CDOmap<Key, Data, HashFcn>*,HashFcn>::iterator i(d_map.find(k));
193  if(i == d_map.end()) { // Create new object
195  obj(new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, d, scope));
196  d_map[k] = obj;
197  } else {
198  (*i).second->set(d, scope);
199  }
200  }
201  // FIXME: no erase(), too much hassle to implement efficiently...
202 
203  // Iterator for CDMap: points to pair<const Key, CDOMap<Key, Data, HashFcn>&>;
204  // in most cases, this will be functionally similar to pair<const Key,Data>.
205  class iterator : public std::iterator<std::input_iterator_tag,std::pair<const Key, Data>,std::ptrdiff_t> {
206  private:
207  // Private members
208  typename std::hash_map<Key,CDOmap<Key, Data, HashFcn>*,HashFcn>::const_iterator d_it;
209  public:
210  // Constructor from std::hash_map
211  iterator(const typename std::hash_map<Key,CDOmap<Key, Data, HashFcn>*,HashFcn>::const_iterator& i)
212  : d_it(i) { }
213  // Copy constructor
214  iterator(const iterator& i): d_it(i.d_it) { }
215  // Default constructor
216  iterator() { }
217  // (Dis)equality
218  bool operator==(const iterator& i) const {
219  return d_it == i.d_it;
220  }
221  bool operator!=(const iterator& i) const {
222  return d_it != i.d_it;
223  }
224  // Dereference operators.
225  std::pair<const Key, Data> operator*() const {
226  const std::pair<const Key, CDOmap<Key, Data, HashFcn>*>& p(*d_it);
227  return std::pair<const Key, Data>(p.first, *p.second);
228  }
229  // Who needs an operator->() for maps anyway?...
230  // It'd be nice, but not possible by design.
231  //std::pair<const Key,Data>* operator->() const {
232  // return &(operator*());
233  //}
234 
235 
236  // Prefix and postfix increment
237  iterator& operator++() { ++d_it; return *this; }
238  // Postfix increment: requires a Proxy object to hold the
239  // intermediate value for dereferencing
240  class Proxy {
241  const std::pair<const Key, Data>* d_pair;
242  public:
243  Proxy(const std::pair<const Key, Data>& p): d_pair(&p) { }
244  std::pair<const Key, Data>& operator*() { return *d_pair; }
245  };
246  // Actual postfix increment: returns Proxy with the old value.
247  // Now, an expression like *i++ will return the current *i, and
248  // then advance the iterator. However, don't try to use Proxy for
249  // anything else.
251  Proxy e(*(*this));
252  ++(*this);
253  return e;
254  }
255  };
256 
257  iterator begin() const { return iterator(d_map.begin()); }
258  iterator end() const { return iterator(d_map.end()); }
259 
262  public:
265  // Default constructor
267  // (Dis)equality
268  bool operator==(const orderedIterator& i) const {
269  return d_it == i.d_it;
270  }
271  bool operator!=(const orderedIterator& i) const {
272  return d_it != i.d_it;
273  }
274  // Dereference operators.
275  std::pair<const Key, Data> operator*() const {
276  return std::pair<const Key, Data>(d_it->getKey(), d_it->get());
277  }
278 
279  // Prefix and postfix increment
280  orderedIterator& operator++() { d_it = d_it->next(); return *this; }
281  // Postfix increment: requires a Proxy object to hold the
282  // intermediate value for dereferencing
283  class Proxy {
284  const std::pair<const Key, Data>* d_pair;
285  public:
286  Proxy(const std::pair<const Key, Data>& p): d_pair(&p) { }
287  std::pair<const Key, Data>& operator*() { return *d_pair; }
288  };
289  // Actual postfix increment: returns Proxy with the old value.
290  // Now, an expression like *i++ will return the current *i, and
291  // then advance the orderedIterator. However, don't try to use Proxy for
292  // anything else.
294  Proxy e(*(*this));
295  ++(*this);
296  return e;
297  }
298  };
299 
300  orderedIterator orderedBegin() const { return orderedIterator(d_first); }
301  orderedIterator orderedEnd() const { return orderedIterator(NULL); }
302 
303  iterator find(const Key& k) const { return iterator(d_map.find(k)); }
304 
305 }; // end of class CDMap
306 
307 
308 }
309 
310 #endif
CDOmap< Key, Data, HashFcn > & ElementReference
Definition: cdmap.h:174
CDOmap< Key, Data, HashFcn > * d_first
Definition: cdmap.h:134
std::pair< const Key, Data > operator*() const
Definition: cdmap.h:225
iterator end() const
Definition: cdmap.h:258
orderedIterator orderedBegin() const
Definition: cdmap.h:300
std::hash_map< Key, CDOmap< Key, Data, HashFcn > *, HashFcn >::const_iterator d_it
Definition: cdmap.h:208
bool operator!=(const orderedIterator &i) const
Definition: cdmap.h:271
virtual void setNull(void)
Set the current object to be invalid.
Definition: cdmap.h:67
void set(const Data &data, int scope=-1)
Definition: cdmap.h:102
void insert(const Key &k, const Data &d, int scope=-1)
Definition: cdmap.h:190
void makeCurrent(int scope=-1)
Definition: context.h:274
std::pair< const Key, Data > operator*() const
Definition: cdmap.h:275
Key d_key
Definition: cdmap.h:50
bool operator!=(const iterator &i) const
Definition: cdmap.h:221
const CDOmap< Key, Data, HashFcn > * d_it
Definition: cdmap.h:261
virtual void restoreData(ContextObj *data)
Restore the current object from the given data.
Definition: cdmap.h:62
const Key & getKey() const
Definition: cdmap.h:105
bool d_inMap
Definition: cdmap.h:52
virtual void setNull(void)
Set the current object to be invalid.
Definition: cdmap.h:153
virtual ContextObj * makeCopy(ContextMemoryManager *cmm)
Make a copy of the current object so it can be restored to its current state.
Definition: cdmap.h:59
Data d_data
Definition: cdmap.h:51
std::vector< CDOmap< Key, Data, HashFcn > * > d_trash
Definition: cdmap.h:133
CDMapData(const ContextObj &co)
Definition: cdmap.h:123
CDOmap< Key, Data, HashFcn > * d_next
Definition: cdmap.h:57
const std::pair< const Key, Data > * d_pair
Definition: cdmap.h:284
void emptyTrash()
Definition: cdmap.h:144
void setNull(void)
Set the current object to be invalid.
Definition: cdmap.h:120
CDMapData(Context *context)
Definition: cdmap.h:122
size_t size() const
Definition: cdmap.h:171
virtual void restoreData(ContextObj *data)
Restore the current object from the given data.
Definition: cdmap.h:141
#define IF_DEBUG(code)
Definition: debug.h:406
CDMap< Key, Data, HashFcn > * d_cdmap
Definition: cdmap.h:53
CDOmap< Key, Data, HashFcn > & operator[](const Key &k)
Definition: cdmap.h:177
Proxy(const std::pair< const Key, Data > &p)
Definition: cdmap.h:286
Context * d_context
Definition: cdmap.h:135
Proxy operator++(int)
Definition: cdmap.h:250
orderedIterator & operator++()
Definition: cdmap.h:280
virtual ContextObj * makeCopy(ContextMemoryManager *cmm)
Make a copy of the current object so it can be restored to its current state.
Definition: cdmap.h:138
bool operator==(const iterator &i) const
Definition: cdmap.h:218
orderedIterator(const CDOmap< Key, Data, HashFcn > *p)
Definition: cdmap.h:263
size_t count(const Key &k) const
Definition: cdmap.h:172
~CDMap()
Definition: cdmap.h:169
iterator & operator++()
Definition: cdmap.h:237
CDMap(Context *context, int scope=-1)
Definition: cdmap.h:165
CDOmap< Key, Data, HashFcn > * next() const
Definition: cdmap.h:109
bool operator==(const orderedIterator &i) const
Definition: cdmap.h:268
iterator(const iterator &i)
Definition: cdmap.h:214
std::hash_map< Key, CDOmap< Key, Data, HashFcn > *, HashFcn > d_map
Definition: cdmap.h:131
iterator begin() const
Definition: cdmap.h:257
CDOmap< Key, Data, HashFcn > & operator=(const Data &data)
Definition: cdmap.h:108
iterator find(const Key &k) const
Definition: cdmap.h:303
std::pair< const Key, Data > & operator*()
Definition: cdmap.h:244
std::pair< const Key, Data > & operator*()
Definition: cdmap.h:287
CDOmap< Key, Data, HashFcn > * d_prev
Definition: cdmap.h:56
const std::pair< const Key, Data > * d_pair
Definition: cdmap.h:241
orderedIterator(const orderedIterator &i)
Definition: cdmap.h:264
iterator(const typename std::hash_map< Key, CDOmap< Key, Data, HashFcn > *, HashFcn >::const_iterator &i)
Definition: cdmap.h:211
void restoreData(ContextObj *data)
Restore the current object from the given data.
Definition: cdmap.h:119
ContextObj * makeCopy(ContextMemoryManager *cmm)
Make a copy of the current object so it can be restored to its current state.
Definition: cdmap.h:117
CDOmap(Context *context, CDMap< Key, Data, HashFcn > *cdmap, const Key &key, const Data &data, int scope=-1)
Definition: cdmap.h:86
Proxy(const std::pair< const Key, Data > &p)
Definition: cdmap.h:243
orderedIterator orderedEnd() const
Definition: cdmap.h:301