From 94c1307c262e4b14f4a91b1bbcf9099ee6202bab Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 12 Mar 2014 10:17:51 +0100 Subject: Added libs/minisat (copy of minisat git master) --- libs/minisat/Vec.h | 134 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 134 insertions(+) create mode 100644 libs/minisat/Vec.h (limited to 'libs/minisat/Vec.h') diff --git a/libs/minisat/Vec.h b/libs/minisat/Vec.h new file mode 100644 index 000000000..2086e0bb2 --- /dev/null +++ b/libs/minisat/Vec.h @@ -0,0 +1,134 @@ +/*******************************************************************************************[Vec.h] +Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson +Copyright (c) 2007-2010, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Minisat_Vec_h +#define Minisat_Vec_h + +#include +#include +#include + +#include "libs/minisat/IntTypes.h" +#include "libs/minisat/XAlloc.h" + +namespace Minisat { + +//================================================================================================= +// Automatically resizable arrays +// +// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc) + +template +class vec { +public: + typedef _Size Size; +private: + T* data; + Size sz; + Size cap; + + // Don't allow copying (error prone): + vec& operator=(vec& other); + vec (vec& other); + + static inline Size max(Size x, Size y){ return (x > y) ? x : y; } + +public: + // Constructors: + vec() : data(NULL), sz(0), cap(0) { } + explicit vec(Size size) : data(NULL), sz(0), cap(0) { growTo(size); } + vec(Size size, const T& pad) : data(NULL), sz(0), cap(0) { growTo(size, pad); } + ~vec() { clear(true); } + + // Pointer to first element: + operator T* (void) { return data; } + + // Size operations: + Size size (void) const { return sz; } + void shrink (Size nelems) { assert(nelems <= sz); for (Size i = 0; i < nelems; i++) sz--, data[sz].~T(); } + void shrink_ (Size nelems) { assert(nelems <= sz); sz -= nelems; } + int capacity (void) const { return cap; } + void capacity (Size min_cap); + void growTo (Size size); + void growTo (Size size, const T& pad); + void clear (bool dealloc = false); + + // Stack interface: + void push (void) { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; } + //void push (const T& elem) { if (sz == cap) capacity(sz+1); data[sz++] = elem; } + void push (const T& elem) { if (sz == cap) capacity(sz+1); new (&data[sz++]) T(elem); } + void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; } + void pop (void) { assert(sz > 0); sz--, data[sz].~T(); } + // NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but + // in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not + // happen given the way capacities are calculated (below). Essentially, all capacities are + // even, but INT_MAX is odd. + + const T& last (void) const { return data[sz-1]; } + T& last (void) { return data[sz-1]; } + + // Vector interface: + const T& operator [] (Size index) const { return data[index]; } + T& operator [] (Size index) { return data[index]; } + + // Duplicatation (preferred instead): + void copyTo(vec& copy) const { copy.clear(); copy.growTo(sz); for (Size i = 0; i < sz; i++) copy[i] = data[i]; } + void moveTo(vec& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; } +}; + + +template +void vec::capacity(Size min_cap) { + if (cap >= min_cap) return; + Size add = max((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2 + const Size size_max = std::numeric_limits::max(); + if ( ((size_max <= std::numeric_limits::max()) && (add > size_max - cap)) + || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM) ) + throw OutOfMemoryException(); + } + + +template +void vec::growTo(Size size, const T& pad) { + if (sz >= size) return; + capacity(size); + for (Size i = sz; i < size; i++) data[i] = pad; + sz = size; } + + +template +void vec::growTo(Size size) { + if (sz >= size) return; + capacity(size); + for (Size i = sz; i < size; i++) new (&data[i]) T(); + sz = size; } + + +template +void vec::clear(bool dealloc) { + if (data != NULL){ + for (Size i = 0; i < sz; i++) data[i].~T(); + sz = 0; + if (dealloc) free(data), data = NULL, cap = 0; } } + +//================================================================================================= +} + +#endif -- cgit v1.2.3