GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/dense_map.h Lines: 91 111 82.0 %
Date: 2021-03-23 Branches: 75 577 13.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file dense_map.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Dejan Jovanovic, 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 This is an abstraction of a Map from unsigned integers to elements
13
 ** of type T.
14
 **
15
 ** This is an abstraction of a Map from an unsigned integer to elements of
16
 ** type T.
17
 ** This class is designed to provide constant time insertion, deletion,
18
 ** element_of, and fast iteration. This is done by storing backing vectors of
19
 ** size greater than the maximum key.
20
 ** This datastructure is appropriate for heavy use datastructures where the
21
 ** Keys are a dense set of integers.
22
 **
23
 ** T must support T(), and operator=().
24
 **
25
 ** The derived utility classes DenseSet and DenseMultiset are also defined.
26
 **/
27
28
#include "cvc4_private.h"
29
30
#pragma once
31
32
#include <limits>
33
#include <vector>
34
35
#include "base/check.h"
36
#include "util/index.h"
37
38
39
namespace CVC4 {
40
41
template <class T>
42
260826
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
260913
  DenseMap() :  d_list(), d_posVector(), d_image() {}
68
69
  /** Returns the number of elements in the set. */
70
27676725
  size_t size() const {
71
27676725
    return d_list.size();
72
  }
73
74
  /** Returns true if the map is empty(). */
75
87779697
  bool empty() const {
76
87779697
    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
12436809
  void purge() {
96
20548456
    while(!empty()){
97
8111647
      pop_back();
98
    }
99
4325162
    Assert(empty());
100
4325162
  }
101
102
  /** Returns true if k is a key of this datastructure. */
103
2342977172
  bool isKey(Key x) const{
104
2342977172
    if( x >= allocated()){
105
1639425
      return false;
106
    }else{
107
2341337747
      Assert(x < allocated());
108
2341337747
      return d_posVector[x] != +POSITION_SENTINEL;
109
    }
110
  }
111
112
  /**
113
   * Maps the key to value in the map.
114
   * Invalidates iterators.
115
   */
116
30218639
  void set(Key key, const T& value){
117
30218639
    if( key >= allocated()){
118
755289
      increaseSize(key);
119
    }
120
121
30218639
    if(!isKey(key)){
122
25803188
      d_posVector[key] = size();
123
25803188
      d_list.push_back(key);
124
    }
125
30218639
    d_image[key] = value;
126
30218639
  }
127
128
  /** Returns a mutable reference to the element mapped by key. */
129
166971929
  T& get(Key key){
130
166971929
    Assert(isKey(key));
131
166971929
    return d_image[key];
132
  }
133
134
  /** Returns a const reference to the element mapped by key.*/
135
1930498976
  const T& operator[](Key key) const {
136
1930498976
    Assert(isKey(key));
137
1930498976
    return d_image[key];
138
  }
139
140
  /** Returns an iterator over the keys of the map. */
141
7312903
  const_iterator begin() const{ return d_list.begin(); }
142
21737456
  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
494108
  void remove(Key x){
155
494108
    Assert(isKey(x));
156
494108
    swapToBack(x);
157
494108
    Assert(d_list.back() == x);
158
494108
    pop_back();
159
494108
  }
160
161
  /** Returns the key at the back of a non-empty list.*/
162
42314693
  Key back() const {
163
42314693
    return d_list.back();
164
  }
165
166
  /** Removes the element associated with the last Key from the map. */
167
25213170
  void pop_back() {
168
25213170
    Assert(!empty());
169
25213170
    Key atBack = back();
170
25213170
    d_posVector[atBack] = +POSITION_SENTINEL;
171
25213170
    d_image[atBack] = T();
172
25213170
    d_list.pop_back();
173
25213170
  }
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
4715288847
  size_t allocated() const {
199
4715288847
    Assert(d_posVector.size() == d_image.size());
200
4715288847
    return d_posVector.size();
201
  }
202
203
755289
  void increaseSize(Key max){
204
755289
    Assert(max >= allocated());
205
755289
    d_posVector.resize(max+1, +POSITION_SENTINEL);
206
755289
    d_image.resize(max+1);
207
755289
  }
208
209
  /** Swaps a member x to the back of d_list. */
210
494108
  void swapToBack(Key x){
211
494108
    Assert(isKey(x));
212
213
494108
    Position currentPos = d_posVector[x];
214
494108
    Key atBack = back();
215
216
494108
    d_list[currentPos] = atBack;
217
494108
    d_posVector[atBack] = currentPos;
218
219
494108
    Position last = size() - 1;
220
221
494108
    d_list[last] = x;
222
494108
    d_posVector[x] = last;
223
494108
  }
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
197901
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
21023678
  bool empty() const { return d_map.empty(); }
241
242
  /** See DenseMap's documentation. */
243
3206422
  void purge() { d_map.purge(); }
244
  void clear() { d_map.clear(); }
245
246
7018536
  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
121849
  void add(Element x){
252
121849
    Assert(!isMember(x));
253
121849
    d_map.set(x, true);
254
121849
  }
255
256
  /** Adds an element to the set even if it is already an element of the set. */
257
15473540
  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
1091496
  const_iterator begin() const{ return d_map.begin(); }
263
1091496
  const_iterator end() const{ return d_map.end(); }
264
265
8623089
  Element back() { return d_map.back(); }
266
8623089
  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
17988
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
17994
  DenseMultiset() :  d_map() {}
288
289
  size_t size() const { return d_map.size(); }
290
  bool empty() const { return d_map.empty(); }
291
292
87337
  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
194809
  void add(Element x, CountType c = 1u){
298
194809
    Assert(c > 0);
299
194809
    if(d_map.isKey(x)){
300
1599
      d_map.set(x, d_map.get(x)+c);
301
    }else{
302
193210
      d_map.set(x,c);
303
    }
304
194809
  }
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
389854
  CountType count(Element x) const {
329
389854
    if(d_map.isKey(x)){
330
196644
      return d_map[x];
331
    }else {
332
193210
      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
}/* CVC4 namespace */