Skip to content

Commit d3f5cda

Browse files
committed
Use numberingt in place of numbering
Because the naming follows our coding standards and it reduces the number of numbering variations to maintain. This does change the type of backing container used in these places, however the performance should be at least equivalent.
1 parent 30957a4 commit d3f5cda

File tree

8 files changed

+7
-11
lines changed

8 files changed

+7
-11
lines changed

src/analyses/custom_bitvector_analysis.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -163,7 +163,7 @@ class custom_bitvector_analysist:public ait<custom_bitvector_domaint>
163163

164164
unsigned get_bit_nr(const exprt &);
165165

166-
typedef numbering<irep_idt> bitst;
166+
typedef numberingt<irep_idt> bitst;
167167
bitst bits;
168168

169169
protected:

src/analyses/escape_analysis.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -120,7 +120,7 @@ class escape_analysist:public ait<escape_domaint>
120120
{
121121
}
122122

123-
numbering<irep_idt> bits;
123+
numberingt<irep_idt> bits;
124124

125125
void insert_cleanup(
126126
goto_functionst::goto_functiont &,

src/analyses/invariant_set.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ class inv_object_storet
5555
protected:
5656
const namespacet &ns;
5757

58-
typedef numbering<irep_idt> mapt;
58+
typedef numberingt<irep_idt> mapt;
5959
mapt map;
6060

6161
struct entryt

src/analyses/local_bitvector_analysis.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,7 @@ class local_bitvector_analysist
183183

184184
typedef std::stack<unsigned> work_queuet;
185185

186-
numbering<irep_idt> pointers;
186+
numberingt<irep_idt> pointers;
187187

188188
// pointers -> flagst
189189
// This is a vector, so it's fast.

src/analyses/local_may_alias.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ class local_may_aliast
6060

6161
typedef std::stack<local_cfgt::node_nrt> work_queuet;
6262

63-
mutable numbering<exprt> objects;
63+
mutable numberingt<exprt, irep_hash> objects;
6464

6565
typedef unsigned_union_find alias_sett;
6666

src/goto-programs/vcd_goto_trace.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@ void output_vcd(
8282

8383
// we first collect all variables that are assigned
8484

85-
numbering<irep_idt> n;
85+
numberingt<irep_idt> n;
8686

8787
for(const auto &step : goto_trace.steps)
8888
{

src/solvers/flattening/boolbv.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -262,7 +262,7 @@ class boolbvt:public arrayst
262262
offset_mapt build_offset_map(const struct_typet &src);
263263

264264
// strings
265-
numbering<irep_idt> string_numbering;
265+
numberingt<irep_idt> string_numbering;
266266
};
267267

268268
#endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H

src/util/numbering.h

-4
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@ Author: Daniel Kroening, [email protected]
99
#ifndef CPROVER_UTIL_NUMBERING_H
1010
#define CPROVER_UTIL_NUMBERING_H
1111

12-
#include <map>
1312
#include <unordered_map>
1413
#include <vector>
1514

@@ -109,9 +108,6 @@ class template_numberingt final
109108
}
110109
};
111110

112-
template <typename Key>
113-
using numbering = template_numberingt<std::map<Key, std::size_t>>; // NOLINT
114-
115111
/// \tparam keyt: The type of keys which will be numbered.
116112
/// \tparam hasht: The type of hashing functor used to hash keys.
117113
template <typename keyt, typename hasht = std::hash<keyt>>

0 commit comments

Comments
 (0)