Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/dense_map.h	Lines:	91	111	82.0 %
Date:	2021-09-16	Branches:	75	577	13.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Dejan Jovanovic, 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.
 * ****************************************************************************
 *
 * This is an abstraction of a Map from unsigned integers to elements
 * of type T.
 *
 * This is an abstraction of a Map from an unsigned integer to elements of
 * type T.
 * This class is designed to provide constant time insertion, deletion,
 * element_of, and fast iteration. This is done by storing backing vectors of
 * size greater than the maximum key.
 * This datastructure is appropriate for heavy use datastructures where the
 * Keys are a dense set of integers.
 *
 * T must support T(), and operator=().
 *
 * The derived utility classes DenseSet and DenseMultiset are also defined.
 */

#include "cvc5_private.h"

#pragma once

#include <limits>
#include <vector>

#include "base/check.h"
#include "util/index.h"

namespace cvc5 {

template <class T>
class DenseMap {
public:
  typedef Index Key;
  typedef std::vector<Key> KeyList;
  typedef KeyList::const_iterator const_iterator;

private:
  //List of the keys in the dense map.
  KeyList d_list;

  typedef Index Position;
  typedef std::vector<Position> PositionMap;
  static const Position POSITION_SENTINEL =
      std::numeric_limits<Position>::max();

  //Each Key in the set is mapped to its position in d_list.
  //Each Key not in the set is mapped to KEY_SENTINEL
  PositionMap d_posVector;

  typedef std::vector<T> ImageMap;
  //d_image : Key |-> T
  ImageMap d_image;

public:

  DenseMap() :  d_list(), d_posVector(), d_image() {}

  /** Returns the number of elements in the set. */
  size_t size() const {
    return d_list.size();
  }

  /** Returns true if the map is empty(). */
  bool empty() const {
    return d_list.empty();
  }

  /**
   * Similar to a std::vector::clear().
   *
   * Invalidates iterators.
   */
  void clear() {
    d_list.clear();
    d_posVector.clear();
    d_image.clear();
    Assert(empty());
  }

  /**
   * Similar to a clear(), but the datastructures are not reset in size.
   * Invalidates iterators.
   */
  void purge() {
    while(!empty()){
      pop_back();
    }
    Assert(empty());
  }

  /** Returns true if k is a key of this datastructure. */
  bool isKey(Key x) const{
    if( x >= allocated()){
      return false;
    }else{
      Assert(x < allocated());
      return d_posVector[x] != +POSITION_SENTINEL;
    }
  }

  /**
   * Maps the key to value in the map.
   * Invalidates iterators.
   */
  void set(Key key, const T& value){
    if( key >= allocated()){
      increaseSize(key);
    }

    if(!isKey(key)){
      d_posVector[key] = size();
      d_list.push_back(key);
    }
    d_image[key] = value;
  }

  /** Returns a mutable reference to the element mapped by key. */
  T& get(Key key){
    Assert(isKey(key));
    return d_image[key];
  }

  /** Returns a const reference to the element mapped by key.*/
  const T& operator[](Key key) const {
    Assert(isKey(key));
    return d_image[key];
  }

  /** Returns an iterator over the keys of the map. */
  const_iterator begin() const{ return d_list.begin(); }
  const_iterator end() const{ return d_list.end(); }

  const KeyList& getKeys() const{
    return d_list;
  }

  /**
   * Removes the mapping associated with key.
   * This changes the order of the keys.
   *
   * Invalidates iterators.
   */
  void remove(Key x){
    Assert(isKey(x));
    swapToBack(x);
    Assert(d_list.back() == x);
    pop_back();
  }

  /** Returns the key at the back of a non-empty list.*/
  Key back() const {
    return d_list.back();
  }

  /** Removes the element associated with the last Key from the map. */
  void pop_back() {
    Assert(!empty());
    Key atBack = back();
    d_posVector[atBack] = +POSITION_SENTINEL;
    d_image[atBack] = T();
    d_list.pop_back();
  }


  /** Adds at least a constant fraction of the elements in the current map to another map. */
  void splitInto(DenseMap<T>& target){
    uint32_t targetSize = size()/2;
    while(size() > targetSize){
      Key key = back();
      target.set(key, get(key));
      pop_back();
    }
  }

  /** Adds the current target map to the current map.*/
  void addAll(const DenseMap<T>& target){
    for(const_iterator i = target.begin(), e = target.end(); i != e; ++i){
      Key k = *i;
      set(k, target[k]);
    }
  }



 private:

  size_t allocated() const {
    Assert(d_posVector.size() == d_image.size());
    return d_posVector.size();
  }

