GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/minisat/mtl/Heap.h Lines: 69 77 89.6 %
Date: 2021-03-22 Branches: 35 124 28.2 %

Line Exec Source
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 "base/check.h"
25
#include "prop/minisat/mtl/Vec.h"
26
27
namespace CVC4 {
28
namespace Minisat {
29
30
//=================================================================================================
31
// A heap implementation with support for decrease/increase key.
32
33
34
template<class Comp>
35
18048
class Heap {
36
    Comp     lt;       // The heap is a minimum-heap with respect to this comparator
37
    vec<int> heap;     // Heap of integers
38
    vec<int> indices;  // Each integers position (index) in the Heap
39
40
    // Index "traversal" functions
41
72854117
    static inline int left  (int i) { return i*2+1; }
42
65588021
    static inline int right (int i) { return (i+1)*2; }
43
42786657
    static inline int parent(int i) { return (i-1) >> 1; }
44
45
46
17621542
    void percolateUp(int i)
47
    {
48
17621542
        int x  = heap[i];
49
17621542
        int p  = parent(i);
50
51
67951772
        while (i != 0 && lt(x, heap[p])){
52
25165115
            heap[i]          = heap[p];
53
25165115
            indices[heap[p]] = i;
54
25165115
            i                = p;
55
25165115
            p                = parent(p);
56
        }
57
17621542
        heap   [i] = x;
58
17621542
        indices[x] = i;
59
17621542
    }
60
61
62
8955911
    void percolateDown(int i)
63
    {
64
8955911
        int x = heap[i];
65
51260133
        while (left(i) < heap.size()){
66
27240823
            int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
67
27240823
            if (!lt(heap[child], x)) break;
68
21152111
            heap[i]          = heap[child];
69
21152111
            indices[heap[i]] = i;
70
21152111
            i                = child;
71
        }
72
8955911
        heap   [i] = x;
73
8955911
        indices[x] = i;
74
8955911
    }
75
76
77
  public:
78
18054
    Heap(const Comp& c) : lt(c) { }
79
80
1452
    int  size      ()          const { return heap.size(); }
81
6082438
    bool empty     ()          const { return heap.size() == 0; }
82
88190492
    bool inHeap    (int n)     const { return n < indices.size() && indices[n] >= 0; }
83
    int operator[](int index) const
84
    {
85
      Assert(index < heap.size());
86
      return heap[index];
87
    }
88
89
10147614
    void decrease(int n)
90
    {
91
10147614
      Assert(inHeap(n));
92
10147614
      percolateUp(indices[n]);
93
10147614
    }
94
1631559
    void increase(int n)
95
    {
96
1631559
      Assert(inHeap(n));
97
1631559
      percolateDown(indices[n]);
98
1631559
    }
99
100
    // Safe variant of insert/decrease/increase:
101
691938
    void update(int n)
102
    {
103
691938
        if (!inHeap(n))
104
13073
            insert(n);
105
        else {
106
678865
            percolateUp(indices[n]);
107
678865
            percolateDown(indices[n]); }
108
691938
    }
109
110
111
6795063
    void insert(int n)
112
    {
113
6795063
        indices.growTo(n+1, -1);
114
6795063
        Assert(!inHeap(n));
115
116
6795063
        indices[n] = heap.size();
117
6795063
        heap.push(n);
118
6795063
        percolateUp(indices[n]);
119
6795063
    }
120
121
122
5995070
    int  removeMin()
123
    {
124
5995070
        int x            = heap[0];
125
5995070
        heap[0]          = heap.last();
126
5995070
        indices[heap[0]] = 0;
127
5995070
        indices[x]       = -1;
128
5995070
        heap.pop();
129
5995070
        if (heap.size() > 1) percolateDown(0);
130
5995070
        return x;
131
    }
132
133
134
    // Rebuild the heap from scratch, using the elements in 'ns':
135
16973
    void build(vec<int>& ns) {
136
1696012
        for (int i = 0; i < heap.size(); i++)
137
1679039
            indices[heap[i]] = -1;
138
16973
        heap.clear();
139
140
1427392
        for (int i = 0; i < ns.size(); i++){
141
1410419
            indices[ns[i]] = i;
142
1410419
            heap.push(ns[i]); }
143
144
719353
        for (int i = heap.size() / 2 - 1; i >= 0; i--)
145
702380
            percolateDown(i);
146
16973
    }
147
148
    void clear(bool dealloc = false)
149
    {
150
        for (int i = 0; i < heap.size(); i++)
151
            indices[heap[i]] = -1;
152
        heap.clear(dealloc);
153
    }
154
};
155
156
157
//=================================================================================================
158
}
159
}
160
161
#endif