src/context/cdo.h

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