  void increaseSize(Key max){
    Assert(max >= allocated());
    d_posVector.resize(max+1, +POSITION_SENTINEL);
    d_image.resize(max+1);
  }

  /** Swaps a member x to the back of d_list. */
  void swapToBack(Key x){
    Assert(isKey(x));

    Position currentPos = d_posVector[x];
    Key atBack = back();

    d_list[currentPos] = atBack;
    d_posVector[atBack] = currentPos;

    Position last = size() - 1;

    d_list[last] = x;
    d_posVector[x] = last;
  }
}; /* class DenseMap<T> */

/**
 * This provides an abstraction for a set of unsigned integers with similar capabilities
 * as DenseMap. This is implemented as a light wrapper for DenseMap<bool> with an
 * interface designed for use as a set instead of a map.
 */
class DenseSet {
private:
  typedef DenseMap<bool> BackingMap;
  BackingMap d_map;
public:
  typedef BackingMap::const_iterator const_iterator;
  typedef BackingMap::Key Element;

  size_t size() const { return d_map.size(); }
  bool empty() const { return d_map.empty(); }

  /** See DenseMap's documentation. */
  void purge() { d_map.purge(); }
  void clear() { d_map.clear(); }

  bool isMember(Element x) const{ return d_map.isKey(x); }

  /**
   * Adds an element that is not a member of the set to the set.
   */
  void add(Element x){
    Assert(!isMember(x));
    d_map.set(x, true);
  }

  /** Adds an element to the set even if it is already an element of the set. */
  void softAdd(Element x){ d_map.set(x, true); }

  /** Removes an element from the set. */
  void remove(Element x){ d_map.remove(x); }

  const_iterator begin() const{ return d_map.begin(); }
  const_iterator end() const{ return d_map.end(); }

  Element back() { return d_map.back(); }
  void pop_back() { d_map.pop_back(); }
}; /* class DenseSet */

/**
 * This provides an abstraction for a multiset of unsigned integers with similar
 * capabilities as DenseMap.
 * This is implemented as a light wrapper for DenseMap<bool> with an
 * interface designed for use as a set instead of a map.
 */
class DenseMultiset {
public:
  typedef uint32_t CountType;

private:
  typedef DenseMap<CountType> BackingMap;
  BackingMap d_map;

public:
  typedef BackingMap::const_iterator const_iterator;
  typedef BackingMap::Key Element;

  DenseMultiset() :  d_map() {}

  size_t size() const { return d_map.size(); }
  bool empty() const { return d_map.empty(); }

  void purge() { d_map.purge(); }
  void clear() { d_map.clear(); }

  bool isMember(Element x) const{ return d_map.isKey(x); }

  void add(Element x, CountType c = 1u){
    Assert(c > 0);
    if(d_map.isKey(x)){
      d_map.set(x, d_map.get(x)+c);
    }else{
      d_map.set(x,c);
    }
  }

  void setCount(Element x, CountType c){
    d_map.set(x, c);
  }

  void removeAll(Element x){ return d_map.remove(x); }

  void removeOne(Element x){
    CountType c = count(x);
    switch(c){
    case 0: break; // do nothing
    case 1: removeAll(x); break; // remove
    default: d_map.set(x, c-1); break; // decrease
    }
  }

  void removeOneOfEverything(){
    BackingMap::KeyList keys(d_map.begin(), d_map.end());
    for(BackingMap::const_iterator i=keys.begin(), i_end = keys.end(); i != i_end; ++i){
      removeOne(*i);
    }
  }

  CountType count(Element x) const {
    if(d_map.isKey(x)){
      return d_map[x];
    }else {
      return 0;
    }
  }

