GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/context/cdqueue.h Lines: 48 48 100.0 %
Date: 2021-03-22 Branches: 113 524 21.6 %

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