Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/context/cdtrail_queue.h	Lines:	23	23	100.0 %
Date:	2021-09-16	Branches:	7	40	17.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Mathias Preiner, Gereon Kremer
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Context-dependent queue class with an explicit trail of elements
 *
 * The implementation is based on a combination of CDList and a CDO<size_t>
 * for tracking the next element to dequeue from the list.
 * The implementation is currently not full featured.
 */

#include "cvc5_private.h"

#ifndef CVC5__CONTEXT__CDTRAIL_QUEUE_H
#define CVC5__CONTEXT__CDTRAIL_QUEUE_H

#include "context/cdlist.h"
#include "context/cdo.h"

namespace cvc5 {
namespace context {

class Context;

template <class T>
class CDTrailQueue {
private:

  /** List of elements in the queue. */
  CDList<T> d_list;

  /** Points to the next element in the current context to dequeue. */
  CDO<size_t> d_iter;


public:

  /** Creates a new CDTrailQueue associated with the current context. */
  CDTrailQueue(Context* context)
    : d_list(context),
      d_iter(context, 0)
  {}

  /** Returns true if the queue is empty in the current context. */
  bool empty() const{
    return d_iter >= d_list.size();
  }

  /**
   * Enqueues an element in the current context.
   * Returns its index in the queue.
   */
  size_t enqueue(const T& data){
    size_t res = d_list.size();
    d_list.push_back(data);
    return res;
  }

  size_t frontIndex() const{
    return d_iter;
  }

  const T& front() const{
    return d_list[frontIndex()];
  }

  /** Moves the iterator for the queue forward. */
  void dequeue(){
    Assert(!empty()) << "Attempting to queue from an empty queue.";
    d_iter = d_iter + 1;
  }

  const T& operator[](size_t index) const{
    Assert(index < d_list.size());
    return d_list[index];
  }

  size_t size() const{
    return d_list.size();
  }

};/* class CDTrailQueue<> */

}  // namespace context
}  // namespace cvc5

#endif /* CVC5__CONTEXT__CDTRAIL_QUEUE_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, Mathias Preiner, Gereon Kremer
4		*
5		* This file is part of the cvc5 project.
6		*
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.
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 {
29		namespace context {
30
31		class Context;
32
33		template <class T>
34	9939	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	9942	CDTrailQueue(Context* context)
48		: d_list(context),
49	9942	d_iter(context, 0)
50	9942	{}
51
52		/** Returns true if the queue is empty in the current context. */
53	5177184	bool empty() const{
54	5177184	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	792882	size_t enqueue(const T& data){
62	792882	size_t res = d_list.size();
63	792882	d_list.push_back(data);
64	792882	return res;
65		}
66
67	748284	size_t frontIndex() const{
68	748284	return d_iter;
69		}
70
71	748284	const T& front() const{
72	748284	return d_list[frontIndex()];
73		}
74
75		/** Moves the iterator for the queue forward. */
76	748284	void dequeue(){
77	748284	Assert(!empty()) << "Attempting to queue from an empty queue.";
78	748284	d_iter = d_iter + 1;
79	748284	}
80
81	20695	const T& operator[](size_t index) const{
82	20695	Assert(index < d_list.size());
83	20695	return d_list[index];
84		}
85
86	912960	size_t size() const{
87	912960	return d_list.size();
88		}
89
90		};/* class CDTrailQueue<> */
91
92		} // namespace context
93		} // namespace cvc5
94
95		#endif /* CVC5__CONTEXT__CDTRAIL_QUEUE_H */