Skip to content

Commit 2e62c66

Browse files
New class for sparse vectors in util
Sparse vectors represent a 2^64 sized space while allocating only space that is used.
1 parent fd96acc commit 2e62c66

File tree

1 file changed

+60
-0
lines changed

1 file changed

+60
-0
lines changed

src/util/sparse_vector.h

+60
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
/*******************************************************************\
2+
3+
Module: Sparse Vectors
4+
5+
Author: Romain Brenguier
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_UTIL_SPARSE_VECTOR_H
10+
#define CPROVER_UTIL_SPARSE_VECTOR_H
11+
12+
#include<cstdint>
13+
14+
template<class T> class sparse_vectort
15+
{
16+
protected:
17+
typedef std::map<uint64_t, T> underlyingt;
18+
underlyingt underlying;
19+
uint64_t _size;
20+
21+
public:
22+
sparse_vectort() :
23+
_size(0) {}
24+
25+
const T &operator[](uint64_t idx) const
26+
{
27+
assert(idx<_size && "index out of range");
28+
return underlying[idx];
29+
}
30+
31+
T &operator[](uint64_t idx)
32+
{
33+
assert(idx<_size && "index out of range");
34+
return underlying[idx];
35+
}
36+
37+
uint64_t size() const
38+
{
39+
return _size;
40+
}
41+
42+
void resize(uint64_t new_size)
43+
{
44+
assert(new_size>=_size && "sparse vector can't be shrunk (yet)");
45+
_size=new_size;
46+
}
47+
48+
typedef typename underlyingt::iterator iteratort;
49+
typedef typename underlyingt::const_iterator const_iteratort;
50+
51+
iteratort begin() { return underlying.begin(); }
52+
const_iteratort begin() const { return underlying.begin(); }
53+
54+
iteratort end() { return underlying.end(); }
55+
const_iteratort end() const { return underlying.end(); }
56+
57+
const_iteratort find(uint64_t idx) { return underlying.find(idx); }
58+
};
59+
60+
#endif // CPROVER_UTIL_SPARSE_VECTOR_H

0 commit comments

Comments
 (0)