CBMC
numbering.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_NUMBERING_H
10 #define CPROVER_UTIL_NUMBERING_H
11 
12 #include "invariant.h"
13 
14 #include <optional>
15 #include <unordered_map>
16 #include <vector>
17 
20 template <typename keyt, typename hasht = std::hash<keyt>>
21 class numberingt final
22 {
23 public:
24  using number_type = std::size_t; // NOLINT
25  using key_type = keyt; // NOLINT
26 
27 private:
28  using data_typet = std::vector<key_type>; // NOLINT
30  std::unordered_map<keyt, number_type, hasht> numbers_;
31 
32 public:
33  using size_type = typename data_typet::size_type; // NOLINT
34  using iterator = typename data_typet::iterator; // NOLINT
35  using const_iterator = typename data_typet::const_iterator; // NOLINT
36 
38  {
39  const auto result = numbers_.emplace(a, number_type(numbers_.size()));
40 
41  if(result.second) // inserted?
42  {
43  data_.emplace_back(a);
44  INVARIANT(data_.size() == numbers_.size(), "vector sizes must match");
45  }
46 
47  return (result.first)->second;
48  }
49 
50  std::optional<number_type> get_number(const key_type &a) const
51  {
52  const auto it = numbers_.find(a);
53  if(it == numbers_.end())
54  {
55  return std::nullopt;
56  }
57  return it->second;
58  }
59 
60  void clear()
61  {
62  data_.clear();
63  numbers_.clear();
64  }
65 
66  size_type size() const
67  {
68  return data_.size();
69  }
70 
71  const key_type &at(size_type t) const
72  {
73  return data_.at(t);
74  }
75 
77  {
78  return data_[t];
79  }
80  const key_type &operator[](size_type t) const
81  {
82  return data_[t];
83  }
84 
86  {
87  return data_.begin();
88  }
90  {
91  return data_.begin();
92  }
94  {
95  return data_.cbegin();
96  }
97 
99  {
100  return data_.end();
101  }
103  {
104  return data_.end();
105  }
107  {
108  return data_.cend();
109  }
110 };
111 
112 
113 #endif // CPROVER_UTIL_NUMBERING_H
keyt key_type
Definition: numbering.h:25
number_type number(const key_type &a)
Definition: numbering.h:37
const key_type & operator[](size_type t) const
Definition: numbering.h:80
std::optional< number_type > get_number(const key_type &a) const
Definition: numbering.h:50
const_iterator cend() const
Definition: numbering.h:106
typename data_typet::size_type size_type
Definition: numbering.h:33
data_typet data_
Definition: numbering.h:29
key_type & operator[](size_type t)
Definition: numbering.h:76
const key_type & at(size_type t) const
Definition: numbering.h:71
size_type size() const
Definition: numbering.h:66
std::vector< key_type > data_typet
Definition: numbering.h:28
const_iterator begin() const
Definition: numbering.h:89
void clear()
Definition: numbering.h:60
iterator begin()
Definition: numbering.h:85
const_iterator end() const
Definition: numbering.h:102
iterator end()
Definition: numbering.h:98
std::unordered_map< keyt, number_type, hasht > numbers_
Definition: numbering.h:30
const_iterator cbegin() const
Definition: numbering.h:93
std::size_t number_type
Definition: numbering.h:24
typename data_typet::const_iterator const_iterator
Definition: numbering.h:35
typename data_typet::iterator iterator
Definition: numbering.h:34
#define size_type
Definition: unistd.c:347