CVC3  2.4.1
smartcdo.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file smartcdo.h
4  *\brief Smart context-dependent object wrapper
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Fri Nov 12 17:28:58 2004
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #ifndef _cvc3__include__smartcdo_h_
23 #define _cvc3__include__smartcdo_h_
24 
25 #include "cdo.h"
26 
27 namespace CVC3 {
28 
29 /*****************************************************************************/
30 /*!
31  *\class SmartCDO
32  *\brief SmartCDO
33  *
34  * Author: Clark Barrett
35  *
36  * Created: Fri Nov 12 17:33:31 2004
37  *
38  * Wrapper for CDO which automatically allocates and deletes a pointer to a
39  * CDO. This allows the copy constructor and operator= to be defined which are
40  * especially useful for storing CDO's in vectors. All operations are const to
41  * enable use as a member of CDLists.
42  *
43  * Be careful not to delete RefCDO during pop(), since this messes up
44  * the backtracking data structures. We delay the deletion by
45  * registering each RefCDO to be notified before and after each pop().
46  * This makes the use of SmartCDO somewhat more expensive, so use it
47  * with care.
48  *
49  */
50 /*****************************************************************************/
51 template <class T>
52 class SmartCDO {
53 
54  template <class U>
55  class RefCDO {
56  friend class SmartCDO;
57  unsigned d_refCount;
59  bool d_delay; //!< Whether to delay our own deletion
60 
61  class RefNotifyObj : public ContextNotifyObj {
62  friend class RefCDO;
64  //! Constructor
65  RefNotifyObj(RefCDO<U>* ref, Context* context)
66  : ContextNotifyObj(context), d_ref(ref) { }
67  void notifyPre() { d_ref->d_delay = true; }
68  void notify() {
69  d_ref->d_delay = false;
70  d_ref->kill();
71  }
72  };
73 
75 
76  friend class RefNotifyObj;
77 
78  RefCDO(Context* context): d_refCount(0), d_cdo(context), d_delay(false),
79  d_notifyObj(new RefNotifyObj(this, context)) {}
80 
81  RefCDO(Context* context, const U& cdo, int scope = -1)
82  : d_refCount(0), d_cdo(context, cdo, scope), d_delay(false),
83  d_notifyObj(new RefNotifyObj(this, context)) {}
84 
85  ~RefCDO() { delete d_notifyObj; }
86  //! Delete itself, unless delayed (then we'll be called again later)
87  void kill() { if(d_refCount==0 && !d_delay) delete this; }
88  };
89 
90  RefCDO<T>* d_data;
91 
92 public:
93  //! Check if the SmartCDO object is Null
94  bool isNull() const { return (d_data==NULL); }
95  //! Default constructor: create a Null SmartCDO object
96  SmartCDO(): d_data(NULL) { }
97  //! Create and initialize SmartCDO object at the current scope
98  SmartCDO(Context* context)
99  { d_data = new RefCDO<T>(context); d_data->d_refCount++; }
100  //! Create and initialize SmartCDO object at the given scope
101  SmartCDO(Context* context, const T& data, int scope = -1)
102  { d_data = new RefCDO<T>(context, data, scope); d_data->d_refCount++; }
103  //! Delete
105  { if (isNull()) return;
106  if (--d_data->d_refCount == 0) d_data->kill(); }
107 
108  SmartCDO(const SmartCDO<T>& cdo) : d_data(cdo.d_data)
109  { if (!isNull()) d_data->d_refCount++; }
110 
112  {
113  if (this == &cdo) return *this;
114  if (!isNull() && --(d_data->d_refCount)) d_data->kill();
115  d_data = cdo.d_data;
116  if (!isNull()) ++(d_data->d_refCount);
117  return *this;
118  }
119 
120  void set(const T& data, int scope=-1) const {
121  DebugAssert(!isNull(), "SmartCDO::set: we are Null");
122  d_data->d_cdo.set(data, scope);
123  }
124  const T& get() const {
125  DebugAssert(!isNull(), "SmartCDO::get: we are Null");
126  return d_data->d_cdo.get();
127  }
128  operator T() const { return get(); }
129  const SmartCDO<T>& operator=(const T& data) const {set(data); return *this;}
130 };
131 
132 }
133 
134 #endif
SmartCDO.
Definition: smartcdo.h:52
bool isNull() const
Check if the SmartCDO object is Null.
Definition: smartcdo.h:94
const SmartCDO< T > & operator=(const T &data) const
Definition: smartcdo.h:129
RefCDO(Context *context, const U &cdo, int scope=-1)
Definition: smartcdo.h:81
SmartCDO(Context *context)
Create and initialize SmartCDO object at the current scope.
Definition: smartcdo.h:98
#define DebugAssert(cond, str)
Definition: debug.h:408
friend class RefNotifyObj
Definition: smartcdo.h:76
SmartCDO(const SmartCDO< T > &cdo)
Definition: smartcdo.h:108
SmartCDO< T > & operator=(const SmartCDO< T > &cdo)
Definition: smartcdo.h:111
RefNotifyObj * d_notifyObj
Definition: smartcdo.h:74
SmartCDO(Context *context, const T &data, int scope=-1)
Create and initialize SmartCDO object at the given scope.
Definition: smartcdo.h:101
void set(const T &data, int scope=-1) const
Definition: smartcdo.h:120
bool d_delay
Whether to delay our own deletion.
Definition: smartcdo.h:59
~SmartCDO()
Delete.
Definition: smartcdo.h:104
void kill()
Delete itself, unless delayed (then we'll be called again later)
Definition: smartcdo.h:87
RefCDO(Context *context)
Definition: smartcdo.h:78
SmartCDO()
Default constructor: create a Null SmartCDO object.
Definition: smartcdo.h:96
RefNotifyObj(RefCDO< U > *ref, Context *context)
Constructor.
Definition: smartcdo.h:65
Definition: expr.cpp:35
RefCDO< T > * d_data
Definition: smartcdo.h:90