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