CBMC
irep_hash_container.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: IREP Hash Container
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_IREP_HASH_CONTAINER_H
13 #define CPROVER_UTIL_IREP_HASH_CONTAINER_H
14 
15 #include <map>
16 #include <vector>
17 
18 #include "irep.h"
19 #include "numbering.h"
20 
22 {
23 public:
24  std::size_t number(const irept &irep);
25 
26  explicit irep_hash_container_baset(bool _full):full(_full)
27  {
28  }
29 
30  void clear()
31  {
32  numbering.clear();
33  }
34 
35 protected:
36  // replacing the following two hash-tables by
37  // std::maps doesn't make much difference in performance
38 
39  // this is the first level: address of the content
40 
42  {
43  std::size_t operator()(const void *p) const
44  {
45  return (std::size_t)p;
46  }
47  };
48 
49  struct irep_entryt
50  {
51  std::size_t number;
52  irept irep; // copy to keep addresses stable
53 
54  irep_entryt(std::size_t _number, const irept &_irep)
55  : number(_number), irep(_irep)
56  {
57  }
58  };
59 
60  typedef std::unordered_map<const void *, irep_entryt, pointer_hasht>
63 
64  // this is the second level: content
65 
66  typedef std::vector<std::size_t> packedt;
67 
68  struct vector_hasht
69  {
70  std::size_t operator()(const packedt &p) const;
71  };
72 
74 
75  void pack(const irept &irep, packedt &);
76 
77  bool full;
78 };
79 
80 // excludes comments
83 {
84 public:
86  {
87  }
88 };
89 
90 // includes comments
93 {
94 public:
96  {
97  }
98 };
99 
100 template <typename Key, typename T>
102 {
103 protected:
104  using mapt = std::map<std::size_t, T>;
105 
106 public:
107  using key_type = Key;
108  using mapped_type = T;
109  using value_type = std::pair<const Key, T>;
110  using const_iterator = typename mapt::const_iterator;
111  using iterator = typename mapt::iterator;
112 
113  const_iterator find(const Key &key) const
114  {
115  return map.find(hash_container.number(key));
116  }
117 
118  iterator find(const Key &key)
119  {
120  return map.find(hash_container.number(key));
121  }
122 
124  {
125  return map.begin();
126  }
127 
129  {
130  return map.begin();
131  }
132 
134  {
135  return map.end();
136  }
137 
139  {
140  return map.end();
141  }
142 
143  void clear()
144  {
146  map.clear();
147  }
148 
149  std::size_t size() const
150  {
151  return map.size();
152  }
153 
154  bool empty() const
155  {
156  return map.empty();
157  }
158 
159  T &operator[](const Key &key)
160  {
161  const std::size_t i = hash_container.number(key);
162  return map[i];
163  }
164 
165  std::pair<iterator, bool> insert(const value_type &value)
166  {
167  const std::size_t i = hash_container.number(value.first);
168  return map.emplace(i, value.second);
169  }
170 
171  void erase(iterator it)
172  {
173  map.erase(it);
174  }
175 
177  {
178  std::swap(hash_container, other.hash_container);
179  std::swap(map, other.map);
180  }
181 
182 protected:
185 };
186 
187 #endif // CPROVER_UTIL_IREP_HASH_CONTAINER_H
std::vector< std::size_t > packedt
numberingt< packedt, vector_hasht > numbering
void pack(const irept &irep, packedt &)
std::size_t number(const irept &irep)
std::unordered_map< const void *, irep_entryt, pointer_hasht > ptr_hasht
typename mapt::iterator iterator
const_iterator find(const Key &key) const
std::pair< iterator, bool > insert(const value_type &value)
std::size_t size() const
std::pair< const Key, T > value_type
T & operator[](const Key &key)
irep_hash_containert hash_container
const_iterator begin() const
std::map< std::size_t, T > mapt
iterator find(const Key &key)
const_iterator end() const
void swap(irep_hash_mapt< Key, T > &other)
typename mapt::const_iterator const_iterator
void erase(iterator it)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:360
irep_entryt(std::size_t _number, const irept &_irep)
std::size_t operator()(const void *p) const
std::size_t operator()(const packedt &p) const