Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/context/cdhashmap.h	Lines:	120	123	97.6 %
Date:	2021-09-12	Branches:	510	1285	39.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Tim King, Dejan Jovanovic
 *
 * 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 map class.
 *
 * Generic templated class for a map which must be saved and restored as
 * contexts are pushed and popped.  Requires that operator= be defined for the
 * data class, and operator== for the key class.  For key types that don't have
 * a std::hash<>, you should provide an explicit HashFcn.
 *
 * See also:
 *  CDInsertHashMap : An "insert-once" CD hash map.
 *  CDTrailHashMap : A lightweight CD hash map with poor iteration
 *    characteristics and some quirks in usage.
 *
 * Internal documentation:
 *
 * CDHashMap<> is something of a work in progress at present (26 May
 * 2010), due to some recent discoveries of problems with its
 * internal state.  Here are some notes on the internal use of
 * CDOhash_maps that may be useful in figuring out this mess:
 *
 *     So you have a CDHashMap<>.
 *
 *     You insert some (key,value) pairs.  Each allocates a CDOhash_map<>
 *     and goes on a doubly-linked list headed by map.d_first and
 *     threaded via CDOhash_map.{d_prev,d_next}.  CDOhash_maps are constructed
 *     with a NULL d_map pointer, but then immediately call
 *     makeCurrent() and set the d_map pointer back to the map.  At
 *     context level 0, this doesn't lead to anything special.  In
 *     higher context levels, this stores away a CDOhash_map with a NULL
 *     map pointer at level 0, and a non-NULL map pointer in the
 *     current context level.  (Remember that for later.)
 *
 *     When a key is associated to a new value in a CDHashMap, its
 *     associated CDOhash_map calls makeCurrent(), then sets the new
 *     value.  The save object is also a CDOhash_map (allocated in context
 *     memory).
 *
 *     Now, CDOhash_maps disappear in a variety of ways.
 *
 *     First, you might pop beyond a "modification of the value"
 *     scope level, requiring a re-association of the key to an old
 *     value.  This is easy.  CDOhash_map::restore() does the work, and
 *     the context memory of the save object is reclaimed as usual.
 *
 *     Second, you might pop beyond a "insert the key" scope level,
 *     requiring that the key be completely removed from the map and
 *     its CDOhash_map object memory freed.  Here, the CDOhash_map is restored
 *     to a "NULL-map" state (see above), signaling it to remove
 *     itself from the map completely and put itself on a "trash
 *     list" for its scope.
 *
 *     Third, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()).
 *     This first calls destroy(), as per ContextObj contract, but
 *     cdhashmapdoesn't save/restore itself, so that does nothing at the
 *     CDHashMap-level. Then, for each element in the map, it marks it as being
 *     "part of a complete map destruction", which essentially short-circuits
 *     CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates
 *     it.
 *
 *     Fourth, you might clear() the CDHashMap.  This does exactly the
 *     same as CDHashMap::~CDHashMap(), except that it doesn't call destroy()
 *     on itself.
 *
 *     ContextObj::deleteSelf() calls the CDOhash_map destructor, then
 *     frees the memory associated to the CDOhash_map.
 *     CDOhash_map::~CDOhash_map() calls destroy(), which restores as much as
 *     possible.
 */

#include "cvc5_private.h"

#ifndef CVC5__CONTEXT__CDHASHMAP_H
#define CVC5__CONTEXT__CDHASHMAP_H

#include <functional>
#include <iterator>
#include <unordered_map>

#include "base/check.h"
#include "context/cdhashmap_forward.h"
#include "context/context.h"

namespace cvc5 {
namespace context {

// Auxiliary class: almost the same as CDO (see cdo.h)

template <class Key, class Data, class HashFcn = std::hash<Key> >
class CDOhash_map : public ContextObj
{
  friend class CDHashMap<Key, Data, HashFcn>;

