Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Tim King, Aina Niemetz, 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 queue class with an explicit trail of elements
      14                 :            :  *
      15                 :            :  * The implementation is based on a combination of CDList and a CDO<size_t>
      16                 :            :  * for tracking the next element to dequeue from the list.
      17                 :            :  * The implementation is currently not full featured.
      18                 :            :  */
      19                 :            : 
      20                 :            : #include "cvc5_private.h"
      21                 :            : 
      22                 :            : #ifndef CVC5__CONTEXT__CDTRAIL_QUEUE_H
      23                 :            : #define CVC5__CONTEXT__CDTRAIL_QUEUE_H
      24                 :            : 
      25                 :            : #include "context/cdlist.h"
      26                 :            : #include "context/cdo.h"
      27                 :            : 
      28                 :            : namespace cvc5::context {
      29                 :            : 
      30                 :            : class Context;
      31                 :            : 
      32                 :            : template <class T>
      33                 :            : class CDTrailQueue {
      34                 :            : private:
      35                 :            : 
      36                 :            :   /** List of elements in the queue. */
      37                 :            :   CDList<T> d_list;
      38                 :            : 
      39                 :            :   /** Points to the next element in the current context to dequeue. */
      40                 :            :   CDO<size_t> d_iter;
      41                 :            : 
      42                 :            : 
      43                 :            : public:
      44                 :            : 
      45                 :            :   /** Creates a new CDTrailQueue associated with the current context. */
      46                 :      49276 :   CDTrailQueue(Context* context)
      47                 :            :     : d_list(context),
      48                 :      49276 :       d_iter(context, 0)
      49                 :      49276 :   {}
      50                 :            : 
      51                 :            :   /** Returns true if the queue is empty in the current context. */
      52                 :    8899050 :   bool empty() const{
      53                 :    8899050 :     return d_iter >= d_list.size();
      54                 :            :   }
      55                 :            : 
      56                 :            :   /**
      57                 :            :    * Enqueues an element in the current context.
      58                 :            :    * Returns its index in the queue.
      59                 :            :    */
      60                 :    1156790 :   size_t enqueue(const T& data){
      61                 :    1156790 :     size_t res = d_list.size();
      62                 :    1156790 :     d_list.push_back(data);
      63                 :    1156790 :     return res;
      64                 :            :   }
      65                 :            : 
      66                 :    1098740 :   size_t frontIndex() const{
      67                 :    1098740 :     return d_iter;
      68                 :            :   }
      69                 :            : 
      70                 :    1098740 :   const T& front() const{
      71                 :    1098740 :     return d_list[frontIndex()];
      72                 :            :   }
      73                 :            : 
      74                 :            :   /** Moves the iterator for the queue forward. */
      75                 :    1098740 :   void dequeue(){
      76 [ -  + ][ -  + ]:    1098740 :     Assert(!empty()) << "Attempting to queue from an empty queue.";
                 [ -  - ]
      77                 :    1098740 :     d_iter = d_iter + 1;
      78                 :    1098740 :   }
      79                 :            : 
      80                 :      38502 :   const T& operator[](size_t index) const{
      81 [ -  + ][ -  + ]:      38502 :     Assert(index < d_list.size());
                 [ -  - ]
      82                 :      38502 :     return d_list[index];
      83                 :            :   }
      84                 :            : 
      85                 :    1365790 :   size_t size() const{
      86                 :    1365790 :     return d_list.size();
      87                 :            :   }
      88                 :            : 
      89                 :            : };/* class CDTrailQueue<> */
      90                 :            : 
      91                 :            : }  // namespace cvc5::context
      92                 :            : 
      93                 :            : #endif /* CVC5__CONTEXT__CDTRAIL_QUEUE_H */