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