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