|
1 |
| package org.sat4j.minisat.core; |
|
2 |
| |
|
3 |
| import java.io.Serializable; |
|
4 |
| |
|
5 |
| import org.sat4j.core.VecInt; |
|
6 |
| import org.sat4j.specs.IVecInt; |
|
7 |
| |
|
8 |
| public class Heap implements Serializable { |
|
9 |
| |
|
10 |
| |
|
11 |
| |
|
12 |
| |
|
13 |
| private static final long serialVersionUID = 1L; |
|
14 |
| |
|
15 |
1173976159
| private final static int left(int i) {
|
|
16 |
1173976159
| return i<<1;
|
|
17 |
| } |
|
18 |
| |
|
19 |
1027679140
| private final static int right(int i) {
|
|
20 |
1027679140
| return (i<<1)^1;
|
|
21 |
| } |
|
22 |
| |
|
23 |
| private final static int parent(int i) { |
|
24 |
| return i >> 1; |
|
25 |
| } |
|
26 |
| |
|
27 |
| private final boolean comp(int a, int b) { |
|
28 |
| return activity[a] > activity[b]; |
|
29 |
| } |
|
30 |
| |
|
31 |
| private final IVecInt heap = new VecInt(); |
|
32 |
| |
|
33 |
| private final IVecInt indices = new VecInt(); |
|
34 |
| |
|
35 |
| private final double [] activity; |
|
36 |
| |
|
37 |
839442624
| @SuppressWarnings("PMD")
|
|
38 |
| final void percolateUp(int i) { |
|
39 |
839442624
| int x = heap.get(i);
|
|
40 |
839442624
| while (parent(i) != 0 && comp(x, heap.get(parent(i)))) {
|
|
41 |
614246023
| heap.set(i, heap.get(parent(i)));
|
|
42 |
614246023
| indices.set(heap.get(i), i);
|
|
43 |
614246023
| i = parent(i);
|
|
44 |
| } |
|
45 |
839442624
| heap.set(i, x);
|
|
46 |
839442624
| indices.set(x, i);
|
|
47 |
| } |
|
48 |
| |
|
49 |
96752798
| final void percolateDown(int i) {
|
|
50 |
96752798
| int x = heap.get(i);
|
|
51 |
96752798
| while (left(i) < heap.size()) {
|
|
52 |
439483248
| int child = right(i) < heap.size()
|
|
53 |
| && comp(heap.get(right(i)), heap.get(left(i))) ? right(i) |
|
54 |
| : left(i); |
|
55 |
439483248
| if (!comp(heap.get(child), x))
|
|
56 |
35639935
| break;
|
|
57 |
403843313
| heap.set(i, heap.get(child));
|
|
58 |
403843313
| indices.set(heap.get(i), i);
|
|
59 |
403843313
| i = child;
|
|
60 |
| } |
|
61 |
96752798
| heap.set(i, x);
|
|
62 |
96752798
| indices.set(x, i);
|
|
63 |
| } |
|
64 |
| |
|
65 |
| boolean ok(int n) { |
|
66 |
| return n >= 0 && n < indices.size(); |
|
67 |
| } |
|
68 |
| |
|
69 |
1249
| public Heap(double [] activity) {
|
|
70 |
1249
| this.activity = activity;
|
|
71 |
1249
| heap.push(-1);
|
|
72 |
| } |
|
73 |
| |
|
74 |
1248
| public void setBounds(int size) {
|
|
75 |
| assert (size >= 0); |
|
76 |
1248
| indices.growTo(size, 0);
|
|
77 |
| } |
|
78 |
| |
|
79 |
2034112175
| public boolean inHeap(int n) {
|
|
80 |
| assert (ok(n)); |
|
81 |
2034112175
| return indices.get(n) != 0;
|
|
82 |
| } |
|
83 |
| |
|
84 |
741890987
| public void increase(int n) {
|
|
85 |
| assert (ok(n)); |
|
86 |
| assert (inHeap(n)); |
|
87 |
741890987
| percolateUp(indices.get(n));
|
|
88 |
| } |
|
89 |
| |
|
90 |
96752823
| public boolean empty() {
|
|
91 |
96752823
| return heap.size() == 1;
|
|
92 |
| } |
|
93 |
| |
|
94 |
97551637
| public void insert(int n) {
|
|
95 |
| assert (ok(n)); |
|
96 |
97551637
| indices.set(n, heap.size());
|
|
97 |
97551637
| heap.push(n);
|
|
98 |
97551637
| percolateUp(indices.get(n));
|
|
99 |
| } |
|
100 |
| |
|
101 |
96752831
| public int getmin() {
|
|
102 |
96752831
| int r = heap.get(1);
|
|
103 |
96752831
| heap.set(1, heap.last());
|
|
104 |
96752831
| indices.set(heap.get(1), 1);
|
|
105 |
96752831
| indices.set(r, 0);
|
|
106 |
96752831
| heap.pop();
|
|
107 |
96752831
| if (heap.size() > 1)
|
|
108 |
96752798
| percolateDown(1);
|
|
109 |
96752831
| return r;
|
|
110 |
| } |
|
111 |
| |
|
112 |
0
| public boolean heapProperty() {
|
|
113 |
0
| return heapProperty(1);
|
|
114 |
| } |
|
115 |
| |
|
116 |
0
| public boolean heapProperty(int i) {
|
|
117 |
0
| return i >= heap.size()
|
|
118 |
| || ((parent(i) == 0 || !comp(heap.get(i), heap.get(parent(i)))) |
|
119 |
| && heapProperty(left(i)) && heapProperty(right(i))); |
|
120 |
| } |
|
121 |
| |
|
122 |
| } |
