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 BVMinisat_Vec_h |
22 |
|
#define BVMinisat_Vec_h |
23 |
|
|
24 |
|
#include <new> |
25 |
|
|
26 |
|
#include "base/check.h" |
27 |
|
#include "prop/bvminisat/mtl/IntTypes.h" |
28 |
|
#include "prop/bvminisat/mtl/XAlloc.h" |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
namespace BVMinisat { |
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 |
54092 |
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 |
11894 |
vec() : data(NULL) , sz(0) , cap(0) { } |
60 |
30 |
explicit vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); } |
61 |
2 |
vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); } |
62 |
11926 |
~vec() { clear(true); } |
63 |
|
|
64 |
|
// Pointer to first element: |
65 |
6158 |
operator T* (void) { return data; } |
66 |
|
|
67 |
|
// Size operations: |
68 |
198024 |
int size (void) const { return sz; } |
69 |
6088 |
void shrink(int nelems) |
70 |
|
{ |
71 |
6088 |
Assert(nelems <= sz); |
72 |
6088 |
for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); |
73 |
6088 |
} |
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 |
458 |
void push (void) { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; } |
87 |
201890 |
void push (const T& elem) { if (sz == cap) capacity(sz+1); data[sz++] = elem; } |
88 |
3282 |
void push_(const T& elem) |
89 |
|
{ |
90 |
3282 |
Assert(sz < cap); |
91 |
3282 |
data[sz++] = elem; |
92 |
3282 |
} |
93 |
2370 |
void pop(void) |
94 |
|
{ |
95 |
2370 |
Assert(sz > 0); |
96 |
2370 |
sz--, data[sz].~T(); |
97 |
2370 |
} |
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 |
3370 |
T& last (void) { return data[sz-1]; } |
105 |
|
|
106 |
|
// Vector interface: |
107 |
192740 |
const T& operator [] (int index) const { return data[index]; } |
108 |
356178 |
T& operator [] (int index) { return data[index]; } |
109 |
|
|
110 |
|
// Duplicatation (preferred instead): |
111 |
1008 |
void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; } |
112 |
28 |
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 |
57516 |
void vec<T>::capacity(int min_cap) { |
118 |
57516 |
if (cap >= min_cap) return; |
119 |
54092 |
int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2 |
120 |
54092 |
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 |
3212 |
void vec<T>::growTo(int size, const T& pad) { |
127 |
3212 |
if (sz >= size) return; |
128 |
1428 |
capacity(size); |
129 |
1428 |
for (int i = sz; i < size; i++) data[i] = pad; |
130 |
1428 |
sz = size; } |
131 |
|
|
132 |
|
|
133 |
|
template<class T> |
134 |
1896 |
void vec<T>::growTo(int size) { |
135 |
1896 |
if (sz >= size) return; |
136 |
1896 |
capacity(size); |
137 |
1896 |
for (int i = sz; i < size; i++) new (&data[i]) T(); |
138 |
1896 |
sz = size; } |
139 |
|
|
140 |
|
|
141 |
|
template<class T> |
142 |
15152 |
void vec<T>::clear(bool dealloc) { |
143 |
15152 |
if (data != NULL){ |
144 |
14948 |
for (int i = 0; i < sz; i++) data[i].~T(); |
145 |
14948 |
sz = 0; |
146 |
14948 |
if (dealloc) free(data), data = NULL, cap = 0; } } |
147 |
|
|
148 |
|
//================================================================================================= |
149 |
|
} // namespace BVMinisat |
150 |
|
} // namespace cvc5 |
151 |
|
|
152 |
|
#endif |