1 /* 2 * This file is part of the Yices SMT Solver. 3 * Copyright (C) 2020 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 TABLE FOR BOOLEAN GATES (ANOTHER ONE) 21 */ 22 23 #ifndef __NEW_GATE_HASH_MAP2_H 24 #define __NEW_GATE_HASH_MAP2_H 25 26 #include <stdint.h> 27 28 #include "solvers/cdcl/new_gates.h" 29 #include "solvers/cdcl/wide_truth_tables.h" 30 31 /* 32 * Keys are arrays of at most four Boolean variables var[0 .. 3]. 33 * Each key is mapped to a vector of pairs <truth-table, literal> 34 * 35 * We use the same conventions as in truth_tables.h and new_gates.h, 36 * except that we can have one more variable: 37 * 38 * Variable/key normalization 39 * -------------------------- 40 * For functions of arity 4: 0 <= var[0] < var[1] < var[2] < var[3] 41 * For functions of arity 3: 0 <= var[0] < var[1] < var[2] and var[3] = null_bvar 42 * For functions of arity 2: 0 <= var[0] < var[1] and var[2] = var[3] = null_bvar 43 * 44 * For functions of arity 1: 0 <= var[0] and var[1] = var[2] = var[3] = null_bvar 45 * Constant functions: var[0] = var[1] = var[2] = var[3] = null_bvar 46 * 47 * Truth table stored in 16bits 48 * ---------------------------- 49 * The truth table encodes f(var[0] ... var[3]) using 16 bits: 50 * - f(x0, x1, x2, x3) is stored in the i-th bit where i = 8*x0 + 4*x1 + 2*x2 + x3 51 * b0 = low order bit, ...., b15 = high-order bit 52 * 53 * For functions of arity 4, this looks like this 54 * 55 * var[0] var[1] var[2] var[3] f 56 * 0 0 0 0 b0 57 * 0 0 0 1 b1 58 * 0 0 1 0 b2 59 * 0 0 1 1 b3 60 * 0 1 0 0 b4 61 * 0 1 0 1 b5 62 * 0 1 1 0 b6 63 * 0 1 1 1 b7 64 * 1 0 0 0 b8 65 * 1 0 0 1 b9 66 * 1 0 1 0 b10 67 * 1 0 1 1 b11 68 * 1 1 0 0 b12 69 * 1 1 0 1 b13 70 * 1 1 1 0 b14 71 * 1 1 1 1 b15 72 * 73 * For functions of arity 3, var[3] is ignored: 74 * 75 * var[0] var[1] var[2] var[3] f 76 * 0 0 0 0 b0 77 * 0 0 0 1 b0 78 * 0 0 1 0 b1 79 * 0 0 1 1 b1 80 * 0 1 0 0 b2 81 * 0 1 0 1 b2 82 * 0 1 1 0 b3 83 * 0 1 1 1 b3 84 * 1 0 0 0 b4 85 * 1 0 0 1 b4 86 * 1 0 1 0 b5 87 * 1 0 1 1 b5 88 * 1 1 0 0 b6 89 * 1 1 0 1 b6 90 * 1 1 1 0 b7 91 * 1 1 1 1 b7 92 * 93 * For functions of arity 2, var[2] and var[3] are ignored: 94 * 95 * var[0] var[1] var[2] var[3] f 96 * 0 0 0 0 b0 97 * 0 0 0 1 b0 98 * 0 0 1 0 b0 99 * 0 0 1 1 b0 100 * 0 1 0 0 b1 101 * 0 1 0 1 b1 102 * 0 1 1 0 b1 103 * 0 1 1 1 b1 104 * 1 0 0 0 b2 105 * 1 0 0 1 b2 106 * 1 0 1 0 b2 107 * 1 0 1 1 b2 108 * 1 1 0 0 b3 109 * 1 1 0 1 b3 110 * 1 1 1 0 b3 111 * 1 1 1 1 b3 112 */ 113 114 /* 115 * Pairs truth-table/literal 116 */ 117 typedef struct gmap_entry_s { 118 uint32_t ttbl; 119 literal_t lit; 120 } gmap_entry_t; 121 122 /* 123 * Table element: 124 * - key = array of 4 variables 125 * - size and capacity 126 * - data = array of pairs 127 */ 128 typedef struct gmap_elem_s { 129 bvar_t var[4]; // key 130 uint32_t size; // size of the data array 131 uint32_t nelems; // number of elements in array data 132 gmap_entry_t data[0]; // real size given by size. 133 } gmap_elem_t; 134 135 136 #define GMAP_ELEM_DEF_SIZE 2 137 #define GMAP_ELEM_MAX_SIZE ((uint32_t)((UINT32_MAX-sizeof(gmap_elem_t))/sizeof(gmap_entry_t))) 138 139 /* 140 * Hash table 141 */ 142 typedef struct gmap_s { 143 gmap_elem_t **data; 144 uint32_t size; // power of two 145 uint32_t nelems; // number of elements in the table 146 uint32_t resize_threshold; 147 } gmap_t; 148 149 150 #define GMAP_DEF_SIZE 1024 151 #define GMAP_MAX_SIZE (UINT32_MAX/sizeof(gmap_elem_t *)) 152 #define GMAP_RESIZE_RATIO 0.6 153 /* 154 * Initialization: 155 * - n: initial size. Must be 0 or a power of 2. 156 * - if n is 0, the default is used. 157 */ 158 extern void init_gmap(gmap_t *gmap, uint32_t n); 159 160 /* 161 * Delete: free memory 162 */ 163 extern void delete_gmap(gmap_t *gmap); 164 165 /* 166 * Reset: empty the table 167 */ 168 extern void reset_gmap(gmap_t *gmap); 169 170 /* 171 * Search for a gate g and return the literal mapped to g. 172 * If g is not in the table, return null_literal. 173 */ 174 extern literal_t gmap_find(const gmap_t *gmap, const bgate_t *g); 175 176 /* 177 * Search for a gate g and return the literal mapped to g. 178 * If g is not in the table, add the gate and map it to l then return l. 179 */ 180 extern literal_t gmap_get(gmap_t *gmap, const bgate_t *g, literal_t l); 181 182 /* 183 * Variants: use ttbl instead of a gate g 184 * - ttbl must be normalized 185 */ 186 extern literal_t gmap_find_ttbl(const gmap_t *gmap, const ttbl_t *tt); 187 extern literal_t gmap_get_ttbl(gmap_t *gmap, const ttbl_t *tt, literal_t l); 188 189 190 /* 191 * More variants: use a wide truth table 192 * - w must be normalized and have no more than four variables. 193 */ 194 extern literal_t gmap_find_wide_ttbl(const gmap_t *gmap, const wide_ttbl_t *w); 195 extern literal_t gmap_get_wide_ttbl(gmap_t *gmap, const wide_ttbl_t *w, literal_t l); 196 197 198 199 #endif /* __NEG_GATE_HASH_MAP2_H */ 200