00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00109 #ifndef __NUSMV_CORE_UTILS_VECTOR_H__
00110 #define __NUSMV_CORE_UTILS_VECTOR_H__
00111
00112 #include "nusmv/core/utils/defs.h"
00113 #include <string.h>
00114
00115
00116 #define DECLARE_VECTOR__impl_(qual, type, name, prefix) \
00117 struct name { \
00118 type *data_; \
00119 size_t size_; \
00120 size_t capacity_; \
00121 }; \
00122 typedef struct name *name; \
00123 qual name prefix ## _create(void); \
00124 qual void prefix ## _destroy(name v); \
00125 qual void prefix ## _push(name v, type elem); \
00126 qual void prefix ## _pop(name v); \
00127 qual void prefix ## _append(name v1, name v2); \
00128 qual void prefix ## _resize(name v, size_t newsz); \
00129 qual void prefix ## _shrink(name v, size_t newsz); \
00130 qual void prefix ## _reserve(name v, size_t cap); \
00131 qual void prefix ## _clear(name v); \
00132 qual void prefix ## _copy(name src, name dest); \
00133 qual void prefix ## _swap(name v1, name v2); \
00134 qual void prefix ## _sort(name v, int (*cmp)(type a, type b, void *p), \
00135 void *p); \
00136 qual void prefix ## _acquire(name v, type *arr, size_t sz); \
00137 qual type *prefix ## _release(name v);
00138
00139 #define VECTOR_SIZE(v) ((v)->size_)
00140 #define VECTOR_CAPACITY(v) ((v)->capacity_)
00141 #define VECTOR_ARRAY(v) ((v)->data_)
00142 #define VECTOR_FIRST(v) (VECTOR_ARRAY(v)[0])
00143 #define VECTOR_AT(v,i) (VECTOR_ARRAY(v)[i])
00144 #define VECTOR_LAST(v) (VECTOR_ARRAY(v)[VECTOR_SIZE(v)-1])
00145
00146 #define EMPTY__nusmv_utils_vector__
00147
00148 #define DECLARE_VECTOR(type, name, prefix) \
00149 DECLARE_VECTOR__impl_(EMPTY__nusmv_utils_vector__, type, name, prefix)
00150
00151 #define DEFINE_VECTOR__impl_(qual, type, name, prefix) \
00152 qual name prefix ## _create(void) \
00153 { \
00154 name ret = ALLOC(struct name, 1); \
00155 ret->data_ = NULL; \
00156 ret->size_ = 0; \
00157 ret->capacity_ = 0; \
00158 \
00159 return ret; \
00160 } \
00161 \
00162 \
00163 qual void prefix ## _destroy(name v) \
00164 { \
00165 if (v->data_) { \
00166 FREE(v->data_); \
00167 } \
00168 FREE(v); \
00169 } \
00170 \
00171 \
00172 qual void prefix ## _push(name v, type elem) \
00173 { \
00174 while (v->size_ >= v->capacity_) { \
00175 prefix ## _reserve(v, v->capacity_ ? v->capacity_ * 2 : 2); \
00176 } \
00177 v->data_[v->size_++] = elem; \
00178 } \
00179 \
00180 \
00181 qual void prefix ## _pop(name v) \
00182 { \
00183 nusmv_assert(v->size_ > 0); \
00184 --v->size_; \
00185 } \
00186 \
00187 \
00188 qual void prefix ## _append(name v1, name v2) \
00189 { \
00190 prefix ## _reserve(v1, v1->size_ + v2->size_); \
00191 memcpy(v1->data_ + v1->size_, v2->data_, sizeof(type) * v2->size_); \
00192 v1->size_ += v2->size_; \
00193 } \
00194 \
00195 \
00196 qual void prefix ## _resize(name v, size_t newsz) \
00197 { \
00198 if (v->size_ >= newsz) { \
00199 v->size_ = newsz; \
00200 } else { \
00201 size_t i; \
00202 prefix ## _reserve(v, newsz); \
00203 for (i = v->size_; i < newsz; ++i) { \
00204 v->data_[i] = 0; \
00205 } \
00206 v->size_ = newsz; \
00207 } \
00208 } \
00209 \
00210 \
00211 qual void prefix ## _shrink(name v, size_t newsz) \
00212 { \
00213 if (newsz == 0) { \
00214 prefix ## _clear(v); \
00215 } else if (newsz < v->size_) { \
00216 v->data_ = REALLOC(type, v->data_, newsz); \
00217 v->size_ = newsz; \
00218 v->capacity_ = newsz; \
00219 } \
00220 } \
00221 \
00222 \
00223 qual void prefix ## _reserve(name v, size_t cap) \
00224 { \
00225 if (cap > 0 && v->capacity_ < cap) { \
00226 v->data_ = REALLOC(type, v->data_, cap); \
00227 v->capacity_ = cap; \
00228 } \
00229 } \
00230 \
00231 \
00232 qual void prefix ## _clear(name v) \
00233 { \
00234 v->size_ = 0; \
00235 v->capacity_ = 0; \
00236 if (v->data_) { \
00237 FREE(v->data_); \
00238 v->data_ = NULL; \
00239 } \
00240 } \
00241 \
00242 \
00243 qual void prefix ## _copy(name src, name dest) \
00244 { \
00245 prefix ## _resize(dest, src->size_); \
00246 dest->size_ = src->size_; \
00247 if (src->data_ != NULL) { \
00248 memcpy(dest->data_, src->data_, sizeof(type) * src->size_); \
00249 } \
00250 } \
00251 \
00252 \
00253 qual void prefix ## _swap(name v1, name v2) \
00254 { \
00255 size_t tmp1; \
00256 type *tmp2; \
00257 \
00258 tmp1 = v1->size_; \
00259 v1->size_ = v2->size_; \
00260 v2->size_ = tmp1; \
00261 \
00262 tmp1 = v1->capacity_; \
00263 v1->capacity_ = v2->capacity_; \
00264 v2->capacity_ = tmp1; \
00265 \
00266 tmp2 = v1->data_; \
00267 v1->data_ = v2->data_; \
00268 v2->data_ = tmp2; \
00269 } \
00270 \
00271 \
00272 static void prefix ## _sort_impl( \
00273 type *arr, size_t size, \
00274 int (*cmp)(type a, type b, void *p), void *p) \
00275 { \
00276 \
00277 if (size <= 15) { \
00278 \
00279 size_t i, j, best_i; \
00280 type tmp; \
00281 \
00282 for (i = 1; i < size; ++i){ \
00283 best_i = i-1; \
00284 for (j = i; j < size; ++j) { \
00285 if (cmp(arr[j], arr[best_i], p) < 0) { \
00286 best_i = j; \
00287 } \
00288 } \
00289 tmp = arr[i-1]; \
00290 arr[i-1] = arr[best_i]; \
00291 arr[best_i] = tmp; \
00292 } \
00293 } else { \
00294 size_t i, j; \
00295 type pivot; \
00296 type tmp; \
00297 pivot = arr[size / 2]; \
00298 i = (size_t)-1; \
00299 j = size; \
00300 \
00301 for (;;) { \
00302 do i++; while(cmp(arr[i], pivot, p) < 0); \
00303 do j--; while(cmp(pivot, arr[j], p) < 0); \
00304 \
00305 if (i >= j) break; \
00306 \
00307 tmp = arr[i]; \
00308 arr[i] = arr[j]; \
00309 arr[j] = tmp; \
00310 } \
00311 \
00312 prefix ## _sort_impl(arr, i, cmp, p); \
00313 prefix ## _sort_impl(&arr[i], size-i, cmp, p); \
00314 } \
00315 } \
00316 \
00317 qual void prefix ## _sort(name v, int (*cmp)(type a, type b, void *p), \
00318 void *p) \
00319 { \
00320 prefix ## _sort_impl(v->data_, v->size_, cmp, p); \
00321 } \
00322 \
00323 \
00324 qual void prefix ## _acquire(name v, type *arr, size_t sz) \
00325 { \
00326 if (v->data_) { \
00327 FREE(v->data_); \
00328 } \
00329 v->data_ = arr; \
00330 v->size_ = sz; \
00331 v->capacity_ = sz; \
00332 } \
00333 \
00334 \
00335 qual type *prefix ## _release(name v) \
00336 { \
00337 type *ret = v->data_; \
00338 v->data_ = NULL; \
00339 v->size_ = 0; \
00340 v->capacity_ = 0; \
00341 return ret; \
00342 }
00343
00344
00345 #define DEFINE_VECTOR(type, name, prefix) \
00346 DEFINE_VECTOR__impl_(EMPTY__nusmv_utils_vector__, type, name, prefix)
00347
00348 #define DEFINE_STATIC_VECTOR(type, name, prefix) \
00349 DECLARE_VECTOR__impl_(static, type, name, prefix) \
00350 DEFINE_VECTOR__impl_(static, type, name, prefix)
00351
00352
00353 DECLARE_VECTOR(void *, Vector_ptr, Vector)
00354 DECLARE_VECTOR(int, IntVector_ptr, IntVector)
00355 DECLARE_VECTOR(double, DoubleVector_ptr, DoubleVector)
00356
00357
00358 #endif
