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