diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-08-15 21:25:21 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-08-15 21:25:21 +0000 |
commit | a6b782a6b8486689e47338c456b816c95cf67a92 (patch) | |
tree | a7f911007e1d27c2fb0e1847d9cabb1c538d65b2 /src/prop/minisat/mtl/Queue.h | |
parent | 58ea6b0b63d2170391a61e0fe3b1a3ecf3b99fb2 (diff) |
Diffstat (limited to 'src/prop/minisat/mtl/Queue.h')
-rw-r--r-- | src/prop/minisat/mtl/Queue.h | 98 |
1 files changed, 37 insertions, 61 deletions
diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h index 291a1f2e3..17567d694 100644 --- a/src/prop/minisat/mtl/Queue.h +++ b/src/prop/minisat/mtl/Queue.h @@ -1,5 +1,6 @@ /*****************************************************************************************[Queue.h] -MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +Copyright (c) 2003-2006, 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, @@ -17,77 +18,52 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#include "cvc4_private.h" +#ifndef Minisat_Queue_h +#define Minisat_Queue_h -#ifndef CVC4_MiniSat_Queue_h -#define CVC4_MiniSat_Queue_h +#include "mtl/Vec.h" -#include "Vec.h" - -namespace CVC4 { -namespace prop { -namespace minisat { +namespace Minisat { //================================================================================================= - -template <class T> +template<class T> class Queue { - vec<T> elems; + vec<T> buf; int first; + int end; public: - Queue(void) : first(0) { } - - void insert(T x) { elems.push(x); } - T peek () const { return elems[first]; } - void pop () { first++; } - - void clear(bool dealloc = false) { elems.clear(dealloc); first = 0; } - int size(void) { return elems.size() - first; } - - //bool has(T x) { for (int i = first; i < elems.size(); i++) if (elems[i] == x) return true; return false; } - - const T& operator [] (int index) const { return elems[first + index]; } - + typedef T Key; + + Queue() : buf(1), first(0), end(0) {} + + void clear (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; } + int size () const { return (end >= first) ? end - first : end - first + buf.size(); } + + const T& operator [] (int index) const { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; } + T& operator [] (int index) { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; } + + T peek () const { assert(first != end); return buf[first]; } + void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; } + void insert(T elem) { // INVARIANT: buf[end] is always unused + buf[end++] = elem; + if (end == buf.size()) end = 0; + if (first == end){ // Resize: + vec<T> tmp((buf.size()*3 + 1) >> 1); + //**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0); + int i = 0; + for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j]; + for (int j = 0 ; j < end ; j++) tmp[i++] = buf[j]; + first = 0; + end = buf.size(); + tmp.moveTo(buf); + } + } }; -//template<class T> -//class Queue { -// vec<T> buf; -// int first; -// int end; -// -//public: -// typedef T Key; -// -// Queue() : buf(1), first(0), end(0) {} -// -// void clear () { buf.shrinkTo(1); first = end = 0; } -// int size () { return (end >= first) ? end - first : end - first + buf.size(); } -// -// T peek () { assert(first != end); return buf[first]; } -// void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; } -// void insert(T elem) { // INVARIANT: buf[end] is always unused -// buf[end++] = elem; -// if (end == buf.size()) end = 0; -// if (first == end){ // Resize: -// vec<T> tmp((buf.size()*3 + 1) >> 1); -// //**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0); -// int i = 0; -// for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j]; -// for (int j = 0 ; j < end ; j++) tmp[i++] = buf[j]; -// first = 0; -// end = buf.size(); -// tmp.moveTo(buf); -// } -// } -//}; //================================================================================================= +} -}/* CVC4::prop::minisat namespace */ -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ - -#endif /* CVC4_MiniSat_Queue_h */ +#endif |