Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/context/cdinsert_hashmap.h	Lines:	102	104	98.1 %
Date:	2021-08-14	Branches:	214	658	32.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Mathias Preiner, Morgan Deters
 *
 * 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 insert only hashmap built using trail of edits
 *
 * Context-dependent hashmap that only allows for one insertion per element.
 * This can be viewed as a highly restricted version of CDHashMap.
 * It is significantly lighter in memory usage than CDHashMap.
 *
 * See also:
 *  CDTrailHashMap : A lightweight CD hash map with poor iteration
 *    characteristics and some quirks in usage.
 *  CDHashMap : A fully featured CD hash map. (The closest to <ext/hash_map>)
 *
 * Notes:
 * - To iterate efficiently over the elements use the key_iterators.
 * - operator[] is only supported as a const derefence (must succeed).
 * - insert(k) must always work.
 * - Use insert_safe if you want to check if the element has been inserted
 *   and only insert if it has not yet been.
 * - Does not accept TNodes as keys.
 * - Supports insertAtContextLevelZero() if the element is not in the map.
 */

#include <deque>
#include <functional>
#include <unordered_map>
#include <utility>

#include "base/check.h"
#include "base/output.h"
#include "context/cdinsert_hashmap_forward.h"
#include "context/context.h"
#include "cvc5_private.h"
#include "expr/node.h"

#pragma once

namespace cvc5 {
namespace context {


template <class Key, class Data, class HashFcn = std::hash<Key> >
class InsertHashMap {
private:
  using KeyVec = std::deque<Key>;
  /** A list of the keys in the map maintained as a stack. */
  KeyVec d_keys;

  using HashMap = std::unordered_map<const Key, const Data, HashFcn>;
  /** The hash_map used for element lookup. */
  HashMap d_hashMap;

public:
  /**
   * An iterator over a list of keys.
   * Use this to efficiently iterate over the elements.
   * (See std::deque<>::iterator).
   */
  typedef typename KeyVec::const_iterator key_iterator;

  /**An iterator over the elements in the hash_map. */
  typedef typename HashMap::const_iterator const_iterator;

  // The type of the <Key, Data> values in the hashmap.
  using value_type = typename HashMap::value_type;

  /**
   * Returns an iterator to the begining of the HashMap.
   * Acts like a hash_map::const_iterator.
   */
  const_iterator begin() const{
    return d_hashMap.begin();
  }
  /**
   * Returns an iterator to the end of the HashMap.
   * Acts like a hash_map::const_iterator.
   */
  const_iterator end() const{
    return d_hashMap.end();
  }

  /**
   * Returns an iterator to the Key k of the map.
   * See hash_map::find()
   */
  const_iterator find(const Key& k) const{
    return d_hashMap.find(k);
  }

  /** Returns an iterator to the start of the set of keys. */
  key_iterator key_begin() const{
    return d_keys.begin();
  }
  /** Returns an iterator to the end of the set of keys. */
  key_iterator key_end() const{
    return d_keys.end();
  }

  /** Returns true if the map is empty. */
  bool empty() const { return d_keys.empty(); }
  /** Returns the number of elements in the map. */
  size_t size() const { return d_keys.size(); }

  /** Returns true if k is a mapped key. */
  bool contains(const Key& k) const {
    return find(k) != end();
  }

  /**
   * Returns a reference the data mapped by k.
   * This must succeed.
   */
  const Data& operator[](const Key& k) const {
    const_iterator ci = find(k);
    Assert(ci != end());
    return (*ci).second;
  }

  /**
   * Inserts an element into the map, and pushes its key to the front
   * of the stack. The key inserted must be not be currently mapped.
   */
  void push_front(const Key& k, const Data& d){
    Assert(!contains(k));
    d_hashMap.insert(std::make_pair(k, d));
    d_keys.push_front(k);
  }

  /**
   * Inserts an element into the map, and pushes its key onto the
   * back on the stack.  The key inserted must be not be currently mapped.
   */
  void push_back(const Key& k, const Data& d){
    Assert(!contains(k));
    d_hashMap.insert(std::make_pair(k, d));
    d_keys.push_back(k);
  }

  /**
   * Pops the key at the front of the list off and removes its key from the map.
   */
  void pop_front(){
    Assert(!empty());
    const Key& front = d_keys.front();
    d_hashMap.erase(front);

    Debug("TrailHashMap") <<"TrailHashMap pop_front " << size() << std::endl;
    d_keys.pop_front();
  }

  /**
   * Pops the key at the back of the stack off and removes its key from the map.
   */
  void pop_back(){
    Assert(!empty());
    const Key& back = d_keys.back();
    d_hashMap.erase(back);

    Debug("TrailHashMap") <<"TrailHashMap pop_back " << size() << std::endl;
    d_keys.pop_back();
  }

