1 /*********************                                                        */
2 /*! \file cdo.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Morgan Deters, Clark Barrett, Tim King
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8  ** in the top-level source directory) and their institutional affiliations.
9  ** All rights reserved.  See the file COPYING in the top-level source
10  ** directory for licensing information.\endverbatim
11  **
12  ** \brief A context-dependent object.
13  **
14  ** A context-dependent object.
15  **/
16 
17 #include "cvc4_private.h"
18 
19 #ifndef __CVC4__CONTEXT__CDO_H
20 #define __CVC4__CONTEXT__CDO_H
21 
22 #include "base/cvc4_assert.h"
23 #include "context/context.h"
24 
25 
26 namespace CVC4 {
27 namespace context {
28 
29 /**
30  * Most basic template for context-dependent objects.  Simply makes a copy
31  * (using the copy constructor) of class T when saving, and copies it back
32  * (using operator=) during restore.
33  */
34 template <class T>
35 class CDO : public ContextObj {
36 
37   /**
38    * The data of type T being stored in this context-dependent object.
39    */
40   T d_data;
41 
42 protected:
43 
44   /**
45    * Copy constructor - it's private to ensure it is only used by save().
46    * Basic CDO objects, cannot be copied-they have to be unique.
47    */
CDO(const CDO<T> & cdo)48   CDO(const CDO<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {}
49 
50   /**
51    * operator= for CDO is private to ensure CDO object is not copied.
52    */
53   CDO<T>& operator=(const CDO<T>& cdo) = delete;
54 
55   /**
56    * Implementation of mandatory ContextObj method save: simply copies the
57    * current data to a copy using the copy constructor.  Memory is allocated
58    * using the ContextMemoryManager.
59    */
save(ContextMemoryManager * pCMM)60   ContextObj* save(ContextMemoryManager* pCMM) override
61   {
62     Debug("context") << "save cdo " << this;
63     ContextObj* p = new(pCMM) CDO<T>(*this);
64     Debug("context") << " to " << p << std::endl;
65     return p;
66   }
67 
68   /**
69    * Implementation of mandatory ContextObj method restore: simply copies the
70    * saved data back from the saved copy using operator= for T.
71    */
restore(ContextObj * pContextObj)72   void restore(ContextObj* pContextObj) override
73   {
74     //Debug("context") << "restore cdo " << this;
75     CDO<T>* p = static_cast<CDO<T>*>(pContextObj);
76     d_data = p->d_data;
77     //Debug("context") << " to " << get() << std::endl;
78     // Explicitly call destructor as it will not otherwise get called.
79     p->d_data.~T();
80   }
81 
82 public:
83 
84   /**
85    * Main constructor - uses default constructor for T to create the initial
86    * value of d_data.
87    */
CDO(Context * context)88   CDO(Context* context) :
89     ContextObj(context),
90     d_data(T()) {
91   }
92 
93   /**
94    * Main constructor - uses default constructor for T to create the
95    * initial value of d_data.
96    *
97    * This version takes an argument that specifies whether this CDO<>
98    * was itself allocated in context memory.  If it was, it is linked
99    * with the current scope rather than scope 0.
100    *
101    * WARNING: Read the notes in src/context/context.h on "Gotchas when
102    * allocating contextual objects with non-standard allocators."
103    */
CDO(bool allocatedInCMM,Context * context)104   CDO(bool allocatedInCMM, Context* context) :
105     ContextObj(allocatedInCMM, context),
106     d_data(T()) {
107   }
108 
109   /**
110    * Constructor from object of type T.  Creates a ContextObj and sets the data
111    * to the given data value.  Note that this value is only valid in the
112    * current Scope.  If the Scope is popped, the value will revert to whatever
113    * is assigned by the default constructor for T
114    */
CDO(Context * context,const T & data)115   CDO(Context* context, const T& data) :
116     ContextObj(context),
117     d_data(T()) {
118     makeCurrent();
119     d_data = data;
120   }
121 
122   /**
123    * Constructor from object of type T.  Creates a ContextObj and sets the data
124    * to the given data value.  Note that this value is only valid in the
125    * current Scope.  If the Scope is popped, the value will revert to whatever
126    * is assigned by the default constructor for T.
127    *
128    * This version takes an argument that specifies whether this CDO<>
129    * was itself allocated in context memory.  If it was, it is linked
130    * with the current scope rather than scope 0.
131    *
132    * WARNING: Read the notes in src/context/context.h on "Gotchas when
133    * allocating contextual objects with non-standard allocators."
134    */
CDO(bool allocatedInCMM,Context * context,const T & data)135   CDO(bool allocatedInCMM, Context* context, const T& data) :
136     ContextObj(allocatedInCMM, context),
137     d_data(T()) {
138     makeCurrent();
139     d_data = data;
140   }
141 
142   /**
143    * Destructor - call destroy() method
144    */
~CDO()145   ~CDO() { destroy(); }
146 
147   /**
148    * Set the data in the CDO.  First call makeCurrent.
149    */
set(const T & data)150   void set(const T& data) {
151     makeCurrent();
152     d_data = data;
153   }
154 
155   /**
156    * Get the current data from the CDO.  Read-only.
157    */
get()158   const T& get() const { return d_data; }
159 
160   /**
161    * For convenience, define operator T() to be the same as get().
162    */
T()163   operator T() { return get(); }
164 
165   /**
166    * For convenience, define operator const T() to be the same as get().
167    */
T()168   operator const T() const { return get(); }
169 
170   /**
171    * For convenience, define operator= that takes an object of type T.
172    */
173   CDO<T>& operator=(const T& data) {
174     set(data);
175     return *this;
176   }
177 
178 };/* class CDO */
179 
180 }/* CVC4::context namespace */
181 }/* CVC4 namespace */
182 
183 #endif /* __CVC4__CONTEXT__CDO_H */
184