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