cprover
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 <map>
13 #include <unordered_map>
14 #include <vector>
15 
16 #include "invariant.h"
17 #include "optional.h"
18 
20 template <typename Map>
22 {
23 public:
24  using number_type = typename Map::mapped_type; // NOLINT
25  using key_type = typename Map::key_type; // NOLINT
26 
27 private:
28  using data_typet = std::vector<key_type>; // NOLINT
30  Map 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 
51  {
52  const auto it = numbers_.find(a);
53  if(it == numbers_.end())
54  {
55  return {};
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 template <typename Key>
114 
115 template <typename Key, typename Hash>
116 using hash_numbering = // NOLINT
118 
119 #endif // CPROVER_UTIL_NUMBERING_H
template_numberingt< exprt >::size_type
typename data_typet::size_type size_type
Definition: numbering.h:33
template_numberingt::begin
iterator begin()
Definition: numbering.h:85
template_numberingt::numbers_
Map numbers_
Definition: numbering.h:30
template_numberingt::operator[]
key_type & operator[](size_type t)
Definition: numbering.h:76
optional.h
template_numberingt
Definition: numbering.h:22
template_numberingt::cbegin
const_iterator cbegin() const
Definition: numbering.h:93
template_numberingt< exprt >::iterator
typename data_typet::iterator iterator
Definition: numbering.h:34
template_numberingt::size
size_type size() const
Definition: numbering.h:66
template_numberingt::get_number
optionalt< number_type > get_number(const key_type &a) const
Definition: numbering.h:50
template_numberingt::number
number_type number(const key_type &a)
Definition: numbering.h:37
template_numberingt< exprt >::key_type
typename Map::key_type key_type
Definition: numbering.h:25
template_numberingt::end
iterator end()
Definition: numbering.h:98
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
template_numberingt< exprt >::number_type
typename Map::mapped_type number_type
Definition: numbering.h:24
template_numberingt::begin
const_iterator begin() const
Definition: numbering.h:89
template_numberingt::data_
data_typet data_
Definition: numbering.h:29
invariant.h
template_numberingt::at
const key_type & at(size_type t) const
Definition: numbering.h:71
template_numberingt::clear
void clear()
Definition: numbering.h:60
template_numberingt::operator[]
const key_type & operator[](size_type t) const
Definition: numbering.h:80
template_numberingt< exprt >::data_typet
std::vector< key_type > data_typet
Definition: numbering.h:28
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
template_numberingt::cend
const_iterator cend() const
Definition: numbering.h:106
template_numberingt::end
const_iterator end() const
Definition: numbering.h:102
template_numberingt< exprt >::const_iterator
typename data_typet::const_iterator const_iterator
Definition: numbering.h:35
validation_modet::INVARIANT
@ INVARIANT