Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/context/cdqueue.h	Lines:	48	48	100.0 %
Date:	2021-08-14	Branches:	113	524	21.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Francois Bobot, Mathias Preiner
 *
 * 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 First-In-First-Out queue class.
 *
 * This implementation may discard elements which are enqueued and dequeued
 * at the same context level.
 *
 * The implementation is based on a CDList with one additional size_t
 * for tracking the next element to dequeue from the list and additional
 * size_t for tracking the previous size of the list.
 */

#include "cvc5_private.h"

#ifndef CVC5__CONTEXT__CDQUEUE_H
#define CVC5__CONTEXT__CDQUEUE_H

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

namespace cvc5 {
namespace context {

template <class T, class CleanUp = DefaultCleanUp<T>, class Allocator = std::allocator<T> >
class CDQueue;

/** We don't define a template with Allocator for the first implementation */
template <class T, class CleanUp, class Allocator>
class CDQueue : public CDList<T, CleanUp, Allocator> {
private:
  typedef CDList<T, CleanUp, Allocator> ParentType;

protected:

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

  /** Points to the size at the last save. */
  size_t d_lastsave;

  /**
   * Private copy constructor used only by save().
   */
  CDQueue(const CDQueue<T, CleanUp, Allocator>& l):
    ParentType(l),
    d_iter(l.d_iter),
    d_lastsave(l.d_lastsave) {}

  /** Implementation of mandatory ContextObj method save:
   *  We assume that the base class do the job inside their copy constructor.
   */
  ContextObj* save(ContextMemoryManager* pCMM) override
  {
    ContextObj* data = new(pCMM) CDQueue<T, CleanUp, Allocator>(*this);
    // We save the d_size in d_lastsave and we should never destruct below this
    // indices before the corresponding restore.
    d_lastsave = ParentType::d_size;
    Debug("cdqueue") << "save " << this
                     << " at level " << this->getContext()->getLevel()
                     << " size at " << this->d_size
                     << " iter at " << this->d_iter
                     << " lastsave at " << this->d_lastsave
                     << " d_list is " << this->d_list
                     << " data:" << data << std::endl;
    return data;
  }

  /**
   * Implementation of mandatory ContextObj method restore: simply
   * restores the previous size, iter and lastsave indices. Note that
   * the list pointer and the allocated size are not changed.
   */
  void restore(ContextObj* data) override
  {
    CDQueue<T, CleanUp, Allocator>* qdata = static_cast<CDQueue<T, CleanUp, Allocator>*>(data);
    d_iter = qdata->d_iter;
    d_lastsave = qdata->d_lastsave;
    ParentType::restore(data);
  }



public:

  /** Creates a new CDQueue associated with the current context. */
  CDQueue(Context* context,
          bool callDestructor = true,
          const CleanUp& cleanup = CleanUp(),
          const Allocator& alloc = Allocator())
    : ParentType(context, callDestructor, cleanup, alloc),
      d_iter(0),
      d_lastsave(0)
  {}

  /** Returns true if the queue is empty in the current context. */
  bool empty() const{
    Assert(d_iter <= ParentType::d_size);
    return d_iter == ParentType::d_size;
  }

  /** Returns the number of elements that have not been dequeued in the context. */
  size_t size() const{
    return ParentType::d_size - d_iter;
  }

  /** Enqueues an element in the current context. */
  void push(const T& data){
    ParentType::push_back(data);
  }

  /**
   * Delete next element. The destructor of this object will be
   * called eventually but not necessarily during the call of this
   * function.
   */
  void pop(){
    Assert(!empty()) << "Attempting to pop from an empty queue.";
    ParentType::makeCurrent();
    d_iter = d_iter + 1;
    if (empty() && d_lastsave != ParentType::d_size) {
      // Some elements have been enqueued and dequeued in the same
      // context and now the queue is empty we can destruct them.
      ParentType::truncateList(d_lastsave);
      Assert(ParentType::d_size == d_lastsave);
      d_iter = d_lastsave;
    }
  }

