1 /**CFile***********************************************************************
2
3 FileName [cuddCompose.c]
4
5 PackageName [cudd]
6
7 Synopsis [Functional composition and variable permutation of DDs.]
8
9 Description [External procedures included in this module:
10 <ul>
11 <li> Cudd_bddCompose()
12 <li> Cudd_addCompose()
13 <li> Cudd_addPermute()
14 <li> Cudd_addSwapVariables()
15 <li> Cudd_bddPermute()
16 <li> Cudd_bddVarMap()
17 <li> Cudd_SetVarMap()
18 <li> Cudd_bddSwapVariables()
19 <li> Cudd_bddAdjPermuteX()
20 <li> Cudd_addVectorCompose()
21 <li> Cudd_addGeneralVectorCompose()
22 <li> Cudd_addNonSimCompose()
23 <li> Cudd_bddVectorCompose()
24 </ul>
25 Internal procedures included in this module:
26 <ul>
27 <li> cuddBddComposeRecur()
28 <li> cuddAddComposeRecur()
29 </ul>
30 Static procedures included in this module:
31 <ul>
32 <li> cuddAddPermuteRecur()
33 <li> cuddBddPermuteRecur()
34 <li> cuddBddVarMapRecur()
35 <li> cuddAddVectorComposeRecur()
36 <li> cuddAddGeneralVectorComposeRecur()
37 <li> cuddAddNonSimComposeRecur()
38 <li> cuddBddVectorComposeRecur()
39 <li> ddIsIthAddVar()
40 <li> ddIsIthAddVarPair()
41 </ul>
42 The permutation functions use a local cache because the results to
43 be remembered depend on the permutation being applied. Since the
44 permutation is just an array, it cannot be stored in the global
45 cache. There are different procedured for BDDs and ADDs. This is
46 because bddPermuteRecur uses cuddBddIteRecur. If this were changed,
47 the procedures could be merged.]
48
49 Author [Fabio Somenzi and Kavita Ravi]
50
51 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
52
53 All rights reserved.
54
55 Redistribution and use in source and binary forms, with or without
56 modification, are permitted provided that the following conditions
57 are met:
58
59 Redistributions of source code must retain the above copyright
60 notice, this list of conditions and the following disclaimer.
61
62 Redistributions in binary form must reproduce the above copyright
63 notice, this list of conditions and the following disclaimer in the
64 documentation and/or other materials provided with the distribution.
65
66 Neither the name of the University of Colorado nor the names of its
67 contributors may be used to endorse or promote products derived from
68 this software without specific prior written permission.
69
70 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
71 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
72 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
73 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
74 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
75 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
76 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
77 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
78 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
79 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
80 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
81 POSSIBILITY OF SUCH DAMAGE.]
82
83 ******************************************************************************/
84
85 #include "misc/util/util_hack.h"
86 #include "cuddInt.h"
87
88 ABC_NAMESPACE_IMPL_START
89
90
91
92
93 /*---------------------------------------------------------------------------*/
94 /* Constant declarations */
95 /*---------------------------------------------------------------------------*/
96
97 /*---------------------------------------------------------------------------*/
98 /* Stucture declarations */
99 /*---------------------------------------------------------------------------*/
100
101 /*---------------------------------------------------------------------------*/
102 /* Type declarations */
103 /*---------------------------------------------------------------------------*/
104
105 /*---------------------------------------------------------------------------*/
106 /* Variable declarations */
107 /*---------------------------------------------------------------------------*/
108
109 #ifndef lint
110 static char rcsid[] DD_UNUSED = "$Id: cuddCompose.c,v 1.45 2004/08/13 18:04:47 fabio Exp $";
111 #endif
112
113 #ifdef DD_DEBUG
114 static int addPermuteRecurHits;
115 static int bddPermuteRecurHits;
116 static int bddVectorComposeHits;
117 static int addVectorComposeHits;
118
119 static int addGeneralVectorComposeHits;
120 #endif
121
122 /*---------------------------------------------------------------------------*/
123 /* Macro declarations */
124 /*---------------------------------------------------------------------------*/
125
126
127 /**AutomaticStart*************************************************************/
128
129 /*---------------------------------------------------------------------------*/
130 /* Static function prototypes */
131 /*---------------------------------------------------------------------------*/
132
133 static DdNode * cuddAddPermuteRecur (DdManager *manager, DdHashTable *table, DdNode *node, int *permut);
134 static DdNode * cuddBddPermuteRecur (DdManager *manager, DdHashTable *table, DdNode *node, int *permut);
135 static DdNode * cuddBddVarMapRecur (DdManager *manager, DdNode *f);
136 static DdNode * cuddAddVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest);
137 static DdNode * cuddAddNonSimComposeRecur (DdManager *dd, DdNode *f, DdNode **vector, DdNode *key, DdNode *cube, int lastsub);
138 static DdNode * cuddBddVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest);
139 DD_INLINE static int ddIsIthAddVar (DdManager *dd, DdNode *f, unsigned int i);
140
141 static DdNode * cuddAddGeneralVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vectorOn, DdNode **vectorOff, int deepest);
142 DD_INLINE static int ddIsIthAddVarPair (DdManager *dd, DdNode *f, DdNode *g, unsigned int i);
143
144 /**AutomaticEnd***************************************************************/
145
146
147 /*---------------------------------------------------------------------------*/
148 /* Definition of exported functions */
149 /*---------------------------------------------------------------------------*/
150
151
152 /**Function********************************************************************
153
154 Synopsis [Substitutes g for x_v in the BDD for f.]
155
156 Description [Substitutes g for x_v in the BDD for f. v is the index of the
157 variable to be substituted. Cudd_bddCompose passes the corresponding
158 projection function to the recursive procedure, so that the cache may
159 be used. Returns the composed BDD if successful; NULL otherwise.]
160
161 SideEffects [None]
162
163 SeeAlso [Cudd_addCompose]
164
165 ******************************************************************************/
166 DdNode *
Cudd_bddCompose(DdManager * dd,DdNode * f,DdNode * g,int v)167 Cudd_bddCompose(
168 DdManager * dd,
169 DdNode * f,
170 DdNode * g,
171 int v)
172 {
173 DdNode *proj, *res;
174
175 /* Sanity check. */
176 if (v < 0 || v >= dd->size) return(NULL);
177
178 proj = dd->vars[v];
179 do {
180 dd->reordered = 0;
181 res = cuddBddComposeRecur(dd,f,g,proj);
182 } while (dd->reordered == 1);
183 return(res);
184
185 } /* end of Cudd_bddCompose */
186
187
188 /**Function********************************************************************
189
190 Synopsis [Substitutes g for x_v in the ADD for f.]
191
192 Description [Substitutes g for x_v in the ADD for f. v is the index of the
193 variable to be substituted. g must be a 0-1 ADD. Cudd_bddCompose passes
194 the corresponding projection function to the recursive procedure, so
195 that the cache may be used. Returns the composed ADD if successful;
196 NULL otherwise.]
197
198 SideEffects [None]
199
200 SeeAlso [Cudd_bddCompose]
201
202 ******************************************************************************/
203 DdNode *
Cudd_addCompose(DdManager * dd,DdNode * f,DdNode * g,int v)204 Cudd_addCompose(
205 DdManager * dd,
206 DdNode * f,
207 DdNode * g,
208 int v)
209 {
210 DdNode *proj, *res;
211
212 /* Sanity check. */
213 if (v < 0 || v >= dd->size) return(NULL);
214
215 proj = dd->vars[v];
216 do {
217 dd->reordered = 0;
218 res = cuddAddComposeRecur(dd,f,g,proj);
219 } while (dd->reordered == 1);
220 return(res);
221
222 } /* end of Cudd_addCompose */
223
224
225 /**Function********************************************************************
226
227 Synopsis [Permutes the variables of an ADD.]
228
229 Description [Given a permutation in array permut, creates a new ADD
230 with permuted variables. There should be an entry in array permut
231 for each variable in the manager. The i-th entry of permut holds the
232 index of the variable that is to substitute the i-th
233 variable. Returns a pointer to the resulting ADD if successful; NULL
234 otherwise.]
235
236 SideEffects [None]
237
238 SeeAlso [Cudd_bddPermute Cudd_addSwapVariables]
239
240 ******************************************************************************/
241 DdNode *
Cudd_addPermute(DdManager * manager,DdNode * node,int * permut)242 Cudd_addPermute(
243 DdManager * manager,
244 DdNode * node,
245 int * permut)
246 {
247 DdHashTable *table;
248 DdNode *res;
249
250 do {
251 manager->reordered = 0;
252 table = cuddHashTableInit(manager,1,2);
253 if (table == NULL) return(NULL);
254 /* Recursively solve the problem. */
255 res = cuddAddPermuteRecur(manager,table,node,permut);
256 if (res != NULL) cuddRef(res);
257 /* Dispose of local cache. */
258 cuddHashTableQuit(table);
259 } while (manager->reordered == 1);
260
261 if (res != NULL) cuddDeref(res);
262 return(res);
263
264 } /* end of Cudd_addPermute */
265
266
267 /**Function********************************************************************
268
269 Synopsis [Swaps two sets of variables of the same size (x and y) in
270 the ADD f.]
271
272 Description [Swaps two sets of variables of the same size (x and y) in
273 the ADD f. The size is given by n. The two sets of variables are
274 assumed to be disjoint. Returns a pointer to the resulting ADD if
275 successful; NULL otherwise.]
276
277 SideEffects [None]
278
279 SeeAlso [Cudd_addPermute Cudd_bddSwapVariables]
280
281 ******************************************************************************/
282 DdNode *
Cudd_addSwapVariables(DdManager * dd,DdNode * f,DdNode ** x,DdNode ** y,int n)283 Cudd_addSwapVariables(
284 DdManager * dd,
285 DdNode * f,
286 DdNode ** x,
287 DdNode ** y,
288 int n)
289 {
290 DdNode *swapped;
291 int i, j, k;
292 int *permut;
293
294 permut = ABC_ALLOC(int,dd->size);
295 if (permut == NULL) {
296 dd->errorCode = CUDD_MEMORY_OUT;
297 return(NULL);
298 }
299 for (i = 0; i < dd->size; i++) permut[i] = i;
300 for (i = 0; i < n; i++) {
301 j = x[i]->index;
302 k = y[i]->index;
303 permut[j] = k;
304 permut[k] = j;
305 }
306
307 swapped = Cudd_addPermute(dd,f,permut);
308 ABC_FREE(permut);
309
310 return(swapped);
311
312 } /* end of Cudd_addSwapVariables */
313
314
315 /**Function********************************************************************
316
317 Synopsis [Permutes the variables of a BDD.]
318
319 Description [Given a permutation in array permut, creates a new BDD
320 with permuted variables. There should be an entry in array permut
321 for each variable in the manager. The i-th entry of permut holds the
322 index of the variable that is to substitute the i-th variable.
323 Returns a pointer to the resulting BDD if successful; NULL
324 otherwise.]
325
326 SideEffects [None]
327
328 SeeAlso [Cudd_addPermute Cudd_bddSwapVariables]
329
330 ******************************************************************************/
331 DdNode *
Cudd_bddPermute(DdManager * manager,DdNode * node,int * permut)332 Cudd_bddPermute(
333 DdManager * manager,
334 DdNode * node,
335 int * permut)
336 {
337 DdHashTable *table;
338 DdNode *res;
339
340 do {
341 manager->reordered = 0;
342 table = cuddHashTableInit(manager,1,2);
343 if (table == NULL) return(NULL);
344 res = cuddBddPermuteRecur(manager,table,node,permut);
345 if (res != NULL) cuddRef(res);
346 /* Dispose of local cache. */
347 cuddHashTableQuit(table);
348
349 } while (manager->reordered == 1);
350
351 if (res != NULL) cuddDeref(res);
352 return(res);
353
354 } /* end of Cudd_bddPermute */
355
356
357 /**Function********************************************************************
358
359 Synopsis [Remaps the variables of a BDD using the default variable map.]
360
361 Description [Remaps the variables of a BDD using the default
362 variable map. A typical use of this function is to swap two sets of
363 variables. The variable map must be registered with Cudd_SetVarMap.
364 Returns a pointer to the resulting BDD if successful; NULL
365 otherwise.]
366
367 SideEffects [None]
368
369 SeeAlso [Cudd_bddPermute Cudd_bddSwapVariables Cudd_SetVarMap]
370
371 ******************************************************************************/
372 DdNode *
Cudd_bddVarMap(DdManager * manager,DdNode * f)373 Cudd_bddVarMap(
374 DdManager * manager /* DD manager */,
375 DdNode * f /* function in which to remap variables */)
376 {
377 DdNode *res;
378
379 if (manager->map == NULL) return(NULL);
380 do {
381 manager->reordered = 0;
382 res = cuddBddVarMapRecur(manager, f);
383 } while (manager->reordered == 1);
384
385 return(res);
386
387 } /* end of Cudd_bddVarMap */
388
389
390 /**Function********************************************************************
391
392 Synopsis [Registers a variable mapping with the manager.]
393
394 Description [Registers with the manager a variable mapping described
395 by two sets of variables. This variable mapping is then used by
396 functions like Cudd_bddVarMap. This function is convenient for
397 those applications that perform the same mapping several times.
398 However, if several different permutations are used, it may be more
399 efficient not to rely on the registered mapping, because changing
400 mapping causes the cache to be cleared. (The initial setting,
401 however, does not clear the cache.) The two sets of variables (x and
402 y) must have the same size (x and y). The size is given by n. The
403 two sets of variables are normally disjoint, but this restriction is
404 not imposeded by the function. When new variables are created, the
405 map is automatically extended (each new variable maps to
406 itself). The typical use, however, is to wait until all variables
407 are created, and then create the map. Returns 1 if the mapping is
408 successfully registered with the manager; 0 otherwise.]
409
410 SideEffects [Modifies the manager. May clear the cache.]
411
412 SeeAlso [Cudd_bddVarMap Cudd_bddPermute Cudd_bddSwapVariables]
413
414 ******************************************************************************/
415 int
Cudd_SetVarMap(DdManager * manager,DdNode ** x,DdNode ** y,int n)416 Cudd_SetVarMap (
417 DdManager *manager /* DD manager */,
418 DdNode **x /* first array of variables */,
419 DdNode **y /* second array of variables */,
420 int n /* length of both arrays */)
421 {
422 int i;
423
424 if (manager->map != NULL) {
425 cuddCacheFlush(manager);
426 } else {
427 manager->map = ABC_ALLOC(int,manager->maxSize);
428 if (manager->map == NULL) {
429 manager->errorCode = CUDD_MEMORY_OUT;
430 return(0);
431 }
432 manager->memused += sizeof(int) * manager->maxSize;
433 }
434 /* Initialize the map to the identity. */
435 for (i = 0; i < manager->size; i++) {
436 manager->map[i] = i;
437 }
438 /* Create the map. */
439 for (i = 0; i < n; i++) {
440 manager->map[x[i]->index] = y[i]->index;
441 manager->map[y[i]->index] = x[i]->index;
442 }
443 return(1);
444
445 } /* end of Cudd_SetVarMap */
446
447
448 /**Function********************************************************************
449
450 Synopsis [Swaps two sets of variables of the same size (x and y) in
451 the BDD f.]
452
453 Description [Swaps two sets of variables of the same size (x and y)
454 in the BDD f. The size is given by n. The two sets of variables are
455 assumed to be disjoint. Returns a pointer to the resulting BDD if
456 successful; NULL otherwise.]
457
458 SideEffects [None]
459
460 SeeAlso [Cudd_bddPermute Cudd_addSwapVariables]
461
462 ******************************************************************************/
463 DdNode *
Cudd_bddSwapVariables(DdManager * dd,DdNode * f,DdNode ** x,DdNode ** y,int n)464 Cudd_bddSwapVariables(
465 DdManager * dd,
466 DdNode * f,
467 DdNode ** x,
468 DdNode ** y,
469 int n)
470 {
471 DdNode *swapped;
472 int i, j, k;
473 int *permut;
474
475 permut = ABC_ALLOC(int,dd->size);
476 if (permut == NULL) {
477 dd->errorCode = CUDD_MEMORY_OUT;
478 return(NULL);
479 }
480 for (i = 0; i < dd->size; i++) permut[i] = i;
481 for (i = 0; i < n; i++) {
482 j = x[i]->index;
483 k = y[i]->index;
484 permut[j] = k;
485 permut[k] = j;
486 }
487
488 swapped = Cudd_bddPermute(dd,f,permut);
489 ABC_FREE(permut);
490
491 return(swapped);
492
493 } /* end of Cudd_bddSwapVariables */
494
495
496 /**Function********************************************************************
497
498 Synopsis [Rearranges a set of variables in the BDD B.]
499
500 Description [Rearranges a set of variables in the BDD B. The size of
501 the set is given by n. This procedure is intended for the
502 `randomization' of the priority functions. Returns a pointer to the
503 BDD if successful; NULL otherwise.]
504
505 SideEffects [None]
506
507 SeeAlso [Cudd_bddPermute Cudd_bddSwapVariables
508 Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_PrioritySelect]
509
510 ******************************************************************************/
511 DdNode *
Cudd_bddAdjPermuteX(DdManager * dd,DdNode * B,DdNode ** x,int n)512 Cudd_bddAdjPermuteX(
513 DdManager * dd,
514 DdNode * B,
515 DdNode ** x,
516 int n)
517 {
518 DdNode *swapped;
519 int i, j, k;
520 int *permut;
521
522 permut = ABC_ALLOC(int,dd->size);
523 if (permut == NULL) {
524 dd->errorCode = CUDD_MEMORY_OUT;
525 return(NULL);
526 }
527 for (i = 0; i < dd->size; i++) permut[i] = i;
528 for (i = 0; i < n-2; i += 3) {
529 j = x[i]->index;
530 k = x[i+1]->index;
531 permut[j] = k;
532 permut[k] = j;
533 }
534
535 swapped = Cudd_bddPermute(dd,B,permut);
536 ABC_FREE(permut);
537
538 return(swapped);
539
540 } /* end of Cudd_bddAdjPermuteX */
541
542
543 /**Function********************************************************************
544
545 Synopsis [Composes an ADD with a vector of 0-1 ADDs.]
546
547 Description [Given a vector of 0-1 ADDs, creates a new ADD by
548 substituting the 0-1 ADDs for the variables of the ADD f. There
549 should be an entry in vector for each variable in the manager.
550 If no substitution is sought for a given variable, the corresponding
551 projection function should be specified in the vector.
552 This function implements simultaneous composition.
553 Returns a pointer to the resulting ADD if successful; NULL
554 otherwise.]
555
556 SideEffects [None]
557
558 SeeAlso [Cudd_addNonSimCompose Cudd_addPermute Cudd_addCompose
559 Cudd_bddVectorCompose]
560
561 ******************************************************************************/
562 DdNode *
Cudd_addVectorCompose(DdManager * dd,DdNode * f,DdNode ** vector)563 Cudd_addVectorCompose(
564 DdManager * dd,
565 DdNode * f,
566 DdNode ** vector)
567 {
568 DdHashTable *table;
569 DdNode *res;
570 int deepest;
571 int i;
572
573 do {
574 dd->reordered = 0;
575 /* Initialize local cache. */
576 table = cuddHashTableInit(dd,1,2);
577 if (table == NULL) return(NULL);
578
579 /* Find deepest real substitution. */
580 for (deepest = dd->size - 1; deepest >= 0; deepest--) {
581 i = dd->invperm[deepest];
582 if (!ddIsIthAddVar(dd,vector[i],i)) {
583 break;
584 }
585 }
586
587 /* Recursively solve the problem. */
588 res = cuddAddVectorComposeRecur(dd,table,f,vector,deepest);
589 if (res != NULL) cuddRef(res);
590
591 /* Dispose of local cache. */
592 cuddHashTableQuit(table);
593 } while (dd->reordered == 1);
594
595 if (res != NULL) cuddDeref(res);
596 return(res);
597
598 } /* end of Cudd_addVectorCompose */
599
600
601 /**Function********************************************************************
602
603 Synopsis [Composes an ADD with a vector of ADDs.]
604
605 Description [Given a vector of ADDs, creates a new ADD by substituting the
606 ADDs for the variables of the ADD f. vectorOn contains ADDs to be substituted
607 for the x_v and vectorOff the ADDs to be substituted for x_v'. There should
608 be an entry in vector for each variable in the manager. If no substitution
609 is sought for a given variable, the corresponding projection function should
610 be specified in the vector. This function implements simultaneous
611 composition. Returns a pointer to the resulting ADD if successful; NULL
612 otherwise.]
613
614 SideEffects [None]
615
616 SeeAlso [Cudd_addVectorCompose Cudd_addNonSimCompose Cudd_addPermute
617 Cudd_addCompose Cudd_bddVectorCompose]
618
619 ******************************************************************************/
620 DdNode *
Cudd_addGeneralVectorCompose(DdManager * dd,DdNode * f,DdNode ** vectorOn,DdNode ** vectorOff)621 Cudd_addGeneralVectorCompose(
622 DdManager * dd,
623 DdNode * f,
624 DdNode ** vectorOn,
625 DdNode ** vectorOff)
626 {
627 DdHashTable *table;
628 DdNode *res;
629 int deepest;
630 int i;
631
632 do {
633 dd->reordered = 0;
634 /* Initialize local cache. */
635 table = cuddHashTableInit(dd,1,2);
636 if (table == NULL) return(NULL);
637
638 /* Find deepest real substitution. */
639 for (deepest = dd->size - 1; deepest >= 0; deepest--) {
640 i = dd->invperm[deepest];
641 if (!ddIsIthAddVarPair(dd,vectorOn[i],vectorOff[i],i)) {
642 break;
643 }
644 }
645
646 /* Recursively solve the problem. */
647 res = cuddAddGeneralVectorComposeRecur(dd,table,f,vectorOn,
648 vectorOff,deepest);
649 if (res != NULL) cuddRef(res);
650
651 /* Dispose of local cache. */
652 cuddHashTableQuit(table);
653 } while (dd->reordered == 1);
654
655 if (res != NULL) cuddDeref(res);
656 return(res);
657
658 } /* end of Cudd_addGeneralVectorCompose */
659
660
661 /**Function********************************************************************
662
663 Synopsis [Composes an ADD with a vector of 0-1 ADDs.]
664
665 Description [Given a vector of 0-1 ADDs, creates a new ADD by
666 substituting the 0-1 ADDs for the variables of the ADD f. There
667 should be an entry in vector for each variable in the manager.
668 This function implements non-simultaneous composition. If any of the
669 functions being composed depends on any of the variables being
670 substituted, then the result depends on the order of composition,
671 which in turn depends on the variable order: The variables farther from
672 the roots in the order are substituted first.
673 Returns a pointer to the resulting ADD if successful; NULL
674 otherwise.]
675
676 SideEffects [None]
677
678 SeeAlso [Cudd_addVectorCompose Cudd_addPermute Cudd_addCompose]
679
680 ******************************************************************************/
681 DdNode *
Cudd_addNonSimCompose(DdManager * dd,DdNode * f,DdNode ** vector)682 Cudd_addNonSimCompose(
683 DdManager * dd,
684 DdNode * f,
685 DdNode ** vector)
686 {
687 DdNode *cube, *key, *var, *tmp, *piece;
688 DdNode *res;
689 int i, lastsub;
690
691 /* The cache entry for this function is composed of three parts:
692 ** f itself, the replacement relation, and the cube of the
693 ** variables being substituted.
694 ** The replacement relation is the product of the terms (yi EXNOR gi).
695 ** This apporach allows us to use the global cache for this function,
696 ** with great savings in memory with respect to using arrays for the
697 ** cache entries.
698 ** First we build replacement relation and cube of substituted
699 ** variables from the vector specifying the desired composition.
700 */
701 key = DD_ONE(dd);
702 cuddRef(key);
703 cube = DD_ONE(dd);
704 cuddRef(cube);
705 for (i = (int) dd->size - 1; i >= 0; i--) {
706 if (ddIsIthAddVar(dd,vector[i],(unsigned int)i)) {
707 continue;
708 }
709 var = Cudd_addIthVar(dd,i);
710 if (var == NULL) {
711 Cudd_RecursiveDeref(dd,key);
712 Cudd_RecursiveDeref(dd,cube);
713 return(NULL);
714 }
715 cuddRef(var);
716 /* Update cube. */
717 tmp = Cudd_addApply(dd,Cudd_addTimes,var,cube);
718 if (tmp == NULL) {
719 Cudd_RecursiveDeref(dd,key);
720 Cudd_RecursiveDeref(dd,cube);
721 Cudd_RecursiveDeref(dd,var);
722 return(NULL);
723 }
724 cuddRef(tmp);
725 Cudd_RecursiveDeref(dd,cube);
726 cube = tmp;
727 /* Update replacement relation. */
728 piece = Cudd_addApply(dd,Cudd_addXnor,var,vector[i]);
729 if (piece == NULL) {
730 Cudd_RecursiveDeref(dd,key);
731 Cudd_RecursiveDeref(dd,var);
732 return(NULL);
733 }
734 cuddRef(piece);
735 Cudd_RecursiveDeref(dd,var);
736 tmp = Cudd_addApply(dd,Cudd_addTimes,key,piece);
737 if (tmp == NULL) {
738 Cudd_RecursiveDeref(dd,key);
739 Cudd_RecursiveDeref(dd,piece);
740 return(NULL);
741 }
742 cuddRef(tmp);
743 Cudd_RecursiveDeref(dd,key);
744 Cudd_RecursiveDeref(dd,piece);
745 key = tmp;
746 }
747
748 /* Now try composition, until no reordering occurs. */
749 do {
750 /* Find real substitution with largest index. */
751 for (lastsub = dd->size - 1; lastsub >= 0; lastsub--) {
752 if (!ddIsIthAddVar(dd,vector[lastsub],(unsigned int)lastsub)) {
753 break;
754 }
755 }
756
757 /* Recursively solve the problem. */
758 dd->reordered = 0;
759 res = cuddAddNonSimComposeRecur(dd,f,vector,key,cube,lastsub+1);
760 if (res != NULL) cuddRef(res);
761
762 } while (dd->reordered == 1);
763
764 Cudd_RecursiveDeref(dd,key);
765 Cudd_RecursiveDeref(dd,cube);
766 if (res != NULL) cuddDeref(res);
767 return(res);
768
769 } /* end of Cudd_addNonSimCompose */
770
771
772 /**Function********************************************************************
773
774 Synopsis [Composes a BDD with a vector of BDDs.]
775
776 Description [Given a vector of BDDs, creates a new BDD by
777 substituting the BDDs for the variables of the BDD f. There
778 should be an entry in vector for each variable in the manager.
779 If no substitution is sought for a given variable, the corresponding
780 projection function should be specified in the vector.
781 This function implements simultaneous composition.
782 Returns a pointer to the resulting BDD if successful; NULL
783 otherwise.]
784
785 SideEffects [None]
786
787 SeeAlso [Cudd_bddPermute Cudd_bddCompose Cudd_addVectorCompose]
788
789 ******************************************************************************/
790 DdNode *
Cudd_bddVectorCompose(DdManager * dd,DdNode * f,DdNode ** vector)791 Cudd_bddVectorCompose(
792 DdManager * dd,
793 DdNode * f,
794 DdNode ** vector)
795 {
796 DdHashTable *table;
797 DdNode *res;
798 int deepest;
799 int i;
800
801 do {
802 dd->reordered = 0;
803 /* Initialize local cache. */
804 table = cuddHashTableInit(dd,1,2);
805 if (table == NULL) return(NULL);
806
807 /* Find deepest real substitution. */
808 for (deepest = dd->size - 1; deepest >= 0; deepest--) {
809 i = dd->invperm[deepest];
810 if (vector[i] != dd->vars[i]) {
811 break;
812 }
813 }
814
815 /* Recursively solve the problem. */
816 res = cuddBddVectorComposeRecur(dd,table,f,vector, deepest);
817 if (res != NULL) cuddRef(res);
818
819 /* Dispose of local cache. */
820 cuddHashTableQuit(table);
821 } while (dd->reordered == 1);
822
823 if (res != NULL) cuddDeref(res);
824 return(res);
825
826 } /* end of Cudd_bddVectorCompose */
827
828
829 /*---------------------------------------------------------------------------*/
830 /* Definition of internal functions */
831 /*---------------------------------------------------------------------------*/
832
833
834 /**Function********************************************************************
835
836 Synopsis [Performs the recursive step of Cudd_bddCompose.]
837
838 Description [Performs the recursive step of Cudd_bddCompose.
839 Exploits the fact that the composition of f' with g
840 produces the complement of the composition of f with g to better
841 utilize the cache. Returns the composed BDD if successful; NULL
842 otherwise.]
843
844 SideEffects [None]
845
846 SeeAlso [Cudd_bddCompose]
847
848 ******************************************************************************/
849 DdNode *
cuddBddComposeRecur(DdManager * dd,DdNode * f,DdNode * g,DdNode * proj)850 cuddBddComposeRecur(
851 DdManager * dd,
852 DdNode * f,
853 DdNode * g,
854 DdNode * proj)
855 {
856 DdNode *F, *G, *f1, *f0, *g1, *g0, *r, *t, *e;
857 unsigned int v, topf, topg, topindex;
858 int comple;
859
860 statLine(dd);
861 v = dd->perm[proj->index];
862 F = Cudd_Regular(f);
863 topf = cuddI(dd,F->index);
864
865 /* Terminal case. Subsumes the test for constant f. */
866 if (topf > v) return(f);
867
868 /* We solve the problem for a regular pointer, and then complement
869 ** the result if the pointer was originally complemented.
870 */
871 comple = Cudd_IsComplement(f);
872
873 /* Check cache. */
874 r = cuddCacheLookup(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj);
875 if (r != NULL) {
876 return(Cudd_NotCond(r,comple));
877 }
878
879 if (topf == v) {
880 /* Compose. */
881 f1 = cuddT(F);
882 f0 = cuddE(F);
883 r = cuddBddIteRecur(dd, g, f1, f0);
884 if (r == NULL) return(NULL);
885 } else {
886 /* Compute cofactors of f and g. Remember the index of the top
887 ** variable.
888 */
889 G = Cudd_Regular(g);
890 topg = cuddI(dd,G->index);
891 if (topf > topg) {
892 topindex = G->index;
893 f1 = f0 = F;
894 } else {
895 topindex = F->index;
896 f1 = cuddT(F);
897 f0 = cuddE(F);
898 }
899 if (topg > topf) {
900 g1 = g0 = g;
901 } else {
902 g1 = cuddT(G);
903 g0 = cuddE(G);
904 if (g != G) {
905 g1 = Cudd_Not(g1);
906 g0 = Cudd_Not(g0);
907 }
908 }
909 /* Recursive step. */
910 t = cuddBddComposeRecur(dd, f1, g1, proj);
911 if (t == NULL) return(NULL);
912 cuddRef(t);
913 e = cuddBddComposeRecur(dd, f0, g0, proj);
914 if (e == NULL) {
915 Cudd_IterDerefBdd(dd, t);
916 return(NULL);
917 }
918 cuddRef(e);
919
920 r = cuddBddIteRecur(dd, dd->vars[topindex], t, e);
921 if (r == NULL) {
922 Cudd_IterDerefBdd(dd, t);
923 Cudd_IterDerefBdd(dd, e);
924 return(NULL);
925 }
926 cuddRef(r);
927 Cudd_IterDerefBdd(dd, t); /* t & e not necessarily part of r */
928 Cudd_IterDerefBdd(dd, e);
929 cuddDeref(r);
930 }
931
932 cuddCacheInsert(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj,r);
933
934 return(Cudd_NotCond(r,comple));
935
936 } /* end of cuddBddComposeRecur */
937
938
939 /**Function********************************************************************
940
941 Synopsis [Performs the recursive step of Cudd_addCompose.]
942
943 Description [Performs the recursive step of Cudd_addCompose.
944 Returns the composed BDD if successful; NULL otherwise.]
945
946 SideEffects [None]
947
948 SeeAlso [Cudd_addCompose]
949
950 ******************************************************************************/
951 DdNode *
cuddAddComposeRecur(DdManager * dd,DdNode * f,DdNode * g,DdNode * proj)952 cuddAddComposeRecur(
953 DdManager * dd,
954 DdNode * f,
955 DdNode * g,
956 DdNode * proj)
957 {
958 DdNode *f1, *f0, *g1, *g0, *r, *t, *e;
959 unsigned int v, topf, topg, topindex;
960
961 statLine(dd);
962 v = dd->perm[proj->index];
963 topf = cuddI(dd,f->index);
964
965 /* Terminal case. Subsumes the test for constant f. */
966 if (topf > v) return(f);
967
968 /* Check cache. */
969 r = cuddCacheLookup(dd,DD_ADD_COMPOSE_RECUR_TAG,f,g,proj);
970 if (r != NULL) {
971 return(r);
972 }
973
974 if (topf == v) {
975 /* Compose. */
976 f1 = cuddT(f);
977 f0 = cuddE(f);
978 r = cuddAddIteRecur(dd, g, f1, f0);
979 if (r == NULL) return(NULL);
980 } else {
981 /* Compute cofactors of f and g. Remember the index of the top
982 ** variable.
983 */
984 topg = cuddI(dd,g->index);
985 if (topf > topg) {
986 topindex = g->index;
987 f1 = f0 = f;
988 } else {
989 topindex = f->index;
990 f1 = cuddT(f);
991 f0 = cuddE(f);
992 }
993 if (topg > topf) {
994 g1 = g0 = g;
995 } else {
996 g1 = cuddT(g);
997 g0 = cuddE(g);
998 }
999 /* Recursive step. */
1000 t = cuddAddComposeRecur(dd, f1, g1, proj);
1001 if (t == NULL) return(NULL);
1002 cuddRef(t);
1003 e = cuddAddComposeRecur(dd, f0, g0, proj);
1004 if (e == NULL) {
1005 Cudd_RecursiveDeref(dd, t);
1006 return(NULL);
1007 }
1008 cuddRef(e);
1009
1010 if (t == e) {
1011 r = t;
1012 } else {
1013 r = cuddUniqueInter(dd, (int) topindex, t, e);
1014 if (r == NULL) {
1015 Cudd_RecursiveDeref(dd, t);
1016 Cudd_RecursiveDeref(dd, e);
1017 return(NULL);
1018 }
1019 }
1020 cuddDeref(t);
1021 cuddDeref(e);
1022 }
1023
1024 cuddCacheInsert(dd,DD_ADD_COMPOSE_RECUR_TAG,f,g,proj,r);
1025
1026 return(r);
1027
1028 } /* end of cuddAddComposeRecur */
1029
1030
1031 /*---------------------------------------------------------------------------*/
1032 /* Definition of static functions */
1033 /*---------------------------------------------------------------------------*/
1034
1035
1036 /**Function********************************************************************
1037
1038 Synopsis [Implements the recursive step of Cudd_addPermute.]
1039
1040 Description [ Recursively puts the ADD in the order given in the
1041 array permut. Checks for trivial cases to terminate recursion, then
1042 splits on the children of this node. Once the solutions for the
1043 children are obtained, it puts into the current position the node
1044 from the rest of the ADD that should be here. Then returns this ADD.
1045 The key here is that the node being visited is NOT put in its proper
1046 place by this instance, but rather is switched when its proper
1047 position is reached in the recursion tree.<p>
1048 The DdNode * that is returned is the same ADD as passed in as node,
1049 but in the new order.]
1050
1051 SideEffects [None]
1052
1053 SeeAlso [Cudd_addPermute cuddBddPermuteRecur]
1054
1055 ******************************************************************************/
1056 static DdNode *
cuddAddPermuteRecur(DdManager * manager,DdHashTable * table,DdNode * node,int * permut)1057 cuddAddPermuteRecur(
1058 DdManager * manager /* DD manager */,
1059 DdHashTable * table /* computed table */,
1060 DdNode * node /* ADD to be reordered */,
1061 int * permut /* permutation array */)
1062 {
1063 DdNode *T,*E;
1064 DdNode *res,*var;
1065 int index;
1066
1067 statLine(manager);
1068 /* Check for terminal case of constant node. */
1069 if (cuddIsConstant(node)) {
1070 return(node);
1071 }
1072
1073 /* If problem already solved, look up answer and return. */
1074 if (node->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) {
1075 #ifdef DD_DEBUG
1076 addPermuteRecurHits++;
1077 #endif
1078 return(res);
1079 }
1080
1081 /* Split and recur on children of this node. */
1082 T = cuddAddPermuteRecur(manager,table,cuddT(node),permut);
1083 if (T == NULL) return(NULL);
1084 cuddRef(T);
1085 E = cuddAddPermuteRecur(manager,table,cuddE(node),permut);
1086 if (E == NULL) {
1087 Cudd_RecursiveDeref(manager, T);
1088 return(NULL);
1089 }
1090 cuddRef(E);
1091
1092 /* Move variable that should be in this position to this position
1093 ** by creating a single var ADD for that variable, and calling
1094 ** cuddAddIteRecur with the T and E we just created.
1095 */
1096 index = permut[node->index];
1097 var = cuddUniqueInter(manager,index,DD_ONE(manager),DD_ZERO(manager));
1098 if (var == NULL) return(NULL);
1099 cuddRef(var);
1100 res = cuddAddIteRecur(manager,var,T,E);
1101 if (res == NULL) {
1102 Cudd_RecursiveDeref(manager,var);
1103 Cudd_RecursiveDeref(manager, T);
1104 Cudd_RecursiveDeref(manager, E);
1105 return(NULL);
1106 }
1107 cuddRef(res);
1108 Cudd_RecursiveDeref(manager,var);
1109 Cudd_RecursiveDeref(manager, T);
1110 Cudd_RecursiveDeref(manager, E);
1111
1112 /* Do not keep the result if the reference count is only 1, since
1113 ** it will not be visited again.
1114 */
1115 if (node->ref != 1) {
1116 ptrint fanout = (ptrint) node->ref;
1117 cuddSatDec(fanout);
1118 if (!cuddHashTableInsert1(table,node,res,fanout)) {
1119 Cudd_RecursiveDeref(manager, res);
1120 return(NULL);
1121 }
1122 }
1123 cuddDeref(res);
1124 return(res);
1125
1126 } /* end of cuddAddPermuteRecur */
1127
1128
1129 /**Function********************************************************************
1130
1131 Synopsis [Implements the recursive step of Cudd_bddPermute.]
1132
1133 Description [ Recursively puts the BDD in the order given in the array permut.
1134 Checks for trivial cases to terminate recursion, then splits on the
1135 children of this node. Once the solutions for the children are
1136 obtained, it puts into the current position the node from the rest of
1137 the BDD that should be here. Then returns this BDD.
1138 The key here is that the node being visited is NOT put in its proper
1139 place by this instance, but rather is switched when its proper position
1140 is reached in the recursion tree.<p>
1141 The DdNode * that is returned is the same BDD as passed in as node,
1142 but in the new order.]
1143
1144 SideEffects [None]
1145
1146 SeeAlso [Cudd_bddPermute cuddAddPermuteRecur]
1147
1148 ******************************************************************************/
1149 static DdNode *
cuddBddPermuteRecur(DdManager * manager,DdHashTable * table,DdNode * node,int * permut)1150 cuddBddPermuteRecur(
1151 DdManager * manager /* DD manager */,
1152 DdHashTable * table /* computed table */,
1153 DdNode * node /* BDD to be reordered */,
1154 int * permut /* permutation array */)
1155 {
1156 DdNode *N,*T,*E;
1157 DdNode *res;
1158 int index;
1159
1160 statLine(manager);
1161 N = Cudd_Regular(node);
1162
1163 /* Check for terminal case of constant node. */
1164 if (cuddIsConstant(N)) {
1165 return(node);
1166 }
1167
1168 /* If problem already solved, look up answer and return. */
1169 if (N->ref != 1 && (res = cuddHashTableLookup1(table,N)) != NULL) {
1170 #ifdef DD_DEBUG
1171 bddPermuteRecurHits++;
1172 #endif
1173 return(Cudd_NotCond(res,N != node));
1174 }
1175
1176 /* Split and recur on children of this node. */
1177 T = cuddBddPermuteRecur(manager,table,cuddT(N),permut);
1178 if (T == NULL) return(NULL);
1179 cuddRef(T);
1180 E = cuddBddPermuteRecur(manager,table,cuddE(N),permut);
1181 if (E == NULL) {
1182 Cudd_IterDerefBdd(manager, T);
1183 return(NULL);
1184 }
1185 cuddRef(E);
1186
1187 /* Move variable that should be in this position to this position
1188 ** by retrieving the single var BDD for that variable, and calling
1189 ** cuddBddIteRecur with the T and E we just created.
1190 */
1191 index = permut[N->index];
1192 res = cuddBddIteRecur(manager,manager->vars[index],T,E);
1193 if (res == NULL) {
1194 Cudd_IterDerefBdd(manager, T);
1195 Cudd_IterDerefBdd(manager, E);
1196 return(NULL);
1197 }
1198 cuddRef(res);
1199 Cudd_IterDerefBdd(manager, T);
1200 Cudd_IterDerefBdd(manager, E);
1201
1202 /* Do not keep the result if the reference count is only 1, since
1203 ** it will not be visited again.
1204 */
1205 if (N->ref != 1) {
1206 ptrint fanout = (ptrint) N->ref;
1207 cuddSatDec(fanout);
1208 if (!cuddHashTableInsert1(table,N,res,fanout)) {
1209 Cudd_IterDerefBdd(manager, res);
1210 return(NULL);
1211 }
1212 }
1213 cuddDeref(res);
1214 return(Cudd_NotCond(res,N != node));
1215
1216 } /* end of cuddBddPermuteRecur */
1217
1218
1219 /**Function********************************************************************
1220
1221 Synopsis [Implements the recursive step of Cudd_bddVarMap.]
1222
1223 Description [Implements the recursive step of Cudd_bddVarMap.
1224 Returns a pointer to the result if successful; NULL otherwise.]
1225
1226 SideEffects [None]
1227
1228 SeeAlso [Cudd_bddVarMap]
1229
1230 ******************************************************************************/
1231 static DdNode *
cuddBddVarMapRecur(DdManager * manager,DdNode * f)1232 cuddBddVarMapRecur(
1233 DdManager *manager /* DD manager */,
1234 DdNode *f /* BDD to be remapped */)
1235 {
1236 DdNode *F, *T, *E;
1237 DdNode *res;
1238 int index;
1239
1240 statLine(manager);
1241 F = Cudd_Regular(f);
1242
1243 /* Check for terminal case of constant node. */
1244 if (cuddIsConstant(F)) {
1245 return(f);
1246 }
1247
1248 /* If problem already solved, look up answer and return. */
1249 if (F->ref != 1 &&
1250 (res = cuddCacheLookup1(manager,Cudd_bddVarMap,F)) != NULL) {
1251 return(Cudd_NotCond(res,F != f));
1252 }
1253
1254 if ( manager->TimeStop && Abc_Clock() > manager->TimeStop )
1255 return NULL;
1256
1257 /* Split and recur on children of this node. */
1258 T = cuddBddVarMapRecur(manager,cuddT(F));
1259 if (T == NULL) return(NULL);
1260 cuddRef(T);
1261 E = cuddBddVarMapRecur(manager,cuddE(F));
1262 if (E == NULL) {
1263 Cudd_IterDerefBdd(manager, T);
1264 return(NULL);
1265 }
1266 cuddRef(E);
1267
1268 /* Move variable that should be in this position to this position
1269 ** by retrieving the single var BDD for that variable, and calling
1270 ** cuddBddIteRecur with the T and E we just created.
1271 */
1272 index = manager->map[F->index];
1273 res = cuddBddIteRecur(manager,manager->vars[index],T,E);
1274 if (res == NULL) {
1275 Cudd_IterDerefBdd(manager, T);
1276 Cudd_IterDerefBdd(manager, E);
1277 return(NULL);
1278 }
1279 cuddRef(res);
1280 Cudd_IterDerefBdd(manager, T);
1281 Cudd_IterDerefBdd(manager, E);
1282
1283 /* Do not keep the result if the reference count is only 1, since
1284 ** it will not be visited again.
1285 */
1286 if (F->ref != 1) {
1287 cuddCacheInsert1(manager,Cudd_bddVarMap,F,res);
1288 }
1289 cuddDeref(res);
1290 return(Cudd_NotCond(res,F != f));
1291
1292 } /* end of cuddBddVarMapRecur */
1293
1294
1295 /**Function********************************************************************
1296
1297 Synopsis [Performs the recursive step of Cudd_addVectorCompose.]
1298
1299 Description []
1300
1301 SideEffects [None]
1302
1303 SeeAlso []
1304
1305 ******************************************************************************/
1306 static DdNode *
cuddAddVectorComposeRecur(DdManager * dd,DdHashTable * table,DdNode * f,DdNode ** vector,int deepest)1307 cuddAddVectorComposeRecur(
1308 DdManager * dd /* DD manager */,
1309 DdHashTable * table /* computed table */,
1310 DdNode * f /* ADD in which to compose */,
1311 DdNode ** vector /* functions to substitute */,
1312 int deepest /* depth of deepest substitution */)
1313 {
1314 DdNode *T,*E;
1315 DdNode *res;
1316
1317 statLine(dd);
1318 /* If we are past the deepest substitution, return f. */
1319 if (cuddI(dd,f->index) > deepest) {
1320 return(f);
1321 }
1322
1323 if ((res = cuddHashTableLookup1(table,f)) != NULL) {
1324 #ifdef DD_DEBUG
1325 addVectorComposeHits++;
1326 #endif
1327 return(res);
1328 }
1329
1330 /* Split and recur on children of this node. */
1331 T = cuddAddVectorComposeRecur(dd,table,cuddT(f),vector,deepest);
1332 if (T == NULL) return(NULL);
1333 cuddRef(T);
1334 E = cuddAddVectorComposeRecur(dd,table,cuddE(f),vector,deepest);
1335 if (E == NULL) {
1336 Cudd_RecursiveDeref(dd, T);
1337 return(NULL);
1338 }
1339 cuddRef(E);
1340
1341 /* Retrieve the 0-1 ADD for the current top variable and call
1342 ** cuddAddIteRecur with the T and E we just created.
1343 */
1344 res = cuddAddIteRecur(dd,vector[f->index],T,E);
1345 if (res == NULL) {
1346 Cudd_RecursiveDeref(dd, T);
1347 Cudd_RecursiveDeref(dd, E);
1348 return(NULL);
1349 }
1350 cuddRef(res);
1351 Cudd_RecursiveDeref(dd, T);
1352 Cudd_RecursiveDeref(dd, E);
1353
1354 /* Do not keep the result if the reference count is only 1, since
1355 ** it will not be visited again
1356 */
1357 if (f->ref != 1) {
1358 ptrint fanout = (ptrint) f->ref;
1359 cuddSatDec(fanout);
1360 if (!cuddHashTableInsert1(table,f,res,fanout)) {
1361 Cudd_RecursiveDeref(dd, res);
1362 return(NULL);
1363 }
1364 }
1365 cuddDeref(res);
1366 return(res);
1367
1368 } /* end of cuddAddVectorComposeRecur */
1369
1370
1371 /**Function********************************************************************
1372
1373 Synopsis [Performs the recursive step of Cudd_addGeneralVectorCompose.]
1374
1375 Description []
1376
1377 SideEffects [None]
1378
1379 SeeAlso []
1380
1381 ******************************************************************************/
1382 static DdNode *
cuddAddGeneralVectorComposeRecur(DdManager * dd,DdHashTable * table,DdNode * f,DdNode ** vectorOn,DdNode ** vectorOff,int deepest)1383 cuddAddGeneralVectorComposeRecur(
1384 DdManager * dd /* DD manager */,
1385 DdHashTable * table /* computed table */,
1386 DdNode * f /* ADD in which to compose */,
1387 DdNode ** vectorOn /* functions to substitute for x_i */,
1388 DdNode ** vectorOff /* functions to substitute for x_i' */,
1389 int deepest /* depth of deepest substitution */)
1390 {
1391 DdNode *T,*E,*t,*e;
1392 DdNode *res;
1393
1394 /* If we are past the deepest substitution, return f. */
1395 if (cuddI(dd,f->index) > deepest) {
1396 return(f);
1397 }
1398
1399 if ((res = cuddHashTableLookup1(table,f)) != NULL) {
1400 #ifdef DD_DEBUG
1401 addGeneralVectorComposeHits++;
1402 #endif
1403 return(res);
1404 }
1405
1406 /* Split and recur on children of this node. */
1407 T = cuddAddGeneralVectorComposeRecur(dd,table,cuddT(f),
1408 vectorOn,vectorOff,deepest);
1409 if (T == NULL) return(NULL);
1410 cuddRef(T);
1411 E = cuddAddGeneralVectorComposeRecur(dd,table,cuddE(f),
1412 vectorOn,vectorOff,deepest);
1413 if (E == NULL) {
1414 Cudd_RecursiveDeref(dd, T);
1415 return(NULL);
1416 }
1417 cuddRef(E);
1418
1419 /* Retrieve the compose ADDs for the current top variable and call
1420 ** cuddAddApplyRecur with the T and E we just created.
1421 */
1422 t = cuddAddApplyRecur(dd,Cudd_addTimes,vectorOn[f->index],T);
1423 if (t == NULL) {
1424 Cudd_RecursiveDeref(dd,T);
1425 Cudd_RecursiveDeref(dd,E);
1426 return(NULL);
1427 }
1428 cuddRef(t);
1429 e = cuddAddApplyRecur(dd,Cudd_addTimes,vectorOff[f->index],E);
1430 if (e == NULL) {
1431 Cudd_RecursiveDeref(dd,T);
1432 Cudd_RecursiveDeref(dd,E);
1433 Cudd_RecursiveDeref(dd,t);
1434 return(NULL);
1435 }
1436 cuddRef(e);
1437 res = cuddAddApplyRecur(dd,Cudd_addPlus,t,e);
1438 if (res == NULL) {
1439 Cudd_RecursiveDeref(dd,T);
1440 Cudd_RecursiveDeref(dd,E);
1441 Cudd_RecursiveDeref(dd,t);
1442 Cudd_RecursiveDeref(dd,e);
1443 return(NULL);
1444 }
1445 cuddRef(res);
1446 Cudd_RecursiveDeref(dd,T);
1447 Cudd_RecursiveDeref(dd,E);
1448 Cudd_RecursiveDeref(dd,t);
1449 Cudd_RecursiveDeref(dd,e);
1450
1451 /* Do not keep the result if the reference count is only 1, since
1452 ** it will not be visited again
1453 */
1454 if (f->ref != 1) {
1455 ptrint fanout = (ptrint) f->ref;
1456 cuddSatDec(fanout);
1457 if (!cuddHashTableInsert1(table,f,res,fanout)) {
1458 Cudd_RecursiveDeref(dd, res);
1459 return(NULL);
1460 }
1461 }
1462 cuddDeref(res);
1463 return(res);
1464
1465 } /* end of cuddAddGeneralVectorComposeRecur */
1466
1467
1468 /**Function********************************************************************
1469
1470 Synopsis [Performs the recursive step of Cudd_addNonSimCompose.]
1471
1472 Description []
1473
1474 SideEffects [None]
1475
1476 SeeAlso []
1477
1478 ******************************************************************************/
1479 static DdNode *
cuddAddNonSimComposeRecur(DdManager * dd,DdNode * f,DdNode ** vector,DdNode * key,DdNode * cube,int lastsub)1480 cuddAddNonSimComposeRecur(
1481 DdManager * dd,
1482 DdNode * f,
1483 DdNode ** vector,
1484 DdNode * key,
1485 DdNode * cube,
1486 int lastsub)
1487 {
1488 DdNode *f1, *f0, *key1, *key0, *cube1, *var;
1489 DdNode *T,*E;
1490 DdNode *r;
1491 unsigned int top, topf, topk, topc;
1492 unsigned int index;
1493 int i;
1494 DdNode **vect1;
1495 DdNode **vect0;
1496
1497 statLine(dd);
1498 /* If we are past the deepest substitution, return f. */
1499 if (cube == DD_ONE(dd) || cuddIsConstant(f)) {
1500 return(f);
1501 }
1502
1503 /* If problem already solved, look up answer and return. */
1504 r = cuddCacheLookup(dd,DD_ADD_NON_SIM_COMPOSE_TAG,f,key,cube);
1505 if (r != NULL) {
1506 return(r);
1507 }
1508
1509 /* Find top variable. we just need to look at f, key, and cube,
1510 ** because all the varibles in the gi are in key.
1511 */
1512 topf = cuddI(dd,f->index);
1513 topk = cuddI(dd,key->index);
1514 top = ddMin(topf,topk);
1515 topc = cuddI(dd,cube->index);
1516 top = ddMin(top,topc);
1517 index = dd->invperm[top];
1518
1519 /* Compute the cofactors. */
1520 if (topf == top) {
1521 f1 = cuddT(f);
1522 f0 = cuddE(f);
1523 } else {
1524 f1 = f0 = f;
1525 }
1526 if (topc == top) {
1527 cube1 = cuddT(cube);
1528 /* We want to eliminate vector[index] from key. Otherwise
1529 ** cache performance is severely affected. Hence we
1530 ** existentially quantify the variable with index "index" from key.
1531 */
1532 var = Cudd_addIthVar(dd, (int) index);
1533 if (var == NULL) {
1534 return(NULL);
1535 }
1536 cuddRef(var);
1537 key1 = cuddAddExistAbstractRecur(dd, key, var);
1538 if (key1 == NULL) {
1539 Cudd_RecursiveDeref(dd,var);
1540 return(NULL);
1541 }
1542 cuddRef(key1);
1543 Cudd_RecursiveDeref(dd,var);
1544 key0 = key1;
1545 } else {
1546 cube1 = cube;
1547 if (topk == top) {
1548 key1 = cuddT(key);
1549 key0 = cuddE(key);
1550 } else {
1551 key1 = key0 = key;
1552 }
1553 cuddRef(key1);
1554 }
1555
1556 /* Allocate two new vectors for the cofactors of vector. */
1557 vect1 = ABC_ALLOC(DdNode *,lastsub);
1558 if (vect1 == NULL) {
1559 dd->errorCode = CUDD_MEMORY_OUT;
1560 Cudd_RecursiveDeref(dd,key1);
1561 return(NULL);
1562 }
1563 vect0 = ABC_ALLOC(DdNode *,lastsub);
1564 if (vect0 == NULL) {
1565 dd->errorCode = CUDD_MEMORY_OUT;
1566 Cudd_RecursiveDeref(dd,key1);
1567 ABC_FREE(vect1);
1568 return(NULL);
1569 }
1570
1571 /* Cofactor the gi. Eliminate vect1[index] and vect0[index], because
1572 ** we do not need them.
1573 */
1574 for (i = 0; i < lastsub; i++) {
1575 DdNode *gi = vector[i];
1576 if (gi == NULL) {
1577 vect1[i] = vect0[i] = NULL;
1578 } else if (gi->index == index) {
1579 vect1[i] = cuddT(gi);
1580 vect0[i] = cuddE(gi);
1581 } else {
1582 vect1[i] = vect0[i] = gi;
1583 }
1584 }
1585 vect1[index] = vect0[index] = NULL;
1586
1587 /* Recur on children. */
1588 T = cuddAddNonSimComposeRecur(dd,f1,vect1,key1,cube1,lastsub);
1589 ABC_FREE(vect1);
1590 if (T == NULL) {
1591 Cudd_RecursiveDeref(dd,key1);
1592 ABC_FREE(vect0);
1593 return(NULL);
1594 }
1595 cuddRef(T);
1596 E = cuddAddNonSimComposeRecur(dd,f0,vect0,key0,cube1,lastsub);
1597 ABC_FREE(vect0);
1598 if (E == NULL) {
1599 Cudd_RecursiveDeref(dd,key1);
1600 Cudd_RecursiveDeref(dd,T);
1601 return(NULL);
1602 }
1603 cuddRef(E);
1604 Cudd_RecursiveDeref(dd,key1);
1605
1606 /* Retrieve the 0-1 ADD for the current top variable from vector,
1607 ** and call cuddAddIteRecur with the T and E we just created.
1608 */
1609 r = cuddAddIteRecur(dd,vector[index],T,E);
1610 if (r == NULL) {
1611 Cudd_RecursiveDeref(dd,T);
1612 Cudd_RecursiveDeref(dd,E);
1613 return(NULL);
1614 }
1615 cuddRef(r);
1616 Cudd_RecursiveDeref(dd,T);
1617 Cudd_RecursiveDeref(dd,E);
1618 cuddDeref(r);
1619
1620 /* Store answer to trim recursion. */
1621 cuddCacheInsert(dd,DD_ADD_NON_SIM_COMPOSE_TAG,f,key,cube,r);
1622
1623 return(r);
1624
1625 } /* end of cuddAddNonSimComposeRecur */
1626
1627
1628 /**Function********************************************************************
1629
1630 Synopsis [Performs the recursive step of Cudd_bddVectorCompose.]
1631
1632 Description []
1633
1634 SideEffects [None]
1635
1636 SeeAlso []
1637
1638 ******************************************************************************/
1639 static DdNode *
cuddBddVectorComposeRecur(DdManager * dd,DdHashTable * table,DdNode * f,DdNode ** vector,int deepest)1640 cuddBddVectorComposeRecur(
1641 DdManager * dd /* DD manager */,
1642 DdHashTable * table /* computed table */,
1643 DdNode * f /* BDD in which to compose */,
1644 DdNode ** vector /* functions to be composed */,
1645 int deepest /* depth of the deepest substitution */)
1646 {
1647 DdNode *F,*T,*E;
1648 DdNode *res;
1649
1650 statLine(dd);
1651 F = Cudd_Regular(f);
1652
1653 /* If we are past the deepest substitution, return f. */
1654 if (cuddI(dd,F->index) > deepest) {
1655 return(f);
1656 }
1657
1658 /* If problem already solved, look up answer and return. */
1659 if ((res = cuddHashTableLookup1(table,F)) != NULL) {
1660 #ifdef DD_DEBUG
1661 bddVectorComposeHits++;
1662 #endif
1663 return(Cudd_NotCond(res,F != f));
1664 }
1665
1666 /* Split and recur on children of this node. */
1667 T = cuddBddVectorComposeRecur(dd,table,cuddT(F),vector, deepest);
1668 if (T == NULL) return(NULL);
1669 cuddRef(T);
1670 E = cuddBddVectorComposeRecur(dd,table,cuddE(F),vector, deepest);
1671 if (E == NULL) {
1672 Cudd_IterDerefBdd(dd, T);
1673 return(NULL);
1674 }
1675 cuddRef(E);
1676
1677 /* Call cuddBddIteRecur with the BDD that replaces the current top
1678 ** variable and the T and E we just created.
1679 */
1680 res = cuddBddIteRecur(dd,vector[F->index],T,E);
1681 if (res == NULL) {
1682 Cudd_IterDerefBdd(dd, T);
1683 Cudd_IterDerefBdd(dd, E);
1684 return(NULL);
1685 }
1686 cuddRef(res);
1687 Cudd_IterDerefBdd(dd, T);
1688 Cudd_IterDerefBdd(dd, E);
1689
1690 /* Do not keep the result if the reference count is only 1, since
1691 ** it will not be visited again.
1692 */
1693 if (F->ref != 1) {
1694 ptrint fanout = (ptrint) F->ref;
1695 cuddSatDec(fanout);
1696 if (!cuddHashTableInsert1(table,F,res,fanout)) {
1697 Cudd_IterDerefBdd(dd, res);
1698 return(NULL);
1699 }
1700 }
1701 cuddDeref(res);
1702 return(Cudd_NotCond(res,F != f));
1703
1704 } /* end of cuddBddVectorComposeRecur */
1705
1706
1707 /**Function********************************************************************
1708
1709 Synopsis [Comparison of a function to the i-th ADD variable.]
1710
1711 Description [Comparison of a function to the i-th ADD variable. Returns 1 if
1712 the function is the i-th ADD variable; 0 otherwise.]
1713
1714 SideEffects [None]
1715
1716 SeeAlso []
1717
1718 ******************************************************************************/
1719 DD_INLINE
1720 static int
ddIsIthAddVar(DdManager * dd,DdNode * f,unsigned int i)1721 ddIsIthAddVar(
1722 DdManager * dd,
1723 DdNode * f,
1724 unsigned int i)
1725 {
1726 return(f->index == i && cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd));
1727
1728 } /* end of ddIsIthAddVar */
1729
1730
1731 /**Function********************************************************************
1732
1733 Synopsis [Comparison of a pair of functions to the i-th ADD variable.]
1734
1735 Description [Comparison of a pair of functions to the i-th ADD
1736 variable. Returns 1 if the functions are the i-th ADD variable and its
1737 complement; 0 otherwise.]
1738
1739 SideEffects [None]
1740
1741 SeeAlso []
1742
1743 ******************************************************************************/
1744 DD_INLINE
1745 static int
ddIsIthAddVarPair(DdManager * dd,DdNode * f,DdNode * g,unsigned int i)1746 ddIsIthAddVarPair(
1747 DdManager * dd,
1748 DdNode * f,
1749 DdNode * g,
1750 unsigned int i)
1751 {
1752 return(f->index == i && g->index == i &&
1753 cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd) &&
1754 cuddT(g) == DD_ZERO(dd) && cuddE(g) == DD_ONE(dd));
1755
1756 } /* end of ddIsIthAddVarPair */
1757
1758
1759 ABC_NAMESPACE_IMPL_END
1760
1761