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

28.57

/src/utils/int_harray_store.h

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2019 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/>.
 */

/*
 * STORE OF HASH-CONS'ED SETS/ARRAYS OF INTEGERS
 */

#ifndef __INT_HARRAY_STORE_H
#define __INT_HARRAY_STORE_H

#include <stddef.h>
#include <stdint.h>

#include "utils/int_array_hsets.h"
#include "utils/int_hash_sets.h"
#include "utils/int_vectors.h"

/*
 * Store: 
 * - hash-set for arrays themselves
 * - all arrays stored in hset are sorted in increasing order
 * - aux & buffer are used internally for computing unions
 */
typedef struct int_harray_store_s {
  int_array_hset_t hset;
  ivector_t buffer;
  int_hset_t aux;
} int_harray_store_t;


/*
 * Initialize: use default sizes for all components
 */
extern void init_harray_store(int_harray_store_t *store);

/*
 * Delete: free memory
 */
extern void delete_harray_store(int_harray_store_t *store);

/*
 * Reset: remove all elements from hset
 */
extern void reset_harray_store(int_harray_store_t *store);


/*
 * Return the empty set
 */
static inline harray_t *empty_harray(int_harray_store_t *store) {
  return int_array_hset_get(&store->hset, 0, NULL);
}

/*
 * Singleton set { x }
 */
static inline harray_t *singleton_harray(int_harray_store_t *store, int32_t x) {
  return int_array_hset_get(&store->hset, 1, &x);
}

/*
 * Construct the set that contains elements x[0]  ... x[n-1]
 * - this sorts array x and removes duplicates then constructs the harray
 * - x may be modified.
 */
extern harray_t *make_harray(int_harray_store_t *store, uint32_t n, int32_t *x);

/*
 * Construct the union of two sets
 * - a and b must be from the store
 */
extern harray_t *merge_two_harrays(int_harray_store_t *store, harray_t *a, harray_t *b);

/*
 * Construct the union of n sets a[0 ... n-1]
 * - a may be modified
 * - return the empty set if n is zero
 */
extern harray_t *merge_harrays(int_harray_store_t *store, harray_t **a, uint32_t n);

/*
 * Return a - { x[0] .... x[n-1] }
 */
extern harray_t *harray_remove_elem(int_harray_store_t *store, harray_t *a, uint32_t n, int32_t *x);


/*
 * Remove arrays that satisfy f (cf. int_array_hsets.h)
 */
static inline void harray_store_remove_arrays(int_harray_store_t *store, void *aux, int_array_hset_filter_t f) {
  int_array_hset_remove_arrays(&store->hset, aux, f);
}


#endif /* __INT_HARRAY_STORE_H */

1	/*
2	* This file is part of the Yices SMT Solver.
3	* Copyright (C) 2019 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	* STORE OF HASH-CONS'ED SETS/ARRAYS OF INTEGERS
21	*/
22
23	#ifndef __INT_HARRAY_STORE_H
24	#define __INT_HARRAY_STORE_H
25
26	#include <stddef.h>
27	#include <stdint.h>
28
29	#include "utils/int_array_hsets.h"
30	#include "utils/int_hash_sets.h"
31	#include "utils/int_vectors.h"
32
33	/*
34	* Store:
35	* - hash-set for arrays themselves
36	* - all arrays stored in hset are sorted in increasing order
37	* - aux & buffer are used internally for computing unions
38	*/
39	typedef struct int_harray_store_s {
40	int_array_hset_t hset;
41	ivector_t buffer;
42	int_hset_t aux;
43	} int_harray_store_t;
44
45
46	/*
47	* Initialize: use default sizes for all components
48	*/
49	extern void init_harray_store(int_harray_store_t *store);
50
51	/*
52	* Delete: free memory
53	*/
54	extern void delete_harray_store(int_harray_store_t *store);
55
56	/*
57	* Reset: remove all elements from hset
58	*/
59	extern void reset_harray_store(int_harray_store_t *store);
60
61
62	/*
63	* Return the empty set
64	*/
65	static inline harray_t empty_harray(int_harray_store_t store) {	42,866✔
66	return int_array_hset_get(&store->hset, 0, NULL);	42,866✔
67	}
68
69	/*
70	* Singleton set { x }
71	*/
72	static inline harray_t singleton_harray(int_harray_store_t store, int32_t x) {	×
73	return int_array_hset_get(&store->hset, 1, &x);	×
74	}
75
76	/*
77	* Construct the set that contains elements x[0] ... x[n-1]
78	* - this sorts array x and removes duplicates then constructs the harray
79	* - x may be modified.
80	*/
81	extern harray_t make_harray(int_harray_store_t store, uint32_t n, int32_t *x);
82
83	/*
84	* Construct the union of two sets
85	* - a and b must be from the store
86	*/
87	extern harray_t merge_two_harrays(int_harray_store_t store, harray_t a, harray_t b);
88
89	/*
90	* Construct the union of n sets a[0 ... n-1]
91	* - a may be modified
92	* - return the empty set if n is zero
93	*/
94	extern harray_t merge_harrays(int_harray_store_t store, harray_t **a, uint32_t n);
95
96	/*
97	* Return a - { x[0] .... x[n-1] }
98	*/
99	extern harray_t harray_remove_elem(int_harray_store_t store, harray_t a, uint32_t n, int32_t x);
100
101
102	/*
103	* Remove arrays that satisfy f (cf. int_array_hsets.h)
104	*/
105	static inline void harray_store_remove_arrays(int_harray_store_t store, void aux, int_array_hset_filter_t f) {	×
106	int_array_hset_remove_arrays(&store->hset, aux, f);	×
107	}	×
108
109
110	#endif /* __INT_HARRAY_STORE_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