GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/minisat/mtl/Heap.h Lines: 69 77 89.6 %
Date: 2021-03-23 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
18052
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
72854252
    static inline int left  (int i) { return i*2+1; }
42
65588107
    static inline int right (int i) { return (i+1)*2; }
43
42786909
    static inline int parent(int i) { return (i-1) >> 1; }
44
45
46
17621766
    void percolateUp(int i)
47
    {
48
17621766
        int x  = heap[i];
49
17621766
        int p  = parent(i);
50
51
67952052
        while (i != 0 && lt(x, heap[p])){
52
25165143
            heap[i]          = heap[p];
53
25165143
            indices[heap[p]] = i;
54
25165143
            i                = p;
55
25165143
            p                = parent(p);
56
        }
57
17621766
        heap   [i] = x;
58
17621766
        indices[x] = i;
59
17621766
    }
60
61
62
8955961
    void percolateDown(int i)
63
    {
64
8955961
        int x = heap[i];
65
51260181
        while (left(i) < heap.size()){
66
27240872
            int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
67
27240872
            if (!lt(heap[child], x)) break;
68
21152110
            heap[i]          = heap[child];
69
21152110
            indices[heap[i]] = i;
70
21152110
            i                = child;
71
        }
72
8955961
        heap   [i] = x;
73
8955961
        indices[x] = i;
74
8955961
    }
75
76
77
  public:
78
18058
    Heap(const Comp& c) : lt(c) { }
79
80
1452
    int  size      ()          const { return heap.size(); }
81
6082462
    bool empty     ()          const { return heap.size() == 0; }
82
88191255
    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
10147630
    void decrease(int n)
90
    {
91
10147630
      Assert(inHeap(n));
92
10147630
      percolateUp(indices[n]);
93
10147630
    }
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
6795271
    void insert(int n)
112
    {
113
6795271
        indices.growTo(n+1, -1);
114
6795271
        Assert(!inHeap(n));
115
116
6795271
        indices[n] = heap.size();
117
6795271
        heap.push(n);
118
6795271
        percolateUp(indices[n]);
119
6795271
    }
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
16985
    void build(vec<int>& ns) {
136
1696230
        for (int i = 0; i < heap.size(); i++)
137
1679245
            indices[heap[i]] = -1;
138
16985
        heap.clear();
139
140
1427504
        for (int i = 0; i < ns.size(); i++){
141
1410519
            indices[ns[i]] = i;
142
1410519
            heap.push(ns[i]); }
143
144
719415
        for (int i = heap.size() / 2 - 1; i >= 0; i--)
145
702430
            percolateDown(i);
146
16985
    }
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