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 * Low-level objects in egraph
21 * (We need to separate these typedefs from the full egraph_types.h
22 * to break circular dependencies between include files).
23 */
24
25 #ifndef __EGRAPH_BASE_TYPES_H
26 #define __EGRAPH_BASE_TYPES_H
27
28 #include <stdint.h>
29 #include <stddef.h>
30
31 #include "solvers/cdcl/smt_core_base_types.h"
32
33
34 /***************************
35 * TERMS AND OCCURRENCES *
36 **************************/
37
38 typedef int32_t eterm_t;
39 typedef int32_t occ_t;
40
41 /*
42 * Maximal number of egraph terms
43 * - no more than 2^30 terms
44 * - we also want to compute (nterms * sizeof(void *)) without overflow
45 * The following limit is safe (but not optimal).
46 */
47 #define MAX_ETERMS (INT32_MAX>>3)
48
49 /*
50 * Conversion between terms and occurrences:
51 * - polarity bit is the low-order bit of a occurrence:
52 * 0 means positive, 1 means negative
53 */
pos_occ(eterm_t t)54 static inline occ_t pos_occ(eterm_t t) {
55 return (t << 1);
56 }
57
neg_occ(eterm_t t)58 static inline occ_t neg_occ(eterm_t t) {
59 return (t << 1) | 1;
60 }
61
62 // polarity 0 --> pos_occ(t), polarity 1 --> neg_occ(t)
mk_occ(eterm_t t,uint32_t polarity)63 static inline occ_t mk_occ(eterm_t t, uint32_t polarity) {
64 assert((polarity & ~1) == 0);
65 return (t << 1) | polarity;
66 }
67
term_of_occ(occ_t x)68 static inline eterm_t term_of_occ(occ_t x) {
69 return x>>1;
70 }
71
polarity_of_occ(occ_t x)72 static inline uint32_t polarity_of_occ(occ_t x) {
73 return ((uint32_t) x) & 1;
74 }
75
is_pos_occ(occ_t x)76 static inline bool is_pos_occ(occ_t x) {
77 return polarity_of_occ(x) == 0;
78 }
79
is_neg_occ(occ_t x)80 static inline bool is_neg_occ(occ_t x) {
81 return polarity_of_occ(x) != 0;
82 }
83
84 // complement of x = same term, opposite polarity
opposite_occ(occ_t x)85 static inline eterm_t opposite_occ(occ_t x) {
86 return x ^ 1;
87 }
88
89 /*
90 * Predefined term and occurrence ids
91 */
92 enum {
93 null_eterm = -1,
94 true_eterm = 0,
95
96 null_occurrence = -1,
97 true_occ = 0, // pos_occ(true_eterm)
98 false_occ = 1, // neg_occ(true_eterm)
99 };
100
101
102 /*
103 * Occurrence code for a boolean x
104 */
bool2occ(bool x)105 static inline occ_t bool2occ(bool x) {
106 assert(x == 0 || x == 1);
107 return x ^ 1;
108 }
109
110
111
112 /*************
113 * CLASSES *
114 ************/
115
116 /*
117 * Class ids and labels are signed integers
118 * A label is a class id + a polarity bit
119 */
120 typedef int32_t class_t;
121 typedef int32_t elabel_t;
122
pos_label(class_t i)123 static inline elabel_t pos_label(class_t i) {
124 return (i << 1);
125 }
126
neg_label(class_t i)127 static inline elabel_t neg_label(class_t i) {
128 return (i << 1) | 1;
129 }
130
class_of(elabel_t l)131 static inline class_t class_of(elabel_t l) {
132 return l >> 1;
133 }
134
sign_of(elabel_t l)135 static inline uint32_t sign_of(elabel_t l) {
136 return ((uint32_t) l) & 1;
137 }
138
is_pos_label(elabel_t l)139 static inline bool is_pos_label(elabel_t l) {
140 return sign_of(l) == 0;
141 }
142
is_neg_label(elabel_t l)143 static inline bool is_neg_label(elabel_t l) {
144 return sign_of(l) != 0;
145 }
146
opposite_label(elabel_t l)147 static inline elabel_t opposite_label(elabel_t l) {
148 return l ^ 1;
149 }
150
151 /*
152 * Predefined class and labels
153 */
154 enum {
155 null_class = -1,
156 null_label = -1,
157
158 bool_constant_class = 0,
159
160 true_label = 0, // pos_label(0)
161 false_label = 1, // neg_label(0)
162 };
163
164
165
166 /****************
167 * COMPOSITES *
168 ***************/
169
170 /*
171 * Different types of composite terms
172 *
173 * TODO? Possible optimization: we could use a special tag for
174 * equality between boolean terms.
175 */
176 typedef enum composite_kind {
177 COMPOSITE_APPLY,
178 COMPOSITE_UPDATE,
179 COMPOSITE_TUPLE,
180 COMPOSITE_EQ,
181 COMPOSITE_ITE,
182 COMPOSITE_DISTINCT,
183 COMPOSITE_OR,
184 COMPOSITE_LAMBDA,
185 } composite_kind_t;
186
187
188 /*
189 * Composite structures:
190 * - tag = arity + kind
191 * - hash = 32bit hash code used for congruence closure
192 * - id = term t: c->id = t iff body[t] = c
193 * - array of children
194 *
195 * For a composite of arity n, child has n elements to store the children
196 * and (optionally) n more elements (hooks).
197 * - the children ids (occ_t) are in cmp->child[0 ... n-1]
198 * - the hooks are in cmp->child[n ... 2n-1]
199 * - the hooks are indices into use vectors:
200 * if cmp is stored in parents[c] at some index k, i.e., we have
201 * cmp->child[i] = t label[t] = c parents[c]->data[k] = cmp
202 * then k is stored in cmp->child[i + n]
203 * - if cmp has several children in class c the hook is set on
204 * the first child of class c. The other hooks are negative.
205 * - this makes it easy and cheap to remove cmp from its parents
206 *
207 * A lambda composite cmp is of the form (lambda t) where t is a term
208 * occurrence
209 * - cmp has arity one but the array child has three elements:
210 * cmp->child[0] = t
211 * cmp->child[1] = hook as above
212 * cmp->child[2] = an integer tag (intended to encode the domain of the lambda term)
213 */
214 typedef struct composite_s {
215 uint32_t tag;
216 uint32_t hash;
217 eterm_t id;
218 int32_t child[0]; // real size depends on arity
219 } composite_t;
220
221 /*
222 * Special indices for child[i + n]
223 */
224 enum {
225 no_ptr = -1, // means not in a use vector
226 duplicate_ptr = -2, // means another child has the same class
227 };
228
229 /*
230 * 32 bit tags:
231 * 3 low-order bits encode the type,
232 * 29 high-order bits encode the arity.
233 */
234 #define CTAG_BITS 3
235 #define CTAG_MASK ((((uint32_t) 1) << CTAG_BITS) - 1)
236 #define CTAG_ARITYMASK (~CTAG_MASK)
237
238 /*
239 * Arity must fit in 29 bits. We also need to ensure
240 * (sizeof(composite_t) + 2.n * sizeof(int32_t)) does not overflow
241 */
242 #define MAX_COMPOSITE_ARITY ((UINT32_MAX>>CTAG_BITS)-sizeof(composite_t))
243
244
245 /*
246 * Tag constructors:
247 * - for variable arity terms, n = number of children
248 * - n == 0 is allowed
249 */
mk_composite_tag(composite_kind_t k,uint32_t n)250 static inline uint32_t mk_composite_tag(composite_kind_t k, uint32_t n) {
251 assert(n <= MAX_COMPOSITE_ARITY);
252 return (n << CTAG_BITS) | k;
253 }
254
mk_apply_tag(uint32_t n)255 static inline uint32_t mk_apply_tag(uint32_t n) {
256 return mk_composite_tag(COMPOSITE_APPLY, n);
257 }
258
mk_update_tag(uint32_t n)259 static inline uint32_t mk_update_tag(uint32_t n) {
260 return mk_composite_tag(COMPOSITE_UPDATE, n);
261 }
262
mk_tuple_tag(uint32_t n)263 static inline uint32_t mk_tuple_tag(uint32_t n) {
264 return mk_composite_tag(COMPOSITE_TUPLE, n);
265 }
266
mk_eq_tag(void)267 static inline uint32_t mk_eq_tag(void) {
268 return mk_composite_tag(COMPOSITE_EQ, 2);
269 }
270
mk_lambda_tag(void)271 static inline uint32_t mk_lambda_tag(void) {
272 return mk_composite_tag(COMPOSITE_LAMBDA, 1);
273 }
274
mk_distinct_tag(uint32_t n)275 static inline uint32_t mk_distinct_tag(uint32_t n) {
276 return mk_composite_tag(COMPOSITE_DISTINCT, n);
277 }
278
mk_ite_tag(void)279 static inline uint32_t mk_ite_tag(void) {
280 return mk_composite_tag(COMPOSITE_ITE, 3);
281 }
282
mk_or_tag(uint32_t n)283 static inline uint32_t mk_or_tag(uint32_t n) {
284 return mk_composite_tag(COMPOSITE_OR, n);
285 }
286
287
288 /*
289 * Extract kind and arity from a tag
290 */
tag_kind(uint32_t tag)291 static inline composite_kind_t tag_kind(uint32_t tag) {
292 return (composite_kind_t) (tag & CTAG_MASK);
293 }
294
tag_arity(uint32_t tag)295 static inline uint32_t tag_arity(uint32_t tag) {
296 return (uint32_t) (tag >> CTAG_BITS);
297 }
298
299
300 /*
301 * Extract components of a composite
302 */
composite_kind(composite_t * c)303 static inline composite_kind_t composite_kind(composite_t *c) {
304 return tag_kind(c->tag);
305 }
306
composite_arity(composite_t * c)307 static inline uint32_t composite_arity(composite_t *c) {
308 return tag_arity(c->tag);
309 }
310
composite_child(composite_t * c,uint32_t i)311 static inline occ_t composite_child(composite_t *c, uint32_t i) {
312 assert(i < composite_arity(c));
313 return c->child[i];
314 }
315
composite_hooks(composite_t * c)316 static inline int32_t *composite_hooks(composite_t *c) {
317 return c->child + composite_arity(c);
318 }
319
lambda_composite_tag(composite_t * c)320 static inline int32_t lambda_composite_tag(composite_t *c) {
321 assert(composite_kind(c) == COMPOSITE_LAMBDA);
322 return c->child[2];
323 }
324
325
326 /*
327 * Fake pointers (body of constants and variables)
328 * - low-order bit is 1
329 * - for a constant, we pack an integer id + 2 bit tag into the pointer
330 */
331 #define VARIABLE_BODY ((composite_t *)1)
332 #define CONSTANT_TAG ((size_t) 3)
333
mk_constant_body(int32_t i)334 static inline composite_t *mk_constant_body(int32_t i) {
335 return (composite_t *) ((((size_t) i) << 2) | CONSTANT_TAG);
336 }
337
atomic_body(composite_t * c)338 static inline bool atomic_body(composite_t *c) {
339 return (((size_t) c) & 0x1) != 0;
340 }
341
composite_body(composite_t * c)342 static inline bool composite_body(composite_t *c) {
343 return ! atomic_body(c);
344 }
345
constant_body(composite_t * c)346 static inline bool constant_body(composite_t *c) {
347 return (((size_t) c) & 0x3) == CONSTANT_TAG;
348 }
349
constant_body_id(composite_t * c)350 static inline int32_t constant_body_id(composite_t *c) {
351 assert(constant_body(c));
352 return (int32_t) (((size_t) c) >> 2);
353 }
354
355
356
357
358
359
360 /***********
361 * ATOMS *
362 **********/
363
364 /*
365 * An egraph atom is a pair <t, v>, where t is a boolean term in the egraph
366 * and v is the corresponding boolean variable in the core
367 * - the atom <t, v> is attached to variable v in the core
368 * - asserting v causes (t == true) to be pushed into the egraph queue;
369 * asserting (not v) causes (t == false) to be pushed into the queue.
370 * - the egraph can detect that atoms are equal, by congruence. To deal
371 * with this, we store the atoms into equivalence classes (via a circular
372 * linked list). If <t1, v1> and <t2, v2> are in the same class then
373 * either t1 == t2 or t1 == (not t2).
374 */
375 typedef struct atom_s atom_t;
376
377 struct atom_s {
378 eterm_t eterm; // egraph term
379 bvar_t boolvar; // core variable
380 atom_t *next; // successor in the class
381 };
382
383
384 /*
385 * Atom objects are allocated via an object store
386 * ATOM_BANK_SIZE is the number of atoms per object-store bank
387 */
388 #define ATOM_BANK_SIZE 256
389
390
391
392
393
394 /******************
395 * EGRAPH TYPES *
396 *****************/
397
398 /*
399 * Bool and tuple are interpreted internally by the egraph
400 * The other types are used for propagating equalities and disequalities
401 * to theory solvers. They identify the theory solver to contact:
402 * - int/real: arithmetic solver
403 * - bv: bitvector solver
404 * - others: specific subsolver (for now, the only known solver is the
405 * function theory solver).
406 */
407 typedef enum etype_s {
408 // etypes with satellite solvers
409 ETYPE_INT, // 0
410 ETYPE_REAL, // 1
411 ETYPE_BV, // 2
412 ETYPE_FUNCTION, // 3
413
414 // etypes internal to the egraph
415 ETYPE_BOOL, // 4
416 ETYPE_TUPLE, // 5
417 ETYPE_NONE, // 6
418
419 } etype_t;
420
421 #define NUM_ETYPES (ETYPE_NONE + 1)
422 #define NUM_SATELLITES (ETYPE_FUNCTION + 1)
423
424 /*
425 * tau is an arithmetic type if tau == 0 or 1
426 */
is_arith_etype(etype_t tau)427 static inline bool is_arith_etype(etype_t tau) {
428 assert(ETYPE_INT <= tau && tau <= ETYPE_NONE);
429 return tau <= 1;
430 }
431
432
433 /*
434 * Theory variables are integer too. null_thvar means no variable attached
435 */
436 typedef int32_t thvar_t;
437
438 enum {
439 null_thvar = -1,
440 };
441
442
443
444
445 /*****************
446 * ATOM TAGS *
447 ****************/
448
449 /*
450 * The egraph may need to propagate atoms to the arithmetic or bitvector solvers.
451 * We mark these atoms using a tag in the two lower order bits of atom pointers.
452 */
453 typedef enum atm_tag {
454 EGRAPH_ATM_TAG = 0,
455 ARITH_ATM_TAG = 1,
456 BV_ATM_TAG = 2,
457 } atm_tag_t;
458
459 #define ATM_TAG_MASK ((size_t) 0x3)
460
461 /*
462 * Get the tag of atm
463 */
atom_tag(void * atm)464 static inline atm_tag_t atom_tag(void *atm) {
465 return ((size_t) atm) & ATM_TAG_MASK;
466 }
467
468 /*
469 * Remove the tag of atm
470 */
untag_atom(void * atm)471 static inline void *untag_atom(void *atm) {
472 return (void *) (((size_t) atm) & ~ATM_TAG_MASK);
473 }
474
475 /*
476 * Attach a tag to a an atom pointer
477 */
tagged_egraph_atom(void * atm)478 static inline void *tagged_egraph_atom(void *atm) {
479 assert((((size_t) atm) & ATM_TAG_MASK) == 0);
480 return (void *)(((size_t) atm) | EGRAPH_ATM_TAG);
481 }
482
tagged_arith_atom(void * atm)483 static inline void *tagged_arith_atom(void *atm) {
484 assert((((size_t) atm) & ATM_TAG_MASK) == 0);
485 return (void *)(((size_t) atm) | ARITH_ATM_TAG);
486 }
487
tagged_bv_atom(void * atm)488 static inline void *tagged_bv_atom(void *atm) {
489 assert((((size_t) atm) & ATM_TAG_MASK) == 0);
490 return (void *)(((size_t) atm) | BV_ATM_TAG);
491 }
492
493
494
495
496
497 #endif /* EGRAPH_BASE_TYPES */
498