@@ -27,9 +27,9 @@ class numbering final
27
27
28
28
private:
29
29
using data_typet = std::vector<T>; // NOLINT
30
- data_typet data ;
30
+ data_typet data_ ;
31
31
using numberst = std::map<T, number_type>; // NOLINT
32
- numberst numbers ;
32
+ numberst numbers_ ;
33
33
34
34
public:
35
35
using size_type = typename data_typet::size_type; // NOLINT
@@ -38,15 +38,13 @@ class numbering final
38
38
39
39
number_type number (const T &a)
40
40
{
41
- std::pair<typename numberst::const_iterator, bool > result=
42
- numbers.insert (
43
- std::pair<T, number_type>
44
- (a, number_type (numbers.size ())));
41
+ std::pair<typename numberst::const_iterator, bool > result = numbers_.insert (
42
+ std::pair<T, number_type>(a, number_type (numbers_.size ())));
45
43
46
44
if (result.second ) // inserted?
47
45
{
48
- data .push_back (a);
49
- INVARIANT (data .size ()==numbers .size (), " vector sizes must match" );
46
+ data_ .push_back (a);
47
+ INVARIANT (data_ .size () == numbers_ .size (), " vector sizes must match" );
50
48
}
51
49
52
50
return (result.first )->second ;
@@ -59,8 +57,8 @@ class numbering final
59
57
60
58
optionalt<number_type> get_number (const T &a) const
61
59
{
62
- const auto it = numbers .find (a);
63
- if (it == numbers .end ())
60
+ const auto it = numbers_ .find (a);
61
+ if (it == numbers_ .end ())
64
62
{
65
63
return {};
66
64
}
@@ -69,22 +67,49 @@ class numbering final
69
67
70
68
void clear ()
71
69
{
72
- data .clear ();
73
- numbers .clear ();
70
+ data_ .clear ();
71
+ numbers_ .clear ();
74
72
}
75
73
76
- size_t size () const { return data.size (); }
74
+ size_t size () const
75
+ {
76
+ return data_.size ();
77
+ }
77
78
78
- T &operator [](size_type t) { return data[t]; }
79
- const T &operator [](size_type t) const { return data[t]; }
79
+ T &operator [](size_type t)
80
+ {
81
+ return data_[t];
82
+ }
83
+ const T &operator [](size_type t) const
84
+ {
85
+ return data_[t];
86
+ }
80
87
81
- iterator begin () { return data.begin (); }
82
- const_iterator begin () const { return data.begin (); }
83
- const_iterator cbegin () const { return data.cbegin (); }
88
+ iterator begin ()
89
+ {
90
+ return data_.begin ();
91
+ }
92
+ const_iterator begin () const
93
+ {
94
+ return data_.begin ();
95
+ }
96
+ const_iterator cbegin () const
97
+ {
98
+ return data_.cbegin ();
99
+ }
84
100
85
- iterator end () { return data.end (); }
86
- const_iterator end () const { return data.end (); }
87
- const_iterator cend () const { return data.cend (); }
101
+ iterator end ()
102
+ {
103
+ return data_.end ();
104
+ }
105
+ const_iterator end () const
106
+ {
107
+ return data_.end ();
108
+ }
109
+ const_iterator cend () const
110
+ {
111
+ return data_.cend ();
112
+ }
88
113
};
89
114
90
115
template <typename T, class hash_fkt >
@@ -96,9 +121,9 @@ class hash_numbering final
96
121
97
122
private:
98
123
using data_typet = std::vector<T>; // NOLINT
99
- data_typet data ;
124
+ data_typet data_ ;
100
125
using numberst = std::unordered_map<T, number_type, hash_fkt>; // NOLINT
101
- numberst numbers ;
126
+ numberst numbers_ ;
102
127
103
128
public:
104
129
using size_type = typename data_typet::size_type; // NOLINT
@@ -107,25 +132,23 @@ class hash_numbering final
107
132
108
133
number_type number (const T &a)
109
134
{
110
- std::pair<typename numberst::const_iterator, bool > result=
111
- numbers.insert (
112
- std::pair<T, number_type>
113
- (a, number_type (numbers.size ())));
135
+ std::pair<typename numberst::const_iterator, bool > result = numbers_.insert (
136
+ std::pair<T, number_type>(a, number_type (numbers_.size ())));
114
137
115
138
if (result.second ) // inserted?
116
139
{
117
140
this ->push_back (a);
118
- assert (this ->size ()==numbers .size ());
141
+ assert (this ->size () == numbers_ .size ());
119
142
}
120
143
121
144
return (result.first )->second ;
122
145
}
123
146
124
147
optionalt<number_type> get_number (const T &a) const
125
148
{
126
- const auto it = numbers .find (a);
149
+ const auto it = numbers_ .find (a);
127
150
128
- if (it == numbers .end ())
151
+ if (it == numbers_ .end ())
129
152
{
130
153
return {};
131
154
}
@@ -134,28 +157,64 @@ class hash_numbering final
134
157
135
158
void clear ()
136
159
{
137
- data .clear ();
138
- numbers .clear ();
160
+ data_ .clear ();
161
+ numbers_ .clear ();
139
162
}
140
163
141
164
template <typename U>
142
- void push_back (U &&u) { data.push_back (std::forward<U>(u)); }
165
+ void push_back (U &&u)
166
+ {
167
+ data_.push_back (std::forward<U>(u));
168
+ }
143
169
144
- T &operator [](size_type t) { return data[t]; }
145
- const T &operator [](size_type t) const { return data[t]; }
170
+ T &operator [](size_type t)
171
+ {
172
+ return data_[t];
173
+ }
174
+ const T &operator [](size_type t) const
175
+ {
176
+ return data_[t];
177
+ }
146
178
147
- T &at (size_type t) { return data.at (t); }
148
- const T &at (size_type t) const { return data.at (t); }
179
+ T &at (size_type t)
180
+ {
181
+ return data_.at (t);
182
+ }
183
+ const T &at (size_type t) const
184
+ {
185
+ return data_.at (t);
186
+ }
149
187
150
- size_type size () const { return data.size (); }
188
+ size_type size () const
189
+ {
190
+ return data_.size ();
191
+ }
151
192
152
- iterator begin () { return data.begin (); }
153
- const_iterator begin () const { return data.begin (); }
154
- const_iterator cbegin () const { return data.cbegin (); }
193
+ iterator begin ()
194
+ {
195
+ return data_.begin ();
196
+ }
197
+ const_iterator begin () const
198
+ {
199
+ return data_.begin ();
200
+ }
201
+ const_iterator cbegin () const
202
+ {
203
+ return data_.cbegin ();
204
+ }
155
205
156
- iterator end () { return data.end (); }
157
- const_iterator end () const { return data.end (); }
158
- const_iterator cend () const { return data.cend (); }
206
+ iterator end ()
207
+ {
208
+ return data_.end ();
209
+ }
210
+ const_iterator end () const
211
+ {
212
+ return data_.end ();
213
+ }
214
+ const_iterator cend () const
215
+ {
216
+ return data_.cend ();
217
+ }
159
218
};
160
219
161
220
#endif // CPROVER_UTIL_NUMBERING_H
0 commit comments