CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
irep_hash_container.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: IREP Hash Container
4
5Author: 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{
23public:
24 std::size_t number(const irept &irep);
25
27 {
28 }
29
30 void clear()
31 {
33 }
34
35protected:
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
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)
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
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
89
90// includes comments
99
100template <typename Key, typename T>
102{
103protected:
104 using mapt = std::map<std::size_t, T>;
105
106public:
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
114 {
115 return map.find(hash_container.number(key));
116 }
117
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
172 {
173 map.erase(it);
174 }
175
177 {
178 std::swap(hash_container, other.hash_container);
179 std::swap(map, other.map);
180 }
181
182protected:
185};
186
187#endif // CPROVER_UTIL_IREP_HASH_CONTAINER_H
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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::size_t size() const
std::pair< const Key, T > value_type
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
T & operator[](const Key &key)
void swap(irep_hash_mapt< Key, T > &other)
typename mapt::const_iterator const_iterator
std::pair< iterator, bool > insert(const value_type &value)
void erase(iterator it)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
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