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