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  * HASH CONSING FOR ARRAYS OF INTEGERS
21  */
22 
23 #ifndef __INT_ARRAY_HSETS_H
24 #define __INT_ARRAY_HSETS_H
25 
26 #include <stdint.h>
27 #include <stdbool.h>
28 
29 
30 /*
31  * Array descriptor:
32  * - hash = hash code
33  * - nelems = number of elements
34  * - data = array of elements
35  */
36 typedef struct harray_s {
37   uint32_t hash;
38   uint32_t nelems;
39   int32_t data[0]; // real size = nelems
40 } harray_t;
41 
42 #define MAX_HARRAY_SIZE ((UINT32_MAX-sizeof(harray_t))/sizeof(int32_t))
43 
44 
45 /*
46  * Table of arrays for hash consing
47  */
48 typedef struct int_array_hset_s {
49   harray_t **data;
50   uint32_t size;
51   uint32_t nelems;
52   uint32_t ndeleted;
53   uint32_t resize_threshold;
54   uint32_t cleanup_threshold;
55 } int_array_hset_t;
56 
57 
58 /*
59  * Default and max size
60  */
61 #define DEF_INT_ARRAY_HSET_SIZE 64
62 #define MAX_INT_ARRAY_HSET_SIZE (UINT32_MAX/sizeof(harray_t*))
63 
64 /*
65  * Ratios: resize_threshold = size * RESIZE_RATIO
66  *         cleanup_threshold = size * CLEANUP_RATIO
67  */
68 #define INT_ARRAY_HSET_RESIZE_RATIO 0.6
69 #define INT_ARRAY_HSET_CLEANUP_RATIO 0.2
70 
71 /*
72  * Marker for deleted sets
73  */
74 #define DELETED_HARRAY ((harray_t *) 1)
75 
76 
77 /*
78  * Initialize a set
79  * - n = initial size: must be a power of 2
80  * - if n = 0 the default size is used
81  */
82 extern void init_int_array_hset(int_array_hset_t *set, uint32_t n);
83 
84 
85 /*
86  * Delete
87  */
88 extern void delete_int_array_hset(int_array_hset_t *set);
89 
90 
91 /*
92  * Empty the set
93  */
94 extern void reset_int_array_hset(int_array_hset_t *set);
95 
96 
97 /*
98  * Find array a[0 .. n-1]
99  * - a[0 ... n-1] must be an array of n elements
100  * - return NULL if it's not in the set
101  */
102 extern harray_t *int_array_hset_find(int_array_hset_t *set, uint32_t n, int32_t *a);
103 
104 
105 /*
106  * Get descriptor for a[0 ... n-1]. Create it if it's not in set already.
107  */
108 extern harray_t *int_array_hset_get(int_array_hset_t *set, uint32_t n, int32_t *a);
109 
110 
111 /*
112  * Remove set a[0...n-1] from the set
113  * - no change if a is not present
114  */
115 extern void int_array_hset_remove(int_array_hset_t *set, uint32_t n, int32_t *a);
116 
117 
118 /*
119  * Remove all arrays that satisfy f
120  * - for every array a in the table, call f(aux, a)
121  * - if that returns true, then a is deleted
122  * - f must not have side effects
123  */
124 typedef bool (*int_array_hset_filter_t)(void *aux, const harray_t *a);
125 
126 extern void int_array_hset_remove_arrays(int_array_hset_t *set, void *aux, int_array_hset_filter_t f);
127 
128 
129 
130 #endif /* __INT_ARRAY_HSETS_H */
131