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 /*
24 * When converting bitvector polynomials to elementary expression,
25 * we use an intermediate DAG representation (cf. bvpoly_compiler.h).
26 * The DAG attempts to maximize sharing of subexpressions (so
27 * that bit-blasting works better).
28 */
29
30 #ifndef __BVPOLY_DAG_H
31 #define __BVPOLY_DAG_H
32
33 #include <assert.h>
34 #include <stdint.h>
35
36 #include "utils/bitvectors.h"
37 #include "utils/int_bv_sets.h"
38 #include "utils/int_hash_map.h"
39 #include "utils/int_hash_tables.h"
40 #include "utils/int_queues.h"
41 #include "utils/int_vectors.h"
42 #include "utils/object_stores.h"
43
44 #include "terms/bv64_polynomials.h"
45 #include "terms/bv_constants.h"
46 #include "terms/bv_polynomials.h"
47 #include "terms/bvpoly_buffers.h"
48 #include "terms/power_products.h"
49
50
51 /*
52 * There are seven types of nodes:
53 * - [leaf x] where x is a bitvector variable
54 * - [zero]
55 * - [constant a] where a is a non-zero constant
56 * - [offset a0 n1] denotes (a0 + n1)
57 * - [mono a0 n1] denotes (a0 * n1)
58 * - [prod n1^d1 ... n_k^d_k] denotes a power product
59 * - [sum n1 + ... + n_k]
60 * Where a0 is a constant, and n_t is a node occurrence.
61 *
62 * The [leaf x] nodes correspond to expressions that don't need
63 * compilation (i.e., [leaf x] is compiled to variable x). The other
64 * nodes are expressions to be compiled.
65 *
66 * A node occurrence encodes bvneg:
67 * - given a node index i, then bvp(i) denotes +i
68 * and bvn(i) denotes (bvneg i) = -i.
69 * - the sign is encoded in the lower-order bit of a node occurrence:
70 * bvp(i) is (i << 1) | 0
71 * bvn(i) is (i << 1) | 1
72 *
73 * Constraints:
74 * - in [mono a0 n]: n must be a positive occurrence
75 * - in [prod n1^d1 ... n_k^d_k]: all n_i's must be positive occurrences
76 * - in [sum n1 ... n_k]: the n_i's must not be offset nodes
77 *
78 * The DAG maintains a mapping from bit-vector variables to node occurrences.
79 * - if x is a bitvector polynomial then dag->vmap stores the bvp(n) or
80 * bvn(n) where n is a node index.
81 * - we also use a set (dag->vset) to store the set of variables x
82 * that are mapped to some node occurrence.
83 *
84 * The node descriptors have a common header that includes:
85 * - tag: the node type
86 * - bitsize: number of bits
87 *
88 * For offset and monomial nodes: the constant is either a 64bit integer or a
89 * pointer to an array of k 32bit words, where k = ceil(bitsize/32).
90 *
91 * The nodes are organized in three disjoint sets:
92 * - leaf nodes
93 * - elementary nodes
94 * - other nodes
95 *
96 * A node is elementary if it is of the following forms:
97 * [zero]
98 * [constant a]
99 * [offset a n] where n is a leaf
100 * [mono a * n] where n is a leaf
101 * [prod n1 * n2] where n1 and n2 are leaves
102 * [sum n1 + n2] where n1 and n2 are leaves
103 *
104 * Each node is identified by a positive integer n
105 * - for node n, we store
106 * desc[n] = node descriptor
107 * use[n] = index of nodes that contain +n or -n
108 * - to represent the sets leaf/elementary/other nodes:
109 * we use an array indexed from -2 to the number of nodes - 1
110 * list[i].pre: predecessor in circular list
111 * list[i].next: successor
112 * the three elements list[-2], list[-1], list[0] are headers
113 * for the lists of non-elementary, elementary, leaf nodes, respectively.
114 *
115 * During compilation, a node i may be replaced by a node occurrence n.
116 * We represent this by mapping i to the special descriptor [alias n].
117 * The alias nodes are not stored in any of the lists.
118 */
119
120
121 /*
122 * NODE INDICES AND OCCURRENCES
123 */
124
125 typedef int32_t bvnode_t;
126 typedef int32_t node_occ_t;
127
128 #define MAX_NODE (INT32_MAX/2)
129
bvp(bvnode_t i)130 static inline node_occ_t bvp(bvnode_t i) {
131 assert(0 <= i && i <= MAX_NODE);
132 return i << 1;
133 }
134
bvn(bvnode_t i)135 static inline node_occ_t bvn(bvnode_t i) {
136 assert(0 <= i && i <= MAX_NODE);
137 return (i << 1) | 1;
138 }
139
node_of_occ(node_occ_t n)140 static inline bvnode_t node_of_occ(node_occ_t n) {
141 assert(0 <= n);
142 return (n >> 1);
143 }
144
sign_of_occ(node_occ_t n)145 static inline uint32_t sign_of_occ(node_occ_t n) {
146 return (uint32_t) (n & 1);
147 }
148
149 // flip the sign
negate_occ(node_occ_t n)150 static inline node_occ_t negate_occ(node_occ_t n) {
151 return n ^ 1;
152 }
153
154 // remove the sign
unsigned_occ(node_occ_t n)155 static inline node_occ_t unsigned_occ(node_occ_t n) {
156 return n & ~1;
157 }
158
159 // coefficient of n: either +1 or -1
coeff_of_occ(node_occ_t n)160 static inline int32_t coeff_of_occ(node_occ_t n) {
161 // this is 1 - 2 * sign_of_occ(n)
162 return 1 - ((n & 1) << 1);
163 }
164
165
166 /*
167 * NODE DESCRIPTORS
168 */
169 typedef enum bvc_tag {
170 BVC_LEAF,
171 BVC_ZERO,
172 BVC_CONSTANT,
173 BVC_OFFSET,
174 BVC_MONO,
175 BVC_PROD,
176 BVC_SUM,
177 BVC_ALIAS,
178 } bvc_tag_t;
179
180 typedef struct bvc_header_s {
181 bvc_tag_t tag;
182 uint32_t bitsize;
183 } bvc_header_t;
184
185 typedef struct bvc_leaf_s {
186 bvc_header_t header;
187 int32_t map; // variable the leaf is compiled to
188 } bvc_leaf_t;
189
190 // zero: no attributes except the bitsize
191 typedef struct bvc_zero_s {
192 bvc_header_t header;
193 } bvc_zero_t;
194
195 typedef struct bvc_constant_s {
196 bvc_header_t header;
197 union {
198 uint64_t c;
199 uint32_t *w;
200 } value;
201 } bvc_constant_t;
202
203 typedef struct bvc_offset_s {
204 bvc_header_t header;
205 node_occ_t nocc;
206 union {
207 uint64_t c;
208 uint32_t *w;
209 } constant;
210 } bvc_offset_t;
211
212 typedef struct bvc_mono_s {
213 bvc_header_t header;
214 node_occ_t nocc;
215 union {
216 uint64_t c;
217 uint32_t *w;
218 } coeff;
219 } bvc_mono_t;
220
221
222 /*
223 * Product
224 * - varexp_t is a pair var/exponent defined in power_products.h
225 * - hash = bitmask based on the nodes occurring in the products
226 * - len = number of pairs in the power product
227 * - prod = array of size elements
228 * The actual operands are stored in prod[0..len-1] but
229 * size may be more than len.
230 */
231 typedef struct bvc_prod_s {
232 bvc_header_t header;
233 uint32_t hash;
234 uint32_t size;
235 uint32_t len;
236 varexp_t prod[0];
237 } bvc_prod_t;
238
239 #define MAX_BVC_PROD_LEN (UINT32_MAX/sizeof(varexp_t))
240
241
242 /*
243 * Sum:
244 * - each integer in the sum array is either +n or -n for some node index n
245 * - len = number of elements in the sum
246 * - hash = bitmask
247 * - sum = array of size elements (size >= len)
248 * The operands are in sum[0 .. len-1].
249 */
250 typedef struct bvc_sum_s {
251 bvc_header_t header;
252 uint32_t hash;
253 uint32_t size;
254 uint32_t len;
255 node_occ_t sum[0]; // real size = len (when allocated)
256 } bvc_sum_t;
257
258 #define MAX_BVC_SUM_LEN (UINT32_MAX/sizeof(int32_t))
259
260
261 typedef struct bvc_alias_s {
262 bvc_header_t header;
263 node_occ_t alias;
264 } bvc_alias_t;
265
266
267 /*
268 * Access to descriptors from a pointer to the header
269 */
node_is_leaf(bvc_header_t * d)270 static inline bool node_is_leaf(bvc_header_t *d) {
271 return d->tag == BVC_LEAF;
272 }
273
node_is_zero(bvc_header_t * d)274 static inline bool node_is_zero(bvc_header_t *d) {
275 return d->tag == BVC_ZERO;
276 }
277
node_is_constant(bvc_header_t * d)278 static inline bool node_is_constant(bvc_header_t *d) {
279 return d->tag == BVC_CONSTANT;
280 }
281
node_is_offset(bvc_header_t * d)282 static inline bool node_is_offset(bvc_header_t *d) {
283 return d->tag == BVC_OFFSET;
284 }
285
node_is_mono(bvc_header_t * d)286 static inline bool node_is_mono(bvc_header_t *d) {
287 return d->tag == BVC_MONO;
288 }
289
node_is_prod(bvc_header_t * d)290 static inline bool node_is_prod(bvc_header_t *d) {
291 return d->tag == BVC_PROD;
292 }
293
node_is_sum(bvc_header_t * d)294 static inline bool node_is_sum(bvc_header_t *d) {
295 return d->tag == BVC_SUM;
296 }
297
node_is_alias(bvc_header_t * d)298 static inline bool node_is_alias(bvc_header_t *d) {
299 return d->tag == BVC_ALIAS;
300 }
301
leaf_node(bvc_header_t * d)302 static inline bvc_leaf_t *leaf_node(bvc_header_t *d) {
303 assert(node_is_leaf(d));
304 return (bvc_leaf_t *) d;
305 }
306
zero_node(bvc_header_t * d)307 static inline bvc_zero_t *zero_node(bvc_header_t *d) {
308 assert(node_is_zero(d));
309 return (bvc_zero_t *) d;
310 }
311
bvconst_node(bvc_header_t * d)312 static inline bvc_constant_t *bvconst_node(bvc_header_t *d) {
313 assert(node_is_constant(d));
314 return (bvc_constant_t *) d;
315 }
316
offset_node(bvc_header_t * d)317 static inline bvc_offset_t *offset_node(bvc_header_t *d) {
318 assert(node_is_offset(d));
319 return (bvc_offset_t *) d;
320 }
321
mono_node(bvc_header_t * d)322 static inline bvc_mono_t *mono_node(bvc_header_t *d) {
323 assert(node_is_mono(d));
324 return (bvc_mono_t *) d;
325 }
326
prod_node(bvc_header_t * d)327 static inline bvc_prod_t *prod_node(bvc_header_t *d) {
328 assert(node_is_prod(d));
329 return (bvc_prod_t *) d;
330 }
331
sum_node(bvc_header_t * d)332 static inline bvc_sum_t *sum_node(bvc_header_t *d) {
333 assert(node_is_sum(d));
334 return (bvc_sum_t *) d;
335 }
336
alias_node(bvc_header_t * d)337 static inline bvc_alias_t *alias_node(bvc_header_t *d) {
338 assert(node_is_alias(d));
339 return (bvc_alias_t *) d;
340 }
341
342
343
344 /*
345 * DAG Structure
346 */
347
348 /*
349 * Elements in the circular lists
350 */
351 typedef struct bvc_item_s {
352 int32_t pre;
353 int32_t next;
354 } bvc_item_t;
355
356 /*
357 * To keep track of the nodes mapped to a variable x:
358 * - vset = set of variables mapped to an existing node
359 * - vmap = map variable x to +/-n, where n is a DAG node index
360 * - flipped = a bitvector to keep track of nodes whose sign was flipped
361 * flipped is NULL by default. It's allocated on demand,
362 * for a node i: flipped[i] = 1 if i's sign was flipped.
363 * So a variable that's initially mapped to node n = pos(i) is mapped to
364 * neg(i) after compilation if i was flipped.
365 */
366 typedef struct bvc_dag_s {
367 // node descriptors + use lists + node sets + flip vector
368 bvc_header_t **desc;
369 int32_t **use;
370 bvc_item_t *list;
371 byte_t *flipped;
372
373 uint32_t nelems; // number of nodes (i.e., desc[1] ... desc[nelems] are non-NULL)
374 uint32_t size; // size of arrays desc and use
375
376 int_htbl_t htbl; // for hash consing
377
378 // mapping from variables to nodes
379 int_bvset_t vset;
380 int_hmap_t vmap;
381
382 // stores for descriptor allocation
383 object_store_t leaf_store;
384 object_store_t zero_store;
385 object_store_t constant_store;
386 object_store_t offset_store;
387 object_store_t mono_store;
388 object_store_t prod_store; // for binary products
389 object_store_t sum_store1; // for sums of len <= 4
390 object_store_t sum_store2; // for sums of len between 4 and 8
391 object_store_t alias_store;
392
393 // auxiliary buffers
394 bvconstant_t aux;
395 pp_buffer_t pp_aux;
396 bvpoly_buffer_t poly_buffer;
397 ivector_t buffer;
398 ivector_t sum_buffer;
399 ivector_t use_buffer;
400
401 // queues to propagate simplifications
402 // node_queue stores the ids of nodes reduced to zero or aliased
403 // flip_queue stores the ids of nodes whose sign must be flipped
404 // flipping signs happens when we do we rewrite (n0 to -n) in
405 // a product like i := (n0^3 * n1). The result is - (n^3*n1) and
406 // we flip the sign of i everywhere.
407 int_queue_t node_queue;
408 int_queue_t flip_queue;
409 } bvc_dag_t;
410
411
412 #define DEF_BVC_DAG_SIZE 500
413 #define MAX_BVC_DAG_SIZE ((UINT32_MAX/sizeof(bvc_item_t)) - 2)
414
415
416 // max len of products and sums allocated in the stores
417 // for larger size, descriptors are allocated using safe_malloc
418 #define PROD_STORE_LEN 2
419 #define SUM_STORE1_LEN 4
420 #define SUM_STORE2_LEN 8
421
422 // list-header indices: three main lists
423 #define BVC_DAG_LEAF_LIST 0
424 #define BVC_DAG_ELEM_LIST (-1)
425 #define BVC_DAG_DEFAULT_LIST (-2)
426 #define BVC_DAG_AUX_LIST (-3)
427
428
429 /*
430 * OPERATIONS
431 */
432
433 /*
434 * Initialize: n = initial size
435 * - if n=0, the default size is used
436 */
437 extern void init_bvc_dag(bvc_dag_t *dag, uint32_t n);
438
439
440 /*
441 * Delete all
442 */
443 extern void delete_bvc_dag(bvc_dag_t *dag);
444
445
446 /*
447 * Empty the DAG
448 */
449 extern void reset_bvc_dag(bvc_dag_t *dag);
450
451
452
453
454 /*
455 * Checks on a node n
456 */
bvc_dag_node_type(bvc_dag_t * dag,bvnode_t n)457 static inline bvc_tag_t bvc_dag_node_type(bvc_dag_t *dag, bvnode_t n) {
458 assert(0 < n && n <= dag->nelems);
459 return dag->desc[n]->tag;
460 }
461
bvc_dag_node_bitsize(bvc_dag_t * dag,bvnode_t n)462 static inline uint32_t bvc_dag_node_bitsize(bvc_dag_t *dag, bvnode_t n) {
463 assert(0 < n && n <= dag->nelems);
464 return dag->desc[n]->bitsize;
465 }
466
bvc_dag_node_is_leaf(bvc_dag_t * dag,bvnode_t n)467 static inline bool bvc_dag_node_is_leaf(bvc_dag_t *dag, bvnode_t n) {
468 assert(0 < n && n <= dag->nelems);
469 return node_is_leaf(dag->desc[n]);
470 }
471
bvc_dag_node_is_zero(bvc_dag_t * dag,bvnode_t n)472 static inline bool bvc_dag_node_is_zero(bvc_dag_t *dag, bvnode_t n) {
473 assert(0 < n && n <= dag->nelems);
474 return node_is_zero(dag->desc[n]);
475 }
476
bvc_dag_node_is_constant(bvc_dag_t * dag,bvnode_t n)477 static inline bool bvc_dag_node_is_constant(bvc_dag_t *dag, bvnode_t n) {
478 assert(0 < n && n <= dag->nelems);
479 return node_is_constant(dag->desc[n]);
480 }
481
bvc_dag_node_is_offset(bvc_dag_t * dag,bvnode_t n)482 static inline bool bvc_dag_node_is_offset(bvc_dag_t *dag, bvnode_t n) {
483 assert(0 < n && n <= dag->nelems);
484 return node_is_offset(dag->desc[n]);
485 }
486
bvc_dag_node_is_mono(bvc_dag_t * dag,bvnode_t n)487 static inline bool bvc_dag_node_is_mono(bvc_dag_t *dag, bvnode_t n) {
488 assert(0 < n && n <= dag->nelems);
489 return node_is_mono(dag->desc[n]);
490 }
491
bvc_dag_node_is_prod(bvc_dag_t * dag,bvnode_t n)492 static inline bool bvc_dag_node_is_prod(bvc_dag_t *dag, bvnode_t n) {
493 assert(0 < n && n <= dag->nelems);
494 return node_is_prod(dag->desc[n]);
495 }
496
bvc_dag_node_is_sum(bvc_dag_t * dag,bvnode_t n)497 static inline bool bvc_dag_node_is_sum(bvc_dag_t *dag, bvnode_t n) {
498 assert(0 < n && n <= dag->nelems);
499 return node_is_sum(dag->desc[n]);
500 }
501
bvc_dag_node_is_alias(bvc_dag_t * dag,bvnode_t n)502 static inline bool bvc_dag_node_is_alias(bvc_dag_t *dag, bvnode_t n) {
503 assert(0 < n && n <= dag->nelems);
504 return node_is_alias(dag->desc[n]);
505 }
506
bvc_dag_node_leaf(bvc_dag_t * dag,bvnode_t n)507 static inline bvc_leaf_t *bvc_dag_node_leaf(bvc_dag_t *dag, bvnode_t n) {
508 assert(0 < n && n <= dag->nelems);
509 return leaf_node(dag->desc[n]);
510 }
511
bvc_dag_node_zero(bvc_dag_t * dag,bvnode_t n)512 static inline bvc_zero_t *bvc_dag_node_zero(bvc_dag_t *dag, bvnode_t n) {
513 assert(0 < n && n <= dag->nelems);
514 return zero_node(dag->desc[n]);
515 }
516
bvc_dag_node_constant(bvc_dag_t * dag,bvnode_t n)517 static inline bvc_constant_t *bvc_dag_node_constant(bvc_dag_t *dag, bvnode_t n) {
518 assert(0 < n && n <= dag->nelems);
519 return bvconst_node(dag->desc[n]);
520 }
521
bvc_dag_node_offset(bvc_dag_t * dag,bvnode_t n)522 static inline bvc_offset_t *bvc_dag_node_offset(bvc_dag_t *dag, bvnode_t n) {
523 assert(0 < n && n <= dag->nelems);
524 return offset_node(dag->desc[n]);
525 }
526
bvc_dag_node_mono(bvc_dag_t * dag,bvnode_t n)527 static inline bvc_mono_t *bvc_dag_node_mono(bvc_dag_t *dag, bvnode_t n) {
528 assert(0 < n && n <= dag->nelems);
529 return mono_node(dag->desc[n]);
530 }
531
bvc_dag_node_prod(bvc_dag_t * dag,bvnode_t n)532 static inline bvc_prod_t *bvc_dag_node_prod(bvc_dag_t *dag, bvnode_t n) {
533 assert(0 < n && n <= dag->nelems);
534 return prod_node(dag->desc[n]);
535 }
536
bvc_dag_node_sum(bvc_dag_t * dag,bvnode_t n)537 static inline bvc_sum_t *bvc_dag_node_sum(bvc_dag_t *dag, bvnode_t n) {
538 assert(0 < n && n <= dag->nelems);
539 return sum_node(dag->desc[n]);
540 }
541
bvc_dag_node_alias(bvc_dag_t * dag,bvnode_t n)542 static inline bvc_alias_t *bvc_dag_node_alias(bvc_dag_t *dag, bvnode_t n) {
543 assert(0 < n && n <= dag->nelems);
544 return alias_node(dag->desc[n]);
545 }
546
547
548 // more checks with n a node_occurrence
bvc_dag_occ_bitsize(bvc_dag_t * dag,node_occ_t n)549 static inline uint32_t bvc_dag_occ_bitsize(bvc_dag_t *dag, node_occ_t n) {
550 return bvc_dag_node_bitsize(dag, node_of_occ(n));
551 }
552
bvc_dag_occ_is_leaf(bvc_dag_t * dag,node_occ_t n)553 static inline bool bvc_dag_occ_is_leaf(bvc_dag_t *dag, node_occ_t n) {
554 return bvc_dag_node_is_leaf(dag, node_of_occ(n));
555 }
556
bvc_dag_occ_is_zero(bvc_dag_t * dag,node_occ_t n)557 static inline bool bvc_dag_occ_is_zero(bvc_dag_t *dag, node_occ_t n) {
558 return bvc_dag_node_is_zero(dag, node_of_occ(n));
559 }
560
bvc_dag_occ_is_constant(bvc_dag_t * dag,node_occ_t n)561 static inline bool bvc_dag_occ_is_constant(bvc_dag_t *dag, node_occ_t n) {
562 return bvc_dag_node_is_constant(dag, node_of_occ(n));
563 }
564
bvc_dag_occ_is_offset(bvc_dag_t * dag,node_occ_t n)565 static inline bool bvc_dag_occ_is_offset(bvc_dag_t *dag, node_occ_t n) {
566 return bvc_dag_node_is_offset(dag, node_of_occ(n));
567 }
568
bvc_dag_occ_is_mono(bvc_dag_t * dag,node_occ_t n)569 static inline bool bvc_dag_occ_is_mono(bvc_dag_t *dag, node_occ_t n) {
570 return bvc_dag_node_is_mono(dag, node_of_occ(n));
571 }
572
bvc_dag_occ_is_prod(bvc_dag_t * dag,node_occ_t n)573 static inline bool bvc_dag_occ_is_prod(bvc_dag_t *dag, node_occ_t n) {
574 return bvc_dag_node_is_prod(dag, node_of_occ(n));
575 }
576
bvc_dag_occ_is_sum(bvc_dag_t * dag,node_occ_t n)577 static inline bool bvc_dag_occ_is_sum(bvc_dag_t *dag, node_occ_t n) {
578 return bvc_dag_node_is_sum(dag, node_of_occ(n));
579 }
580
bvc_dag_occ_is_alias(bvc_dag_t * dag,node_occ_t n)581 static inline bool bvc_dag_occ_is_alias(bvc_dag_t *dag, node_occ_t n) {
582 return bvc_dag_node_is_alias(dag, node_of_occ(n));
583 }
584
585
586 /*
587 * Check whether n is a shared node occurrence
588 * (i.e., +n or -n occur more than once)
589 */
590 extern bool bvc_dag_occ_is_shared(bvc_dag_t *dag, node_occ_t n);
591
592
593
594 /*
595 * MAPPING VARIABLES --> NODES
596 */
597
598 /*
599 * Check whether x is in vset (i.e., there's a node attached to x)
600 */
bvc_dag_var_is_present(bvc_dag_t * dag,int32_t x)601 static inline bool bvc_dag_var_is_present(bvc_dag_t *dag, int32_t x) {
602 assert(x > 0);
603 return int_bvset_member(&dag->vset, x);
604 }
605
606 /*
607 * Store the mapping [x --> n]
608 * - x must be positive
609 * - x must not be mapped already (not in vset)
610 */
611 extern void bvc_dag_map_var(bvc_dag_t *dag, int32_t x, node_occ_t n);
612
613 /*
614 * Get the node occurrence mapped to x
615 */
bvc_dag_nocc_of_var(bvc_dag_t * dag,int32_t x)616 static inline node_occ_t bvc_dag_nocc_of_var(bvc_dag_t *dag, int32_t x) {
617 assert(bvc_dag_var_is_present(dag, x));
618 return int_hmap_find(&dag->vmap, x)->val;
619 }
620
621 /*
622 * Check whether node n was flipped during processing
623 */
624 extern bool bvc_dag_nocc_has_flipped(bvc_dag_t *dag, node_occ_t n);
625
626
627
628 /*
629 * NODE CONSTRUCTION
630 */
631
632 /*
633 * Create a leaf node mapped to x
634 * - x must be positive
635 * - x must not be mapped (i.e., not in dag->vset)
636 * - creates q := [leaf x]
637 * - returns bvp(q)
638 */
639 extern node_occ_t bvc_dag_leaf(bvc_dag_t *dag, int32_t x, uint32_t bitsize);
640
641
642 /*
643 * Get a node mapped to x
644 * - if there isn't one, create a leaf node [leaf x]
645 */
646 extern node_occ_t bvc_dag_get_nocc_of_var(bvc_dag_t *dag, int32_t x, uint32_t bitsize);
647
648
649 /*
650 * Variable of a leaf node-occurrence n
651 */
bvc_dag_get_var_of_leaf(bvc_dag_t * dag,node_occ_t n)652 static inline int32_t bvc_dag_get_var_of_leaf(bvc_dag_t *dag, node_occ_t n) {
653 return bvc_dag_node_leaf(dag, node_of_occ(n))->map;
654 }
655
656
657 /*
658 * Compilation result for node_occurrence n:
659 * - modulo signs, this is the variable of n if n is a leaf node
660 * or the variable of n' if n is aliased to n'
661 * - to encode the signs, we return either bvp(x) or bvn(x)
662 * where x is a variable
663 * bvp(x) means that n is compiled to x
664 * bvn(x) means that n is compiled to (bvneg x)
665 * - in all other cases, the function returns -1
666 */
667 extern int32_t bvc_dag_get_nocc_compilation(bvc_dag_t *dag, node_occ_t n);
668
669
670 /*
671 * Construct a monomial node q
672 * - a must be normalized modulo 2^bitsize
673 * - depending on the coefficient a and the sign of n:
674 * q := [mono a n] and returns bvp(q)
675 * or q := [mono (-a) n] and returns bvn(q)
676 * or q := [mono a (-n)] and returns bvn(q)
677 * or q := [mono (-a) (-n)] and returns bvp(q)
678 *
679 * There are two versions: one for bitsize <= 64, one for bitsize > 64.
680 */
681 extern node_occ_t bvc_dag_mono64(bvc_dag_t *dag, uint64_t a, node_occ_t n, uint32_t bitsize);
682 extern node_occ_t bvc_dag_mono(bvc_dag_t *dag, uint32_t *a, node_occ_t n, uint32_t bitsize);
683
684
685 /*
686 * Construct an offset node q
687 * - a must be normalized modulo 2^bitsize
688 * - this creates q := [offset a n] and returns q
689 * There are two versions: one for bitsize <= 64, one for bitsize > 64.
690 */
691 extern node_occ_t bvc_dag_offset64(bvc_dag_t *dag, uint64_t a, node_occ_t n, uint32_t bitsize);
692 extern node_occ_t bvc_dag_offset(bvc_dag_t *dag, uint32_t *a, node_occ_t n, uint32_t bitsize);
693
694
695
696 /*
697 * Construct a power product node q
698 * - q is defined by the exponents in power product p and the
699 * nodes in array a: if p is x_1^d_1 ... x_k^d_k
700 * then a must have k elements a[0] ... a[k-1]
701 * - if all a[i] are positive, then q is [prod a[0]^d_1 ... a[k-1]^d_k]
702 * - otherwise, signs are adjusted to ensure that all nodes in the product
703 * have positive sign. Then the result q is either the positive or negative
704 * occurrence of the product (depending on the sign of a[i]s and on
705 * whether the exponents are odd or even).
706 */
707 extern node_occ_t bvc_dag_pprod(bvc_dag_t *dag, pprod_t *p, node_occ_t *a, uint32_t bitsize);
708
709
710 /*
711 * Construct a sum node q
712 * - a = array of n node occurrences
713 * - n must be positive
714 *
715 * If n == 1, this returns a[0].
716 * Otherwise, a is sorted and a node q := [sum a[0] ... a[n-1]] is created
717 */
718 extern node_occ_t bvc_dag_sum(bvc_dag_t *dag, node_occ_t *a, uint32_t n, uint32_t bitsize);
719
720
721 /*
722 * Convert a polynomial p to a DAG node q and return q
723 * - q is defined by the coefficients in p and
724 * the node occurrences in array a
725 * - p must be non-zero and non-constant: it's of the
726 * form b_0 x_0 + b_1 x_1 + ... + b_k x_k where k >= 1.
727 * - array a must have k+1 elements a[0] ... a[k]
728 *
729 * If x_0 is const_idx then a[0] is ignored and q is the root node for
730 * (b_0 + b_1 a[1] + ... + b_k a[k]). Otherwise, q is the root node
731 * for (b_0 a[0] + b_1 a[1] + ... + b_k a[k]).
732 */
733 extern node_occ_t bvc_dag_poly64(bvc_dag_t *dag, bvpoly64_t *p, node_occ_t *a);
734 extern node_occ_t bvc_dag_poly(bvc_dag_t *dag, bvpoly_t *p, node_occ_t *a);
735
736
737 /*
738 * Same thing for a polynomial p stored in buffer b
739 * - b must be normalized and non-constant
740 */
741 extern node_occ_t bvc_dag_poly_buffer(bvc_dag_t *dag, bvpoly_buffer_t *b, node_occ_t *a);
742
743
744
745
746 /*
747 * ITERATION THROUGH THE LISTS
748 */
749
750 /*
751 * First node in one of the three node lists (a negative index means that the list is empty)
752 */
bvc_first_leaf(bvc_dag_t * dag)753 static inline bvnode_t bvc_first_leaf(bvc_dag_t *dag) {
754 return dag->list[BVC_DAG_LEAF_LIST].next;
755 }
756
bvc_first_elem_node(bvc_dag_t * dag)757 static inline bvnode_t bvc_first_elem_node(bvc_dag_t *dag) {
758 return dag->list[BVC_DAG_ELEM_LIST].next;
759 }
760
bvc_first_complex_node(bvc_dag_t * dag)761 static inline bvnode_t bvc_first_complex_node(bvc_dag_t *dag) {
762 return dag->list[BVC_DAG_DEFAULT_LIST].next;
763 }
764
765
766 /*
767 * Move node i to the auxiliary list (remove i from the leaf/elem/complex
768 * list first).
769 */
770 extern void bvc_move_node_to_aux_list(bvc_dag_t *dag, bvnode_t i);
771
772 /*
773 * Move the auxiliary list to the elem/complex list
774 */
775 extern void bvc_move_aux_to_elem_list(bvc_dag_t *dag);
776 extern void bvc_move_aux_to_complex_list(bvc_dag_t *dag);
777
778
779
780 /*
781 * Length of each list
782 */
783 extern uint32_t bvc_num_leaves(bvc_dag_t *dag);
784 extern uint32_t bvc_num_elem_nodes(bvc_dag_t *dag);
785 extern uint32_t bvc_num_complex_nodes(bvc_dag_t *dag);
786
787
788
789 /*
790 * REDUCTION
791 */
792
793 /*
794 * Convert node i to a leaf node (for variable x)
795 * - i must not be a leaf or alias node
796 */
797 extern void bvc_dag_convert_to_leaf(bvc_dag_t *dag, bvnode_t i, int32_t x);
798
799
800 /*
801 * Replace all occurrences of {n1, n2} in sums by n
802 * - a node p = [sum ... n1 ... n2 ...] is rewritten to [sum ... n ... ...]
803 * a node p = [sum ... neg(n1) .. neg(n2) ...] is rewritten to [sum ... neg(n) .. ...]
804 */
805 extern void bvc_dag_reduce_sum(bvc_dag_t *dag, node_occ_t n, node_occ_t n1, node_occ_t n2);
806
807
808 /*
809 * Replace all occurrences of {n1, n2} in products by n
810 * - n, n1, and n2 must be positive occurrences
811 */
812 extern void bvc_dag_reduce_prod(bvc_dag_t *dag, node_occ_t n, node_occ_t n1, node_occ_t n2);
813
814
815 /*
816 * Check whether there is a sum node that can be reduced by +n1 +n2 or -n1 -n2
817 */
818 extern bool bvc_dag_check_reduce_sum(bvc_dag_t *dag, node_occ_t n1, node_occ_t n2);
819
820
821 /*
822 * Check whether there's a product node that can be reduced by n1 * n2
823 */
824 extern bool bvc_dag_check_reduce_prod(bvc_dag_t *dag, node_occ_t n1, node_occ_t n2);
825
826
827 /*
828 * Add an elementary node to enable reduction of at least one non-elementary node
829 * - the list of non-elementary node must not be empty
830 */
831 extern void bvc_dag_force_elem_node(bvc_dag_t *dag);
832
833
834 #endif /* __BVPOLY_DAG_H */
835