CVC3

cdmap_ordered.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file cdmap_ordered.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_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 // Class: CDMapOrdered (Context Dependent Map)             //
00033 // Author: Sergey Berezin                                                    //
00034 // Created: Thu May 15 15:55:09 2003               //
00035 // Description: Generic templated class for a map which must be saved        //
00036 //              and restored as contexts are pushed and popped.  Requires    //
00037 //              that operator= be defined for the data class, and            //
00038 //              operator< for the key class.                                 //
00039 //                                                                           //
00040 ///////////////////////////////////////////////////////////////////////////////
00041 
00042 // Auxiliary class: almost the same as CDO (see cdo.h), but on
00043 // setNull() call it erases itself from the map.
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; // whether the data must be in the map
00052   CDMapOrdered<Key, Data>* d_cdmap;
00053 
00054   // Doubly-linked list for keeping track of elements in order of insertion
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     // Erase itself from the map and put itself into trash.  We cannot
00068     // "delete this" here, because it will break context operations in
00069     // a non-trivial way.
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 /* use bottom scope */),
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 }; // end of class CDOmapOrdered
00114 
00115 // Dummy subclass of ContextObj to serve as our data class
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 // The actual class CDMapOrdered
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   // The vector of CDOmapOrdered objects to be destroyed
00133   std::vector<CDOmapOrdered<Key,Data>*> d_trash;
00134   CDOmapOrdered<Key,Data>* 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) CDMapOrderedData(*this); }
00140   // Similarly, nothing to restore
00141   virtual void restoreData(ContextObj* data) { }
00142   
00143   // Destroy stale CDOmapOrdered objects from trash
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     // Delete all the elements and clear the map
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   // The usual operators of map
00166   size_t size() const { return d_map.size(); }
00167   size_t count(const Key& k) const { return d_map.count(k); }
00168 
00169   // If a key is not present, a new object is created and inserted
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()) { // Create new object
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()) { // Create new object
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   // FIXME: no erase(), too much hassle to implement efficiently...
00195 
00196   // Iterator for CDMapOrdered: points to pair<const Key, CDOMap<Key,Data>&>;
00197   // in most cases, this will be functionally similar to pair<const Key,Data>.
00198   class iterator : public std::iterator<std::input_iterator_tag,std::pair<const Key, Data>,std::ptrdiff_t> {
00199     private:
00200       // Private members
00201       typename std::map<Key,CDOmapOrdered<Key,Data>*>::const_iterator d_it;
00202     public:
00203       // Constructor from std::map
00204       iterator(const typename std::map<Key,CDOmapOrdered<Key,Data>*>::const_iterator& i)
00205       : d_it(i) { }
00206       // Copy constructor
00207       iterator(const iterator& i): d_it(i.d_it) { }
00208       // Default constructor
00209       iterator() { }
00210       // (Dis)equality
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       // Dereference operators.
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       // Who needs an operator->() for maps anyway?...
00223       // It'd be nice, but not possible by design.
00224       //std::pair<const Key,Data>* operator->() const {
00225       //  return &(operator*());
00226       //}
00227       
00228 
00229       // Prefix and postfix increment
00230       iterator& operator++() { ++d_it; return *this; }
00231       // Postfix increment: requires a Proxy object to hold the
00232       // intermediate value for dereferencing
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       // Actual postfix increment: returns Proxy with the old value.
00240       // Now, an expression like *i++ will return the current *i, and
00241       // then advance the iterator.  However, don't try to use Proxy for
00242       // anything else.
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       // Default constructor
00259       orderedIterator() { }
00260       // (Dis)equality
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       // Dereference operators.
00268       std::pair<const Key, Data> operator*() const {
00269   return std::pair<const Key, Data>(d_it->getKey(), d_it->get());
00270       }
00271 
00272       // Prefix and postfix increment
00273       orderedIterator& operator++() { d_it = d_it->next(); return *this; }
00274       // Postfix increment: requires a Proxy object to hold the
00275       // intermediate value for dereferencing
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       // Actual postfix increment: returns Proxy with the old value.
00283       // Now, an expression like *i++ will return the current *i, and
00284       // then advance the orderedIterator.  However, don't try to use Proxy for
00285       // anything else.
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 }; // end of class CDMapOrdered
00299 
00300 
00301 }
00302 
00303 #endif