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 * UTILITIES TO ACCESS CONTEXT STRUCTURES
21 */
22
23 #include "context/context_utils.h"
24 #include "context/internalization_codes.h"
25
26
27
28 /*
29 * SUBST AND MARK VECTOR
30 */
31
32 /*
33 * If variable elimination is enabled, then ctx->subst is used to
34 * store candidate substitutions before we check for substitution
35 * cycles. The mark vector is used to mark terms during cycle detection.
36 */
37
38 /*
39 * Allocate and initialize ctx->subst
40 */
context_get_subst(context_t * ctx)41 pseudo_subst_t *context_get_subst(context_t *ctx) {
42 pseudo_subst_t *tmp;
43
44 tmp = ctx->subst;
45 if (tmp == NULL) {
46 tmp = (pseudo_subst_t *) safe_malloc(sizeof(pseudo_subst_t));
47 init_pseudo_subst(tmp, 0);
48 ctx->subst = tmp;
49 }
50
51 return tmp;
52 }
53
54
55 /*
56 * Free ctx->subst
57 */
context_free_subst(context_t * ctx)58 void context_free_subst(context_t *ctx) {
59 if (ctx->subst != NULL) {
60 delete_pseudo_subst(ctx->subst);
61 safe_free(ctx->subst);
62 ctx->subst = NULL;
63 }
64 }
65
66
67 /*
68 * Allocate and initialize mark vectors
69 */
context_get_marks(context_t * ctx)70 mark_vector_t *context_get_marks(context_t *ctx) {
71 mark_vector_t *tmp;
72
73 tmp = ctx->marks;
74 if (tmp == NULL) {
75 tmp = (mark_vector_t *) safe_malloc(sizeof(mark_vector_t));
76 init_mark_vector(tmp, 100, WHITE);
77 ctx->marks = tmp;
78 }
79
80 return tmp;
81 }
82
83
84 /*
85 * Free the mark vector
86 */
context_free_marks(context_t * ctx)87 void context_free_marks(context_t *ctx) {
88 if (ctx->marks != NULL) {
89 delete_mark_vector(ctx->marks);
90 safe_free(ctx->marks);
91 ctx->marks = NULL;
92 }
93 }
94
95
96
97 /*
98 * CACHES
99 */
100
101 /*
102 * There are two internal caches for visiting formulas/terms.
103 * - the 'cache' uses a bitvector implementation and should be
104 * better for operations that visit many terms.
105 * - the 'small_cache' uses a hash table and should be better
106 * for operations that visit a small number of terms.
107 */
108
109 /*
110 * Allocate and initialize the internal small_cache if needed
111 */
context_get_small_cache(context_t * ctx)112 int_hset_t *context_get_small_cache(context_t *ctx) {
113 int_hset_t *tmp;
114
115 tmp = ctx->small_cache;
116 if (tmp == NULL) {
117 tmp = (int_hset_t *) safe_malloc(sizeof(int_hset_t));
118 init_int_hset(tmp, 32);
119 ctx->small_cache = tmp;
120 }
121 return tmp;
122 }
123
124
125 /*
126 * Empty the small_cache
127 */
context_reset_small_cache(context_t * ctx)128 void context_reset_small_cache(context_t *ctx) {
129 int_hset_t *tmp;
130
131 tmp = ctx->small_cache;
132 if (tmp != NULL) {
133 int_hset_reset(tmp);
134 }
135 }
136
137 /*
138 * Free the small_cache
139 */
context_free_small_cache(context_t * ctx)140 void context_free_small_cache(context_t *ctx) {
141 int_hset_t *tmp;
142
143 tmp = ctx->small_cache;
144 if (tmp != NULL) {
145 delete_int_hset(tmp);
146 safe_free(tmp);
147 ctx->small_cache = NULL;
148 }
149 }
150
151
152 /*
153 * Allocate and initialize the cache
154 */
context_get_cache(context_t * ctx)155 int_bvset_t *context_get_cache(context_t *ctx) {
156 int_bvset_t *tmp;
157
158 tmp = ctx->cache;
159 if (tmp == NULL) {
160 tmp = (int_bvset_t *) safe_malloc(sizeof(int_bvset_t));
161 init_int_bvset(tmp, 0);
162 ctx->cache = tmp;
163 }
164
165 return tmp;
166 }
167
168
169
170 /*
171 * Free the cache
172 */
context_free_cache(context_t * ctx)173 void context_free_cache(context_t *ctx) {
174 int_bvset_t *tmp;
175
176 tmp = ctx->cache;
177 if (tmp != NULL) {
178 delete_int_bvset(tmp);
179 safe_free(tmp);
180 ctx->cache = NULL;
181 }
182 }
183
184
185 /*
186 * ARITHMETIC BUFFERS
187 */
188
189 /*
190 * There are three buffers for internal construction of polynomials
191 * - arith_buffer is more expensive (requires more memory) but
192 * it supports more operations (e.g., term constructors in yices_api.c
193 * take arith_buffers as arguments).
194 * - poly_buffer is a cheaper data structure, but it does not support
195 * all the operations
196 * - aux_poly is even cheaper, but it's for direct construction only
197 */
198
199 /*
200 * Allocate the arithmetic buffer + store if necessary
201 */
context_get_arith_buffer(context_t * ctx)202 rba_buffer_t *context_get_arith_buffer(context_t *ctx) {
203 rba_buffer_t *tmp;
204
205 tmp = ctx->arith_buffer;
206 if (tmp == NULL) {
207 tmp = (rba_buffer_t *) safe_malloc(sizeof(rba_buffer_t));
208 init_rba_buffer(tmp, ctx->terms->pprods);
209 ctx->arith_buffer = tmp;
210 }
211
212 return tmp;
213 }
214
215
216 /*
217 * Free the arithmetic buffer + store
218 */
context_free_arith_buffer(context_t * ctx)219 void context_free_arith_buffer(context_t *ctx) {
220 rba_buffer_t *tmp;
221
222 tmp = ctx->arith_buffer;
223 if (tmp != NULL) {
224 delete_rba_buffer(tmp);
225 safe_free(tmp);
226 ctx->arith_buffer = NULL;
227 }
228 }
229
230
231
232 /*
233 * Allocate the poly_buffer
234 */
context_get_poly_buffer(context_t * ctx)235 poly_buffer_t *context_get_poly_buffer(context_t *ctx) {
236 poly_buffer_t *tmp;
237
238 tmp = ctx->poly_buffer;
239 if (tmp == NULL) {
240 tmp = (poly_buffer_t *) safe_malloc(sizeof(poly_buffer_t));
241 init_poly_buffer(tmp);
242 ctx->poly_buffer = tmp;
243 }
244
245 return tmp;
246 }
247
248
249 /*
250 * Free it
251 */
context_free_poly_buffer(context_t * ctx)252 void context_free_poly_buffer(context_t *ctx) {
253 poly_buffer_t *tmp;
254
255 tmp = ctx->poly_buffer;
256 if (tmp != NULL) {
257 delete_poly_buffer(tmp);
258 safe_free(tmp);
259 ctx->poly_buffer = NULL;
260 }
261 }
262
263
264 /*
265 * Reset it
266 */
context_reset_poly_buffer(context_t * ctx)267 void context_reset_poly_buffer(context_t *ctx) {
268 if (ctx->poly_buffer != NULL) {
269 reset_poly_buffer(ctx->poly_buffer);
270 }
271 }
272
273
274 /*
275 * Allocate the auxiliary polynomial buffer and make it large enough
276 * for n monomials.
277 */
context_get_aux_poly(context_t * ctx,uint32_t n)278 polynomial_t *context_get_aux_poly(context_t *ctx, uint32_t n) {
279 polynomial_t *p;
280 uint32_t k;
281
282 assert(n > 0);
283
284 p = ctx->aux_poly;
285 k = ctx->aux_poly_size;
286 if (k < n) {
287 if (k == 0) {
288 assert(p == NULL);
289 if (n < 10) n = 10;
290 p = alloc_raw_polynomial(n);
291 } else {
292 free_polynomial(p);
293 p = alloc_raw_polynomial(n);
294 }
295 ctx->aux_poly = p;
296 ctx->aux_poly_size = n;
297 }
298
299 assert(p != NULL && ctx->aux_poly_size >= n);
300
301 return p;
302 }
303
304
305 /*
306 * Reset the auxiliary polynomial
307 */
context_free_aux_poly(context_t * ctx)308 void context_free_aux_poly(context_t *ctx) {
309 polynomial_t *p;
310
311 p = ctx->aux_poly;
312 if (p != NULL) {
313 free_polynomial(p);
314 ctx->aux_poly = NULL;
315 ctx->aux_poly_size = 0;
316 }
317 }
318
319
320 /*
321 * Buffer for bitvector polynomials
322 */
context_get_bvpoly_buffer(context_t * ctx)323 bvpoly_buffer_t *context_get_bvpoly_buffer(context_t *ctx) {
324 bvpoly_buffer_t *tmp;
325
326 tmp = ctx->bvpoly_buffer;
327 if (tmp == NULL) {
328 tmp = (bvpoly_buffer_t *) safe_malloc(sizeof(bvpoly_buffer_t));
329 init_bvpoly_buffer(tmp);
330 ctx->bvpoly_buffer = tmp;
331 }
332
333 return tmp;
334 }
335
context_free_bvpoly_buffer(context_t * ctx)336 void context_free_bvpoly_buffer(context_t *ctx) {
337 bvpoly_buffer_t *tmp;
338
339 tmp = ctx->bvpoly_buffer;
340 if (tmp != NULL) {
341 delete_bvpoly_buffer(tmp);
342 safe_free(tmp);
343 ctx->bvpoly_buffer = NULL;
344 }
345 }
346
347
348 /*
349 * CACHE/HASH MAP FOR LIFTED EQUALITIES
350 */
351
352 /*
353 * If lift-if is enabled then arithmetic equalities
354 * (eq (ite c t1 t2) u) are rewritten to (ite c (eq t1 u) (eq t2 u))
355 * We don't create new terms (eq t1 u) or (eq t2 u). Instead, we store
356 * the internalization of equalities (eq t1 u) in the eq_cache:
357 * This cache maps pairs of terms <t, u> to a literal l (such that
358 * l is the internalization of (t == u)).
359 */
360
361 /*
362 * Allocate and initialize the cache
363 */
context_get_eq_cache(context_t * ctx)364 pmap2_t *context_get_eq_cache(context_t *ctx) {
365 pmap2_t *tmp;
366
367 tmp = ctx->eq_cache;
368 if (tmp == NULL) {
369 tmp = (pmap2_t *) safe_malloc(sizeof(pmap2_t));
370 init_pmap2(tmp);
371 pmap2_set_level(tmp, ctx->base_level);
372 ctx->eq_cache = tmp;
373 }
374
375 return tmp;
376 }
377
378
379 /*
380 * Free the cache
381 */
context_free_eq_cache(context_t * ctx)382 void context_free_eq_cache(context_t *ctx) {
383 pmap2_t *tmp;
384
385 tmp = ctx->eq_cache;
386 if (tmp != NULL) {
387 delete_pmap2(tmp);
388 safe_free(tmp);
389 ctx->eq_cache = NULL;
390 }
391 }
392
393
394 /*
395 * Push/pop/reset if the cache exists
396 */
context_eq_cache_push(context_t * ctx)397 void context_eq_cache_push(context_t *ctx) {
398 pmap2_t *tmp;
399
400 tmp = ctx->eq_cache;
401 if (tmp != NULL) {
402 pmap2_push(tmp);
403 }
404 }
405
context_eq_cache_pop(context_t * ctx)406 void context_eq_cache_pop(context_t *ctx) {
407 pmap2_t *tmp;
408
409 tmp = ctx->eq_cache;
410 if (tmp != NULL) {
411 pmap2_pop(tmp);
412 }
413 }
414
415
416
417 /*
418 * Check what's mapped to (t1, t2) in the internal eq_cache.
419 * - return null_literal if nothing is mapped to (t1, t2) (or if the cache does not exit)
420 */
find_in_eq_cache(context_t * ctx,term_t t1,term_t t2)421 literal_t find_in_eq_cache(context_t *ctx, term_t t1, term_t t2) {
422 pmap2_t *eq_cache;
423 pmap2_rec_t *eq;
424 term_t aux;
425 literal_t l;
426
427 l = null_literal;
428 eq_cache = ctx->eq_cache;
429 if (eq_cache != NULL) {
430 // normalize the pair: we want t1 >= t2
431 if (t1 < t2) {
432 aux = t1; t1 = t2; t2 = aux;
433 }
434 assert(t1 >= t2);
435
436 eq = pmap2_find(eq_cache, t1, t2);
437 if (eq != NULL) {
438 l = eq->val;
439 assert(l != null_literal);
440 }
441 }
442
443 return l;
444 }
445
446
447 /*
448 * Add the mapping (t1, t2) --> l to the equality cache.
449 * - allocate and initialize the cache if needed.
450 * - the pair (t1, t2) must not be in the cache already.
451 * - l must be different from null_literal
452 */
add_to_eq_cache(context_t * ctx,term_t t1,term_t t2,literal_t l)453 void add_to_eq_cache(context_t *ctx, term_t t1, term_t t2, literal_t l) {
454 pmap2_t *eq_cache;
455 pmap2_rec_t *eq;
456 term_t aux;
457
458 assert(l != null_literal);
459
460 eq_cache = context_get_eq_cache(ctx);
461 if (t1 < t2) {
462 aux = t1; t1 = t2; t2 = aux;
463 }
464 eq = pmap2_get(eq_cache, t1, t2);
465 assert(eq != NULL && eq->val == -1);
466 eq->val = l;
467 }
468
469
470 /*
471 * DIV/MOD TABLE
472 */
473
474 /*
475 * Return the table. Allocate and initialize it if needed.
476 */
context_get_divmod_table(context_t * ctx)477 divmod_tbl_t *context_get_divmod_table(context_t *ctx) {
478 divmod_tbl_t *tmp;
479
480 tmp = ctx->divmod_table;
481 if (tmp == NULL) {
482 tmp = (divmod_tbl_t *) safe_malloc(sizeof(divmod_tbl_t));
483 init_divmod_table(tmp);
484 divmod_table_set_level(tmp, ctx->base_level);
485 ctx->divmod_table = tmp;
486 }
487
488 return tmp;
489 }
490
491
492 /*
493 * Free the table
494 */
context_free_divmod_table(context_t * ctx)495 void context_free_divmod_table(context_t *ctx) {
496 divmod_tbl_t *tmp;
497
498 tmp = ctx->divmod_table;
499 if (tmp != NULL) {
500 delete_divmod_table(tmp);
501 safe_free(tmp);
502 ctx->divmod_table = NULL;
503 }
504 }
505
506
507 /*
508 * Push/pop/reset
509 */
context_divmod_table_push(context_t * ctx)510 void context_divmod_table_push(context_t *ctx) {
511 divmod_tbl_t *tmp;
512
513 tmp = ctx->divmod_table;
514 if (tmp != NULL) {
515 divmod_table_push(tmp);
516 }
517 }
518
context_divmod_table_pop(context_t * ctx)519 void context_divmod_table_pop(context_t *ctx) {
520 divmod_tbl_t *tmp;
521
522 tmp = ctx->divmod_table;
523 if (tmp != NULL) {
524 divmod_table_pop(tmp);
525 }
526 }
527
context_reset_divmod_table(context_t * ctx)528 void context_reset_divmod_table(context_t *ctx) {
529 divmod_tbl_t *tmp;
530
531 tmp = ctx->divmod_table;
532 if (tmp != NULL) {
533 reset_divmod_table(tmp);
534 }
535 }
536
537
538 /*
539 * Find records in the table:
540 * - three functions for floor/ceil/div
541 * - all find functions return null_thvar if the table does not exist or
542 * if the relevant record is not in the table.
543 */
context_find_var_for_floor(context_t * ctx,thvar_t x)544 thvar_t context_find_var_for_floor(context_t *ctx, thvar_t x) {
545 divmod_tbl_t *tmp;
546 divmod_rec_t *r;
547 thvar_t y;
548
549 y = null_thvar;
550 tmp = ctx->divmod_table;
551 if (tmp != NULL) {
552 r = divmod_table_find_floor(tmp, x);
553 if (r != NULL) {
554 y = r->val;
555 }
556 }
557
558 return y;
559 }
560
context_find_var_for_ceil(context_t * ctx,thvar_t x)561 thvar_t context_find_var_for_ceil(context_t *ctx, thvar_t x) {
562 divmod_tbl_t *tmp;
563 divmod_rec_t *r;
564 thvar_t y;
565
566 y = null_thvar;
567 tmp = ctx->divmod_table;
568 if (tmp != NULL) {
569 r = divmod_table_find_ceil(tmp, x);
570 if (r != NULL) {
571 y = r->val;
572 }
573 }
574
575 return y;
576 }
577
context_find_var_for_div(context_t * ctx,thvar_t x,const rational_t * k)578 thvar_t context_find_var_for_div(context_t *ctx, thvar_t x, const rational_t *k) {
579 divmod_tbl_t *tmp;
580 divmod_rec_t *r;
581 thvar_t y;
582
583 y = null_thvar;
584 tmp = ctx->divmod_table;
585 if (tmp != NULL) {
586 r = divmod_table_find_div(tmp, x, k);
587 if (r != NULL) {
588 y = r->val;
589 }
590 }
591
592 return y;
593 }
594
595
596 /*
597 * Add records in the table:
598 * - three functions for floor/ceil/div
599 * - all three functions initialize the table if needed
600 */
601
602 // record for y = (floor x)
context_record_floor(context_t * ctx,thvar_t x,thvar_t y)603 void context_record_floor(context_t *ctx, thvar_t x, thvar_t y) {
604 divmod_tbl_t *tmp;
605 divmod_rec_t *r;
606
607 tmp = context_get_divmod_table(ctx);
608 r = divmod_table_get_floor(tmp, x);
609 assert(r->val < 0);
610 r->val = y;
611 }
612
613 // record for y = (ceil x)
context_record_ceil(context_t * ctx,thvar_t x,thvar_t y)614 void context_record_ceil(context_t *ctx, thvar_t x, thvar_t y) {
615 divmod_tbl_t *tmp;
616 divmod_rec_t *r;
617
618 tmp = context_get_divmod_table(ctx);
619 r = divmod_table_get_ceil(tmp, x);
620 assert(r->val < 0);
621 r->val = y;
622 }
623
624 // record for y = (div x k)
context_record_div(context_t * ctx,thvar_t x,const rational_t * k,thvar_t y)625 void context_record_div(context_t *ctx, thvar_t x, const rational_t *k, thvar_t y) {
626 divmod_tbl_t *tmp;
627 divmod_rec_t *r;
628
629 tmp = context_get_divmod_table(ctx);
630 r = divmod_table_get_div(tmp, x, k);
631 assert(r->val < 0);
632 r->val = y;
633 }
634
635
636
637 /*
638 * FACTORING OF DISJUNCTS
639 */
640
641 /*
642 * Return the explorer data structure
643 * - allocate and initialize it if needed
644 */
context_get_explorer(context_t * ctx)645 bfs_explorer_t *context_get_explorer(context_t *ctx) {
646 bfs_explorer_t *tmp;
647
648 tmp = ctx->explorer;
649 if (tmp == NULL) {
650 tmp = (bfs_explorer_t *) safe_malloc(sizeof(bfs_explorer_t));
651 init_bfs_explorer(tmp, ctx->terms);
652 ctx->explorer = tmp;
653 }
654
655 return tmp;
656 }
657
658 /*
659 * Free the explorer if it's not NULL
660 */
context_free_explorer(context_t * ctx)661 void context_free_explorer(context_t *ctx) {
662 bfs_explorer_t *tmp;
663
664 tmp = ctx->explorer;
665 if (tmp != NULL) {
666 delete_bfs_explorer(tmp);
667 safe_free(tmp);
668 ctx->explorer = NULL;
669 }
670 }
671
672
673 /*
674 * Reset the explorer if it's not NULL
675 */
context_reset_explorer(context_t * ctx)676 void context_reset_explorer(context_t *ctx) {
677 bfs_explorer_t *tmp;
678
679 tmp = ctx->explorer;
680 if (tmp != NULL) {
681 reset_bfs_explorer(tmp);
682 }
683 }
684
685 /*
686 * Get the common factors of term t
687 * - this checks whether t is of the form (or (and ..) (and ..) ...))
688 * and stores all terms that occur in each conjuncts into vector v
689 * - example: if t is (or (and A B) (and A C D)) then A is stored in v
690 * - if t is not (OR ...) then t is added to v
691 */
context_factor_disjunction(context_t * ctx,term_t t,ivector_t * v)692 void context_factor_disjunction(context_t *ctx, term_t t, ivector_t *v) {
693 bfs_explorer_t *explorer;
694
695 explorer = context_get_explorer(ctx);
696 bfs_factor_disjunction(explorer, t, v);
697 }
698
699
700
701 /*
702 * DIFFERENCE-LOGIC DATA
703 */
704
705 /*
706 * Map to compute a bound on the length path:
707 * - allocate and initialize the table if needed
708 */
context_get_edge_map(context_t * ctx)709 int_rat_hmap_t *context_get_edge_map(context_t *ctx) {
710 int_rat_hmap_t *tmp;
711
712 tmp = ctx->edge_map;
713 if (tmp == NULL) {
714 tmp = (int_rat_hmap_t *) safe_malloc(sizeof(int_rat_hmap_t));
715 init_int_rat_hmap(tmp, 0);
716 ctx->edge_map = tmp;
717 }
718
719 return tmp;
720 }
721
722 /*
723 * Delete the map
724 */
context_free_edge_map(context_t * ctx)725 void context_free_edge_map(context_t *ctx) {
726 int_rat_hmap_t *tmp;
727
728 tmp = ctx->edge_map;
729 if (tmp != NULL) {
730 delete_int_rat_hmap(tmp);
731 ctx->edge_map = NULL;
732 }
733 }
734
735
736 /*
737 * Difference-logic profile:
738 * - allocate and initialize the structure if it does not exist
739 */
context_get_dl_profile(context_t * ctx)740 dl_data_t *context_get_dl_profile(context_t *ctx) {
741 dl_data_t *tmp;
742
743 tmp = ctx->dl_profile;
744 if (tmp == NULL) {
745 tmp = (dl_data_t *) safe_malloc(sizeof(dl_data_t));
746 q_init(&tmp->path_bound);
747 tmp->num_vars = 0;
748 tmp->num_atoms = 0;
749 tmp->num_eqs = 0;
750 ctx->dl_profile = tmp;
751 }
752
753 return tmp;
754 }
755
756
757 /*
758 * Free the profile record
759 */
context_free_dl_profile(context_t * ctx)760 void context_free_dl_profile(context_t *ctx) {
761 dl_data_t *tmp;
762
763 tmp = ctx->dl_profile;
764 if (tmp != NULL) {
765 q_clear(&tmp->path_bound);
766 safe_free(tmp);
767 ctx->dl_profile = NULL;
768 }
769 }
770
771
772 /*
773 * CHECKS
774 */
775
776 /*
777 * Check whether t is true or false (i.e., mapped to 'true_occ' or 'false_occ'
778 * in the internalization table.
779 * - t must be a root in the internalization table
780 */
term_is_true(context_t * ctx,term_t t)781 bool term_is_true(context_t *ctx, term_t t) {
782 bool tt;
783
784 assert(intern_tbl_is_root(&ctx->intern, t));
785 tt = is_pos_term(t);
786 t = unsigned_term(t);
787
788 return intern_tbl_root_is_mapped(&ctx->intern, t) &&
789 intern_tbl_map_of_root(&ctx->intern, t) == bool2code(tt);
790 }
791
term_is_false(context_t * ctx,term_t t)792 bool term_is_false(context_t *ctx, term_t t) {
793 bool tt;
794
795 assert(intern_tbl_is_root(&ctx->intern, t));
796 tt = is_pos_term(t);
797 t = unsigned_term(t);
798
799 return intern_tbl_root_is_mapped(&ctx->intern, t) &&
800 intern_tbl_map_of_root(&ctx->intern, t) == bool2code(! tt);
801 }
802
803
804 /*
805 * Check whether (or a[0] ... a[n-1]) is true by checking whether
806 * one of the a[i] is internalized to a true term
807 */
disjunct_is_true(context_t * ctx,term_t * a,uint32_t n)808 bool disjunct_is_true(context_t *ctx, term_t *a, uint32_t n) {
809 uint32_t i;
810 term_t x;
811
812 for (i=0; i<n; i++) {
813 x = intern_tbl_get_root(&ctx->intern, a[i]);
814 if (term_is_true(ctx, x)) return true;
815 }
816
817 return false;
818 }
819
820
821 /*
822 * Check whether x is an if-then-else term
823 */
term_is_ite(context_t * ctx,term_t x)824 bool term_is_ite(context_t *ctx, term_t x) {
825 x = intern_tbl_get_root(&ctx->intern, x);
826 return is_pos_term(x) && is_ite_term(ctx->terms, x) &&
827 !intern_tbl_root_is_mapped(&ctx->intern, x);
828 }
829
830
831 /*
832 * Checks whether ite contains nested if-then-elses
833 */
ite_is_deep(context_t * ctx,composite_term_t * ite)834 bool ite_is_deep(context_t *ctx, composite_term_t *ite) {
835 assert(ite->arity == 3);
836 return term_is_ite(ctx, ite->arg[1]) || term_is_ite(ctx, ite->arg[2]);
837 }
838
839
840 /*
841 * AUXILIARY EQUALITIES
842 */
843
844 /*
845 * Add an auxiliary equality (x == y) to the context
846 * - this create eq := (eq x y) then add it to aux_eq
847 */
add_aux_eq(context_t * ctx,term_t x,term_t y)848 void add_aux_eq(context_t *ctx, term_t x, term_t y) {
849 term_table_t *terms;
850 term_t eq;
851
852 x = intern_tbl_get_root(&ctx->intern, x);
853 y = intern_tbl_get_root(&ctx->intern, y);
854
855 if (x != y) {
856 /*
857 * Build/get term (eq x y)
858 */
859 terms = ctx->terms;
860 if (x > y) {
861 eq = eq_term(terms, y, x);
862 } else {
863 eq = eq_term(terms, x, y);
864 }
865
866 assert(intern_tbl_is_root(&ctx->intern, eq));
867
868 ivector_push(&ctx->aux_eqs, eq);
869 }
870 }
871
872
873 /*
874 * Add an auxiliary arithmetic equality to the context.
875 * - this adds eq to aux_eq
876 */
add_arith_aux_eq(context_t * ctx,term_t eq)877 void add_arith_aux_eq(context_t *ctx, term_t eq) {
878 assert(intern_tbl_is_root(&ctx->intern, eq));
879 assert(is_pos_term(eq));
880 assert(term_kind(ctx->terms, eq) == ARITH_EQ_ATOM ||
881 term_kind(ctx->terms, eq) == ARITH_BINEQ_ATOM);
882 ivector_push(&ctx->aux_eqs, eq);
883 }
884
885
886
887 /*
888 * LEARNED ATOMS
889 */
890
891 /*
892 * Add an atom (learned by preprocessing) to ctx->aux_atoms
893 */
add_aux_atom(context_t * ctx,term_t atom)894 void add_aux_atom(context_t *ctx, term_t atom) {
895 assert(is_boolean_term(ctx->terms, atom));
896 ivector_push(&ctx->aux_atoms, atom);
897 }
898
899
900