diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-08-13 17:19:28 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-08-13 17:19:28 +0000 |
commit | 040f00ac35e51a6968aab57c5cfccd02927b7e9f (patch) | |
tree | c0b2cdd0ff249c3811befcd12d011dc89a5099b9 /src/prop/minisat/mtl/Queue.h | |
parent | 704b56f3f5bdba6601dd687c8e649e36de50a6e7 (diff) |
Removing old version of MiniSat for proper vendor import
Diffstat (limited to 'src/prop/minisat/mtl/Queue.h')
-rw-r--r-- | src/prop/minisat/mtl/Queue.h | 93 |
1 files changed, 0 insertions, 93 deletions
diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h deleted file mode 100644 index 291a1f2e3..000000000 --- a/src/prop/minisat/mtl/Queue.h +++ /dev/null @@ -1,93 +0,0 @@ -/*****************************************************************************************[Queue.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_Queue_h -#define CVC4_MiniSat_Queue_h - -#include "Vec.h" - -namespace CVC4 { -namespace prop { -namespace minisat { - -//================================================================================================= - - -template <class T> -class Queue { - vec<T> elems; - int first; - -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]; } - -}; - -//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 */ |