00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021 #ifndef _cvc3__include__cdmap_ordered_h_
00022 #define _cvc3__include__cdmap_ordered_h_
00023
00024 #include <map>
00025 #include <iterator>
00026 #include "context.h"
00027
00028 namespace CVC3 {
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042
00043
00044
00045 template <class Key, class Data> class CDMapOrdered;
00046
00047 template <class Key, class Data>
00048 class CDOmapOrdered :public ContextObj {
00049 Key d_key;
00050 Data d_data;
00051 bool d_inMap;
00052 CDMapOrdered<Key, Data>* d_cdmap;
00053
00054
00055 CDOmapOrdered<Key,Data>* d_prev;
00056 CDOmapOrdered<Key,Data>* d_next;
00057
00058 virtual ContextObj* makeCopy(ContextMemoryManager* cmm)
00059 { return new(cmm) CDOmapOrdered<Key,Data>(*this); }
00060
00061 virtual void restoreData(ContextObj* data) {
00062 CDOmapOrdered<Key,Data>* p((CDOmapOrdered<Key,Data>*)data);
00063 if(p->d_inMap) { d_data = p->d_data; d_inMap = true; }
00064 else setNull();
00065 }
00066 virtual void setNull(void) {
00067
00068
00069
00070 if(d_cdmap->d_map.count(d_key) > 0) {
00071 d_cdmap->d_map.erase(d_key);
00072 d_cdmap->d_trash.push_back(this);
00073 }
00074 d_prev->d_next = d_next;
00075 d_next->d_prev = d_prev;
00076 if (d_cdmap->d_first == this) {
00077 d_cdmap->d_first = d_next;
00078 if (d_next == this) {
00079 d_cdmap->d_first = NULL;
00080 }
00081 }
00082 }
00083
00084 public:
00085 CDOmapOrdered(Context* context, CDMapOrdered<Key, Data>* cdmap,
00086 const Key& key, const Data& data, int scope = -1)
00087 : ContextObj(context, true ),
00088 d_key(key), d_inMap(false), d_cdmap(cdmap) {
00089 set(data, scope);
00090 IF_DEBUG(setName("CDOmapOrdered"));
00091 CDOmapOrdered<Key, Data>*& first = d_cdmap->d_first;
00092 if (first == NULL) {
00093 first = d_next = d_prev = this;
00094 }
00095 else {
00096 d_prev = first->d_prev;
00097 d_next = first;
00098 d_prev->d_next = first->d_prev = this;
00099 }
00100 }
00101 ~CDOmapOrdered() {}
00102 void set(const Data& data, int scope=-1) {
00103 makeCurrent(scope); d_data = data; d_inMap = true;
00104 }
00105 const Key& getKey() const { return d_key; }
00106 const Data& get() const { return d_data; }
00107 operator Data() { return get(); }
00108 CDOmapOrdered<Key,Data>& operator=(const Data& data) { set(data); return *this; }
00109 CDOmapOrdered<Key,Data>* next() const {
00110 if (d_next == d_cdmap->d_first) return NULL;
00111 else return d_next;
00112 }
00113 };
00114
00115
00116 class CDMapOrderedData : public ContextObj {
00117 ContextObj* makeCopy(ContextMemoryManager* cmm)
00118 { return new(cmm) CDMapOrderedData(*this); }
00119 void restoreData(ContextObj* data) { }
00120 void setNull(void) { }
00121 public:
00122 CDMapOrderedData(Context* context): ContextObj(context) { }
00123 CDMapOrderedData(const ContextObj& co): ContextObj(co) { }
00124 };
00125
00126
00127 template <class Key, class Data>
00128 class CDMapOrdered: public ContextObj {
00129 friend class CDOmapOrdered<Key, Data>;
00130 private:
00131 std::map<Key,CDOmapOrdered<Key,Data>*> d_map;
00132
00133 std::vector<CDOmapOrdered<Key,Data>*> d_trash;
00134 CDOmapOrdered<Key,Data>* d_first;
00135 Context* d_context;
00136
00137
00138 virtual ContextObj* makeCopy(ContextMemoryManager* cmm)
00139 { return new(cmm) CDMapOrderedData(*this); }
00140
00141 virtual void restoreData(ContextObj* data) { }
00142
00143
00144 void emptyTrash() {
00145 for(typename std::vector<CDOmapOrdered<Key,Data>*>::iterator
00146 i=d_trash.begin(), iend=d_trash.end(); i!=iend; ++i)
00147 delete *i;
00148 d_trash.clear();
00149 }
00150
00151 virtual void setNull(void) {
00152
00153 for(typename std::map<Key,CDOmapOrdered<Key,Data>*>::iterator
00154 i=d_map.begin(), iend=d_map.end();
00155 i!=iend; ++i) delete (*i).second;
00156 d_map.clear();
00157 emptyTrash();
00158 }
00159 public:
00160 CDMapOrdered(Context* context, int scope = -1)
00161 : ContextObj(context), d_first(NULL), d_context(context) {
00162 IF_DEBUG(setName("CDMapOrdered"));
00163 }
00164 ~CDMapOrdered() { setNull(); }
00165
00166 size_t size() const { return d_map.size(); }
00167 size_t count(const Key& k) const { return d_map.count(k); }
00168
00169
00170 CDOmapOrdered<Key,Data>& operator[](const Key& k) {
00171 emptyTrash();
00172 typename std::map<Key,CDOmapOrdered<Key,Data>*>::iterator i(d_map.find(k));
00173 CDOmapOrdered<Key,Data>* obj;
00174 if(i == d_map.end()) {
00175 obj = new CDOmapOrdered<Key,Data>(d_context, this, k, Data());
00176 d_map[k] = obj;
00177 } else {
00178 obj = (*i).second;
00179 }
00180 return *obj;
00181 }
00182
00183 void insert(const Key& k, const Data& d, int scope = -1) {
00184 emptyTrash();
00185 typename std::map<Key,CDOmapOrdered<Key,Data>*>::iterator i(d_map.find(k));
00186 if(i == d_map.end()) {
00187 CDOmapOrdered<Key,Data>*
00188 obj(new CDOmapOrdered<Key,Data>(d_context, this, k, d, scope));
00189 d_map[k] = obj;
00190 } else {
00191 (*i).second->set(d, scope);
00192 }
00193 }
00194
00195
00196
00197
00198 class iterator : public std::iterator<std::input_iterator_tag,std::pair<const Key, Data>,std::ptrdiff_t> {
00199 private:
00200
00201 typename std::map<Key,CDOmapOrdered<Key,Data>*>::const_iterator d_it;
00202 public:
00203
00204 iterator(const typename std::map<Key,CDOmapOrdered<Key,Data>*>::const_iterator& i)
00205 : d_it(i) { }
00206
00207 iterator(const iterator& i): d_it(i.d_it) { }
00208
00209 iterator() { }
00210
00211 bool operator==(const iterator& i) const {
00212 return d_it == i.d_it;
00213 }
00214 bool operator!=(const iterator& i) const {
00215 return d_it != i.d_it;
00216 }
00217
00218 std::pair<const Key, Data> operator*() const {
00219 const std::pair<const Key, CDOmapOrdered<Key,Data>*>& p(*d_it);
00220 return std::pair<const Key, Data>(p.first, *p.second);
00221 }
00222
00223
00224
00225
00226
00227
00228
00229
00230 iterator& operator++() { ++d_it; return *this; }
00231
00232
00233 class Proxy {
00234 const std::pair<const Key, Data>* d_pair;
00235 public:
00236 Proxy(const std::pair<const Key, Data>& p): d_pair(&p) { }
00237 std::pair<const Key, Data>& operator*() { return *d_pair; }
00238 };
00239
00240
00241
00242
00243 Proxy operator++(int) {
00244 Proxy e(*(*this));
00245 ++(*this);
00246 return e;
00247 }
00248 };
00249
00250 iterator begin() const { return iterator(d_map.begin()); }
00251 iterator end() const { return iterator(d_map.end()); }
00252
00253 class orderedIterator {
00254 const CDOmapOrdered<Key,Data>* d_it;
00255 public:
00256 orderedIterator(const CDOmapOrdered<Key,Data>* p): d_it(p) {}
00257 orderedIterator(const orderedIterator& i): d_it(i.d_it) { }
00258
00259 orderedIterator() { }
00260
00261 bool operator==(const orderedIterator& i) const {
00262 return d_it == i.d_it;
00263 }
00264 bool operator!=(const orderedIterator& i) const {
00265 return d_it != i.d_it;
00266 }
00267
00268 std::pair<const Key, Data> operator*() const {
00269 return std::pair<const Key, Data>(d_it->getKey(), d_it->get());
00270 }
00271
00272
00273 orderedIterator& operator++() { d_it = d_it->next(); return *this; }
00274
00275
00276 class Proxy {
00277 const std::pair<const Key, Data>* d_pair;
00278 public:
00279 Proxy(const std::pair<const Key, Data>& p): d_pair(&p) { }
00280 std::pair<const Key, Data>& operator*() { return *d_pair; }
00281 };
00282
00283
00284
00285
00286 Proxy operator++(int) {
00287 Proxy e(*(*this));
00288 ++(*this);
00289 return e;
00290 }
00291 };
00292
00293 orderedIterator orderedBegin() const { return orderedIterator(d_first); }
00294 orderedIterator orderedEnd() const { return orderedIterator(NULL); }
00295
00296 iterator find(const Key& k) const { return iterator(d_map.find(k)); }
00297
00298 };
00299
00300
00301 }
00302
00303 #endif