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 * EGRAPH-UTILITIES SHARED BY SEVERAL EGRAPH MODULES
21 */
22
23
24 #ifndef __EGRAPH_UTILS_H
25 #define __EGRAPH_UTILS_H
26
27 #include <assert.h>
28
29 #include "solvers/egraph/egraph_types.h"
30
31
32 /*********************
33 * INTERNAL IMAP *
34 ********************/
35
36 /*
37 * Allocate and initialize the internal imap (int_hash_map)
38 */
39 extern void egraph_alloc_imap(egraph_t *egraph);
40
41
42 /*
43 * Return a pointer to egraph->imap (allocate and initialize it if needed)
44 */
egraph_get_imap(egraph_t * egraph)45 static inline int_hmap_t *egraph_get_imap(egraph_t *egraph) {
46 if (egraph->imap == NULL) {
47 egraph_alloc_imap(egraph);
48 }
49 return egraph->imap;
50 }
51
52
53
54
55 /***********************************
56 * ACCESS TO TERM AND CLASS DATA *
57 **********************************/
58
59 /*
60 * Number of terms
61 */
egraph_num_terms(egraph_t * egraph)62 static inline uint32_t egraph_num_terms(egraph_t *egraph) {
63 return egraph->terms.nterms;
64 }
65
66 /*
67 * Number of classes
68 */
egraph_num_classes(egraph_t * egraph)69 static inline uint32_t egraph_num_classes(egraph_t *egraph) {
70 return egraph->classes.nclasses;
71 }
72
73
74 /*
75 * Check whether t is a valid term (not deleted)
76 */
egraph_term_is_valid(egraph_t * egraph,eterm_t t)77 static inline bool egraph_term_is_valid(egraph_t *egraph, eterm_t t) {
78 return 0 <= t && t < egraph->terms.nterms;
79 }
80
81 // same thing for x = t+ or t-
egraph_occ_is_valid(egraph_t * egraph,occ_t x)82 static inline bool egraph_occ_is_valid(egraph_t *egraph, occ_t x) {
83 return egraph_term_is_valid(egraph, term_of_occ(x));
84 }
85
86 // same thing for a class c
egraph_class_is_valid(egraph_t * egraph,class_t c)87 static inline bool egraph_class_is_valid(egraph_t *egraph, class_t c) {
88 return 0 <= c && c < egraph->classes.nclasses;
89 }
90
91 // same thing for a label l
egraph_label_is_valid(egraph_t * egraph,elabel_t l)92 static inline bool egraph_label_is_valid(egraph_t *egraph, elabel_t l) {
93 return egraph_class_is_valid(egraph, class_of(l));
94 }
95
96
97 /*
98 * Get fields of term t
99 */
egraph_term_body(egraph_t * egraph,eterm_t t)100 static inline composite_t *egraph_term_body(egraph_t *egraph, eterm_t t) {
101 assert(egraph_term_is_valid(egraph, t));
102 return egraph->terms.body[t];
103 }
104
egraph_term_label(egraph_t * egraph,eterm_t t)105 static inline elabel_t egraph_term_label(egraph_t *egraph, eterm_t t) {
106 assert(egraph_term_is_valid(egraph, t));
107 return egraph->terms.label[t];
108 }
109
egraph_term_class(egraph_t * egraph,eterm_t t)110 static inline class_t egraph_term_class(egraph_t *egraph, eterm_t t) {
111 return class_of(egraph_term_label(egraph, t));
112 }
113
egraph_term_next(egraph_t * egraph,eterm_t t)114 static inline eterm_t egraph_term_next(egraph_t *egraph, eterm_t t) {
115 assert(egraph_term_is_valid(egraph, t));
116 return term_of_occ(egraph->terms.next[t]);
117 }
118
egraph_term_real_type(egraph_t * egraph,eterm_t t)119 static inline type_t egraph_term_real_type(egraph_t *egraph, eterm_t t) {
120 assert(egraph_term_is_valid(egraph, t));
121 return egraph->terms.real_type[t];
122 }
123
124 // theory variable of t at the base level
egraph_term_base_thvar(egraph_t * egraph,eterm_t t)125 static inline thvar_t egraph_term_base_thvar(egraph_t *egraph, eterm_t t) {
126 assert(egraph_term_is_valid(egraph, t));
127 return egraph->terms.thvar[t];
128 }
129
130
131
132
133 /*
134 * Get fields of class c
135 */
egraph_class_dmask(egraph_t * egraph,class_t c)136 static inline uint32_t egraph_class_dmask(egraph_t *egraph, class_t c) {
137 assert(egraph_class_is_valid(egraph, c));
138 return egraph->classes.dmask[c];
139 }
140
egraph_class_root(egraph_t * egraph,class_t c)141 static inline occ_t egraph_class_root(egraph_t *egraph, class_t c) {
142 assert(egraph_class_is_valid(egraph, c));
143 return egraph->classes.root[c];
144 }
145
egraph_class_parents(egraph_t * egraph,class_t c)146 static inline use_vector_t *egraph_class_parents(egraph_t *egraph, class_t c) {
147 assert(egraph_class_is_valid(egraph, c));
148 return egraph->classes.parents + c;
149 }
150
151 // number of parents
egraph_class_nparents(egraph_t * egraph,class_t c)152 static inline uint32_t egraph_class_nparents(egraph_t *egraph, class_t c) {
153 return egraph_class_parents(egraph, c)->nelems;
154 }
155
egraph_class_type(egraph_t * egraph,class_t c)156 static inline etype_t egraph_class_type(egraph_t *egraph, class_t c) {
157 assert(egraph_class_is_valid(egraph, c));
158 return (etype_t) egraph->classes.etype[c];
159 }
160
egraph_class_thvar(egraph_t * egraph,class_t c)161 static inline thvar_t egraph_class_thvar(egraph_t *egraph, class_t c) {
162 assert(egraph_class_is_valid(egraph, c));
163 return egraph->classes.thvar[c];
164 }
165
166
167
168 /*
169 * Check theory var and type of class c
170 */
egraph_class_has_thvar(egraph_t * egraph,class_t c)171 static inline bool egraph_class_has_thvar(egraph_t *egraph, class_t c) {
172 return egraph_class_thvar(egraph, c) != null_thvar;
173 }
174
egraph_class_is_bool(egraph_t * egraph,class_t c)175 static inline bool egraph_class_is_bool(egraph_t *egraph, class_t c) {
176 return egraph_class_type(egraph, c) == ETYPE_BOOL;
177 }
178
egraph_class_is_int(egraph_t * egraph,class_t c)179 static inline bool egraph_class_is_int(egraph_t *egraph, class_t c) {
180 return egraph_class_type(egraph, c) == ETYPE_INT;
181 }
182
egraph_class_is_real(egraph_t * egraph,class_t c)183 static inline bool egraph_class_is_real(egraph_t *egraph, class_t c) {
184 return egraph_class_type(egraph, c) == ETYPE_REAL;
185 }
186
egraph_class_is_arith(egraph_t * egraph,class_t c)187 static inline bool egraph_class_is_arith(egraph_t *egraph, class_t c) {
188 return is_arith_etype(egraph_class_type(egraph, c));
189 }
190
egraph_class_is_bv(egraph_t * egraph,class_t c)191 static inline bool egraph_class_is_bv(egraph_t *egraph, class_t c) {
192 return egraph_class_type(egraph, c) == ETYPE_BV;
193 }
194
egraph_class_is_tuple(egraph_t * egraph,class_t c)195 static inline bool egraph_class_is_tuple(egraph_t *egraph, class_t c) {
196 return egraph_class_type(egraph, c) == ETYPE_TUPLE;
197 }
198
egraph_class_is_function(egraph_t * egraph,class_t c)199 static inline bool egraph_class_is_function(egraph_t *egraph, class_t c) {
200 return egraph_class_type(egraph, c) == ETYPE_FUNCTION;
201 }
202
203
204
205 /*
206 * Checks on t
207 */
egraph_term_is_variable(egraph_t * egraph,eterm_t t)208 static inline bool egraph_term_is_variable(egraph_t *egraph, eterm_t t) {
209 return egraph_term_body(egraph, t) == VARIABLE_BODY;
210 }
211
egraph_term_is_constant(egraph_t * egraph,eterm_t t)212 static inline bool egraph_term_is_constant(egraph_t *egraph, eterm_t t) {
213 return constant_body(egraph_term_body(egraph, t));
214 }
215
egraph_term_is_atomic(egraph_t * egraph,eterm_t t)216 static inline bool egraph_term_is_atomic(egraph_t *egraph, eterm_t t) {
217 return atomic_body(egraph_term_body(egraph, t));
218 }
219
egraph_term_is_composite(egraph_t * egraph,eterm_t t)220 static inline bool egraph_term_is_composite(egraph_t *egraph, eterm_t t) {
221 return composite_body(egraph_term_body(egraph, t));
222 }
223
egraph_term_is_eq(egraph_t * egraph,eterm_t t)224 static inline bool egraph_term_is_eq(egraph_t *egraph, eterm_t t) {
225 composite_t *cmp;
226 cmp = egraph_term_body(egraph, t);
227 return composite_body(cmp) && composite_kind(cmp) == COMPOSITE_EQ;
228 }
229
egraph_term_is_composite_tuple(egraph_t * egraph,eterm_t t)230 static inline bool egraph_term_is_composite_tuple(egraph_t *egraph, eterm_t t) {
231 composite_t *cmp;
232 cmp = egraph_term_body(egraph, t);
233 return composite_body(cmp) && composite_kind(cmp) == COMPOSITE_TUPLE;
234 }
235
egraph_term_is_lambda(egraph_t * egraph,eterm_t t)236 static inline bool egraph_term_is_lambda(egraph_t *egraph, eterm_t t) {
237 composite_t *cmp;
238 cmp = egraph_term_body(egraph, t);
239 return composite_body(cmp) && composite_kind(cmp) == COMPOSITE_LAMBDA;
240 }
241
242
243
244 /*
245 * Assign type tau to term t
246 */
egraph_set_term_real_type(egraph_t * egraph,eterm_t t,type_t tau)247 static inline void egraph_set_term_real_type(egraph_t *egraph, eterm_t t, type_t tau) {
248 assert(egraph_term_is_valid(egraph, t) && egraph->terms.real_type[t] == NULL_TYPE);
249 egraph->terms.real_type[t] = tau;
250 }
251
252 /*
253 * Current type and theory var of t (via t's class)
254 */
egraph_term_type(egraph_t * egraph,eterm_t t)255 static inline etype_t egraph_term_type(egraph_t *egraph, eterm_t t) {
256 return egraph_class_type(egraph, egraph_term_class(egraph, t));
257 }
258
egraph_term_thvar(egraph_t * egraph,eterm_t t)259 static inline thvar_t egraph_term_thvar(egraph_t *egraph, eterm_t t) {
260 return egraph_class_thvar(egraph, egraph_term_class(egraph, t));
261 }
262
263 // check theory for term t
egraph_term_is_bool(egraph_t * egraph,eterm_t t)264 static inline bool egraph_term_is_bool(egraph_t *egraph, eterm_t t) {
265 return egraph_class_is_bool(egraph, egraph_term_class(egraph, t));
266 }
267
egraph_term_is_arith(egraph_t * egraph,eterm_t t)268 static inline bool egraph_term_is_arith(egraph_t *egraph, eterm_t t) {
269 return egraph_class_is_arith(egraph, egraph_term_class(egraph, t));
270 }
271
egraph_term_is_bv(egraph_t * egraph,eterm_t t)272 static inline bool egraph_term_is_bv(egraph_t *egraph, eterm_t t) {
273 return egraph_class_is_bv(egraph, egraph_term_class(egraph, t));
274 }
275
egraph_term_is_tuple(egraph_t * egraph,eterm_t t)276 static inline bool egraph_term_is_tuple(egraph_t *egraph, eterm_t t) {
277 return egraph_class_is_tuple(egraph, egraph_term_class(egraph, t));
278 }
279
egraph_term_is_function(egraph_t * egraph,eterm_t t)280 static inline bool egraph_term_is_function(egraph_t *egraph, eterm_t t) {
281 return egraph_class_is_function(egraph, egraph_term_class(egraph, t));
282 }
283
284
285
286
287
288 /*
289 * Class and label for a term occurrence x = t+ or t-
290 */
egraph_label(egraph_t * egraph,occ_t x)291 static inline elabel_t egraph_label(egraph_t *egraph, occ_t x) {
292 return egraph_term_label(egraph, term_of_occ(x)) ^ polarity_of_occ(x);
293 }
294
egraph_class(egraph_t * egraph,occ_t x)295 static inline class_t egraph_class(egraph_t *egraph, occ_t x) {
296 return egraph_term_class(egraph, term_of_occ(x));
297 }
298
299 // successor occurrence of x in its class
egraph_next(egraph_t * egraph,occ_t x)300 static inline occ_t egraph_next(egraph_t *egraph, occ_t x) {
301 assert(egraph_occ_is_valid(egraph, x));
302 return egraph->terms.next[term_of_occ(x)] ^ polarity_of_occ(x);
303 }
304
305 // assign label c to x
egraph_set_label(egraph_t * egraph,occ_t x,elabel_t l)306 static inline void egraph_set_label(egraph_t *egraph, occ_t x, elabel_t l) {
307 assert(egraph_occ_is_valid(egraph, x));
308 egraph->terms.label[term_of_occ(x)] = l ^ polarity_of_occ(x);
309 }
310
311 // assign y as successor of x
egraph_set_next(egraph_t * egraph,occ_t x,occ_t y)312 static inline void egraph_set_next(egraph_t *egraph, occ_t x, occ_t y) {
313 assert(egraph_occ_is_valid(egraph, x) && egraph_occ_is_valid(egraph, y));
314 egraph->terms.next[term_of_occ(x)] = y ^ polarity_of_occ(x);
315 }
316
317
318
319 /*
320 * Type and theory variable of x (via its class)
321 */
egraph_type(egraph_t * egraph,occ_t x)322 static inline etype_t egraph_type(egraph_t *egraph, occ_t x) {
323 return egraph_class_type(egraph, egraph_class(egraph, x));
324 }
325
egraph_thvar(egraph_t * egraph,occ_t x)326 static inline thvar_t egraph_thvar(egraph_t *egraph, occ_t x) {
327 return egraph_class_thvar(egraph, egraph_class(egraph, x));
328 }
329
330 // variable attached to x at the base level (null_thvar if none)
egraph_base_thvar(egraph_t * egraph,occ_t x)331 static inline thvar_t egraph_base_thvar(egraph_t *egraph, occ_t x) {
332 return egraph_term_base_thvar(egraph, term_of_occ(x));
333 }
334
335 // check theory for occurrence x
egraph_occ_is_bool(egraph_t * egraph,occ_t x)336 static inline bool egraph_occ_is_bool(egraph_t *egraph, occ_t x) {
337 return egraph_class_is_bool(egraph, egraph_class(egraph, x));
338 }
339
egraph_occ_is_arith(egraph_t * egraph,occ_t x)340 static inline bool egraph_occ_is_arith(egraph_t *egraph, occ_t x) {
341 return egraph_class_is_arith(egraph, egraph_class(egraph, x));
342 }
343
egraph_occ_is_bv(egraph_t * egraph,occ_t x)344 static inline bool egraph_occ_is_bv(egraph_t *egraph, occ_t x) {
345 return egraph_class_is_bv(egraph, egraph_class(egraph, x));
346 }
347
egraph_occ_is_tuple(egraph_t * egraph,occ_t x)348 static inline bool egraph_occ_is_tuple(egraph_t *egraph, occ_t x) {
349 return egraph_class_is_tuple(egraph, egraph_class(egraph, x));
350 }
351
egraph_occ_is_function(egraph_t * egraph,occ_t x)352 static inline bool egraph_occ_is_function(egraph_t *egraph, occ_t x) {
353 return egraph_class_is_function(egraph, egraph_class(egraph, x));
354 }
355
356
357
358
359 /*
360 * Equality tests based on labels
361 */
362 // check whether x == y
egraph_equal_occ(egraph_t * egraph,occ_t x,occ_t y)363 static inline bool egraph_equal_occ(egraph_t *egraph, occ_t x, occ_t y) {
364 return egraph_label(egraph, x) == egraph_label(egraph, y);
365 }
366
367 // check whether x == not y
egraph_opposite_occ(egraph_t * egraph,occ_t x,occ_t y)368 static inline bool egraph_opposite_occ(egraph_t *egraph, occ_t x, occ_t y) {
369 return egraph_label(egraph, x) == opposite_label(egraph_label(egraph, y));
370 }
371
372 // check whether x == true
egraph_occ_is_true(egraph_t * egraph,occ_t x)373 static inline bool egraph_occ_is_true(egraph_t *egraph, occ_t x) {
374 return egraph_label(egraph, x) == true_label;
375 }
376
377 // check whether x == false
egraph_occ_is_false(egraph_t * egraph,occ_t x)378 static inline bool egraph_occ_is_false(egraph_t *egraph, occ_t x) {
379 return egraph_label(egraph, x) == false_label;
380 }
381
382 // check whether x and y are in the same class (either x == y or x == not y)
egraph_same_class(egraph_t * egraph,occ_t x,occ_t y)383 static inline bool egraph_same_class(egraph_t *egraph, occ_t x, occ_t y) {
384 return egraph_class(egraph, x) == egraph_class(egraph, y);
385 }
386
387
388 /*
389 * Truth-value of eterm t:
390 * - if label[t] is C0+ == 0, t is true --> truth_value is VAL_TRUE (== 3)
391 * - if label[t] is C0- == 1, t is false --> truth_value is VAL_FALSE (== 2)
392 *
393 * Use only if t's class is C0
394 */
egraph_term_truth_value(egraph_t * egraph,eterm_t t)395 static inline bval_t egraph_term_truth_value(egraph_t *egraph, eterm_t t) {
396 assert(egraph_term_class(egraph, t) == bool_constant_class);
397 return VAL_TRUE ^ egraph_term_label(egraph, t);
398 }
399
400 // variants: check whether t is true or false
egraph_term_is_true(egraph_t * egraph,eterm_t t)401 static inline bool egraph_term_is_true(egraph_t *egraph, eterm_t t) {
402 return egraph_term_label(egraph, t) == true_label;
403 }
404
egraph_term_is_false(egraph_t * egraph,eterm_t t)405 static inline bool egraph_term_is_false(egraph_t *egraph, eterm_t t) {
406 return egraph_term_label(egraph, t) == false_label;
407 }
408
409
410 /*
411 * Equality test for two terms t1 and t2
412 */
egraph_equal_terms(egraph_t * egraph,eterm_t t1,eterm_t t2)413 static inline bool egraph_equal_terms(egraph_t *egraph, eterm_t t1, eterm_t t2) {
414 return egraph_term_label(egraph, t1) == egraph_term_label(egraph, t2);
415 }
416
417
418
419 /*
420 * Check whether c is a root class
421 */
egraph_class_is_root_class(egraph_t * egraph,class_t c)422 static inline bool egraph_class_is_root_class(egraph_t *egraph, class_t c) {
423 return egraph_class(egraph, egraph_class_root(egraph, c)) == c;
424 }
425
426
427
428
429 /*
430 * Successor term of t in edge eq
431 * - eq->lhs or eq->rhs must be either t+ or t-
432 */
edge_next(equeue_elem_t * eq,eterm_t t)433 static inline eterm_t edge_next(equeue_elem_t *eq, eterm_t t) {
434 assert(term_of_occ(eq->lhs) == t || term_of_occ(eq->rhs) == t);
435 return term_of_occ(eq->lhs ^ eq->rhs) ^ t;
436 }
437
438 /*
439 * Successor occurrence of u in edge eq
440 * - eq is either (u == v) or ((not u) == v)
441 * - since (not x) is (x ^ 0x1), xor does the trick:
442 * - if eq is (u == v) then u ^ v ^ u == v
443 * - if eq is ((not u) == v) then
444 * (not u) ^ v ^ u == (u ^ 0x1) ^ v ^ u == v ^ 0x1 == (not v)
445 */
edge_next_occ(equeue_elem_t * eq,occ_t u)446 static inline occ_t edge_next_occ(equeue_elem_t *eq, occ_t u) {
447 assert(term_of_occ(eq->lhs) == term_of_occ(u) ||
448 term_of_occ(eq->rhs) == term_of_occ(u));
449 return eq->lhs ^ eq->rhs ^ u;
450 }
451
452
453
454
455 /**************************************
456 * PARAMETERS AND OPTIONAL FEATURES *
457 *************************************/
458
459 /*
460 * Check whether option(s) defined by x is (or are) enabled.
461 * x must be a bit mask.
462 */
egraph_option_enabled(egraph_t * egraph,uint32_t x)463 static inline bool egraph_option_enabled(egraph_t *egraph, uint32_t x) {
464 return (egraph->options & x) != 0;
465 }
466
egraph_option_disabled(egraph_t * egraph,uint32_t x)467 static inline bool egraph_option_disabled(egraph_t *egraph, uint32_t x) {
468 return (egraph->options &x) == 0;
469 }
470
471
472 /*
473 * Set the option flag
474 */
egraph_set_options(egraph_t * egraph,uint32_t x)475 static inline void egraph_set_options(egraph_t *egraph, uint32_t x) {
476 egraph->options = x;
477 }
478
egraph_enable_options(egraph_t * egraph,uint32_t x)479 static inline void egraph_enable_options(egraph_t *egraph, uint32_t x) {
480 egraph->options |= x;
481 }
482
egraph_disable_options(egraph_t * egraph,uint32_t x)483 static inline void egraph_disable_options(egraph_t *egraph, uint32_t x) {
484 egraph->options &= ~x;
485 }
486
487
488 /*
489 * Enable the generation of ackermann lemmas (non-boolean) with a limit n.
490 */
egraph_enable_dyn_ackermann(egraph_t * egraph,uint32_t n)491 static inline void egraph_enable_dyn_ackermann(egraph_t *egraph, uint32_t n) {
492 egraph_enable_options(egraph, EGRAPH_DYNAMIC_ACKERMANN);
493 egraph->max_ackermann = n;
494 }
495
egraph_disable_dyn_ackermann(egraph_t * egraph)496 static inline void egraph_disable_dyn_ackermann(egraph_t *egraph) {
497 egraph_disable_options(egraph, EGRAPH_DYNAMIC_ACKERMANN);
498 }
499
egraph_get_max_ackermann(egraph_t * egraph)500 static inline uint32_t egraph_get_max_ackermann(egraph_t *egraph) {
501 return egraph->max_ackermann;
502 }
503
504
505 /*
506 * Set/get the threshold for Ackermann lemma generation
507 */
egraph_set_ackermann_threshold(egraph_t * egraph,uint16_t x)508 static inline void egraph_set_ackermann_threshold(egraph_t *egraph, uint16_t x) {
509 assert(x > 0);
510 egraph->ackermann_threshold = x;
511 }
512
egraph_get_ackermann_threshold(egraph_t * egraph)513 static inline uint16_t egraph_get_ackermann_threshold(egraph_t *egraph) {
514 return egraph->ackermann_threshold;
515 }
516
517
518 /*
519 * Enable the generation of ackermann lemmas (boolean) with a limit n.
520 */
egraph_enable_dyn_boolackermann(egraph_t * egraph,uint32_t n)521 static inline void egraph_enable_dyn_boolackermann(egraph_t *egraph, uint32_t n) {
522 egraph_enable_options(egraph, EGRAPH_DYNAMIC_BOOLACKERMANN);
523 egraph->max_boolackermann = n;
524 }
525
egraph_disable_dyn_boolackermann(egraph_t * egraph)526 static inline void egraph_disable_dyn_boolackermann(egraph_t *egraph) {
527 egraph_disable_options(egraph, EGRAPH_DYNAMIC_BOOLACKERMANN);
528 }
529
egraph_get_max_boolackermann(egraph_t * egraph)530 static inline uint32_t egraph_get_max_boolackermann(egraph_t *egraph) {
531 return egraph->max_boolackermann;
532 }
533
534
535 /*
536 * Set/get the threshold for boolean Ackermann lemma generation
537 */
egraph_set_boolack_threshold(egraph_t * egraph,uint16_t x)538 static inline void egraph_set_boolack_threshold(egraph_t *egraph, uint16_t x) {
539 assert(x > 0);
540 egraph->boolack_threshold = x;
541 }
542
egraph_get_boolack_threshold(egraph_t * egraph)543 static inline uint16_t egraph_get_boolack_threshold(egraph_t *egraph) {
544 return egraph->boolack_threshold;
545 }
546
547
548 /*
549 * Set a quota: maximal number of new equalities created
550 */
egraph_set_aux_eq_quota(egraph_t * egraph,uint32_t n)551 static inline void egraph_set_aux_eq_quota(egraph_t *egraph, uint32_t n) {
552 egraph->aux_eq_quota = n;
553 }
554
egraph_get_aux_eq_quota(egraph_t * egraph)555 static inline uint32_t egraph_get_aux_eq_quota(egraph_t *egraph) {
556 return egraph->aux_eq_quota;
557 }
558
559
560 /*
561 * Set the maximal number of interface equalities generated per call to final_check
562 */
egraph_set_max_interface_eqs(egraph_t * egraph,uint32_t n)563 static inline void egraph_set_max_interface_eqs(egraph_t *egraph, uint32_t n) {
564 egraph->max_interface_eqs = n;
565 }
566
egraph_get_max_interface_eqs(egraph_t * egraph)567 static inline uint32_t egraph_get_max_interface_eqs(egraph_t *egraph) {
568 return egraph->max_interface_eqs;
569 }
570
571
572 /*
573 * Select final_check version:
574 * - optimistic version should work better on most problems
575 * - baseline version generates more interface equalities but it works
576 * better on a few problems (in QF_UFLIA)
577 * - baseline is the default
578 */
egraph_enable_optimistic_final_check(egraph_t * egraph)579 static inline void egraph_enable_optimistic_final_check(egraph_t *egraph) {
580 egraph_enable_options(egraph, EGRAPH_OPTIMISTIC_FCHECK);
581 }
582
egraph_disable_optimistic_final_check(egraph_t * egraph)583 static inline void egraph_disable_optimistic_final_check(egraph_t *egraph) {
584 egraph_disable_options(egraph, EGRAPH_OPTIMISTIC_FCHECK);
585 }
586
587
588
589
590 /************************************
591 * SUPPORT FOR GARBAGE COLLECTION *
592 ***********************************/
593
594 /*
595 * Mark all types used by egraph to preserve them from deletion on
596 * the next call to type_table_gc.
597 *
598 * Marked types include:
599 * - any type tau that occurs in egraph->terms.real_type[i]
600 * - all types that occur in egraph->tag_table.
601 */
602 extern void egraph_gc_mark(egraph_t *egraph);
603
604
605 #endif
606