  const_iterator begin() const{ return d_map.begin(); }
  const_iterator end() const{ return d_map.end(); }
  Element back() { return d_map.back(); }
  void pop_back() { d_map.pop_back(); }
}; /* class DenseMultiset */

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, Dejan Jovanovic, 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		* This is an abstraction of a Map from unsigned integers to elements
14		* of type T.
15		*
16		* This is an abstraction of a Map from an unsigned integer to elements of
17		* type T.
18		* This class is designed to provide constant time insertion, deletion,
19		* element_of, and fast iteration. This is done by storing backing vectors of
20		* size greater than the maximum key.
21		* This datastructure is appropriate for heavy use datastructures where the
22		* Keys are a dense set of integers.
23		*
24		* T must support T(), and operator=().
25		*
26		* The derived utility classes DenseSet and DenseMultiset are also defined.
27		*/
28
29		#include "cvc5_private.h"
30
31		#pragma once
32
33		#include <limits>
34		#include <vector>
35
36		#include "base/check.h"
37		#include "util/index.h"
38
39		namespace cvc5 {
40
41		template <class T>
42	288231	class DenseMap {
43		public:
44		typedef Index Key;
45		typedef std::vector<Key> KeyList;
46		typedef KeyList::const_iterator const_iterator;
47
48		private:
49		//List of the keys in the dense map.
50		KeyList d_list;
51
52		typedef Index Position;
53		typedef std::vector<Position> PositionMap;
54		static const Position POSITION_SENTINEL =
55		std::numeric_limits<Position>::max();
56
57		//Each Key in the set is mapped to its position in d_list.
58		//Each Key not in the set is mapped to KEY_SENTINEL
59		PositionMap d_posVector;
60
61		typedef std::vector<T> ImageMap;
62		//d_image : Key \|-> T
63		ImageMap d_image;
64
65		public:
66
67	288318	DenseMap() : d_list(), d_posVector(), d_image() {}
68
69		/** Returns the number of elements in the set. */
70	30621186	size_t size() const {
71	30621186	return d_list.size();
72		}
73
74		/** Returns true if the map is empty(). */
75	95503421	bool empty() const {
76	95503421	return d_list.empty();
77		}
78
79		/**
80		* Similar to a std::vector::clear().
81		*
82		* Invalidates iterators.
83		*/
84		void clear() {
85		d_list.clear();
86		d_posVector.clear();
87		d_image.clear();
88		Assert(empty());
89		}
90
91		/**
92		* Similar to a clear(), but the datastructures are not reset in size.
93		* Invalidates iterators.
94		*/
95	12920286	void purge() {
96	21507612	while(!empty()){
97	8587326	pop_back();
98		}
99	4332960	Assert(empty());
100	4332960	}
101
102		/** Returns true if k is a key of this datastructure. */
103	3058360607	bool isKey(Key x) const{
104	3058360607	if( x >= allocated()){
105	1939503	return false;
106		}else{
107	3056421104	Assert(x < allocated());
108	3056421104	return d_posVector[x] != +POSITION_SENTINEL;
109		}
110		}
111
112		/**
113		* Maps the key to value in the map.
114		* Invalidates iterators.
115		*/
116	33408210	void set(Key key, const T& value){
117	33408210	if( key >= allocated()){
118	861893	increaseSize(key);
119		}
120
121	33408210	if(!isKey(key)){
122	28602164	d_posVector[key] = size();
123	28602164	d_list.push_back(key);
124		}
125	33408210	d_image[key] = value;
126	33408210	}
127
128		/** Returns a mutable reference to the element mapped by key. */
129	179630222	T& get(Key key){
130	179630222	Assert(isKey(key));
131	179630222	return d_image[key];
132		}
133
134		/** Returns a const reference to the element mapped by key.*/
135	2390252380	const T& operator[](Key key) const {
136	2390252380	Assert(isKey(key));
137	2390252380	return d_image[key];
138		}
139
140		/** Returns an iterator over the keys of the map. */
141	8142997	const_iterator begin() const{ return d_list.begin(); }
142	30349066	const_iterator end() const{ return d_list.end(); }
143
144		const KeyList& getKeys() const{
145		return d_list;
146		}
147
148		/**
149		* Removes the mapping associated with key.
150		* This changes the order of the keys.
151		*
152		* Invalidates iterators.
153		*/
154	535242	void remove(Key x){
155	535242	Assert(isKey(x));
156	535242	swapToBack(x);
157	535242	Assert(d_list.back() == x);
158	535242	pop_back();
159	535242	}
160
161		/** Returns the key at the back of a non-empty list.*/
162	47286668	Key back() const {
163	47286668	return d_list.back();
164		}
165
166		/** Removes the element associated with the last Key from the map. */
167	27936997	void pop_back() {
168	27936997	Assert(!empty());
169	27936997	Key atBack = back();
170	27936997	d_posVector[atBack] = +POSITION_SENTINEL;
171	27936997	d_image[atBack] = T();
172	27936997	d_list.pop_back();
173	27936997	}
174
175
176		/** Adds at least a constant fraction of the elements in the current map to another map. */
177		void splitInto(DenseMap<T>& target){
178		uint32_t targetSize = size()/2;
179		while(size() > targetSize){
180		Key key = back();
181		target.set(key, get(key));
182		pop_back();
183		}
184		}
185
186		/** Adds the current target map to the current map.*/
187		void addAll(const DenseMap<T>& target){
188		for(const_iterator i = target.begin(), e = target.end(); i != e; ++i){
189		Key k = *i;
190		set(k, target[k]);
191		}
192		}
193
194
195
196		private:
197
198	6149051814	size_t allocated() const {
199	6149051814	Assert(d_posVector.size() == d_image.size());
200	6149051814	return d_posVector.size();
201		}
202
203	861893	void increaseSize(Key max){
204	861893	Assert(max >= allocated());
205	861893	d_posVector.resize(max+1, +POSITION_SENTINEL);
206	861893	d_image.resize(max+1);
207	861893	}
208
209		/** Swaps a member x to the back of d_list. */
210	535242	void swapToBack(Key x){
211	535242	Assert(isKey(x));
212
213	535242	Position currentPos = d_posVector[x];
214	535242	Key atBack = back();
215
216	535242	d_list[currentPos] = atBack;
217	535242	d_posVector[atBack] = currentPos;
218
219	535242	Position last = size() - 1;
220
221	535242	d_list[last] = x;
222	535242	d_posVector[x] = last;
223	535242	}
224		}; /* class DenseMap<T> */
225
226		/**
227		* This provides an abstraction for a set of unsigned integers with similar capabilities
228		* as DenseMap. This is implemented as a light wrapper for DenseMap<bool> with an
229		* interface designed for use as a set instead of a map.
230		*/
231	218691	class DenseSet {
232		private:
233		typedef DenseMap<bool> BackingMap;
234		BackingMap d_map;
235		public:
236		typedef BackingMap::const_iterator const_iterator;
237		typedef BackingMap::Key Element;
238
239		size_t size() const { return d_map.size(); }
240	22926937	bool empty() const { return d_map.empty(); }
241
242		/** See DenseMap's documentation. */
243	3117383	void purge() { d_map.purge(); }
244		void clear() { d_map.clear(); }
245
246	7399772	bool isMember(Element x) const{ return d_map.isKey(x); }
247
248		/**
249		* Adds an element that is not a member of the set to the set.
250		*/
251	133555	void add(Element x){
252	133555	Assert(!isMember(x));
253	133555	d_map.set(x, true);
254	133555	}
255
256		/** Adds an element to the set even if it is already an element of the set. */
257	17445874	void softAdd(Element x){ d_map.set(x, true); }
258
259		/** Removes an element from the set. */
260		void remove(Element x){ d_map.remove(x); }
261
262	1168920	const_iterator begin() const{ return d_map.begin(); }
263	1168920	const_iterator end() const{ return d_map.end(); }
264
265	10009876	Element back() { return d_map.back(); }
266	10009876	void pop_back() { d_map.pop_back(); }
267		}; /* class DenseSet */
268
269		/**
270		* This provides an abstraction for a multiset of unsigned integers with similar
271		* capabilities as DenseMap.
272		* This is implemented as a light wrapper for DenseMap<bool> with an
273		* interface designed for use as a set instead of a map.
274		*/
275	19878	class DenseMultiset {
276		public:
277		typedef uint32_t CountType;
278
279		private:
280		typedef DenseMap<CountType> BackingMap;
281		BackingMap d_map;
282
283		public:
284		typedef BackingMap::const_iterator const_iterator;
285		typedef BackingMap::Key Element;
286
287	19884	DenseMultiset() : d_map() {}
288
289		size_t size() const { return d_map.size(); }
290		bool empty() const { return d_map.empty(); }
291
292	96601	void purge() { d_map.purge(); }
293		void clear() { d_map.clear(); }
294
295		bool isMember(Element x) const{ return d_map.isKey(x); }
296
297	211071	void add(Element x, CountType c = 1u){
298	211071	Assert(c > 0);
299	211071	if(d_map.isKey(x)){
300	1672	d_map.set(x, d_map.get(x)+c);
301		}else{
302	209399	d_map.set(x,c);
303		}
304	211071	}
305
306		void setCount(Element x, CountType c){
307		d_map.set(x, c);
308		}
309
310		void removeAll(Element x){ return d_map.remove(x); }
311
312		void removeOne(Element x){
313		CountType c = count(x);
314		switch(c){
315		case 0: break; // do nothing
316		case 1: removeAll(x); break; // remove
317		default: d_map.set(x, c-1); break; // decrease
318		}
319		}
320
321		void removeOneOfEverything(){
322		BackingMap::KeyList keys(d_map.begin(), d_map.end());
323		for(BackingMap::const_iterator i=keys.begin(), i_end = keys.end(); i != i_end; ++i){
324		removeOne(*i);
325		}
326		}
327
328	422374	CountType count(Element x) const {
329	422374	if(d_map.isKey(x)){
330	212975	return d_map[x];
331		}else {
332	209399	return 0;
333		}
334		}
335
336		const_iterator begin() const{ return d_map.begin(); }
337		const_iterator end() const{ return d_map.end(); }
338		Element back() { return d_map.back(); }
339		void pop_back() { d_map.pop_back(); }
340		}; /* class DenseMultiset */
341
342		} // namespace cvc5