9 #ifndef CPROVER_UTIL_NUMBERING_H 10 #define CPROVER_UTIL_NUMBERING_H 13 #include <unordered_map> 20 template <
typename Map>
34 using iterator =
typename data_typet::iterator;
43 data_.emplace_back(a);
47 return (result.first)->second;
95 return data_.cbegin();
112 template <
typename Key>
115 template <
typename Key,
typename Hash>
119 #endif // CPROVER_UTIL_NUMBERING_H const_iterator cend() const
number_type number(const key_type &a)
unsignedbv_typet size_type()
const_iterator begin() const
#define INVARIANT(CONDITION, REASON)
optionalt< number_type > get_number(const key_type &a) const
const_iterator end() const
typename data_typet::size_type size_type
const key_type & at(size_type t) const
nonstd::optional< T > optionalt
key_type & operator[](size_type t)
typename data_typet::iterator iterator
const key_type & operator[](size_type t) const
typename exprt ::mapped_type number_type
typename data_typet::const_iterator const_iterator
std::vector< key_type > data_typet
typename exprt ::key_type key_type
const_iterator cbegin() const