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 * DAG OF BIT-VECTOR EXPRESSIONS
21 */
22
23 #include <assert.h>
24
25 #include "solvers/bv/bvpoly_dag.h"
26 #include "terms/bv64_constants.h"
27 #include "utils/bit_tricks.h"
28 #include "utils/hash_functions.h"
29 #include "utils/index_vectors.h"
30 #include "utils/int_array_sort.h"
31 #include "utils/int_array_sort2.h"
32 #include "utils/memalloc.h"
33
34
35
36 /*
37 * LIST OPERATIONS
38 */
39
40 /*
41 * Initialize list[k] to a singleton list
42 */
init_list(bvc_item_t * list,int32_t k)43 static inline void init_list(bvc_item_t *list, int32_t k) {
44 list[k].pre = k;
45 list[k].next = k;
46 }
47
48
49 /*
50 * Add i before k in list[k]
51 */
list_add(bvc_item_t * list,int32_t k,int32_t i)52 static inline void list_add(bvc_item_t *list, int32_t k, int32_t i) {
53 int32_t j;
54
55 assert(i != k);
56
57 j = list[k].pre;
58 list[j].next = i;
59 list[i].pre = j;
60 list[i].next = k;
61 list[k].pre = i;
62 }
63
64
65 /*
66 * Length of list k
67 */
list_length(bvc_item_t * list,int32_t k)68 static uint32_t list_length(bvc_item_t *list, int32_t k) {
69 uint32_t n;
70 int32_t j;
71
72 n = 0;
73 j = list[k].next;
74 while (j != k) {
75 n ++;
76 j = list[j].next;
77 }
78
79 return n;
80 }
81
82
83 /*
84 * Remove i from its current list
85 */
list_remove(bvc_item_t * list,int32_t i)86 static inline void list_remove(bvc_item_t *list, int32_t i) {
87 int32_t j, k;
88
89 j = list[i].pre;
90 k = list[i].next;
91 list[j].next = k;
92 list[k].pre = j;
93 }
94
95
96
97 /*
98 * Add n to one of the three node lists:
99 * - list[0] --> leaves
100 * - list[-1] --> elementary nodes
101 * - list[-2] --> default list
102 */
bvc_dag_add_to_leaves(bvc_dag_t * dag,bvnode_t n)103 static inline void bvc_dag_add_to_leaves(bvc_dag_t *dag, bvnode_t n) {
104 assert(0 < n && n <= dag->nelems);
105 list_add(dag->list, BVC_DAG_LEAF_LIST, n);
106 }
107
108
109 /*
110 * Move n to a different list
111 */
bvc_dag_move_to_leaves(bvc_dag_t * dag,bvnode_t n)112 static inline void bvc_dag_move_to_leaves(bvc_dag_t *dag, bvnode_t n) {
113 assert(0 < n && n <= dag->nelems);
114 list_remove(dag->list, n);
115 list_add(dag->list, BVC_DAG_LEAF_LIST, n);
116 }
117
bvc_dag_move_to_elementary_list(bvc_dag_t * dag,bvnode_t n)118 static inline void bvc_dag_move_to_elementary_list(bvc_dag_t *dag, bvnode_t n) {
119 assert(0 < n && n <= dag->nelems);
120 list_remove(dag->list, n);
121 list_add(dag->list, BVC_DAG_ELEM_LIST, n);
122 }
123
124
125 /*
126 * Auxiliary list
127 */
bvc_move_node_to_aux_list(bvc_dag_t * dag,bvnode_t n)128 void bvc_move_node_to_aux_list(bvc_dag_t *dag, bvnode_t n) {
129 assert(0 < n && n <= dag->nelems);
130 list_remove(dag->list, n);
131 list_add(dag->list, BVC_DAG_AUX_LIST, n);
132 }
133
134 /*
135 * Move list with header k into the list with header j
136 * list[j] must be empty (contain only j).
137 */
bvc_move_list(bvc_item_t * list,int32_t k,int32_t j)138 static void bvc_move_list(bvc_item_t *list, int32_t k, int32_t j) {
139 int32_t next_k, pre_k;
140
141 assert(j != k && j<=0 && k<=0 && list[j].pre == j && list[j].next == j);
142 pre_k = list[k].pre;
143 next_k = list[k].next;
144 if (pre_k != k) {
145 assert(next_k != k);
146 list[j].pre = pre_k;
147 list[pre_k].next = j;
148 list[j].next = next_k;
149 list[next_k].pre = j;
150
151 list[k].pre = k;
152 list[k].next = k;
153 }
154 }
155
156 /*
157 * Restore the elementary or default list from the aux list
158 */
bvc_move_aux_to_elem_list(bvc_dag_t * dag)159 void bvc_move_aux_to_elem_list(bvc_dag_t *dag) {
160 bvc_move_list(dag->list, BVC_DAG_AUX_LIST, BVC_DAG_ELEM_LIST);
161 }
162
bvc_move_aux_to_complex_list(bvc_dag_t * dag)163 void bvc_move_aux_to_complex_list(bvc_dag_t *dag) {
164 bvc_move_list(dag->list, BVC_DAG_AUX_LIST, BVC_DAG_DEFAULT_LIST);
165 }
166
167
168 /*
169 * FLIP BITS
170 */
alloc_flip_vector(bvc_dag_t * dag)171 static void alloc_flip_vector(bvc_dag_t *dag) {
172 if (dag->flipped == NULL) {
173 dag->flipped = allocate_bitvector0(dag->size);
174 }
175 }
176
177 // n = new size, dag->size = current size
extend_flip_vector(bvc_dag_t * dag,uint32_t n)178 static void extend_flip_vector(bvc_dag_t *dag, uint32_t n) {
179 assert(dag->size < n);
180 if (dag->flipped != NULL) {
181 dag->flipped = extend_bitvector0(dag->flipped, dag->size, n);
182 }
183 }
184
delete_flip_vector(bvc_dag_t * dag)185 static void delete_flip_vector(bvc_dag_t *dag) {
186 if (dag->flipped != NULL) {
187 delete_bitvector(dag->flipped);
188 dag->flipped = NULL;
189 }
190 }
191
192 // record that node i is flipped
mark_flipped_node(bvc_dag_t * dag,bvnode_t i)193 static void mark_flipped_node(bvc_dag_t *dag, bvnode_t i) {
194 assert(0 < i && i <= dag->nelems);
195 alloc_flip_vector(dag);
196 flip_bit(dag->flipped, i);
197 }
198
199 // check whether node i is flipped
node_has_flipped(bvc_dag_t * dag,bvnode_t i)200 static bool node_has_flipped(bvc_dag_t *dag, bvnode_t i) {
201 assert(0 < i && i <= dag->nelems);
202 return dag->flipped != NULL && tst_bit(dag->flipped, i);
203 }
204
205
206 /*
207 * DAG OPERATIONS
208 */
209
210 /*
211 * Initialize dag:
212 * - n = initial size. If n=0, use the default size.
213 */
init_bvc_dag(bvc_dag_t * dag,uint32_t n)214 void init_bvc_dag(bvc_dag_t *dag, uint32_t n) {
215 bvc_item_t *tmp;
216
217 if (n == 0) {
218 n = DEF_BVC_DAG_SIZE;
219 }
220 if (n >= MAX_BVC_DAG_SIZE) {
221 out_of_memory();
222 }
223 assert(n > 0);
224
225 dag->desc = (bvc_header_t **) safe_malloc(n * sizeof(bvc_header_t *));
226 dag->use = (int32_t **) safe_malloc(n * sizeof(int32_t *));
227 tmp = (bvc_item_t *) safe_malloc((n + 3) * sizeof(bvc_item_t));
228 dag->list = tmp + 3;
229 dag->flipped = NULL; // allocated on demand
230
231 dag->desc[0] = NULL;
232 dag->use[0] = NULL;
233 init_list(dag->list, -3);
234 init_list(dag->list, -2);
235 init_list(dag->list, -1);
236 init_list(dag->list, 0);
237
238 dag->nelems = 0;
239 dag->size = n;
240
241 init_int_htbl(&dag->htbl, 0);
242 init_int_bvset(&dag->vset, 0); // use bvset default size (1024)
243 init_int_hmap(&dag->vmap, 128);
244
245 init_objstore(&dag->leaf_store, sizeof(bvc_leaf_t), 500);
246 init_objstore(&dag->zero_store, sizeof(bvc_zero_t), 100);
247 init_objstore(&dag->constant_store, sizeof(bvc_constant_t), 100);
248 init_objstore(&dag->offset_store, sizeof(bvc_offset_t), 500);
249 init_objstore(&dag->mono_store, sizeof(bvc_mono_t), 500);
250 init_objstore(&dag->prod_store, sizeof(bvc_prod_t) + PROD_STORE_LEN * sizeof(varexp_t), 100);
251 init_objstore(&dag->sum_store1, sizeof(bvc_sum_t) + SUM_STORE1_LEN * sizeof(int32_t), 500);
252 init_objstore(&dag->sum_store2, sizeof(bvc_sum_t) + SUM_STORE2_LEN * sizeof(int32_t), 500);
253 init_objstore(&dag->alias_store, sizeof(bvc_alias_t), 100);
254
255 init_bvconstant(&dag->aux);
256 init_pp_buffer(&dag->pp_aux, 10);
257 init_bvpoly_buffer(&dag->poly_buffer);
258 init_ivector(&dag->buffer, 10);
259 init_ivector(&dag->sum_buffer, 10);
260 init_ivector(&dag->use_buffer, 10);
261 init_int_queue(&dag->node_queue, 0);
262 init_int_queue(&dag->flip_queue, 0);
263 }
264
265
266
267 /*
268 * Increase the size (by 50%)
269 */
extend_bvc_dag(bvc_dag_t * dag)270 static void extend_bvc_dag(bvc_dag_t *dag) {
271 bvc_item_t *tmp;
272 uint32_t n;
273
274 n = dag->size + 1;
275 n += (n >> 1);
276 if (n >= MAX_BVC_DAG_SIZE) {
277 out_of_memory();
278 }
279
280 assert(n > dag->size);
281
282 dag->desc = (bvc_header_t **) safe_realloc(dag->desc, n * sizeof(bvc_header_t *));
283 dag->use = (int32_t **) safe_realloc(dag->use, n * sizeof(int32_t *));
284 tmp = dag->list - 3;
285 tmp = (bvc_item_t *) safe_realloc(tmp, (n + 3) * sizeof(bvc_item_t));
286 dag->list = tmp + 3;
287
288 extend_flip_vector(dag, n);
289
290 dag->size = n;
291 }
292
293
294 /*
295 * Add a new node n with descriptor d
296 * - set use[n] to NULL
297 * - list[n] is not initialized
298 */
bvc_dag_add_node(bvc_dag_t * dag,bvc_header_t * d)299 static bvnode_t bvc_dag_add_node(bvc_dag_t *dag, bvc_header_t *d) {
300 uint32_t i;
301
302 i = dag->nelems + 1;
303 if (i == dag->size) {
304 extend_bvc_dag(dag);
305 }
306 assert(i < dag->size);
307
308 dag->desc[i] = d;
309 dag->use[i] = NULL;
310
311 dag->nelems = i;
312
313 return i;
314 }
315
316
317 /*
318 * Free memory used by descriptor d
319 * - free d itself if it's not form a store (i.e., d->size is large)
320 * - free d->constant.w if d->bitsize > 64
321 */
delete_descriptor(bvc_header_t * d)322 static void delete_descriptor(bvc_header_t *d) {
323 switch (d->tag) {
324 case BVC_LEAF:
325 case BVC_ZERO:
326 break;
327
328 case BVC_CONSTANT:
329 if (d->bitsize > 64) {
330 bvconst_free(bvconst_node(d)->value.w, (d->bitsize + 31) >> 5);
331 }
332 break;
333
334 case BVC_OFFSET:
335 if (d->bitsize > 64) {
336 bvconst_free(offset_node(d)->constant.w, (d->bitsize + 31) >> 5);
337 }
338 break;
339
340 case BVC_MONO:
341 if (d->bitsize > 64) {
342 bvconst_free(mono_node(d)->coeff.w, (d->bitsize + 31) >> 5);
343 }
344 break;
345
346 case BVC_PROD:
347 if (prod_node(d)->size > PROD_STORE_LEN) {
348 safe_free(d);
349 }
350 break;
351
352 case BVC_SUM:
353 if (sum_node(d)->size > SUM_STORE2_LEN) {
354 safe_free(d);
355 }
356 break;
357
358 case BVC_ALIAS:
359 break;
360 }
361 }
362
363
364 /*
365 * Delete the DAG
366 */
delete_bvc_dag(bvc_dag_t * dag)367 void delete_bvc_dag(bvc_dag_t *dag) {
368 uint32_t i, n;
369
370 n = dag->nelems;
371 for (i=1; i<=n; i++) {
372 delete_descriptor(dag->desc[i]);
373 delete_index_vector(dag->use[i]);
374 }
375
376 safe_free(dag->desc);
377 safe_free(dag->use);
378 safe_free(dag->list - 3);
379 delete_flip_vector(dag);
380
381 dag->desc = NULL;
382 dag->use = NULL;
383 dag->list = NULL;
384
385 delete_int_htbl(&dag->htbl);
386 delete_int_bvset(&dag->vset);
387 delete_int_hmap(&dag->vmap);
388
389 delete_objstore(&dag->leaf_store);
390 delete_objstore(&dag->zero_store);
391 delete_objstore(&dag->constant_store);
392 delete_objstore(&dag->offset_store);
393 delete_objstore(&dag->mono_store);
394 delete_objstore(&dag->prod_store);
395 delete_objstore(&dag->sum_store1);
396 delete_objstore(&dag->sum_store2);
397 delete_objstore(&dag->alias_store);
398
399 delete_bvconstant(&dag->aux);
400 delete_pp_buffer(&dag->pp_aux);
401 delete_bvpoly_buffer(&dag->poly_buffer);
402 delete_ivector(&dag->buffer);
403 delete_ivector(&dag->sum_buffer);
404 delete_ivector(&dag->use_buffer);
405 delete_int_queue(&dag->node_queue);
406 delete_int_queue(&dag->flip_queue);
407 }
408
409
410 /*
411 * Empty: remove all nodes
412 */
reset_bvc_dag(bvc_dag_t * dag)413 void reset_bvc_dag(bvc_dag_t *dag) {
414 uint32_t i, n;
415
416 n = dag->nelems;
417 for (i=1; i<=n; i++) {
418 delete_descriptor(dag->desc[i]);
419 delete_index_vector(dag->use[i]);
420 }
421
422 dag->nelems = 0;
423
424 // reset the lists
425 init_list(dag->list, -3);
426 init_list(dag->list, -2);
427 init_list(dag->list, -1);
428 init_list(dag->list, 0);
429
430 reset_int_htbl(&dag->htbl);
431 reset_int_bvset(&dag->vset);
432 int_hmap_reset(&dag->vmap);
433
434 reset_objstore(&dag->leaf_store);
435 reset_objstore(&dag->zero_store);
436 reset_objstore(&dag->constant_store);
437 reset_objstore(&dag->offset_store);
438 reset_objstore(&dag->mono_store);
439 reset_objstore(&dag->prod_store);
440 reset_objstore(&dag->sum_store1);
441 reset_objstore(&dag->sum_store2);
442 reset_objstore(&dag->alias_store);
443
444 pp_buffer_reset(&dag->pp_aux);
445 reset_bvpoly_buffer(&dag->poly_buffer, 32); // any positive bit-size would do
446 ivector_reset(&dag->buffer);
447 ivector_reset(&dag->sum_buffer);
448 ivector_reset(&dag->use_buffer);
449 int_queue_reset(&dag->node_queue);
450 int_queue_reset(&dag->flip_queue);
451 }
452
453
454
455
456 /*
457 * NODE DESCRIPTOR ALLOCATION
458 */
459
460 /*
461 * Descriptor allocation
462 * - for prod and sum, n = length of the sum or product
463 */
alloc_leaf(bvc_dag_t * dag)464 static inline bvc_leaf_t *alloc_leaf(bvc_dag_t *dag) {
465 return (bvc_leaf_t *) objstore_alloc(&dag->leaf_store);
466 }
467
alloc_zero(bvc_dag_t * dag)468 static inline bvc_zero_t *alloc_zero(bvc_dag_t *dag) {
469 return (bvc_zero_t *) objstore_alloc(&dag->zero_store);
470 }
471
alloc_bvconst(bvc_dag_t * dag)472 static inline bvc_constant_t *alloc_bvconst(bvc_dag_t *dag) {
473 return (bvc_constant_t *) objstore_alloc(&dag->constant_store);
474 }
475
alloc_offset(bvc_dag_t * dag)476 static inline bvc_offset_t *alloc_offset(bvc_dag_t *dag) {
477 return (bvc_offset_t *) objstore_alloc(&dag->offset_store);
478 }
479
alloc_mono(bvc_dag_t * dag)480 static inline bvc_mono_t *alloc_mono(bvc_dag_t *dag) {
481 return (bvc_mono_t *) objstore_alloc(&dag->mono_store);
482 }
483
alloc_prod(bvc_dag_t * dag,uint32_t n)484 static bvc_prod_t *alloc_prod(bvc_dag_t *dag, uint32_t n) {
485 void *tmp;
486
487 if (n <= PROD_STORE_LEN) {
488 tmp = objstore_alloc(&dag->prod_store);
489 } else if (n <= MAX_BVC_PROD_LEN) {
490 tmp = safe_malloc(sizeof(bvc_prod_t) + n * sizeof(varexp_t));
491 } else {
492 out_of_memory();
493 }
494
495 return (bvc_prod_t *) tmp;
496 }
497
alloc_sum(bvc_dag_t * dag,uint32_t n)498 static bvc_sum_t *alloc_sum(bvc_dag_t *dag, uint32_t n) {
499 void *tmp;
500
501 if (n <= SUM_STORE1_LEN) {
502 tmp = objstore_alloc(&dag->sum_store1);
503 } else if (n <= SUM_STORE2_LEN) {
504 tmp = objstore_alloc(&dag->sum_store2);
505 } else if (n <= MAX_BVC_SUM_LEN) {
506 tmp = safe_malloc(sizeof(bvc_sum_t) + n * sizeof(int32_t));
507 } else {
508 out_of_memory();
509 }
510
511 return (bvc_sum_t *) tmp;
512 }
513
514
alloc_alias(bvc_dag_t * dag)515 static inline bvc_alias_t *alloc_alias(bvc_dag_t *dag) {
516 return (bvc_alias_t *) objstore_alloc(&dag->alias_store);
517 }
518
519
520 /*
521 * De-allocation
522 */
free_leaf(bvc_dag_t * dag,bvc_leaf_t * d)523 static inline void free_leaf(bvc_dag_t *dag, bvc_leaf_t *d) {
524 objstore_free(&dag->leaf_store, d);
525 }
526
free_zero(bvc_dag_t * dag,bvc_zero_t * d)527 static inline void free_zero(bvc_dag_t *dag, bvc_zero_t *d) {
528 objstore_free(&dag->zero_store, d);
529 }
530
free_bvconst(bvc_dag_t * dag,bvc_constant_t * d)531 static inline void free_bvconst(bvc_dag_t *dag, bvc_constant_t *d) {
532 if (d->header.bitsize > 64) {
533 bvconst_free(d->value.w, (d->header.bitsize + 31) >> 5);
534 }
535 objstore_free(&dag->constant_store, d);
536 }
537
free_offset(bvc_dag_t * dag,bvc_offset_t * d)538 static void free_offset(bvc_dag_t *dag, bvc_offset_t *d) {
539 if (d->header.bitsize > 64) {
540 bvconst_free(d->constant.w, (d->header.bitsize + 31) >> 5);
541 }
542 objstore_free(&dag->offset_store, d);
543 }
544
free_mono(bvc_dag_t * dag,bvc_mono_t * d)545 static void free_mono(bvc_dag_t *dag, bvc_mono_t *d) {
546 if (d->header.bitsize > 64) {
547 bvconst_free(d->coeff.w, (d->header.bitsize + 31) >> 5);
548 }
549 objstore_free(&dag->mono_store, d);
550 }
551
free_prod(bvc_dag_t * dag,bvc_prod_t * d)552 static void free_prod(bvc_dag_t *dag, bvc_prod_t *d) {
553 if (d->size <= PROD_STORE_LEN) {
554 objstore_free(&dag->prod_store, d);
555 } else {
556 safe_free(d);
557 }
558 }
559
free_sum(bvc_dag_t * dag,bvc_sum_t * d)560 static void free_sum(bvc_dag_t *dag, bvc_sum_t *d) {
561 if (d->size <= SUM_STORE1_LEN) {
562 objstore_free(&dag->sum_store1, d);
563 } else if (d->size <= SUM_STORE2_LEN) {
564 objstore_free(&dag->sum_store2, d);
565 } else {
566 safe_free(d);
567 }
568 }
569
free_alias(bvc_dag_t * dag,bvc_alias_t * d)570 static inline void free_alias(bvc_dag_t *dag, bvc_alias_t *d) {
571 objstore_free(&dag->alias_store, d);
572 }
573
free_descriptor(bvc_dag_t * dag,bvc_header_t * d)574 static void free_descriptor(bvc_dag_t *dag, bvc_header_t *d) {
575 switch (d->tag) {
576 case BVC_LEAF:
577 free_leaf(dag, leaf_node(d));
578 break;
579
580 case BVC_ZERO:
581 free_zero(dag, zero_node(d));
582 break;
583
584 case BVC_CONSTANT:
585 free_bvconst(dag, bvconst_node(d));
586 break;
587
588 case BVC_OFFSET:
589 free_offset(dag, offset_node(d));
590 break;
591
592 case BVC_MONO:
593 free_mono(dag, mono_node(d));
594 break;
595
596 case BVC_PROD:
597 free_prod(dag, prod_node(d));
598 break;
599
600 case BVC_SUM:
601 free_sum(dag, sum_node(d));
602 break;
603
604 case BVC_ALIAS:
605 free_alias(dag, alias_node(d));
606 break;
607 }
608 }
609
610
611
612 /*
613 * Check whether a node is elementary
614 */
offset_node_is_elementary(bvc_dag_t * dag,bvc_offset_t * d)615 static inline bool offset_node_is_elementary(bvc_dag_t *dag, bvc_offset_t *d) {
616 return bvc_dag_occ_is_leaf(dag, d->nocc);
617 }
618
mono_node_is_elementary(bvc_dag_t * dag,bvc_mono_t * d)619 static inline bool mono_node_is_elementary(bvc_dag_t *dag, bvc_mono_t *d) {
620 return bvc_dag_occ_is_leaf(dag, d->nocc);
621 }
622
prod_node_is_elementary(bvc_dag_t * dag,bvc_prod_t * d)623 static bool prod_node_is_elementary(bvc_dag_t *dag, bvc_prod_t *d) {
624 assert(d->len >= 1);
625
626 if (d->len == 1) {
627 return d->prod[0].exp == 2 && bvc_dag_occ_is_leaf(dag, d->prod[0].var);
628 } else if (d->len == 2) {
629 return d->prod[0].exp + d->prod[1].exp == 2 &&
630 bvc_dag_occ_is_leaf(dag, d->prod[0].var) &&
631 bvc_dag_occ_is_leaf(dag, d->prod[1].var);
632 } else {
633 return false;
634 }
635 }
636
sum_node_is_elementary(bvc_dag_t * dag,bvc_sum_t * d)637 static bool sum_node_is_elementary(bvc_dag_t *dag, bvc_sum_t * d) {
638 assert(d->len >= 2);
639 return d->len == 2 && bvc_dag_occ_is_leaf(dag, d->sum[0]) && bvc_dag_occ_is_leaf(dag, d->sum[1]);
640 }
641
node_is_elementary(bvc_dag_t * dag,bvnode_t i)642 static bool node_is_elementary(bvc_dag_t *dag, bvnode_t i) {
643 bvc_header_t *d;
644
645 assert(0 < i && i <= dag->nelems);
646
647 d = dag->desc[i];
648 switch (d->tag) {
649 case BVC_LEAF:
650 case BVC_ALIAS:
651 break;
652
653 case BVC_ZERO:
654 case BVC_CONSTANT:
655 return true;
656
657 case BVC_OFFSET:
658 return offset_node_is_elementary(dag, offset_node(d));
659
660 case BVC_MONO:
661 return mono_node_is_elementary(dag, mono_node(d));
662
663 case BVC_PROD:
664 return prod_node_is_elementary(dag, prod_node(d));
665
666 case BVC_SUM:
667 return sum_node_is_elementary(dag, sum_node(d));
668 }
669
670 return false;
671 }
672
673
674
675
676 /*
677 * MORE CHECKS
678 */
bvnode_num_occs(bvc_dag_t * dag,bvnode_t i)679 static uint32_t bvnode_num_occs(bvc_dag_t *dag, bvnode_t i) {
680 int32_t *l;
681
682 assert(0 < i && i <= dag->nelems);
683 l = dag->use[i];
684 return l != NULL ? iv_size(l) : 0;
685 }
686
687
688 /*
689 * Check whether n is shared (i.e., it occurs more than once)
690 */
bvc_dag_occ_is_shared(bvc_dag_t * dag,node_occ_t n)691 bool bvc_dag_occ_is_shared(bvc_dag_t *dag, node_occ_t n) {
692 int32_t *l;
693
694 assert(0 < node_of_occ(n) && node_of_occ(n) <= dag->nelems);
695
696 l = dag->use[node_of_occ(n)];
697 return l != NULL && iv_size(l) > 1;
698 }
699
700
701
702
703
704 /*
705 * NODE CONSTRUCTION
706 */
707
708 /*
709 * Add i to the use list of n.
710 */
bvc_dag_add_dependency(bvc_dag_t * dag,bvnode_t n,bvnode_t i)711 static inline void bvc_dag_add_dependency(bvc_dag_t *dag, bvnode_t n, bvnode_t i) {
712 assert(0 < n && n <= dag->nelems && 0 < i && i <= dag->nelems && i != n);
713 add_index_to_vector(dag->use + n, i);
714 }
715
716
717 /*
718 * Bit hash:
719 * - for a node index n, the bit_hash is a 32bit word
720 * equal to (1 << (n & 31)): i.e., bit i is set if (n % 32 == i).
721 * - for a set of node indices, the bit hash is the bitwise or
722 * of the bit_hash of each element
723 *
724 * This gives a quick filter to test inclusion between sets of
725 * nodes: if bit_hash(A) & bit_hash(B) != bit_hash(A) then
726 * A can't be a subset of B.
727 */
bit_hash(bvnode_t n)728 static inline uint32_t bit_hash(bvnode_t n) {
729 assert(n > 0);
730 return ((uint32_t) 1) << (n & 31);
731 }
732
bit_hash_occ(node_occ_t n)733 static inline uint32_t bit_hash_occ(node_occ_t n) {
734 return bit_hash(node_of_occ(n));
735 }
736
737
738 /*
739 * Create a leaf node
740 */
bvc_dag_mk_leaf(bvc_dag_t * dag,int32_t x,uint32_t bitsize)741 static bvnode_t bvc_dag_mk_leaf(bvc_dag_t *dag, int32_t x, uint32_t bitsize) {
742 bvc_leaf_t *d;
743 bvnode_t q;
744
745 d = alloc_leaf(dag);
746 d->header.tag = BVC_LEAF;
747 d->header.bitsize = bitsize;
748 d->map = x;
749
750 q = bvc_dag_add_node(dag, &d->header);
751 bvc_dag_add_to_leaves(dag, q);
752
753 return q;
754 }
755
756
757 /*
758 * Create a zero node
759 */
bvc_dag_mk_zero(bvc_dag_t * dag,uint32_t bitsize)760 static bvnode_t bvc_dag_mk_zero(bvc_dag_t *dag, uint32_t bitsize) {
761 bvc_zero_t *d;
762 bvnode_t q;
763
764 d = alloc_zero(dag);
765 d->header.tag = BVC_ZERO;
766 d->header.bitsize = bitsize;
767
768 q = bvc_dag_add_node(dag, &d->header);
769
770 // add to the list of elementary nodes
771 list_add(dag->list, BVC_DAG_ELEM_LIST, q);
772
773 return q;
774 }
775
776
777 /*
778 * Create a constant node
779 * - a = constant (normalized modulo 2^bitsize)
780 * - a must not be zero
781 */
bvc_dag_mk_const64(bvc_dag_t * dag,uint64_t a,uint32_t bitsize)782 static bvnode_t bvc_dag_mk_const64(bvc_dag_t *dag, uint64_t a, uint32_t bitsize) {
783 bvc_constant_t *d;
784 bvnode_t q;
785
786 assert(1 <= bitsize && bitsize <= 64 && a == norm64(a, bitsize) && a != 0);
787
788 d = alloc_bvconst(dag);
789 d->header.tag = BVC_CONSTANT;
790 d->header.bitsize = bitsize;
791 d->value.c = a;
792
793 q = bvc_dag_add_node(dag, &d->header);
794
795 // elementary node
796 list_add(dag->list, BVC_DAG_ELEM_LIST, q);
797
798 return q;
799 }
800
bvc_dag_mk_const(bvc_dag_t * dag,uint32_t * a,uint32_t bitsize)801 static bvnode_t bvc_dag_mk_const(bvc_dag_t *dag, uint32_t *a, uint32_t bitsize) {
802 bvc_constant_t *d;
803 uint32_t *c;
804 uint32_t k;
805 bvnode_t q;
806
807 assert(bitsize > 64);
808
809 // make a copy of a: a must be normalized and non-zero
810 k = (bitsize + 31) >> 5;
811 c = bvconst_alloc(k);
812 bvconst_set(c, k, a);
813 assert(bvconst_is_normalized(c, bitsize) && bvconst_is_nonzero(c, k));
814
815 d = alloc_bvconst(dag);
816 d->header.tag = BVC_CONSTANT;
817 d->header.bitsize = bitsize;
818 d->value.w = c;
819
820 q = bvc_dag_add_node(dag, &d->header);
821
822 // elementary node
823 list_add(dag->list, BVC_DAG_ELEM_LIST, q);
824
825 return q;
826 }
827
828
829
830 /*
831 * Create an offset node q := [offset a n]
832 */
bvc_dag_mk_offset64(bvc_dag_t * dag,uint64_t a,node_occ_t n,uint32_t bitsize)833 static bvnode_t bvc_dag_mk_offset64(bvc_dag_t *dag, uint64_t a, node_occ_t n, uint32_t bitsize) {
834 bvc_offset_t *d;
835 bvnode_t q;
836 int32_t k;
837
838 assert(1 <= bitsize && bitsize <= 64 && a == norm64(a, bitsize));
839
840 d = alloc_offset(dag);
841 d->header.tag = BVC_OFFSET;
842 d->header.bitsize = bitsize;
843 d->nocc = n;
844 d->constant.c = a;
845
846 q = bvc_dag_add_node(dag, &d->header);
847 bvc_dag_add_dependency(dag, node_of_occ(n), q); // q depends on n
848
849 k = BVC_DAG_DEFAULT_LIST;
850 if (bvc_dag_occ_is_leaf(dag, n)) {
851 k = BVC_DAG_ELEM_LIST;
852 }
853 list_add(dag->list, k, q);
854
855 return q;
856 }
857
858
bvc_dag_mk_offset(bvc_dag_t * dag,uint32_t * a,node_occ_t n,uint32_t bitsize)859 static bvnode_t bvc_dag_mk_offset(bvc_dag_t *dag, uint32_t *a, node_occ_t n, uint32_t bitsize) {
860 bvc_offset_t *d;
861 uint32_t *c;
862 uint32_t k;
863 bvnode_t q;
864 int32_t l;
865
866 assert(bitsize > 64);
867
868 // make a copy of a: a must be normalized so the copy will be normalized too
869 k = (bitsize + 31) >> 5;
870 c = bvconst_alloc(k);
871 bvconst_set(c, k, a);
872 assert(bvconst_is_normalized(c, bitsize));
873
874 d = alloc_offset(dag);
875 d->header.tag = BVC_OFFSET;
876 d->header.bitsize = bitsize;
877 d->nocc = n;
878 d->constant.w = c;
879
880 q = bvc_dag_add_node(dag, &d->header);
881 bvc_dag_add_dependency(dag, node_of_occ(n), q); // q depends on n
882
883 l = BVC_DAG_DEFAULT_LIST;
884 if (bvc_dag_occ_is_leaf(dag, n)) {
885 l = BVC_DAG_ELEM_LIST;
886 }
887 list_add(dag->list, l, q);
888
889
890 return q;
891 }
892
893
894
895 /*
896 * Create a monomial node q := [mono a, n]
897 */
bvc_dag_mk_mono64(bvc_dag_t * dag,uint64_t a,node_occ_t n,uint32_t bitsize)898 static bvnode_t bvc_dag_mk_mono64(bvc_dag_t *dag, uint64_t a, node_occ_t n, uint32_t bitsize) {
899 bvc_mono_t *d;
900 bvnode_t q;
901 int32_t k;
902
903 assert(1 <= bitsize && bitsize <= 64 && a == norm64(a, bitsize));
904
905 d = alloc_mono(dag);
906 d->header.tag = BVC_MONO;
907 d->header.bitsize = bitsize;
908 d->nocc = n;
909 d->coeff.c = a;
910
911 q = bvc_dag_add_node(dag, &d->header);
912 bvc_dag_add_dependency(dag, node_of_occ(n), q); // q depends on n
913
914 k = BVC_DAG_DEFAULT_LIST;
915 if (bvc_dag_occ_is_leaf(dag, n)) {
916 k = BVC_DAG_ELEM_LIST;
917 }
918 list_add(dag->list, k, q);
919
920
921 return q;
922 }
923
924
bvc_dag_mk_mono(bvc_dag_t * dag,uint32_t * a,node_occ_t n,uint32_t bitsize)925 static bvnode_t bvc_dag_mk_mono(bvc_dag_t *dag, uint32_t *a, node_occ_t n, uint32_t bitsize) {
926 bvc_mono_t *d;
927 uint32_t *c;
928 uint32_t k;
929 bvnode_t q;
930 int32_t l;
931
932 assert(bitsize > 64 && bvconst_is_normalized(a, bitsize));
933
934 // make a copy of a.
935 // a must be normalized so the copy will be normalized too
936 k = (bitsize + 31) >> 5;
937 c = bvconst_alloc(k);
938 bvconst_set(c, k, a);
939 assert(bvconst_is_normalized(c, bitsize));
940
941 d = alloc_mono(dag);
942 d->header.tag = BVC_MONO;
943 d->header.bitsize = bitsize;
944 d->nocc = n;
945 d->coeff.w = c;
946
947 q = bvc_dag_add_node(dag, &d->header);
948 bvc_dag_add_dependency(dag, node_of_occ(n), q); // q depends on n
949
950 l = BVC_DAG_DEFAULT_LIST;
951 if (bvc_dag_occ_is_leaf(dag, n)) {
952 l = BVC_DAG_ELEM_LIST;
953 }
954 list_add(dag->list, l, q);
955
956 return q;
957 }
958
959
960 /*
961 * Product node defined by a[0 ... n-1]:
962 * - each a[i] is a pair (node, exponent)
963 */
bvc_dag_mk_prod(bvc_dag_t * dag,varexp_t * a,uint32_t n,uint32_t bitsize)964 static bvnode_t bvc_dag_mk_prod(bvc_dag_t *dag, varexp_t *a, uint32_t n, uint32_t bitsize) {
965 bvc_prod_t *d;
966 uint32_t i;
967 int32_t q, k;
968
969 d = alloc_prod(dag, n);
970 d->header.tag = BVC_PROD;
971 d->header.bitsize = bitsize;
972 d->hash = 0;
973 d->size = n;
974 d->len = n;
975 for (i=0; i<n; i++) {
976 d->prod[i] = a[i];
977 d->hash |= bit_hash_occ(a[i].var);
978 }
979
980 q = bvc_dag_add_node(dag, &d->header);
981 for (i=0; i<n; i++) {
982 bvc_dag_add_dependency(dag, node_of_occ(a[i].var), q);
983 }
984
985 k = BVC_DAG_DEFAULT_LIST;
986 if (prod_node_is_elementary(dag, d)) {
987 k = BVC_DAG_ELEM_LIST;
988 }
989 list_add(dag->list, k, q);
990
991 return q;
992 }
993
994
995
996 /*
997 * Sum mode a[0] + ... + a[n-1]
998 * - each a[i] is a node occurrence
999 */
bvc_dag_mk_sum(bvc_dag_t * dag,node_occ_t * a,uint32_t n,uint32_t bitsize)1000 static bvnode_t bvc_dag_mk_sum(bvc_dag_t *dag, node_occ_t *a, uint32_t n, uint32_t bitsize) {
1001 bvc_sum_t *d;
1002 uint32_t i;
1003 bvnode_t q;
1004 int32_t k;
1005
1006 d = alloc_sum(dag, n);
1007 d->header.tag = BVC_SUM;
1008 d->header.bitsize = bitsize;
1009 d->hash = 0;
1010 d->size = n;
1011 d->len = n;
1012 for (i=0; i<n; i++) {
1013 d->sum[i] = a[i];
1014 d->hash |= bit_hash_occ(a[i]);
1015 }
1016
1017 q = bvc_dag_add_node(dag, &d->header);
1018 for (i=0; i<n; i++) {
1019 bvc_dag_add_dependency(dag, node_of_occ(a[i]), q);
1020 }
1021
1022 k = BVC_DAG_DEFAULT_LIST;
1023 if (sum_node_is_elementary(dag, d)) {
1024 k = BVC_DAG_ELEM_LIST;
1025 }
1026 list_add(dag->list, k, q);
1027
1028 return q;
1029 }
1030
1031
1032 /*
1033 * HASH CONSING
1034 */
1035 typedef struct bvc_leaf_hobj_s {
1036 int_hobj_t m;
1037 bvc_dag_t *dag;
1038 uint32_t bitsize;
1039 int32_t map;
1040 } bvc_leaf_hobj_t;
1041
1042 typedef struct bvc_zero_hobj_s {
1043 int_hobj_t m;
1044 bvc_dag_t *dag;
1045 uint32_t bitsize;
1046 } bvc_zero_hobj_t;
1047
1048 typedef struct bvc_const64_hobj_s {
1049 int_hobj_t m;
1050 bvc_dag_t *dag;
1051 uint64_t c;
1052 uint32_t bitsize;
1053 } bvc_const64_hobj_t;
1054
1055 typedef struct bvc_const_hobj_s {
1056 int_hobj_t m;
1057 bvc_dag_t *dag;
1058 uint32_t *c;
1059 uint32_t bitsize;
1060 } bvc_const_hobj_t;
1061
1062
1063 // same struct for both offset/mono with 64bit constant
1064 typedef struct bvc64_hobj_s {
1065 int_hobj_t m;
1066 bvc_dag_t *dag;
1067 uint64_t c;
1068 uint32_t bitsize;
1069 node_occ_t nocc;
1070 } bvc64_hobj_t;
1071
1072 // struct for offset/mono with larger constant
1073 typedef struct bvc_hobj_s {
1074 int_hobj_t m;
1075 bvc_dag_t *dag;
1076 uint32_t *c;
1077 uint32_t bitsize;
1078 node_occ_t nocc;
1079 } bvc_hobj_t;
1080
1081 typedef struct bvc_prod_hobj_s {
1082 int_hobj_t m;
1083 bvc_dag_t *dag;
1084 varexp_t *pp;
1085 uint32_t bitsize;
1086 uint32_t len;
1087 } bvc_prod_hobj_t;
1088
1089 typedef struct bvc_sum_hobj_s {
1090 int_hobj_t m;
1091 bvc_dag_t *dag;
1092 node_occ_t *noccs;
1093 uint32_t bitsize;
1094 uint32_t len;
1095 } bvc_sum_hobj_t;
1096
1097
1098 /*
1099 * Hash functions
1100 */
hash_bvc_leaf_hobj(bvc_leaf_hobj_t * p)1101 static uint32_t hash_bvc_leaf_hobj(bvc_leaf_hobj_t *p) {
1102 return jenkins_hash_pair(p->map, 0, 0x12930a32);
1103 }
1104
hash_bvc_zero_hobj(bvc_zero_hobj_t * p)1105 static uint32_t hash_bvc_zero_hobj(bvc_zero_hobj_t *p) {
1106 return jenkins_hash_uint32(p->bitsize);
1107 }
1108
hash_bvc_const64_hobj(bvc_const64_hobj_t * p)1109 static uint32_t hash_bvc_const64_hobj(bvc_const64_hobj_t *p) {
1110 uint32_t a;
1111
1112 a = jenkins_hash_uint64(p->c);
1113 return jenkins_hash_pair(a, p->bitsize, 0x38e89caf);
1114 }
1115
hash_bvc_const_hobj(bvc_const_hobj_t * p)1116 static uint32_t hash_bvc_const_hobj(bvc_const_hobj_t *p) {
1117 uint32_t a;
1118
1119 a = bvconst_hash(p->c, p->bitsize);
1120 return jenkins_hash_pair(a, p->bitsize, 0xeefa345a);
1121 }
1122
hash_bvc_offset64_hobj(bvc64_hobj_t * p)1123 static uint32_t hash_bvc_offset64_hobj(bvc64_hobj_t *p) {
1124 uint32_t a, b;
1125
1126 a = jenkins_hash_uint64(p->c);
1127 b = jenkins_hash_int32(p->nocc);
1128 return jenkins_hash_pair(a, b, 0x23da32aa);
1129 }
1130
hash_bvc_offset_hobj(bvc_hobj_t * p)1131 static uint32_t hash_bvc_offset_hobj(bvc_hobj_t *p) {
1132 uint32_t a, b;
1133
1134 a = bvconst_hash(p->c, p->bitsize);
1135 b = jenkins_hash_int32(p->nocc);
1136 return jenkins_hash_pair(a, b, 0x32288cc9);
1137 }
1138
hash_bvc_mono64_hobj(bvc64_hobj_t * p)1139 static uint32_t hash_bvc_mono64_hobj(bvc64_hobj_t *p) {
1140 uint32_t a, b;
1141
1142 a = jenkins_hash_uint64(p->c);
1143 b = jenkins_hash_int32(p->nocc);
1144 return jenkins_hash_pair(a, b, 0xaef43e27);
1145 }
1146
hash_bvc_mono_hobj(bvc_hobj_t * p)1147 static uint32_t hash_bvc_mono_hobj(bvc_hobj_t *p) {
1148 uint32_t a, b;
1149
1150 a = bvconst_hash(p->c, p->bitsize);
1151 b = jenkins_hash_int32(p->nocc);
1152 return jenkins_hash_pair(a, b, 0xfe43a091);
1153 }
1154
1155 // p->pp = array of len pairs of int32_t
hash_bvc_prod_hobj(bvc_prod_hobj_t * p)1156 static uint32_t hash_bvc_prod_hobj(bvc_prod_hobj_t *p) {
1157 assert(p->len <= UINT32_MAX/2);
1158 return jenkins_hash_intarray2((int32_t *) p->pp, 2 * p->len, 0x7432cde2);
1159 }
1160
hash_bvc_sum_hobj(bvc_sum_hobj_t * p)1161 static uint32_t hash_bvc_sum_hobj(bvc_sum_hobj_t *p) {
1162 return jenkins_hash_intarray2(p->noccs, p->len, 0xaeb32a06);
1163 }
1164
1165
1166 /*
1167 * Equality tests
1168 */
eq_bvc_leaf_hobj(bvc_leaf_hobj_t * p,bvnode_t i)1169 static bool eq_bvc_leaf_hobj(bvc_leaf_hobj_t *p, bvnode_t i) {
1170 bvc_header_t *d;
1171
1172 d = p->dag->desc[i];
1173 return d->tag == BVC_LEAF && leaf_node(d)->map == p->map;
1174 }
1175
eq_bvc_zero_hobj(bvc_zero_hobj_t * p,bvnode_t i)1176 static bool eq_bvc_zero_hobj(bvc_zero_hobj_t *p, bvnode_t i) {
1177 bvc_header_t *d;
1178
1179 d = p->dag->desc[i];
1180 return d->tag == BVC_ZERO && d->bitsize == p->bitsize;
1181 }
1182
eq_bvc_const64_hobj(bvc_const64_hobj_t * p,bvnode_t i)1183 static bool eq_bvc_const64_hobj(bvc_const64_hobj_t *p, bvnode_t i) {
1184 bvc_header_t *d;
1185 bvc_constant_t *o;
1186
1187 d = p->dag->desc[i];
1188 if (d->tag != BVC_CONSTANT || d->bitsize != p->bitsize) {
1189 return false;
1190 }
1191 o = bvconst_node(d);
1192 return o->value.c == p->c;
1193 }
1194
eq_bvc_const_hobj(bvc_const_hobj_t * p,bvnode_t i)1195 static bool eq_bvc_const_hobj(bvc_const_hobj_t *p, bvnode_t i) {
1196 bvc_header_t *d;
1197 bvc_constant_t *o;
1198 uint32_t k;
1199
1200 d = p->dag->desc[i];
1201 if (d->tag != BVC_CONSTANT || d->bitsize != p->bitsize) {
1202 return false;
1203 }
1204 o = bvconst_node(d);
1205 k = (d->bitsize + 31) >> 5;
1206 return bvconst_eq(o->value.w, p->c, k);
1207 }
1208
eq_bvc_offset64_hobj(bvc64_hobj_t * p,bvnode_t i)1209 static bool eq_bvc_offset64_hobj(bvc64_hobj_t *p, bvnode_t i) {
1210 bvc_header_t *d;
1211 bvc_offset_t *o;
1212
1213 d = p->dag->desc[i];
1214 if (d->tag != BVC_OFFSET || d->bitsize != p->bitsize) {
1215 return false;
1216 }
1217 o = offset_node(d);
1218 return o->nocc == p->nocc && o->constant.c == p->c;
1219 }
1220
eq_bvc_offset_hobj(bvc_hobj_t * p,bvnode_t i)1221 static bool eq_bvc_offset_hobj(bvc_hobj_t *p, bvnode_t i) {
1222 bvc_header_t *d;
1223 bvc_offset_t *o;
1224 uint32_t k;
1225
1226 d = p->dag->desc[i];
1227 if (d->tag != BVC_OFFSET && d->bitsize != p->bitsize) {
1228 return false;
1229 }
1230 o = offset_node(d);
1231 k = (d->bitsize + 31) >> 5;
1232 return o->nocc == p->nocc && bvconst_eq(o->constant.w, p->c, k);
1233 }
1234
eq_bvc_mono64_hobj(bvc64_hobj_t * p,bvnode_t i)1235 static bool eq_bvc_mono64_hobj(bvc64_hobj_t *p, bvnode_t i) {
1236 bvc_header_t *d;
1237 bvc_mono_t *o;
1238
1239 d = p->dag->desc[i];
1240 if (d->tag != BVC_MONO && d->bitsize != p->bitsize) {
1241 return false;
1242 }
1243 o = mono_node(d);
1244 return o->nocc == p->nocc && o->coeff.c == p->c;
1245 }
1246
eq_bvc_mono_hobj(bvc_hobj_t * p,bvnode_t i)1247 static bool eq_bvc_mono_hobj(bvc_hobj_t *p, bvnode_t i) {
1248 bvc_header_t *d;
1249 bvc_mono_t *o;
1250 uint32_t k;
1251
1252 d = p->dag->desc[i];
1253 if (d->tag != BVC_MONO || d->bitsize != p->bitsize) {
1254 return false;
1255 }
1256 o = mono_node(d);
1257 k = (d->bitsize + 31) >> 5;
1258 return o->nocc == p->nocc && bvconst_eq(o->coeff.w, p->c, k);
1259 }
1260
eq_bvc_prod_hobj(bvc_prod_hobj_t * p,bvnode_t i)1261 static bool eq_bvc_prod_hobj(bvc_prod_hobj_t *p, bvnode_t i) {
1262 bvc_header_t *d;
1263 bvc_prod_t *o;
1264 uint32_t j, n;
1265
1266 d = p->dag->desc[i];
1267 if (d->tag != BVC_PROD || d->bitsize != p->bitsize) {
1268 return false;
1269 }
1270 o = prod_node(d);
1271 n = o->len;
1272 if (n != p-> len) {
1273 return false;
1274 }
1275
1276 for (j=0; j<n; j++) {
1277 if (p->pp[j].var != o->prod[j].var ||
1278 p->pp[j].exp != o->prod[j].exp) {
1279 return false;
1280 }
1281 }
1282
1283 return true;
1284 }
1285
eq_bvc_sum_hobj(bvc_sum_hobj_t * p,bvnode_t i)1286 static bool eq_bvc_sum_hobj(bvc_sum_hobj_t *p, bvnode_t i) {
1287 bvc_header_t *d;
1288 bvc_sum_t *o;
1289 uint32_t j, n;
1290
1291 d = p->dag->desc[i];
1292 if (d->tag != BVC_SUM || d->bitsize != p->bitsize) {
1293 return false;
1294 }
1295 o = sum_node(d);
1296 n = o->len;
1297 if (n != p-> len) {
1298 return false;
1299 }
1300
1301 for (j=0; j<n; j++) {
1302 if (p->noccs[j] != o->sum[j]) {
1303 return false;
1304 }
1305 }
1306
1307 return true;
1308 }
1309
1310
1311 /*
1312 * Constructors
1313 */
build_bvc_leaf_hobj(bvc_leaf_hobj_t * p)1314 static bvnode_t build_bvc_leaf_hobj(bvc_leaf_hobj_t *p) {
1315 return bvc_dag_mk_leaf(p->dag, p->map, p->bitsize);
1316 }
1317
build_bvc_zero_hobj(bvc_zero_hobj_t * p)1318 static bvnode_t build_bvc_zero_hobj(bvc_zero_hobj_t *p) {
1319 return bvc_dag_mk_zero(p->dag, p->bitsize);
1320 }
1321
build_bvc_const64_hobj(bvc_const64_hobj_t * p)1322 static bvnode_t build_bvc_const64_hobj(bvc_const64_hobj_t *p) {
1323 return bvc_dag_mk_const64(p->dag, p->c, p->bitsize);
1324 }
1325
build_bvc_const_hobj(bvc_const_hobj_t * p)1326 static bvnode_t build_bvc_const_hobj(bvc_const_hobj_t *p) {
1327 return bvc_dag_mk_const(p->dag, p->c, p->bitsize);
1328 }
1329
build_bvc_offset64_hobj(bvc64_hobj_t * p)1330 static bvnode_t build_bvc_offset64_hobj(bvc64_hobj_t *p) {
1331 return bvc_dag_mk_offset64(p->dag, p->c, p->nocc, p->bitsize);
1332 }
1333
build_bvc_offset_hobj(bvc_hobj_t * p)1334 static bvnode_t build_bvc_offset_hobj(bvc_hobj_t *p) {
1335 return bvc_dag_mk_offset(p->dag, p->c, p->nocc, p->bitsize);
1336 }
1337
build_bvc_mono64_hobj(bvc64_hobj_t * p)1338 static bvnode_t build_bvc_mono64_hobj(bvc64_hobj_t *p) {
1339 return bvc_dag_mk_mono64(p->dag, p->c, p->nocc, p->bitsize);
1340 }
1341
build_bvc_mono_hobj(bvc_hobj_t * p)1342 static bvnode_t build_bvc_mono_hobj(bvc_hobj_t *p) {
1343 return bvc_dag_mk_mono(p->dag, p->c, p->nocc, p->bitsize);
1344 }
1345
build_bvc_prod_hobj(bvc_prod_hobj_t * p)1346 static bvnode_t build_bvc_prod_hobj(bvc_prod_hobj_t *p) {
1347 return bvc_dag_mk_prod(p->dag, p->pp, p->len, p->bitsize);
1348 }
1349
build_bvc_sum_hobj(bvc_sum_hobj_t * p)1350 static bvnode_t build_bvc_sum_hobj(bvc_sum_hobj_t *p) {
1351 return bvc_dag_mk_sum(p->dag, p->noccs, p->len, p->bitsize);
1352 }
1353
1354 /*
1355 * Hash-consing constructors
1356 */
bvc_dag_get_leaf(bvc_dag_t * dag,int32_t x,uint32_t bitsize)1357 static bvnode_t bvc_dag_get_leaf(bvc_dag_t *dag, int32_t x, uint32_t bitsize) {
1358 bvc_leaf_hobj_t bvc_leaf_hobj;
1359 bvc_leaf_hobj.m.hash = (hobj_hash_t) hash_bvc_leaf_hobj;
1360 bvc_leaf_hobj.m.eq = (hobj_eq_t) eq_bvc_leaf_hobj;
1361 bvc_leaf_hobj.m.build = (hobj_build_t) build_bvc_leaf_hobj;
1362 bvc_leaf_hobj.dag = dag;
1363 bvc_leaf_hobj.bitsize = bitsize;
1364 bvc_leaf_hobj.map = x;
1365 return int_htbl_get_obj(&dag->htbl, &bvc_leaf_hobj.m);
1366 }
1367
bvc_dag_get_zero(bvc_dag_t * dag,uint32_t bitsize)1368 static bvnode_t bvc_dag_get_zero(bvc_dag_t *dag, uint32_t bitsize) {
1369 bvc_zero_hobj_t bvc_zero_hobj;
1370 bvc_zero_hobj.m.hash = (hobj_hash_t) hash_bvc_zero_hobj;
1371 bvc_zero_hobj.m.eq = (hobj_eq_t) eq_bvc_zero_hobj;
1372 bvc_zero_hobj.m.build = (hobj_build_t) build_bvc_zero_hobj;
1373 bvc_zero_hobj.dag = dag;
1374 bvc_zero_hobj.bitsize = bitsize;
1375 return int_htbl_get_obj(&dag->htbl, &bvc_zero_hobj.m);
1376 }
1377
bvc_dag_get_const64(bvc_dag_t * dag,uint64_t a,uint32_t bitsize)1378 static bvnode_t bvc_dag_get_const64(bvc_dag_t *dag, uint64_t a, uint32_t bitsize) {
1379 bvc_const64_hobj_t bvc_const64_hobj;
1380 bvc_const64_hobj.m.hash = (hobj_hash_t) hash_bvc_const64_hobj;
1381 bvc_const64_hobj.m.eq = (hobj_eq_t) eq_bvc_const64_hobj;
1382 bvc_const64_hobj.m.build = (hobj_build_t) build_bvc_const64_hobj;
1383 bvc_const64_hobj.dag = dag;
1384 bvc_const64_hobj.c = a;
1385 bvc_const64_hobj.bitsize = bitsize;
1386 return int_htbl_get_obj(&dag->htbl, &bvc_const64_hobj.m);
1387 }
1388
bvc_dag_get_const(bvc_dag_t * dag,uint32_t * a,uint32_t bitsize)1389 static bvnode_t bvc_dag_get_const(bvc_dag_t *dag, uint32_t *a, uint32_t bitsize) {
1390 bvc_const_hobj_t bvc_const_hobj;
1391 bvc_const_hobj.m.hash = (hobj_hash_t) hash_bvc_const_hobj;
1392 bvc_const_hobj.m.eq = (hobj_eq_t) eq_bvc_const_hobj;
1393 bvc_const_hobj.m.build = (hobj_build_t) build_bvc_const_hobj;
1394 bvc_const_hobj.dag = dag;
1395 bvc_const_hobj.c = a;
1396 bvc_const_hobj.bitsize = bitsize;
1397 return int_htbl_get_obj(&dag->htbl, &bvc_const_hobj.m);
1398 }
1399
bvc_dag_get_offset64(bvc_dag_t * dag,uint64_t a,node_occ_t n,uint32_t bitsize)1400 static bvnode_t bvc_dag_get_offset64(bvc_dag_t *dag, uint64_t a, node_occ_t n, uint32_t bitsize) {
1401 bvc64_hobj_t bvc_offset64_hobj;
1402 bvc_offset64_hobj.m.hash = (hobj_hash_t) hash_bvc_offset64_hobj;
1403 bvc_offset64_hobj.m.eq = (hobj_eq_t) eq_bvc_offset64_hobj;
1404 bvc_offset64_hobj.m.build = (hobj_build_t) build_bvc_offset64_hobj;
1405 bvc_offset64_hobj.dag = dag;
1406 bvc_offset64_hobj.c = a;
1407 bvc_offset64_hobj.bitsize = bitsize;
1408 bvc_offset64_hobj.nocc = n;
1409 return int_htbl_get_obj(&dag->htbl, &bvc_offset64_hobj.m);
1410 }
1411
bvc_dag_get_offset(bvc_dag_t * dag,uint32_t * a,node_occ_t n,uint32_t bitsize)1412 static bvnode_t bvc_dag_get_offset(bvc_dag_t *dag, uint32_t *a, node_occ_t n, uint32_t bitsize) {
1413 bvc_hobj_t bvc_offset_hobj;
1414 bvc_offset_hobj.m.hash = (hobj_hash_t) hash_bvc_offset_hobj;
1415 bvc_offset_hobj.m.eq = (hobj_eq_t) eq_bvc_offset_hobj;
1416 bvc_offset_hobj.m.build = (hobj_build_t) build_bvc_offset_hobj;
1417 bvc_offset_hobj.dag = dag;
1418 bvc_offset_hobj.c = a;
1419 bvc_offset_hobj.bitsize = bitsize;
1420 bvc_offset_hobj.nocc = n;
1421 return int_htbl_get_obj(&dag->htbl, &bvc_offset_hobj.m);
1422 }
1423
bvc_dag_get_mono64(bvc_dag_t * dag,uint64_t a,node_occ_t n,uint32_t bitsize)1424 static bvnode_t bvc_dag_get_mono64(bvc_dag_t *dag, uint64_t a, node_occ_t n, uint32_t bitsize) {
1425 bvc64_hobj_t bvc_mono64_hobj;
1426 bvc_mono64_hobj.m.hash = (hobj_hash_t) hash_bvc_mono64_hobj;
1427 bvc_mono64_hobj.m.eq = (hobj_eq_t) eq_bvc_mono64_hobj;
1428 bvc_mono64_hobj.m.build = (hobj_build_t) build_bvc_mono64_hobj;
1429 bvc_mono64_hobj.dag = dag;
1430 bvc_mono64_hobj.c = a;
1431 bvc_mono64_hobj.bitsize = bitsize;
1432 bvc_mono64_hobj.nocc = n;
1433 return int_htbl_get_obj(&dag->htbl, &bvc_mono64_hobj.m);
1434 }
1435
bvc_dag_get_mono(bvc_dag_t * dag,uint32_t * a,node_occ_t n,uint32_t bitsize)1436 static bvnode_t bvc_dag_get_mono(bvc_dag_t *dag, uint32_t *a, node_occ_t n, uint32_t bitsize) {
1437 bvc_hobj_t bvc_mono_hobj;
1438 bvc_mono_hobj .m.hash = (hobj_hash_t) hash_bvc_mono_hobj;
1439 bvc_mono_hobj.m.eq = (hobj_eq_t) eq_bvc_mono_hobj;
1440 bvc_mono_hobj.m.build = (hobj_build_t) build_bvc_mono_hobj;
1441 bvc_mono_hobj.dag = dag;
1442 bvc_mono_hobj.c = a;
1443 bvc_mono_hobj.bitsize = bitsize;
1444 bvc_mono_hobj.nocc = n;
1445 return int_htbl_get_obj(&dag->htbl, &bvc_mono_hobj.m);
1446 }
1447
1448 // note: a must be sorted
bvc_dag_get_prod(bvc_dag_t * dag,varexp_t * a,uint32_t len,uint32_t bitsize)1449 static bvnode_t bvc_dag_get_prod(bvc_dag_t *dag, varexp_t *a, uint32_t len, uint32_t bitsize) {
1450 bvc_prod_hobj_t bvc_prod_hobj;
1451 bvc_prod_hobj.m.hash = (hobj_hash_t) hash_bvc_prod_hobj;
1452 bvc_prod_hobj.m.eq = (hobj_eq_t) eq_bvc_prod_hobj;
1453 bvc_prod_hobj.m.build = (hobj_build_t) build_bvc_prod_hobj;
1454 bvc_prod_hobj.dag = dag;
1455 bvc_prod_hobj.pp = a;
1456 bvc_prod_hobj.bitsize = bitsize;
1457 bvc_prod_hobj.len = len;
1458 return int_htbl_get_obj(&dag->htbl, &bvc_prod_hobj.m);
1459 }
1460
1461 // a must be sorted
bvc_dag_get_sum(bvc_dag_t * dag,node_occ_t * a,uint32_t len,uint32_t bitsize)1462 static bvnode_t bvc_dag_get_sum(bvc_dag_t *dag, node_occ_t *a, uint32_t len, uint32_t bitsize) {
1463 bvc_sum_hobj_t bvc_sum_hobj;
1464 bvc_sum_hobj.m.hash = (hobj_hash_t) hash_bvc_sum_hobj;
1465 bvc_sum_hobj.m.eq = (hobj_eq_t) eq_bvc_sum_hobj;
1466 bvc_sum_hobj.m.build = (hobj_build_t) build_bvc_sum_hobj;
1467 bvc_sum_hobj.dag = dag;
1468 bvc_sum_hobj.noccs = a;
1469 bvc_sum_hobj.bitsize = bitsize;
1470 bvc_sum_hobj.len = len;
1471 return int_htbl_get_obj(&dag->htbl, &bvc_sum_hobj.m);
1472 }
1473
1474
1475
1476
1477
1478
1479 /*
1480 * NORMALIZATION + NODE CONSTRUCTION
1481 */
1482
1483 /*
1484 * Store mapping [x --> n] in dag->vmap
1485 * - x must be positive
1486 * - n must be a valid node_occurrence in dag
1487 */
bvc_dag_map_var(bvc_dag_t * dag,int32_t x,node_occ_t n)1488 void bvc_dag_map_var(bvc_dag_t *dag, int32_t x, node_occ_t n) {
1489 int_hmap_pair_t *p;
1490
1491 assert(x > 0 && !bvc_dag_var_is_present(dag, x));
1492 int_bvset_add(&dag->vset, x);
1493 p = int_hmap_get(&dag->vmap, x);
1494 assert(p->val == -1);
1495 p->val = n;
1496 }
1497
1498
1499
1500 /*
1501 * Leaf node attached to variable x
1502 * - x must be positive
1503 */
bvc_dag_leaf(bvc_dag_t * dag,int32_t x,uint32_t bitsize)1504 node_occ_t bvc_dag_leaf(bvc_dag_t *dag, int32_t x, uint32_t bitsize) {
1505 assert(x > 0);
1506 return bvp(bvc_dag_get_leaf(dag, x, bitsize));
1507 }
1508
1509
1510 /*
1511 * Check whether node n was flipped during processing
1512 */
bvc_dag_nocc_has_flipped(bvc_dag_t * dag,node_occ_t n)1513 bool bvc_dag_nocc_has_flipped(bvc_dag_t *dag, node_occ_t n) {
1514 return node_has_flipped(dag, node_of_occ(n));
1515 }
1516
1517
1518
1519 /*
1520 * Zero node
1521 */
bvc_dag_zero(bvc_dag_t * dag,uint32_t bitsize)1522 static inline node_occ_t bvc_dag_zero(bvc_dag_t *dag, uint32_t bitsize) {
1523 assert(1 <= bitsize);
1524 return bvp(bvc_dag_get_zero(dag, bitsize));
1525 }
1526
1527
1528 /*
1529 * Non-zero constant nodes
1530 */
bvc_dag_const64(bvc_dag_t * dag,uint64_t a,uint32_t bitsize)1531 static inline node_occ_t bvc_dag_const64(bvc_dag_t *dag, uint64_t a, uint32_t bitsize) {
1532 return bvp(bvc_dag_get_const64(dag, a, bitsize));
1533 }
1534
bvc_dag_const(bvc_dag_t * dag,uint32_t * a,uint32_t bitsize)1535 static inline node_occ_t bvc_dag_const(bvc_dag_t *dag, uint32_t *a, uint32_t bitsize) {
1536 return bvp(bvc_dag_get_const(dag, a, bitsize));
1537 }
1538
1539
1540 /*
1541 * Get a node mapped to x
1542 * - if there's none, create the node [leaf x] and return it
1543 */
bvc_dag_get_nocc_of_var(bvc_dag_t * dag,int32_t x,uint32_t bitsize)1544 node_occ_t bvc_dag_get_nocc_of_var(bvc_dag_t *dag, int32_t x, uint32_t bitsize) {
1545 node_occ_t n;
1546
1547 assert(x > 0);
1548
1549 if (bvc_dag_var_is_present(dag, x)) {
1550 return bvc_dag_nocc_of_var(dag, x);
1551 } else {
1552 /*
1553 * NOTE: we don't want to add the map [x --> n] in vmap
1554 * - because of possible circularities, x may be mapped
1555 * later to another node.
1556 */
1557 n = bvc_dag_leaf(dag, x, bitsize);
1558 return n;
1559 }
1560 }
1561
1562
1563
1564 /*
1565 * Construct an offset node q
1566 * - a must be normalized modulo 2^bitsize (and not be 0)
1567 */
bvc_dag_offset64(bvc_dag_t * dag,uint64_t a,node_occ_t n,uint32_t bitsize)1568 node_occ_t bvc_dag_offset64(bvc_dag_t *dag, uint64_t a, node_occ_t n, uint32_t bitsize) {
1569 assert(1 <= bitsize && bitsize <= 64 && a == norm64(a, bitsize) && a != 0);
1570 return bvp(bvc_dag_get_offset64(dag, a, n, bitsize));
1571 }
1572
bvc_dag_offset(bvc_dag_t * dag,uint32_t * a,node_occ_t n,uint32_t bitsize)1573 node_occ_t bvc_dag_offset(bvc_dag_t *dag, uint32_t *a, node_occ_t n, uint32_t bitsize) {
1574 assert(64 < bitsize && bvconst_is_normalized(a, bitsize));
1575 return bvp(bvc_dag_get_offset(dag, a, n, bitsize));
1576 }
1577
1578
1579
1580
1581 /*
1582 * Construct a monomial node q
1583 * - a must be normalized modulo 2^bitsize and must not be 0
1584 *
1585 * Depending on a and n, this gets turned into one of the following nodes:
1586 * - if a is +1 --> n
1587 * - if a is -1 --> -n
1588 * - otherwise,
1589 * 1) force n to positive sign
1590 * 2) depending on the number of '1' bits in a and -a,
1591 * build either [mono a n] or [mono (-a) n]
1592 *
1593 * Heuristics:
1594 * - the number of adders required for (a * n) is equal to the number of '1'
1595 * bits in a (i.e., to popcount(a)).
1596 * - (BVMUL a n) has cost equal to popcount(a)
1597 * (BVNEG (BVMUL -a n)) has cost equal to popcount(-a) + 1 (we count
1598 * BVNEG as one more adder)
1599 *
1600 *
1601 * NOTE: there are better techniques
1602 * - could use a signed digit representation for the constant a
1603 * - if there are several monomials (a_0 x) ... (a_t x), then
1604 * there are optimizations used in digital filter circuits:
1605 *
1606 * Reference:
1607 * Dempster & McLeod, Constant integer multiplication using minimum adders,
1608 * IEE Proceedings, Circuits, Devices & Systems, vol. 141, Issue 5, pp. 407-413,
1609 * October 1994
1610 */
bvc_dag_mono64(bvc_dag_t * dag,uint64_t a,node_occ_t n,uint32_t bitsize)1611 node_occ_t bvc_dag_mono64(bvc_dag_t *dag, uint64_t a, node_occ_t n, uint32_t bitsize) {
1612 uint64_t minus_a;
1613 uint32_t sign, ka, kma;
1614 bvnode_t q;
1615
1616 assert(1 <= bitsize && bitsize <= 64 && a == norm64(a, bitsize) && a != 0);
1617
1618 if (a == 1) return n;
1619 if (a == mask64(bitsize)) return negate_occ(n);
1620
1621 sign = sign_of_occ(n);
1622 n = unsigned_occ(n);
1623
1624 /*
1625 * normalization:
1626 * - is popcount(a) < popcount(-a) then build [mono a n]
1627 * - if popcount(-a) < popcount(a) then build [mono (-a) n]
1628 * - if there's a tie, we build [mono (-a) n] if -a is positive
1629 * or [mono a n] otherwise
1630 *
1631 * Note: if a is 0b10000...00 then both a and -a are negative and equal
1632 * so the tie-breaking rule works too (we want to build [mono a n]
1633 * in this case).
1634 */
1635 minus_a = norm64(-a, bitsize);
1636 ka = popcount64(a);
1637 kma = popcount64(minus_a);
1638 assert(1 <= ka && ka <= bitsize && 1 <= kma && kma <= bitsize);
1639
1640 if (kma < ka || (kma == ka && is_pos64(minus_a, bitsize))) {
1641 a = minus_a;
1642 sign ^= 1; // flip the sign
1643 }
1644
1645 q = bvc_dag_get_mono64(dag, a, n, bitsize);
1646
1647 return (q << 1) | sign;
1648 }
1649
bvc_dag_mono(bvc_dag_t * dag,uint32_t * a,node_occ_t n,uint32_t bitsize)1650 node_occ_t bvc_dag_mono(bvc_dag_t *dag, uint32_t *a, node_occ_t n, uint32_t bitsize) {
1651 uint32_t *minus_a;
1652 uint32_t w, sign, ka, kma;
1653 bvnode_t q;
1654
1655 w = (bitsize + 31) >> 5; // number of words in a
1656
1657 assert(64 < bitsize && bvconst_is_normalized(a, bitsize) && !bvconst_is_zero(a, w));
1658
1659 if (bvconst_is_one(a, w)) return n;
1660 if (bvconst_is_minus_one(a, bitsize)) return negate_occ(n);
1661
1662 sign = sign_of_occ(n);
1663 n = unsigned_occ(n);
1664
1665 /*
1666 * Normalization: we store -a in dag->aux
1667 */
1668 bvconstant_copy(&dag->aux, bitsize, a);
1669 minus_a = dag->aux.data;
1670 bvconst_negate(minus_a, w);
1671 bvconst_normalize(minus_a, bitsize);
1672
1673 ka = bvconst_popcount(a, w);
1674 kma = bvconst_popcount(minus_a, w);
1675 assert(1 <= ka && ka <= bitsize && 1 <= kma && kma <= bitsize);
1676
1677 if (kma < ka || (kma == ka && !bvconst_tst_bit(minus_a, bitsize - 1))) {
1678 a = minus_a;
1679 sign ^= 1; // flip the sign
1680 }
1681
1682 q = bvc_dag_get_mono(dag, a, n, bitsize);
1683 return (q << 1) | sign;
1684 }
1685
1686
1687 /*
1688 * Variant of bvc_dag_mono when the coefficient c is small (stored as int32_t)
1689 */
bvc_dag_simple_mono(bvc_dag_t * dag,int32_t c,node_occ_t n,uint32_t bitsize)1690 static node_occ_t bvc_dag_simple_mono(bvc_dag_t *dag, int32_t c, node_occ_t n, uint32_t bitsize) {
1691 uint64_t d;
1692 uint32_t sign;
1693 bvnode_t q;
1694
1695 assert(c != 0 && bitsize > 64);
1696
1697 if (c == 1) return n;
1698 if (c == -1) return negate_occ(n);
1699
1700 sign = sign_of_occ(n);
1701 n = unsigned_occ(n);
1702
1703 d = (uint64_t) c;
1704 if (c < 0) {
1705 d = -d;
1706 sign ^= 1;
1707 }
1708
1709 // store the coeff in dag->aux
1710 bvconstant_copy64(&dag->aux, bitsize, d);
1711 q = bvc_dag_get_mono(dag, dag->aux.data, n, bitsize);
1712 return (q << 1) | sign;
1713 }
1714
1715
1716 /*
1717 * Construct a sum node q
1718 * - a = array of n node occurrences
1719 * - n must be positive
1720 *
1721 * If n == 1, this returns a[0].
1722 * Otherwise, a is sorted and a node q := [sum a[0] ... a[n-1]] is created
1723 */
bvc_dag_sum(bvc_dag_t * dag,node_occ_t * a,uint32_t n,uint32_t bitsize)1724 node_occ_t bvc_dag_sum(bvc_dag_t *dag, node_occ_t *a, uint32_t n, uint32_t bitsize) {
1725 assert(n > 0);
1726
1727 if (n == 1) return a[0];
1728
1729 int_array_sort(a, n);
1730 return bvp(bvc_dag_get_sum(dag, a, n, bitsize));
1731 }
1732
1733
1734 /*
1735 * Binary sum: n1 n2
1736 */
bvc_dag_sum2(bvc_dag_t * dag,node_occ_t n1,node_occ_t n2,uint32_t bitsize)1737 static node_occ_t bvc_dag_sum2(bvc_dag_t *dag, node_occ_t n1, node_occ_t n2, uint32_t bitsize) {
1738 node_occ_t a[2];
1739
1740 assert(!bvc_dag_occ_is_zero(dag, n1) && !bvc_dag_occ_is_zero(dag, n2));
1741
1742 if (n1 < n2) {
1743 a[0] = n1;
1744 a[1] = n2;
1745 } else {
1746 a[0] = n2;
1747 a[1] = n1;
1748 }
1749
1750 return bvp(bvc_dag_get_sum(dag, a, 2, bitsize));
1751 }
1752
1753
1754 /*
1755 * Return the sign of (n ^ d)
1756 * - the result is 1 if n is of the form bvn(x) and d is odd
1757 * (i.e., the product has negative sign)
1758 * - the result is 0 otherwise (positive sign)
1759 */
sign_of_varexp(node_occ_t n,uint32_t exp)1760 static uint32_t sign_of_varexp(node_occ_t n, uint32_t exp) {
1761 // return 1 if the low-order bits of n and exp are both 1
1762 return n & exp & 1;
1763 }
1764
1765
1766 /*
1767 * For debugging: check that all nodes in prod[i].var have positive sign.
1768 */
1769 #ifndef NDEBUG
good_pprod(varexp_t * prod,uint32_t n)1770 static bool good_pprod(varexp_t *prod, uint32_t n) {
1771 uint32_t i;
1772
1773 for (i=0; i<n; i++) {
1774 if (sign_of_occ(prod[i].var) == 1) {
1775 return false;
1776 }
1777 }
1778
1779 return true;
1780 }
1781 #endif
1782
1783 /*
1784 * Check that sign is correct for the product a[i]^d_i
1785 * where d_i is p->prod[i].exp
1786 */
1787 #ifndef NDEBUG
is_odd(uint32_t k)1788 static bool is_odd(uint32_t k) {
1789 return (k & 1) == 1;
1790 }
1791
is_neg_node_occ(node_occ_t n)1792 static bool is_neg_node_occ(node_occ_t n) {
1793 return sign_of_occ(n) == 1;
1794 }
1795
good_sign(uint32_t sign,pprod_t * p,node_occ_t * a)1796 static bool good_sign(uint32_t sign, pprod_t *p, node_occ_t *a) {
1797 uint32_t i, n;
1798 bool is_pos;
1799
1800 is_pos = true;
1801 n = p->len;
1802 for (i=0; i<n; i++) {
1803 if (is_odd(p->prod[i].exp) && is_neg_node_occ(a[i])) {
1804 // odd exponent and negative node occurrence: flip the sign
1805 is_pos = !is_pos;
1806 }
1807 }
1808
1809 return (is_pos && sign == 0) || (!is_pos && sign == 1);
1810 }
1811 #endif
1812
1813
1814 /*
1815 * Check whether one of a[0 ... n-1] is zero and return it
1816 * - return -1 otherwise
1817 */
bvc_dag_has_zero(bvc_dag_t * dag,node_occ_t * a,uint32_t n)1818 static node_occ_t bvc_dag_has_zero(bvc_dag_t *dag, node_occ_t *a, uint32_t n) {
1819 uint32_t i;
1820
1821 for (i=0; i<n; i++) {
1822 if (bvc_dag_occ_is_zero(dag, a[i])) {
1823 return a[i];
1824 }
1825 }
1826 return -1;
1827 }
1828
1829
1830 /*
1831 * Construct a product node q
1832 * - q is defined by the exponents in power product p and the
1833 * nodes in array a: if p is x_1^d_1 ... x_k^d_k
1834 * then a must have k elements a[0] ... a[k-1]
1835 * and q is [prod a[0]^d_1 ... a[k-1]^d_k]
1836 */
bvc_dag_pprod(bvc_dag_t * dag,pprod_t * p,node_occ_t * a,uint32_t bitsize)1837 node_occ_t bvc_dag_pprod(bvc_dag_t *dag, pprod_t *p, node_occ_t *a, uint32_t bitsize) {
1838 pp_buffer_t *buffer;
1839 uint32_t i, n, e, sign;
1840 node_occ_t r;
1841
1842 n = p->len;
1843
1844 r = bvc_dag_has_zero(dag, a, n);
1845 if (r < 0) {
1846 /*
1847 * Not a zero product: build the power product in dag->pp_aux keep
1848 * track of signs
1849 */
1850 sign = 0;
1851 buffer = &dag->pp_aux;
1852 pp_buffer_reset(buffer);
1853 for (i=0; i<n; i++) {
1854 /*
1855 * If a[i]^exp is negative, flip sign. Otherwise keep sign unchanged
1856 * Remove a[i]'s sign in the product
1857 */
1858 e = p->prod[i].exp;
1859 sign ^= sign_of_varexp(a[i], e);
1860 pp_buffer_mul_varexp(buffer, unsigned_occ(a[i]), p->prod[i].exp);
1861 }
1862 pp_buffer_normalize(buffer);
1863
1864 assert(good_sign(sign, p, a) && good_pprod(buffer->prod, buffer->len));
1865
1866 r = bvp(bvc_dag_get_prod(dag, buffer->prod, buffer->len, bitsize)) | sign;
1867 }
1868
1869 return r;
1870 }
1871
1872
1873
1874 /*
1875 * Binary product: n1 n2
1876 * - both must be non-zero
1877 */
bvc_dag_pprod2(bvc_dag_t * dag,node_occ_t n1,node_occ_t n2,uint32_t bitsize)1878 static node_occ_t bvc_dag_pprod2(bvc_dag_t *dag, node_occ_t n1, node_occ_t n2, uint32_t bitsize) {
1879 pp_buffer_t *buffer;
1880
1881 assert(!bvc_dag_occ_is_zero(dag, n1) && !bvc_dag_occ_is_zero(dag, n2));
1882
1883 buffer = &dag->pp_aux;
1884 pp_buffer_reset(buffer);
1885 pp_buffer_set_var(buffer, n1);
1886 pp_buffer_mul_var(buffer, n2);
1887 pp_buffer_normalize(buffer);
1888
1889 return bvp(bvc_dag_get_prod(dag, buffer->prod, buffer->len, bitsize));
1890 }
1891
1892
1893
1894 /*
1895 * NORMALIZATION OF SUMS
1896 */
1897
1898 /*
1899 * Check whether n1 and n2 are occurrences of the same node
1900 * - i.e., all bits are the same except possible bit 0
1901 */
same_node(node_occ_t n1,node_occ_t n2)1902 static inline bool same_node(node_occ_t n1, node_occ_t n2) {
1903 return ((n1 ^ n2) >> 1) == 0;
1904 }
1905
1906
1907 /*
1908 * Check whether array a[0 ... n-1] contains duplicates
1909 * - a must be sorted in increasing order
1910 */
bvc_array_has_duplicates(const node_occ_t * a,uint32_t n)1911 static bool bvc_array_has_duplicates(const node_occ_t *a, uint32_t n) {
1912 uint32_t i;
1913
1914 for (i=1; i<n; i++) {
1915 assert(a[i-1] <= a[i]);
1916 if (same_node(a[i-1], a[i])) return true;
1917 }
1918
1919 return false;
1920 }
1921
1922
1923 /*
1924 * Sum after normalization: array a is sorted & has no duplicates
1925 */
bvc_dag_normal_sum(bvc_dag_t * dag,node_occ_t * a,uint32_t n,uint32_t bitsize)1926 static node_occ_t bvc_dag_normal_sum(bvc_dag_t *dag, node_occ_t *a, uint32_t n, uint32_t bitsize) {
1927 assert(n > 0 && !bvc_array_has_duplicates(a, n));
1928
1929 return n == 1 ? a[0] : bvp(bvc_dag_get_sum(dag, a, n, bitsize));
1930 }
1931
1932
1933 /*
1934 * Normalize sum vector v:
1935 * - each element of v is a node occurrence
1936 * - if v contains duplicate node, then we replace them by monomials
1937 */
bvc_normalize_sum64(bvc_dag_t * dag,ivector_t * v,uint32_t bitsize)1938 static void bvc_normalize_sum64(bvc_dag_t *dag, ivector_t *v, uint32_t bitsize) {
1939 uint32_t i, j, n;
1940 int32_t c;
1941 bvnode_t p, q;
1942 uint64_t a;
1943
1944 assert(1 <= bitsize && bitsize <= 64);
1945
1946 n = v->size;
1947 if (n > 1) {
1948 int_array_sort(v->data, n);
1949 if (bvc_array_has_duplicates(v->data, n)) {
1950
1951 for (;;) {
1952 assert(n == v->size && n >= 2);
1953
1954 j = 0;
1955 p = node_of_occ(v->data[0]);
1956 c = coeff_of_occ(v->data[0]);
1957 for (i=1; i<n; i++) {
1958 q = node_of_occ(v->data[i]);
1959 if (p == q) {
1960 // repeat node
1961 c += coeff_of_occ(v->data[i]);
1962 } else {
1963 // new node for monomial c*p
1964 a = norm64((uint64_t) c, bitsize);
1965 if (a != 0) {
1966 v->data[j] = bvc_dag_mono64(dag, a, bvp(p), bitsize);
1967 j ++;
1968 }
1969 // current node + its coefficient
1970 p = q;
1971 c = coeff_of_occ(v->data[i]);
1972 }
1973 }
1974 // last node
1975 a = norm64((uint64_t) c, bitsize);
1976 if (a != 0) {
1977 v->data[j] = bvc_dag_mono64(dag, a, bvp(p), bitsize);
1978 j ++;
1979 }
1980
1981 v->size = j;
1982
1983 // if j == n, v didn't change so we're done
1984 // if j == 0 or 1, v can't have duplicates
1985 if (j == n || j < 2) break;
1986
1987 n = j;
1988 int_array_sort(v->data, n);
1989 }
1990 }
1991 }
1992 }
1993
1994
1995 /*
1996 * Same thing but coefficients have more than 64 bits
1997 */
bvc_normalize_sum(bvc_dag_t * dag,ivector_t * v,uint32_t bitsize)1998 static void bvc_normalize_sum(bvc_dag_t *dag, ivector_t *v, uint32_t bitsize) {
1999 uint32_t i, j, n;
2000 int32_t c;
2001 bvnode_t p, q;
2002
2003 assert(bitsize > 64);
2004
2005 n = v->size;
2006 if (n > 1) {
2007 int_array_sort(v->data, n);
2008 if (bvc_array_has_duplicates(v->data, n)) {
2009
2010 for (;;) {
2011 assert(n == v->size && n >= 2);
2012
2013 j = 0;
2014 p = node_of_occ(v->data[0]);
2015 c = coeff_of_occ(v->data[0]);
2016 for (i=1; i<n; i++) {
2017 q = node_of_occ(v->data[i]);
2018 if (p == q) {
2019 // repeat node
2020 c += coeff_of_occ(v->data[i]);
2021 } else {
2022 // new node for monomial c*p
2023 if (c != 0) {
2024 v->data[j] = bvc_dag_simple_mono(dag, c, bvp(p), bitsize);
2025 j ++;
2026 }
2027 // current node + its coefficient
2028 p = q;
2029 c = coeff_of_occ(v->data[i]);
2030 }
2031 }
2032 // last node
2033 if (c != 0) {
2034 v->data[j] = bvc_dag_simple_mono(dag, c, bvp(p), bitsize);
2035 j ++;
2036 }
2037
2038 v->size = j;
2039
2040 // if j == n, v didn't change so we're done
2041 // if j <= 0 or 1, v can't have duplicates
2042 if (j == n || j < 2) break;
2043
2044 n = j;
2045 int_array_sort(v->data, n);
2046 }
2047 }
2048 }
2049 }
2050
2051
2052 /*
2053 * Convert buffer p to a DAG.
2054 * - p contains a polynomial a_0 x_0 + ... a_n x_n
2055 * - each x_i must be node index (can be positive or negative)
2056 * - there mustn't be duplicates among x_0 ... x_n
2057 * all node_of_occ(x_i) must be distinct.
2058 */
bvc_dag_of_buffer64(bvc_dag_t * dag,bvpoly_buffer_t * buffer)2059 static node_occ_t bvc_dag_of_buffer64(bvc_dag_t *dag, bvpoly_buffer_t *buffer) {
2060 ivector_t *v;
2061 uint32_t i, n, bitsize;
2062 node_occ_t r;
2063
2064 n = bvpoly_buffer_num_terms(buffer);
2065 bitsize = bvpoly_buffer_bitsize(buffer);
2066 assert(bitsize <= 64);
2067
2068 if (n == 0) {
2069 // empty sum
2070 r = bvc_dag_zero(dag, bitsize);
2071 } else if (n == 1 && bvpoly_buffer_var(buffer, 0) == const_idx) {
2072 // constant
2073 r = bvc_dag_const64(dag, bvpoly_buffer_coeff64(buffer, 0), bitsize);
2074 } else {
2075 i = 0;
2076 if (bvpoly_buffer_var(buffer, 0) == const_idx) {
2077 // skip the constant
2078 i = 1;
2079 }
2080
2081 // build the monomials and store the corresponding node occs in v
2082 v = &dag->buffer;
2083 assert(v->size == 0);
2084
2085 while (i < n) {
2086 r = bvc_dag_mono64(dag, bvpoly_buffer_coeff64(buffer, i), bvpoly_buffer_var(buffer, i), bitsize);
2087 ivector_push(v, r);
2088 i ++;
2089 }
2090
2091 // v may contain duplicate nodes
2092 bvc_normalize_sum64(dag, v, bitsize);
2093
2094 if (v->size == 0) {
2095 // the sum reduced to zero
2096 if (bvpoly_buffer_var(buffer, 0) == const_idx) {
2097 r = bvc_dag_const64(dag, bvpoly_buffer_coeff64(buffer, 0), bitsize);
2098 } else {
2099 r = bvc_dag_zero(dag, bitsize);
2100 }
2101
2102 } else {
2103 // build the sum
2104 r = bvc_dag_normal_sum(dag, v->data, v->size, bitsize);
2105 ivector_reset(v);
2106
2107 // add the constant if any
2108 if (bvpoly_buffer_var(buffer, 0) == const_idx) {
2109 r = bvc_dag_offset64(dag, bvpoly_buffer_coeff64(buffer, 0), r, bitsize);
2110 }
2111 }
2112 }
2113
2114 return r;
2115 }
2116
2117
2118 // same thing for a polynomial with large coefficients
bvc_dag_of_buffer(bvc_dag_t * dag,bvpoly_buffer_t * buffer)2119 static node_occ_t bvc_dag_of_buffer(bvc_dag_t *dag, bvpoly_buffer_t *buffer) {
2120 ivector_t *v;
2121 uint32_t i, n, bitsize;
2122 node_occ_t r;
2123
2124 n = bvpoly_buffer_num_terms(buffer);
2125 bitsize = bvpoly_buffer_bitsize(buffer);
2126 assert(bitsize > 64);
2127
2128 if (n == 0) {
2129 r = bvc_dag_zero(dag, bitsize);
2130 } else if (n == 1 && bvpoly_buffer_var(buffer, 0) == const_idx) {
2131 r = bvc_dag_const(dag, bvpoly_buffer_coeff(buffer, 0), bitsize);
2132 } else {
2133 i = 0;
2134 if (bvpoly_buffer_var(buffer, 0) == const_idx) {
2135 // skip the constant
2136 i = 1;
2137 }
2138
2139 // build the monomials and store the corresponding node occs in v
2140 v = &dag->buffer;
2141 assert(v->size == 0);
2142
2143 while (i < n) {
2144 r = bvc_dag_mono(dag, bvpoly_buffer_coeff(buffer, i), bvpoly_buffer_var(buffer, i), bitsize);
2145 ivector_push(v, r);
2146 i ++;
2147 }
2148
2149 // v may contain duplicate nodes
2150 bvc_normalize_sum(dag, v, bitsize);
2151
2152 if (v->size == 0) {
2153 // the sum reduced to zero
2154 if (bvpoly_buffer_var(buffer, 0) == const_idx) {
2155 r = bvc_dag_const(dag, bvpoly_buffer_coeff(buffer, 0), bitsize);
2156 } else {
2157 r = bvc_dag_zero(dag, bitsize);
2158 }
2159
2160 } else {
2161 // build the sum
2162 r = bvc_dag_sum(dag, v->data, v->size, bitsize);
2163 ivector_reset(v);
2164
2165 // add the constant if any
2166 if (bvpoly_buffer_var(buffer, 0) == const_idx) {
2167 r = bvc_dag_offset(dag, bvpoly_buffer_coeff(buffer, 0), r, bitsize);
2168 }
2169 }
2170 }
2171
2172 return r;
2173 }
2174
2175
2176 /*
2177 * Add a * node to buffer
2178 */
bvpoly_buffer_add64(bvc_dag_t * dag,bvpoly_buffer_t * buffer,uint64_t a,node_occ_t n)2179 static void bvpoly_buffer_add64(bvc_dag_t *dag, bvpoly_buffer_t *buffer, uint64_t a, node_occ_t n) {
2180 bvc_constant_t *d;
2181 bvnode_t k;
2182
2183 if (bvc_dag_occ_is_zero(dag, n)) {
2184 return;
2185 }
2186
2187 if (bvc_dag_occ_is_constant(dag, n)) {
2188 k = node_of_occ(n);
2189 d = bvc_dag_node_constant(dag, k);
2190 assert(d->header.bitsize <= 64);
2191
2192 if (sign_of_occ(n) == 1) {
2193 bvpoly_buffer_submul_const64(buffer, d->value.c, a);
2194 } else {
2195 bvpoly_buffer_addmul_const64(buffer, d->value.c, a);
2196 }
2197 return;
2198 }
2199
2200 if (sign_of_occ(n) == 1) {
2201 bvpoly_buffer_sub_mono64(buffer, unsigned_occ(n), a);
2202 } else {
2203 bvpoly_buffer_add_mono64(buffer, n, a);
2204 }
2205 }
2206
bvpoly_buffer_add(bvc_dag_t * dag,bvpoly_buffer_t * buffer,uint32_t * a,node_occ_t n)2207 static void bvpoly_buffer_add(bvc_dag_t *dag, bvpoly_buffer_t *buffer, uint32_t *a, node_occ_t n) {
2208 bvc_constant_t *d;
2209 bvnode_t k;
2210
2211 if (bvc_dag_occ_is_zero(dag, n)) {
2212 return;
2213 }
2214
2215 if (bvc_dag_occ_is_constant(dag, n)) {
2216 k = node_of_occ(n);
2217 d = bvc_dag_node_constant(dag, k);
2218 assert(d->header.bitsize <= 64);
2219
2220 if (sign_of_occ(n) == 1) {
2221 bvpoly_buffer_submul_constant(buffer, d->value.w, a);
2222 } else {
2223 bvpoly_buffer_addmul_constant(buffer, d->value.w, a);
2224 }
2225 return;
2226 }
2227
2228 if (sign_of_occ(n) == 1) {
2229 bvpoly_buffer_sub_monomial(buffer, unsigned_occ(n), a);
2230 } else {
2231 bvpoly_buffer_add_monomial(buffer, n, a);
2232 }
2233 }
2234
2235
2236
2237
2238
2239 /*
2240 * Convert a polynomial p to a DAG node q and return q
2241 * - q is defined by the coefficients in p and the node indices
2242 * in array a: if p is b_0 x_0 + b_1 x_1 + ... + b_k x_k
2243 * then a must have k+1 elements a[0] ... a[k]
2244 * and q is built for (b_0 * a[0] + b_1 a[1] + ... + b_k a[k])
2245 *
2246 * - if x_0 is const_idx, then a[0] is ignored and
2247 * q is built for (b_0 + b_1 a[1] + ... + b_k a[k]).
2248 *
2249 * The DAG for p = (b0 + b_1 a[1] + .... + b_k a[k]) is
2250 * [offset b0 [sum [mono b_1 a[1]] ... [mono b_k a[k]]]].
2251 *
2252 * Special cases: if the sum cancels returns a zero_node. Also
2253 * check whether the sum is a constant.
2254 */
bvc_dag_poly64(bvc_dag_t * dag,bvpoly64_t * p,node_occ_t * a)2255 node_occ_t bvc_dag_poly64(bvc_dag_t *dag, bvpoly64_t *p, node_occ_t *a) {
2256 bvpoly_buffer_t *buffer;
2257 uint32_t i, n, bitsize;
2258
2259 n = p->nterms;
2260 bitsize = p->bitsize;
2261 assert(bitsize <= 64);
2262
2263 buffer = &dag->poly_buffer;
2264 reset_bvpoly_buffer(buffer, bitsize);
2265 i = 0;
2266 if (n > 0 && p->mono[0].var == const_idx) {
2267 // constant term
2268 bvpoly_buffer_add_const64(buffer, p->mono[0].coeff);
2269 i ++;
2270 }
2271 while (i < n) {
2272 bvpoly_buffer_add64(dag, buffer, p->mono[i].coeff, a[i]);
2273 i ++;
2274 }
2275 normalize_bvpoly_buffer(buffer);
2276
2277 return bvc_dag_of_buffer64(dag, buffer);
2278 }
2279
bvc_dag_poly(bvc_dag_t * dag,bvpoly_t * p,node_occ_t * a)2280 node_occ_t bvc_dag_poly(bvc_dag_t *dag, bvpoly_t *p, node_occ_t *a) {
2281 bvpoly_buffer_t *buffer;
2282 uint32_t i, n, bitsize;
2283
2284
2285 n = p->nterms;
2286 bitsize = p->bitsize;
2287 assert(bitsize > 64);
2288
2289 buffer = &dag->poly_buffer;
2290 reset_bvpoly_buffer(buffer, bitsize);
2291 i = 0;
2292 if (n > 0 && p->mono[0].var == const_idx) {
2293 bvpoly_buffer_add_constant(buffer, p->mono[0].coeff);
2294 i ++;
2295 }
2296 while (i < n) {
2297 bvpoly_buffer_add(dag, buffer, p->mono[i].coeff, a[i]);
2298 i ++;
2299 }
2300 normalize_bvpoly_buffer(buffer);
2301
2302 return bvc_dag_of_buffer(dag, buffer);
2303 }
2304
2305
2306 /*
2307 * Same thing but p is stored in buffer b
2308 */
bvc_dag_poly_buffer(bvc_dag_t * dag,bvpoly_buffer_t * b,node_occ_t * a)2309 node_occ_t bvc_dag_poly_buffer(bvc_dag_t *dag, bvpoly_buffer_t *b, node_occ_t *a) {
2310 bvpoly_buffer_t *buffer;
2311 uint32_t nbits, i, n;
2312 node_occ_t r;
2313
2314 n = bvpoly_buffer_num_terms(b);
2315 nbits = bvpoly_buffer_bitsize(b);
2316
2317 buffer = &dag->poly_buffer;
2318 reset_bvpoly_buffer(buffer, nbits);
2319 if (nbits <= 64) {
2320 i = 0;
2321 if (n > 0 && bvpoly_buffer_var(b, 0) == const_idx) {
2322 bvpoly_buffer_add_const64(buffer, bvpoly_buffer_coeff64(b, 0));
2323 i ++;
2324 }
2325 while (i < n) {
2326 bvpoly_buffer_add64(dag, buffer, bvpoly_buffer_coeff64(b, i), a[i]);
2327 i ++;
2328 }
2329 normalize_bvpoly_buffer(buffer);
2330 r = bvc_dag_of_buffer64(dag, buffer);
2331
2332 } else {
2333 i = 0;
2334 if (n > 0 && bvpoly_buffer_var(b, 0) == const_idx) {
2335 bvpoly_buffer_add_constant(buffer, bvpoly_buffer_coeff(b, 0));
2336 i ++;
2337 }
2338 while (i < n) {
2339 bvpoly_buffer_add(dag, buffer, bvpoly_buffer_coeff(b, i), a[i]);
2340 i ++;
2341 }
2342 normalize_bvpoly_buffer(buffer);
2343 r = bvc_dag_of_buffer(dag, buffer);
2344 }
2345
2346 return r;
2347 }
2348
2349
2350
2351 /*
2352 * LIST LENGTHS
2353 */
bvc_num_leaves(bvc_dag_t * dag)2354 uint32_t bvc_num_leaves(bvc_dag_t *dag) {
2355 return list_length(dag->list, BVC_DAG_LEAF_LIST);
2356 }
2357
bvc_num_elem_nodes(bvc_dag_t * dag)2358 uint32_t bvc_num_elem_nodes(bvc_dag_t *dag) {
2359 return list_length(dag->list, BVC_DAG_ELEM_LIST);
2360 }
2361
bvc_num_complex_nodes(bvc_dag_t * dag)2362 uint32_t bvc_num_complex_nodes(bvc_dag_t *dag) {
2363 return list_length(dag->list, BVC_DAG_DEFAULT_LIST);
2364 }
2365
2366
2367
2368 /*
2369 * REDUCTION
2370 */
2371
2372 /*
2373 * Remove i from the use list of n.
2374 */
bvc_dag_remove_dependent(bvc_dag_t * dag,bvnode_t n,bvnode_t i)2375 static void bvc_dag_remove_dependent(bvc_dag_t *dag, bvnode_t n, bvnode_t i) {
2376 int32_t *l;
2377 uint32_t j, m;
2378
2379 assert(0 < n && n <= dag->nelems && 0 < i && i <= dag->nelems);
2380
2381 l = dag->use[n];
2382 assert(l != NULL);
2383
2384 m = iv_size(l);
2385
2386 for (j=0; j<m; j++) {
2387 if (l[j] == i) break;
2388 }
2389 j ++;
2390 assert(0 < j && j <= m);
2391 while (j < m) {
2392 l[j-1] = l[j];
2393 j ++;
2394 }
2395
2396 index_vector_shrink(l, m-1);
2397 }
2398
2399
2400 /*
2401 * Remove i from all the use lists
2402 * - d = descriptor of node i
2403 */
remove_prod_from_uses(bvc_dag_t * dag,bvnode_t i,bvc_prod_t * d)2404 static void remove_prod_from_uses(bvc_dag_t *dag, bvnode_t i, bvc_prod_t *d) {
2405 uint32_t j, m;
2406
2407 m = d->len;
2408 for (j=0; j<m; j++) {
2409 bvc_dag_remove_dependent(dag, node_of_occ(d->prod[j].var), i);
2410 }
2411 }
2412
remove_sum_from_uses(bvc_dag_t * dag,bvnode_t i,bvc_sum_t * d)2413 static void remove_sum_from_uses(bvc_dag_t *dag, bvnode_t i, bvc_sum_t *d) {
2414 uint32_t j, m;
2415
2416 m = d->len;
2417 for (j=0; j<m; j++) {
2418 bvc_dag_remove_dependent(dag, node_of_occ(d->sum[j]), i);
2419 }
2420 }
2421
remove_from_uses(bvc_dag_t * dag,bvnode_t i,bvc_header_t * d)2422 static void remove_from_uses(bvc_dag_t *dag, bvnode_t i, bvc_header_t *d) {
2423 assert(0 < i && i <= dag->nelems && dag->desc[i] == d);
2424
2425 switch (d->tag) {
2426 case BVC_LEAF:
2427 case BVC_ZERO:
2428 case BVC_CONSTANT:
2429 break;
2430
2431 case BVC_OFFSET:
2432 bvc_dag_remove_dependent(dag, node_of_occ(offset_node(d)->nocc), i);
2433 break;
2434
2435 case BVC_MONO:
2436 bvc_dag_remove_dependent(dag, node_of_occ(mono_node(d)->nocc), i);
2437 break;
2438
2439 case BVC_PROD:
2440 remove_prod_from_uses(dag, i, prod_node(d));
2441 break;
2442
2443 case BVC_SUM:
2444 remove_sum_from_uses(dag, i, sum_node(d));
2445 break;
2446
2447 case BVC_ALIAS:
2448 break;
2449 }
2450 }
2451
2452
2453 /*
2454 * Scan the dependents of a leaf node i (after i is converted to a leaf)
2455 * - all dependents that have become elementary are moved to the elem_list
2456 */
reclassify_dependents(bvc_dag_t * dag,bvnode_t i)2457 static void reclassify_dependents(bvc_dag_t *dag, bvnode_t i) {
2458 int32_t *l;
2459 uint32_t j, m;
2460 bvnode_t r;
2461
2462 l = dag->use[i];
2463 if (l != NULL) {
2464 m = iv_size(l);
2465 for (j=0; j<m; j++) {
2466 r = l[j];
2467 if (node_is_elementary(dag, r)) {
2468 bvc_dag_move_to_elementary_list(dag, r);
2469 }
2470 }
2471 }
2472 }
2473
2474
2475 /*
2476 * Convert i to a leaf node (for variable x)
2477 * - i must not be a leaf node or alias node already
2478 */
bvc_dag_convert_to_leaf(bvc_dag_t * dag,bvnode_t i,int32_t x)2479 void bvc_dag_convert_to_leaf(bvc_dag_t *dag, bvnode_t i, int32_t x) {
2480 bvc_header_t *d;
2481 bvc_leaf_t *o;
2482 uint32_t bitsize;
2483
2484 assert(0 < i && i <= dag->nelems);
2485 d = dag->desc[i];
2486 assert(d->tag != BVC_LEAF && d->tag != BVC_ALIAS);
2487 bitsize = d->bitsize;
2488 remove_from_uses(dag, i, d);
2489 free_descriptor(dag, d);
2490
2491 o = alloc_leaf(dag);
2492 o->header.tag = BVC_LEAF;
2493 o->header.bitsize = bitsize;
2494 o->map = x;
2495
2496 dag->desc[i] = &o->header;
2497
2498 bvc_dag_move_to_leaves(dag, i);
2499
2500 reclassify_dependents(dag, i);
2501 }
2502
2503
2504 /*
2505 * Convert i to an alias node for n
2506 * - i must not be a LEAF or ALIAS node already
2507 * - add i to the node_queue
2508 */
convert_to_alias(bvc_dag_t * dag,bvnode_t i,node_occ_t n)2509 static void convert_to_alias(bvc_dag_t *dag, bvnode_t i, node_occ_t n) {
2510 bvc_header_t *d;
2511 bvc_alias_t *o;
2512 uint32_t bitsize;
2513
2514 assert(0 < i && i <= dag->nelems);
2515 d = dag->desc[i];
2516 assert(d->tag != BVC_LEAF && d->tag != BVC_ALIAS);
2517 bitsize = d->bitsize;
2518 remove_from_uses(dag, i, d);
2519 free_descriptor(dag, d);
2520
2521 o = alloc_alias(dag);
2522 o->header.tag = BVC_ALIAS;
2523 o->header.bitsize = bitsize;
2524 o->alias = n;
2525
2526 dag->desc[i] = &o->header;
2527
2528 list_remove(dag->list, i); // remove i from leaf/elem/default lists
2529
2530 int_queue_push(&dag->node_queue, i); // to process dependents
2531 }
2532
2533
2534 /*
2535 * Convert node i by a zero node
2536 * - i must not be a LEAF or ALIAS node
2537 * - add i to the node_queue
2538 */
convert_to_zero(bvc_dag_t * dag,bvnode_t i)2539 static void convert_to_zero(bvc_dag_t *dag, bvnode_t i) {
2540 bvc_header_t *d;
2541 bvc_zero_t *z;
2542 uint32_t bitsize;
2543
2544 assert(0 < i && i <= dag->nelems);
2545 d = dag->desc[i];
2546 assert(d->tag != BVC_LEAF && d->tag != BVC_ALIAS);
2547 bitsize = d->bitsize;
2548 remove_from_uses(dag, i, d);
2549 free_descriptor(dag, d);
2550
2551 z = alloc_zero(dag);
2552 z->header.tag = BVC_ZERO;
2553 z->header.bitsize = bitsize;
2554
2555 dag->desc[i] = &z->header;
2556
2557 bvc_dag_move_to_elementary_list(dag, i);
2558
2559 int_queue_push(&dag->node_queue, i);
2560 }
2561
2562
2563
2564 /*
2565 * SUPPORT FOR PRODUCT REDUCTION
2566 */
2567
2568 /*
2569 * Find position where n occurs in p
2570 * - return -1 if n does not occur in p
2571 */
pprod_get_index(bvc_prod_t * p,node_occ_t n)2572 static int32_t pprod_get_index(bvc_prod_t *p, node_occ_t n) {
2573 uint32_t i, m;
2574
2575 assert(sign_of_occ(n) == 0);
2576
2577 m = p->len;
2578 for (i=0; i<m; i++) {
2579 if (p->prod[i].var == n) {
2580 return i;
2581 }
2582 }
2583
2584 return -1;
2585 }
2586
2587 #ifndef NDEBUG
2588 /*
2589 * Check that all variables in a power product denote positive nodes
2590 * and that all the exponents are positive
2591 */
pprod_is_normalized(bvc_prod_t * p)2592 static bool pprod_is_normalized(bvc_prod_t *p) {
2593 uint32_t i, n;
2594
2595 n = p->len;
2596 for (i=0; i<n; i++) {
2597 if (sign_of_occ(p->prod[i].var) != 0) return false;
2598 if (p->prod[i].exp == 0) return false;
2599 }
2600
2601 return true;
2602 }
2603 #endif
2604
2605
2606 /*
2607 * Remove all zero exponents from p and recompute the bit hash
2608 */
cleanup_prod(bvc_prod_t * p)2609 static void cleanup_prod(bvc_prod_t *p) {
2610 uint32_t i, j, n;
2611
2612 j = 0;
2613 n = p->len;
2614 p->hash = 0;
2615 for (i=0; i<n; i++) {
2616 if (p->prod[i].exp > 0) {
2617 p->prod[j] = p->prod[i];
2618 p->hash |= bit_hash_occ(p->prod[i].var);
2619 j ++;
2620 }
2621 }
2622 p->len = j;
2623 }
2624
2625
2626 /*
2627 * Construct the product p * (r ^ e) then delete p
2628 */
mk_prod_times_occ_power(bvc_dag_t * dag,bvc_prod_t * p,node_occ_t r,uint32_t e)2629 static bvc_prod_t *mk_prod_times_occ_power(bvc_dag_t *dag, bvc_prod_t *p, node_occ_t r, uint32_t e) {
2630 bvc_prod_t *tmp;
2631 uint32_t i, n;
2632
2633 n = p->len;
2634 tmp = alloc_prod(dag, n+1);
2635 tmp->header.tag = BVC_PROD;
2636 tmp->header.bitsize = p->header.bitsize;
2637 tmp->hash = p->hash;
2638 tmp->size = n+1;
2639 tmp->len = n+1;
2640
2641 for (i=0; i<n; i++) {
2642 assert(p->prod[i].var != r && p->prod[i].exp > 0);
2643 tmp->prod[i] = p->prod[i];
2644 }
2645 tmp->prod[n].var = r;
2646 tmp->prod[n].exp = e;
2647 tmp->hash |= bit_hash_occ(r);
2648
2649 free_prod(dag, p);
2650
2651 return tmp;
2652 }
2653
2654
2655
2656 /*
2657 * FLIP SIGNS TO NORMALIZE
2658 */
2659
2660 /*
2661 * Flip the sign of node i in an offset or sum node
2662 */
flip_sign_of_node_in_offset(bvc_dag_t * dag,bvc_offset_t * d,bvnode_t i)2663 static void flip_sign_of_node_in_offset(bvc_dag_t *dag, bvc_offset_t *d, bvnode_t i) {
2664 assert(node_of_occ(d->nocc) == i);
2665 d->nocc ^= 1; // flip low-order bit
2666 }
2667
flip_sign_of_node_in_sum(bvc_dag_t * dag,bvc_sum_t * d,bvnode_t i)2668 static void flip_sign_of_node_in_sum(bvc_dag_t *dag, bvc_sum_t *d, bvnode_t i) {
2669 uint32_t j, n;
2670
2671 n = d->len;
2672 for (j=0; j<n; j++) {
2673 if (node_of_occ(d->sum[j]) == i) {
2674 d->sum[j] ^= 1;
2675 }
2676 }
2677 }
2678
2679 /*
2680 * Flip the sign of node i in a monomial d
2681 * - d = descriptor of node x
2682 * - x := [MONO a +i], we flip the sign of x
2683 */
flip_sign_of_node_in_monomial(bvc_dag_t * dag,bvc_mono_t * d,bvnode_t x,bvnode_t i)2684 static void flip_sign_of_node_in_monomial(bvc_dag_t *dag, bvc_mono_t *d, bvnode_t x, bvnode_t i) {
2685 assert(d->nocc == bvp(i));
2686 int_queue_push(&dag->flip_queue, x);
2687 }
2688
2689 /*
2690 * Flip the sign of node i in product d
2691 * - d must be the descriptor of node x
2692 * - i must occur in the product
2693 * - if i's exponent is even, nothing changes
2694 * - if i's exponent is odd, we flip the sign of x
2695 */
flip_sign_of_node_in_product(bvc_dag_t * dag,bvc_prod_t * d,bvnode_t x,bvnode_t i)2696 static void flip_sign_of_node_in_product(bvc_dag_t *dag, bvc_prod_t *d, bvnode_t x, bvnode_t i) {
2697 int32_t k;
2698
2699 assert(pprod_is_normalized(d));
2700
2701 k = pprod_get_index(d, bvp(i));
2702 assert(0 <= k && k < d->len && d->prod[k].var == bvp(i));
2703 if ((d->prod[k].exp & 1) == 1) {
2704 int_queue_push(&dag->flip_queue, x);
2705 }
2706 }
2707
2708
2709 /*
2710 * Flip the sign of node i in descriptor d
2711 * - d must be the descriptor of node x
2712 */
flip_sign_of_node_in_descriptor(bvc_dag_t * dag,bvc_header_t * d,bvnode_t x,bvnode_t i)2713 static void flip_sign_of_node_in_descriptor(bvc_dag_t *dag, bvc_header_t *d, bvnode_t x, bvnode_t i) {
2714 switch (d->tag) {
2715 case BVC_LEAF:
2716 case BVC_ALIAS:
2717 case BVC_ZERO:
2718 case BVC_CONSTANT:
2719 // should not happen
2720 assert(false);
2721 break;
2722
2723 case BVC_OFFSET:
2724 flip_sign_of_node_in_offset(dag, offset_node(d), i);
2725 break;
2726
2727 case BVC_MONO:
2728 flip_sign_of_node_in_monomial(dag, mono_node(d), x, i);
2729 break;
2730
2731 case BVC_SUM:
2732 flip_sign_of_node_in_sum(dag, sum_node(d), i);
2733 break;
2734
2735 case BVC_PROD:
2736 flip_sign_of_node_in_product(dag, prod_node(d), x, i);
2737 break;
2738 }
2739 }
2740
2741 /*
2742 * Flip the sign of node i
2743 * - replace +i by -i and -i by +i in all nodes that depend on i.
2744 */
flip_sign_of_node(bvc_dag_t * dag,bvnode_t i)2745 static void flip_sign_of_node(bvc_dag_t *dag, bvnode_t i) {
2746 int32_t *l;
2747 uint32_t j, m;
2748 bvnode_t x;
2749
2750 l = dag->use[i];
2751 if (l != NULL) {
2752 m = iv_size(l);
2753 for (j=0; j<m; j++) {
2754 x = l[j];
2755 assert(0 < x && x <= dag->nelems);
2756 flip_sign_of_node_in_descriptor(dag, dag->desc[x], x, i);
2757 }
2758 }
2759 }
2760
2761
2762 /*
2763 * Flip the signs of all nodes in the flip_queue
2764 */
propagate_flips(bvc_dag_t * dag)2765 static void propagate_flips(bvc_dag_t *dag) {
2766 int_queue_t *queue;
2767 bvnode_t i;
2768
2769 queue = &dag->flip_queue;
2770 while (! int_queue_is_empty(queue)) {
2771 i = int_queue_pop(queue);
2772 flip_sign_of_node(dag, i);
2773
2774 mark_flipped_node(dag, i);
2775 }
2776 }
2777
2778
2779 /*
2780 * SUM REDUCTION
2781 */
2782
2783 /*
2784 * Node for c * n:
2785 * - return -1 if c is zero
2786 */
simple_mono_in_sum(bvc_dag_t * dag,int32_t c,node_occ_t n)2787 static node_occ_t simple_mono_in_sum(bvc_dag_t *dag, int32_t c, node_occ_t n) {
2788 uint32_t bitsize;
2789 uint64_t a;
2790 node_occ_t mono;
2791
2792 mono = -1;
2793 bitsize = bvc_dag_occ_bitsize(dag, n);
2794 if (bitsize > 64) {
2795 if (c != 0) mono = bvc_dag_simple_mono(dag, c, n, bitsize);
2796 } else {
2797 a = norm64((uint64_t) c, bitsize);
2798 if (a != 0) mono = bvc_dag_mono64(dag, a, n, bitsize);
2799 }
2800
2801 return mono;
2802 }
2803
2804 /*
2805 * Remove duplicates from v
2806 * - the duplicate is either +n or -n
2807 */
normalize_sum_after_replace(bvc_dag_t * dag,ivector_t * v,node_occ_t n)2808 static void normalize_sum_after_replace(bvc_dag_t *dag, ivector_t *v, node_occ_t n) {
2809 uint32_t i, j, m;
2810 node_occ_t x;
2811 int32_t c;
2812
2813 m = v->size;
2814 for (;;) {
2815 c = 0;
2816 // compute c := coefficient of n in v
2817 // and remove all occurrences of n from v
2818 j = 0;
2819 for (i=0; i<m; i++) {
2820 x = v->data[i];
2821 if (same_node(x, n)) {
2822 if (x == n) {
2823 c ++;
2824 } else {
2825 assert(x == negate_occ(n));
2826 c --;
2827 }
2828 } else {
2829 v->data[j] = x;
2830 j ++;
2831 }
2832 }
2833
2834 assert(j <= m);
2835
2836 // construct x := c * n
2837 x = simple_mono_in_sum(dag, c, n);
2838 if (x < 0) break; // c * n is zero so we're done
2839
2840 // add c * n to vector v
2841 v->data[j] = x;
2842 j ++;
2843 if (same_node(x, n)) break; // c * n is either +n or -n so we're done
2844
2845 // x may be a duplicate now
2846 n = x;
2847 m = j;
2848 }
2849
2850 v->size = j;
2851 }
2852
2853 /*
2854 * Replace the pair n1, n2 by n in p->sum
2855 * - n1 and n2 occur in p->sum at index k1 and k2 respectively
2856 * - store the result in vector dag->sum_buffer
2857 */
replace_pair_in_sum(bvc_dag_t * dag,bvc_sum_t * p,node_occ_t n,node_occ_t n1,node_occ_t n2,uint32_t k1,uint32_t k2)2858 static void replace_pair_in_sum(bvc_dag_t *dag, bvc_sum_t *p, node_occ_t n, node_occ_t n1, node_occ_t n2,
2859 uint32_t k1, uint32_t k2) {
2860 ivector_t *v;
2861 uint32_t i, m;
2862 node_occ_t x;
2863 bool has_duplicate;
2864
2865 assert(k1 < p->len && p->sum[k1] == n1);
2866 assert(k2 < p->len && p->sum[k2] == n2);
2867 assert(k1 != k2);
2868
2869 // construct v := nodes in p->sum with n1 and n2 removed and n added.
2870 // set has_duplicate to true if p->sum already contains n or -n
2871 v = &dag->sum_buffer;
2872 ivector_reset(v);
2873 has_duplicate = false;
2874
2875 m = p->len;
2876 for (i=0; i<m; i++) {
2877 if (i != k1 && i != k2) {
2878 x = p->sum[i];
2879 ivector_push(v, x);
2880 has_duplicate |= same_node(x, n);
2881 }
2882 }
2883 ivector_push(v, n);
2884
2885 if (has_duplicate) {
2886 normalize_sum_after_replace(dag, v, n);
2887 }
2888 }
2889
2890
2891 /*
2892 * Replace n0 by n1 in p->sum
2893 * - store the result in dag->sum_buffer
2894 */
replace_node_in_sum(bvc_dag_t * dag,bvc_sum_t * p,bvnode_t n0,node_occ_t n1)2895 static void replace_node_in_sum(bvc_dag_t *dag, bvc_sum_t *p, bvnode_t n0, node_occ_t n1) {
2896 ivector_t *v;
2897 uint32_t i, m;
2898 node_occ_t x;
2899 bool has_duplicate;
2900
2901 v = &dag->sum_buffer;
2902 ivector_reset(v);
2903 has_duplicate = false;
2904
2905 m = p->len;
2906 for (i=0; i<m; i++) {
2907 x = p->sum[i];
2908 if (node_of_occ(x) == n0) {
2909 // either x == +n0 or x == -n0
2910 // in the first case, we replace x by n1
2911 // in the second case, we replace x by not(n1) = n1 ^ 1
2912 x = n1 ^ sign_of_occ(x);
2913 } else {
2914 has_duplicate |= same_node(x, n1);
2915 }
2916 ivector_push(v, x);
2917 }
2918
2919 if (has_duplicate) {
2920 normalize_sum_after_replace(dag, v, n1);
2921 }
2922 }
2923
2924
2925 /*
2926 * Change the definition of a sum node i
2927 * - p = descriptor of node i
2928 * - a = new array of nodes = new definition
2929 * - n = number of elements in a
2930 */
rebuild_sum(bvc_dag_t * dag,bvc_sum_t * p,bvnode_t i,node_occ_t * a,uint32_t n)2931 static void rebuild_sum(bvc_dag_t *dag, bvc_sum_t *p, bvnode_t i, node_occ_t *a, uint32_t n) {
2932 uint32_t j, m;
2933 node_occ_t x;
2934
2935 assert(n <= p->len);
2936
2937 if (n == 0) {
2938 // i is reduced to zero
2939 convert_to_zero(dag, i);
2940 } else if (n == 1) {
2941 // i is reduced to a single node
2942 convert_to_alias(dag, i, a[0]);
2943 } else {
2944 // i remains a sum
2945 m = p->len;
2946 for (j=0; j<m; j++) {
2947 x = p->sum[j];
2948 bvc_dag_remove_dependent(dag, node_of_occ(x), i);
2949 }
2950
2951 p->hash = 0;
2952 for (j=0; j<n; j++) {
2953 x = a[j];
2954 p->sum[j] = x;
2955 p->hash |= bit_hash_occ(x);
2956 bvc_dag_add_dependency(dag, node_of_occ(x), i);
2957 }
2958 p->len = n;
2959
2960 if (sum_node_is_elementary(dag, p)) {
2961 bvc_dag_move_to_elementary_list(dag, i);
2962 }
2963 }
2964 }
2965
2966
2967 /*
2968 * Replace the pair n1, n2 by n in p->sum:
2969 * - p must be the descriptor of node i
2970 * - n1 and n2 must occur in p at position k1 and k2, respectively
2971 * - move i to the elementary list if p becomes elementary
2972 */
rewrite_pair_in_sum(bvc_dag_t * dag,bvc_sum_t * p,bvnode_t i,node_occ_t n,node_occ_t n1,node_occ_t n2,uint32_t k1,uint32_t k2)2973 static void rewrite_pair_in_sum(bvc_dag_t *dag, bvc_sum_t *p, bvnode_t i,
2974 node_occ_t n, node_occ_t n1, node_occ_t n2, uint32_t k1, uint32_t k2) {
2975 ivector_t *v;
2976 uint32_t m;
2977
2978 // compute the reduced sum in dag->sum_buffer
2979 replace_pair_in_sum(dag, p, n, n1, n2, k1, k2);
2980
2981 v = &dag->sum_buffer;
2982 m = v->size;
2983 assert(m < p->len);
2984 rebuild_sum(dag, p, i, v->data, m);
2985 }
2986
2987 /*
2988 * Simplify sum when n0 is aliased to n1
2989 * - replace n0 by n1 in p
2990 * - p must be the descriptor of node i
2991 * - n0 must occur in p
2992 */
alias_node_in_sum(bvc_dag_t * dag,bvc_sum_t * p,bvnode_t i,bvnode_t n0,node_occ_t n1)2993 static void alias_node_in_sum(bvc_dag_t *dag, bvc_sum_t *p, bvnode_t i, bvnode_t n0, node_occ_t n1) {
2994 ivector_t *v;
2995 uint32_t m;
2996
2997 // replace n0 by n1 then normalize
2998 replace_node_in_sum(dag, p, n0, n1);
2999
3000 v = &dag->sum_buffer;
3001 m = v->size;
3002 assert(m <= p->len);
3003 rebuild_sum(dag, p, i, v->data, m);
3004 }
3005
3006
3007 /*
3008 * Simplify sum when n is converted to zero:
3009 * - remove n from p
3010 * - p must be the descriptor of node i
3011 * - either +n or -n must occur in p
3012 */
zero_node_in_sum(bvc_dag_t * dag,bvc_sum_t * p,bvnode_t i,bvnode_t n)3013 static void zero_node_in_sum(bvc_dag_t *dag, bvc_sum_t *p, bvnode_t i, bvnode_t n) {
3014 uint32_t j, k, m;
3015 node_occ_t x;
3016
3017 assert(p->len >= 2);
3018
3019 m = p->len;
3020
3021 if (m == 2) {
3022 if (node_of_occ(p->sum[0]) == n) {
3023 // i := aliased to p->sum[1]
3024 convert_to_alias(dag, i, p->sum[1]);
3025 } else {
3026 assert(node_of_occ(p->sum[1]) == n);
3027 // i := aliase to p->sum[0]
3028 convert_to_alias(dag, i, p->sum[0]);
3029 }
3030 } else {
3031 // i := shorter sum
3032 k = 0;
3033 p->hash = 0;
3034 for (j=0; j<m; j++) {
3035 x = p->sum[j];
3036 if (node_of_occ(x) != n) {
3037 p->sum[k] = j;
3038 p->hash |= bit_hash_occ(x);
3039 k ++;
3040 }
3041 }
3042 assert(k == m-1);
3043 p->len = k;
3044 bvc_dag_remove_dependent(dag, n, i);
3045
3046 if (sum_node_is_elementary(dag, p)) {
3047 bvc_dag_move_to_elementary_list(dag, i);
3048 }
3049 }
3050 }
3051
3052
3053
3054 /*
3055 * PRODUCT REDUCTION
3056 */
3057
3058 /*
3059 * Simplify a product when n0 is aliased to n1
3060 * - this removes n0 from p and multiplies
3061 * - p must be the descriptor of node i
3062 * - n0 must occur in p
3063 */
alias_node_in_product(bvc_dag_t * dag,bvc_prod_t * p,bvnode_t i,bvnode_t n0,node_occ_t n)3064 static void alias_node_in_product(bvc_dag_t *dag, bvc_prod_t *p, bvnode_t i, bvnode_t n0, node_occ_t n) {
3065 int32_t k0, k;
3066 uint32_t e0;
3067 bool flip_sign;
3068
3069 assert(pprod_is_normalized(p));
3070
3071 k0 = pprod_get_index(p, bvp(n0));
3072 assert(0 <= k0 && k0 < p->len && p->prod[k0].var == bvp(n0));
3073
3074 e0 = p->prod[k0].exp;
3075
3076 // we'll have to flip the sign if e0 is odd and n is a negative occurrence
3077 flip_sign = ((e0 & 1) == 1) && sign_of_occ(n) == 1;
3078
3079 // force n to be positive
3080 n = unsigned_occ(n);
3081 assert(sign_of_occ(n) == 0);
3082
3083 k = pprod_get_index(p, n);
3084 if (k < 0) {
3085 // n does not occur in p. We just replace n0 by n
3086 p->prod[k0].var = n;
3087 } else {
3088 // n does occur in p.
3089 assert(k < p->len && p->prod[k0].var == n);
3090 p->prod[k0].exp = 0;
3091 p->prod[k].exp += e0;
3092 cleanup_prod(p);
3093 }
3094
3095 assert(pprod_is_normalized(p));
3096 if (prod_node_is_elementary(dag, p)) {
3097 bvc_dag_move_to_elementary_list(dag, i);
3098 }
3099
3100 if (flip_sign) {
3101 int_queue_push(&dag->flip_queue, i);
3102 propagate_flips(dag);
3103 }
3104 }
3105
3106
3107
3108 /*
3109 * Simplify node x after node i is converted to zero
3110 * - d = descriptor of node x
3111 * - d must contain i
3112 */
zero_node_in_descriptor(bvc_dag_t * dag,bvc_header_t * d,bvnode_t x,bvnode_t i)3113 static void zero_node_in_descriptor(bvc_dag_t *dag, bvc_header_t *d, bvnode_t x, bvnode_t i) {
3114 switch (d->tag) {
3115 case BVC_SUM:
3116 zero_node_in_sum(dag, sum_node(d), x, i);
3117 break;
3118
3119 case BVC_MONO:
3120 case BVC_PROD:
3121 convert_to_zero(dag, x);
3122 break;
3123
3124 default:
3125 // don't touch x.
3126 // we could convert OFFSET nodes to CONSTANT NODES?
3127 break;
3128 }
3129 }
3130
3131 /*
3132 * Simplify nodes that depend on i after i is converted to zero
3133 */
propagate_zero_node(bvc_dag_t * dag,bvnode_t i)3134 static void propagate_zero_node(bvc_dag_t *dag, bvnode_t i) {
3135 ivector_t *v;
3136 int32_t *l;
3137 uint32_t j, m;
3138 bvnode_t x;
3139
3140 assert(bvc_dag_node_is_zero(dag, i));
3141
3142 l = dag->use[i];
3143 if (l != NULL) {
3144 m = iv_size(l);
3145
3146 // copy l into dag->use_buffer since l may be modified
3147 v = &dag->use_buffer;
3148 ivector_copy(v, l, m);
3149
3150 for (j=0; j<m; j++) {
3151 x = v->data[j];
3152 assert(0 < x && x <= dag->nelems);
3153 zero_node_in_descriptor(dag, dag->desc[x], x, i);
3154 }
3155
3156 ivector_reset(v);
3157 }
3158 }
3159
3160
3161
3162 /*
3163 * Replace i by n in descriptor d
3164 * - i is known to occur in d
3165 * - d is the descriptor of node x
3166 */
alias_node_in_offset(bvc_dag_t * dag,bvc_offset_t * d,bvnode_t x,bvnode_t i,node_occ_t n)3167 static void alias_node_in_offset(bvc_dag_t *dag, bvc_offset_t *d, bvnode_t x, bvnode_t i, node_occ_t n) {
3168 // if d->nocc == bvp(i) then d->nocc := n
3169 // if d->nocc == bvn(i) then d->nocc := negate(n);
3170 assert(node_of_occ(d->nocc) == i);
3171 d->nocc = n ^ sign_of_occ(d->nocc);
3172 if (offset_node_is_elementary(dag, d)) {
3173 bvc_dag_move_to_elementary_list(dag, x);
3174 }
3175 }
3176
alias_node_in_mono(bvc_dag_t * dag,bvc_mono_t * d,bvnode_t x,bvnode_t i,node_occ_t n)3177 static void alias_node_in_mono(bvc_dag_t *dag, bvc_mono_t *d, bvnode_t x, bvnode_t i, node_occ_t n) {
3178 assert(d->nocc == bvp(i));
3179 d->nocc = unsigned_occ(n);
3180 if (mono_node_is_elementary(dag, d)) {
3181 bvc_dag_move_to_elementary_list(dag, x);
3182 }
3183
3184 if (sign_of_occ(n) == 1) {
3185 int_queue_push(&dag->flip_queue, x);
3186 propagate_flips(dag);
3187 }
3188 }
3189
3190
3191 /*
3192 * Simplify node x after i is aliased to n
3193 * - d = descriptor of node x
3194 * - i must occur in d
3195 */
alias_node_in_descriptor(bvc_dag_t * dag,bvc_header_t * d,bvnode_t x,bvnode_t i,node_occ_t n)3196 static void alias_node_in_descriptor(bvc_dag_t *dag, bvc_header_t *d, bvnode_t x, bvnode_t i, node_occ_t n) {
3197 switch (d->tag) {
3198 case BVC_LEAF:
3199 case BVC_ALIAS:
3200 case BVC_ZERO:
3201 case BVC_CONSTANT:
3202 // should not happen
3203 assert(false);
3204 break;
3205
3206 case BVC_OFFSET:
3207 alias_node_in_offset(dag, offset_node(d), x, i, n);
3208 break;
3209
3210 case BVC_MONO:
3211 alias_node_in_mono(dag, mono_node(d), x, i, n);
3212 break;
3213
3214 case BVC_SUM:
3215 alias_node_in_sum(dag, sum_node(d), x, i, n);
3216 break;
3217
3218 case BVC_PROD:
3219 alias_node_in_product(dag, prod_node(d), x, i, n);
3220 break;
3221 }
3222 }
3223
3224
3225 /*
3226 * Simplify nodes that depend on i after i is aliased to node n
3227 */
propagate_alias_node(bvc_dag_t * dag,bvnode_t i,node_occ_t n)3228 static void propagate_alias_node(bvc_dag_t *dag, bvnode_t i, node_occ_t n) {
3229 ivector_t *v;
3230 int32_t *l;
3231 uint32_t j, m;
3232 bvnode_t x;
3233
3234 assert(bvc_dag_node_is_alias(dag, i));
3235
3236 l = dag->use[i];
3237 if (l != NULL) {
3238 m = iv_size(l);
3239
3240 // copy l into dag->buffer since l may be modified
3241 v = &dag->use_buffer;
3242 ivector_copy(v, l, m);
3243 for (j=0; j<m; j++) {
3244 x = v->data[j];
3245 assert(0 < x && x <= dag->nelems);
3246 alias_node_in_descriptor(dag, dag->desc[x], x, i, n);
3247 bvc_dag_add_dependency(dag, node_of_occ(n), x); // now x depends on n
3248 }
3249 ivector_reset(v);
3250
3251 delete_index_vector(l);
3252 dag->use[i] = NULL;
3253 }
3254 }
3255
3256
3257 /*
3258 * Propagate simplifications
3259 * - the queue stores nodes that were converted to zero or aliased to some occurrence n
3260 */
propagate_simplifications(bvc_dag_t * dag)3261 static void propagate_simplifications(bvc_dag_t *dag) {
3262 int_queue_t *queue;
3263 bvc_alias_t *d;
3264 bvnode_t i;
3265
3266 queue = &dag->node_queue;
3267 while (! int_queue_is_empty(queue)) {
3268 i = int_queue_pop(queue);
3269 if (bvc_dag_node_is_zero(dag, i)) {
3270 propagate_zero_node(dag, i);
3271 } else {
3272 d = bvc_dag_node_alias(dag, i);
3273 propagate_alias_node(dag, i, d->alias);
3274 }
3275 }
3276 }
3277
3278
3279
3280
3281 /*
3282 * Check whether node i is a sum that contains +n1 and +n2 or -n1 and -n2
3283 * If so replace the pair n1, n2 by n in node i
3284 * - h = bit hash of {n1, n2}
3285 */
try_reduce_sum(bvc_dag_t * dag,bvnode_t i,uint32_t h,node_occ_t n,node_occ_t n1,node_occ_t n2)3286 static void try_reduce_sum(bvc_dag_t *dag, bvnode_t i, uint32_t h, node_occ_t n, node_occ_t n1, node_occ_t n2) {
3287 bvc_header_t *d;
3288 bvc_sum_t *p;
3289 uint32_t j, m;
3290 int32_t k1, k2;
3291 int32_t l1, l2;
3292
3293 assert(0 < i && i <= dag->nelems && !same_node(n1, n2));
3294
3295 d = dag->desc[i];
3296 if (node_is_sum(d)) {
3297 p = sum_node(d);
3298 if ((h & p->hash) == h) {
3299 // variables v1 (for n1) and v2 (for n2) may occur in p
3300 m = p->len;
3301 k1 = -1;
3302 k2 = -1;
3303 l1 = -1;
3304 l2 = -1;
3305
3306 /*
3307 * loop to get:
3308 * k1 = last occurrence of +n1 in p (or -1)
3309 * k2 = last occurrence of +n2 in p (or -1)
3310 * l1 = last occurrence of -n1 in p (or -1)
3311 * l2 = last occurrence of -n2 in p (or -1)
3312 */
3313 for (j=0; j<m; j++) {
3314 if (same_node(n1, p->sum[j])) {
3315 if (p->sum[j] == n1) {
3316 k1 = j;
3317 } else {
3318 assert(p->sum[j] == negate_occ(n1));
3319 l1 = j;
3320 }
3321 } else if (same_node(n2, p->sum[j])) {
3322 if (p->sum[j] == n2) {
3323 k2 = j;
3324 } else {
3325 assert(p->sum[j] == negate_occ(n2));
3326 l2 = j;
3327 }
3328 }
3329 }
3330
3331 if (k1 >= 0 && k2 >= 0) {
3332 assert(p->sum[k1] == n1 && p->sum[k2] == n2);
3333 rewrite_pair_in_sum(dag, p, i, n, n1, n2, k1, k2);
3334 }
3335 if (l1 >= 0 && l2 >= 0) {
3336 assert(p->sum[l1] == negate_occ(n1) && p->sum[l2] == negate_occ(n2));
3337 rewrite_pair_in_sum(dag, p, i, negate_occ(n), negate_occ(n1), negate_occ(n2), l1, l2);
3338 }
3339 }
3340 }
3341 }
3342
3343
3344 /*
3345 * Replace all occurrences of {n1, n2} in sums by n
3346 * - n must be a leaf node
3347 */
bvc_dag_reduce_sum(bvc_dag_t * dag,node_occ_t n,node_occ_t n1,node_occ_t n2)3348 void bvc_dag_reduce_sum(bvc_dag_t *dag, node_occ_t n, node_occ_t n1, node_occ_t n2) {
3349 ivector_t *v;
3350 int32_t *l1, *l2;
3351 uint32_t m, i;
3352 bvnode_t r1, r2;
3353 uint32_t h;
3354
3355 r1 = node_of_occ(n1);
3356 r2 = node_of_occ(n2);
3357 h = bit_hash(r1) | bit_hash(r2);
3358
3359 assert(0 < r1 && r1 <= dag->nelems && 0 < r2 && r2 <= dag->nelems);
3360
3361 l1 = dag->use[r1];
3362 l2 = dag->use[r2];
3363
3364 if (l1 != NULL && l2 != NULL) {
3365 m = iv_size(l1);
3366 i = iv_size(l2);
3367 if (i < m) {
3368 m = i;
3369 l1 = l2;
3370 }
3371
3372 /*
3373 * l1 = smallest of use[r1], use[r2]
3374 * m = length of l1
3375 */
3376 // copy l1 into dag->buffer since try_reduce_sum may modify l1
3377 v = &dag->buffer;
3378 ivector_copy(v, l1, m);
3379 for (i=0; i<m; i++) {
3380 try_reduce_sum(dag, v->data[i], h, n, n1, n2);
3381 }
3382 ivector_reset(v);
3383
3384 propagate_simplifications(dag);
3385 }
3386
3387 }
3388
3389
3390
3391 /*
3392 * Check whether node i is a sum that contains n1 and n2 or -n1 and -n2
3393 * - h = bit hash of {n1, n2}
3394 */
check_reduce_sum(bvc_dag_t * dag,bvnode_t i,uint32_t h,node_occ_t n1,node_occ_t n2)3395 static bool check_reduce_sum(bvc_dag_t *dag, bvnode_t i, uint32_t h, node_occ_t n1, node_occ_t n2) {
3396 bvc_header_t *d;
3397 bvc_sum_t *p;
3398 uint32_t j, m;
3399 int32_t k1, k2;
3400 int32_t l1, l2;
3401
3402 assert(0 < i && i <= dag->nelems && !same_node(n1, n2));
3403
3404 d = dag->desc[i];
3405 if (node_is_sum(d)) {
3406 p = sum_node(d);
3407 if ((h & p->hash) == h) {
3408 m = p->len;
3409 k1 = -1;
3410 k2 = -1;
3411 l1 = -1;
3412 l2 = -1;
3413 for (j=0; j<m; j++) {
3414 if (p->sum[j] == n1) {
3415 k1 = j;
3416 if (k2 >= 0) {
3417 assert(p->sum[k2] == n2);
3418 return true;
3419 }
3420 } else if (p->sum[j] == negate_occ(n1)) {
3421 l1 = j;
3422 if (l2 >= 0) {
3423 assert(p->sum[l2] == negate_occ(n2));
3424 return true;
3425 }
3426 } else if (p->sum[j] == n2) {
3427 k2 = j;
3428 if (k1 >= 0) {
3429 assert(p->sum[k1] == n1);
3430 return true;
3431 }
3432 } else if (p->sum[j] == negate_occ(n2)) {
3433 l2 = j;
3434 if (l1 >= 0) {
3435 assert(p->sum[l1] == negate_occ(n1));
3436 return true;
3437 }
3438 }
3439 }
3440 }
3441 }
3442
3443
3444 return false;
3445 }
3446
3447
3448 /*
3449 * Check whether there is a sum node that can be reduced by n1 + n2 or -n1 -n2
3450 * - n1 and n2 must be distinct
3451 */
bvc_dag_check_reduce_sum(bvc_dag_t * dag,node_occ_t n1,node_occ_t n2)3452 bool bvc_dag_check_reduce_sum(bvc_dag_t *dag, node_occ_t n1, node_occ_t n2) {
3453 int32_t *l1, *l2;
3454 uint32_t m, i;
3455 bvnode_t r1, r2;
3456 uint32_t h;
3457
3458 r1 = node_of_occ(n1);
3459 r2 = node_of_occ(n2);
3460 h = bit_hash(r1) | bit_hash(r2);
3461
3462 assert(0 < r1 && r1 <= dag->nelems && 0 < r2 && r2 <= dag->nelems && r1 != r2);
3463
3464 l1 = dag->use[r1];
3465 l2 = dag->use[r2];
3466
3467 if (l1 != NULL && l2 != NULL) {
3468 m = iv_size(l1);
3469 i = iv_size(l2);
3470 if (i < m) {
3471 m = i;
3472 l1 = l2;
3473 }
3474
3475 for (i=0; i<m; i++) {
3476 if (check_reduce_sum(dag, l1[i], h, n1, n2)) {
3477 return true;
3478 }
3479 }
3480 }
3481
3482 return false;
3483 }
3484
3485
3486
3487
3488 /*
3489 * PRODUCT REDUCTION
3490 */
3491
3492
3493 /*
3494 * Check whether node i is a product that contains n1 * n2
3495 * If so, replace the pair n1 * n2 by n in node i
3496 * - h must be the bit hash of {n1, n2}
3497 * - n1 and n2 must be distinct positive occurrences
3498 */
try_reduce_prod(bvc_dag_t * dag,bvnode_t i,uint32_t h,node_occ_t n,node_occ_t n1,node_occ_t n2)3499 static void try_reduce_prod(bvc_dag_t *dag, bvnode_t i, uint32_t h, node_occ_t n, node_occ_t n1, node_occ_t n2) {
3500 bvc_header_t *d;
3501 bvc_prod_t *p;
3502 int32_t k1, k2, k;
3503 uint32_t e1, e2;
3504
3505 assert(0 < i && i <= dag->nelems && n1 != n2);
3506
3507 d = dag->desc[i];
3508 if (node_is_prod(d)) {
3509 p = prod_node(d);
3510 if ((h & p->hash) == h) {
3511 k1 = pprod_get_index(p, n1);
3512 k2 = pprod_get_index(p, n2);
3513 if (k1 >= 0 && k2 >= 0) {
3514 /*
3515 * p contains n1^e1 * n2^e2 where e1>0 and e2>0
3516 * If e1 <= e2: n1^e1 * n2^e2 --> n^e1 * n2^(e2 - e1)
3517 * If e2 < e1: n1^e1 * n2^e2 --> n^e2 * n1^(e1 - e2)
3518 */
3519 e1 = p->prod[k1].exp;
3520 e2 = p->prod[k2].exp;
3521 if (e1 <= e2) {
3522 bvc_dag_remove_dependent(dag, node_of_occ(n1), i);
3523 p->prod[k1].exp = 0;
3524 p->prod[k2].exp -= e1;
3525 if (e1 == e2) {
3526 bvc_dag_remove_dependent(dag, node_of_occ(n2), i);
3527 }
3528 } else {
3529 bvc_dag_remove_dependent(dag, node_of_occ(n2), i);
3530 p->prod[k1].exp -= e2;
3531 p->prod[k2].exp = 0;
3532 k1 = k2;
3533 e1 = e2;
3534 }
3535
3536 // increase exponent of n by e1
3537 assert(p->prod[k1].exp == 0);
3538 k = pprod_get_index(p, n);
3539 if (k >= 0) {
3540 p->prod[k].exp += e1;
3541 } else {
3542 bvc_dag_add_dependency(dag, node_of_occ(n), i);
3543 // store n^e1 at index k1
3544 p->prod[k1].var = n;
3545 p->prod[k1].exp = e1;
3546 }
3547
3548 cleanup_prod(p);
3549 if (prod_node_is_elementary(dag, p)) {
3550 bvc_dag_move_to_elementary_list(dag, i);
3551 }
3552 }
3553 }
3554
3555 }
3556 }
3557
3558
3559 /*
3560 * Check whether node i is a product that contains n1^2
3561 * If so replace n1^2 by n in node i
3562 * - h must be the hash of n1
3563 */
try_reduce_square(bvc_dag_t * dag,bvnode_t i,uint32_t h,node_occ_t n,node_occ_t n1)3564 static void try_reduce_square(bvc_dag_t *dag, bvnode_t i, uint32_t h, node_occ_t n, node_occ_t n1) {
3565 bvc_header_t *d;
3566 bvc_prod_t *p;
3567 int32_t k1, k;
3568 uint32_t e;
3569
3570 assert(0 < i && i <= dag->nelems);
3571
3572 d = dag->desc[i];
3573 if (node_is_prod(d)) {
3574 p = prod_node(d);
3575 if ((h & p->hash) == h) {
3576 k1 = pprod_get_index(p, n1);
3577 if (k1 >= 0) {
3578 e = p->prod[k1].exp;
3579 if (e >= 2) {
3580 /*
3581 * p contains n1^e with e >= 2
3582 * If e is 2t+1: n1^e ---> n1 * n^t
3583 * If e is 2t: n1^e ---> n^t
3584 */
3585 if ((e & 1) == 0) {
3586 p->prod[k1].exp = 0;
3587 bvc_dag_remove_dependent(dag, node_of_occ(n1), i);
3588 } else {
3589 p->prod[k1].exp = 1;
3590 }
3591
3592 e >>= 1;
3593 k = pprod_get_index(p, n);
3594 if (k >= 0) {
3595 p->prod[k].exp += e;
3596 cleanup_prod(p);
3597 } else {
3598 bvc_dag_add_dependency(dag, node_of_occ(n), i);
3599 if (p->prod[k1].exp == 0) {
3600 // store n^e at index k1
3601 p->prod[k1].var = n;
3602 p->prod[k1].exp = e;
3603 cleanup_prod(p);
3604 } else {
3605 p = mk_prod_times_occ_power(dag, p, n, e);
3606 dag->desc[i] = &p->header;
3607 }
3608 }
3609 assert(pprod_is_normalized(p));
3610 if (prod_node_is_elementary(dag, p)) {
3611 bvc_dag_move_to_elementary_list(dag, i);
3612 }
3613 }
3614 }
3615
3616 }
3617 }
3618 }
3619
3620
3621
3622 /*
3623 * Replace all occurrences of {n1, n2} in products by n
3624 */
bvc_dag_reduce_prod(bvc_dag_t * dag,node_occ_t n,node_occ_t n1,node_occ_t n2)3625 void bvc_dag_reduce_prod(bvc_dag_t *dag, node_occ_t n, node_occ_t n1, node_occ_t n2) {
3626 ivector_t *v;
3627 int32_t *l1, *l2;
3628 uint32_t m, i;
3629 bvnode_t r1, r2;
3630 uint32_t h;
3631
3632 r1 = node_of_occ(n1);
3633 r2 = node_of_occ(n2);
3634 h = bit_hash(r1) | bit_hash(r2);
3635
3636 assert(0 < r1 && r1 <= dag->nelems && 0 < r2 && r2 <= dag->nelems);
3637
3638 l1 = dag->use[r1];
3639 l2 = dag->use[r2];
3640
3641 if (l1 != NULL && l2 != NULL) {
3642 m = iv_size(l1);
3643 i = iv_size(l2);
3644 if (i < m) {
3645 m = i;
3646 l1 = l2;
3647 }
3648
3649 /*
3650 * l1 = smallest of use[r1], use[r2]
3651 * m = length of l1
3652 */
3653 // copy l1 into dag->buffer since try_reduce_prod may modify l1
3654 v = &dag->buffer;
3655 ivector_copy(v, l1, m);
3656
3657 if (n1 == n2) {
3658 for (i=0; i<m; i++) {
3659 try_reduce_square(dag, v->data[i], h, n, n1);
3660 }
3661 } else {
3662 for (i=0; i<m; i++) {
3663 try_reduce_prod(dag, v->data[i], h, n, n1, n2);
3664 }
3665 }
3666
3667 ivector_reset(v);
3668
3669 propagate_simplifications(dag);
3670 }
3671
3672 }
3673
3674
3675 /*
3676 * Check whether i is a polynomial that contains n1 * n2 as a subproduct
3677 * - h = bit_hash of {n1, n2}
3678 */
check_reduce_prod(bvc_dag_t * dag,bvnode_t i,uint32_t h,node_occ_t n1,node_occ_t n2)3679 static bool check_reduce_prod(bvc_dag_t *dag, bvnode_t i, uint32_t h, node_occ_t n1, node_occ_t n2) {
3680 bvc_header_t *d;
3681 bvc_prod_t *p;
3682
3683 assert(0 < i && i <= dag->nelems && n1 != n2);
3684
3685 d = dag->desc[i];
3686 if (node_is_prod(d)) {
3687 p = prod_node(d);
3688 if ((h & p->hash) == h) {
3689 return pprod_get_index(p, n1) >= 0 && pprod_get_index(p, n2) >= 0;
3690 }
3691 }
3692
3693 return false;
3694 }
3695
3696
3697 /*
3698 * Check whether i is a polynomial that contains n1^2 as a subproduct
3699 * - h = bit_hash of {n1}
3700 */
check_reduce_square(bvc_dag_t * dag,bvnode_t i,uint32_t h,node_occ_t n1)3701 static bool check_reduce_square(bvc_dag_t *dag, bvnode_t i, uint32_t h, node_occ_t n1) {
3702 bvc_header_t *d;
3703 bvc_prod_t *p;
3704 int32_t k;
3705
3706 assert(0 < i && i <= dag->nelems);
3707
3708 d = dag->desc[i];
3709 if (node_is_prod(d)) {
3710 p = prod_node(d);
3711 if ((h & p->hash) == h) {
3712 k = pprod_get_index(p, n1);
3713 return k >= 0 && p->prod[k].exp >= 2;
3714 }
3715 }
3716
3717 return false;
3718 }
3719
3720
3721 /*
3722 * Check whether there's a product node that can be reduced by n1 * n2
3723 */
bvc_dag_check_reduce_prod(bvc_dag_t * dag,node_occ_t n1,node_occ_t n2)3724 bool bvc_dag_check_reduce_prod(bvc_dag_t *dag, node_occ_t n1, node_occ_t n2) {
3725 int32_t *l1, *l2;
3726 uint32_t m, i;
3727 bvnode_t r1, r2;
3728 uint32_t h;
3729
3730 r1 = node_of_occ(n1);
3731 r2 = node_of_occ(n2);
3732 h = bit_hash(r1) | bit_hash(r2);
3733
3734 assert(0 < r1 && r1 <= dag->nelems && 0 < r2 && r2 <= dag->nelems);
3735
3736 l1 = dag->use[r1];
3737 l2 = dag->use[r2];
3738
3739 if (l1 != NULL && l2 != NULL) {
3740 m = iv_size(l1);
3741 i = iv_size(l2);
3742 if (i < m) {
3743 m = i;
3744 l1 = l2;
3745 }
3746
3747 /*
3748 * l1 = smallest of use[r1], use[r2]
3749 * m = length of l1
3750 */
3751 if (n1 == n2) {
3752 for (i=0; i<m; i++) {
3753 if (check_reduce_square(dag, l1[i], h, n1)) {
3754 return true;
3755 }
3756 }
3757 } else {
3758 for (i=0; i<m; i++) {
3759 if (check_reduce_prod(dag, l1[i], h, n1, n2)) {
3760 return true;
3761 }
3762 }
3763 }
3764 }
3765
3766 return false;
3767 }
3768
3769
3770
3771 /*
3772 * GENERATION OF NEW ELEMENTARY NODES
3773 *
3774 *
3775 * Heuristic:
3776 * - we try to find two leaf nodes r and s that occur often together in sums or products.
3777 * - then we introduce a new elementary node t := (SUM +/-r +/-s) or k := (prod r s)
3778 */
3779
3780 /*
3781 * Affinity metric for a pair of node (r, s) in sums
3782 * - we compute two scores:
3783 * score[0] = number of sums where r and s occur with the same sign
3784 * score[1] = number of sums where r and s occur with opposite signs
3785 */
affinity_scores_in_sum(bvc_sum_t * p,bvnode_t r,bvnode_t s,uint32_t score[2])3786 static void affinity_scores_in_sum(bvc_sum_t *p, bvnode_t r, bvnode_t s, uint32_t score[2]) {
3787 uint32_t i, n;
3788 node_occ_t x;
3789 int32_t k1, k2;
3790
3791 assert(s != r);
3792
3793 n = p->len;
3794 k1 = -1;
3795 k2 = -1;
3796 for (i=0; i<n; i++) {
3797 x = p->sum[i];
3798 if (node_of_occ(x) == r) {
3799 assert(k1 < 0);
3800 k1 = i;
3801 } else if (node_of_occ(x) == s) {
3802 assert(k2 < 0);
3803 k2 = i;
3804 }
3805 }
3806
3807 if (k1 >= 0 && k2 >= 0) {
3808 // p->sum[k1] contains +/- r
3809 // p->sum[k2] contains +/- s
3810 i = sign_of_occ(p->sum[k1]) ^ sign_of_occ(p->sum[k2]);
3811 score[i] ++;
3812 }
3813 }
3814
3815
3816 // full scores for (r, s): both must have non-empty use lists
affinity_scores_sum(bvc_dag_t * dag,bvnode_t r,bvnode_t s,uint32_t score[2])3817 static void affinity_scores_sum(bvc_dag_t *dag, bvnode_t r, bvnode_t s, uint32_t score[2]) {
3818 bvc_header_t *d;
3819 bvc_sum_t *p;
3820 int32_t *l1, *l2;
3821 uint32_t h, i, n;
3822 bvnode_t x;
3823
3824 assert(0 < r && r <= dag->nelems && 0 < s && s <= dag->nelems && s != r);
3825
3826 h = bit_hash(r) | bit_hash(s);
3827
3828 score[0] = 0;
3829 score[1] = 0;
3830
3831 l1 = dag->use[r];
3832 l2 = dag->use[s];
3833 assert(l1 != NULL && l2 != NULL);
3834
3835 n = iv_size(l1);
3836 i = iv_size(l2);
3837 if (i < n) {
3838 l1 = l2;
3839 n = i;
3840 }
3841
3842 /*
3843 * l1 = smallest of use[r] and use[s] and n = length of l1
3844 */
3845 for (i=0; i<n; i++) {
3846 x = l1[i];
3847 assert(0 < x && x <= dag->nelems);
3848 d = dag->desc[x];
3849 if (d->tag == BVC_SUM) {
3850 p = sum_node(d);
3851 if ((p->hash & h) == h) {
3852 // p may contain r and s
3853 affinity_scores_in_sum(p, r, s, score);
3854 }
3855 }
3856 }
3857 }
3858
3859
3860
3861 /*
3862 * Affinity score for products = number of products that contain (r * s)
3863 * - r and s may be equal
3864 */
node_pair_occurs_in_prod(bvc_prod_t * p,bvnode_t r,bvnode_t s)3865 static bool node_pair_occurs_in_prod(bvc_prod_t *p, bvnode_t r, bvnode_t s) {
3866 assert(r != s);
3867 return pprod_get_index(p, bvp(r)) >= 0 && pprod_get_index(p, bvp(s)) >= 0;
3868 }
3869
node_square_occurs_in_prod(bvc_prod_t * p,bvnode_t r)3870 static bool node_square_occurs_in_prod(bvc_prod_t *p, bvnode_t r) {
3871 int32_t k;
3872
3873 k = pprod_get_index(p, bvp(r));
3874 return k >= 0 && p->prod[k].exp >= 2;
3875 }
3876
3877
3878 // affinity for (r * s): both must have non-empty use list and be distinct
affinity_score_prod(bvc_dag_t * dag,bvnode_t r,bvnode_t s)3879 static uint32_t affinity_score_prod(bvc_dag_t *dag, bvnode_t r, bvnode_t s) {
3880 bvc_header_t *d;
3881 bvc_prod_t *p;
3882 int32_t *l1, *l2;
3883 uint32_t h, i, n, score;
3884 bvnode_t x;
3885
3886 assert(0 < r && r <= dag->nelems && 0 < s && s <= dag->nelems && r != s);
3887
3888 score = 0;
3889
3890 h = bit_hash(r) | bit_hash(s);
3891
3892 l1 = dag->use[r];
3893 l2 = dag->use[s];
3894 assert(l1 != NULL && l2 != NULL);
3895
3896 n = iv_size(l1);
3897 i = iv_size(l2);
3898 if (i < n) {
3899 l1 = l2;
3900 n = i;
3901 }
3902
3903 /*
3904 * l1 = smallest of use[r] and use[s] and n = length of l1
3905 */
3906 for (i=0; i<n; i++) {
3907 x = l1[i];
3908 assert(0 < x && x <= dag->nelems);
3909 d = dag->desc[x];
3910 if (d->tag == BVC_PROD) {
3911 p = prod_node(d);
3912 if ((p->hash & h) == h && node_pair_occurs_in_prod(p, r, s)) {
3913 score ++;
3914 }
3915 }
3916 }
3917
3918 return score;
3919 }
3920
3921
3922 // score for (r * r)
affinity_score_square(bvc_dag_t * dag,bvnode_t r)3923 static uint32_t affinity_score_square(bvc_dag_t *dag, bvnode_t r) {
3924 bvc_header_t *d;
3925 bvc_prod_t *p;
3926 int32_t *l;
3927 uint32_t h, i, n, score;
3928 bvnode_t x;
3929
3930 assert(0 < r && r <= dag->nelems);
3931
3932 score = 0;
3933 h = bit_hash(r);
3934
3935 l = dag->use[r];
3936 assert(l != NULL);
3937
3938 n = iv_size(l);
3939 for (i=0; i<n; i++) {
3940 x = l[i];
3941 assert(0 < x && x <= dag->nelems);
3942 d = dag->desc[x];
3943 if (d->tag == BVC_PROD) {
3944 p = prod_node(d);
3945 if ((p->hash & h) == h && node_square_occurs_in_prod(p, r)) {
3946 score ++;
3947 }
3948 }
3949 }
3950
3951 return score;
3952 }
3953
3954
3955
3956
3957 /*
3958 * Heuristic: sort nodes of v by decreasing occurrence count
3959 */
3960 // ordering function: x < y if x has more dependents than y
bvc_node_lt(bvc_dag_t * dag,bvnode_t x,bvnode_t y)3961 static bool bvc_node_lt(bvc_dag_t *dag, bvnode_t x, bvnode_t y) {
3962 return bvnode_num_occs(dag, x) > bvnode_num_occs(dag, y);
3963 }
3964
bvc_sort_nodes(bvc_dag_t * dag,ivector_t * v)3965 static inline void bvc_sort_nodes(bvc_dag_t *dag, ivector_t *v) {
3966 int_array_sort2(v->data, v->size, dag, (int_cmp_fun_t) bvc_node_lt);
3967 }
3968
3969
3970 /*
3971 * Collect all leaf-nodes that occur in p
3972 * - store them in v
3973 */
sum_get_leaves(bvc_dag_t * dag,bvc_sum_t * p,ivector_t * v)3974 static void sum_get_leaves(bvc_dag_t *dag, bvc_sum_t *p, ivector_t *v) {
3975 uint32_t i, n;
3976 bvnode_t x;
3977
3978 n = p->len;
3979 for (i=0; i<n; i++) {
3980 x = node_of_occ(p->sum[i]);
3981 if (bvc_dag_node_is_leaf(dag, x)) {
3982 ivector_push(v, x);
3983 }
3984 }
3985 }
3986
3987
3988 /*
3989 * Same thing for a product p. If x has exponent >= 2 then it's stored twice.
3990 */
prod_get_leaves(bvc_dag_t * dag,bvc_prod_t * p,ivector_t * v)3991 static void prod_get_leaves(bvc_dag_t *dag, bvc_prod_t *p, ivector_t *v) {
3992 uint32_t i, n;
3993 bvnode_t x;
3994
3995 n = p->len;
3996 for (i=0; i<n; i++) {
3997 x = node_of_occ(p->prod[i].var);
3998 assert(p->prod[i].exp >= 1);
3999 if (bvc_dag_node_is_leaf(dag, x)) {
4000 ivector_push(v, x);
4001 if (p->prod[i].exp > 1) {
4002 ivector_push(v, x);
4003 }
4004 }
4005 }
4006 }
4007
4008
4009 /*
4010 * Structure to store the best pair of nodes found so far and its score
4011 */
4012 typedef struct bvc_pair_s {
4013 uint32_t score;
4014 bvnode_t n1;
4015 bvnode_t n2;
4016 } bvc_pair_t;
4017
4018
4019
4020 /*
4021 * Form all pairs (r, a[i]) and store the one with maximal affinity into b
4022 * if the affinity score is better than b->score
4023 * - n = number of nodes in a
4024 * - all nodes of a must be different from r
4025 */
search_sum_pairs(bvc_dag_t * dag,bvc_pair_t * b,bvnode_t * a,uint32_t n,bvnode_t r)4026 static void search_sum_pairs(bvc_dag_t *dag, bvc_pair_t *b, bvnode_t *a, uint32_t n, bvnode_t r) {
4027 uint32_t score[2];
4028 uint32_t i;
4029 bvnode_t s;
4030
4031 for (i=0; i<n; i++) {
4032 s = a[i];
4033 assert(s != r);
4034 if (bvnode_num_occs(dag, s) > b->score) {
4035 affinity_scores_sum(dag, r, s, score);
4036 if (score[0] > b->score) {
4037 b->score = score[0];
4038 b->n1 = bvp(r);
4039 b->n2 = bvp(s);
4040 }
4041
4042 if (score[1] > b->score) {
4043 b->score = score[1];
4044 b->n1 = bvp(r);
4045 b->n2 = bvn(s);
4046 }
4047 }
4048 }
4049 }
4050
search_prod_pairs(bvc_dag_t * dag,bvc_pair_t * b,bvnode_t * a,uint32_t n,bvnode_t r)4051 static void search_prod_pairs(bvc_dag_t *dag, bvc_pair_t *b, bvnode_t *a, uint32_t n, bvnode_t r) {
4052 uint32_t i, score;
4053 bvnode_t s;
4054
4055 for (i=0; i<n; i++) {
4056 s = a[i];
4057 if (bvnode_num_occs(dag, s) > b->score) {
4058 if (r == s) {
4059 score = affinity_score_square(dag, r);
4060 } else {
4061 score = affinity_score_prod(dag, r, s);
4062 }
4063 if (score > b->score) {
4064 b->score = score;
4065 b->n1 = bvp(r);
4066 b->n2 = bvp(s);
4067 }
4068 }
4069 }
4070 }
4071
4072
4073 /*
4074 * Find the pair of elements of a with maximal affinity and store it in b if
4075 * its score is better than b->score
4076 * - a = array of n distinct nodes
4077 */
full_search_sum_pairs(bvc_dag_t * dag,bvc_pair_t * b,bvnode_t * a,uint32_t n)4078 static void full_search_sum_pairs(bvc_dag_t *dag, bvc_pair_t *b, bvnode_t *a, uint32_t n) {
4079 uint32_t i, m;
4080 bvnode_t r;
4081
4082 assert(n >= 2);
4083
4084 /*
4085 * If n is large, we limit the search to the first 3 elements of a
4086 */
4087 m = n-1;
4088 if (n >= 5) {
4089 m = 3;
4090 }
4091
4092 for (i=0; i<m; i++) {
4093 r = a[i];
4094 if (bvnode_num_occs(dag, r) > b->score) {
4095 search_sum_pairs(dag, b, a+(i+1), n-(i+1), r);
4096 }
4097 }
4098 }
4099
4100
full_search_prod_pairs(bvc_dag_t * dag,bvc_pair_t * b,bvnode_t * a,uint32_t n)4101 static void full_search_prod_pairs(bvc_dag_t *dag, bvc_pair_t *b, bvnode_t *a, uint32_t n) {
4102 uint32_t i, m;
4103 bvnode_t r;
4104
4105 assert(n >= 2);
4106
4107 /*
4108 * If n is large, we limit the search to the first 3 elements of a
4109 */
4110 m = n-1;
4111 if (n >= 5) {
4112 m = 3;
4113 }
4114
4115 for (i=0; i<m; i++) {
4116 r = a[i];
4117 if (bvnode_num_occs(dag, r) > b->score) {
4118 search_prod_pairs(dag, b, a+(i+1), n-(i+1), r);
4119 }
4120 }
4121 }
4122
4123
4124
4125 /*
4126 * Select a pair of leaf nodes r, s that occur in p and store it in b if its score
4127 * is better than b->score
4128 */
search_pair_in_sum(bvc_dag_t * dag,bvc_pair_t * b,bvc_sum_t * p)4129 static void search_pair_in_sum(bvc_dag_t *dag, bvc_pair_t *b, bvc_sum_t *p) {
4130 ivector_t *v;
4131 uint32_t n;
4132
4133 v = &dag->buffer;
4134 assert(v->size == 0);
4135
4136 sum_get_leaves(dag, p, v);
4137 n = v->size;
4138 if (n >= 2) {
4139 bvc_sort_nodes(dag, v);
4140 full_search_sum_pairs(dag, b, v->data, n);
4141 }
4142
4143 ivector_reset(v);
4144 }
4145
4146
search_pair_in_prod(bvc_dag_t * dag,bvc_pair_t * b,bvc_prod_t * p)4147 static void search_pair_in_prod(bvc_dag_t *dag, bvc_pair_t *b, bvc_prod_t *p) {
4148 ivector_t *v;
4149 uint32_t n;
4150
4151 v = &dag->buffer;
4152 assert(v->size == 0);
4153
4154 prod_get_leaves(dag, p, v);
4155 n = v->size;
4156 if (n >= 2) {
4157 bvc_sort_nodes(dag, v);
4158 full_search_prod_pairs(dag, b, v->data, n);
4159 }
4160
4161 ivector_reset(v);
4162 }
4163
4164
4165
4166 /*
4167 * Generate an elementary node that will enable reduction of a least one
4168 * non-elementary node of dag.
4169 * - the list of non-elementary node must not be empty
4170 */
bvc_dag_force_elem_node(bvc_dag_t * dag)4171 void bvc_dag_force_elem_node(bvc_dag_t *dag) {
4172 bvc_pair_t aux;
4173 bvc_header_t *d;
4174 bvc_prod_t *p;
4175 bvc_sum_t *q;
4176 bvnode_t i;
4177
4178 aux.score = 0;
4179 aux.n1 = -1;
4180 aux.n2 = -1;
4181
4182 i = bvc_first_complex_node(dag);
4183 while (i > 0) {
4184 assert(i <= dag->nelems);
4185
4186 d = dag->desc[i];
4187 switch (d->tag) {
4188 case BVC_PROD:
4189 p = prod_node(d);
4190 assert(!prod_node_is_elementary(dag, p));
4191 search_pair_in_prod(dag, &aux, p);
4192 if (aux.score > 0) {
4193 // found a new pair
4194 assert(aux.n1 > 0 && aux.n2 > 0);
4195 (void) bvc_dag_pprod2(dag, aux.n1, aux.n2, d->bitsize);
4196 return;
4197 }
4198 break;
4199
4200 case BVC_SUM:
4201 q = sum_node(d);
4202 assert(!sum_node_is_elementary(dag, q));
4203 if (q->len >= 2) {
4204 search_pair_in_sum(dag, &aux, q);
4205 if (aux.score > 0) {
4206 // found a new pair
4207 assert(aux.n1 > 0 && aux.n2 > 0);
4208 (void) bvc_dag_sum2(dag, aux.n1, aux.n2, d->bitsize);
4209 return;
4210 }
4211 }
4212 break;
4213
4214 default:
4215 break;
4216 }
4217 i = dag->list[i].next;
4218 }
4219
4220 // should not reach this point
4221 assert(false);
4222 }
4223
4224
4225
4226 /*
4227 * Compilation result for node_occurrence n
4228 * - follow alias chain until we reach a lead node
4229 * - modulo signs, this is the variable of n if n is a leaf node
4230 * or the variable of n' if n is aliased to n'
4231 * - to encode the signs, we return either bvp(x) or bvn(x)
4232 * where x is a variable
4233 * bvp(x) means that n is compiled to x
4234 * bvn(x) means that n is compiled to (bvneg x)
4235 * - in all other cases, the function returns -1
4236 */
bvc_dag_get_nocc_compilation(bvc_dag_t * dag,node_occ_t n)4237 int32_t bvc_dag_get_nocc_compilation(bvc_dag_t *dag, node_occ_t n) {
4238 bvc_header_t *d;
4239 bvnode_t i;
4240 int32_t x;
4241
4242 i = node_of_occ(n);
4243 assert(0 < i && i <= dag->nelems);
4244 d = dag->desc[i];
4245
4246 while (d->tag == BVC_ALIAS) {
4247 /*
4248 * i is node of n
4249 * i --> [alias n1]
4250 * if n is bvp(i), then alias(n) = n1
4251 * if n is bvn(i), then alias(n) = n1 ^ 1
4252 * so alias(n) = n1 ^ sign_of(n)
4253 */
4254 n = sign_of_occ(n) ^ alias_node(d)->alias;
4255 i = node_of_occ(n);
4256 assert(0 < i && i <= dag->nelems);
4257 d = dag->desc[i];
4258 }
4259
4260 if (d->tag == BVC_LEAF) {
4261 x = leaf_node(d)->map;
4262 return (x << 1) | sign_of_occ(n);
4263 }
4264
4265 return -1;
4266 }
4267