Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Clark Barrett, Morgan Deters, Tim King
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * A context-dependent object.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5parser_public.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__CONTEXT__CDO_H
      19                 :            : #define CVC5__CONTEXT__CDO_H
      20                 :            : 
      21                 :            : #include "context/context.h"
      22                 :            : 
      23                 :            : namespace cvc5::context {
      24                 :            : 
      25                 :            : /**
      26                 :            :  * Most basic template for context-dependent objects.  Simply makes a copy
      27                 :            :  * (using the copy constructor) of class T when saving, and copies it back
      28                 :            :  * (using operator=) during restore.
      29                 :            :  */
      30                 :            : template <class T>
      31                 :            : class CDO : public ContextObj {
      32                 :            : 
      33                 :            :   /**
      34                 :            :    * The data of type T being stored in this context-dependent object.
      35                 :            :    */
      36                 :            :   T d_data;
      37                 :            : 
      38                 :            : protected:
      39                 :            : 
      40                 :            :   /**
      41                 :            :    * Copy constructor - it's private to ensure it is only used by save().
      42                 :            :    * Basic CDO objects, cannot be copied-they have to be unique.
      43                 :            :    */
      44                 :  163590992 :   CDO(const CDO<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {}
      45                 :            : 
      46                 :            :   /**
      47                 :            :    * operator= for CDO is private to ensure CDO object is not copied.
      48                 :            :    */
      49                 :            :   CDO<T>& operator=(const CDO<T>& cdo) = delete;
      50                 :            : 
      51                 :            :   /**
      52                 :            :    * Implementation of mandatory ContextObj method save: simply copies the
      53                 :            :    * current data to a copy using the copy constructor.  Memory is allocated
      54                 :            :    * using the ContextMemoryManager.
      55                 :            :    */
      56                 :  163590992 :   ContextObj* save(ContextMemoryManager* pCMM) override
      57                 :            :   {
      58                 :  163590992 :     return new (pCMM) CDO<T>(*this);
      59                 :            :   }
      60                 :            : 
      61                 :            :   /**
      62                 :            :    * Implementation of mandatory ContextObj method restore: simply copies the
      63                 :            :    * saved data back from the saved copy using operator= for T.
      64                 :            :    */
      65                 :  163586727 :   void restore(ContextObj* pContextObj) override
      66                 :            :   {
      67                 :  163586727 :     CDO<T>* p = static_cast<CDO<T>*>(pContextObj);
      68                 :  163586727 :     d_data = p->d_data;
      69                 :            :     // Explicitly call destructor as it will not otherwise get called.
      70                 :   43671208 :     p->d_data.~T();
      71                 :  163586727 :   }
      72                 :            : 
      73                 :            : public:
      74                 :            : 
      75                 :            :   /**
      76                 :            :    * Main constructor - uses default constructor for T to create the initial
      77                 :            :    * value of d_data.
      78                 :            :    */
      79                 :    3021923 :   CDO(Context* context) :
      80                 :            :     ContextObj(context),
      81                 :    3021923 :     d_data(T()) {
      82                 :    3021923 :   }
      83                 :            : 
      84                 :            :   /**
      85                 :            :    * Constructor from object of type T.  Creates a ContextObj and sets the data
      86                 :            :    * to the given data value.  Note that this value is only valid in the
      87                 :            :    * current Scope.  If the Scope is popped, the value will revert to whatever
      88                 :            :    * is assigned by the default constructor for T
      89                 :            :    */
      90                 :   13845372 :   CDO(Context* context, const T& data) :
      91                 :            :     ContextObj(context),
      92                 :   13845372 :     d_data(T()) {
      93                 :   13845372 :     makeCurrent();
      94                 :   13845372 :     d_data = data;
      95                 :   13845372 :   }
      96                 :            : 
      97                 :            :   /**
      98                 :            :    * Destructor - call destroy() method
      99                 :            :    */
     100                 :   16782146 :   ~CDO() { destroy(); }
     101                 :            : 
     102                 :            :   /**
     103                 :            :    * Set the data in the CDO.  First call makeCurrent.
     104                 :            :    */
     105                 :  741617476 :   void set(const T& data) {
     106                 :  741617476 :     makeCurrent();
     107                 :  741617476 :     d_data = data;
     108                 :  741617476 :   }
     109                 :            : 
     110                 :            :   /**
     111                 :            :    * Get the current data from the CDO.  Read-only.
     112                 :            :    */
     113                 : 4416777010 :   const T& get() const { return d_data; }
     114                 :            : 
     115                 :            :   /**
     116                 :            :    * For convenience, define operator T() to be the same as get().
     117                 :            :    */
     118                 : 3036554271 :   operator T() { return get(); }
     119                 :            : 
     120                 :            :   /**
     121                 :            :    * For convenience, define operator const T() to be the same as get().
     122                 :            :    */
     123                 :  497921075 :   operator const T() const { return get(); }
     124                 :            : 
     125                 :            :   /**
     126                 :            :    * For convenience, define operator= that takes an object of type T.
     127                 :            :    */
     128                 :  740709031 :   CDO<T>& operator=(const T& data) {
     129                 :  740709031 :     set(data);
     130                 :  740709031 :     return *this;
     131                 :            :   }
     132                 :            : 
     133                 :            : };/* class CDO */
     134                 :            : 
     135                 :            : }  // namespace cvc5::context
     136                 :            : 
     137                 :            : #endif /* CVC5__CONTEXT__CDO_H */