SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Vec.h
Go to the documentation of this file.
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 <assert.h>
25 #include <iostream>
26 #include <new>
27 
28 #include "IntTypes.h"
29 #include "XAlloc.h"
30 
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  {
41  T* data;
42  int sz;
43  int cap;
44 
45  // Don't allow copying (error prone):
47  {
48  assert( 0 );
49  return *this;
50  }
51 
52  vec( vec<T>& )
53  {
54  assert( 0 );
55  }
56 
57  // Helpers for calculating next capacity:
58  static inline int imax( int x, int y )
59  {
60  int mask = (y - x) >> (sizeof(int) * 8 - 1);
61  return (x & mask) + (y & (~mask));
62  }
63 
64  //static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
65  static inline void nextCap( int& cap )
66  {
67  cap += ((cap >> 1) + 2) & ~1;
68  }
69 
70  public:
71  // Constructors:
72  vec():
73  data( NULL ),
74  sz( 0 ),
75  cap( 0 )
76  {}
77  explicit vec( int size ):
78  data( NULL ),
79  sz( 0 ),
80  cap( 0 )
81  {
82  growTo( size );
83  }
84  vec( int size, const T& pad ):
85  data( NULL ),
86  sz( 0 ),
87  cap( 0 )
88  {
89  growTo( size, pad );
90  }
91  vec( vec<T>&& _toMove )
92  {
93  data = _toMove.data;
94  sz = _toMove.sz;
95  cap = _toMove.cap;
96  _toMove.data = NULL;
97  _toMove.sz = 0;
98  _toMove.cap = 0;
99  }
101  {
102  clear( true );
103  }
104 
105  vec<T>& operator = ( vec<T>&& _toMove )
106  {
107  _toMove.moveTo( *this );
108  return *this;
109  }
110 
111  // Pointer to first element:
112  operator T*( void )
113  {
114  return data;
115  }
116 
117  // Size operations:
118  int size( void ) const
119  {
120  return sz;
121  }
122 
123  void shrink( int nelems )
124  {
125  assert( nelems <= sz );
126  for( int i = 0; i < nelems; i++ )
127  sz--, data[sz].~T();
128  }
129 
130  void shrink_( int nelems )
131  {
132  assert( nelems <= sz );
133  sz -= nelems;
134  }
135 
136  int capacity( void ) const
137  {
138  return cap;
139  }
140 
141  void capacity( int min_cap );
142  void growTo( int size );
143  void growTo( int size, const T& pad );
144  void clear( bool dealloc = false );
145 
146  // Stack interface:
147  void push( void )
148  {
149  if( sz == cap )
150  capacity( sz + 1 );
151  new( &data[sz] ) T();
152  sz++;
153  }
154 
155  void push( const T& elem )
156  {
157  if( sz == cap )
158  capacity( sz + 1 );
159  data[sz++] = elem;
160  }
161 
162  void push_( const T& elem )
163  {
164  assert( sz < cap );
165  data[sz++] = elem;
166  }
167 
168  void pop( void )
169  {
170  assert( sz > 0 );
171  sz--, data[sz].~T();
172  }
173  // NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but
174  // in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not
175  // happen given the way capacities are calculated (below). Essentially, all capacities are
176  // even, but INT_MAX is odd.
177 
178  const T& last( void ) const
179  {
180  return data[sz - 1];
181  }
182 
183  T& last( void )
184  {
185  return data[sz - 1];
186  }
187 
188  // Vector interface:
189  const T& operator []( int index ) const
190  {
191  return data[index];
192  }
193 
194  T& operator []( int index )
195  {
196  return data[index];
197  }
198 
199  // Duplicatation (preferred instead):
200  void copyTo( vec<T>& copy ) const
201  {
202  copy.clear();
203  copy.growTo( sz );
204  for( int i = 0; i < sz; i++ )
205  copy[i] = data[i];
206  }
207 
208  void moveTo( vec<T>& dest )
209  {
210  dest.clear( true );
211  dest.data = data;
212  dest.sz = sz;
213  dest.cap = cap;
214  data = NULL;
215  sz = 0;
216  cap = 0;
217  }
218  };
219 
220  template<typename T>
221  inline std::ostream& operator<<(std::ostream& os, const vec<T>& v) {
222  os << "[";
223  for (int i = 0; i < v.size(); i++) {
224  if (i > 0) os << ", ";
225  os << v[i];
226  }
227  return os << "]";
228  }
229 
230  template<>
231  inline std::ostream& operator<<(std::ostream& os, const vec<char>& v) {
232  os << "[";
233  for (int i = 0; i < v.size(); i++) {
234  if (i > 0) os << ", ";
235  os << static_cast<int>(v[i]);
236  }
237  return os << "]";
238  }
239 
240  template<class T>
241  void vec<T>::capacity( int min_cap )
242  {
243  if( cap >= min_cap )
244  return;
245  int add = imax( (min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1 ); // NOTE: grow by approximately 3/2
246  if( (add > INT_MAX - cap || ((data = (T*)::realloc( data, (unsigned)(cap += add) * sizeof(T) )) == NULL)) && errno == ENOMEM )
247  throw OutOfMemoryException();
248  }
249 
250  template<class T>
251  void vec<T>::growTo( int size, const T& pad )
252  {
253  if( sz >= size )
254  return;
255  capacity( size );
256  for( int i = sz; i < size; i++ )
257  data[i] = pad;
258  sz = size;
259  }
260 
261  template<class T>
262  void vec<T>::growTo( int size )
263  {
264  if( sz >= size )
265  return;
266  capacity( size );
267  for( int i = sz; i < size; i++ )
268  new( &data[i] ) T();
269  sz = size;
270  }
271 
272  template<class T>
273  void vec<T>::clear( bool dealloc )
274  {
275  if( data != NULL )
276  {
277  for( int i = 0; i < sz; i++ )
278  data[i].~T();
279  sz = 0;
280  if( dealloc )
281  free( data ), data = NULL, cap = 0;
282  }
283  }
284 
285  //=================================================================================================
286 }
287 
288 #endif
void shrink(int nelems)
Definition: Vec.h:123
static int imax(int x, int y)
Definition: Vec.h:58
const T & operator[](int index) const
Definition: Vec.h:189
void growTo(int size)
Definition: Vec.h:262
void push_(const T &elem)
Definition: Vec.h:162
vec(vec< T > &&_toMove)
Definition: Vec.h:91
static void nextCap(int &cap)
Definition: Vec.h:65
void copyTo(vec< T > &copy) const
Definition: Vec.h:200
void moveTo(vec< T > &dest)
Definition: Vec.h:208
int capacity(void) const
Definition: Vec.h:136
int sz
Definition: Vec.h:42
T & last(void)
Definition: Vec.h:183
int size(void) const
Definition: Vec.h:118
int cap
Definition: Vec.h:43
void push(const T &elem)
Definition: Vec.h:155
vec< T > & operator=(vec< T > &)
Definition: Vec.h:46
const T & last(void) const
Definition: Vec.h:178
~vec()
Definition: Vec.h:100
vec(int size, const T &pad)
Definition: Vec.h:84
vec()
Definition: Vec.h:72
void shrink_(int nelems)
Definition: Vec.h:130
void clear(bool dealloc=false)
Definition: Vec.h:273
T * data
Definition: Vec.h:41
void capacity(int min_cap)
Definition: Vec.h:241
void push(void)
Definition: Vec.h:147
vec(vec< T > &)
Definition: Vec.h:52
void pop(void)
Definition: Vec.h:168
void growTo(int size, const T &pad)
Definition: Vec.h:251
vec(int size)
Definition: Vec.h:77
Definition: Alg.h:27
static void copy(const T &from, T &to)
Definition: Alg.h:60
std::ostream & operator<<(std::ostream &os, const Lit &l)
Definition: SolverTypes.h:75