  /**
   * Pops the back of the stack until the size is below s.
   */
  void pop_to_size(size_t s){
    while(size() > s){
      pop_back();
    }
  }
};/* class TrailHashMap<> */

template <class Key, class Data, class HashFcn>
class CDInsertHashMap : public ContextObj {
private:
  typedef InsertHashMap<Key, Data, HashFcn> IHM;

  /** An InsertHashMap that backs all of the data. */
  IHM* d_insertMap;

  /** For restores, we need to keep track of the previous size. */
  size_t d_size;

  /**
   * To support insertAtContextLevelZero() and restores,
   * we have called d_insertMap->d_pushFront().
   */
  size_t d_pushFronts;

  /**
   * Private copy constructor used only by save().  d_insertMap is
   * not copied: only the base class information and
   * d_size and d_pushFronts are needed in restore.
   */
  CDInsertHashMap(const CDInsertHashMap& l) :
    ContextObj(l),
    d_insertMap(NULL),
    d_size(l.d_size),
    d_pushFronts(l.d_pushFronts)
  {
    Debug("CDInsertHashMap") << "copy ctor: " << this
                    << " from " << &l
                    << " size " << d_size << std::endl;
  }
  CDInsertHashMap& operator=(const CDInsertHashMap&) = delete;

  /**
   * Implementation of mandatory ContextObj method save: simply copies
   * the current size information to a copy using the copy constructor (the
   * pointer and the allocated size are *not* copied as they are not
   * restored on a pop).  The saved information is allocated using the
   * ContextMemoryManager.
   */
  ContextObj* save(ContextMemoryManager* pCMM) override
  {
    ContextObj* data = new(pCMM) CDInsertHashMap<Key, Data, HashFcn>(*this);
    Debug("CDInsertHashMap") << "save " << this
                            << " at level " << this->getContext()->getLevel()
                            << " size at " << this->d_size
                            << " d_list is " << this->d_insertMap
                            << " data:" << data << std::endl;
    return data;
  }
protected:
  /**
   * Implementation of mandatory ContextObj method restore:
   * restore to the previous size taking into account the number
   * of new pushFront calls have happened since saving.
   * The d_insertMap is untouched and d_pushFronts is also kept.
   */
 void restore(ContextObj* data) override
 {
   Debug("CDInsertHashMap")
       << "restore " << this << " level " << this->getContext()->getLevel()
       << " data == " << data << " d_insertMap == " << this->d_insertMap
       << std::endl;
   size_t oldSize = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_size;
   size_t oldPushFronts =
       ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_pushFronts;
   Assert(oldPushFronts <= d_pushFronts);

   // The size to restore to.
   size_t restoreSize = oldSize + (d_pushFronts - oldPushFronts);
   d_insertMap->pop_to_size(restoreSize);
   d_size = restoreSize;
   Assert(d_insertMap->size() == d_size);
   Debug("CDInsertHashMap")
       << "restore " << this << " level " << this->getContext()->getLevel()
       << " size back to " << this->d_size << std::endl;
  }
public:

 /**
   * Main constructor: d_insertMap starts as an empty map, with the size is 0
   */
  CDInsertHashMap(Context* context) :
    ContextObj(context),
    d_insertMap(new IHM()),
    d_size(0),
    d_pushFronts(0){
    Assert(d_insertMap->size() == d_size);
  }

  /**
   * Destructor: delete the d_insertMap
   */
  ~CDInsertHashMap() {
    this->destroy();
    delete d_insertMap;
  }

  /** An iterator over the elements in the hash_map. */
  typedef typename IHM::const_iterator const_iterator;

  /**
   * An iterator over a list of keys.
   * Use this to efficiently iterate over the elements.
   * (See std::deque<>::iterator).
   */
  typedef typename IHM::key_iterator key_iterator;

  // The type of the <key, data> values in the hashmap.
  using value_type = typename IHM::value_type;

  /** Returns true if the map is empty in the current context. */
  bool empty() const{
    return d_size == 0;
  }

  /** Returns true the size of the map in the current context. */
  size_t size() const {
    return d_size;
  }

  /**
   * Inserts an element into the map.
   * The key inserted must be not be currently mapped.
   * This is implemented using d_insertMap.push_back().
   */
  void insert(const Key& k, const Data& d){
    makeCurrent();
    ++d_size;
    d_insertMap->push_back(k, d);
    Assert(d_insertMap->size() == d_size);
  }

  /**
   * Checks if the key k is mapped already.
   * If it is, this returns false.
   * Otherwise it is inserted and this returns true.
   */
  bool insert_safe(const Key& k, const Data& d){
    if(contains(k)){
      return false;
    }else{
      insert(k,d);
      return true;
    }
  }

