cprover
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 <vector>
16 
17 #include "irep.h"
18 #include "numbering.h"
19 
21 {
22 public:
23  std::size_t number(const irept &irep);
24 
25  explicit irep_hash_container_baset(bool _full):full(_full)
26  {
27  }
28 
29  void clear()
30  {
31  numbering.clear();
32  }
33 
34 protected:
35  // replacing the following two hash-tables by
36  // std::maps doesn't make much difference in performance
37 
38  // this is the first level: address of the content
39 
41  {
42  std::size_t operator()(const void *p) const
43  {
44  return (std::size_t)p;
45  }
46  };
47 
48  struct irep_entryt
49  {
50  std::size_t number;
51  irept irep; // copy to keep addresses stable
52  };
53 
54  typedef std::unordered_map<const void *, irep_entryt, pointer_hasht>
57 
58  // this is the second level: content
59 
60  typedef std::vector<std::size_t> packedt;
61 
62  struct vector_hasht
63  {
64  std::size_t operator()(const packedt &p) const;
65  };
66 
69 
70  void pack(const irept &irep, packedt &);
71 
72  bool full;
73 };
74 
75 // excludes comments
78 {
79 public:
81  {
82  }
83 };
84 
85 // includes comments
88 {
89 public:
91  {
92  }
93 };
94 
95 template <typename Key, typename T>
97 {
98 protected:
99  using mapt = std::map<std::size_t, T>;
100 
101 public:
102  using key_type = Key;
103  using mapped_type = T;
104  using value_type = std::pair<const Key, T>;
105  using const_iterator = typename mapt::const_iterator;
106  using iterator = typename mapt::iterator;
107 
108  const_iterator find(const Key &key) const
109  {
110  return map.find(hash_container.number(key));
111  }
112 
113  iterator find(const Key &key)
114  {
115  return map.find(hash_container.number(key));
116  }
117 
119  {
120  return map.begin();
121  }
122 
124  {
125  return map.begin();
126  }
127 
129  {
130  return map.end();
131  }
132 
134  {
135  return map.end();
136  }
137 
138  void clear()
139  {
141  map.clear();
142  }
143 
144  std::size_t size() const
145  {
146  return map.size();
147  }
148 
149  bool empty() const
150  {
151  return map.empty();
152  }
153 
154  T &operator[](const Key &key)
155  {
156  const std::size_t i = hash_container.number(key);
157  return map[i];
158  }
159 
160  std::pair<iterator, bool> insert(const value_type &value)
161  {
162  const std::size_t i = hash_container.number(value.first);
163  return map.emplace(i, value.second);
164  }
165 
166  void erase(iterator it)
167  {
168  map.erase(it);
169  }
170 
172  {
173  std::swap(hash_container, other.hash_container);
174  std::swap(map, other.map);
175  }
176 
177 protected:
180 };
181 
182 #endif // CPROVER_UTIL_IREP_HASH_CONTAINER_H
irep_hash_mapt::swap
void swap(irep_hash_mapt< Key, T > &other)
Definition: irep_hash_container.h:171
irep_hash_mapt::end
const_iterator end() const
Definition: irep_hash_container.h:128
irep_hash_mapt::map
mapt map
Definition: irep_hash_container.h:179
irep_hash_container_baset::numbering
numberingt numbering
Definition: irep_hash_container.h:68
irep_hash_container_baset::pack
void pack(const irept &irep, packedt &)
Definition: irep_hash_container.cpp:46
irep_hash_container_baset::packedt
std::vector< std::size_t > packedt
Definition: irep_hash_container.h:60
template_numberingt
Definition: numbering.h:21
irep_hash_container_baset::pointer_hasht::operator()
std::size_t operator()(const void *p) const
Definition: irep_hash_container.h:42
irep_hash_container_baset::vector_hasht::operator()
std::size_t operator()(const packedt &p) const
Definition: irep_hash_container.cpp:37
irep_hash_mapt::value_type
std::pair< const Key, T > value_type
Definition: irep_hash_container.h:104
irep_hash_mapt::clear
void clear()
Definition: irep_hash_container.h:138
irep_hash_mapt::begin
const_iterator begin() const
Definition: irep_hash_container.h:118
irep_hash_mapt::hash_container
irep_hash_containert hash_container
Definition: irep_hash_container.h:178
irep_hash_mapt::key_type
Key key_type
Definition: irep_hash_container.h:102
irep_hash_mapt
Definition: irep_hash_container.h:96
irep_hash_container_baset
Definition: irep_hash_container.h:20
irep_hash_container_baset::irep_entryt::number
std::size_t number
Definition: irep_hash_container.h:50
irep_full_hash_containert::irep_full_hash_containert
irep_full_hash_containert()
Definition: irep_hash_container.h:90
irep_hash_mapt::mapped_type
T mapped_type
Definition: irep_hash_container.h:103
irep_hash_container_baset::clear
void clear()
Definition: irep_hash_container.h:29
irep_hash_mapt::find
const_iterator find(const Key &key) const
Definition: irep_hash_container.h:108
irep_hash_mapt::mapt
std::map< std::size_t, T > mapt
Definition: irep_hash_container.h:99
irep_hash_container_baset::pointer_hasht
Definition: irep_hash_container.h:40
irep_hash_containert
Definition: irep_hash_container.h:76
numbering.h
irep_hash_mapt::size
std::size_t size() const
Definition: irep_hash_container.h:144
irep_hash_mapt::end
iterator end()
Definition: irep_hash_container.h:133
irep_hash_mapt::begin
iterator begin()
Definition: irep_hash_container.h:123
irep_hash_mapt::find
iterator find(const Key &key)
Definition: irep_hash_container.h:113
irep_hash_mapt::empty
bool empty() const
Definition: irep_hash_container.h:149
irep_hash_container_baset::vector_hasht
Definition: irep_hash_container.h:62
irep_hash_mapt::operator[]
T & operator[](const Key &key)
Definition: irep_hash_container.h:154
irep_hash_mapt::const_iterator
typename mapt::const_iterator const_iterator
Definition: irep_hash_container.h:105
irep_hash_container_baset::number
std::size_t number(const irept &irep)
Definition: irep_hash_container.cpp:17
irep_hash_mapt::insert
std::pair< iterator, bool > insert(const value_type &value)
Definition: irep_hash_container.h:160
irep_hash_container_baset::full
bool full
Definition: irep_hash_container.h:72
irep_hash_container_baset::numberingt
hash_numbering< packedt, vector_hasht > numberingt
Definition: irep_hash_container.h:67
irep_full_hash_containert
Definition: irep_hash_container.h:86
irept
Base class for tree-like data structures with sharing.
Definition: irep.h:156
irep_hash_containert::irep_hash_containert
irep_hash_containert()
Definition: irep_hash_container.h:80
template_numberingt::clear
void clear()
Definition: numbering.h:60
irep_hash_mapt::iterator
typename mapt::iterator iterator
Definition: irep_hash_container.h:106
irep_hash_mapt::erase
void erase(iterator it)
Definition: irep_hash_container.h:166
irep_hash_container_baset::ptr_hasht
std::unordered_map< const void *, irep_entryt, pointer_hasht > ptr_hasht
Definition: irep_hash_container.h:55
irep_hash_container_baset::irep_entryt
Definition: irep_hash_container.h:48
irep_hash_container_baset::irep_hash_container_baset
irep_hash_container_baset(bool _full)
Definition: irep_hash_container.h:25
irep_hash_container_baset::irep_entryt::irep
irept irep
Definition: irep_hash_container.h:51
irep.h
irep_hash_container_baset::ptr_hash
ptr_hasht ptr_hash
Definition: irep_hash_container.h:56