1 |
|
/*****************************************************************************************[Queue.h] |
2 |
|
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson |
3 |
|
Copyright (c) 2007-2010, Niklas Sorensson |
4 |
|
|
5 |
|
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and |
6 |
|
associated documentation files (the "Software"), to deal in the Software without restriction, |
7 |
|
including without limitation the rights to use, copy, modify, merge, publish, distribute, |
8 |
|
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is |
9 |
|
furnished to do so, subject to the following conditions: |
10 |
|
|
11 |
|
The above copyright notice and this permission notice shall be included in all copies or |
12 |
|
substantial portions of the Software. |
13 |
|
|
14 |
|
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT |
15 |
|
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND |
16 |
|
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, |
17 |
|
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT |
18 |
|
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. |
19 |
|
**************************************************************************************************/ |
20 |
|
|
21 |
|
#ifndef BVMinisat_Queue_h |
22 |
|
#define BVMinisat_Queue_h |
23 |
|
|
24 |
|
#include "base/check.h" |
25 |
|
#include "prop/bvminisat/mtl/Vec.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace BVMinisat { |
29 |
|
|
30 |
|
//================================================================================================= |
31 |
|
|
32 |
|
template<class T> |
33 |
2 |
class Queue { |
34 |
|
vec<T> buf; |
35 |
|
int first; |
36 |
|
int end; |
37 |
|
|
38 |
|
public: |
39 |
|
typedef T Key; |
40 |
|
|
41 |
2 |
Queue() : buf(1), first(0), end(0) {} |
42 |
|
|
43 |
|
void clear (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; } |
44 |
10554 |
int size () const { return (end >= first) ? end - first : end - first + buf.size(); } |
45 |
|
|
46 |
|
const T& operator[](int index) const |
47 |
|
{ |
48 |
|
Assert(index >= 0); |
49 |
|
Assert(index < size()); |
50 |
|
return buf[(first + index) % buf.size()]; |
51 |
|
} |
52 |
4392 |
T& operator[](int index) |
53 |
|
{ |
54 |
4392 |
Assert(index >= 0); |
55 |
4392 |
Assert(index < size()); |
56 |
4392 |
return buf[(first + index) % buf.size()]; |
57 |
|
} |
58 |
|
|
59 |
1924 |
T peek() const |
60 |
|
{ |
61 |
1924 |
Assert(first != end); |
62 |
1924 |
return buf[first]; |
63 |
|
} |
64 |
1924 |
void pop() |
65 |
|
{ |
66 |
1924 |
Assert(first != end); |
67 |
1924 |
first++; |
68 |
1924 |
if (first == buf.size()) first = 0; |
69 |
1924 |
} |
70 |
1924 |
void insert(T elem) { // INVARIANT: buf[end] is always unused |
71 |
1924 |
buf[end++] = elem; |
72 |
1924 |
if (end == buf.size()) end = 0; |
73 |
1924 |
if (first == end){ // Resize: |
74 |
56 |
vec<T> tmp((buf.size()*3 + 1) >> 1); |
75 |
|
//**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0); |
76 |
28 |
int i = 0; |
77 |
28 |
for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j]; |
78 |
28 |
for (int j = 0 ; j < end ; j++) tmp[i++] = buf[j]; |
79 |
28 |
first = 0; |
80 |
28 |
end = buf.size(); |
81 |
28 |
tmp.moveTo(buf); |
82 |
|
} |
83 |
1924 |
} |
84 |
|
}; |
85 |
|
|
86 |
|
|
87 |
|
//================================================================================================= |
88 |
|
} // namespace BVMinisat |
89 |
|
} // namespace cvc5 |
90 |
|
|
91 |
|
#endif |