1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
/*
* This file is part of the source code of the software program
* Vampire. It is protected by applicable
* copyright laws.
*
* This source code is distributed under the licence found here
* https://vprover.github.io/license.html
* and in the source directory
*/
/**
* @file Vector.hpp
* Defines a class of constant-size generic vectors. The size is given as an
* argument when we allocate the vector.
*
* @since 01/02/2008 Manchester
*/
#ifndef __Vector__
#define __Vector__
#include "Forwards.hpp"
#include "Debug/Assertion.hpp"
#include "Allocator.hpp"
namespace Indexing {
class CodeTree;
class ClauseCodeTree;
}
namespace Lib {
/**
* Class of constant size generic vectors. The size of a vector is fixed when it
* is allocated and cannot change, unlike that of arrays. Vectors of size 0 are
* not allowed.
* @since 01/02/2008 Manchester
*/
template<typename C>
class Vector
{
public:
/** Return a reference to the n-th element of the vector */
inline C& operator[] (size_t n)
{
ASS(n < _length);
return _array[n];
} // operator[]
/** Return a reference to the n-th element of the array */
inline const C& operator[](size_t n) const
{
ASS(n < _length);
return _array[n];
}
/** Return the length (the capacity) of the array */
size_t length() const { return _length; }
/** allocate a vector of the size @b length */
static Vector* allocate(size_t length)
{
ASS_G(length,0);
size_t sz=sizeof(Vector) + (length-1)*sizeof(C);
Vector* v = reinterpret_cast<Vector*>(ALLOC_KNOWN(sz,"Vector"));
v->_length = length;
C* arr = v->_array;
// in the case C is a class with an initialiser, apply the constructor of it
// to every element of the allocated array
array_new<C>(arr,length);
return v;
} // allocate
/** deallocate the vector */
void deallocate()
{
// in the case C is a class with an initialiser, apply the destructor of it
// to every element of the allocated array
array_delete(_array, _length);
size_t sz=sizeof(Vector) + (_length-1)*sizeof(C);
DEALLOC_KNOWN(this,sz,"Vector");
} // deallocate
bool operator==(const Vector& v) const
{
if(length()!=v.length()) {
return false;
}
size_t sz = length();
for(size_t i=0; i!=sz; ++i) {
if((*this)[i]!=v[i]) {
return false;
}
}
return true;
}
bool operator!=(const Vector& o) const
{ return !((*this)==o); }
/**
* Convert the vector to its string representation. To use this function,
* elements must have a toString() function too.
*/
std::string toString()
{
std::string res;
for(size_t i=0;i<_length;i++) {
if (i>0) {
res+=",";
}
res+=(*this)[i].toString();
}
return res;
} // toString
friend class Indexing::CodeTree;
friend class Indexing::ClauseCodeTree;
/**
* Iterator that deallocates the vector when it yields the last value.
*/
class DestructiveIterator
{
public:
DECL_ELEMENT_TYPE(C);
DestructiveIterator(Vector& v)
: cur(v._array), afterLast(v._array+v.length()), vec(&v)
{
if (cur==afterLast) {
vec->deallocate();
}
}
bool hasNext()
{
return cur!=afterLast;
}
C next()
{
ASS(hasNext());
C res=*cur;
cur++;
if (cur==afterLast) {
vec->deallocate();
}
return res;
}
private:
C* cur;
C* afterLast;
Vector* vec;
}; // Vector::DestructiveIterator
protected:
/** array's length */
size_t _length;
/** array's content */
C _array[1];
private:
/** declared but not defined to prevent its use */
void* operator new(size_t,size_t length);
/** not used, will cause an assertion violation */
void operator delete(void*)
{
ASSERTION_VIOLATION
}
/** declared but not defined to prevent its use */
Vector();
}; // class Vector
} // namespace Lib
#endif