12367760548

Committed 17 Dec 2024 06:41AM UTC coverage: 65.285% (-0.6%) from 65.92%

Build # 12367760548

Build Type

push

github

Committed by

web-flow

Commit Message

Fixes GitHub coverage issue (#544)

* Update action.yml

* Update action.yml

Run Details

81020 of 124102 relevant lines covered (65.29%)

1509382.01 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

66.67

/src/utils/generic_heap.h

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */

/*
 * BINARY HEAP OF INTEGERS WITH CUSTOMIZABLE ORDERING
 * - stores a set of integers, all in range [0 ... n]
 * - the ordering is defined by a function provided when
 *   the heap is constructed
 */

#ifndef __GENERIC_HEAP_H
#define __GENERIC_HEAP_H

#include <stdint.h>
#include <stdbool.h>
#include <assert.h>


/*
 * Function type for comparison functions
 * - the function is called as cmp(user_data, x, y)
 *   where x and y are distinct elements in the heap
 * - it must return true for x < y, false otherwise
 * - user_data is a generic void * pointer
 */
typedef bool (* heap_cmp_fun_t)(void *data, int32_t x, int32_t y);


/*
 * Heap structure
 * - nelems = number of elements stored in the heap
 * - heap = array of integers
 *   heap[0] is a marker
 *   heap[1 ... nelems] contains the rest (as a binary tree)
 * - idx = array [0 ... n]:
 *   if x is in the heap then idx[x] = i such that heap[i] = x
 *   if x is not in the heap then idx[x] = -1
 * - size = full size of array heap
 * - idx_size = size of the heap_index array
 *
 * The ordering is defined by heap->cmp and heap->data
 * - both are setup when the heap is initialized
 */
typedef struct generic_heap_s {
  // the heap itself
  int32_t *heap;
  uint32_t nelems;
  uint32_t size;
  // index array and its size
  int32_t *idx;
  uint32_t idx_size;
  // ordering
  heap_cmp_fun_t cmp;
  void *data;
} generic_heap_t;

#define DEF_GENERIC_HEAP_SIZE 80
#define MAX_GENERIC_HEAP_SIZE (UINT32_MAX/4)

#define DEF_GENERIC_HEAP_IDX_SIZE 80
#define MAX_GENERIC_HEAP_IDX_SIZE (UINT32_MAX/4)



/*
 * Initialize heap:
 * - n = initial size. If n=0, the default is used.
 * - m = initial size of idx. If m=0, the default is used.
 * - cmp = the comparison function
 * - data = some data used for computing the ordering
 */
extern void init_generic_heap(generic_heap_t *heap, uint32_t n, uint32_t m,
                              heap_cmp_fun_t cmp, void *data);


/*
 * Delete: free all memory
 */
extern void delete_generic_heap(generic_heap_t *heap);


/*
 * Empty the heap
 */
extern void reset_generic_heap(generic_heap_t *heap);


/*
 * Add element x: do nothing is x is in the heap already
 * - x must be non-negative
 */
extern void generic_heap_add(generic_heap_t *heap, int32_t x);


/*
 * Remove element x. Do nothing if x is not in the heap
 * - x must be non-negative
 */
extern void generic_heap_remove(generic_heap_t *heap, int32_t x);


/*
 * Check whether the heap is empty
 */
static inline bool generic_heap_is_empty(generic_heap_t *heap) {
  return heap->nelems == 0;
}


/*
 * Number of elements
 */
static inline uint32_t generic_heap_nelems(generic_heap_t *heap) {
  return heap->nelems;
}



/*
 * Check whether x is in the heap
 */
static inline bool generic_heap_member(generic_heap_t *heap, int32_t x) {
  assert(0 <= x);
  return x < heap->idx_size && heap->idx[x] >= 0;
}

/*
 * Get the minimal element and remove it from the heap
 * - return -1 if the heap is empty
 */
extern int32_t generic_heap_get_min(generic_heap_t *heap);


/*
 * Return the minimal element but don't remove it
 * - return -1 if the heap is empty
 */
static inline int32_t generic_heap_top(generic_heap_t *heap) {
  return heap->nelems == 0 ? -1 : heap->heap[1];
}



/*
 * Update functions allow the position of an element x to change in
 * the ordering.
 * - move_up: if x is now smaller in the ordering (closer to min)
 * - move_down: if x is now larger in the ordering (further from min)
 * - update x: general form.
 * For all three functions, x must be present in the heap
 */
extern void generic_heap_move_up(generic_heap_t *heap, int32_t x);
extern void generic_heap_move_down(generic_heap_t *heap, int32_t x);
extern void generic_heap_update(generic_heap_t *heap, int32_t x);



#endif /* __GENERIC_HEAP_H */

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	* The ordering is defined by heap->cmp and heap->data
57	* - both are setup when the heap is initialized
58	*/
59	typedef struct generic_heap_s {
60	// the heap itself
61	int32_t *heap;
62	uint32_t nelems;
63	uint32_t size;
64	// index array and its size
65	int32_t *idx;
66	uint32_t idx_size;
67	// ordering
68	heap_cmp_fun_t cmp;
69	void *data;
70	} generic_heap_t;
71
72	#define DEF_GENERIC_HEAP_SIZE 80
73	#define MAX_GENERIC_HEAP_SIZE (UINT32_MAX/4)
74
75	#define DEF_GENERIC_HEAP_IDX_SIZE 80
76	#define MAX_GENERIC_HEAP_IDX_SIZE (UINT32_MAX/4)
77
78
79
80	/*
81	* Initialize heap:
82	* - n = initial size. If n=0, the default is used.
83	* - m = initial size of idx. If m=0, the default is used.
84	* - cmp = the comparison function
85	* - data = some data used for computing the ordering
86	*/
87	extern void init_generic_heap(generic_heap_t *heap, uint32_t n, uint32_t m,
88	heap_cmp_fun_t cmp, void *data);
89
90
91	/*
92	* Delete: free all memory
93	*/
94	extern void delete_generic_heap(generic_heap_t *heap);
95
96
97	/*
98	* Empty the heap
99	*/
100	extern void reset_generic_heap(generic_heap_t *heap);
101
102
103	/*
104	* Add element x: do nothing is x is in the heap already
105	* - x must be non-negative
106	*/
107	extern void generic_heap_add(generic_heap_t *heap, int32_t x);
108
109
110	/*
111	* Remove element x. Do nothing if x is not in the heap
112	* - x must be non-negative
113	*/
114	extern void generic_heap_remove(generic_heap_t *heap, int32_t x);
115
116
117	/*
118	* Check whether the heap is empty
119	*/
120	static inline bool generic_heap_is_empty(generic_heap_t *heap) {	11,451,432✔
121	return heap->nelems == 0;	11,451,432✔
122	}
123
124
125	/*
126	* Number of elements
127	*/
128	static inline uint32_t generic_heap_nelems(generic_heap_t *heap) {	×
129	return heap->nelems;	×
130	}
131
132
133
134	/*
135	* Check whether x is in the heap
136	*/
137	static inline bool generic_heap_member(generic_heap_t *heap, int32_t x) {	557,415✔
138	assert(0 <= x);
139	return x < heap->idx_size && heap->idx[x] >= 0;	557,415✔
140	}
141
142	/*
143	* Get the minimal element and remove it from the heap
144	* - return -1 if the heap is empty
145	*/
146	extern int32_t generic_heap_get_min(generic_heap_t *heap);
147
148
149	/*
150	* Return the minimal element but don't remove it
151	* - return -1 if the heap is empty
152	*/
153	static inline int32_t generic_heap_top(generic_heap_t *heap) {
154	return heap->nelems == 0 ? -1 : heap->heap[1];
155	}
156
157
158
159	/*
160	* Update functions allow the position of an element x to change in
161	* the ordering.
162	* - move_up: if x is now smaller in the ordering (closer to min)
163	* - move_down: if x is now larger in the ordering (further from min)
164	* - update x: general form.
165	* For all three functions, x must be present in the heap
166	*/
167	extern void generic_heap_move_up(generic_heap_t *heap, int32_t x);
168	extern void generic_heap_move_down(generic_heap_t *heap, int32_t x);
169	extern void generic_heap_update(generic_heap_t *heap, int32_t x);
170
171
172
173	#endif /* __GENERIC_HEAP_H */

SRI-CSL / yices2 / 12367760548

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous