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