 public:
  // The type of the <Key, Data> pair mapped by this class.
  //
  // Implementation:
  // The data and key visible to users of CDHashMap are only visible through
  // const references. Thus the type of dereferencing a
  // CDHashMap<Key, Data>::iterator.second is intended to always be a
  // `const Data&`. (Otherwise, to get a Data& safely, access operations
  // would need to makeCurrent() to get the Data&, which is an unacceptable
  // performance hit.) To allow for the desired updating in other scenarios, we
  // store a std::pair<const Key, const Data> and break the const encapsulation
  // when necessary.
  using value_type = std::pair<const Key, const Data>;

 private:
  value_type d_value;

  // See documentation of value_type for why this is needed.
  Key& mutable_key() { return const_cast<Key&>(d_value.first); }
  // See documentation of value_type for why this is needed.
  Data& mutable_data() { return const_cast<Data&>(d_value.second); }

  CDHashMap<Key, Data, HashFcn>* d_map;

  // Doubly-linked list for keeping track of elements in order of insertion
  CDOhash_map* d_prev;
  CDOhash_map* d_next;

  ContextObj* save(ContextMemoryManager* pCMM) override
  {
    return new (pCMM) CDOhash_map(*this);
  }

  void restore(ContextObj* data) override
  {
    CDOhash_map* p = static_cast<CDOhash_map*>(data);
    if (d_map != NULL)
    {
      if (p->d_map == NULL)
      {
        Assert(d_map->d_map.find(getKey()) != d_map->d_map.end()
               && (*d_map->d_map.find(getKey())).second == this);
        // no longer in map (popped beyond first level in which it was)
        d_map->d_map.erase(getKey());
        // If we call deleteSelf() here, it re-enters restore().  So,
        // put it on a "trash heap" instead, for later deletion.
        //
        // FIXME multithreading
        if (d_map->d_first == this)
        {
          Debug("gc") << "remove first-elem " << this << " from map " << d_map
                      << " with next-elem " << d_next << std::endl;
          if (d_next == this)
          {
            Assert(d_prev == this);
            d_map->d_first = NULL;
          }
          else
          {
            d_map->d_first = d_next;
          }
        }
        else
        {
          Debug("gc") << "remove nonfirst-elem " << this << " from map "
                      << d_map << std::endl;
        }
        d_next->d_prev = d_prev;
        d_prev->d_next = d_next;

        Debug("gc") << "CDHashMap<> trash push_back " << this << std::endl;
        // this->deleteSelf();
        enqueueToGarbageCollect();
      }
      else
      {
        mutable_data() = p->get();
      }
    }
    // Explicitly call destructors for the key and the data as they will not
    // otherwise get called.
    p->mutable_key().~Key();
    p->mutable_data().~Data();
  }

  /** ensure copy ctor is only called by us */
  CDOhash_map(const CDOhash_map& other)
      : ContextObj(other),
        // don't need to save the key---and if we do we can get
        // refcounts for Node keys messed up and leak memory
        d_value(Key(), other.d_value.second),
        d_map(other.d_map),
        d_prev(NULL),
        d_next(NULL)
  {
  }
  CDOhash_map& operator=(const CDOhash_map&) = delete;

 public:
  CDOhash_map(Context* context,
              CDHashMap<Key, Data, HashFcn>* map,
              const Key& key,
              const Data& data,
              bool atLevelZero = false)
      : ContextObj(false, context), d_value(key, data), d_map(NULL)
  {
    if (atLevelZero)
    {
      // "Initializing" map insertion: this entry will never be
      // removed from the map, it's inserted at level 0 as an
      // "initializing" element.  See
      // CDHashMap<>::insertAtContextLevelZero().
      mutable_data() = data;
    }
    else
    {
      // Normal map insertion: first makeCurrent(), then set the data
      // and then, later, the map.  Order is important; we can't
      // initialize d_map in the constructor init list above, because
      // we want the restore of d_map to NULL to signal us to remove
      // the element from the map.

      set(data);
    }
    d_map = map;

    CDOhash_map*& first = d_map->d_first;
    if (first == NULL)
    {
      first = d_next = d_prev = this;
      Debug("gc") << "add first-elem " << this << " to map " << d_map
                  << std::endl;
    }
    else
    {
      Debug("gc") << "add nonfirst-elem " << this << " to map " << d_map
                  << " with first-elem " << first << "[" << first->d_prev << " "
                  << first->d_next << std::endl;
      d_prev = first->d_prev;
      d_next = first;
      d_prev->d_next = this;
      first->d_prev = this;
    }
  }

