CVC3

cdmap.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file cdmap.h
00004  *
00005  * Author: Sergey Berezin
00006  *
00007  * Created: Thu May 15 15:55:09 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  *
00016  * <hr>
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 // Class: CDMap (Context Dependent Map)              //
00032 // Author: Sergey Berezin                                                    //
00033 // Created: Thu May 15 15:55:09 2003               //
00034 // Description: Generic templated class for a map which must be saved        //
00035 //              and restored as contexts are pushed and popped.  Requires    //
00036 //              that operator= be defined for the data class, and            //
00037 //              operator== for the key class.   In addition, a hash<Key>     //
00038 //              template specialization must be defined, or a hash class     //
00039 //              explicitly provided in the template.                         //
00040 //                                                                           //
00041 ///////////////////////////////////////////////////////////////////////////////
00042 
00043 // Auxiliary class: almost the same as CDO (see cdo.h), but on
00044 // setNull() call it erases itself from the map.
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; // whether the data must be in the map
00053   CDMap<Key, Data, HashFcn>* d_cdmap;
00054 
00055   // Doubly-linked list for keeping track of elements in order of insertion
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     // Erase itself from the map and put itself into trash.  We cannot
00069     // "delete this" here, because it will break context operations in
00070     // a non-trivial way.
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), d_key(key), d_inMap(false), d_cdmap(cdmap) {
00089     set(data, scope);
00090     IF_DEBUG(setName("CDOmap");)
00091     CDOmap<Key, Data, HashFcn>*& 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   ~CDOmap() {}
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   CDOmap<Key, Data, HashFcn>& operator=(const Data& data) { set(data); return *this; }
00109   CDOmap<Key, Data, HashFcn>* next() const {
00110     if (d_next == d_cdmap->d_first) return NULL;
00111     else return d_next;
00112   }
00113 }; // end of class CDOmap
00114 
00115 // Dummy subclass of ContextObj to serve as our data class
00116 class CDMapData : public ContextObj {
00117   ContextObj* makeCopy(ContextMemoryManager* cmm)
00118     { return new(cmm) CDMapData(*this); }
00119   void restoreData(ContextObj* data) { }
00120   void setNull(void) { }
00121  public:
00122   CDMapData(Context* context): ContextObj(context) { }
00123   CDMapData(const ContextObj& co): ContextObj(co) { }
00124 };
00125 
00126 // The actual class CDMap
00127 template <class Key, class Data, class HashFcn>
00128 class CDMap: public ContextObj {
00129   friend class CDOmap<Key, Data, HashFcn>;
00130  private:
00131   std::hash_map<Key,CDOmap<Key, Data, HashFcn>*,HashFcn> d_map;
00132   // The vector of CDOmap objects to be destroyed
00133   std::vector<CDOmap<Key, Data, HashFcn>*> d_trash;
00134   CDOmap<Key, Data, HashFcn>* d_first;
00135   Context* d_context;
00136 
00137   // Nothing to save; the elements take care of themselves
00138   virtual ContextObj* makeCopy(ContextMemoryManager* cmm)
00139     { return new(cmm) CDMapData(*this); }
00140   // Similarly, nothing to restore
00141   virtual void restoreData(ContextObj* data) { }
00142 
00143   // Destroy stale CDOmap objects from trash
00144   void emptyTrash() {
00145     for(typename std::vector<CDOmap<Key, Data, HashFcn>*>::iterator
00146     i=d_trash.begin(), iend=d_trash.end(); i!=iend; ++i) {
00147       delete *i;
00148       free(*i);
00149     }
00150     d_trash.clear();
00151   }
00152 
00153   virtual void setNull(void) {
00154     // Delete all the elements and clear the map
00155     for(typename std::hash_map<Key,CDOmap<Key, Data, HashFcn>*,HashFcn>::iterator
00156     i=d_map.begin(), iend=d_map.end();
00157   i!=iend; ++i) {
00158       delete (*i).second;
00159       free((*i).second);
00160     }
00161     d_map.clear();
00162     emptyTrash();
00163   }
00164 public:
00165   CDMap(Context* context, int scope = -1)
00166     : ContextObj(context), d_first(NULL), d_context(context) {
00167     IF_DEBUG(setName("CDMap"));   ;
00168   }
00169   ~CDMap() { setNull(); }
00170   // The usual operators of map
00171   size_t size() const { return d_map.size(); }
00172   size_t count(const Key& k) const { return d_map.count(k); }
00173 
00174   typedef CDOmap<Key, Data, HashFcn>& ElementReference;
00175 
00176   // If a key is not present, a new object is created and inserted
00177   CDOmap<Key, Data, HashFcn>& operator[](const Key& k) {
00178     emptyTrash();
00179     typename std::hash_map<Key,CDOmap<Key, Data, HashFcn>*,HashFcn>::iterator i(d_map.find(k));
00180     CDOmap<Key, Data, HashFcn>* obj;
00181     if(i == d_map.end()) { // Create new object
00182       obj = new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, Data());
00183       d_map[k] = obj;
00184     } else {
00185       obj = (*i).second;
00186     }
00187     return *obj;
00188   }
00189 
00190   void insert(const Key& k, const Data& d, int scope = -1) {
00191     emptyTrash();
00192     typename std::hash_map<Key,CDOmap<Key, Data, HashFcn>*,HashFcn>::iterator i(d_map.find(k));
00193     if(i == d_map.end()) { // Create new object
00194       CDOmap<Key, Data, HashFcn>*
00195   obj(new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, d, scope));
00196       d_map[k] = obj;
00197     } else {
00198       (*i).second->set(d, scope);
00199     }
00200   }
00201   // FIXME: no erase(), too much hassle to implement efficiently...
00202 
00203   // Iterator for CDMap: points to pair<const Key, CDOMap<Key, Data, HashFcn>&>;
00204   // in most cases, this will be functionally similar to pair<const Key,Data>.
00205   class iterator : public std::iterator<std::input_iterator_tag,std::pair<const Key, Data>,std::ptrdiff_t> {
00206     private:
00207       // Private members
00208       typename std::hash_map<Key,CDOmap<Key, Data, HashFcn>*,HashFcn>::const_iterator d_it;
00209     public:
00210       // Constructor from std::hash_map
00211       iterator(const typename std::hash_map<Key,CDOmap<Key, Data, HashFcn>*,HashFcn>::const_iterator& i)
00212       : d_it(i) { }
00213       // Copy constructor
00214       iterator(const iterator& i): d_it(i.d_it) { }
00215       // Default constructor
00216       iterator() { }
00217       // (Dis)equality
00218       bool operator==(const iterator& i) const {
00219   return d_it == i.d_it;
00220       }
00221       bool operator!=(const iterator& i) const {
00222   return d_it != i.d_it;
00223       }
00224       // Dereference operators.
00225       std::pair<const Key, Data> operator*() const {
00226   const std::pair<const Key, CDOmap<Key, Data, HashFcn>*>& p(*d_it);
00227   return std::pair<const Key, Data>(p.first, *p.second);
00228       }
00229       // Who needs an operator->() for maps anyway?...
00230       // It'd be nice, but not possible by design.
00231       //std::pair<const Key,Data>* operator->() const {
00232       //  return &(operator*());
00233       //}
00234 
00235 
00236       // Prefix and postfix increment
00237       iterator& operator++() { ++d_it; return *this; }
00238       // Postfix increment: requires a Proxy object to hold the
00239       // intermediate value for dereferencing
00240       class Proxy {
00241   const std::pair<const Key, Data>* d_pair;
00242       public:
00243   Proxy(const std::pair<const Key, Data>& p): d_pair(&p) { }
00244   std::pair<const Key, Data>& operator*() { return *d_pair; }
00245       };
00246       // Actual postfix increment: returns Proxy with the old value.
00247       // Now, an expression like *i++ will return the current *i, and
00248       // then advance the iterator.  However, don't try to use Proxy for
00249       // anything else.
00250       Proxy operator++(int) {
00251   Proxy e(*(*this));
00252   ++(*this);
00253   return e;
00254       }
00255   };
00256 
00257   iterator begin() const { return iterator(d_map.begin()); }
00258   iterator end() const { return iterator(d_map.end()); }
00259 
00260   class orderedIterator {
00261       const CDOmap<Key, Data, HashFcn>* d_it;
00262     public:
00263       orderedIterator(const CDOmap<Key, Data, HashFcn>* p): d_it(p) {}
00264       orderedIterator(const orderedIterator& i): d_it(i.d_it) { }
00265       // Default constructor
00266       orderedIterator() { }
00267       // (Dis)equality
00268       bool operator==(const orderedIterator& i) const {
00269   return d_it == i.d_it;
00270       }
00271       bool operator!=(const orderedIterator& i) const {
00272   return d_it != i.d_it;
00273       }
00274       // Dereference operators.
00275       std::pair<const Key, Data> operator*() const {
00276   return std::pair<const Key, Data>(d_it->getKey(), d_it->get());
00277       }
00278 
00279       // Prefix and postfix increment
00280       orderedIterator& operator++() { d_it = d_it->next(); return *this; }
00281       // Postfix increment: requires a Proxy object to hold the
00282       // intermediate value for dereferencing
00283       class Proxy {
00284   const std::pair<const Key, Data>* d_pair;
00285       public:
00286   Proxy(const std::pair<const Key, Data>& p): d_pair(&p) { }
00287   std::pair<const Key, Data>& operator*() { return *d_pair; }
00288       };
00289       // Actual postfix increment: returns Proxy with the old value.
00290       // Now, an expression like *i++ will return the current *i, and
00291       // then advance the orderedIterator.  However, don't try to use Proxy for
00292       // anything else.
00293       Proxy operator++(int) {
00294   Proxy e(*(*this));
00295   ++(*this);
00296   return e;
00297       }
00298   };
00299 
00300   orderedIterator orderedBegin() const { return orderedIterator(d_first); }
00301   orderedIterator orderedEnd() const { return orderedIterator(NULL); }
00302 
00303   iterator find(const Key& k) const { return iterator(d_map.find(k)); }
00304 
00305 }; // end of class CDMap
00306 
00307 
00308 }
00309 
00310 #endif