Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Tim King, Francois Bobot, Mathias Preiner
       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                 :            :  * Context-dependent First-In-First-Out queue class.
      14                 :            :  *
      15                 :            :  * This implementation may discard elements which are enqueued and dequeued
      16                 :            :  * at the same context level.
      17                 :            :  *
      18                 :            :  * The implementation is based on a CDList with one additional size_t
      19                 :            :  * for tracking the next element to dequeue from the list and additional
      20                 :            :  * size_t for tracking the previous size of the list.
      21                 :            :  */
      22                 :            : 
      23                 :            : #include "cvc5_private.h"
      24                 :            : 
      25                 :            : #ifndef CVC5__CONTEXT__CDQUEUE_H
      26                 :            : #define CVC5__CONTEXT__CDQUEUE_H
      27                 :            : 
      28                 :            : #include "context/context.h"
      29                 :            : #include "context/cdlist.h"
      30                 :            : 
      31                 :            : namespace cvc5::context {
      32                 :            : 
      33                 :            : template <class T, class CleanUp = DefaultCleanUp<T>, class Allocator = std::allocator<T> >
      34                 :            : class CDQueue;
      35                 :            : 
      36                 :            : /** We don't define a template with Allocator for the first implementation */
      37                 :            : template <class T, class CleanUp, class Allocator>
      38                 :            : class CDQueue : public CDList<T, CleanUp, Allocator> {
      39                 :            : private:
      40                 :            :   typedef CDList<T, CleanUp, Allocator> ParentType;
      41                 :            : 
      42                 :            : protected:
      43                 :            : 
      44                 :            :   /** Points to the next element in the current context to dequeue. */
      45                 :            :   size_t d_iter;
      46                 :            : 
      47                 :            :   /** Points to the size at the last save. */
      48                 :            :   size_t d_lastsave;
      49                 :            : 
      50                 :            :   /**
      51                 :            :    * Private copy constructor used only by save().
      52                 :            :    */
      53                 :   15011165 :   CDQueue(const CDQueue<T, CleanUp, Allocator>& l):
      54                 :            :     ParentType(l),
      55                 :   15011165 :     d_iter(l.d_iter),
      56                 :   15011165 :     d_lastsave(l.d_lastsave) {}
      57                 :            : 
      58                 :            :   /** Implementation of mandatory ContextObj method save:
      59                 :            :    *  We assume that the base class do the job inside their copy constructor.
      60                 :            :    */
      61                 :   15011165 :   ContextObj* save(ContextMemoryManager* pCMM) override
      62                 :            :   {
      63                 :   15011165 :     ContextObj* data = new(pCMM) CDQueue<T, CleanUp, Allocator>(*this);
      64                 :            :     // We save the d_size in d_lastsave and we should never destruct below this
      65                 :            :     // indices before the corresponding restore.
      66                 :   15011165 :     d_lastsave = ParentType::d_size;
      67                 :   15011165 :     return data;
      68                 :            :   }
      69                 :            : 
      70                 :            :   /**
      71                 :            :    * Implementation of mandatory ContextObj method restore: simply
      72                 :            :    * restores the previous size, iter and lastsave indices. Note that
      73                 :            :    * the list pointer and the allocated size are not changed.
      74                 :            :    */
      75                 :   15010881 :   void restore(ContextObj* data) override
      76                 :            :   {
      77                 :   15010881 :     CDQueue<T, CleanUp, Allocator>* qdata = static_cast<CDQueue<T, CleanUp, Allocator>*>(data);
      78                 :   15010881 :     d_iter = qdata->d_iter;
      79                 :   15010881 :     d_lastsave = qdata->d_lastsave;
      80                 :   15010881 :     ParentType::restore(data);
      81                 :   15010881 :   }
      82                 :            : 
      83                 :            : 
      84                 :            : 
      85                 :            : public:
      86                 :            : 
      87                 :            :   /** Creates a new CDQueue associated with the current context. */
      88                 :     571125 :  CDQueue(Context* context,
      89                 :            :          bool callCleanup = true,
      90                 :            :          const CleanUp& cleanup = CleanUp(),
      91                 :            :          const Allocator& alloc = Allocator())
      92                 :     571125 :      : ParentType(context, callCleanup, cleanup), d_iter(0), d_lastsave(0)
      93                 :            :  {
      94                 :     571125 :  }
      95                 :            : 
      96                 :            :  /** Returns true if the queue is empty in the current context. */
      97                 :  294729347 :  bool empty() const
      98                 :            :  {
      99 [ -  + ][ -  + ]:  294729347 :    Assert(d_iter <= ParentType::d_size);
                 [ -  - ]
     100                 :  294729347 :    return d_iter == ParentType::d_size;
     101                 :            :   }
     102                 :            : 
     103                 :            :   /** Returns the number of elements that have not been dequeued in the context. */
     104                 :      68131 :   size_t size() const{
     105                 :      68131 :     return ParentType::d_size - d_iter;
     106                 :            :   }
     107                 :            : 
     108                 :            :   /** Enqueues an element in the current context. */
     109                 :   65520360 :   void push(const T& data){
     110                 :   65520360 :     ParentType::push_back(data);
     111                 :   65520360 :   }
     112                 :            : 
     113                 :            :   /**
     114                 :            :    * Delete next element. The destructor of this object will be
     115                 :            :    * called eventually but not necessarily during the call of this
     116                 :            :    * function.
     117                 :            :    */
     118                 :   63070104 :   void pop(){
     119 [ -  + ][ -  + ]:   63070104 :     Assert(!empty()) << "Attempting to pop from an empty queue.";
                 [ -  - ]
     120                 :   63070104 :     ParentType::makeCurrent();
     121                 :   63070104 :     d_iter = d_iter + 1;
     122 [ +  + ][ +  + ]:   63070104 :     if (empty() && d_lastsave != ParentType::d_size) {
                 [ +  + ]
     123                 :            :       // Some elements have been enqueued and dequeued in the same
     124                 :            :       // context and now the queue is empty we can destruct them.
     125                 :   14260599 :       ParentType::truncateList(d_lastsave);
     126 [ -  + ][ -  + ]:   14260599 :       Assert(ParentType::d_size == d_lastsave);
                 [ -  - ]
     127                 :   14260599 :       d_iter = d_lastsave;
     128                 :            :     }
     129                 :   63070104 :   }
     130                 :            : 
     131                 :            :   /** Returns a reference to the next element on the queue. */
     132                 :   63070104 :   const T& front() const{
     133 [ -  + ][ -  + ]:   63070104 :     Assert(!empty()) << "No front in an empty queue.";
                 [ -  - ]
     134                 :   63070104 :     return ParentType::d_list[d_iter];
     135                 :            :   }
     136                 :            : 
     137                 :            :   /**
     138                 :            :    * Returns the most recent item added to the queue.
     139                 :            :    */
     140                 :            :   const T& back() const {
     141                 :            :     Assert(!empty()) << "CDQueue::back() called on empty list";
     142                 :            :     return ParentType::d_list[ParentType::d_size - 1];
     143                 :            :   }
     144                 :            : 
     145                 :            :   typedef typename ParentType::const_iterator const_iterator;
     146                 :            : 
     147                 :     105627 :   const_iterator begin() const {
     148                 :     105627 :     return ParentType::begin() + d_iter;
     149                 :            :   }
     150                 :            : 
     151                 :     105627 :   const_iterator end() const {
     152                 :     105627 :     return ParentType::end();
     153                 :            :   }
     154                 :            : 
     155                 :            : };/* class CDQueue<> */
     156                 :            : 
     157                 :            : }  // namespace cvc5::context
     158                 :            : 
     159                 :            : #endif /* CVC5__CONTEXT__CDQUEUE_H */