  ~CDOhash_map() { destroy(); }

  void set(const Data& data)
  {
    makeCurrent();
    mutable_data() = data;
  }

  const Key& getKey() const { return d_value.first; }

  const Data& get() const { return d_value.second; }

  const value_type& getValue() const { return d_value; }

  operator Data() { return get(); }

  const Data& operator=(const Data& data)
  {
    set(data);
    return data;
  }

  CDOhash_map* next() const
  {
    if (d_next == d_map->d_first)
    {
      return NULL;
    }
    else
    {
      return d_next;
    }
  }
}; /* class CDOhash_map<> */

/**
 * Generic templated class for a map which must be saved and restored
 * as contexts are pushed and popped.  Requires that operator= be
 * defined for the data class, and operator== for the key class.
 */
template <class Key, class Data, class HashFcn>
class CDHashMap : public ContextObj
{
  typedef CDOhash_map<Key, Data, HashFcn> Element;
  typedef std::unordered_map<Key, Element*, HashFcn> table_type;

  friend class CDOhash_map<Key, Data, HashFcn>;

  table_type d_map;

  Element* d_first;
  Context* d_context;

  // Nothing to save; the elements take care of themselves
  ContextObj* save(ContextMemoryManager* pCMM) override
  {
    Unreachable();
    SuppressWrongNoReturnWarning;
  }

  // Similarly, nothing to restore
  void restore(ContextObj* data) override { Unreachable(); }

  // no copy or assignment
  CDHashMap(const CDHashMap&) = delete;
  CDHashMap& operator=(const CDHashMap&) = delete;

 public:
  CDHashMap(Context* context)
      : ContextObj(context), d_map(), d_first(NULL), d_context(context)
  {
  }

  ~CDHashMap()
  {
    Debug("gc") << "cdhashmap" << this << " disappearing, destroying..."
                << std::endl;
    destroy();
    Debug("gc") << "cdhashmap" << this << " disappearing, done destroying"
                << std::endl;
    clear();
  }

  void clear()
  {
    Debug("gc") << "clearing cdhashmap" << this << ", emptying trash"
                << std::endl;
    Debug("gc") << "done emptying trash for " << this << std::endl;

    for (auto& key_element_pair : d_map)
    {
      // mark it as being a destruction (short-circuit restore())
      Element* element = key_element_pair.second;
      element->d_map = nullptr;
      element->deleteSelf();
    }
    d_map.clear();
    d_first = nullptr;
  }

  // The usual operators of map

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

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

  size_t count(const Key& k) const { return d_map.count(k); }

  // If a key is not present, a new object is created and inserted
  Element& operator[](const Key& k)
  {
    const auto res = d_map.insert({k, nullptr});
    if (res.second)
    {  // create new object
      res.first->second = new (true) Element(d_context, this, k, Data());
    }
    return *(res.first->second);
  }

  bool insert(const Key& k, const Data& d)
  {
    const auto res = d_map.insert({k, nullptr});
    if (res.second)
    {  // create new object
      res.first->second = new (true) Element(d_context, this, k, d);
    }
    else
    {
      res.first->second->set(d);
    }
    return res.second;
  }

