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 
10 #ifndef CPROVER_UTIL_NUMBERING_H
11 #define CPROVER_UTIL_NUMBERING_H
12 
13 #include <cassert>
14 #include <map>
15 #include <unordered_map>
16 #include <vector>
17 
18 
19 template <typename T>
20 // NOLINTNEXTLINE(readability/identifiers)
21 class numbering:public std::vector<T>
22 {
23 public:
24  // NOLINTNEXTLINE(readability/identifiers)
25  typedef std::size_t number_type;
26 
27  number_type number(const T &a)
28  {
29  std::pair<typename numberst::const_iterator, bool> result=
30  numbers.insert(
31  std::pair<T, number_type>
32  (a, number_type(numbers.size())));
33 
34  if(result.second) // inserted?
35  {
36  this->push_back(a);
37  assert(this->size()==numbers.size());
38  }
39 
40  return (result.first)->second;
41  }
42 
43  number_type operator()(const T &a)
44  {
45  return number(a);
46  }
47 
48  bool get_number(const T &a, number_type &n) const
49  {
50  typename numberst::const_iterator it=numbers.find(a);
51 
52  if(it==numbers.end())
53  return true;
54 
55  n=it->second;
56  return false;
57  }
58 
59  void clear()
60  {
61  subt::clear();
62  numbers.clear();
63  }
64 
65 protected:
66  typedef std::vector<T> subt;
67 
68  typedef std::map<T, number_type> numberst;
69  numberst numbers;
70 };
71 
72 template <typename T, class hash_fkt>
73 // NOLINTNEXTLINE(readability/identifiers)
74 class hash_numbering:public std::vector<T>
75 {
76 public:
77  // NOLINTNEXTLINE(readability/identifiers)
78  typedef unsigned int number_type;
79 
80  number_type number(const T &a)
81  {
82  std::pair<typename numberst::const_iterator, bool> result=
83  numbers.insert(
84  std::pair<T, number_type>
85  (a, number_type(numbers.size())));
86 
87  if(result.second) // inserted?
88  {
89  this->push_back(a);
90  assert(this->size()==numbers.size());
91  }
92 
93  return (result.first)->second;
94  }
95 
96  bool get_number(const T &a, number_type &n) const
97  {
98  typename numberst::const_iterator it=numbers.find(a);
99 
100  if(it==numbers.end())
101  return true;
102 
103  n=it->second;
104  return false;
105  }
106 
107  void clear()
108  {
109  subt::clear();
110  numbers.clear();
111  }
112 
113 protected:
114  typedef std::vector<T> subt;
115 
116  typedef std::unordered_map<T, number_type, hash_fkt> numberst;
117  numberst numbers;
118 };
119 
120 #endif // CPROVER_UTIL_NUMBERING_H
void clear()
Definition: numbering.h:59
std::vector< T > subt
Definition: numbering.h:66
number_type operator()(const T &a)
Definition: numbering.h:43
numberst numbers
Definition: numbering.h:69
bool get_number(const T &a, number_type &n) const
Definition: numbering.h:96
bool get_number(const T &a, number_type &n) const
Definition: numbering.h:48
numberst numbers
Definition: numbering.h:117
std::map< T, number_type > numberst
Definition: numbering.h:68
std::size_t number_type
Definition: numbering.h:25
std::vector< T > subt
Definition: numbering.h:114
void clear()
Definition: numbering.h:107
number_type number(const T &a)
Definition: numbering.h:27
std::unordered_map< T, number_type, hash_fkt > numberst
Definition: numbering.h:116
unsigned int number_type
Definition: numbering.h:78
number_type number(const T &a)
Definition: numbering.h:80