Branch data Line data Source code
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
6 : : this software and associated documentation files (the "Software"), to deal in
7 : : the Software without restriction, including without limitation the rights to
8 : : use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
9 : : the Software, and to permit persons to whom the Software is furnished to do so,
10 : : subject to the following conditions:
11 : :
12 : : The above copyright notice and this permission notice shall be included in all
13 : : copies or substantial portions of the Software.
14 : :
15 : : THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16 : : IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
17 : : FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
18 : : COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
19 : : IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
20 : : CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
21 : : **************************************************************************************************/
22 : :
23 : : #ifndef Minisat_Vec_h
24 : : #define Minisat_Vec_h
25 : :
26 : : #include <new>
27 : :
28 : : #include "base/check.h"
29 : : #include "prop/minisat/mtl/IntTypes.h"
30 : : #include "prop/minisat/mtl/XAlloc.h"
31 : :
32 : : namespace cvc5::internal {
33 : : namespace Minisat {
34 : :
35 : : //=================================================================================================
36 : : // Automatically resizable arrays
37 : : //
38 : : // NOTE! Don't use this vector on datatypes that cannot be re-located in memory
39 : : // (with realloc)
40 : :
41 : : template <class T>
42 : : class vec
43 : : {
44 : : T* data;
45 : : int sz;
46 : : int cap;
47 : :
48 : : // Helpers for calculating next capacity:
49 : 30496135 : static inline int imax(int x, int y)
50 : : {
51 : 30496135 : int mask = (y - x) >> (sizeof(int) * 8 - 1);
52 : 30496135 : return (x & mask) + (y & (~mask));
53 : : }
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 : 28958254 : vec() : data(nullptr), sz(0), cap(0) {}
60 : 60972 : explicit vec(int size) : data(nullptr), sz(0), cap(0) { growTo(size); }
61 : 51874 : vec(int size, const T& pad) : data(nullptr), sz(0), cap(0)
62 : : {
63 : 51874 : growTo(size, pad);
64 : 51874 : }
65 : 29054816 : ~vec() { clear(true); }
66 : :
67 : : // Don't allow copying (error prone):
68 : : vec(const vec<T>&) = delete;
69 : : vec<T>& operator=(const vec<T>&) = delete;
70 : :
71 : : // Pointer to first element:
72 : 149127379 : operator T*(void) { return data; }
73 : :
74 : : // Size operations:
75 : 7263906330 : int size(void) const { return sz; }
76 : 154875957 : void shrink(int nelems)
77 : : {
78 [ - + ][ - + ]: 154875957 : Assert(nelems <= sz);
[ - - ]
79 [ + + ]: 635350407 : for (int i = 0; i < nelems; i++) sz--, data[sz].~T();
80 : 154875957 : }
81 : : void shrink_(int nelems)
82 : : {
83 : : Assert(nelems <= sz);
84 : : sz -= nelems;
85 : : }
86 : 0 : int capacity(void) const { return cap; }
87 : : void capacity(int min_cap);
88 : : void growTo(int size);
89 : : void growTo(int size, const T& pad);
90 : : void clear(bool dealloc = false);
91 : :
92 : : // Stack interface:
93 : 7302581 : void push(void)
94 : : {
95 [ + + ]: 7302581 : if (sz == cap) capacity(sz + 1);
96 : 7302581 : new (&data[sz]) T();
97 : 7302581 : sz++;
98 : 7302581 : }
99 : 521660257 : void push(const T& elem)
100 : : {
101 [ + + ]: 521660257 : if (sz == cap) capacity(sz + 1);
102 : 521660257 : data[sz++] = elem;
103 : 521660257 : }
104 : 147497001 : void push_(const T& elem)
105 : : {
106 [ - + ][ - + ]: 147497001 : Assert(sz < cap);
[ - - ]
107 : 147497001 : data[sz++] = elem;
108 : 147497001 : }
109 : 52548591 : void pop(void)
110 : : {
111 [ - + ][ - + ]: 52548591 : Assert(sz > 0);
[ - - ]
112 : 52548591 : sz--, data[sz].~T();
113 : 52548591 : }
114 : : // NOTE: it seems possible that overflow can happen in the 'sz+1' expression
115 : : // of 'push()', but in fact it can not since it requires that 'cap' is equal
116 : : // to INT_MAX. This in turn can not happen given the way capacities are
117 : : // calculated (below). Essentially, all capacities are even, but INT_MAX is
118 : : // odd.
119 : :
120 : : const T& last(void) const { return data[sz - 1]; }
121 : 57046791 : T& last(void) { return data[sz - 1]; }
122 : :
123 : : // Vector interface:
124 : 6150132007 : const T& operator[](int index) const { return data[index]; }
125 : 5348895269 : T& operator[](int index) { return data[index]; }
126 : :
127 : : // Duplication (preferred instead):
128 : 11210365 : void copyTo(vec<T>& copy) const
129 : : {
130 : 11210365 : copy.clear();
131 : 11210365 : copy.growTo(sz);
132 [ + + ]: 88541491 : for (int i = 0; i < sz; i++) copy[i] = data[i];
133 : 11210365 : }
134 : 9098 : void moveTo(vec<T>& dest)
135 : : {
136 : 9098 : dest.clear(true);
137 : 9098 : dest.data = data;
138 : 9098 : dest.sz = sz;
139 : 9098 : dest.cap = cap;
140 : 9098 : data = nullptr;
141 : 9098 : sz = 0;
142 : 9098 : cap = 0;
143 : 9098 : }
144 : : };
145 : :
146 : : template <class T>
147 : 50702288 : void vec<T>::capacity(int min_cap)
148 : : {
149 [ + + ]: 50702288 : if (cap >= min_cap) return;
150 : 30496135 : int add = imax((min_cap - cap + 1) & ~1,
151 : 30496135 : ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
152 : : // Casting data to void* silences the -Wclass-memaccess warning. This is safe
153 : : // as long as T is relocatable, which is true for the current instantiations
154 : : // of T.
155 : 60992270 : if (add > INT_MAX - cap
156 [ + - ][ - + ]: 30496135 : || (((data = (T*)::realloc((void*)data, (cap += add) * sizeof(T)))
[ - + ]
157 : : == nullptr)
158 [ - - ]: 0 : && errno == ENOMEM))
159 : 0 : throw OutOfMemoryException();
160 : : }
161 : :
162 : : template <class T>
163 : 25533938 : void vec<T>::growTo(int size, const T& pad)
164 : : {
165 [ + + ]: 25533938 : if (sz >= size) return;
166 : 7148027 : capacity(size);
167 [ + + ]: 14351948 : for (int i = sz; i < size; i++) data[i] = pad;
168 : 7148027 : sz = size;
169 : : }
170 : :
171 : : template <class T>
172 : 16064641 : void vec<T>::growTo(int size)
173 : : {
174 [ + + ]: 16064641 : if (sz >= size) return;
175 : 16061898 : capacity(size);
176 [ + + ]: 99622720 : for (int i = sz; i < size; i++) new (&data[i]) T();
177 : 16061898 : sz = size;
178 : : }
179 : :
180 : : template <class T>
181 : 68124589 : void vec<T>::clear(bool dealloc)
182 : : {
183 [ + + ]: 68124589 : if (data != nullptr)
184 : : {
185 [ + + ]: 282717801 : for (int i = 0; i < sz; i++) data[i].~T();
186 : 48539878 : sz = 0;
187 [ + + ]: 48539878 : if (dealloc) free(data), data = nullptr, cap = 0;
188 : : }
189 : 68124589 : }
190 : :
191 : : //=================================================================================================
192 : : } // namespace Minisat
193 : : } // namespace cvc5::internal
194 : :
195 : : #endif
|