  /**
   * Version of insert() for CDHashMap<> that inserts data value d at
   * context level zero.  This is a special escape hatch for inserting
   * "initializing" data into the map.  Imagine something happens at a
   * deep context level L that causes insertion into a map, such that
   * the object should have an "initializing" value v1 below context
   * level L, and a "current" value v2 at context level L.  Then you
   * can (assuming key k):
   *
   *   map.insertAtContextLevelZero(k, v1);
   *   map.insert(k, v2);
   *
   * The justification for this "escape hatch" has to do with
   * variables and assignments in theories (e.g., in arithmetic).
   * Let's say you introduce a new variable x at some deep decision
   * level (thanks to lazy registration, or a splitting lemma, or
   * whatever).  x might be mapped to something, but for theory
   * implementation simplicity shouldn't disappear from the map on
   * backjump; rather, it can take another (legal) value, or a special
   * value to indicate it needs to be recomputed.
   *
   * It is an error (checked via AlwaysAssert()) to
   * insertAtContextLevelZero() a key that already is in the map.
   */
  void insertAtContextLevelZero(const Key& k, const Data& d)
  {
    AlwaysAssert(d_map.find(k) == d_map.end());

    Element* obj =
        new (true) Element(d_context, this, k, d, true /* atLevelZero */);
    d_map.insert(std::make_pair(k, obj));
  }

  // FIXME: no erase(), too much hassle to implement efficiently...

  using value_type = typename CDOhash_map<Key, Data, HashFcn>::value_type;

  class iterator
  {
    const Element* d_it;

   public:
    using iterator_category = std::input_iterator_tag;
    using value_type = typename CDOhash_map<Key, Data, HashFcn>::value_type;
    using difference_type = ptrdiff_t;
    using pointer = typename CDOhash_map<Key, Data, HashFcn>::value_type*;
    using reference = typename CDOhash_map<Key, Data, HashFcn>::value_type&;

    iterator(const Element* p) : d_it(p) {}
    iterator(const iterator& i) : d_it(i.d_it) {}

    // Default constructor
    iterator() : d_it(nullptr) {}

    // (Dis)equality
    bool operator==(const iterator& i) const { return d_it == i.d_it; }
    bool operator!=(const iterator& i) const { return d_it != i.d_it; }

    // Dereference operators.
    const value_type& operator*() const { return d_it->getValue(); }
    const value_type* operator->() const { return &d_it->getValue(); }

    // Prefix increment
    iterator& operator++()
    {
      d_it = d_it->next();
      return *this;
    }

    // Postfix increment is not yet supported.
  }; /* class CDHashMap<>::iterator */

  typedef iterator const_iterator;

  iterator begin() const { return iterator(d_first); }

  iterator end() const { return iterator(NULL); }

  iterator find(const Key& k) const
  {
    typename table_type::const_iterator i = d_map.find(k);

    if (i == d_map.end())
    {
      return end();
    }
    else
    {
      return iterator((*i).second);
    }
  }

}; /* class CDHashMap<> */

}  // namespace context
}  // namespace cvc5