  /**
   * Version of insert() for CDMap<> that inserts data value d at
   * context level zero.
   *
   * It is an error to insertAtContextLevelZero()
   * a key that already is in the map.
   */
  void insertAtContextLevelZero(const Key& k, const Data& d){
    makeCurrent();
    ++d_size;
    ++d_pushFronts;
    d_insertMap->push_front(k, d);
  }

  /** Returns true if k is a mapped key in the context. */
  bool contains(const Key& k) const {
    return d_insertMap->contains(k);
  }

  /**
   * Returns a reference the data mapped by k.
   * k must be in the map in this context.
   */
  const Data& operator[](const Key& k) const {
    return (*d_insertMap)[k];
  }

   /**
    * Returns a const_iterator to the value_type if k is a mapped key in
    * the context.
    */
  const_iterator find(const Key& k) const {
    return d_insertMap->find(k);
  }

  /**
   * Returns an iterator to the begining of the map.
   * Acts like a hash_map::const_iterator.
   */
  const_iterator begin() const{
    return d_insertMap->begin();
  }

  /**
   * Returns an iterator to the end of the map.
   * Acts like a hash_map::const_iterator.
   */
  const_iterator end() const{
    return d_insertMap->end();
  }

  /** Returns an iterator to the start of the set of keys. */
  key_iterator key_begin() const{
    return d_insertMap->key_begin();
  }
  /** Returns an iterator to the end of the set of keys. */
  key_iterator key_end() const{
    return d_insertMap->key_end();
  }
};/* class CDInsertHashMap<> */

template <class Data, class HashFcn>
class CDInsertHashMap<TNode, Data, HashFcn> : public ContextObj {
  /* CDInsertHashMap is challenging to get working with TNode.
   * Consider using CDHashMap<TNode,...> instead.
   *
   * Explanation:
   * CDInsertHashMap uses keys for deallocation.
   * If the key is a TNode and the backing (the hard node reference)
   * for the key in another data structure removes the key at the same context
   * the ref count could drop to 0.  The key would then not be eligible to be
   * hashed. Getting the order right with a guarantee is too hard.
   */

