1 |
|
/*******************************************************************************************[Vec.h] |
2 |
|
Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson |
3 |
|
Copyright (c) 2007-2010, Niklas Sorensson |
4 |
|
|
5 |
|
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and |
6 |
|
associated documentation files (the "Software"), to deal in the Software without restriction, |
7 |
|
including without limitation the rights to use, copy, modify, merge, publish, distribute, |
8 |
|
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is |
9 |
|
furnished to do so, subject to the following conditions: |
10 |
|
|
11 |
|
The above copyright notice and this permission notice shall be included in all copies or |
12 |
|
substantial portions of the Software. |
13 |
|
|
14 |
|
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT |
15 |
|
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND |
16 |
|
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, |
17 |
|
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT |
18 |
|
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. |
19 |
|
**************************************************************************************************/ |
20 |
|
|
21 |
|
#ifndef Minisat_Vec_h |
22 |
|
#define Minisat_Vec_h |
23 |
|
|
24 |
|
#include <new> |
25 |
|
|
26 |
|
#include "base/check.h" |
27 |
|
#include "prop/minisat/mtl/IntTypes.h" |
28 |
|
#include "prop/minisat/mtl/XAlloc.h" |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
namespace Minisat { |
32 |
|
|
33 |
|
//================================================================================================= |
34 |
|
// Automatically resizable arrays |
35 |
|
// |
36 |
|
// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc) |
37 |
|
|
38 |
|
template<class T> |
39 |
|
class vec { |
40 |
|
T* data; |
41 |
|
int sz; |
42 |
|
int cap; |
43 |
|
|
44 |
|
// Don't allow copying (error prone): |
45 |
|
vec<T>& operator=(vec<T>& other) |
46 |
|
{ |
47 |
|
Assert(0); |
48 |
|
return *this; |
49 |
|
} |
50 |
|
vec(vec<T>& other) { Assert(0); } |
51 |
|
|
52 |
|
// Helpers for calculating next capacity: |
53 |
16540212 |
static inline int imax (int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); } |
54 |
|
//static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; } |
55 |
|
static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; } |
56 |
|
|
57 |
|
public: |
58 |
|
// Constructors: |
59 |
13531108 |
vec() : data(NULL) , sz(0) , cap(0) { } |
60 |
13209 |
explicit vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); } |
61 |
9920 |
vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); } |
62 |
13554237 |
~vec() { clear(true); } |
63 |
|
|
64 |
|
// Pointer to first element: |
65 |
119301329 |
operator T* (void) { return data; } |
66 |
|
|
67 |
|
// Size operations: |
68 |
4829544654 |
int size (void) const { return sz; } |
69 |
137084117 |
void shrink(int nelems) |
70 |
|
{ |
71 |
137084117 |
Assert(nelems <= sz); |
72 |
137084117 |
for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); |
73 |
137084117 |
} |
74 |
|
void shrink_(int nelems) |
75 |
|
{ |
76 |
|
Assert(nelems <= sz); |
77 |
|
sz -= nelems; |
78 |
|
} |
79 |
|
int capacity (void) const { return cap; } |
80 |
|
void capacity (int min_cap); |
81 |
|
void growTo (int size); |
82 |
|
void growTo (int size, const T& pad); |
83 |
|
void clear (bool dealloc = false); |
84 |
|
|
85 |
|
// Stack interface: |
86 |
3731309 |
void push (void) { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; } |
87 |
381303712 |
void push (const T& elem) { if (sz == cap) capacity(sz+1); data[sz++] = elem; } |
88 |
116589264 |
void push_(const T& elem) |
89 |
|
{ |
90 |
116589264 |
Assert(sz < cap); |
91 |
116589264 |
data[sz++] = elem; |
92 |
116589264 |
} |
93 |
45673202 |
void pop(void) |
94 |
|
{ |
95 |
45673202 |
Assert(sz > 0); |
96 |
45673202 |
sz--, data[sz].~T(); |
97 |
45673202 |
} |
98 |
|
// NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but |
99 |
|
// in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not |
100 |
|
// happen given the way capacities are calculated (below). Essentially, all capacities are |
101 |
|
// even, but INT_MAX is odd. |
102 |
|
|
103 |
|
const T& last (void) const { return data[sz-1]; } |
104 |
48176620 |
T& last (void) { return data[sz-1]; } |
105 |
|
|
106 |
|
// Vector interface: |
107 |
3799407904 |
const T& operator [] (int index) const { return data[index]; } |
108 |
4425475081 |
T& operator [] (int index) { return data[index]; } |
109 |
|
|
110 |
|
// Duplication (preferred instead): |
111 |
6329117 |
void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; } |
112 |
3289 |
void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; } |
113 |
|
}; |
114 |
|
|
115 |
|
|
116 |
|
template<class T> |
117 |
28629363 |
void vec<T>::capacity(int min_cap) { |
118 |
28629363 |
if (cap >= min_cap) return; |
119 |
16540212 |
int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2 |
120 |
16540212 |
if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)) |
121 |
|
throw OutOfMemoryException(); |
122 |
|
} |
123 |
|
|
124 |
|
|
125 |
|
template<class T> |
126 |
9280672 |
void vec<T>::growTo(int size, const T& pad) { |
127 |
9280672 |
if (sz >= size) return; |
128 |
4126322 |
capacity(size); |
129 |
4126322 |
for (int i = sz; i < size; i++) data[i] = pad; |
130 |
4126322 |
sz = size; } |
131 |
|
|
132 |
|
|
133 |
|
template<class T> |
134 |
9093153 |
void vec<T>::growTo(int size) { |
135 |
9093153 |
if (sz >= size) return; |
136 |
9091938 |
capacity(size); |
137 |
9091938 |
for (int i = sz; i < size; i++) new (&data[i]) T(); |
138 |
9091938 |
sz = size; } |
139 |
|
|
140 |
|
|
141 |
|
template<class T> |
142 |
48070586 |
void vec<T>::clear(bool dealloc) { |
143 |
48070586 |
if (data != NULL){ |
144 |
41180329 |
for (int i = 0; i < sz; i++) data[i].~T(); |
145 |
41180329 |
sz = 0; |
146 |
41180329 |
if (dealloc) free(data), data = NULL, cap = 0; } } |
147 |
|
|
148 |
|
//================================================================================================= |
149 |
|
} |
150 |
|
} // namespace cvc5 |
151 |
|
|
152 |
|
#endif |