GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/context/cdinsert_hashmap.h Lines: 104 104 100.0 %
Date: 2021-03-23 Branches: 214 658 32.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cdinsert_hashmap.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Mathias Preiner, Morgan Deters
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 insert only hashmap built using trail of edits
13
 **
14
 ** Context-dependent hashmap that only allows for one insertion per element.
15
 ** This can be viewed as a highly restricted version of CDHashMap.
16
 ** It is significantly lighter in memory usage than CDHashMap.
17
 **
18
 ** See also:
19
 **  CDTrailHashMap : A lightweight CD hash map with poor iteration
20
 **    characteristics and some quirks in usage.
21
 **  CDHashMap : A fully featured CD hash map. (The closest to <ext/hash_map>)
22
 **
23
 ** Notes:
24
 ** - To iterate efficiently over the elements use the key_iterators.
25
 ** - operator[] is only supported as a const derefence (must succeed).
26
 ** - insert(k) must always work.
27
 ** - Use insert_safe if you want to check if the element has been inserted
28
 **   and only insert if it has not yet been.
29
 ** - Does not accept TNodes as keys.
30
 ** - Supports insertAtContextLevelZero() if the element is not in the map.
31
 **/
32
33
#include "cvc4_private.h"
34
35
#include <deque>
36
#include <functional>
37
#include <unordered_map>
38
#include <utility>
39
40
#include "base/check.h"
41
#include "base/output.h"
42
#include "context/cdinsert_hashmap_forward.h"
43
#include "context/context.h"
44
#include "expr/node.h"
45
46
#pragma once
47
48
namespace CVC4 {
49
namespace context {
50
51
52
template <class Key, class Data, class HashFcn = std::hash<Key> >
53
1567806
class InsertHashMap {
54
private:
55
  using KeyVec = std::deque<Key>;
56
  /** A list of the keys in the map maintained as a stack. */
57
  KeyVec d_keys;
58
59
  using HashMap = std::unordered_map<const Key, const Data, HashFcn>;
60
  /** The hash_map used for element lookup. */
61
  HashMap d_hashMap;
62
63
public:
64
  /**
65
   * An iterator over a list of keys.
66
   * Use this to efficiently iterate over the elements.
67
   * (See std::deque<>::iterator).
68
   */
69
  typedef typename KeyVec::const_iterator key_iterator;
70
71
  /**An iterator over the elements in the hash_map. */
72
  typedef typename HashMap::const_iterator const_iterator;
73
74
  // The type of the <Key, Data> values in the hashmap.
75
  using value_type = typename HashMap::value_type;
76
77
  /**
78
   * Returns an iterator to the begining of the HashMap.
79
   * Acts like a hash_map::const_iterator.
80
   */
81
973
  const_iterator begin() const{
82
973
    return d_hashMap.begin();
83
  }
84
  /**
85
   * Returns an iterator to the end of the HashMap.
86
   * Acts like a hash_map::const_iterator.
87
   */
88
387253508
  const_iterator end() const{
89
387253508
    return d_hashMap.end();
90
  }
91
92
  /**
93
   * Returns an iterator to the Key k of the map.
94
   * See hash_map::find()
95
   */
96
387252409
  const_iterator find(const Key& k) const{
97
387252409
    return d_hashMap.find(k);
98
  }
99
100
  /** Returns an iterator to the start of the set of keys. */
101
603
  key_iterator key_begin() const{
102
603
    return d_keys.begin();
103
  }
104
  /** Returns an iterator to the end of the set of keys. */
105
603
  key_iterator key_end() const{
106
603
    return d_keys.end();
107
  }
108
109
  /** Returns true if the map is empty. */
110
22055337
  bool empty() const { return d_keys.empty(); }
111
  /** Returns the number of elements in the map. */
112
74536678
  size_t size() const { return d_keys.size(); }
113
114
  /** Returns true if k is a mapped key. */
115
114683667
  bool contains(const Key& k) const {
116
114683667
    return find(k) != end();
117
  }
118
119
  /**
120
   * Returns a reference the data mapped by k.
121
   * This must succeed.
122
   */
123
119021053
  const Data& operator[](const Key& k) const {
124
119021053
    const_iterator ci = find(k);
125
119021053
    Assert(ci != end());
126
119021053
    return (*ci).second;
127
  }
128
129
  /**
130
   * Inserts an element into the map, and pushes its key to the front
131
   * of the stack. The key inserted must be not be currently mapped.
132
   */
133
  void push_front(const Key& k, const Data& d){
134
    Assert(!contains(k));
135
    d_hashMap.insert(std::make_pair(k, d));
136
    d_keys.push_front(k);
137
  }
138
139
  /**
140
   * Inserts an element into the map, and pushes its key onto the
141
   * back on the stack.  The key inserted must be not be currently mapped.
142
   */
143
26401916
  void push_back(const Key& k, const Data& d){
144
26401916
    Assert(!contains(k));
145
26401916
    d_hashMap.insert(std::make_pair(k, d));
146
26401916
    d_keys.push_back(k);
147
26401916
  }
148
149
  /**
150
   * Pops the key at the front of the list off and removes its key from the map.
151
   */
152
  void pop_front(){
153
    Assert(!empty());
154
    const Key& front = d_keys.front();
155
    d_hashMap.erase(front);
156
157
    Debug("TrailHashMap") <<"TrailHashMap pop_front " << size() << std::endl;
158
    d_keys.pop_front();
159
  }
160
161
  /**
162
   * Pops the key at the back of the stack off and removes its key from the map.
163
   */
164
22055337
  void pop_back(){
165
22055337
    Assert(!empty());
166
22055337
    const Key& back = d_keys.back();
167
22055337
    d_hashMap.erase(back);
168
169
22055337
    Debug("TrailHashMap") <<"TrailHashMap pop_back " << size() << std::endl;
170
22055337
    d_keys.pop_back();
171
22055337
  }
172
173
  /**
174
   * Pops the back of the stack until the size is below s.
175
   */
176
23675339
  void pop_to_size(size_t s){
177
45730676
    while(size() > s){
178
22055337
      pop_back();
179
    }
180
1620002
  }
181
};/* class TrailHashMap<> */
182
183
template <class Key, class Data, class HashFcn>
184
class CDInsertHashMap : public ContextObj {
185
private:
186
  typedef InsertHashMap<Key, Data, HashFcn> IHM;
187
188
  /** An InsertHashMap that backs all of the data. */
189
  IHM* d_insertMap;
190
191
  /** For restores, we need to keep track of the previous size. */
192
  size_t d_size;
193
194
  /**
195
   * To support insertAtContextLevelZero() and restores,
196
   * we have called d_insertMap->d_pushFront().
197
   */
198
  size_t d_pushFronts;
199
200
  /**
201
   * Private copy constructor used only by save().  d_insertMap is
202
   * not copied: only the base class information and
203
   * d_size and d_pushFronts are needed in restore.
204
   */
205
1620004
  CDInsertHashMap(const CDInsertHashMap& l) :
206
    ContextObj(l),
207
    d_insertMap(NULL),
208
1620004
    d_size(l.d_size),
209
3240008
    d_pushFronts(l.d_pushFronts)
210
  {
211
4860012
    Debug("CDInsertHashMap") << "copy ctor: " << this
212
3240008
                    << " from " << &l
213
1620004
                    << " size " << d_size << std::endl;
214
1620004
  }
215
  CDInsertHashMap& operator=(const CDInsertHashMap&) = delete;
216
217
  /**
218
   * Implementation of mandatory ContextObj method save: simply copies
219
   * the current size information to a copy using the copy constructor (the
220
   * pointer and the allocated size are *not* copied as they are not
221
   * restored on a pop).  The saved information is allocated using the
222
   * ContextMemoryManager.
223
   */
224
1620004
  ContextObj* save(ContextMemoryManager* pCMM) override
225
  {
226
1620004
    ContextObj* data = new(pCMM) CDInsertHashMap<Key, Data, HashFcn>(*this);
227
4860012
    Debug("CDInsertHashMap") << "save " << this
228
3240008
                            << " at level " << this->getContext()->getLevel()
229
1620004
                            << " size at " << this->d_size
230
1620004
                            << " d_list is " << this->d_insertMap
231
1620004
                            << " data:" << data << std::endl;
232
1620004
    return data;
233
  }
234
protected:
235
  /**
236
   * Implementation of mandatory ContextObj method restore:
237
   * restore to the previous size taking into account the number
238
   * of new pushFront calls have happened since saving.
239
   * The d_insertMap is untouched and d_pushFronts is also kept.
240
   */
241
1620002
 void restore(ContextObj* data) override
242
 {
243
4860006
   Debug("CDInsertHashMap")
244
3240004
       << "restore " << this << " level " << this->getContext()->getLevel()
245
1620002
       << " data == " << data << " d_insertMap == " << this->d_insertMap
246
       << std::endl;
247
1620002
   size_t oldSize = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_size;
248
1620002
   size_t oldPushFronts =
249
1620002
       ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_pushFronts;
250
1620002
   Assert(oldPushFronts <= d_pushFronts);
251
252
   // The size to restore to.
253
1620002
   size_t restoreSize = oldSize + (d_pushFronts - oldPushFronts);
254
1620002
   d_insertMap->pop_to_size(restoreSize);
255
1620002
   d_size = restoreSize;
256
1620002
   Assert(d_insertMap->size() == d_size);
257
4860006
   Debug("CDInsertHashMap")
258
3240004
       << "restore " << this << " level " << this->getContext()->getLevel()
259
1620002
       << " size back to " << this->d_size << std::endl;
260
1620002
  }
261
public:
262
263
 /**
264
   * Main constructor: d_insertMap starts as an empty map, with the size is 0
265
   */
266
784084
  CDInsertHashMap(Context* context) :
267
    ContextObj(context),
268
784084
    d_insertMap(new IHM()),
269
    d_size(0),
270
1568168
    d_pushFronts(0){
271
784084
    Assert(d_insertMap->size() == d_size);
272
784084
  }
273
274
  /**
275
   * Destructor: delete the d_insertMap
276
   */
277
783722
  ~CDInsertHashMap() {
278
783722
    this->destroy();
279
783722
    delete d_insertMap;
280
1567444
  }
281
282
  /** An iterator over the elements in the hash_map. */
283
  typedef typename IHM::const_iterator const_iterator;
284
285
  /**
286
   * An iterator over a list of keys.
287
   * Use this to efficiently iterate over the elements.
288
   * (See std::deque<>::iterator).
289
   */
290
  typedef typename IHM::key_iterator key_iterator;
291
292
  // The type of the <key, data> values in the hashmap.
293
  using value_type = typename IHM::value_type;
294
295
  /** Returns true if the map is empty in the current context. */
296
47
  bool empty() const{
297
47
    return d_size == 0;
298
  }
299
300
  /** Returns true the size of the map in the current context. */
301
6790
  size_t size() const {
302
6790
    return d_size;
303
  }
304
305
  /**
306
   * Inserts an element into the map.
307
   * The key inserted must be not be currently mapped.
308
   * This is implemented using d_insertMap.push_back().
309
   */
310
26401916
  void insert(const Key& k, const Data& d){
311
26401916
    makeCurrent();
312
26401916
    ++d_size;
313
26401916
    d_insertMap->push_back(k, d);
314
26401916
    Assert(d_insertMap->size() == d_size);
315
26401916
  }
316
317
  /**
318
   * Checks if the key k is mapped already.
319
   * If it is, this returns false.
320
   * Otherwise it is inserted and this returns true.
321
   */
322
19774458
  bool insert_safe(const Key& k, const Data& d){
323
19774458
    if(contains(k)){
324
750638
      return false;
325
    }else{
326
19023820
      insert(k,d);
327
19023820
      return true;
328
    }
329
  }
330
331
  /**
332
   * Version of insert() for CDMap<> that inserts data value d at
333
   * context level zero.
334
   *
335
   * It is an error to insertAtContextLevelZero()
336
   * a key that already is in the map.
337
   */
338
  void insertAtContextLevelZero(const Key& k, const Data& d){
339
    makeCurrent();
340
    ++d_size;
341
    ++d_pushFronts;
342
    d_insertMap->push_front(k, d);
343
  }
344
345
  /** Returns true if k is a mapped key in the context. */
346
88281751
  bool contains(const Key& k) const {
347
88281751
    return d_insertMap->contains(k);
348
  }
349
350
  /**
351
   * Returns a reference the data mapped by k.
352
   * k must be in the map in this context.
353
   */
354
119021053
  const Data& operator[](const Key& k) const {
355
119021053
    return (*d_insertMap)[k];
356
  }
357
358
   /**
359
    * Returns a const_iterator to the value_type if k is a mapped key in
360
    * the context.
361
    */
362
153547689
  const_iterator find(const Key& k) const {
363
153547689
    return d_insertMap->find(k);
364
  }
365
366
  /**
367
   * Returns an iterator to the begining of the map.
368
   * Acts like a hash_map::const_iterator.
369
   */
370
973
  const_iterator begin() const{
371
973
    return d_insertMap->begin();
372
  }
373
374
  /**
375
   * Returns an iterator to the end of the map.
376
   * Acts like a hash_map::const_iterator.
377
   */
378
153548788
  const_iterator end() const{
379
153548788
    return d_insertMap->end();
380
  }
381
382
  /** Returns an iterator to the start of the set of keys. */
383
603
  key_iterator key_begin() const{
384
603
    return d_insertMap->key_begin();
385
  }
386
  /** Returns an iterator to the end of the set of keys. */
387
603
  key_iterator key_end() const{
388
603
    return d_insertMap->key_end();
389
  }
390
};/* class CDInsertHashMap<> */
391
392
template <class Data, class HashFcn>
393
class CDInsertHashMap<TNode, Data, HashFcn> : public ContextObj {
394
  /* CDInsertHashMap is challenging to get working with TNode.
395
   * Consider using CDHashMap<TNode,...> instead.
396
   *
397
   * Explanation:
398
   * CDInsertHashMap uses keys for deallocation.
399
   * If the key is a TNode and the backing (the hard node reference)
400
   * for the key in another data structure removes the key at the same context
401
   * the ref count could drop to 0.  The key would then not be eligible to be
402
   * hashed. Getting the order right with a guarantee is too hard.
403
   */
404
405
  static_assert(sizeof(Data) == 0,
406
                "Cannot create a CDInsertHashMap with TNode keys");
407
};
408
409
}/* CVC4::context namespace */
410
}/* CVC4 namespace */