Branch data     Line data    Source code

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