SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Heap.h
Go to the documentation of this file.
1 /******************************************************************************************[Heap.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 Minisat_Heap_h
22 #define Minisat_Heap_h
23 
24 #include "Vec.h"
25 
26 namespace Minisat
27 {
28  //=================================================================================================
29  // A heap implementation with support for decrease/increase key.
30 
31  template<class Comp>
32  class Heap
33  {
34  Comp lt; // The heap is a minimum-heap with respect to this comparator
35  vec<int> heap; // Heap of integers
36  vec<int> indices; // Each integers position (index) in the Heap
37 
38  // Index "traversal" functions
39  static inline int left( int i )
40  {
41  return i * 2 + 1;
42  }
43 
44  static inline int right( int i )
45  {
46  return (i + 1) * 2;
47  }
48 
49  static inline int parent( int i )
50  {
51  return (i - 1) >> 1;
52  }
53 
54  void percolateUp( int i )
55  {
56  int x = heap[i];
57  int p = parent( i );
58 
59  while( i != 0 && lt( x, heap[p] ) )
60  {
61  heap[i] = heap[p];
62  indices[heap[p]] = i;
63  i = p;
64  p = parent( p );
65  }
66  heap[i] = x;
67  indices[x] = i;
68  }
69 
70  void percolateDown( int i )
71  {
72  int x = heap[i];
73  while( left( i ) < heap.size() )
74  {
75  int child = right( i ) < heap.size() && lt( heap[right( i )], heap[left( i )] ) ? right( i ) : left( i );
76  if( !lt( heap[child], x ) )
77  break;
78  heap[i] = heap[child];
79  indices[heap[i]] = i;
80  i = child;
81  }
82  heap[i] = x;
83  indices[x] = i;
84  }
85 
86  public:
87  Heap( const Comp& c ):
88  lt( c )
89  {}
90 
91  int size() const
92  {
93  return heap.size();
94  }
95 
96  bool empty() const
97  {
98  return heap.size() == 0;
99  }
100 
101  bool inHeap( int n ) const
102  {
103  return n < indices.size() && indices[n] >= 0;
104  }
105 
106  int operator []( int index ) const
107  {
108  assert( index < heap.size() );
109  return heap[index];
110  }
111 
112  void decrease( int n )
113  {
114  assert( inHeap( n ) );
115  percolateUp( indices[n] );
116  }
117 
118  void increase( int n )
119  {
120  assert( inHeap( n ) );
121  percolateDown( indices[n] );
122  }
123 
124  // Safe variant of insert/decrease/increase:
125  void update( int n )
126  {
127  if( !inHeap( n ) )
128  insert( n );
129  else
130  {
131  percolateUp( indices[n] );
132  percolateDown( indices[n] );
133  }
134  }
135 
136  void insert( int n )
137  {
138  indices.growTo( n + 1, -1 );
139  assert( !inHeap( n ) );
140 
141  indices[n] = heap.size();
142  heap.push( n );
143  percolateUp( indices[n] );
144  }
145 
146  int removeMin()
147  {
148  int x = heap[0];
149  heap[0] = heap.last();
150  indices[heap[0]] = 0;
151  indices[x] = -1;
152  heap.pop();
153  if( heap.size() > 1 )
154  percolateDown( 0 );
155  return x;
156  }
157 
158  // Rebuild the heap from scratch, using the elements in 'ns':
159  void build( vec<int>& ns )
160  {
161  for( int i = 0; i < heap.size(); i++ )
162  indices[heap[i]] = -1;
163  heap.clear();
164 
165  for( int i = 0; i < ns.size(); i++ )
166  {
167  indices[ns[i]] = i;
168  heap.push( ns[i] );
169  }
170 
171  for( int i = heap.size() / 2 - 1; i >= 0; i-- )
172  percolateDown( i );
173  }
174 
175  void clear( bool dealloc = false )
176  {
177  for( int i = 0; i < heap.size(); i++ )
178  indices[heap[i]] = -1;
179  heap.clear( dealloc );
180  }
181 
182  void print() const
183  {
184  std::cout << "Order heap:";
185  for( int i = 0; i < heap.size(); i++ )
186  std::cout << " " << heap[i];
187  std::cout << std::endl;
188  }
189  };
190 
191  //=================================================================================================
192 }
193 
194 #endif
vec< int > indices
Definition: Heap.h:36
static int parent(int i)
Definition: Heap.h:49
void print() const
Definition: Heap.h:182
void build(vec< int > &ns)
Definition: Heap.h:159
void insert(int n)
Definition: Heap.h:136
Comp lt
Definition: Heap.h:34
void decrease(int n)
Definition: Heap.h:112
int operator[](int index) const
Definition: Heap.h:106
int removeMin()
Definition: Heap.h:146
int size() const
Definition: Heap.h:91
void clear(bool dealloc=false)
Definition: Heap.h:175
bool empty() const
Definition: Heap.h:96
static int right(int i)
Definition: Heap.h:44
void update(int n)
Definition: Heap.h:125
void increase(int n)
Definition: Heap.h:118
vec< int > heap
Definition: Heap.h:35
void percolateUp(int i)
Definition: Heap.h:54
static int left(int i)
Definition: Heap.h:39
Heap(const Comp &c)
Definition: Heap.h:87
void percolateDown(int i)
Definition: Heap.h:70
bool inHeap(int n) const
Definition: Heap.h:101
void growTo(int size)
Definition: Vec.h:262
int size(void) const
Definition: Vec.h:118
const T & last(void) const
Definition: Vec.h:178
void clear(bool dealloc=false)
Definition: Vec.h:273
void push(void)
Definition: Vec.h:147
void pop(void)
Definition: Vec.h:168
Definition: Alg.h:27