diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index 906365b97a8..16c3fad0c4f 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -181,10 +181,10 @@ unsigned custom_bitvector_analysist::get_bit_nr( else if(string_expr.id()==ID_string_constant) { irep_idt value=string_expr.get(ID_value); - return bits(value); + return bits.number(value); } else - return bits("(unknown)"); + return bits.number("(unknown)"); } std::set custom_bitvector_analysist::aliases( diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp index 4ed9d19cd21..0445d5a1596 100644 --- a/src/analyses/invariant_set.cpp +++ b/src/analyses/invariant_set.cpp @@ -52,7 +52,12 @@ bool inv_object_storet::get(const exprt &expr, unsigned &n) return false; } - return map.get_number(s, n); + if(const auto number = map.get_number(s)) + { + n = *number; + return false; + } + return true; } unsigned inv_object_storet::add(const exprt &expr) diff --git a/src/solvers/flattening/boolbv_constant.cpp b/src/solvers/flattening/boolbv_constant.cpp index 612cee9d63c..d7fcb497ce6 100644 --- a/src/solvers/flattening/boolbv_constant.cpp +++ b/src/solvers/flattening/boolbv_constant.cpp @@ -48,7 +48,7 @@ bvt boolbvt::convert_constant(const constant_exprt &expr) else if(expr_type.id()==ID_string) { // we use the numbering for strings - std::size_t number=string_numbering(expr.get_value()); + std::size_t number = string_numbering.number(expr.get_value()); return bv_utils.build_constant(number, bv.size()); } else if(expr_type.id()==ID_range) diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp index a0f86997e12..ff7c92abf94 100644 --- a/src/solvers/flattening/boolbv_get.cpp +++ b/src/solvers/flattening/boolbv_get.cpp @@ -330,13 +330,14 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const valuest values; { - std::size_t number; - - if(arrays.get_number(expr, number)) + const auto opt_num = arrays.get_number(expr); + if(!opt_num) + { return nil_exprt(); + } // get root - number=arrays.find_number(number); + const auto number = arrays.find_number(*opt_num); assert(number #include +#include -template -// NOLINTNEXTLINE(readability/identifiers) -class numbering final +/// \tparam Map a map from a key type to some numeric type +template +class template_numberingt final { public: - // NOLINTNEXTLINE(readability/identifiers) - typedef std::size_t number_type; + using number_type = typename Map::mapped_type; // NOLINT + using key_type = typename Map::key_type; // NOLINT private: - typedef std::vector data_typet; - data_typet data; - typedef std::map numberst; - numberst numbers; + using data_typet = std::vector; // NOLINT + data_typet data_; + Map numbers_; public: - // NOLINTNEXTLINE(readability/identifiers) - typedef typename data_typet::size_type size_type; - // NOLINTNEXTLINE(readability/identifiers) - typedef typename data_typet::iterator iterator; - // NOLINTNEXTLINE(readability/identifiers) - typedef typename data_typet::const_iterator const_iterator; - - number_type number(const T &a) + using size_type = typename data_typet::size_type; // NOLINT + using iterator = typename data_typet::iterator; // NOLINT + using const_iterator = typename data_typet::const_iterator; // NOLINT + + number_type number(const key_type &a) { - std::pair result= - numbers.insert( - std::pair - (a, number_type(numbers.size()))); + const auto result = numbers_.emplace(a, number_type(numbers_.size())); if(result.second) // inserted? { - data.push_back(a); - INVARIANT(data.size()==numbers.size(), "vector sizes must match"); + data_.emplace_back(a); + INVARIANT(data_.size() == numbers_.size(), "vector sizes must match"); } return (result.first)->second; } - number_type operator()(const T &a) + optionalt get_number(const key_type &a) const { - return number(a); + const auto it = numbers_.find(a); + if(it == numbers_.end()) + { + return {}; + } + return it->second; } - bool get_number(const T &a, number_type &n) const + void clear() { - typename numberst::const_iterator it=numbers.find(a); - - if(it==numbers.end()) - return true; - - n=it->second; - return false; + data_.clear(); + numbers_.clear(); } - void clear() + size_type size() const { - data.clear(); - numbers.clear(); + return data_.size(); } - size_t size() const { return data.size(); } - - T &operator[](size_type t) { return data[t]; } - const T &operator[](size_type t) const { return data[t]; } - - iterator begin() { return data.begin(); } - const_iterator begin() const { return data.begin(); } - const_iterator cbegin() const { return data.cbegin(); } - - iterator end() { return data.end(); } - const_iterator end() const { return data.end(); } - const_iterator cend() const { return data.cend(); } -}; - -template -// NOLINTNEXTLINE(readability/identifiers) -class hash_numbering final -{ -public: - // NOLINTNEXTLINE(readability/identifiers) - typedef unsigned int number_type; - -private: - typedef std::vector data_typet; - data_typet data; - typedef std::unordered_map numberst; - numberst numbers; - -public: - // NOLINTNEXTLINE(readability/identifiers) - typedef typename data_typet::size_type size_type; - // NOLINTNEXTLINE(readability/identifiers) - typedef typename data_typet::iterator iterator; - // NOLINTNEXTLINE(readability/identifiers) - typedef typename data_typet::const_iterator const_iterator; - - number_type number(const T &a) + key_type &operator[](size_type t) { - std::pair result= - numbers.insert( - std::pair - (a, number_type(numbers.size()))); - - if(result.second) // inserted? - { - this->push_back(a); - assert(this->size()==numbers.size()); - } - - return (result.first)->second; + return data_[t]; } - - bool get_number(const T &a, number_type &n) const + const key_type &operator[](size_type t) const { - typename numberst::const_iterator it=numbers.find(a); - - if(it==numbers.end()) - return true; - - n=it->second; - return false; + return data_[t]; } - void clear() + iterator begin() { - data.clear(); - numbers.clear(); + return data_.begin(); + } + const_iterator begin() const + { + return data_.begin(); + } + const_iterator cbegin() const + { + return data_.cbegin(); } - template - void push_back(U &&u) { data.push_back(std::forward(u)); } - - T &operator[](size_type t) { return data[t]; } - const T &operator[](size_type t) const { return data[t]; } - - T &at(size_type t) { return data.at(t); } - const T &at(size_type t) const { return data.at(t); } - - size_type size() const { return data.size(); } + iterator end() + { + return data_.end(); + } + const_iterator end() const + { + return data_.end(); + } + const_iterator cend() const + { + return data_.cend(); + } +}; - iterator begin() { return data.begin(); } - const_iterator begin() const { return data.begin(); } - const_iterator cbegin() const { return data.cbegin(); } +template +using numbering = template_numberingt>; // NOLINT - iterator end() { return data.end(); } - const_iterator end() const { return data.end(); } - const_iterator cend() const { return data.cend(); } -}; +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 42dd4738735..f871ad669c7 100644 --- a/src/util/union_find.h +++ b/src/util/union_find.h @@ -168,16 +168,14 @@ class union_find final // are 'a' and 'b' in the same set? bool same_set(const T &a, const T &b) const { - number_type na, nb; - bool have_na=!numbers.get_number(a, na), - have_nb=!numbers.get_number(b, nb); + const optionalt na = numbers.get_number(a); + const optionalt nb = numbers.get_number(a); - if(have_na && have_nb) - return uuf.same_set(na, nb); - else if(!have_na && !have_nb) + if(na && nb) + return uuf.same_set(*na, *nb); + if(!na && !nb) return a==b; - else - return false; + return false; } // are 'a' and 'b' in the same set? @@ -259,9 +257,9 @@ class union_find final uuf.isolate(number(a)); } - bool get_number(const T &a, number_type &n) const + optionalt get_number(const T &a) const { - return numbers.get_number(a, n); + return numbers.get_number(a); } size_t size() const { return numbers.size(); }