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 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::internal {
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 : 30843936 : 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 : 34684554 : vec() : data(NULL) , sz(0) , cap(0) { }
60 : 62356 : explicit vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); }
61 : 51576 : vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); }
62 : 34786501 : ~vec() { clear(true); }
63 : :
64 : : // Pointer to first element:
65 : 166644662 : operator T* (void) { return data; }
66 : :
67 : : // Size operations:
68 : 7602510193 : int size (void) const { return sz; }
69 : 172468936 : void shrink(int nelems)
70 : : {
71 [ - + ][ - + ]: 172468936 : Assert(nelems <= sz);
[ - - ]
72 [ + + ]: 690470276 : for (int i = 0; i < nelems; i++) sz--, data[sz].~T();
73 : 172468936 : }
74 : : void shrink_(int nelems)
75 : : {
76 : : Assert(nelems <= sz);
77 : : sz -= nelems;
78 : : }
79 : 0 : 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 [ + + ]: 7605263 : void push (void) { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; }
87 [ + + ]: 538234638 : void push (const T& elem) { if (sz == cap) capacity(sz+1); data[sz++] = elem; }
88 : 164805000 : void push_(const T& elem)
89 : : {
90 [ - + ][ - + ]: 164805000 : Assert(sz < cap);
[ - - ]
91 : 164805000 : data[sz++] = elem;
92 : 164805000 : }
93 : 47372920 : void pop(void)
94 : : {
95 [ - + ][ - + ]: 47372920 : Assert(sz > 0);
[ - - ]
96 : 47372920 : sz--, data[sz].~T();
97 : 47372920 : }
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 : 51972420 : T& last (void) { return data[sz-1]; }
105 : :
106 : : // Vector interface:
107 : 6154492040 : const T& operator [] (int index) const { return data[index]; }
108 : 4974553340 : T& operator [] (int index) { return data[index]; }
109 : :
110 : : // Duplication (preferred instead):
111 [ + + ]: 89094100 : void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
112 : 10780 : 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 : 52573293 : void vec<T>::capacity(int min_cap) {
118 [ + + ]: 52573293 : if (cap >= min_cap) return;
119 : 30843936 : int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
120 [ + - ][ - + ]: 30843936 : if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
[ - - ][ - + ]
121 : 0 : throw OutOfMemoryException();
122 : : }
123 : :
124 : :
125 : : template<class T>
126 : 19864986 : void vec<T>::growTo(int size, const T& pad) {
127 [ + + ]: 19864986 : if (sz >= size) return;
128 : 7677536 : capacity(size);
129 [ + + ]: 15410922 : for (int i = sz; i < size; i++) data[i] = pad;
130 : 7677536 : sz = size; }
131 : :
132 : :
133 : : template<class T>
134 : 16984477 : void vec<T>::growTo(int size) {
135 [ + + ]: 16984477 : if (sz >= size) return;
136 : 16981477 : capacity(size);
137 [ + + ]: 100952457 : for (int i = sz; i < size; i++) new (&data[i]) T();
138 : 16981477 : sz = size; }
139 : :
140 : :
141 : : template<class T>
142 : 79420976 : void vec<T>::clear(bool dealloc) {
143 [ + + ]: 79420976 : if (data != NULL){
144 [ + + ]: 290742345 : for (int i = 0; i < sz; i++) data[i].~T();
145 : 53784693 : sz = 0;
146 [ + + ]: 53784693 : if (dealloc) free(data), data = NULL, cap = 0; } }
147 : :
148 : : //=================================================================================================
149 : : }
150 : : } // namespace cvc5::internal
151 : :
152 : : #endif
|