  /** Returns a reference to the next element on the queue. */
  const T& front() const{
    Assert(!empty()) << "No front in an empty queue.";
    return ParentType::d_list[d_iter];
  }

  /**
   * Returns the most recent item added to the queue.
   */
  const T& back() const {
    Assert(!empty()) << "CDQueue::back() called on empty list";
    return ParentType::d_list[ParentType::d_size - 1];
  }

  typedef typename ParentType::const_iterator const_iterator;

  const_iterator begin() const {
    return ParentType::begin() + d_iter;
  }

  const_iterator end() const {
    return ParentType::end();
  }

};/* class CDQueue<> */

}  // namespace context
}  // namespace cvc5

#endif /* CVC5__CONTEXT__CDQUEUE_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, Francois Bobot, Mathias Preiner
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 First-In-First-Out queue class.
14		*
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 "cvc5_private.h"
24
25		#ifndef CVC5__CONTEXT__CDQUEUE_H
26		#define CVC5__CONTEXT__CDQUEUE_H
27
28		#include "context/context.h"
29		#include "context/cdlist.h"
30
31		namespace cvc5 {
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	110797	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	4032012	CDQueue(const CDQueue<T, CleanUp, Allocator>& l):
55		ParentType(l),
56	4032012	d_iter(l.d_iter),
57	8064024	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	4032012	ContextObj* save(ContextMemoryManager* pCMM) override
63		{
64	4032012	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	4032012	d_lastsave = ParentType::d_size;
68	12096036	Debug("cdqueue") << "save " << this
69	8064024	<< " at level " << this->getContext()->getLevel()
70	4032012	<< " size at " << this->d_size
71	4032012	<< " iter at " << this->d_iter
72	4032012	<< " lastsave at " << this->d_lastsave
73	4032012	<< " d_list is " << this->d_list
74	4032012	<< " data:" << data << std::endl;
75	4032012	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	4032012	void restore(ContextObj* data) override
84		{
85	4032012	CDQueue<T, CleanUp, Allocator>* qdata = static_cast<CDQueue<T, CleanUp, Allocator>*>(data);
86	4032012	d_iter = qdata->d_iter;
87	4032012	d_lastsave = qdata->d_lastsave;
88	4032012	ParentType::restore(data);
89	4032012	}
90
91
92
93		public:
94
95		/** Creates a new CDQueue associated with the current context. */
96	110797	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	110797	d_lastsave(0)
103	110797	{}
104
105		/** Returns true if the queue is empty in the current context. */
106	77578714	bool empty() const{
107	77578714	Assert(d_iter <= ParentType::d_size);
108	77578714	return d_iter == ParentType::d_size;
109		}
110
111		/** Returns the number of elements that have not been dequeued in the context. */
112	56149	size_t size() const{
113	56149	return ParentType::d_size - d_iter;
114		}
115
116		/** Enqueues an element in the current context. */
117	18529846	void push(const T& data){
118	18529846	ParentType::push_back(data);
119	18529846	}
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	15912616	void pop(){
127	15912616	Assert(!empty()) << "Attempting to pop from an empty queue.";
128	15912616	ParentType::makeCurrent();
129	15912616	d_iter = d_iter + 1;
130	15912616	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	3976534	ParentType::truncateList(d_lastsave);
134	3976534	Assert(ParentType::d_size == d_lastsave);
135	3976534	d_iter = d_lastsave;
136		}
137	15912616	}
138
139		/** Returns a reference to the next element on the queue. */
140	15912616	const T& front() const{
141	15912616	Assert(!empty()) << "No front in an empty queue.";
142	15912616	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	12708	const_iterator begin() const {
156	12708	return ParentType::begin() + d_iter;
157		}
158
159	12708	const_iterator end() const {
160	12708	return ParentType::end();
161		}
162
163		};/* class CDQueue<> */
164
165		} // namespace context
166		} // namespace cvc5
167
168		#endif /* CVC5__CONTEXT__CDQUEUE_H */