1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 /*
20 * BINARY HEAP OF INTEGERS WITH CUSTOMIZABLE ORDERING
21 * - stores a set of integers, all in range [0 ... n]
22 * - the ordering is defined by a function provided when
23 * the heap is constructed
24 */
25
26 #ifndef __GENERIC_HEAP_H
27 #define __GENERIC_HEAP_H
28
29 #include <stdint.h>
30 #include <stdbool.h>
31 #include <assert.h>
32
33
34 /*
35 * Function type for comparison functions
36 * - the function is called as cmp(user_data, x, y)
37 * where x and y are distinct elements in the heap
38 * - it must return true for x < y, false otherwise
39 * - user_data is a generic void * pointer
40 */
41 typedef bool (* heap_cmp_fun_t)(void *data, int32_t x, int32_t y);
42
43
44 /*
45 * Heap structure
46 * - nelems = number of elements stored in the heap
47 * - heap = array of integers
48 * heap[0] is a marker
49 * heap[1 ... nelems] contains the rest (as a binary tree)
50 * - idx = array [0 ... n]:
51 * if x is in the heap then idx[x] = i such that heap[i] = x
52 * if x is not in the heap then idx[x] = -1
53 * - size = full size of array heap
54 * - idx_size = size of the heap_index array
55 *
56 * Ordering is defined by:
57 * - heap->cmp and heap->data
58 * - both are setup when the heap is initialized
59 */
60 typedef struct generic_heap_s {
61 // the heap itself
62 int32_t *heap;
63 uint32_t nelems;
64 uint32_t size;
65 // index array and its size
66 int32_t *idx;
67 uint32_t idx_size;
68 // ordering
69 heap_cmp_fun_t cmp;
70 void *data;
71 } generic_heap_t;
72
73 #define DEF_GENERIC_HEAP_SIZE 80
74 #define MAX_GENERIC_HEAP_SIZE (UINT32_MAX/4)
75
76 #define DEF_GENERIC_HEAP_IDX_SIZE 80
77 #define MAX_GENERIC_HEAP_IDX_SIZE (UINT32_MAX/4)
78
79
80
81 /*
82 * Initialize heap:
83 * - n = initial size. If n=0, the default is used.
84 * - m = initial size of idx. If m=0, the default is used.
85 * - cmp = the comparison function
86 * - data = some data used for computing the ordering
87 */
88 extern void init_generic_heap(generic_heap_t *heap, uint32_t n, uint32_t m,
89 heap_cmp_fun_t cmp, void *data);
90
91
92 /*
93 * Delete: free all memory
94 */
95 extern void delete_generic_heap(generic_heap_t *heap);
96
97
98 /*
99 * Empty the heap
100 */
101 extern void reset_generic_heap(generic_heap_t *heap);
102
103
104 /*
105 * Add element x: do nothing is x is in the heap already
106 * - x must be non-negative
107 */
108 extern void generic_heap_add(generic_heap_t *heap, int32_t x);
109
110
111 /*
112 * Remove element x. Do nothing if x is not in the heap
113 * - x must be non-negative
114 */
115 extern void generic_heap_remove(generic_heap_t *heap, int32_t x);
116
117
118 /*
119 * Check whether the heap is empty
120 */
generic_heap_is_empty(generic_heap_t * heap)121 static inline bool generic_heap_is_empty(generic_heap_t *heap) {
122 return heap->nelems == 0;
123 }
124
125
126 /*
127 * Number of elements
128 */
generic_heap_nelems(generic_heap_t * heap)129 static inline uint32_t generic_heap_nelems(generic_heap_t *heap) {
130 return heap->nelems;
131 }
132
133
134
135 /*
136 * Check whether x is in the heap
137 */
generic_heap_member(generic_heap_t * heap,int32_t x)138 static inline bool generic_heap_member(generic_heap_t *heap, int32_t x) {
139 assert(0 <= x);
140 return x < heap->idx_size && heap->idx[x] >= 0;
141 }
142
143 /*
144 * Get the minimal element and remove it from the heap
145 * - return -1 if the heap is empty
146 */
147 extern int32_t generic_heap_get_min(generic_heap_t *heap);
148
149
150 /*
151 * Return the minimal element but don't remove it
152 * - return -1 if the heap is empty
153 */
generic_heap_top(generic_heap_t * heap)154 static inline int32_t generic_heap_top(generic_heap_t *heap) {
155 return heap->nelems == 0 ? -1 : heap->heap[1];
156 }
157
158
159
160 /*
161 * Update functions allow the position of an element x to change in
162 * the ordering.
163 * - move_up: if x is now smaller in the ordering (closer to min)
164 * - move_down: if x is now larger in the ordering (further from min)
165 * - update x: general form.
166 * For all three functions, x must be present in the heap
167 */
168 extern void generic_heap_move_up(generic_heap_t *heap, int32_t x);
169 extern void generic_heap_move_down(generic_heap_t *heap, int32_t x);
170 extern void generic_heap_update(generic_heap_t *heap, int32_t x);
171
172
173
174 #endif /* __GENERIC_HEAP_H */
175