CVC3  2.4.1
cdlist.h
Go to the documentation of this file.
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 
48  virtual ContextObj* makeCopy(ContextMemoryManager* cmm) { return new(cmm) CDList<T>(*this); }
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(); }
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.
57  CDList(const CDList<T>& l): ContextObj(l), d_list(NULL), d_size(l.d_size) { }
58 public:
59  CDList(Context* context) : ContextObj(context), d_size(0) {
60  d_list = new std::deque<T>();
61  IF_DEBUG(setName("CDList");)
62  }
63  virtual ~CDList() { if(d_list != NULL) delete d_list; }
64  unsigned size() const { return d_size; }
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(); }
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  }
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  }
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;
88  const_iterator begin() const {
89  return d_list->begin();
90  }
91  const_iterator end() const {
92  return begin() + d_size;
93  }
94 };
95 
96 }
97 
98 #endif