1 /*****************************************************************************/
2 /*!
3  * \file cdlist.h
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Wed Feb 12 18:45:26 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__include__cdlist_h_
22 #define _cvc3__include__cdlist_h_
23 
24 #include "context.h"
25 #include <deque>
26 
27 namespace CVC3 {
28 
29 ///////////////////////////////////////////////////////////////////////////////
30 //                                                                           //
31 // Class: CDList (Context Dependent List)				     //
32 // Author: Clark Barrett                                                     //
33 // Created: Wed Feb 12 17:28:25 2003					     //
34 // Description: Generic templated class for list which grows monotonically   //
35 //              over time (if the context is not popped) but must also be    //
36 //              saved and restored as contexts are pushed and popped.        //
37 //                                                                           //
38 ///////////////////////////////////////////////////////////////////////////////
39 // TODO: more efficient implementation
40 template <class T>
41 class CDList :public ContextObj {
42   //! The actual data.
43   /*! Use deque because it doesn't create/destroy data on resize.
44     This pointer is only non-NULL in the master copy. */
45   std::deque<T>* d_list; //
46   unsigned d_size;
47 
makeCopy(ContextMemoryManager * cmm)48   virtual ContextObj* makeCopy(ContextMemoryManager* cmm) { return new(cmm) CDList<T>(*this); }
restoreData(ContextObj * data)49   virtual void restoreData(ContextObj* data)
50     { d_size = ((CDList<T>*)data)->d_size;
51       while (d_list->size() > d_size) d_list->pop_back(); }
setNull(void)52   virtual void setNull(void)
53     { while (d_list->size()) d_list->pop_back(); d_size = 0; }
54 
55   // Copy constructor (private).  Do NOT copy d_list.  It's not used
56   // in restore, and it will be deleted in destructor.
CDList(const CDList<T> & l)57   CDList(const CDList<T>& l): ContextObj(l), d_list(NULL), d_size(l.d_size) { }
58 public:
CDList(Context * context)59   CDList(Context* context) : ContextObj(context), d_size(0) {
60     d_list = new std::deque<T>();
61     IF_DEBUG(setName("CDList");)
62   }
~CDList()63   virtual ~CDList() { if(d_list != NULL) delete d_list; }
size()64   unsigned size() const { return d_size; }
empty()65   bool empty() const { return d_size == 0; }
66   T& push_back(const T& data, int scope = -1)
67    { makeCurrent(scope); d_list->push_back(data); ++d_size; return d_list->back(); }
pop_back()68   void pop_back()
69   { DebugAssert(isCurrent() && getRestore() &&
70                 d_size > ((CDList<T>*)getRestore())->d_size, "pop_back precond violated");
71     d_list->pop_back(); --d_size; }
72   const T& operator[](unsigned i) const {
73     DebugAssert(i < size(),
74 		"CDList["+int2string(i)+"]: i < size="+int2string(size()));
75     return (*d_list)[i];
76   }
at(unsigned i)77   const T& at(unsigned i) const {
78     DebugAssert(i < size(),
79 		"CDList["+int2string(i)+"]: i < size="+int2string(size()));
80     return (*d_list)[i];
81   }
back()82   const T& back() const {
83     DebugAssert(size() > 0,
84 		"CDList::back(): size="+int2string(size()));
85     return d_list->back();
86   }
87   typedef typename std::deque<T>::const_iterator const_iterator;
begin()88   const_iterator begin() const {
89     return d_list->begin();
90   }
end()91   const_iterator end() const {
92     return begin() + d_size;
93   }
94 };
95 
96 }
97 
98 #endif
99