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 * SUPPORT FOR BREAKING SYMMETRIES IN UF FORMULAS 21 */ 22 23 #ifndef __SYMMETRY_BREAKING_H 24 #define __SYMMETRY_BREAKING_H 25 26 #include <stdint.h> 27 #include <setjmp.h> 28 29 #include "context/context_types.h" 30 #include "terms/term_manager.h" 31 #include "utils/csets.h" 32 #include "utils/int_hash_sets.h" 33 #include "utils/int_queues.h" 34 #include "utils/int_stack.h" 35 #include "utils/int_vectors.h" 36 37 38 /* 39 * RANGE CONSTRAINTS 40 */ 41 42 /* 43 * An assertion f is a range constraint if it's equivalent to 44 * a formula of the form (or (= t c_1) .... (= t c_n)) 45 * where c_1 ... c_n are distinct uninterpreted constants 46 * and t is a term. 47 * 48 * We collect such assertions into an array of range-constraint records: 49 * - each record stores the terms [c1 ... c_n] 50 * + a set of terms t_1 .... t_m and a set of indices i_1 .... i_m 51 * - for each index i_j in { i_1 ,.... i_m }, the 52 * assertion ctx->top_formula[i_j] is a range constraint 53 * equivalent to (or (= t_j c1) .... (= t_j c_n)) 54 * - every c_i and every t_j is a root term in ctx->intern 55 * 56 * We want to be able to check inclusion between sets of constants in 57 * different constraints. To accelerate this, we store a 32bit hash 58 * used as a bit map: 59 * - bit i of hash is 1 if there's a constant c_j such that (c_j mod 32) = i 60 */ 61 62 /* 63 * Range-constraint record: 64 * - cst[0 ... nc - 1] = the constants 65 * - trm[0 ... nt - 1] = the terms 66 * idx[0 ... nt - 1] = the corresponding indices 67 * - num_constants = nc number of constants 68 * - hash = bit map 69 * - num_terms = nt = number of terms 70 * size = size of arrays trm and idx 71 * The constants in cst are sorted (in increasing order). 72 */ 73 typedef struct rng_record_s { 74 term_t *cst; 75 term_t *trm; 76 uint32_t *idx; 77 uint32_t num_constants; 78 uint32_t hash; 79 uint32_t num_terms; 80 uint32_t size; 81 } rng_record_t; 82 83 #define DEF_RNG_RECORD_SIZE 20 84 #define MAX_RNG_RECORD_SIZE (UINT32_MAX/sizeof(term_t)) 85 86 87 /* 88 * Array/vector of these records 89 */ 90 typedef struct rng_vector_s { 91 rng_record_t *data; 92 uint32_t nelems; 93 uint32_t size; 94 } rng_vector_t; 95 96 #define DEF_RNG_VECTOR_SIZE 2 97 #define MAX_RNG_VECTOR_SIZE (UINT32_MAX/sizeof(rng_record_t)) 98 99 100 101 /* 102 * SUBSTITUTION 103 */ 104 105 /* 106 * To check whether a set of assertions is invariant by permutations 107 * of a set of constants {c_0. ,,, c_n}, we check invariance for 108 * - the permutation that swaps c_0 and c_1 109 * - the circular permutation c_0 := c_1, ...., c_n := c_0 110 * 111 * We need to apply such substitutions in the assertion context (i,e., 112 * by taking into account the internalization table). We use the following 113 * data structure to store a substitution and its results. 114 * - array subst[t] = result of applying the substitution to term index t 115 * or -1 if it's not computed yet. 116 * - nterms = initialization bound: for any t in 0 ... nterms, subst[t] is 117 * defined or initialized (i.e, NULL_TERM) 118 * - size = full size of the array. 119 * Subst is a mapping from term indices to terms 120 * 121 * Auxiliary data structures: 122 * - mngr = term manager for term construction/simplification 123 * - stack for allocation of integer arrays (in recursive calls) 124 * - env = jmp buffer to exception handling 125 */ 126 typedef struct ctx_subst_s { 127 intern_tbl_t *intern; 128 term_table_t *terms; 129 term_t *subst; 130 uint32_t nterms; 131 uint32_t size; 132 term_manager_t mngr; 133 int_stack_t stack; 134 jmp_buf env; 135 } ctx_subst_t; 136 137 #define DEF_CTX_SUBST_SIZE 100 138 #define MAX_CTX_SUBST_SIZE (UINT32_MAX/sizeof(term_t)) 139 140 141 /* 142 * Arrays used during symmetry breaking 143 * 144 * Given a fixed set of constants C0 (obtained from a rng_record_t), 145 * we keep three subsets of C0: 146 * - available = constants that don't occur in any symmetry breaking clause 147 * - used = complement of available = set of constants already used 148 * - removed = auxiliary set: this is a subset of available that's added 149 * to used at every iteration 150 * 151 * We use the following data structures: 152 * - constants = fixed array of constants 153 * - num_constants = size of this array 154 * - available = set of indices in [0 ... num_constants - 1] (as a cset) 155 * - removed = set of indices in [0 ... num_constants - 1] (as a cset too) 156 * - used = array of constants 157 * - num_used = number of elements in this array 158 * 159 * Initially: 160 * - available := full set 161 * - removed := empty set 162 * - used := empty array 163 * 164 * At each iteration: we select a term t and generate a symmetry breaking 165 * clause for t. The sets are updated as follows: 166 * - removed := available \inter constants of t 167 * a := a constant of available that's not in removed 168 * - used := used \union removed 169 * - available := available \minus removed 170 * 171 * Set of candidates: 172 * - we store the set of candidate terms in an array candidates 173 * - num_candidates = number of elements in this array 174 * - for each i in [0 ... num_candidates - 1], we keep 175 * cost[i] = cost of candidates[i] 176 * hash[i] = hash code for accelerating processing of candidates[i] 177 * 178 * - cost[i] is the size of the set of constants of candidates[i] 179 * that also occur in 'available'. If term t = candidates[i] is 180 * selected then we'll remove cost[i]+1 constants from 'available' and 181 * move them to 'used'. 182 * 183 * - hash[i] is a 32bit hash of the set of constants occurring in 184 * candidates[i] and in 'available'. In each iteration, we check 185 * whether (hash[i] & removed->hash) is 0. If so, cost[i] and hash[i] 186 * don't change. 187 */ 188 typedef struct sym_breaker_sets_s { 189 // fixed part 190 term_t *constants; 191 uint32_t num_constants; 192 193 // subsets 194 cset_t available; 195 cset_t removed; 196 term_t *used; 197 uint32_t num_used; 198 uint32_t used_size; 199 200 // candidate set + scores 201 term_t *candidates; 202 uint32_t *cost; 203 uint32_t *hash; 204 uint32_t num_candidates; 205 uint32_t candidate_size; 206 207 // auxiliary vector to compute constants of a term 208 ivector_t aux; 209 } sym_breaker_sets_t; 210 211 212 #define MAX_SBREAK_SET_SIZE (UINT32_MAX/sizeof(term_t)) 213 214 215 /* 216 * Symmetry breaker 217 * - pointers to the relevant context + term table 218 * - vector of range constraint descriptors 219 * - substitution 220 * - auxiliary structures to explore terms 221 */ 222 typedef struct sym_breaker_s { 223 context_t *ctx; 224 term_table_t *terms; 225 226 // vector of range_constraints 227 rng_vector_t range_constraints; 228 229 // array for sorting and removing subsumed constraints 230 rng_record_t **sorted_constraints; 231 uint32_t num_constraints; // size of this array 232 233 // sets used for symmetry breaking 234 sym_breaker_sets_t sets; 235 236 // auxiliary structures 237 int_queue_t queue; 238 int_hset_t cache; 239 ivector_t aux; 240 } sym_breaker_t; 241 242 243 244 245 /* 246 * OPERATIONS 247 */ 248 249 /* 250 * Initialize sym_breaker 251 * - ctx = relevant context 252 */ 253 extern void init_sym_breaker(sym_breaker_t *breaker, context_t *ctx); 254 255 256 /* 257 * Delete it: free all memory it uses 258 */ 259 extern void delete_sym_breaker(sym_breaker_t *breaker); 260 261 262 /* 263 * Collect all domain constraints from ctx->top_formulas 264 * - all constraints found are added the range_constraint record 265 */ 266 extern void collect_range_constraints(sym_breaker_t *breaker); 267 268 269 /* 270 * Check whether the assertions are invariant by permutation of 271 * constants in record r. 272 */ 273 extern bool check_assertion_invariance(sym_breaker_t *breaker, rng_record_t *r); 274 275 276 /* 277 * Check whether r1's constant set is included (strictly) in r2's constant set 278 */ 279 extern bool range_record_subset(rng_record_t *r1, rng_record_t *r2); 280 281 282 /* 283 * Copy r into set structure s 284 * - constants of r are stored in s->cst 285 * - s->used_cst is reset 286 * - terms of r are stored in s->candidates 287 */ 288 extern void breaker_sets_copy_record(sym_breaker_sets_t *s, rng_record_t *r); 289 290 291 /* 292 * Add candidates of r into s 293 * - this should be done only if r->cst is a subset of s->cst 294 */ 295 extern void breaker_sets_add_record(sym_breaker_sets_t *s, rng_record_t *r); 296 297 298 /* 299 * Break symmetries using s 300 */ 301 extern void break_symmetries(sym_breaker_t *breaker, sym_breaker_sets_t *s); 302 303 304 305 306 307 308 #endif /* __SYMMETRY_BREAKING_H */ 309