diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h index 511c3093833..1585b28159c 100644 --- a/src/analyses/custom_bitvector_analysis.h +++ b/src/analyses/custom_bitvector_analysis.h @@ -163,7 +163,7 @@ class custom_bitvector_analysist:public ait unsigned get_bit_nr(const exprt &); - typedef numbering bitst; + typedef numberingt bitst; bitst bits; protected: diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h index 7107fa310f5..fe7ab348cfc 100644 --- a/src/analyses/escape_analysis.h +++ b/src/analyses/escape_analysis.h @@ -120,7 +120,7 @@ class escape_analysist:public ait { } - numbering bits; + numberingt bits; void insert_cleanup( goto_functionst::goto_functiont &, diff --git a/src/analyses/invariant_set.h b/src/analyses/invariant_set.h index d26df7fe7d4..421bd153052 100644 --- a/src/analyses/invariant_set.h +++ b/src/analyses/invariant_set.h @@ -55,7 +55,7 @@ class inv_object_storet protected: const namespacet &ns; - typedef hash_numbering mapt; + typedef numberingt mapt; mapt map; struct entryt diff --git a/src/analyses/local_bitvector_analysis.h b/src/analyses/local_bitvector_analysis.h index e675ef5d876..3151a14e9eb 100644 --- a/src/analyses/local_bitvector_analysis.h +++ b/src/analyses/local_bitvector_analysis.h @@ -183,7 +183,7 @@ class local_bitvector_analysist typedef std::stack work_queuet; - numbering pointers; + numberingt pointers; // pointers -> flagst // This is a vector, so it's fast. diff --git a/src/analyses/local_may_alias.h b/src/analyses/local_may_alias.h index 307513a64eb..a07aaa8e586 100644 --- a/src/analyses/local_may_alias.h +++ b/src/analyses/local_may_alias.h @@ -60,7 +60,7 @@ class local_may_aliast typedef std::stack work_queuet; - mutable numbering objects; + mutable numberingt objects; typedef unsigned_union_find alias_sett; diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp index f14749c2433..d06308abd23 100644 --- a/src/goto-programs/vcd_goto_trace.cpp +++ b/src/goto-programs/vcd_goto_trace.cpp @@ -82,7 +82,7 @@ void output_vcd( // we first collect all variables that are assigned - numbering n; + numberingt n; for(const auto &step : goto_trace.steps) { diff --git a/src/pointer-analysis/object_numbering.h b/src/pointer-analysis/object_numbering.h index 4e51a68f8fc..0e0250d4856 100644 --- a/src/pointer-analysis/object_numbering.h +++ b/src/pointer-analysis/object_numbering.h @@ -25,6 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -typedef hash_numbering object_numberingt; +typedef numberingt object_numberingt; #endif // CPROVER_POINTER_ANALYSIS_OBJECT_NUMBERING_H diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index ce518c36442..eafb928a06a 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -29,7 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com const value_set_fit::object_map_dt value_set_fit::object_map_dt::blank{}; object_numberingt value_set_fit::object_numbering; -hash_numbering value_set_fit::function_numbering; +numberingt value_set_fit::function_numbering; static const char *alloc_adapter_prefix="alloc_adaptor::"; diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h index d96f4c0a80a..795d13d666f 100644 --- a/src/pointer-analysis/value_set_fi.h +++ b/src/pointer-analysis/value_set_fi.h @@ -39,7 +39,7 @@ class value_set_fit unsigned to_function, from_function; unsigned to_target_index, from_target_index; static object_numberingt object_numbering; - static hash_numbering function_numbering; + static numberingt function_numbering; void set_from(const irep_idt &function, unsigned inx) { diff --git a/src/pointer-analysis/value_set_fivr.h b/src/pointer-analysis/value_set_fivr.h index adb95534526..f37202df954 100644 --- a/src/pointer-analysis/value_set_fivr.h +++ b/src/pointer-analysis/value_set_fivr.h @@ -36,7 +36,7 @@ class value_set_fivrt unsigned to_function, from_function; unsigned to_target_index, from_target_index; static object_numberingt object_numbering; - static hash_numbering function_numbering; + static numberingt function_numbering; void set_from(const irep_idt &function, unsigned inx) { diff --git a/src/pointer-analysis/value_set_fivrns.h b/src/pointer-analysis/value_set_fivrns.h index d89196e68a9..b9c628d9a6f 100644 --- a/src/pointer-analysis/value_set_fivrns.h +++ b/src/pointer-analysis/value_set_fivrns.h @@ -37,7 +37,7 @@ class value_set_fivrnst unsigned to_function, from_function; unsigned to_target_index, from_target_index; static object_numberingt object_numbering; - static hash_numbering function_numbering; + static numberingt function_numbering; void set_from(const irep_idt &function, unsigned inx) { diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h index b556c76b1d2..9a74d66dd65 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -68,7 +68,7 @@ class arrayst:public equalityt array_equalitiest array_equalities; // this is used to find the clusters of arrays being compared - union_find arrays; + union_find arrays; // this tracks the array indicies for each array typedef std::set index_sett; diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 28f4245a270..ad2ebf26b2f 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -262,7 +262,7 @@ class boolbvt:public arrayst offset_mapt build_offset_map(const struct_typet &src); // strings - numbering string_numbering; + numberingt string_numbering; }; #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H diff --git a/src/solvers/flattening/pointer_logic.h b/src/solvers/flattening/pointer_logic.h index 5e9636ce08f..8736c4ae28c 100644 --- a/src/solvers/flattening/pointer_logic.h +++ b/src/solvers/flattening/pointer_logic.h @@ -23,7 +23,7 @@ class pointer_logict { public: // this numbers the objects - hash_numbering objects; + numberingt objects; struct pointert { diff --git a/src/util/irep_hash_container.h b/src/util/irep_hash_container.h index 58c64525d7f..3ece8bf4587 100644 --- a/src/util/irep_hash_container.h +++ b/src/util/irep_hash_container.h @@ -69,8 +69,7 @@ class irep_hash_container_baset std::size_t operator()(const packedt &p) const; }; - typedef hash_numbering numberingt; - numberingt numbering; + numberingt numbering; void pack(const irept &irep, packedt &); diff --git a/src/util/numbering.h b/src/util/numbering.h index b658bc299c3..ea9fc6e94eb 100644 --- a/src/util/numbering.h +++ b/src/util/numbering.h @@ -9,25 +9,25 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_NUMBERING_H #define CPROVER_UTIL_NUMBERING_H -#include #include #include #include "invariant.h" #include "optional.h" -/// \tparam Map: a map from a key type to some numeric type -template -class template_numberingt final +/// \tparam keyt: The type of keys which will be numbered. +/// \tparam hasht: The type of hashing functor used to hash keys. +template > +class numberingt final { public: - using number_type = typename Map::mapped_type; // NOLINT - using key_type = typename Map::key_type; // NOLINT + using number_type = std::size_t; // NOLINT + using key_type = keyt; // NOLINT private: using data_typet = std::vector; // NOLINT data_typet data_; - Map numbers_; + std::unordered_map numbers_; public: using size_type = typename data_typet::size_type; // NOLINT @@ -109,11 +109,5 @@ class template_numberingt final } }; -template -using numbering = template_numberingt>; // NOLINT - -template -using hash_numbering = // NOLINT - template_numberingt>; #endif // CPROVER_UTIL_NUMBERING_H diff --git a/src/util/union_find.h b/src/util/union_find.h index b71422bad58..81bac4b2740 100644 --- a/src/util/union_find.h +++ b/src/util/union_find.h @@ -132,23 +132,25 @@ class unsigned_union_find size_type get_other(size_type a); }; -template +/// \tparam T: The type of values stored. +/// \tparam hasht: The type of hash used for looking up the value numbering. +template > // NOLINTNEXTLINE(readability/identifiers) class union_find final { - typedef numbering numbering_typet; + using numbering_typet = numberingt; numbering_typet numbers; // NOLINTNEXTLINE(readability/identifiers) - typedef typename numbering_typet::number_type number_type; + using number_type = typename numbering_typet::number_type; public: // NOLINTNEXTLINE(readability/identifiers) - typedef typename numbering_typet::size_type size_type; + using size_type = typename numbering_typet::size_type; // NOLINTNEXTLINE(readability/identifiers) - typedef typename numbering_typet::iterator iterator; + using iterator = typename numbering_typet::iterator; // NOLINTNEXTLINE(readability/identifiers) - typedef typename numbering_typet::const_iterator const_iterator; + using const_iterator = typename numbering_typet::const_iterator; // true == already in same set bool make_union(const T &a, const T &b) @@ -160,8 +162,7 @@ class union_find final } // true == already in same set - bool make_union(typename numbering::const_iterator it_a, - typename numbering::const_iterator it_b) + bool make_union(const_iterator it_a, const_iterator it_b) { size_type na=it_a-numbers.begin(), nb=it_b-numbers.begin(); bool is_union=find_number(na)==find_number(nb); @@ -183,13 +184,12 @@ class union_find final } // are 'a' and 'b' in the same set? - bool same_set(typename numbering::const_iterator it_a, - typename numbering::const_iterator it_b) const + bool same_set(const_iterator it_a, const_iterator it_b) const { return uuf.same_set(it_a-numbers.begin(), it_b-numbers.begin()); } - const T &find(typename numbering::const_iterator it) const + const T &find(const_iterator it) const { return numbers[find_number(it-numbers.begin())]; } @@ -199,7 +199,7 @@ class union_find final return numbers[find_number(number(a))]; } - size_type find_number(typename numbering::const_iterator it) const + size_type find_number(const_iterator it) const { return find_number(it-numbers.begin()); } @@ -228,7 +228,7 @@ class union_find final return uuf.is_root(na); } - bool is_root(typename numbering::const_iterator it) const + bool is_root(const_iterator it) const { return uuf.is_root(it-numbers.begin()); } @@ -251,7 +251,7 @@ class union_find final uuf.clear(); } - void isolate(typename numbering::const_iterator it) + void isolate(const_iterator it) { uuf.isolate(it-numbers.begin()); } @@ -281,7 +281,7 @@ class union_find final protected: unsigned_union_find uuf; - typedef numbering subt; + using subt = numbering_typet; }; #endif // CPROVER_UTIL_UNION_FIND_H