CVC3

cdlist.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file cdlist.h
00004  * 
00005  * Author: Clark Barrett
00006  * 
00007  * Created: Wed Feb 12 18:45:26 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__cdlist_h_
00022 #define _cvc3__include__cdlist_h_
00023 
00024 #include "context.h"
00025 #include <deque>
00026 
00027 namespace CVC3 {
00028 
00029 ///////////////////////////////////////////////////////////////////////////////
00030 //                                                                           //
00031 // Class: CDList (Context Dependent List)            //
00032 // Author: Clark Barrett                                                     //
00033 // Created: Wed Feb 12 17:28:25 2003               //
00034 // Description: Generic templated class for list which grows monotonically   //
00035 //              over time (if the context is not popped) but must also be    //
00036 //              saved and restored as contexts are pushed and popped.        //
00037 //                                                                           //
00038 ///////////////////////////////////////////////////////////////////////////////
00039 // TODO: more efficient implementation
00040 template <class T>
00041 class CDList :public ContextObj {
00042   //! The actual data.  
00043   /*! Use deque because it doesn't create/destroy data on resize.
00044     This pointer is only non-NULL in the master copy. */
00045   std::deque<T>* d_list; // 
00046   unsigned d_size;
00047 
00048   virtual ContextObj* makeCopy(ContextMemoryManager* cmm) { return new(cmm) CDList<T>(*this); }
00049   virtual void restoreData(ContextObj* data)
00050     { d_size = ((CDList<T>*)data)->d_size;
00051       while (d_list->size() > d_size) d_list->pop_back(); }
00052   virtual void setNull(void)
00053     { while (d_list->size()) d_list->pop_back(); d_size = 0; }
00054 
00055   // Copy constructor (private).  Do NOT copy d_list.  It's not used
00056   // in restore, and it will be deleted in destructor.
00057   CDList(const CDList<T>& l): ContextObj(l), d_list(NULL), d_size(l.d_size) { }
00058 public:
00059   CDList(Context* context) : ContextObj(context), d_size(0) {
00060     d_list = new std::deque<T>();
00061     IF_DEBUG(setName("CDList");)
00062   }
00063   virtual ~CDList() { if(d_list != NULL) delete d_list; }
00064   unsigned size() const { return d_size; }
00065   bool empty() const { return d_size == 0; }
00066   T& push_back(const T& data, int scope = -1)
00067    { makeCurrent(scope); d_list->push_back(data); ++d_size; return d_list->back(); }
00068   void pop_back()
00069   { DebugAssert(isCurrent() && getRestore() &&
00070                 d_size > ((CDList<T>*)getRestore())->d_size, "pop_back precond violated");
00071     d_list->pop_back(); --d_size; }
00072   const T& operator[](unsigned i) const {
00073     DebugAssert(i < size(),
00074     "CDList["+int2string(i)+"]: i < size="+int2string(size()));
00075     return (*d_list)[i];
00076   }
00077   const T& at(unsigned i) const {
00078     DebugAssert(i < size(),
00079     "CDList["+int2string(i)+"]: i < size="+int2string(size()));
00080     return (*d_list)[i];
00081   }
00082   const T& back() const {
00083     DebugAssert(size() > 0,
00084     "CDList::back(): size="+int2string(size()));
00085     return d_list->back();
00086   }
00087   typedef typename std::deque<T>::const_iterator const_iterator;
00088   const_iterator begin() const {
00089     return d_list->begin();
00090   }
00091   const_iterator end() const {
00092     return begin() + d_size;
00093   }
00094 };
00095 
00096 }
00097 
00098 #endif