CBMC
sparse_vector.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Sparse Vectors
4 
5 Author: Romain Brenguier
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_SPARSE_VECTOR_H
13 #define CPROVER_UTIL_SPARSE_VECTOR_H
14 
15 #include "invariant.h"
16 
17 #include <cstdint>
18 #include <map>
19 
20 template<class T> class sparse_vectort
21 {
22 protected:
23  typedef std::map<uint64_t, T> underlyingt;
25  uint64_t _size;
26 
27 public:
29  _size(0) {}
30 
31  const T &operator[](uint64_t idx) const
32  {
33  INVARIANT(idx<_size, "index out of range");
34  return underlying[idx];
35  }
36 
37  T &operator[](uint64_t idx)
38  {
39  INVARIANT(idx<_size, "index out of range");
40  return underlying[idx];
41  }
42 
43  uint64_t size() const
44  {
45  return _size;
46  }
47 
48  void resize(uint64_t new_size)
49  {
50  INVARIANT(new_size>=_size, "sparse vector can't be shrunk (yet)");
51  _size=new_size;
52  }
53 
54  void clear()
55  {
56  underlying.clear();
57  _size = 0;
58  }
59 
60  typedef typename underlyingt::iterator iteratort;
61  typedef typename underlyingt::const_iterator const_iteratort;
62 
63  iteratort begin() { return underlying.begin(); }
64  const_iteratort begin() const { return underlying.begin(); }
65 
66  iteratort end() { return underlying.end(); }
67  const_iteratort end() const { return underlying.end(); }
68 
69  const_iteratort find(uint64_t idx) { return underlying.find(idx); }
70 };
71 
72 #endif // CPROVER_UTIL_SPARSE_VECTOR_H
uint64_t _size
Definition: sparse_vector.h:25
const_iteratort find(uint64_t idx)
Definition: sparse_vector.h:69
const_iteratort begin() const
Definition: sparse_vector.h:64
void resize(uint64_t new_size)
Definition: sparse_vector.h:48
const T & operator[](uint64_t idx) const
Definition: sparse_vector.h:31
T & operator[](uint64_t idx)
Definition: sparse_vector.h:37
underlyingt underlying
Definition: sparse_vector.h:24
iteratort begin()
Definition: sparse_vector.h:63
underlyingt::iterator iteratort
Definition: sparse_vector.h:60
const_iteratort end() const
Definition: sparse_vector.h:67
iteratort end()
Definition: sparse_vector.h:66
underlyingt::const_iterator const_iteratort
Definition: sparse_vector.h:61
uint64_t size() const
Definition: sparse_vector.h:43
std::map< uint64_t, T > underlyingt
Definition: sparse_vector.h:23