00001 /*****************************************************************************/ 00002 /*! 00003 * \file cdo.h 00004 * 00005 * Author: Clark Barrett 00006 * 00007 * Created: Wed Feb 12 17:27:43 2003 00008 * 00009 * <hr> 00010 * 00011 * License to use, copy, modify, sell and/or distribute this software 00012 * and its documentation for any purpose is hereby granted without 00013 * royalty, subject to the terms and conditions defined in the \ref 00014 * LICENSE file provided with this distribution. 00015 * 00016 * <hr> 00017 * 00018 */ 00019 /*****************************************************************************/ 00020 00021 #ifndef _cvc3__include__cdo_h_ 00022 #define _cvc3__include__cdo_h_ 00023 00024 #include "context.h" 00025 00026 namespace CVC3 { 00027 00028 /////////////////////////////////////////////////////////////////////////////// 00029 // // 00030 // Class: CDO (Context Dependent Object) // 00031 // Author: Clark Barrett // 00032 // Created: Wed Feb 12 17:28:25 2003 // 00033 // Description: Generic templated class for an object which must be saved // 00034 // and restored as contexts are pushed and popped. Requires // 00035 // that operator= be defined for the data class. // 00036 // // 00037 /////////////////////////////////////////////////////////////////////////////// 00038 template <class T> 00039 class CDO :public ContextObj { 00040 T d_data; 00041 00042 virtual ContextObj* makeCopy(ContextMemoryManager* cmm) 00043 { return new(cmm) CDO<T>(*this); } 00044 virtual void restoreData(ContextObj* data) { 00045 d_data = ((CDO<T>*)data)->d_data; 00046 } 00047 virtual void setNull(void) { d_data = T(); } 00048 00049 // Disable copy constructor and operator= 00050 // If you need these, use smartcdo instead 00051 CDO(const CDO<T>& cdo): ContextObj(cdo), d_data(cdo.d_data) { } 00052 CDO<T>& operator=(const CDO<T>& cdo) {} 00053 00054 public: 00055 CDO(Context* context) : ContextObj(context) 00056 { IF_DEBUG(setName("CDO")); } 00057 CDO(Context* context, const T& data, int scope = -1) 00058 : ContextObj(context) { 00059 IF_DEBUG(setName("CDO")); 00060 set(data, scope); 00061 } 00062 ~CDO() {} 00063 void set(const T& data, int scope=-1) { makeCurrent(scope); d_data = data; } 00064 const T& get() const { return d_data; } 00065 operator T() { return get(); } 00066 CDO<T>& operator=(const T& data) { set(data); return *this; } 00067 00068 }; 00069 00070 } 00071 00072 #endif