GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/bvminisat/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 BVMinisat_Heap_h
22
#define BVMinisat_Heap_h
23
24
#include "base/check.h"
25
#include "prop/bvminisat/mtl/Vec.h"
26
27
namespace CVC4 {
28
namespace BVMinisat {
29
30
//=================================================================================================
31
// A heap implementation with support for decrease/increase key.
32
33
34
template<class Comp>
35
17948
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
560709180
    static inline int left  (int i) { return i*2+1; }
42
514851020
    static inline int right (int i) { return (i+1)*2; }
43
172421854
    static inline int parent(int i) { return (i-1) >> 1; }
44
45
46
47060422
    void percolateUp(int i)
47
    {
48
47060422
        int x  = heap[i];
49
47060422
        int p  = parent(i);
50
51
297783286
        while (i != 0 && lt(x, heap[p])){
52
125361432
            heap[i]          = heap[p];
53
125361432
            indices[heap[p]] = i;
54
125361432
            i                = p;
55
125361432
            p                = parent(p);
56
        }
57
47060422
        heap   [i] = x;
58
47060422
        indices[x] = i;
59
47060422
    }
60
61
62
48212442
    void percolateDown(int i)
63
    {
64
48212442
        int x = heap[i];
65
406775950
        while (left(i) < heap.size()){
66
212293471
            int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
67
212293471
            if (!lt(heap[child], x)) break;
68
179281754
            heap[i]          = heap[child];
69
179281754
            indices[heap[i]] = i;
70
179281754
            i                = child;
71
        }
72
48212442
        heap   [i] = x;
73
48212442
        indices[x] = i;
74
48212442
    }
75
76
77
  public:
78
17954
    Heap(const Comp& c) : lt(c) { }
79
80
5671
    int  size      ()          const { return heap.size(); }
81
29556456
    bool empty     ()          const { return heap.size() == 0; }
82
333816970
    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
15218680
    void decrease(int n)
90
    {
91
15218680
      Assert(inHeap(n));
92
15218680
      percolateUp(indices[n]);
93
15218680
    }
94
17712056
    void increase(int n)
95
    {
96
17712056
      Assert(inHeap(n));
97
17712056
      percolateDown(indices[n]);
98
17712056
    }
99
100
    // Safe variant of insert/decrease/increase:
101
165789
    void update(int n)
102
    {
103
165789
        if (!inHeap(n))
104
842
            insert(n);
105
        else {
106
164947
            percolateUp(indices[n]);
107
164947
            percolateDown(indices[n]); }
108
165789
    }
109
110
111
31676795
    void insert(int n)
112
    {
113
31676795
        indices.growTo(n+1, -1);
114
31676795
        Assert(!inHeap(n));
115
116
31676795
        indices[n] = heap.size();
117
31676795
        heap.push(n);
118
31676795
        percolateUp(indices[n]);
119
31676795
    }
120
121
122
29546167
    int  removeMin()
123
    {
124
29546167
        int x            = heap[0];
125
29546167
        heap[0]          = heap.last();
126
29546167
        indices[heap[0]] = 0;
127
29546167
        indices[x]       = -1;
128
29546167
        heap.pop();
129
29546167
        if (heap.size() > 1) percolateDown(0);
130
29546167
        return x;
131
    }
132
133
134
    // Rebuild the heap from scratch, using the elements in 'ns':
135
1610
    void build(vec<int>& ns) {
136
1624070
        for (int i = 0; i < heap.size(); i++)
137
1622460
            indices[heap[i]] = -1;
138
1610
        heap.clear();
139
140
1620251
        for (int i = 0; i < ns.size(); i++){
141
1618641
            indices[ns[i]] = i;
142
1618641
            heap.push(ns[i]); }
143
144
810576
        for (int i = heap.size() / 2 - 1; i >= 0; i--)
145
808966
            percolateDown(i);
146
1610
    }
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
} /* CVC4::BVMinisat namespace */
159
} /* CVC4 namespace */
160
161
162
#endif