source: vis_dev/glu-2.3/src/cuBdd/cuddCompose.c@ 34

Last change on this file since 34 was 13, checked in by cecile, 15 years ago

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