GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/context/cdtrail_queue.h Lines: 23 23 100.0 %
Date: 2021-03-22 Branches: 7 40 17.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cdtrail_queue.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, 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 with an explicit trail of elements
13
 **
14
 ** Context-dependent First-In-First-Out queue class.
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 "cvc4_private.h"
21
22
#ifndef CVC4__CONTEXT__CDTRAIL_QUEUE_H
23
#define CVC4__CONTEXT__CDTRAIL_QUEUE_H
24
25
#include "context/cdlist.h"
26
#include "context/cdo.h"
27
28
namespace CVC4 {
29
namespace context {
30
31
class Context;
32
33
template <class T>
34
8992
class CDTrailQueue {
35
private:
36
37
  /** List of elements in the queue. */
38
  CDList<T> d_list;
39
40
  /** Points to the next element in the current context to dequeue. */
41
  CDO<size_t> d_iter;
42
43
44
public:
45
46
  /** Creates a new CDTrailQueue associated with the current context. */
47
8995
  CDTrailQueue(Context* context)
48
    : d_list(context),
49
8995
      d_iter(context, 0)
50
8995
  {}
51
52
  /** Returns true if the queue is empty in the current context. */
53
5070202
  bool empty() const{
54
5070202
    return d_iter >= d_list.size();
55
  }
56
57
  /**
58
   * Enqueues an element in the current context.
59
   * Returns its index in the queue.
60
   */
61
738699
  size_t enqueue(const T& data){
62
738699
    size_t res = d_list.size();
63
738699
    d_list.push_back(data);
64
738699
    return res;
65
  }
66
67
682244
  size_t frontIndex() const{
68
682244
    return d_iter;
69
  }
70
71
682244
  const T& front() const{
72
682244
    return d_list[frontIndex()];
73
  }
74
75
  /** Moves the iterator for the queue forward. */
76
682244
  void dequeue(){
77
682244
    Assert(!empty()) << "Attempting to queue from an empty queue.";
78
682244
    d_iter = d_iter + 1;
79
682244
  }
80
81
26532
  const T& operator[](size_t index) const{
82
26532
    Assert(index < d_list.size());
83
26532
    return d_list[index];
84
  }
85
86
842927
  size_t size() const{
87
842927
    return d_list.size();
88
  }
89
90
};/* class CDTrailQueue<> */
91
92
}/* CVC4::context namespace */
93
}/* CVC4 namespace */
94
95
#endif /* CVC4__CONTEXT__CDTRAIL_QUEUE_H */