cprover
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
;
24
underlyingt
underlying
;
25
uint64_t
_size
;
26
27
public
:
28
sparse_vectort
() :
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
typedef
typename
underlyingt::iterator
iteratort
;
55
typedef
typename
underlyingt::const_iterator
const_iteratort
;
56
57
iteratort
begin
() {
return
underlying
.begin(); }
58
const_iteratort
begin
()
const
{
return
underlying
.begin(); }
59
60
iteratort
end
() {
return
underlying
.end(); }
61
const_iteratort
end
()
const
{
return
underlying
.end(); }
62
63
const_iteratort
find
(uint64_t idx) {
return
underlying
.find(idx); }
64
};
65
66
#endif // CPROVER_UTIL_SPARSE_VECTOR_H
sparse_vectort::end
const_iteratort end() const
Definition:
sparse_vector.h:61
sparse_vectort
Definition:
sparse_vector.h:21
sparse_vectort::operator[]
const T & operator[](uint64_t idx) const
Definition:
sparse_vector.h:31
sparse_vectort::end
iteratort end()
Definition:
sparse_vector.h:60
sparse_vectort::size
uint64_t size() const
Definition:
sparse_vector.h:43
sparse_vectort::begin
const_iteratort begin() const
Definition:
sparse_vector.h:58
sparse_vectort::_size
uint64_t _size
Definition:
sparse_vector.h:25
sparse_vectort::begin
iteratort begin()
Definition:
sparse_vector.h:57
sparse_vectort::iteratort
underlyingt::iterator iteratort
Definition:
sparse_vector.h:54
sparse_vectort::const_iteratort
underlyingt::const_iterator const_iteratort
Definition:
sparse_vector.h:55
sparse_vectort::operator[]
T & operator[](uint64_t idx)
Definition:
sparse_vector.h:37
sparse_vectort::sparse_vectort
sparse_vectort()
Definition:
sparse_vector.h:28
sparse_vectort::resize
void resize(uint64_t new_size)
Definition:
sparse_vector.h:48
sparse_vectort::underlying
underlyingt underlying
Definition:
sparse_vector.h:24
sparse_vectort::underlyingt
std::map< uint64_t, T > underlyingt
Definition:
sparse_vector.h:23
invariant.h
sparse_vectort::find
const_iteratort find(uint64_t idx)
Definition:
sparse_vector.h:63
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition:
invariant.h:424
util
sparse_vector.h
Generated by
1.8.20