#endif /* CVC5__CONTEXT__CDHASHMAP_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Tim King, Dejan Jovanovic
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 map class.
14		*
15		* Generic templated class for a map which must be saved and restored as
16		* contexts are pushed and popped. Requires that operator= be defined for the
17		* data class, and operator== for the key class. For key types that don't have
18		* a std::hash<>, you should provide an explicit HashFcn.
19		*
20		* See also:
21		* CDInsertHashMap : An "insert-once" CD hash map.
22		* CDTrailHashMap : A lightweight CD hash map with poor iteration
23		* characteristics and some quirks in usage.
24		*
25		* Internal documentation:
26		*
27		* CDHashMap<> is something of a work in progress at present (26 May
28		* 2010), due to some recent discoveries of problems with its
29		* internal state. Here are some notes on the internal use of
30		* CDOhash_maps that may be useful in figuring out this mess:
31		*
32		* So you have a CDHashMap<>.
33		*
34		* You insert some (key,value) pairs. Each allocates a CDOhash_map<>
35		* and goes on a doubly-linked list headed by map.d_first and
36		* threaded via CDOhash_map.{d_prev,d_next}. CDOhash_maps are constructed
37		* with a NULL d_map pointer, but then immediately call
38		* makeCurrent() and set the d_map pointer back to the map. At
39		* context level 0, this doesn't lead to anything special. In
40		* higher context levels, this stores away a CDOhash_map with a NULL
41		* map pointer at level 0, and a non-NULL map pointer in the
42		* current context level. (Remember that for later.)
43		*
44		* When a key is associated to a new value in a CDHashMap, its
45		* associated CDOhash_map calls makeCurrent(), then sets the new
46		* value. The save object is also a CDOhash_map (allocated in context
47		* memory).
48		*
49		* Now, CDOhash_maps disappear in a variety of ways.
50		*
51		* First, you might pop beyond a "modification of the value"
52		* scope level, requiring a re-association of the key to an old
53		* value. This is easy. CDOhash_map::restore() does the work, and
54		* the context memory of the save object is reclaimed as usual.
55		*
56		* Second, you might pop beyond a "insert the key" scope level,
57		* requiring that the key be completely removed from the map and
58		* its CDOhash_map object memory freed. Here, the CDOhash_map is restored
59		* to a "NULL-map" state (see above), signaling it to remove
60		* itself from the map completely and put itself on a "trash
61		* list" for its scope.
62		*
63		* Third, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()).
64		* This first calls destroy(), as per ContextObj contract, but
65		* cdhashmapdoesn't save/restore itself, so that does nothing at the
66		* CDHashMap-level. Then, for each element in the map, it marks it as being
67		* "part of a complete map destruction", which essentially short-circuits
68		* CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates
69		* it.
70		*
71		* Fourth, you might clear() the CDHashMap. This does exactly the
72		* same as CDHashMap::~CDHashMap(), except that it doesn't call destroy()
73		* on itself.
74		*
75		* ContextObj::deleteSelf() calls the CDOhash_map destructor, then
76		* frees the memory associated to the CDOhash_map.
77		* CDOhash_map::~CDOhash_map() calls destroy(), which restores as much as
78		* possible.
79		*/
80
81		#include "cvc5_private.h"
82
83		#ifndef CVC5__CONTEXT__CDHASHMAP_H
84		#define CVC5__CONTEXT__CDHASHMAP_H
85
86		#include <functional>
87		#include <iterator>
88		#include <unordered_map>
89
90		#include "base/check.h"
91		#include "context/cdhashmap_forward.h"
92		#include "context/context.h"
93
94		namespace cvc5 {
95		namespace context {
96
97		// Auxiliary class: almost the same as CDO (see cdo.h)
98
99		template <class Key, class Data, class HashFcn = std::hash<Key> >
100		class CDOhash_map : public ContextObj
101		{
102		friend class CDHashMap<Key, Data, HashFcn>;
103
104		public:
105		// The type of the <Key, Data> pair mapped by this class.
106		//
107		// Implementation:
108		// The data and key visible to users of CDHashMap are only visible through
109		// const references. Thus the type of dereferencing a
110		// CDHashMap<Key, Data>::iterator.second is intended to always be a
111		// `const Data&`. (Otherwise, to get a Data& safely, access operations
112		// would need to makeCurrent() to get the Data&, which is an unacceptable
113		// performance hit.) To allow for the desired updating in other scenarios, we
114		// store a std::pair<const Key, const Data> and break the const encapsulation
115		// when necessary.
116		using value_type = std::pair<const Key, const Data>;
117
118		private:
119		value_type d_value;
120
121		// See documentation of value_type for why this is needed.
122	58535353	Key& mutable_key() { return const_cast<Key&>(d_value.first); }
123		// See documentation of value_type for why this is needed.
124	194342979	Data& mutable_data() { return const_cast<Data&>(d_value.second); }
125
126		CDHashMap<Key, Data, HashFcn>* d_map;
127
128		// Doubly-linked list for keeping track of elements in order of insertion
129		CDOhash_map* d_prev;
130		CDOhash_map* d_next;
131
132	58535356	ContextObj* save(ContextMemoryManager* pCMM) override
133		{
134	58535356	return new (pCMM) CDOhash_map(*this);
135		}
136
137	58535353	void restore(ContextObj* data) override
138		{
139	58535353	CDOhash_map* p = static_cast<CDOhash_map*>(data);
140	58535353	if (d_map != NULL)
141		{
142	58482269	if (p->d_map == NULL)
143		{
144	57284662	Assert(d_map->d_map.find(getKey()) != d_map->d_map.end()
145		&& (*d_map->d_map.find(getKey())).second == this);
146		// no longer in map (popped beyond first level in which it was)
147	57284662	d_map->d_map.erase(getKey());
148		// If we call deleteSelf() here, it re-enters restore(). So,
149		// put it on a "trash heap" instead, for later deletion.
150		//
151		// FIXME multithreading
152	57284662	if (d_map->d_first == this)
153		{
154	876496	Debug("gc") << "remove first-elem " << this << " from map " << d_map
155	438248	<< " with next-elem " << d_next << std::endl;
156	438248	if (d_next == this)
157		{
158	438230	Assert(d_prev == this);
159	438230	d_map->d_first = NULL;
160		}
161		else
162		{
163	18	d_map->d_first = d_next;
164		}
165		}
166		else
167		{
168	113692828	Debug("gc") << "remove nonfirst-elem " << this << " from map "
169	56846414	<< d_map << std::endl;
170		}
171	57284662	d_next->d_prev = d_prev;
172	57284662	d_prev->d_next = d_next;
173
174	57284662	Debug("gc") << "CDHashMap<> trash push_back " << this << std::endl;
175		// this->deleteSelf();
176	57284662	enqueueToGarbageCollect();
177		}
178		else
179		{
180	1197607	mutable_data() = p->get();
181		}
182		}
183		// Explicitly call destructors for the key and the data as they will not
184		// otherwise get called.
185	58535353	p->mutable_key().~Key();
186	58535353	p->mutable_data().~Data();
187	58535353	}
188
189		/** ensure copy ctor is only called by us */
190	58535356	CDOhash_map(const CDOhash_map& other)
191		: ContextObj(other),
192		// don't need to save the key---and if we do we can get
193		// refcounts for Node keys messed up and leak memory
194		d_value(Key(), other.d_value.second),
195	58535356	d_map(other.d_map),
196		d_prev(NULL),
197	117070712	d_next(NULL)
198		{
199	58535356	}
200		CDOhash_map& operator=(const CDOhash_map&) = delete;
201
202		public:
203	69199160	CDOhash_map(Context* context,
204		CDHashMap<Key, Data, HashFcn>* map,
205		const Key& key,
206		const Data& data,
207		bool atLevelZero = false)
208	69199160	: ContextObj(false, context), d_value(key, data), d_map(NULL)
209		{
210	69199160	if (atLevelZero)
211		{
212		// "Initializing" map insertion: this entry will never be
213		// removed from the map, it's inserted at level 0 as an
214		// "initializing" element. See
215		// CDHashMap<>::insertAtContextLevelZero().
216	35930	mutable_data() = data;
217		}
218		else
219		{
220		// Normal map insertion: first makeCurrent(), then set the data
221		// and then, later, the map. Order is important; we can't
222		// initialize d_map in the constructor init list above, because
223		// we want the restore of d_map to NULL to signal us to remove
224		// the element from the map.
225
226	69163230	set(data);
227		}
228	69199160	d_map = map;
229
230	69199160	CDOhash_map*& first = d_map->d_first;
231	69199160	if (first == NULL)
232		{
233	1621055	first = d_next = d_prev = this;
234	1621055	Debug("gc") << "add first-elem " << this << " to map " << d_map
235		<< std::endl;
236		}
237		else
238		{
239	135156210	Debug("gc") << "add nonfirst-elem " << this << " to map " << d_map
240	67578105	<< " with first-elem " << first << "[" << first->d_prev << " "
241	67578105	<< first->d_next << std::endl;
242	67578105	d_prev = first->d_prev;
243	67578105	d_next = first;
244	67578105	d_prev->d_next = this;
245	67578105	first->d_prev = this;
246		}
247	69199160	}
248
249	69199153	~CDOhash_map() { destroy(); }
250
251	134574089	void set(const Data& data)
252		{
253	134574089	makeCurrent();
254	134574089	mutable_data() = data;
255	134574089	}
256
257	171853986	const Key& getKey() const { return d_value.first; }
258
259	17679419	const Data& get() const { return d_value.second; }
260
261	122966615	const value_type& getValue() const { return d_value; }
262
263	10622326	operator Data() { return get(); }
264
265	65285791	const Data& operator=(const Data& data)
266		{
267	65285791	set(data);
268	65285791	return data;
269		}
270
271	2042795	CDOhash_map* next() const
272		{
273	2042795	if (d_next == d_map->d_first)
274		{
275	147289	return NULL;
276		}
277		else
278		{
279	1895506	return d_next;
280		}
281		}
282		}; /* class CDOhash_map<> */
283
284		/**
285		* Generic templated class for a map which must be saved and restored
286		* as contexts are pushed and popped. Requires that operator= be
287		* defined for the data class, and operator== for the key class.
288		*/
289		template <class Key, class Data, class HashFcn>
290		class CDHashMap : public ContextObj
291		{
292		typedef CDOhash_map<Key, Data, HashFcn> Element;
293		typedef std::unordered_map<Key, Element*, HashFcn> table_type;
294
295		friend class CDOhash_map<Key, Data, HashFcn>;
296
297		table_type d_map;
298
299		Element* d_first;
300		Context* d_context;
301
302		// Nothing to save; the elements take care of themselves
303		ContextObj* save(ContextMemoryManager* pCMM) override
304		{
305		Unreachable();
306		SuppressWrongNoReturnWarning;
307		}
308
309		// Similarly, nothing to restore
310		void restore(ContextObj* data) override { Unreachable(); }
311
312		// no copy or assignment
313		CDHashMap(const CDHashMap&) = delete;
314		CDHashMap& operator=(const CDHashMap&) = delete;
315
316		public:
317	3012237	CDHashMap(Context* context)
318	3012237	: ContextObj(context), d_map(), d_first(NULL), d_context(context)
319		{
320	3012237	}
321
322	3001404	~CDHashMap()
323		{
324	3001404	Debug("gc") << "cdhashmap" << this << " disappearing, destroying..."
325		<< std::endl;
326	3001404	destroy();
327	3001404	Debug("gc") << "cdhashmap" << this << " disappearing, done destroying"
328		<< std::endl;
329	3001404	clear();
330	6002808	}
331
332	3001404	void clear()
333		{
334	3001404	Debug("gc") << "clearing cdhashmap" << this << ", emptying trash"
335		<< std::endl;
336	3001404	Debug("gc") << "done emptying trash for " << this << std::endl;
337
338	14915895	for (auto& key_element_pair : d_map)
339		{
340		// mark it as being a destruction (short-circuit restore())
341	11914491	Element* element = key_element_pair.second;
342	11914491	element->d_map = nullptr;
343	11914491	element->deleteSelf();
344		}
345	3001404	d_map.clear();
346	3001404	d_first = nullptr;
347	3001404	}
348
349		// The usual operators of map
350
351	155688	size_t size() const { return d_map.size(); }
352
353	3589544	bool empty() const { return d_map.empty(); }
354
355		size_t count(const Key& k) const { return d_map.count(k); }
356
357		// If a key is not present, a new object is created and inserted
358	81767603	Element& operator[](const Key& k)
359		{
360	81767603	const auto res = d_map.insert({k, nullptr});
361	81767603	if (res.second)
362		{ // create new object
363	56210199	res.first->second = new (true) Element(d_context, this, k, Data());
364		}
365	81767603	return *(res.first->second);
366		}
367
368	13078099	bool insert(const Key& k, const Data& d)
369		{
370	13078099	const auto res = d_map.insert({k, nullptr});
371	13078099	if (res.second)
372		{ // create new object
373	12953031	res.first->second = new (true) Element(d_context, this, k, d);
374		}
375		else
376		{
377	125068	res.first->second->set(d);
378		}
379	13078099	return res.second;
380		}
381
382		/**
383		* Version of insert() for CDHashMap<> that inserts data value d at
384		* context level zero. This is a special escape hatch for inserting
385		* "initializing" data into the map. Imagine something happens at a
386		* deep context level L that causes insertion into a map, such that
387		* the object should have an "initializing" value v1 below context
388		* level L, and a "current" value v2 at context level L. Then you
389		* can (assuming key k):
390		*
391		* map.insertAtContextLevelZero(k, v1);
392		* map.insert(k, v2);
393		*
394		* The justification for this "escape hatch" has to do with
395		* variables and assignments in theories (e.g., in arithmetic).
396		* Let's say you introduce a new variable x at some deep decision
397		* level (thanks to lazy registration, or a splitting lemma, or
398		* whatever). x might be mapped to something, but for theory
399		* implementation simplicity shouldn't disappear from the map on
400		* backjump; rather, it can take another (legal) value, or a special
401		* value to indicate it needs to be recomputed.
402		*
403		* It is an error (checked via AlwaysAssert()) to
404		* insertAtContextLevelZero() a key that already is in the map.
405		*/
406	35930	void insertAtContextLevelZero(const Key& k, const Data& d)
407		{
408	35930	AlwaysAssert(d_map.find(k) == d_map.end());
409
410	35930	Element* obj =
411	35930	new (true) Element(d_context, this, k, d, true /* atLevelZero */);
412	35934	d_map.insert(std::make_pair(k, obj));
413	35930	}
414
415		// FIXME: no erase(), too much hassle to implement efficiently...
416
417		using value_type = typename CDOhash_map<Key, Data, HashFcn>::value_type;
418
419		class iterator
420		{
421		const Element* d_it;
422
423		public:
424		using iterator_category = std::input_iterator_tag;
425		using value_type = typename CDOhash_map<Key, Data, HashFcn>::value_type;
426		using difference_type = ptrdiff_t;
427		using pointer = typename CDOhash_map<Key, Data, HashFcn>::value_type*;
428		using reference = typename CDOhash_map<Key, Data, HashFcn>::value_type&;
429
430	560686766	iterator(const Element* p) : d_it(p) {}
431	104	iterator(const iterator& i) : d_it(i.d_it) {}
432
433		// Default constructor
434	120446	iterator() : d_it(nullptr) {}
435
436		// (Dis)equality
437	76164842	bool operator==(const iterator& i) const { return d_it == i.d_it; }
438	203450057	bool operator!=(const iterator& i) const { return d_it != i.d_it; }
439
440		// Dereference operators.
441	115079859	const value_type& operator*() const { return d_it->getValue(); }
442	7886756	const value_type* operator->() const { return &d_it->getValue(); }
443
444		// Prefix increment
445	2042795	iterator& operator++()
446		{
447	2042795	d_it = d_it->next();
448	2042795	return *this;
449		}
450
451		// Postfix increment is not yet supported.
452		}; /* class CDHashMap<>::iterator */
453
454		typedef iterator const_iterator;
455
456	379557	iterator begin() const { return iterator(d_first); }
457
458	400555827	iterator end() const { return iterator(NULL); }
459
460	280873156	iterator find(const Key& k) const
461		{
462	280873156	typename table_type::const_iterator i = d_map.find(k);
463
464	280873156	if (i == d_map.end())
465		{
466	121121774	return end();
467		}
468		else
469		{
470	159751382	return iterator((*i).second);
471		}
472		}
473
474		}; /* class CDHashMap<> */
475
476		} // namespace context
477		} // namespace cvc5
478
479		#endif /* CVC5__CONTEXT__CDHASHMAP_H */