src/context/cdlist.h

   1 /*********************                                                        */
   2 /*! \file cdlist.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): barrett, taking
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Context-dependent list class.
  15  **
  16  ** Context-dependent list class.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef __CVC4__CONTEXT__CDLIST_H
  22 #define __CVC4__CONTEXT__CDLIST_H
  23
  24 #include "context/context.h"
  25 #include "util/Assert.h"
  26
  27 namespace CVC4 {
  28 namespace context {
  29
  30 /**
  31  * Generic context-dependent dynamic array.  Note that for efficiency, this
  32  * implementation makes the following assumptions:
  33  * 1. Over time, objects are only added to the list.  Objects are only
  34  *    removed when a pop restores the list to a previous state.
  35  * 2. T objects can safely be copied using their copy constructor,
  36  *    operator=, and memcpy.
  37  */
  38 template <class T>
  39 class CDList : public ContextObj {
  40   /**
  41    * d_list is a dynamic array of objects of type T.
  42    */
  43   T* d_list;
  44
  45   /**
  46    * Whether to call the destructor when items are popped from the
  47    * list.  True by default, but can be set to false by setting the
  48    * second argument in the constructor to false.
  49    */
  50   bool d_callDestructor;
  51
  52   /**
  53    * Number of objects in d_list
  54    */
  55   unsigned d_size;
  56
  57   /**
  58    * Allocated size of d_list.
  59    */
  60   unsigned d_sizeAlloc;
  61
  62 protected:
  63
  64   /**
  65    * Implementation of mandatory ContextObj method save: simply copies the
  66    * current size to a copy using the copy constructor (the pointer and the
  67    * allocated size are *not* copied as they are not restored on a pop).
  68    * The saved information is allocated using the ContextMemoryManager.
  69    */
  70   ContextObj* save(ContextMemoryManager* pCMM) {
  71     return new(pCMM) CDList<T>(*this);
  72   }
  73
  74   /**
  75    * Implementation of mandatory ContextObj method restore: simply restores the
  76    * previous size.  Note that the list pointer and the allocated size are not
  77    * changed.
  78    */
  79   void restore(ContextObj* data) {
  80     if(d_callDestructor) {
  81       unsigned size = ((CDList<T>*)data)->d_size;
  82       while(d_size != size) {
  83         --d_size;
  84         d_list[d_size].~T();
  85       }
  86     } else {
  87       d_size = ((CDList<T>*)data)->d_size;
  88     }
  89   }
  90
  91 private:
  92
  93   /**
  94    * Private copy constructor used only by save above.  d_list and d_sizeAlloc
  95    * are not copied: only the base class information and d_size are needed in
  96    * restore.
  97    */
  98   CDList(const CDList<T>& l) :
  99     ContextObj(l),
 100     d_list(NULL),
 101     d_callDestructor(l.d_callDestructor),
 102     d_size(l.d_size),
 103     d_sizeAlloc(0) {
 104   }
 105
 106   /**
 107    * Reallocate the array with more space.
 108    * Throws bad_alloc if memory allocation fails.
 109    */
 110   void grow() {
 111     if(d_list == NULL) {
 112       // Allocate an initial list if one does not yet exist
 113       d_sizeAlloc = 10;
 114       d_list = (T*) malloc(sizeof(T) * d_sizeAlloc);
 115       if(d_list == NULL) {
 116         throw std::bad_alloc();
 117       }
 118     } else {
 119       // Allocate a new array with double the size
 120       d_sizeAlloc *= 2;
 121       T* tmpList = (T*) realloc(d_list, sizeof(T) * d_sizeAlloc);
 122       if(tmpList == NULL) {
 123         throw std::bad_alloc();
 124       }
 125       d_list = tmpList;
 126     }
 127   }
 128
 129 public:
 130   /**
 131    * Main constructor: d_list starts as NULL, size is 0
 132    */
 133  CDList(Context* context, bool callDestructor = true) :
 134    ContextObj(context),
 135    d_list(NULL),
 136    d_callDestructor(callDestructor),
 137    d_size(0),
 138    d_sizeAlloc(0) {
 139  }
 140
 141   /**
 142    * Destructor: delete the list
 143    */
 144   ~CDList() throw(AssertionException) {
 145     destroy();
 146
 147     if(d_callDestructor) {
 148       for(unsigned i = 0; i < d_size; ++i) {
 149         d_list[i].~T();
 150       }
 151     }
 152
 153     free(d_list);
 154   }
 155
 156   /**
 157    * Return the current size of (i.e. valid number of objects in) the list
 158    */
 159   unsigned size() const {
 160     return d_size;
 161   }
 162
 163   /**
 164    * Return true iff there are no valid objects in the list.
 165    */
 166   bool empty() const {
 167     return d_size == 0;
 168   }
 169
 170   /**
 171    * Add an item to the end of the list.
 172    */
 173   void push_back(const T& data) {
 174     makeCurrent();
 175
 176     if(d_size == d_sizeAlloc) {
 177       grow();
 178     }
 179
 180     ::new((void*)(d_list + d_size)) T(data);
 181     ++d_size;
 182   }
 183
 184   /**
 185    * Access to the ith item in the list.
 186    */
 187   const T& operator[](unsigned i) const {
 188     Assert(i < d_size, "index out of bounds in CDList::operator[]");
 189     return d_list[i];
 190   }
 191
 192   /**
 193    * Returns the most recent item added to the list.
 194    */
 195   const T& back() const {
 196     Assert(d_size > 0, "CDList::back() called on empty list");
 197     return d_list[d_size - 1];
 198   }
 199
 200   /**
 201    * Iterator for CDList class.  It has to be const because we don't allow
 202    * items in the list to be changed.  It's a straightforward wrapper around a
 203    * pointer.  Note that for efficiency, we implement only prefix increment and
 204    * decrement.  Also note that it's OK to create an iterator from an empty,
 205    * uninitialized list, as begin() and end() will have the same value (NULL).
 206    */
 207   class const_iterator {
 208     T* d_it;
 209
 210     const_iterator(T* it) : d_it(it) {}
 211
 212     friend class CDList<T>;
 213
 214   public:
 215
 216     const_iterator() : d_it(NULL) {}
 217
 218     inline bool operator==(const const_iterator& i) const {
 219       return d_it == i.d_it;
 220     }
 221
 222     inline bool operator!=(const const_iterator& i) const {
 223       return d_it != i.d_it;
 224     }
 225
 226     inline const T& operator*() const {
 227       return *d_it;
 228     }
 229
 230     /** Prefix increment */
 231     const_iterator& operator++() {
 232       ++d_it;
 233       return *this;
 234     }
 235
 236     /** Prefix decrement */
 237     const_iterator& operator--() { --d_it; return *this; }
 238
 239     // Postfix operations on iterators: requires a Proxy object to
 240     // hold the intermediate value for dereferencing
 241     class Proxy {
 242       const T* d_t;
 243
 244     public:
 245
 246       Proxy(const T& p): d_t(&p) {}
 247
 248       T& operator*() {
 249         return *d_t;
 250       }
 251     };/* class CDList<>::const_iterator::Proxy */
 252
 253     /** Postfix increment: returns Proxy with the old value. */
 254     Proxy operator++(int) {
 255       Proxy e(*(*this));
 256       ++(*this);
 257       return e;
 258     }
 259
 260     /** Postfix decrement: returns Proxy with the old value. */
 261     Proxy operator--(int) {
 262       Proxy e(*(*this));
 263       --(*this);
 264       return e;
 265     }
 266
 267   };/* class CDList<>::const_iterator */
 268
 269   /**
 270    * Returns an iterator pointing to the first item in the list.
 271    */
 272   const_iterator begin() const {
 273     return const_iterator(d_list);
 274   }
 275
 276   /**
 277    * Returns an iterator pointing one past the last item in the list.
 278    */
 279   const_iterator end() const {
 280     return const_iterator(d_list + d_size);
 281   }
 282
 283 };/* class CDList */
 284
 285 }/* CVC4::context namespace */
 286 }/* CVC4 namespace */
 287
 288 #endif /* __CVC4__CONTEXT__CDLIST_H */