  static_assert(sizeof(Data) == 0,
                "Cannot create a CDInsertHashMap with TNode keys");
};

}  // namespace context
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, Mathias Preiner, Morgan Deters
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 insert only hashmap built using trail of edits
14		*
15		* Context-dependent hashmap that only allows for one insertion per element.
16		* This can be viewed as a highly restricted version of CDHashMap.
17		* It is significantly lighter in memory usage than CDHashMap.
18		*
19		* See also:
20		* CDTrailHashMap : A lightweight CD hash map with poor iteration
21		* characteristics and some quirks in usage.
22		* CDHashMap : A fully featured CD hash map. (The closest to <ext/hash_map>)
23		*
24		* Notes:
25		* - To iterate efficiently over the elements use the key_iterators.
26		* - operator[] is only supported as a const derefence (must succeed).
27		* - insert(k) must always work.
28		* - Use insert_safe if you want to check if the element has been inserted
29		* and only insert if it has not yet been.
30		* - Does not accept TNodes as keys.
31		* - Supports insertAtContextLevelZero() if the element is not in the map.
32		*/
33
34		#include <deque>
35		#include <functional>
36		#include <unordered_map>
37		#include <utility>
38
39		#include "base/check.h"
40		#include "base/output.h"
41		#include "context/cdinsert_hashmap_forward.h"
42		#include "context/context.h"
43		#include "cvc5_private.h"
44		#include "expr/node.h"
45
46		#pragma once
47
48		namespace cvc5 {
49		namespace context {
50
51
52		template <class Key, class Data, class HashFcn = std::hash<Key> >
53	1569328	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	80	const_iterator begin() const{
82	80	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	472802648	const_iterator end() const{
89	472802648	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	472802414	const_iterator find(const Key& k) const{
97	472802414	return d_hashMap.find(k);
98		}
99
100		/** Returns an iterator to the start of the set of keys. */
101	583	key_iterator key_begin() const{
102	583	return d_keys.begin();
103		}
104		/** Returns an iterator to the end of the set of keys. */
105	583	key_iterator key_end() const{
106	583	return d_keys.end();
107		}
108
109		/** Returns true if the map is empty. */
110	28417190	bool empty() const { return d_keys.empty(); }
111		/** Returns the number of elements in the map. */
112	93492973	size_t size() const { return d_keys.size(); }
113
114		/** Returns true if k is a mapped key. */
115	260038641	bool contains(const Key& k) const {
116	260038641	return find(k) != end();
117		}
118
119		/**
120		* Returns a reference the data mapped by k.
121		* This must succeed.
122		*/
123	85214744	const Data& operator[](const Key& k) const {
124	85214744	const_iterator ci = find(k);
125	85214744	Assert(ci != end());
126	85214744	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	31618295	void push_back(const Key& k, const Data& d){
144	31618295	Assert(!contains(k));
145	31618295	d_hashMap.insert(std::make_pair(k, d));
146	31618295	d_keys.push_back(k);
147	31618295	}
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	28417190	void pop_back(){
165	28417190	Assert(!empty());
166	28417190	const Key& back = d_keys.back();
167	28417190	d_hashMap.erase(back);
168
169	28417190	Debug("TrailHashMap") <<"TrailHashMap pop_back " << size() << std::endl;
170	28417190	d_keys.pop_back();
171	28417190	}
172
173		/**
174		* Pops the back of the stack until the size is below s.
175		*/
176	30545007	void pop_to_size(size_t s){
177	58962197	while(size() > s){
178	28417190	pop_back();
179		}
180	2127817	}
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	2127817	CDInsertHashMap(const CDInsertHashMap& l) :
206		ContextObj(l),
207		d_insertMap(NULL),
208	2127817	d_size(l.d_size),
209	4255634	d_pushFronts(l.d_pushFronts)
210		{
211	6383451	Debug("CDInsertHashMap") << "copy ctor: " << this
212	4255634	<< " from " << &l
213	2127817	<< " size " << d_size << std::endl;
214	2127817	}
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	2127817	ContextObj* save(ContextMemoryManager* pCMM) override
225		{
226	2127817	ContextObj* data = new(pCMM) CDInsertHashMap<Key, Data, HashFcn>(*this);
227	6383451	Debug("CDInsertHashMap") << "save " << this
228	4255634	<< " at level " << this->getContext()->getLevel()
229	2127817	<< " size at " << this->d_size
230	2127817	<< " d_list is " << this->d_insertMap
231	2127817	<< " data:" << data << std::endl;
232	2127817	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	2127817	void restore(ContextObj* data) override
242		{
243	6383451	Debug("CDInsertHashMap")
244	4255634	<< "restore " << this << " level " << this->getContext()->getLevel()
245	2127817	<< " data == " << data << " d_insertMap == " << this->d_insertMap
246		<< std::endl;
247	2127817	size_t oldSize = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_size;
248	2127817	size_t oldPushFronts =
249	2127817	((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_pushFronts;
250	2127817	Assert(oldPushFronts <= d_pushFronts);
251
252		// The size to restore to.
253	2127817	size_t restoreSize = oldSize + (d_pushFronts - oldPushFronts);
254	2127817	d_insertMap->pop_to_size(restoreSize);
255	2127817	d_size = restoreSize;
256	2127817	Assert(d_insertMap->size() == d_size);
257	6383451	Debug("CDInsertHashMap")
258	4255634	<< "restore " << this << " level " << this->getContext()->getLevel()
259	2127817	<< " size back to " << this->d_size << std::endl;
260	2127817	}
261		public:
262
263		/**
264		* Main constructor: d_insertMap starts as an empty map, with the size is 0
265		*/
266	784664	CDInsertHashMap(Context* context) :
267		ContextObj(context),
268	784664	d_insertMap(new IHM()),
269		d_size(0),
270	1569328	d_pushFronts(0){
271	784664	Assert(d_insertMap->size() == d_size);
272	784664	}
273
274		/**
275		* Destructor: delete the d_insertMap
276		*/
277	784664	~CDInsertHashMap() {
278	784664	this->destroy();
279	784664	delete d_insertMap;
280	1569328	}
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		bool empty() const{
297		return d_size == 0;
298		}
299
300		/** Returns true the size of the map in the current context. */
301	7540	size_t size() const {
302	7540	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	31618295	void insert(const Key& k, const Data& d){
311	31618295	makeCurrent();
312	31618295	++d_size;
313	31618295	d_insertMap->push_back(k, d);
314	31618295	Assert(d_insertMap->size() == d_size);
315	31618295	}
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	10100881	bool insert_safe(const Key& k, const Data& d){
323	10100881	if(contains(k)){
324	1123406	return false;
325		}else{
326	8977475	insert(k,d);
327	8977475	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	228420346	bool contains(const Key& k) const {
347	228420346	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	85214744	const Data& operator[](const Key& k) const {
355	85214744	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	127549029	const_iterator find(const Key& k) const {
363	127549029	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	80	const_iterator begin() const{
371	80	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	127549263	const_iterator end() const{
379	127549263	return d_insertMap->end();
380		}
381
382		/** Returns an iterator to the start of the set of keys. */
383	583	key_iterator key_begin() const{
384	583	return d_insertMap->key_begin();
385		}
386		/** Returns an iterator to the end of the set of keys. */
387	583	key_iterator key_end() const{
388	583	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		} // namespace context
410		} // namespace cvc5