smartcdo.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file smartcdo.h
00004  *\brief Smart context-dependent object wrapper
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Fri Nov 12 17:28:58 2004
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  */
00020 /*****************************************************************************/
00021 
00022 #ifndef _cvc3__include__smartcdo_h_
00023 #define _cvc3__include__smartcdo_h_
00024 
00025 #include "cdo.h"
00026 
00027 namespace CVC3 {
00028 
00029 /*****************************************************************************/
00030 /*!
00031  *\class SmartCDO
00032  *\brief SmartCDO
00033  *
00034  * Author: Clark Barrett
00035  *
00036  * Created: Fri Nov 12 17:33:31 2004
00037  *
00038  * Wrapper for CDO which automatically allocates and deletes a pointer to a
00039  * CDO.  This allows the copy constructor and operator= to be defined which are
00040  * especially useful for storing CDO's in vectors.  All operations are const to
00041  * enable use as a member of CDLists.
00042  *
00043  * Be careful not to delete RefCDO during pop(), since this messes up
00044  * the backtracking data structures.  We delay the deletion by
00045  * registering each RefCDO to be notified before and after each pop().
00046  * This makes the use of SmartCDO somewhat more expensive, so use it
00047  * with care.
00048  * 
00049  */
00050 /*****************************************************************************/
00051 template <class T>
00052 class SmartCDO {
00053 
00054   template <class U>
00055   class RefCDO {
00056     friend class SmartCDO;
00057     unsigned d_refCount;
00058     CDO<U> d_cdo;
00059     bool d_delay; //!< Whether to delay our own deletion
00060 
00061     class RefNotifyObj : public ContextNotifyObj {
00062       friend class RefCDO;
00063       RefCDO<U>* d_ref;
00064       //! Constructor
00065       RefNotifyObj(RefCDO<U>* ref, Context* context)
00066   : ContextNotifyObj(context), d_ref(ref) { }
00067       void notifyPre() { d_ref->d_delay = true; }
00068       void notify() {
00069   d_ref->d_delay = false;
00070   d_ref->kill();
00071       }
00072     };
00073 
00074     RefNotifyObj* d_notifyObj;
00075 
00076     friend class RefNotifyObj;
00077 
00078     RefCDO(Context* context): d_refCount(0), d_cdo(context), d_delay(false),
00079       d_notifyObj(new RefNotifyObj(this, context)) {}
00080 
00081     RefCDO(Context* context, const U& cdo, int scope = -1)
00082       : d_refCount(0), d_cdo(context, cdo, scope), d_delay(false),
00083       d_notifyObj(new RefNotifyObj(this, context)) {}
00084 
00085     ~RefCDO() { delete d_notifyObj; }
00086     //! Delete itself, unless delayed (then we'll be called again later)
00087     void kill() { if(d_refCount==0 && !d_delay) delete this; }
00088   };
00089 
00090   RefCDO<T>* d_data;
00091 
00092 public:
00093   //! Check if the SmartCDO object is Null
00094   bool isNull() const { return (d_data==NULL); }
00095   //! Default constructor: create a Null SmartCDO object
00096   SmartCDO(): d_data(NULL) { }
00097   //! Create and initialize SmartCDO object at the current scope
00098   SmartCDO(Context* context)
00099     { d_data = new RefCDO<T>(context); d_data->d_refCount++; }
00100   //! Create and initialize SmartCDO object at the given scope
00101   SmartCDO(Context* context, const T& data, int scope = -1)
00102     { d_data = new RefCDO<T>(context, data, scope); d_data->d_refCount++; }
00103   //! Delete 
00104   ~SmartCDO()
00105     { if (isNull()) return;
00106       if (--d_data->d_refCount == 0) d_data->kill(); }
00107 
00108   SmartCDO(const SmartCDO<T>& cdo) : d_data(cdo.d_data)
00109     { if (!isNull()) d_data->d_refCount++; }
00110 
00111   SmartCDO<T>& operator=(const SmartCDO<T>& cdo)
00112   {
00113     if (this == &cdo) return *this;
00114     if (!isNull() && --(d_data->d_refCount)) d_data->kill();
00115     d_data = cdo.d_data;
00116     if (!isNull()) ++(d_data->d_refCount);
00117     return *this;
00118   }
00119 
00120   void set(const T& data, int scope=-1) const {
00121     DebugAssert(!isNull(), "SmartCDO::set: we are Null");
00122     d_data->d_cdo.set(data, scope);
00123   }
00124   const T& get() const {
00125     DebugAssert(!isNull(), "SmartCDO::get: we are Null");
00126     return d_data->d_cdo.get();
00127   }
00128   operator T() const { return get(); }
00129   const SmartCDO<T>& operator=(const T& data) const {set(data); return *this;}
00130 };
00131 
00132 }
00133 
00134 #endif

Generated on Wed Nov 18 16:13:31 2009 for CVC3 by  doxygen 1.5.2