summaryrefslogtreecommitdiff
path: root/src/prop/minisat/mtl/Vec.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/minisat/mtl/Vec.h')
-rw-r--r--src/prop/minisat/mtl/Vec.h142
1 files changed, 0 insertions, 142 deletions
diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h
deleted file mode 100644
index 364991aa9..000000000
--- a/src/prop/minisat/mtl/Vec.h
+++ /dev/null
@@ -1,142 +0,0 @@
-/*******************************************************************************************[Vec.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, 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.
-**************************************************************************************************/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4_MiniSat_Vec_h
-#define CVC4_MiniSat_Vec_h
-
-#include <cstdlib>
-#include <cassert>
-#include <new>
-
-namespace CVC4 {
-namespace prop {
-namespace minisat {
-
-//=================================================================================================
-// Automatically resizable arrays
-//
-// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
-
-template<class T>
-class vec {
- T* data;
- int sz;
- int cap;
-
- void init(int size, const T& pad);
- void grow(int min_cap);
-
- // Don't allow copying (error prone):
- vec<T>& operator = (vec<T>& other) { assert(0); return *this; }
- vec (vec<T>& other) { assert(0); }
-
- static inline int imin(int x, int y) {
- int mask = (x-y) >> (sizeof(int)*8-1);
- return (x&mask) + (y&(~mask)); }
-
- static inline int imax(int x, int y) {
- int mask = (y-x) >> (sizeof(int)*8-1);
- return (x&mask) + (y&(~mask)); }
-
-public:
- // Types:
- typedef int Key;
- typedef T Datum;
-
- // Constructors:
- vec(void) : data(NULL) , sz(0) , cap(0) { }
- vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); }
- vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); }
- vec(T* array, int size) : data(array), sz(size), cap(size) { } // (takes ownership of array -- will be deallocated with 'free()')
- ~vec(void) { clear(true); }
-
- // Ownership of underlying array:
- T* release (void) { T* ret = data; data = NULL; sz = 0; cap = 0; return ret; }
- operator T* (void) { return data; } // (unsafe but convenient)
- operator const T* (void) const { return data; }
-
- // Size operations:
- int size (void) const { return sz; }
- void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); }
- void shrink_(int nelems) { assert(nelems <= sz); sz -= nelems; }
- void pop (void) { sz--, data[sz].~T(); }
- void growTo (int size);
- void growTo (int size, const T& pad);
- void clear (bool dealloc = false);
- void capacity (int size) { grow(size); }
-
- // Stack interface:
-#if 1
- void push (void) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(); sz++; }
- //void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(elem); sz++; }
- void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } data[sz++] = elem; }
- void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; }
-#else
- void push (void) { if (sz == cap) grow(sz+1); new (&data[sz]) T() ; sz++; }
- void push (const T& elem) { if (sz == cap) grow(sz+1); new (&data[sz]) T(elem); sz++; }
-#endif
-
- const T& last (void) const { return data[sz-1]; }
- T& last (void) { return data[sz-1]; }
-
- // Vector interface:
- const T& operator [] (int index) const { return data[index]; }
- T& operator [] (int index) { return data[index]; }
-
-
- // Duplicatation (preferred instead):
- void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (&copy[i]) T(data[i]); }
- void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
-};
-
-template<class T>
-void vec<T>::grow(int min_cap) {
- if (min_cap <= cap) return;
- if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2;
- else do cap = (cap*3+1) >> 1; while (cap < min_cap);
- data = (T*)realloc(data, cap * sizeof(T)); }
-
-template<class T>
-void vec<T>::growTo(int size, const T& pad) {
- if (sz >= size) return;
- grow(size);
- for (int i = sz; i < size; i++) new (&data[i]) T(pad);
- sz = size; }
-
-template<class T>
-void vec<T>::growTo(int size) {
- if (sz >= size) return;
- grow(size);
- for (int i = sz; i < size; i++) new (&data[i]) T();
- sz = size; }
-
-template<class T>
-void vec<T>::clear(bool dealloc) {
- if (data != NULL){
- for (int i = 0; i < sz; i++) data[i].~T();
- sz = 0;
- if (dealloc) free(data), data = NULL, cap = 0; } }
-
-}/* CVC4::prop::minisat namespace */
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4_MiniSat_Vec_h */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback