CVC3
cdo.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file cdo.h
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Wed Feb 12 17:27:43 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__cdo_h_
22 #define _cvc3__include__cdo_h_
23 
24 #include "context.h"
25 
26 namespace CVC3 {
27 
28 ///////////////////////////////////////////////////////////////////////////////
29 // //
30 // Class: CDO (Context Dependent Object) //
31 // Author: Clark Barrett //
32 // Created: Wed Feb 12 17:28:25 2003 //
33 // Description: Generic templated class for an object which must be saved //
34 // and restored as contexts are pushed and popped. Requires //
35 // that operator= be defined for the data class. //
36 // //
37 ///////////////////////////////////////////////////////////////////////////////
38 template <class T>
39 class CDO :public ContextObj {
40  T d_data;
41 
43  { return new(cmm) CDO<T>(*this); }
44  virtual void restoreData(ContextObj* data) {
45  d_data = ((CDO<T>*)data)->d_data;
46  }
47  virtual void setNull(void) { d_data = T(); }
48 
49  // Disable copy constructor and operator=
50  // If you need these, use smartcdo instead
51  CDO(const CDO<T>& cdo): ContextObj(cdo), d_data(cdo.d_data) { }
52  CDO<T>& operator=(const CDO<T>& cdo) {}
53 
54 public:
55  CDO(Context* context) : ContextObj(context)
56  { IF_DEBUG(setName("CDO");) }
57  CDO(Context* context, const T& data, int scope = -1)
58  : ContextObj(context) {
59  IF_DEBUG(setName("CDO")); ;
60  set(data, scope);
61  }
62  ~CDO() {}
63  void set(const T& data, int scope=-1) { makeCurrent(scope); d_data = data; }
64  const T& get() const { return d_data; }
65  operator T() { return get(); }
66  CDO<T>& operator=(const T& data) { set(data); return *this; }
67 
68 };
69 
70 }
71 
72 #endif