1 /**CFile****************************************************************
2
3 FileName [extraBddMisc.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [extra]
8
9 Synopsis [DD-based utilities.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: extraBddMisc.c,v 1.4 2005/10/04 00:19:54 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "extraBdd.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 /*---------------------------------------------------------------------------*/
27 /* Constant declarations */
28 /*---------------------------------------------------------------------------*/
29
30 /*---------------------------------------------------------------------------*/
31 /* Stucture declarations */
32 /*---------------------------------------------------------------------------*/
33
34 /*---------------------------------------------------------------------------*/
35 /* Type declarations */
36 /*---------------------------------------------------------------------------*/
37
38 /*---------------------------------------------------------------------------*/
39 /* Variable declarations */
40 /*---------------------------------------------------------------------------*/
41
42 /*---------------------------------------------------------------------------*/
43 /* Macro declarations */
44 /*---------------------------------------------------------------------------*/
45
46
47 /**AutomaticStart*************************************************************/
48
49 /*---------------------------------------------------------------------------*/
50 /* Static function prototypes */
51 /*---------------------------------------------------------------------------*/
52
53 // file "extraDdTransfer.c"
54 static DdNode * extraTransferPermuteRecur( DdManager * ddS, DdManager * ddD, DdNode * f, st__table * table, int * Permute );
55 static DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute );
56 static DdNode * cuddBddPermuteRecur ARGS( ( DdManager * manager, DdHashTable * table, DdNode * node, int *permut ) );
57
58 static DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute );
59
60 // file "cuddUtils.c"
61 void ddSupportStep2(DdNode *f, int *support);
62 void ddClearFlag2(DdNode *f);
63
64 static DdNode* extraZddPrimes( DdManager *dd, DdNode* F );
65
66 /**AutomaticEnd***************************************************************/
67
68 /*---------------------------------------------------------------------------*/
69 /* Definition of exported functions */
70 /*---------------------------------------------------------------------------*/
71
72 /**Function********************************************************************
73
74 Synopsis [Convert a {A,B}DD from a manager to another with variable remapping.]
75
76 Description [Convert a {A,B}DD from a manager to another one. The orders of the
77 variables in the two managers may be different. Returns a
78 pointer to the {A,B}DD in the destination manager if successful; NULL
79 otherwise. The i-th entry in the array Permute tells what is the index
80 of the i-th variable from the old manager in the new manager.]
81
82 SideEffects [None]
83
84 SeeAlso []
85
86 ******************************************************************************/
Extra_TransferPermute(DdManager * ddSource,DdManager * ddDestination,DdNode * f,int * Permute)87 DdNode * Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute )
88 {
89 DdNode * bRes;
90 do
91 {
92 ddDestination->reordered = 0;
93 bRes = extraTransferPermute( ddSource, ddDestination, f, Permute );
94 }
95 while ( ddDestination->reordered == 1 );
96 return ( bRes );
97
98 } /* end of Extra_TransferPermute */
99
100 /**Function********************************************************************
101
102 Synopsis [Transfers the BDD from one manager into another level by level.]
103
104 Description [Transfers the BDD from one manager into another while
105 preserving the correspondence between variables level by level.]
106
107 SideEffects [None]
108
109 SeeAlso []
110
111 ******************************************************************************/
Extra_TransferLevelByLevel(DdManager * ddSource,DdManager * ddDestination,DdNode * f)112 DdNode * Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f )
113 {
114 DdNode * bRes;
115 int * pPermute;
116 int nMin, nMax, i;
117
118 nMin = ddMin(ddSource->size, ddDestination->size);
119 nMax = ddMax(ddSource->size, ddDestination->size);
120 pPermute = ABC_ALLOC( int, nMax );
121 // set up the variable permutation
122 for ( i = 0; i < nMin; i++ )
123 pPermute[ ddSource->invperm[i] ] = ddDestination->invperm[i];
124 if ( ddSource->size > ddDestination->size )
125 {
126 for ( ; i < nMax; i++ )
127 pPermute[ ddSource->invperm[i] ] = -1;
128 }
129 bRes = Extra_TransferPermute( ddSource, ddDestination, f, pPermute );
130 ABC_FREE( pPermute );
131 return bRes;
132 }
133
134 /**Function********************************************************************
135
136 Synopsis [Remaps the function to depend on the topmost variables on the manager.]
137
138 Description []
139
140 SideEffects []
141
142 SeeAlso []
143
144 ******************************************************************************/
Extra_bddRemapUp(DdManager * dd,DdNode * bF)145 DdNode * Extra_bddRemapUp(
146 DdManager * dd,
147 DdNode * bF )
148 {
149 int * pPermute;
150 DdNode * bSupp, * bTemp, * bRes;
151 int Counter;
152
153 pPermute = ABC_ALLOC( int, dd->size );
154
155 // get support
156 bSupp = Cudd_Support( dd, bF ); Cudd_Ref( bSupp );
157
158 // create the variable map
159 // to remap the DD into the upper part of the manager
160 Counter = 0;
161 for ( bTemp = bSupp; bTemp != dd->one; bTemp = cuddT(bTemp) )
162 pPermute[bTemp->index] = dd->invperm[Counter++];
163
164 // transfer the BDD and remap it
165 bRes = Cudd_bddPermute( dd, bF, pPermute ); Cudd_Ref( bRes );
166
167 // remove support
168 Cudd_RecursiveDeref( dd, bSupp );
169
170 // return
171 Cudd_Deref( bRes );
172 ABC_FREE( pPermute );
173 return bRes;
174 }
175
176 /**Function********************************************************************
177
178 Synopsis [Moves the BDD by the given number of variables up or down.]
179
180 Description []
181
182 SideEffects []
183
184 SeeAlso [Extra_bddShift]
185
186 ******************************************************************************/
Extra_bddMove(DdManager * dd,DdNode * bF,int nVars)187 DdNode * Extra_bddMove(
188 DdManager * dd, /* the DD manager */
189 DdNode * bF,
190 int nVars)
191 {
192 DdNode * res;
193 DdNode * bVars;
194 if ( nVars == 0 )
195 return bF;
196 if ( Cudd_IsConstant(bF) )
197 return bF;
198 assert( nVars <= dd->size );
199 if ( nVars > 0 )
200 bVars = dd->vars[nVars];
201 else
202 bVars = Cudd_Not(dd->vars[-nVars]);
203
204 do {
205 dd->reordered = 0;
206 res = extraBddMove( dd, bF, bVars );
207 } while (dd->reordered == 1);
208 return(res);
209
210 } /* end of Extra_bddMove */
211
212 /**Function*************************************************************
213
214 Synopsis []
215
216 Description []
217
218 SideEffects []
219
220 SeeAlso []
221
222 ***********************************************************************/
Extra_StopManager(DdManager * dd)223 void Extra_StopManager( DdManager * dd )
224 {
225 int RetValue;
226 // check for remaining references in the package
227 RetValue = Cudd_CheckZeroRef( dd );
228 if ( RetValue > 10 )
229 // if ( RetValue )
230 printf( "\nThe number of referenced nodes = %d\n\n", RetValue );
231 // Cudd_PrintInfo( dd, stdout );
232 Cudd_Quit( dd );
233 }
234
235 /**Function********************************************************************
236
237 Synopsis [Outputs the BDD in a readable format.]
238
239 Description []
240
241 SideEffects [None]
242
243 SeeAlso []
244
245 ******************************************************************************/
Extra_bddPrint(DdManager * dd,DdNode * F)246 void Extra_bddPrint( DdManager * dd, DdNode * F )
247 {
248 DdGen * Gen;
249 int * Cube;
250 CUDD_VALUE_TYPE Value;
251 int nVars = dd->size;
252 int fFirstCube = 1;
253 int i;
254
255 if ( F == NULL )
256 {
257 printf("NULL");
258 return;
259 }
260 if ( F == b0 )
261 {
262 printf("Constant 0");
263 return;
264 }
265 if ( F == b1 )
266 {
267 printf("Constant 1");
268 return;
269 }
270
271 Cudd_ForeachCube( dd, F, Gen, Cube, Value )
272 {
273 if ( fFirstCube )
274 fFirstCube = 0;
275 else
276 // Output << " + ";
277 printf( " + " );
278
279 for ( i = 0; i < nVars; i++ )
280 if ( Cube[i] == 0 )
281 printf( "[%d]'", i );
282 // printf( "%c'", (char)('a'+i) );
283 else if ( Cube[i] == 1 )
284 printf( "[%d]", i );
285 // printf( "%c", (char)('a'+i) );
286 }
287
288 // printf("\n");
289 }
290
291 /**Function********************************************************************
292
293 Synopsis [Outputs the BDD in a readable format.]
294
295 Description []
296
297 SideEffects [None]
298
299 SeeAlso []
300
301 ******************************************************************************/
Extra_bddPrintSupport(DdManager * dd,DdNode * F)302 void Extra_bddPrintSupport( DdManager * dd, DdNode * F )
303 {
304 DdNode * bSupp;
305 bSupp = Cudd_Support( dd, F ); Cudd_Ref( bSupp );
306 Extra_bddPrint( dd, bSupp );
307 Cudd_RecursiveDeref( dd, bSupp );
308 }
309
310 /**Function********************************************************************
311
312 Synopsis [Returns the size of the support.]
313
314 Description []
315
316 SideEffects []
317
318 SeeAlso []
319
320 ******************************************************************************/
Extra_bddSuppSize(DdManager * dd,DdNode * bSupp)321 int Extra_bddSuppSize( DdManager * dd, DdNode * bSupp )
322 {
323 int Counter = 0;
324 while ( bSupp != b1 )
325 {
326 assert( !Cudd_IsComplement(bSupp) );
327 assert( cuddE(bSupp) == b0 );
328
329 bSupp = cuddT(bSupp);
330 Counter++;
331 }
332 return Counter;
333 }
334
335 /**Function********************************************************************
336
337 Synopsis [Returns 1 if the support contains the given BDD variable.]
338
339 Description []
340
341 SideEffects []
342
343 SeeAlso []
344
345 ******************************************************************************/
Extra_bddSuppContainVar(DdManager * dd,DdNode * bS,DdNode * bVar)346 int Extra_bddSuppContainVar( DdManager * dd, DdNode * bS, DdNode * bVar )
347 {
348 for( ; bS != b1; bS = cuddT(bS) )
349 if ( bS->index == bVar->index )
350 return 1;
351 return 0;
352 }
353
354 /**Function********************************************************************
355
356 Synopsis [Returns 1 if two supports represented as BDD cubes are overlapping.]
357
358 Description []
359
360 SideEffects []
361
362 SeeAlso []
363
364 ******************************************************************************/
Extra_bddSuppOverlapping(DdManager * dd,DdNode * S1,DdNode * S2)365 int Extra_bddSuppOverlapping( DdManager * dd, DdNode * S1, DdNode * S2 )
366 {
367 while ( S1->index != CUDD_CONST_INDEX && S2->index != CUDD_CONST_INDEX )
368 {
369 // if the top vars are the same, they intersect
370 if ( S1->index == S2->index )
371 return 1;
372 // if the top vars are different, skip the one, which is higher
373 if ( dd->perm[S1->index] < dd->perm[S2->index] )
374 S1 = cuddT(S1);
375 else
376 S2 = cuddT(S2);
377 }
378 return 0;
379 }
380
381 /**Function********************************************************************
382
383 Synopsis [Returns the number of different vars in two supports.]
384
385 Description [Counts the number of variables that appear in one support and
386 does not appear in other support. If the number exceeds DiffMax, returns DiffMax.]
387
388 SideEffects []
389
390 SeeAlso []
391
392 ******************************************************************************/
Extra_bddSuppDifferentVars(DdManager * dd,DdNode * S1,DdNode * S2,int DiffMax)393 int Extra_bddSuppDifferentVars( DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax )
394 {
395 int Result = 0;
396 while ( S1->index != CUDD_CONST_INDEX && S2->index != CUDD_CONST_INDEX )
397 {
398 // if the top vars are the same, this var is the same
399 if ( S1->index == S2->index )
400 {
401 S1 = cuddT(S1);
402 S2 = cuddT(S2);
403 continue;
404 }
405 // the top var is different
406 Result++;
407
408 if ( Result >= DiffMax )
409 return DiffMax;
410
411 // if the top vars are different, skip the one, which is higher
412 if ( dd->perm[S1->index] < dd->perm[S2->index] )
413 S1 = cuddT(S1);
414 else
415 S2 = cuddT(S2);
416 }
417
418 // consider the remaining variables
419 if ( S1->index != CUDD_CONST_INDEX )
420 Result += Extra_bddSuppSize(dd,S1);
421 else if ( S2->index != CUDD_CONST_INDEX )
422 Result += Extra_bddSuppSize(dd,S2);
423
424 if ( Result >= DiffMax )
425 return DiffMax;
426 return Result;
427 }
428
429
430 /**Function********************************************************************
431
432 Synopsis [Checks the support containment.]
433
434 Description [This function returns 1 if one support is contained in another.
435 In this case, bLarge (bSmall) is assigned to point to the larger (smaller) support.
436 If the supports are identical, return 0 and does not assign the supports!]
437
438 SideEffects []
439
440 SeeAlso []
441
442 ******************************************************************************/
Extra_bddSuppCheckContainment(DdManager * dd,DdNode * bL,DdNode * bH,DdNode ** bLarge,DdNode ** bSmall)443 int Extra_bddSuppCheckContainment( DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall )
444 {
445 DdNode * bSL = bL;
446 DdNode * bSH = bH;
447 int fLcontainsH = 1;
448 int fHcontainsL = 1;
449 int TopVar;
450
451 if ( bSL == bSH )
452 return 0;
453
454 while ( bSL != b1 || bSH != b1 )
455 {
456 if ( bSL == b1 )
457 { // Low component has no vars; High components has some vars
458 fLcontainsH = 0;
459 if ( fHcontainsL == 0 )
460 return 0;
461 else
462 break;
463 }
464
465 if ( bSH == b1 )
466 { // similarly
467 fHcontainsL = 0;
468 if ( fLcontainsH == 0 )
469 return 0;
470 else
471 break;
472 }
473
474 // determine the topmost var of the supports by comparing their levels
475 if ( dd->perm[bSL->index] < dd->perm[bSH->index] )
476 TopVar = bSL->index;
477 else
478 TopVar = bSH->index;
479
480 if ( TopVar == bSL->index && TopVar == bSH->index )
481 { // they are on the same level
482 // it does not tell us anything about their containment
483 // skip this var
484 bSL = cuddT(bSL);
485 bSH = cuddT(bSH);
486 }
487 else if ( TopVar == bSL->index ) // and TopVar != bSH->index
488 { // Low components is higher and contains more vars
489 // it is not possible that High component contains Low
490 fHcontainsL = 0;
491 // skip this var
492 bSL = cuddT(bSL);
493 }
494 else // if ( TopVar == bSH->index ) // and TopVar != bSL->index
495 { // similarly
496 fLcontainsH = 0;
497 // skip this var
498 bSH = cuddT(bSH);
499 }
500
501 // check the stopping condition
502 if ( !fHcontainsL && !fLcontainsH )
503 return 0;
504 }
505 // only one of them can be true at the same time
506 assert( !fHcontainsL || !fLcontainsH );
507 if ( fHcontainsL )
508 {
509 *bLarge = bH;
510 *bSmall = bL;
511 }
512 else // fLcontainsH
513 {
514 *bLarge = bL;
515 *bSmall = bH;
516 }
517 return 1;
518 }
519
520
521 /**Function********************************************************************
522
523 Synopsis [Finds variables on which the DD depends and returns them as am array.]
524
525 Description [Finds the variables on which the DD depends. Returns an array
526 with entries set to 1 for those variables that belong to the support;
527 NULL otherwise. The array is allocated by the user and should have at least
528 as many entries as the maximum number of variables in BDD and ZDD parts of
529 the manager.]
530
531 SideEffects [None]
532
533 SeeAlso [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport]
534
535 ******************************************************************************/
536 int *
Extra_SupportArray(DdManager * dd,DdNode * f,int * support)537 Extra_SupportArray(
538 DdManager * dd, /* manager */
539 DdNode * f, /* DD whose support is sought */
540 int * support ) /* array allocated by the user */
541 {
542 int i, size;
543
544 /* Initialize support array for ddSupportStep. */
545 size = ddMax(dd->size, dd->sizeZ);
546 for (i = 0; i < size; i++)
547 support[i] = 0;
548
549 /* Compute support and clean up markers. */
550 ddSupportStep2(Cudd_Regular(f),support);
551 ddClearFlag2(Cudd_Regular(f));
552
553 return(support);
554
555 } /* end of Extra_SupportArray */
556
557 /**Function********************************************************************
558
559 Synopsis [Finds the variables on which a set of DDs depends.]
560
561 Description [Finds the variables on which a set of DDs depends.
562 The set must contain either BDDs and ADDs, or ZDDs.
563 Returns a BDD consisting of the product of the variables if
564 successful; NULL otherwise.]
565
566 SideEffects [None]
567
568 SeeAlso [Cudd_Support Cudd_ClassifySupport]
569
570 ******************************************************************************/
571 int *
Extra_VectorSupportArray(DdManager * dd,DdNode ** F,int n,int * support)572 Extra_VectorSupportArray(
573 DdManager * dd, /* manager */
574 DdNode ** F, /* array of DDs whose support is sought */
575 int n, /* size of the array */
576 int * support ) /* array allocated by the user */
577 {
578 int i, size;
579
580 /* Allocate and initialize support array for ddSupportStep. */
581 size = ddMax( dd->size, dd->sizeZ );
582 for ( i = 0; i < size; i++ )
583 support[i] = 0;
584
585 /* Compute support and clean up markers. */
586 for ( i = 0; i < n; i++ )
587 ddSupportStep2( Cudd_Regular(F[i]), support );
588 for ( i = 0; i < n; i++ )
589 ddClearFlag2( Cudd_Regular(F[i]) );
590
591 return support;
592 }
593
594 /**Function********************************************************************
595
596 Synopsis [Find any cube belonging to the on-set of the function.]
597
598 Description []
599
600 SideEffects []
601
602 SeeAlso []
603
604 ******************************************************************************/
Extra_bddFindOneCube(DdManager * dd,DdNode * bF)605 DdNode * Extra_bddFindOneCube( DdManager * dd, DdNode * bF )
606 {
607 char * s_Temp;
608 DdNode * bCube, * bTemp;
609 int v;
610
611 // get the vector of variables in the cube
612 s_Temp = ABC_ALLOC( char, dd->size );
613 Cudd_bddPickOneCube( dd, bF, s_Temp );
614
615 // start the cube
616 bCube = b1; Cudd_Ref( bCube );
617 for ( v = 0; v < dd->size; v++ )
618 if ( s_Temp[v] == 0 )
619 {
620 // Cube &= !s_XVars[v];
621 bCube = Cudd_bddAnd( dd, bTemp = bCube, Cudd_Not(dd->vars[v]) ); Cudd_Ref( bCube );
622 Cudd_RecursiveDeref( dd, bTemp );
623 }
624 else if ( s_Temp[v] == 1 )
625 {
626 // Cube &= s_XVars[v];
627 bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[v] ); Cudd_Ref( bCube );
628 Cudd_RecursiveDeref( dd, bTemp );
629 }
630 Cudd_Deref(bCube);
631 ABC_FREE( s_Temp );
632 return bCube;
633 }
634
635 /**Function********************************************************************
636
637 Synopsis [Returns one cube contained in the given BDD.]
638
639 Description [This function returns the cube with the smallest
640 bits-to-integer value.]
641
642 SideEffects []
643
644 ******************************************************************************/
Extra_bddGetOneCube(DdManager * dd,DdNode * bFunc)645 DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc )
646 {
647 DdNode * bFuncR, * bFunc0, * bFunc1;
648 DdNode * bRes0, * bRes1, * bRes;
649
650 bFuncR = Cudd_Regular(bFunc);
651 if ( cuddIsConstant(bFuncR) )
652 return bFunc;
653
654 // cofactor
655 if ( Cudd_IsComplement(bFunc) )
656 {
657 bFunc0 = Cudd_Not( cuddE(bFuncR) );
658 bFunc1 = Cudd_Not( cuddT(bFuncR) );
659 }
660 else
661 {
662 bFunc0 = cuddE(bFuncR);
663 bFunc1 = cuddT(bFuncR);
664 }
665
666 // try to find the cube with the negative literal
667 bRes0 = Extra_bddGetOneCube( dd, bFunc0 ); Cudd_Ref( bRes0 );
668
669 if ( bRes0 != b0 )
670 {
671 bRes = Cudd_bddAnd( dd, bRes0, Cudd_Not(dd->vars[bFuncR->index]) ); Cudd_Ref( bRes );
672 Cudd_RecursiveDeref( dd, bRes0 );
673 }
674 else
675 {
676 Cudd_RecursiveDeref( dd, bRes0 );
677 // try to find the cube with the positive literal
678 bRes1 = Extra_bddGetOneCube( dd, bFunc1 ); Cudd_Ref( bRes1 );
679 assert( bRes1 != b0 );
680 bRes = Cudd_bddAnd( dd, bRes1, dd->vars[bFuncR->index] ); Cudd_Ref( bRes );
681 Cudd_RecursiveDeref( dd, bRes1 );
682 }
683
684 Cudd_Deref( bRes );
685 return bRes;
686 }
687
688 /**Function********************************************************************
689
690 Synopsis [Performs the reordering-sensitive step of Extra_bddMove().]
691
692 Description []
693
694 SideEffects []
695
696 SeeAlso []
697
698 ******************************************************************************/
Extra_bddComputeRangeCube(DdManager * dd,int iStart,int iStop)699 DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop )
700 {
701 DdNode * bTemp, * bProd;
702 int i;
703 assert( iStart <= iStop );
704 assert( iStart >= 0 && iStart <= dd->size );
705 assert( iStop >= 0 && iStop <= dd->size );
706 bProd = b1; Cudd_Ref( bProd );
707 for ( i = iStart; i < iStop; i++ )
708 {
709 bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] ); Cudd_Ref( bProd );
710 Cudd_RecursiveDeref( dd, bTemp );
711 }
712 Cudd_Deref( bProd );
713 return bProd;
714 }
715
716 /**Function********************************************************************
717
718 Synopsis [Computes the cube of BDD variables corresponding to bits it the bit-code]
719
720 Description [Returns a bdd composed of elementary bdds found in array BddVars[] such
721 that the bdd vars encode the number Value of bit length CodeWidth (if fMsbFirst is 1,
722 the most significant bit is encoded with the first bdd variable). If the variables
723 BddVars are not specified, takes the first CodeWidth variables of the manager]
724
725 SideEffects []
726
727 SeeAlso []
728
729 ******************************************************************************/
Extra_bddBitsToCube(DdManager * dd,int Code,int CodeWidth,DdNode ** pbVars,int fMsbFirst)730 DdNode * Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst )
731 {
732 int z;
733 DdNode * bTemp, * bVar, * bVarBdd, * bResult;
734
735 bResult = b1; Cudd_Ref( bResult );
736 for ( z = 0; z < CodeWidth; z++ )
737 {
738 bVarBdd = (pbVars)? pbVars[z]: dd->vars[z];
739 if ( fMsbFirst )
740 bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (CodeWidth-1-z)))==0 );
741 else
742 bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (z)))==0 );
743 bResult = Cudd_bddAnd( dd, bTemp = bResult, bVar ); Cudd_Ref( bResult );
744 Cudd_RecursiveDeref( dd, bTemp );
745 }
746 Cudd_Deref( bResult );
747
748 return bResult;
749 } /* end of Extra_bddBitsToCube */
750
751 /**Function********************************************************************
752
753 Synopsis [Finds the support as a negative polarity cube.]
754
755 Description [Finds the variables on which a DD depends. Returns a BDD
756 consisting of the product of the variables in the negative polarity
757 if successful; NULL otherwise.]
758
759 SideEffects [None]
760
761 SeeAlso [Cudd_VectorSupport Cudd_Support]
762
763 ******************************************************************************/
Extra_bddSupportNegativeCube(DdManager * dd,DdNode * f)764 DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f )
765 {
766 int *support;
767 DdNode *res, *tmp, *var;
768 int i, j;
769 int size;
770
771 /* Allocate and initialize support array for ddSupportStep. */
772 size = ddMax( dd->size, dd->sizeZ );
773 support = ABC_ALLOC( int, size );
774 if ( support == NULL )
775 {
776 dd->errorCode = CUDD_MEMORY_OUT;
777 return ( NULL );
778 }
779 for ( i = 0; i < size; i++ )
780 {
781 support[i] = 0;
782 }
783
784 /* Compute support and clean up markers. */
785 ddSupportStep2( Cudd_Regular( f ), support );
786 ddClearFlag2( Cudd_Regular( f ) );
787
788 /* Transform support from array to cube. */
789 do
790 {
791 dd->reordered = 0;
792 res = DD_ONE( dd );
793 cuddRef( res );
794 for ( j = size - 1; j >= 0; j-- )
795 { /* for each level bottom-up */
796 i = ( j >= dd->size ) ? j : dd->invperm[j];
797 if ( support[i] == 1 )
798 {
799 var = cuddUniqueInter( dd, i, dd->one, Cudd_Not( dd->one ) );
800 //////////////////////////////////////////////////////////////////
801 var = Cudd_Not(var);
802 //////////////////////////////////////////////////////////////////
803 cuddRef( var );
804 tmp = cuddBddAndRecur( dd, res, var );
805 if ( tmp == NULL )
806 {
807 Cudd_RecursiveDeref( dd, res );
808 Cudd_RecursiveDeref( dd, var );
809 res = NULL;
810 break;
811 }
812 cuddRef( tmp );
813 Cudd_RecursiveDeref( dd, res );
814 Cudd_RecursiveDeref( dd, var );
815 res = tmp;
816 }
817 }
818 }
819 while ( dd->reordered == 1 );
820
821 ABC_FREE( support );
822 if ( res != NULL )
823 cuddDeref( res );
824 return ( res );
825
826 } /* end of Extra_SupportNeg */
827
828 /**Function********************************************************************
829
830 Synopsis [Returns 1 if the BDD is the BDD of elementary variable.]
831
832 Description []
833
834 SideEffects []
835
836 SeeAlso []
837
838 ******************************************************************************/
Extra_bddIsVar(DdNode * bFunc)839 int Extra_bddIsVar( DdNode * bFunc )
840 {
841 bFunc = Cudd_Regular( bFunc );
842 if ( cuddIsConstant(bFunc) )
843 return 0;
844 return cuddIsConstant( cuddT(bFunc) ) && cuddIsConstant( Cudd_Regular(cuddE(bFunc)) );
845 }
846
847 /**Function********************************************************************
848
849 Synopsis [Creates AND composed of the first nVars of the manager.]
850
851 Description []
852
853 SideEffects []
854
855 SeeAlso []
856
857 ******************************************************************************/
Extra_bddCreateAnd(DdManager * dd,int nVars)858 DdNode * Extra_bddCreateAnd( DdManager * dd, int nVars )
859 {
860 DdNode * bFunc, * bTemp;
861 int i;
862 bFunc = Cudd_ReadOne(dd); Cudd_Ref( bFunc );
863 for ( i = 0; i < nVars; i++ )
864 {
865 bFunc = Cudd_bddAnd( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) ); Cudd_Ref( bFunc );
866 Cudd_RecursiveDeref( dd, bTemp );
867 }
868 Cudd_Deref( bFunc );
869 return bFunc;
870 }
871
872 /**Function********************************************************************
873
874 Synopsis [Creates OR composed of the first nVars of the manager.]
875
876 Description []
877
878 SideEffects []
879
880 SeeAlso []
881
882 ******************************************************************************/
Extra_bddCreateOr(DdManager * dd,int nVars)883 DdNode * Extra_bddCreateOr( DdManager * dd, int nVars )
884 {
885 DdNode * bFunc, * bTemp;
886 int i;
887 bFunc = Cudd_ReadLogicZero(dd); Cudd_Ref( bFunc );
888 for ( i = 0; i < nVars; i++ )
889 {
890 bFunc = Cudd_bddOr( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) ); Cudd_Ref( bFunc );
891 Cudd_RecursiveDeref( dd, bTemp );
892 }
893 Cudd_Deref( bFunc );
894 return bFunc;
895 }
896
897 /**Function********************************************************************
898
899 Synopsis [Creates EXOR composed of the first nVars of the manager.]
900
901 Description []
902
903 SideEffects []
904
905 SeeAlso []
906
907 ******************************************************************************/
Extra_bddCreateExor(DdManager * dd,int nVars)908 DdNode * Extra_bddCreateExor( DdManager * dd, int nVars )
909 {
910 DdNode * bFunc, * bTemp;
911 int i;
912 bFunc = Cudd_ReadLogicZero(dd); Cudd_Ref( bFunc );
913 for ( i = 0; i < nVars; i++ )
914 {
915 bFunc = Cudd_bddXor( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) ); Cudd_Ref( bFunc );
916 Cudd_RecursiveDeref( dd, bTemp );
917 }
918 Cudd_Deref( bFunc );
919 return bFunc;
920 }
921
922 /**Function********************************************************************
923
924 Synopsis [Computes the set of primes as a ZDD.]
925
926 Description []
927
928 SideEffects []
929
930 SeeAlso []
931
932 ******************************************************************************/
Extra_zddPrimes(DdManager * dd,DdNode * F)933 DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F )
934 {
935 DdNode *res;
936 do {
937 dd->reordered = 0;
938 res = extraZddPrimes(dd, F);
939 if ( dd->reordered == 1 )
940 printf("\nReordering in Extra_zddPrimes()\n");
941 } while (dd->reordered == 1);
942 return(res);
943
944 } /* end of Extra_zddPrimes */
945
946 /**Function********************************************************************
947
948 Synopsis [Permutes the variables of the array of BDDs.]
949
950 Description [Given a permutation in array permut, creates a new BDD
951 with permuted variables. There should be an entry in array permut
952 for each variable in the manager. The i-th entry of permut holds the
953 index of the variable that is to substitute the i-th variable.
954 The DDs in the resulting array are already referenced.]
955
956 SideEffects [None]
957
958 SeeAlso [Cudd_addPermute Cudd_bddSwapVariables]
959
960 ******************************************************************************/
Extra_bddPermuteArray(DdManager * manager,DdNode ** bNodesIn,DdNode ** bNodesOut,int nNodes,int * permut)961 void Extra_bddPermuteArray( DdManager * manager, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut )
962 {
963 DdHashTable *table;
964 int i, k;
965 do
966 {
967 manager->reordered = 0;
968 table = cuddHashTableInit( manager, 1, 2 );
969
970 /* permute the output functions one-by-one */
971 for ( i = 0; i < nNodes; i++ )
972 {
973 bNodesOut[i] = cuddBddPermuteRecur( manager, table, bNodesIn[i], permut );
974 if ( bNodesOut[i] == NULL )
975 {
976 /* deref the array of the already computed outputs */
977 for ( k = 0; k < i; k++ )
978 Cudd_RecursiveDeref( manager, bNodesOut[k] );
979 break;
980 }
981 cuddRef( bNodesOut[i] );
982 }
983 /* Dispose of local cache. */
984 cuddHashTableQuit( table );
985 }
986 while ( manager->reordered == 1 );
987 } /* end of Extra_bddPermuteArray */
988
989
990 /**Function********************************************************************
991
992 Synopsis [Computes the positive polarty cube composed of the first vars in the array.]
993
994 Description []
995
996 SideEffects []
997
998 SeeAlso []
999
1000 ******************************************************************************/
Extra_bddComputeCube(DdManager * dd,DdNode ** bXVars,int nVars)1001 DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars )
1002 {
1003 DdNode * bRes;
1004 DdNode * bTemp;
1005 int i;
1006
1007 bRes = b1; Cudd_Ref( bRes );
1008 for ( i = 0; i < nVars; i++ )
1009 {
1010 bRes = Cudd_bddAnd( dd, bTemp = bRes, bXVars[i] ); Cudd_Ref( bRes );
1011 Cudd_RecursiveDeref( dd, bTemp );
1012 }
1013
1014 Cudd_Deref( bRes );
1015 return bRes;
1016 }
1017
1018 /**Function********************************************************************
1019
1020 Synopsis [Changes the polarity of vars listed in the cube.]
1021
1022 Description []
1023
1024 SideEffects []
1025
1026 SeeAlso []
1027
1028 ******************************************************************************/
Extra_bddChangePolarity(DdManager * dd,DdNode * bFunc,DdNode * bVars)1029 DdNode * Extra_bddChangePolarity(
1030 DdManager * dd, /* the DD manager */
1031 DdNode * bFunc,
1032 DdNode * bVars)
1033 {
1034 DdNode *res;
1035 do {
1036 dd->reordered = 0;
1037 res = extraBddChangePolarity( dd, bFunc, bVars );
1038 } while (dd->reordered == 1);
1039 return(res);
1040
1041 } /* end of Extra_bddChangePolarity */
1042
1043
1044 /**Function*************************************************************
1045
1046 Synopsis [Checks if the given variable belongs to the cube.]
1047
1048 Description [Return -1 if the var does not appear in the cube.
1049 Otherwise, returns polarity (0 or 1) of the var in the cube.]
1050
1051 SideEffects []
1052
1053 SeeAlso []
1054
1055 ***********************************************************************/
Extra_bddVarIsInCube(DdNode * bCube,int iVar)1056 int Extra_bddVarIsInCube( DdNode * bCube, int iVar )
1057 {
1058 DdNode * bCube0, * bCube1;
1059 while ( Cudd_Regular(bCube)->index != CUDD_CONST_INDEX )
1060 {
1061 bCube0 = Cudd_NotCond( cuddE(Cudd_Regular(bCube)), Cudd_IsComplement(bCube) );
1062 bCube1 = Cudd_NotCond( cuddT(Cudd_Regular(bCube)), Cudd_IsComplement(bCube) );
1063 // make sure it is a cube
1064 assert( (Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX) || // bCube0 == 0
1065 (Cudd_IsComplement(bCube1) && Cudd_Regular(bCube1)->index == CUDD_CONST_INDEX) ); // bCube1 == 0
1066 // quit if it is the last one
1067 if ( Cudd_Regular(bCube)->index == iVar )
1068 return (int)(Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX);
1069 // get the next cube
1070 if ( (Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX) )
1071 bCube = bCube1;
1072 else
1073 bCube = bCube0;
1074 }
1075 return -1;
1076 }
1077
1078 /**Function*************************************************************
1079
1080 Synopsis [Computes the AND of two BDD with different orders.]
1081
1082 Description [Derives the result of Boolean AND of bF and bG in ddF.
1083 The array pPermute gives the mapping of variables of ddG into that of ddF.]
1084
1085 SideEffects []
1086
1087 SeeAlso []
1088
1089 ***********************************************************************/
Extra_bddAndPermute(DdManager * ddF,DdNode * bF,DdManager * ddG,DdNode * bG,int * pPermute)1090 DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute )
1091 {
1092 DdHashTable * table;
1093 DdNode * bRes;
1094 do
1095 {
1096 ddF->reordered = 0;
1097 table = cuddHashTableInit( ddF, 2, 256 );
1098 if (table == NULL) return NULL;
1099 bRes = extraBddAndPermute( table, ddF, bF, ddG, bG, pPermute );
1100 if ( bRes ) cuddRef( bRes );
1101 cuddHashTableQuit( table );
1102 if ( bRes ) cuddDeref( bRes );
1103 //if ( ddF->reordered == 1 )
1104 //printf( "Reordering happened\n" );
1105 }
1106 while ( ddF->reordered == 1 );
1107 //printf( "|F| =%6d |G| =%6d |H| =%6d |F|*|G| =%9d\n",
1108 // Cudd_DagSize(bF), Cudd_DagSize(bG), Cudd_DagSize(bRes),
1109 // Cudd_DagSize(bF) * Cudd_DagSize(bG) );
1110 return ( bRes );
1111 }
1112
1113 /*---------------------------------------------------------------------------*/
1114 /* Definition of internal functions */
1115 /*---------------------------------------------------------------------------*/
1116
1117 /**Function********************************************************************
1118
1119 Synopsis [Performs the reordering-sensitive step of Extra_bddMove().]
1120
1121 Description []
1122
1123 SideEffects []
1124
1125 SeeAlso []
1126
1127 ******************************************************************************/
extraBddMove(DdManager * dd,DdNode * bF,DdNode * bDist)1128 DdNode * extraBddMove(
1129 DdManager * dd, /* the DD manager */
1130 DdNode * bF,
1131 DdNode * bDist)
1132 {
1133 DdNode * bRes;
1134
1135 if ( Cudd_IsConstant(bF) )
1136 return bF;
1137
1138 if ( (bRes = cuddCacheLookup2(dd, extraBddMove, bF, bDist)) )
1139 return bRes;
1140 else
1141 {
1142 DdNode * bRes0, * bRes1;
1143 DdNode * bF0, * bF1;
1144 DdNode * bFR = Cudd_Regular(bF);
1145 int VarNew;
1146
1147 if ( Cudd_IsComplement(bDist) )
1148 VarNew = bFR->index - Cudd_Not(bDist)->index;
1149 else
1150 VarNew = bFR->index + bDist->index;
1151 assert( VarNew < dd->size );
1152
1153 // cofactor the functions
1154 if ( bFR != bF ) // bFunc is complemented
1155 {
1156 bF0 = Cudd_Not( cuddE(bFR) );
1157 bF1 = Cudd_Not( cuddT(bFR) );
1158 }
1159 else
1160 {
1161 bF0 = cuddE(bFR);
1162 bF1 = cuddT(bFR);
1163 }
1164
1165 bRes0 = extraBddMove( dd, bF0, bDist );
1166 if ( bRes0 == NULL )
1167 return NULL;
1168 cuddRef( bRes0 );
1169
1170 bRes1 = extraBddMove( dd, bF1, bDist );
1171 if ( bRes1 == NULL )
1172 {
1173 Cudd_RecursiveDeref( dd, bRes0 );
1174 return NULL;
1175 }
1176 cuddRef( bRes1 );
1177
1178 /* only bRes0 and bRes1 are referenced at this point */
1179 bRes = cuddBddIteRecur( dd, dd->vars[VarNew], bRes1, bRes0 );
1180 if ( bRes == NULL )
1181 {
1182 Cudd_RecursiveDeref( dd, bRes0 );
1183 Cudd_RecursiveDeref( dd, bRes1 );
1184 return NULL;
1185 }
1186 cuddRef( bRes );
1187 Cudd_RecursiveDeref( dd, bRes0 );
1188 Cudd_RecursiveDeref( dd, bRes1 );
1189
1190 /* insert the result into cache */
1191 cuddCacheInsert2( dd, extraBddMove, bF, bDist, bRes );
1192 cuddDeref( bRes );
1193 return bRes;
1194 }
1195 } /* end of extraBddMove */
1196
1197
1198 /**Function********************************************************************
1199
1200 Synopsis [Finds three cofactors of the cover w.r.t. to the topmost variable.]
1201
1202 Description [Finds three cofactors of the cover w.r.t. to the topmost variable.
1203 Does not check the cover for being a constant. Assumes that ZDD variables encoding
1204 positive and negative polarities are adjacent in the variable order. Is different
1205 from cuddZddGetCofactors3() in that it does not compute the cofactors w.r.t. the
1206 given variable but takes the cofactors with respent to the topmost variable.
1207 This function is more efficient when used in recursive procedures because it does
1208 not require referencing of the resulting cofactors (compare cuddZddProduct()
1209 and extraZddPrimeProduct()).]
1210
1211 SideEffects [None]
1212
1213 SeeAlso [cuddZddGetCofactors3]
1214
1215 ******************************************************************************/
1216 void
extraDecomposeCover(DdManager * dd,DdNode * zC,DdNode ** zC0,DdNode ** zC1,DdNode ** zC2)1217 extraDecomposeCover(
1218 DdManager* dd, /* the manager */
1219 DdNode* zC, /* the cover */
1220 DdNode** zC0, /* the pointer to the negative var cofactor */
1221 DdNode** zC1, /* the pointer to the positive var cofactor */
1222 DdNode** zC2 ) /* the pointer to the cofactor without var */
1223 {
1224 if ( (zC->index & 1) == 0 )
1225 { /* the top variable is present in positive polarity and maybe in negative */
1226
1227 DdNode *Temp = cuddE( zC );
1228 *zC1 = cuddT( zC );
1229 if ( cuddIZ(dd,Temp->index) == cuddIZ(dd,zC->index) + 1 )
1230 { /* Temp is not a terminal node
1231 * top var is present in negative polarity */
1232 *zC2 = cuddE( Temp );
1233 *zC0 = cuddT( Temp );
1234 }
1235 else
1236 { /* top var is not present in negative polarity */
1237 *zC2 = Temp;
1238 *zC0 = dd->zero;
1239 }
1240 }
1241 else
1242 { /* the top variable is present only in negative */
1243 *zC1 = dd->zero;
1244 *zC2 = cuddE( zC );
1245 *zC0 = cuddT( zC );
1246 }
1247 } /* extraDecomposeCover */
1248
1249
1250
1251 /**Function********************************************************************
1252
1253 Synopsis [Counts the total number of cubes in the ISOPs of the functions.]
1254
1255 Description [Returns -1 if the number of cubes exceeds the limit.]
1256
1257 SideEffects [None]
1258
1259 SeeAlso [Extra_TransferPermute]
1260
1261 ******************************************************************************/
extraBddCountCubes(DdManager * dd,DdNode * L,DdNode * U,st__table * table,int * pnCubes,int Limit)1262 static DdNode * extraBddCountCubes( DdManager * dd, DdNode * L, DdNode * U, st__table *table, int * pnCubes, int Limit )
1263 {
1264 DdNode *one = DD_ONE(dd);
1265 DdNode *zero = Cudd_Not(one);
1266 int v, top_l, top_u;
1267 DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
1268 DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
1269 DdNode *Isub0, *Isub1, *Id;
1270 DdNode *x;
1271 DdNode *term0, *term1, *sum;
1272 DdNode *Lv, *Uv, *Lnv, *Unv;
1273 DdNode *r;
1274 int index;
1275 int Count0 = 0, Count1 = 0, Count2 = 0;
1276
1277 statLine(dd);
1278 if (L == zero)
1279 {
1280 *pnCubes = 0;
1281 return(zero);
1282 }
1283 if (U == one)
1284 {
1285 *pnCubes = 1;
1286 return(one);
1287 }
1288
1289 /* Check cache */
1290 r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
1291 if (r)
1292 {
1293 int nCubes = 0;
1294 if ( st__lookup( table, (char *)r, (char **)&nCubes ) )
1295 *pnCubes = nCubes;
1296 else assert( 0 );
1297 return r;
1298 }
1299
1300 top_l = dd->perm[Cudd_Regular(L)->index];
1301 top_u = dd->perm[Cudd_Regular(U)->index];
1302 v = ddMin(top_l, top_u);
1303
1304 /* Compute cofactors */
1305 if (top_l == v) {
1306 index = Cudd_Regular(L)->index;
1307 Lv = Cudd_T(L);
1308 Lnv = Cudd_E(L);
1309 if (Cudd_IsComplement(L)) {
1310 Lv = Cudd_Not(Lv);
1311 Lnv = Cudd_Not(Lnv);
1312 }
1313 }
1314 else {
1315 index = Cudd_Regular(U)->index;
1316 Lv = Lnv = L;
1317 }
1318
1319 if (top_u == v) {
1320 Uv = Cudd_T(U);
1321 Unv = Cudd_E(U);
1322 if (Cudd_IsComplement(U)) {
1323 Uv = Cudd_Not(Uv);
1324 Unv = Cudd_Not(Unv);
1325 }
1326 }
1327 else {
1328 Uv = Unv = U;
1329 }
1330
1331 Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
1332 if (Lsub0 == NULL)
1333 return(NULL);
1334 Cudd_Ref(Lsub0);
1335 Usub0 = Unv;
1336 Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
1337 if (Lsub1 == NULL) {
1338 Cudd_RecursiveDeref(dd, Lsub0);
1339 return(NULL);
1340 }
1341 Cudd_Ref(Lsub1);
1342 Usub1 = Uv;
1343
1344 Isub0 = extraBddCountCubes(dd, Lsub0, Usub0, table, &Count0, Limit);
1345 if (Isub0 == NULL) {
1346 Cudd_RecursiveDeref(dd, Lsub0);
1347 Cudd_RecursiveDeref(dd, Lsub1);
1348 return(NULL);
1349 }
1350 Cudd_Ref(Isub0);
1351 Isub1 = extraBddCountCubes(dd, Lsub1, Usub1, table, &Count1, Limit);
1352 if (Isub1 == NULL) {
1353 Cudd_RecursiveDeref(dd, Lsub0);
1354 Cudd_RecursiveDeref(dd, Lsub1);
1355 Cudd_RecursiveDeref(dd, Isub0);
1356 return(NULL);
1357 }
1358 Cudd_Ref(Isub1);
1359 Cudd_RecursiveDeref(dd, Lsub0);
1360 Cudd_RecursiveDeref(dd, Lsub1);
1361
1362 Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
1363 if (Lsuper0 == NULL) {
1364 Cudd_RecursiveDeref(dd, Isub0);
1365 Cudd_RecursiveDeref(dd, Isub1);
1366 return(NULL);
1367 }
1368 Cudd_Ref(Lsuper0);
1369 Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
1370 if (Lsuper1 == NULL) {
1371 Cudd_RecursiveDeref(dd, Isub0);
1372 Cudd_RecursiveDeref(dd, Isub1);
1373 Cudd_RecursiveDeref(dd, Lsuper0);
1374 return(NULL);
1375 }
1376 Cudd_Ref(Lsuper1);
1377 Usuper0 = Unv;
1378 Usuper1 = Uv;
1379
1380 /* Ld = Lsuper0 + Lsuper1 */
1381 Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
1382 Ld = Cudd_NotCond(Ld, Ld != NULL);
1383 if (Ld == NULL) {
1384 Cudd_RecursiveDeref(dd, Isub0);
1385 Cudd_RecursiveDeref(dd, Isub1);
1386 Cudd_RecursiveDeref(dd, Lsuper0);
1387 Cudd_RecursiveDeref(dd, Lsuper1);
1388 return(NULL);
1389 }
1390 Cudd_Ref(Ld);
1391 Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
1392 if (Ud == NULL) {
1393 Cudd_RecursiveDeref(dd, Isub0);
1394 Cudd_RecursiveDeref(dd, Isub1);
1395 Cudd_RecursiveDeref(dd, Lsuper0);
1396 Cudd_RecursiveDeref(dd, Lsuper1);
1397 Cudd_RecursiveDeref(dd, Ld);
1398 return(NULL);
1399 }
1400 Cudd_Ref(Ud);
1401 Cudd_RecursiveDeref(dd, Lsuper0);
1402 Cudd_RecursiveDeref(dd, Lsuper1);
1403
1404 Id = extraBddCountCubes(dd, Ld, Ud, table, &Count2, Limit);
1405 if (Id == NULL) {
1406 Cudd_RecursiveDeref(dd, Isub0);
1407 Cudd_RecursiveDeref(dd, Isub1);
1408 Cudd_RecursiveDeref(dd, Ld);
1409 Cudd_RecursiveDeref(dd, Ud);
1410 return(NULL);
1411 }
1412 Cudd_Ref(Id);
1413 Cudd_RecursiveDeref(dd, Ld);
1414 Cudd_RecursiveDeref(dd, Ud);
1415
1416 x = cuddUniqueInter(dd, index, one, zero);
1417 if (x == NULL) {
1418 Cudd_RecursiveDeref(dd, Isub0);
1419 Cudd_RecursiveDeref(dd, Isub1);
1420 Cudd_RecursiveDeref(dd, Id);
1421 return(NULL);
1422 }
1423 Cudd_Ref(x);
1424 term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
1425 if (term0 == NULL) {
1426 Cudd_RecursiveDeref(dd, Isub0);
1427 Cudd_RecursiveDeref(dd, Isub1);
1428 Cudd_RecursiveDeref(dd, Id);
1429 Cudd_RecursiveDeref(dd, x);
1430 return(NULL);
1431 }
1432 Cudd_Ref(term0);
1433 Cudd_RecursiveDeref(dd, Isub0);
1434 term1 = cuddBddAndRecur(dd, x, Isub1);
1435 if (term1 == NULL) {
1436 Cudd_RecursiveDeref(dd, Isub1);
1437 Cudd_RecursiveDeref(dd, Id);
1438 Cudd_RecursiveDeref(dd, x);
1439 Cudd_RecursiveDeref(dd, term0);
1440 return(NULL);
1441 }
1442 Cudd_Ref(term1);
1443 Cudd_RecursiveDeref(dd, x);
1444 Cudd_RecursiveDeref(dd, Isub1);
1445 /* sum = term0 + term1 */
1446 sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
1447 sum = Cudd_NotCond(sum, sum != NULL);
1448 if (sum == NULL) {
1449 Cudd_RecursiveDeref(dd, Id);
1450 Cudd_RecursiveDeref(dd, term0);
1451 Cudd_RecursiveDeref(dd, term1);
1452 return(NULL);
1453 }
1454 Cudd_Ref(sum);
1455 Cudd_RecursiveDeref(dd, term0);
1456 Cudd_RecursiveDeref(dd, term1);
1457 /* r = sum + Id */
1458 r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
1459 r = Cudd_NotCond(r, r != NULL);
1460 if (r == NULL) {
1461 Cudd_RecursiveDeref(dd, Id);
1462 Cudd_RecursiveDeref(dd, sum);
1463 return(NULL);
1464 }
1465 Cudd_Ref(r);
1466 Cudd_RecursiveDeref(dd, sum);
1467 Cudd_RecursiveDeref(dd, Id);
1468
1469 cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
1470 *pnCubes = Count0 + Count1 + Count2;
1471 if ( st__add_direct( table, (char *)r, (char *)(ABC_PTRINT_T)*pnCubes ) == st__OUT_OF_MEM )
1472 {
1473 Cudd_RecursiveDeref( dd, r );
1474 return NULL;
1475 }
1476 if ( *pnCubes > Limit )
1477 {
1478 Cudd_RecursiveDeref( dd, r );
1479 return NULL;
1480 }
1481 //printf( "%d ", *pnCubes );
1482 Cudd_Deref(r);
1483 return r;
1484 }
Extra_bddCountCubes(DdManager * dd,DdNode ** pFuncs,int nFuncs,int fMode,int nLimit,int * pGuide)1485 int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fMode, int nLimit, int * pGuide )
1486 {
1487 DdNode * pF0, * pF1;
1488 int i, Count, Count0, Count1, CounterAll = 0;
1489 st__table *table = st__init_table( st__ptrcmp, st__ptrhash );
1490 unsigned int saveLimit = dd->maxLive;
1491 dd->maxLive = dd->keys - dd->dead + 1000000; // limit on intermediate BDD nodes
1492 for ( i = 0; i < nFuncs; i++ )
1493 {
1494 if ( !pFuncs[i] )
1495 continue;
1496 pF1 = pF0 = NULL;
1497 Count0 = Count1 = nLimit;
1498 if ( fMode == -1 || fMode == 1 ) // both or pos
1499 pF1 = extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count1, nLimit );
1500 pFuncs[i] = Cudd_Not( pFuncs[i] );
1501 if ( fMode == -1 || fMode == 0 ) // both or neg
1502 pF0 = extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count0, Count1 );
1503 pFuncs[i] = Cudd_Not( pFuncs[i] );
1504 if ( !pF1 && !pF0 )
1505 break;
1506 if ( !pF0 ) pGuide[i] = 1, Count = Count1; // use pos
1507 else if ( !pF1 ) pGuide[i] = 0, Count = Count0; // use neg
1508 else if ( Count1 <= Count0 ) pGuide[i] = 1, Count = Count1; // use pos
1509 else pGuide[i] = 0, Count = Count0; // use neg
1510 CounterAll += Count;
1511 //printf( "Output %5d has %5d cubes (%d) (%5d and %5d)\n", nOuts++, Count, pGuide[i], Count1, Count0 );
1512 }
1513 dd->maxLive = saveLimit;
1514 st__free_table( table );
1515 return i == nFuncs ? CounterAll : -1;
1516 } /* end of Extra_bddCountCubes */
1517
1518 /*---------------------------------------------------------------------------*/
1519 /* Definition of static Functions */
1520 /*---------------------------------------------------------------------------*/
1521
1522 /**Function********************************************************************
1523
1524 Synopsis [Convert a BDD from a manager to another one.]
1525
1526 Description [Convert a BDD from a manager to another one. Returns a
1527 pointer to the BDD in the destination manager if successful; NULL
1528 otherwise.]
1529
1530 SideEffects [None]
1531
1532 SeeAlso [Extra_TransferPermute]
1533
1534 ******************************************************************************/
extraTransferPermute(DdManager * ddS,DdManager * ddD,DdNode * f,int * Permute)1535 DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute )
1536 {
1537 DdNode *res;
1538 st__table *table = NULL;
1539 st__generator *gen = NULL;
1540 DdNode *key, *value;
1541
1542 table = st__init_table( st__ptrcmp, st__ptrhash );
1543 if ( table == NULL )
1544 goto failure;
1545 res = extraTransferPermuteRecur( ddS, ddD, f, table, Permute );
1546 if ( res != NULL )
1547 cuddRef( res );
1548
1549 /* Dereference all elements in the table and dispose of the table.
1550 ** This must be done also if res is NULL to avoid leaks in case of
1551 ** reordering. */
1552 gen = st__init_gen( table );
1553 if ( gen == NULL )
1554 goto failure;
1555 while ( st__gen( gen, ( const char ** ) &key, ( char ** ) &value ) )
1556 {
1557 Cudd_RecursiveDeref( ddD, value );
1558 }
1559 st__free_gen( gen );
1560 gen = NULL;
1561 st__free_table( table );
1562 table = NULL;
1563
1564 if ( res != NULL )
1565 cuddDeref( res );
1566 return ( res );
1567
1568 failure:
1569 if ( table != NULL )
1570 st__free_table( table );
1571 if ( gen != NULL )
1572 st__free_gen( gen );
1573 return ( NULL );
1574
1575 } /* end of extraTransferPermute */
1576
1577
1578 /**Function********************************************************************
1579
1580 Synopsis [Performs the recursive step of Extra_TransferPermute.]
1581
1582 Description [Performs the recursive step of Extra_TransferPermute.
1583 Returns a pointer to the result if successful; NULL otherwise.]
1584
1585 SideEffects [None]
1586
1587 SeeAlso [extraTransferPermute]
1588
1589 ******************************************************************************/
1590 static DdNode *
extraTransferPermuteRecur(DdManager * ddS,DdManager * ddD,DdNode * f,st__table * table,int * Permute)1591 extraTransferPermuteRecur(
1592 DdManager * ddS,
1593 DdManager * ddD,
1594 DdNode * f,
1595 st__table * table,
1596 int * Permute )
1597 {
1598 DdNode *ft, *fe, *t, *e, *var, *res;
1599 DdNode *one, *zero;
1600 int index;
1601 int comple = 0;
1602
1603 statLine( ddD );
1604 one = DD_ONE( ddD );
1605 comple = Cudd_IsComplement( f );
1606
1607 /* Trivial cases. */
1608 if ( Cudd_IsConstant( f ) )
1609 return ( Cudd_NotCond( one, comple ) );
1610
1611
1612 /* Make canonical to increase the utilization of the cache. */
1613 f = Cudd_NotCond( f, comple );
1614 /* Now f is a regular pointer to a non-constant node. */
1615
1616 /* Check the cache. */
1617 if ( st__lookup( table, ( char * ) f, ( char ** ) &res ) )
1618 return ( Cudd_NotCond( res, comple ) );
1619
1620 if ( ddS->TimeStop && Abc_Clock() > ddS->TimeStop )
1621 return NULL;
1622 if ( ddD->TimeStop && Abc_Clock() > ddD->TimeStop )
1623 return NULL;
1624
1625 /* Recursive step. */
1626 if ( Permute )
1627 index = Permute[f->index];
1628 else
1629 index = f->index;
1630
1631 ft = cuddT( f );
1632 fe = cuddE( f );
1633
1634 t = extraTransferPermuteRecur( ddS, ddD, ft, table, Permute );
1635 if ( t == NULL )
1636 {
1637 return ( NULL );
1638 }
1639 cuddRef( t );
1640
1641 e = extraTransferPermuteRecur( ddS, ddD, fe, table, Permute );
1642 if ( e == NULL )
1643 {
1644 Cudd_RecursiveDeref( ddD, t );
1645 return ( NULL );
1646 }
1647 cuddRef( e );
1648
1649 zero = Cudd_Not(ddD->one);
1650 var = cuddUniqueInter( ddD, index, one, zero );
1651 if ( var == NULL )
1652 {
1653 Cudd_RecursiveDeref( ddD, t );
1654 Cudd_RecursiveDeref( ddD, e );
1655 return ( NULL );
1656 }
1657 res = cuddBddIteRecur( ddD, var, t, e );
1658
1659 if ( res == NULL )
1660 {
1661 Cudd_RecursiveDeref( ddD, t );
1662 Cudd_RecursiveDeref( ddD, e );
1663 return ( NULL );
1664 }
1665 cuddRef( res );
1666 Cudd_RecursiveDeref( ddD, t );
1667 Cudd_RecursiveDeref( ddD, e );
1668
1669 if ( st__add_direct( table, ( char * ) f, ( char * ) res ) ==
1670 st__OUT_OF_MEM )
1671 {
1672 Cudd_RecursiveDeref( ddD, res );
1673 return ( NULL );
1674 }
1675 return ( Cudd_NotCond( res, comple ) );
1676
1677 } /* end of extraTransferPermuteRecur */
1678
1679 /**Function********************************************************************
1680
1681 Synopsis [Performs the recursive step of Cudd_Support.]
1682
1683 Description [Performs the recursive step of Cudd_Support. Performs a
1684 DFS from f. The support is accumulated in supp as a side effect. Uses
1685 the LSB of the then pointer as visited flag.]
1686
1687 SideEffects [None]
1688
1689 SeeAlso [ddClearFlag]
1690
1691 ******************************************************************************/
1692 void
ddSupportStep2(DdNode * f,int * support)1693 ddSupportStep2(
1694 DdNode * f,
1695 int * support)
1696 {
1697 if (cuddIsConstant(f) || Cudd_IsComplement(f->next)) {
1698 return;
1699 }
1700
1701 support[f->index] = 1;
1702 ddSupportStep2(cuddT(f),support);
1703 ddSupportStep2(Cudd_Regular(cuddE(f)),support);
1704 /* Mark as visited. */
1705 f->next = Cudd_Not(f->next);
1706 return;
1707
1708 } /* end of ddSupportStep */
1709
1710
1711 /**Function********************************************************************
1712
1713 Synopsis [Performs a DFS from f, clearing the LSB of the next
1714 pointers.]
1715
1716 Description []
1717
1718 SideEffects [None]
1719
1720 SeeAlso [ddSupportStep ddDagInt]
1721
1722 ******************************************************************************/
1723 void
ddClearFlag2(DdNode * f)1724 ddClearFlag2(
1725 DdNode * f)
1726 {
1727 if (!Cudd_IsComplement(f->next)) {
1728 return;
1729 }
1730 /* Clear visited flag. */
1731 f->next = Cudd_Regular(f->next);
1732 if (cuddIsConstant(f)) {
1733 return;
1734 }
1735 ddClearFlag2(cuddT(f));
1736 ddClearFlag2(Cudd_Regular(cuddE(f)));
1737 return;
1738
1739 } /* end of ddClearFlag */
1740
1741
1742 /**Function********************************************************************
1743
1744 Synopsis [Composed three subcovers into one ZDD.]
1745
1746 Description []
1747
1748 SideEffects [None]
1749
1750 SeeAlso []
1751
1752 ******************************************************************************/
1753 DdNode *
extraComposeCover(DdManager * dd,DdNode * zC0,DdNode * zC1,DdNode * zC2,int TopVar)1754 extraComposeCover(
1755 DdManager* dd, /* the manager */
1756 DdNode* zC0, /* the pointer to the negative var cofactor */
1757 DdNode* zC1, /* the pointer to the positive var cofactor */
1758 DdNode* zC2, /* the pointer to the cofactor without var */
1759 int TopVar) /* the index of the positive ZDD var */
1760 {
1761 DdNode * zRes, * zTemp;
1762 /* compose with-neg-var and without-var using the neg ZDD var */
1763 zTemp = cuddZddGetNode( dd, 2*TopVar + 1, zC0, zC2 );
1764 if ( zTemp == NULL )
1765 {
1766 Cudd_RecursiveDerefZdd(dd, zC0);
1767 Cudd_RecursiveDerefZdd(dd, zC1);
1768 Cudd_RecursiveDerefZdd(dd, zC2);
1769 return NULL;
1770 }
1771 cuddRef( zTemp );
1772 cuddDeref( zC0 );
1773 cuddDeref( zC2 );
1774
1775 /* compose with-pos-var and previous result using the pos ZDD var */
1776 zRes = cuddZddGetNode( dd, 2*TopVar, zC1, zTemp );
1777 if ( zRes == NULL )
1778 {
1779 Cudd_RecursiveDerefZdd(dd, zC1);
1780 Cudd_RecursiveDerefZdd(dd, zTemp);
1781 return NULL;
1782 }
1783 cuddDeref( zC1 );
1784 cuddDeref( zTemp );
1785 return zRes;
1786 } /* extraComposeCover */
1787
1788 /**Function********************************************************************
1789
1790 Synopsis [Performs the recursive step of prime computation.]
1791
1792 Description []
1793
1794 SideEffects []
1795
1796 SeeAlso []
1797
1798 ******************************************************************************/
extraZddPrimes(DdManager * dd,DdNode * F)1799 DdNode* extraZddPrimes( DdManager *dd, DdNode* F )
1800 {
1801 DdNode *zRes;
1802
1803 if ( F == Cudd_Not( dd->one ) )
1804 return dd->zero;
1805 if ( F == dd->one )
1806 return dd->one;
1807
1808 /* check cache */
1809 zRes = cuddCacheLookup1Zdd(dd, extraZddPrimes, F);
1810 if (zRes)
1811 return(zRes);
1812 {
1813 /* temporary variables */
1814 DdNode *bF01, *zP0, *zP1;
1815 /* three components of the prime set */
1816 DdNode *zResE, *zResP, *zResN;
1817 int fIsComp = Cudd_IsComplement( F );
1818
1819 /* find cofactors of F */
1820 DdNode * bF0 = Cudd_NotCond( Cudd_E( F ), fIsComp );
1821 DdNode * bF1 = Cudd_NotCond( Cudd_T( F ), fIsComp );
1822
1823 /* find the intersection of cofactors */
1824 bF01 = cuddBddAndRecur( dd, bF0, bF1 );
1825 if ( bF01 == NULL ) return NULL;
1826 cuddRef( bF01 );
1827
1828 /* solve the problems for cofactors */
1829 zP0 = extraZddPrimes( dd, bF0 );
1830 if ( zP0 == NULL )
1831 {
1832 Cudd_RecursiveDeref( dd, bF01 );
1833 return NULL;
1834 }
1835 cuddRef( zP0 );
1836
1837 zP1 = extraZddPrimes( dd, bF1 );
1838 if ( zP1 == NULL )
1839 {
1840 Cudd_RecursiveDeref( dd, bF01 );
1841 Cudd_RecursiveDerefZdd( dd, zP0 );
1842 return NULL;
1843 }
1844 cuddRef( zP1 );
1845
1846 /* check for local unateness */
1847 if ( bF01 == bF0 ) /* unate increasing */
1848 {
1849 /* intersection is useless */
1850 cuddDeref( bF01 );
1851 /* the primes of intersection are the primes of F0 */
1852 zResE = zP0;
1853 /* there are no primes with negative var */
1854 zResN = dd->zero;
1855 cuddRef( zResN );
1856 /* primes with positive var are primes of F1 that are not primes of F01 */
1857 zResP = cuddZddDiff( dd, zP1, zP0 );
1858 if ( zResP == NULL )
1859 {
1860 Cudd_RecursiveDerefZdd( dd, zResE );
1861 Cudd_RecursiveDerefZdd( dd, zResN );
1862 Cudd_RecursiveDerefZdd( dd, zP1 );
1863 return NULL;
1864 }
1865 cuddRef( zResP );
1866 Cudd_RecursiveDerefZdd( dd, zP1 );
1867 }
1868 else if ( bF01 == bF1 ) /* unate decreasing */
1869 {
1870 /* intersection is useless */
1871 cuddDeref( bF01 );
1872 /* the primes of intersection are the primes of F1 */
1873 zResE = zP1;
1874 /* there are no primes with positive var */
1875 zResP = dd->zero;
1876 cuddRef( zResP );
1877 /* primes with negative var are primes of F0 that are not primes of F01 */
1878 zResN = cuddZddDiff( dd, zP0, zP1 );
1879 if ( zResN == NULL )
1880 {
1881 Cudd_RecursiveDerefZdd( dd, zResE );
1882 Cudd_RecursiveDerefZdd( dd, zResP );
1883 Cudd_RecursiveDerefZdd( dd, zP0 );
1884 return NULL;
1885 }
1886 cuddRef( zResN );
1887 Cudd_RecursiveDerefZdd( dd, zP0 );
1888 }
1889 else /* not unate */
1890 {
1891 /* primes without the top var are primes of F10 */
1892 zResE = extraZddPrimes( dd, bF01 );
1893 if ( zResE == NULL )
1894 {
1895 Cudd_RecursiveDerefZdd( dd, bF01 );
1896 Cudd_RecursiveDerefZdd( dd, zP0 );
1897 Cudd_RecursiveDerefZdd( dd, zP1 );
1898 return NULL;
1899 }
1900 cuddRef( zResE );
1901 Cudd_RecursiveDeref( dd, bF01 );
1902
1903 /* primes with the negative top var are those of P0 that are not in F10 */
1904 zResN = cuddZddDiff( dd, zP0, zResE );
1905 if ( zResN == NULL )
1906 {
1907 Cudd_RecursiveDerefZdd( dd, zResE );
1908 Cudd_RecursiveDerefZdd( dd, zP0 );
1909 Cudd_RecursiveDerefZdd( dd, zP1 );
1910 return NULL;
1911 }
1912 cuddRef( zResN );
1913 Cudd_RecursiveDerefZdd( dd, zP0 );
1914
1915 /* primes with the positive top var are those of P1 that are not in F10 */
1916 zResP = cuddZddDiff( dd, zP1, zResE );
1917 if ( zResP == NULL )
1918 {
1919 Cudd_RecursiveDerefZdd( dd, zResE );
1920 Cudd_RecursiveDerefZdd( dd, zResN );
1921 Cudd_RecursiveDerefZdd( dd, zP1 );
1922 return NULL;
1923 }
1924 cuddRef( zResP );
1925 Cudd_RecursiveDerefZdd( dd, zP1 );
1926 }
1927
1928 zRes = extraComposeCover( dd, zResN, zResP, zResE, Cudd_Regular(F)->index );
1929 if ( zRes == NULL ) return NULL;
1930
1931 /* insert the result into cache */
1932 cuddCacheInsert1(dd, extraZddPrimes, F, zRes);
1933 return zRes;
1934 }
1935 } /* end of extraZddPrimes */
1936
1937 /**Function********************************************************************
1938
1939 Synopsis [Implements the recursive step of Cudd_bddPermute.]
1940
1941 Description [ Recursively puts the BDD in the order given in the array permut.
1942 Checks for trivial cases to terminate recursion, then splits on the
1943 children of this node. Once the solutions for the children are
1944 obtained, it puts into the current position the node from the rest of
1945 the BDD that should be here. Then returns this BDD.
1946 The key here is that the node being visited is NOT put in its proper
1947 place by this instance, but rather is switched when its proper position
1948 is reached in the recursion tree.<p>
1949 The DdNode * that is returned is the same BDD as passed in as node,
1950 but in the new order.]
1951
1952 SideEffects [None]
1953
1954 SeeAlso [Cudd_bddPermute cuddAddPermuteRecur]
1955
1956 ******************************************************************************/
1957 static DdNode *
cuddBddPermuteRecur(DdManager * manager,DdHashTable * table,DdNode * node,int * permut)1958 cuddBddPermuteRecur( DdManager * manager /* DD manager */ ,
1959 DdHashTable * table /* computed table */ ,
1960 DdNode * node /* BDD to be reordered */ ,
1961 int *permut /* permutation array */ )
1962 {
1963 DdNode *N, *T, *E;
1964 DdNode *res;
1965 int index;
1966
1967 statLine( manager );
1968 N = Cudd_Regular( node );
1969
1970 /* Check for terminal case of constant node. */
1971 if ( cuddIsConstant( N ) )
1972 {
1973 return ( node );
1974 }
1975
1976 /* If problem already solved, look up answer and return. */
1977 if ( N->ref != 1 && ( res = cuddHashTableLookup1( table, N ) ) != NULL )
1978 {
1979 return ( Cudd_NotCond( res, N != node ) );
1980 }
1981
1982 /* Split and recur on children of this node. */
1983 T = cuddBddPermuteRecur( manager, table, cuddT( N ), permut );
1984 if ( T == NULL )
1985 return ( NULL );
1986 cuddRef( T );
1987 E = cuddBddPermuteRecur( manager, table, cuddE( N ), permut );
1988 if ( E == NULL )
1989 {
1990 Cudd_IterDerefBdd( manager, T );
1991 return ( NULL );
1992 }
1993 cuddRef( E );
1994
1995 /* Move variable that should be in this position to this position
1996 ** by retrieving the single var BDD for that variable, and calling
1997 ** cuddBddIteRecur with the T and E we just created.
1998 */
1999 index = permut[N->index];
2000 res = cuddBddIteRecur( manager, manager->vars[index], T, E );
2001 if ( res == NULL )
2002 {
2003 Cudd_IterDerefBdd( manager, T );
2004 Cudd_IterDerefBdd( manager, E );
2005 return ( NULL );
2006 }
2007 cuddRef( res );
2008 Cudd_IterDerefBdd( manager, T );
2009 Cudd_IterDerefBdd( manager, E );
2010
2011 /* Do not keep the result if the reference count is only 1, since
2012 ** it will not be visited again.
2013 */
2014 if ( N->ref != 1 )
2015 {
2016 ptrint fanout = ( ptrint ) N->ref;
2017 cuddSatDec( fanout );
2018 if ( !cuddHashTableInsert1( table, N, res, fanout ) )
2019 {
2020 Cudd_IterDerefBdd( manager, res );
2021 return ( NULL );
2022 }
2023 }
2024 cuddDeref( res );
2025 return ( Cudd_NotCond( res, N != node ) );
2026
2027 } /* end of cuddBddPermuteRecur */
2028
2029
2030 /**Function********************************************************************
2031
2032 Synopsis [Performs the reordering-sensitive step of Extra_bddChangePolarity().]
2033
2034 Description []
2035
2036 SideEffects []
2037
2038 SeeAlso []
2039
2040 ******************************************************************************/
extraBddChangePolarity(DdManager * dd,DdNode * bFunc,DdNode * bVars)2041 DdNode * extraBddChangePolarity(
2042 DdManager * dd, /* the DD manager */
2043 DdNode * bFunc,
2044 DdNode * bVars)
2045 {
2046 DdNode * bRes;
2047
2048 if ( bVars == b1 )
2049 return bFunc;
2050 if ( Cudd_IsConstant(bFunc) )
2051 return bFunc;
2052
2053 if ( (bRes = cuddCacheLookup2(dd, extraBddChangePolarity, bFunc, bVars)) )
2054 return bRes;
2055 else
2056 {
2057 DdNode * bFR = Cudd_Regular(bFunc);
2058 int LevelF = dd->perm[bFR->index];
2059 int LevelV = dd->perm[bVars->index];
2060
2061 if ( LevelV < LevelF )
2062 bRes = extraBddChangePolarity( dd, bFunc, cuddT(bVars) );
2063 else // if ( LevelF <= LevelV )
2064 {
2065 DdNode * bRes0, * bRes1;
2066 DdNode * bF0, * bF1;
2067 DdNode * bVarsNext;
2068
2069 // cofactor the functions
2070 if ( bFR != bFunc ) // bFunc is complemented
2071 {
2072 bF0 = Cudd_Not( cuddE(bFR) );
2073 bF1 = Cudd_Not( cuddT(bFR) );
2074 }
2075 else
2076 {
2077 bF0 = cuddE(bFR);
2078 bF1 = cuddT(bFR);
2079 }
2080
2081 if ( LevelF == LevelV )
2082 bVarsNext = cuddT(bVars);
2083 else
2084 bVarsNext = bVars;
2085
2086 bRes0 = extraBddChangePolarity( dd, bF0, bVarsNext );
2087 if ( bRes0 == NULL )
2088 return NULL;
2089 cuddRef( bRes0 );
2090
2091 bRes1 = extraBddChangePolarity( dd, bF1, bVarsNext );
2092 if ( bRes1 == NULL )
2093 {
2094 Cudd_RecursiveDeref( dd, bRes0 );
2095 return NULL;
2096 }
2097 cuddRef( bRes1 );
2098
2099 if ( LevelF == LevelV )
2100 { // swap the cofactors
2101 DdNode * bTemp;
2102 bTemp = bRes0;
2103 bRes0 = bRes1;
2104 bRes1 = bTemp;
2105 }
2106
2107 /* only aRes0 and aRes1 are referenced at this point */
2108
2109 /* consider the case when Res0 and Res1 are the same node */
2110 if ( bRes0 == bRes1 )
2111 bRes = bRes1;
2112 /* consider the case when Res1 is complemented */
2113 else if ( Cudd_IsComplement(bRes1) )
2114 {
2115 bRes = cuddUniqueInter(dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0));
2116 if ( bRes == NULL )
2117 {
2118 Cudd_RecursiveDeref(dd,bRes0);
2119 Cudd_RecursiveDeref(dd,bRes1);
2120 return NULL;
2121 }
2122 bRes = Cudd_Not(bRes);
2123 }
2124 else
2125 {
2126 bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
2127 if ( bRes == NULL )
2128 {
2129 Cudd_RecursiveDeref(dd,bRes0);
2130 Cudd_RecursiveDeref(dd,bRes1);
2131 return NULL;
2132 }
2133 }
2134 cuddDeref( bRes0 );
2135 cuddDeref( bRes1 );
2136 }
2137
2138 /* insert the result into cache */
2139 cuddCacheInsert2(dd, extraBddChangePolarity, bFunc, bVars, bRes);
2140 return bRes;
2141 }
2142 } /* end of extraBddChangePolarity */
2143
2144
2145
2146 static int Counter = 0;
2147
2148 /**Function*************************************************************
2149
2150 Synopsis [Computes the AND of two BDD with different orders.]
2151
2152 Description []
2153
2154 SideEffects []
2155
2156 SeeAlso []
2157
2158 ***********************************************************************/
extraBddAndPermute(DdHashTable * table,DdManager * ddF,DdNode * bF,DdManager * ddG,DdNode * bG,int * pPermute)2159 DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute )
2160 {
2161 DdNode * bF0, * bF1, * bG0, * bG1, * bRes0, * bRes1, * bRes, * bVar;
2162 int LevF, LevG, Lev;
2163
2164 // if F == 0, return 0
2165 if ( bF == Cudd_Not(ddF->one) )
2166 return Cudd_Not(ddF->one);
2167 // if G == 0, return 0
2168 if ( bG == Cudd_Not(ddG->one) )
2169 return Cudd_Not(ddF->one);
2170 // if G == 1, return F
2171 if ( bG == ddG->one )
2172 return bF;
2173 // cannot use F == 1, because the var order of G has to be changed
2174
2175 // check cache
2176 if ( //(Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1) &&
2177 (bRes = cuddHashTableLookup2(table, bF, bG)) )
2178 return bRes;
2179 Counter++;
2180
2181 if ( ddF->TimeStop && Abc_Clock() > ddF->TimeStop )
2182 return NULL;
2183 if ( ddG->TimeStop && Abc_Clock() > ddG->TimeStop )
2184 return NULL;
2185
2186 // find the topmost variable in F and G using var order of F
2187 LevF = cuddI( ddF, Cudd_Regular(bF)->index );
2188 LevG = cuddI( ddF, pPermute ? pPermute[Cudd_Regular(bG)->index] : Cudd_Regular(bG)->index );
2189 Lev = Abc_MinInt( LevF, LevG );
2190 assert( Lev < ddF->size );
2191 bVar = ddF->vars[ddF->invperm[Lev]];
2192
2193 // cofactor
2194 bF0 = (Lev < LevF) ? bF : Cudd_NotCond( cuddE(Cudd_Regular(bF)), Cudd_IsComplement(bF) );
2195 bF1 = (Lev < LevF) ? bF : Cudd_NotCond( cuddT(Cudd_Regular(bF)), Cudd_IsComplement(bF) );
2196 bG0 = (Lev < LevG) ? bG : Cudd_NotCond( cuddE(Cudd_Regular(bG)), Cudd_IsComplement(bG) );
2197 bG1 = (Lev < LevG) ? bG : Cudd_NotCond( cuddT(Cudd_Regular(bG)), Cudd_IsComplement(bG) );
2198
2199 // call for cofactors
2200 bRes0 = extraBddAndPermute( table, ddF, bF0, ddG, bG0, pPermute );
2201 if ( bRes0 == NULL )
2202 return NULL;
2203 cuddRef( bRes0 );
2204 // call for cofactors
2205 bRes1 = extraBddAndPermute( table, ddF, bF1, ddG, bG1, pPermute );
2206 if ( bRes1 == NULL )
2207 {
2208 Cudd_IterDerefBdd( ddF, bRes0 );
2209 return NULL;
2210 }
2211 cuddRef( bRes1 );
2212
2213 // compose the result
2214 bRes = cuddBddIteRecur( ddF, bVar, bRes1, bRes0 );
2215 if ( bRes == NULL )
2216 {
2217 Cudd_IterDerefBdd( ddF, bRes0 );
2218 Cudd_IterDerefBdd( ddF, bRes1 );
2219 return NULL;
2220 }
2221 cuddRef( bRes );
2222 Cudd_IterDerefBdd( ddF, bRes0 );
2223 Cudd_IterDerefBdd( ddF, bRes1 );
2224
2225 // cache the result
2226 // if ( Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1 )
2227 {
2228 ptrint fanout = (ptrint)Cudd_Regular(bF)->ref * Cudd_Regular(bG)->ref;
2229 cuddSatDec(fanout);
2230 cuddHashTableInsert2( table, bF, bG, bRes, fanout );
2231 }
2232 cuddDeref( bRes );
2233 return bRes;
2234 }
2235
2236 /**Function*************************************************************
2237
2238 Synopsis [Testbench.]
2239
2240 Description [This procedure takes BDD manager ddF and two BDDs
2241 in this manager (bF and bG). It creates a new manager ddG,
2242 transfers bG into it and then reorders it, resulting in bG2.
2243 Then it tries to compute the product of bF and bG2 in ddF.]
2244
2245 SideEffects []
2246
2247 SeeAlso []
2248
2249 ***********************************************************************/
Extra_TestAndPerm(DdManager * ddF,DdNode * bF,DdNode * bG)2250 void Extra_TestAndPerm( DdManager * ddF, DdNode * bF, DdNode * bG )
2251 {
2252 DdManager * ddG;
2253 DdNode * bG2, * bRes1, * bRes2;
2254 abctime clk;
2255 // disable variable ordering in ddF
2256 Cudd_AutodynDisable( ddF );
2257
2258 // create new BDD manager
2259 ddG = Cudd_Init( ddF->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
2260 // transfer BDD into it
2261 Cudd_ShuffleHeap( ddG, ddF->invperm );
2262 bG2 = Extra_TransferLevelByLevel( ddF, ddG, bG ); Cudd_Ref( bG2 );
2263 // reorder the new manager
2264 Cudd_ReduceHeap( ddG, CUDD_REORDER_SYMM_SIFT, 1 );
2265
2266 // compute the result
2267 clk = Abc_Clock();
2268 bRes1 = Cudd_bddAnd( ddF, bF, bG ); Cudd_Ref( bRes1 );
2269 Abc_PrintTime( 1, "Runtime of Cudd_bddAnd ", Abc_Clock() - clk );
2270
2271 // compute the result
2272 Counter = 0;
2273 clk = Abc_Clock();
2274 bRes2 = Extra_bddAndPermute( ddF, bF, ddG, bG2, NULL ); Cudd_Ref( bRes2 );
2275 Abc_PrintTime( 1, "Runtime of new procedure", Abc_Clock() - clk );
2276 printf( "Recursive calls = %d\n", Counter );
2277 printf( "|F| =%6d |G| =%6d |H| =%6d |F|*|G| =%9d ",
2278 Cudd_DagSize(bF), Cudd_DagSize(bG), Cudd_DagSize(bRes2),
2279 Cudd_DagSize(bF) * Cudd_DagSize(bG) );
2280
2281 if ( bRes1 == bRes2 )
2282 printf( "Result verified.\n\n" );
2283 else
2284 printf( "Result is incorrect.\n\n" );
2285
2286 Cudd_RecursiveDeref( ddF, bRes1 );
2287 Cudd_RecursiveDeref( ddF, bRes2 );
2288 // quit the new manager
2289 Cudd_RecursiveDeref( ddG, bG2 );
2290 Extra_StopManager( ddG );
2291
2292 // re-enable variable ordering in ddF
2293 Cudd_AutodynEnable( ddF, CUDD_REORDER_SYMM_SIFT );
2294 }
2295
2296 /**Function*************************************************************
2297
2298 Synopsis [Writes ZDD into a PLA file.]
2299
2300 Description []
2301
2302 SideEffects []
2303
2304 SeeAlso []
2305
2306 ***********************************************************************/
Extra_zddDumpPla(DdManager * dd,DdNode * F,int nVars,char * pFileName)2307 void Extra_zddDumpPla( DdManager * dd, DdNode * F, int nVars, char * pFileName )
2308 {
2309 DdGen *gen;
2310 char * pCube;
2311 int * pPath, i;
2312 FILE * pFile = fopen( pFileName, "wb" );
2313 if ( pFile == NULL )
2314 {
2315 printf( "Cannot open file \"%s\" for writing.\n", pFileName );
2316 return;
2317 }
2318 fprintf( pFile, "# PLA file dumped by Extra_zddDumpPla() in ABC\n" );
2319 fprintf( pFile, ".i %d\n", nVars );
2320 fprintf( pFile, ".o 1\n" );
2321 pCube = ABC_CALLOC( char, dd->sizeZ );
2322 Cudd_zddForeachPath( dd, F, gen, pPath )
2323 {
2324 for ( i = 0; i < nVars; i++ )
2325 pCube[i] = '-';
2326 for ( i = 0; i < nVars; i++ )
2327 if ( pPath[2*i] == 1 || pPath[2*i+1] == 1 )
2328 pCube[i] = '0' + (pPath[2*i] == 1);
2329 fprintf( pFile, "%s 1\n", pCube );
2330 }
2331 fprintf( pFile, ".e\n\n" );
2332 fclose( pFile );
2333 ABC_FREE( pCube );
2334 }
2335
2336 /**Function*************************************************************
2337
2338 Synopsis [Constructing ZDD of a graph.]
2339
2340 Description []
2341
2342 SideEffects []
2343
2344 SeeAlso []
2345
2346 ***********************************************************************/
Extra_GraphExperiment()2347 void Extra_GraphExperiment()
2348 {
2349 int Edges[5][5] = {
2350 {1, 3, 4},
2351 {1, 5},
2352 {2, 3, 5},
2353 {2, 4}
2354 };
2355 int e, n;
2356
2357 DdManager * dd = Cudd_Init( 0, 6, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
2358
2359 // create the edges
2360 DdNode * zGraph, * zEdge, * zVar, * zTemp;
2361 zGraph = DD_ZERO(dd); Cudd_Ref( zGraph );
2362 for ( e = 0; Edges[e][0]; e++ )
2363 {
2364 zEdge = DD_ONE(dd); Cudd_Ref( zEdge );
2365 for ( n = 0; Edges[e][n]; n++ )
2366 {
2367 zVar = cuddZddGetNode( dd, Edges[e][n], DD_ONE(dd), DD_ZERO(dd) ); Cudd_Ref( zVar );
2368 zEdge = Cudd_zddUnateProduct( dd, zTemp = zEdge, zVar ); Cudd_Ref( zEdge );
2369 Cudd_RecursiveDerefZdd( dd, zTemp );
2370 Cudd_RecursiveDerefZdd( dd, zVar );
2371 }
2372 zGraph = Cudd_zddUnion( dd, zTemp = zGraph, zEdge ); Cudd_Ref( zGraph );
2373 Cudd_RecursiveDerefZdd( dd, zTemp );
2374 Cudd_RecursiveDerefZdd( dd, zEdge );
2375 }
2376
2377 Cudd_zddPrintMinterm( dd, zGraph );
2378
2379 Cudd_RecursiveDerefZdd( dd, zGraph );
2380 Cudd_Quit(dd);
2381 }
2382
2383
2384
2385
2386 /**Function********************************************************************
2387
2388 Synopsis [Performs the reordering-sensitive step of Extra_zddCombination().]
2389
2390 Description [Generates in a bottom-up fashion ZDD for one combination
2391 whose var values are given in the array VarValues. If necessary,
2392 creates new variables on the fly.]
2393
2394 SideEffects []
2395
2396 SeeAlso []
2397
2398 ******************************************************************************/
extraZddCombination(DdManager * dd,int * VarValues,int nVars)2399 DdNode * extraZddCombination(
2400 DdManager* dd,
2401 int* VarValues,
2402 int nVars )
2403 {
2404 int lev, index;
2405 DdNode *zRes, *zTemp;
2406
2407 /* transform the combination from the array VarValues into a ZDD cube. */
2408 zRes = dd->one;
2409 cuddRef(zRes);
2410
2411 /* go through levels starting bottom-up and create nodes
2412 * if these variables are present in the comb
2413 */
2414 for (lev = nVars - 1; lev >= 0; lev--)
2415 {
2416 index = (lev >= dd->sizeZ) ? lev : dd->invpermZ[lev];
2417 if (VarValues[index] == 1)
2418 {
2419 /* compose zRes with ZERO for the given ZDD variable */
2420 zRes = cuddZddGetNode( dd, index, zTemp = zRes, dd->zero );
2421 if ( zRes == NULL )
2422 {
2423 Cudd_RecursiveDerefZdd( dd, zTemp );
2424 return NULL;
2425 }
2426 cuddRef( zRes );
2427 cuddDeref( zTemp );
2428 }
2429 }
2430 cuddDeref( zRes );
2431 return zRes;
2432
2433 } /* end of extraZddCombination */
2434
2435 /**Function********************************************************************
2436
2437 Synopsis [Creates ZDD of the combination containing given variables.]
2438
2439 Description [Creates ZDD of the combination containing given variables.
2440 VarValues contains 1 for a variable that belongs to the
2441 combination and 0 for a varible that does not belong.
2442 nVars is number of ZDD variables in the array.]
2443
2444 SideEffects [New ZDD variables are created if indices of the variables
2445 present in the combination are larger than the currently
2446 allocated number of ZDD variables.]
2447
2448 SeeAlso []
2449
2450 ******************************************************************************/
Extra_zddCombination(DdManager * dd,int * VarValues,int nVars)2451 DdNode * Extra_zddCombination(
2452 DdManager *dd,
2453 int* VarValues,
2454 int nVars )
2455 {
2456 DdNode *res;
2457 do {
2458 dd->reordered = 0;
2459 res = extraZddCombination(dd, VarValues, nVars);
2460 } while (dd->reordered == 1);
2461 return(res);
2462
2463 } /* end of Extra_zddCombination */
2464
2465 /**Function********************************************************************
2466
2467 Synopsis [Generates a random set of combinations.]
2468
2469 Description [Given a set of n elements, each of which is encoded using one
2470 ZDD variable, this function generates a random set of k subsets
2471 (combinations of elements) with density d. Assumes that k and n
2472 are positive integers. Returns NULL if density is less than 0.0
2473 or more than 1.0.]
2474
2475 SideEffects [Allocates new ZDD variables if their current number is less than n.]
2476
2477 SeeAlso []
2478
2479 ******************************************************************************/
Extra_zddRandomSet(DdManager * dd,int n,int k,double d)2480 DdNode* Extra_zddRandomSet(
2481 DdManager * dd, /* the DD manager */
2482 int n, /* the number of elements */
2483 int k, /* the number of combinations (subsets) */
2484 double d) /* average density of elements in combinations */
2485 {
2486 DdNode *Result, *TempComb, *Aux;
2487 int c, v, Limit, *VarValues;
2488
2489 /* sanity check the parameters */
2490 if ( n <= 0 || k <= 0 || d < 0.0 || d > 1.0 )
2491 return NULL;
2492
2493 /* allocate temporary storage for variable values */
2494 VarValues = ABC_ALLOC( int, n );
2495 if (VarValues == NULL)
2496 {
2497 dd->errorCode = CUDD_MEMORY_OUT;
2498 return NULL;
2499 }
2500
2501 /* start the new set */
2502 Result = dd->zero;
2503 Cudd_Ref( Result );
2504
2505 /* seed random number generator */
2506 Cudd_Srandom( time(NULL) );
2507 // Cudd_Srandom( 4 );
2508 /* determine the limit below which var belongs to the combination */
2509 Limit = (int)(d * 2147483561.0);
2510
2511 /* add combinations one by one */
2512 for ( c = 0; c < k; c++ )
2513 {
2514 for ( v = 0; v < n; v++ )
2515 if ( Cudd_Random() <= Limit )
2516 VarValues[v] = 1;
2517 else
2518 VarValues[v] = 0;
2519
2520 TempComb = Extra_zddCombination( dd, VarValues, n );
2521 Cudd_Ref( TempComb );
2522
2523 /* make sure that this combination is not already in the set */
2524 if ( c )
2525 { /* at least one combination is already included */
2526
2527 Aux = Cudd_zddDiff( dd, Result, TempComb );
2528 Cudd_Ref( Aux );
2529 if ( Aux != Result )
2530 {
2531 Cudd_RecursiveDerefZdd( dd, Aux );
2532 Cudd_RecursiveDerefZdd( dd, TempComb );
2533 c--;
2534 continue;
2535 }
2536 else
2537 { /* Aux is the same node as Result */
2538 Cudd_Deref( Aux );
2539 }
2540 }
2541
2542 Result = Cudd_zddUnion( dd, Aux = Result, TempComb );
2543 Cudd_Ref( Result );
2544 Cudd_RecursiveDerefZdd( dd, Aux );
2545 Cudd_RecursiveDerefZdd( dd, TempComb );
2546 }
2547
2548 ABC_FREE( VarValues );
2549 Cudd_Deref( Result );
2550 return Result;
2551
2552 } /* end of Extra_zddRandomSet */
2553
2554 /**Function********************************************************************
2555
2556 Synopsis []
2557
2558 Description []
2559
2560 SideEffects []
2561
2562 SeeAlso []
2563
2564 ******************************************************************************/
Extra_ZddTest()2565 void Extra_ZddTest()
2566 {
2567 int N = 64;
2568 int K0 = 1000;
2569 int i, Size;
2570 DdManager * dd = Cudd_Init( 0, 32, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
2571 for ( i = 1; i <= 10; i++ )
2572 {
2573 int K = K0 * i;
2574 DdNode * zRandSet = Extra_zddRandomSet( dd, N, K, 0.5 ); Cudd_Ref(zRandSet);
2575 Size = Cudd_zddDagSize(zRandSet);
2576 //Cudd_zddPrintMinterm( dd, zRandSet );
2577 printf( "N = %5d K = %5d BddSize = %6d MemBdd = %8.3f MB MemBit = %8.3f MB Ratio = %8.3f %%\n",
2578 N, K, Size, 20.0*Size/(1<<20), 0.125 * N * K /(1<<20), 100.0*(0.125 * N * K)/(20.0*Size) );
2579 Cudd_RecursiveDerefZdd( dd, zRandSet );
2580 }
2581 Cudd_Quit(dd);
2582 }
2583
2584
2585 /**Function********************************************************************
2586
2587 Synopsis [Performs the reordering-sensitive step of Extra_bddTuples().]
2588
2589 Description [Generates in a bottom-up fashion BDD for all combinations
2590 composed of k variables out of variables belonging to bVarsN.]
2591
2592 SideEffects []
2593
2594 SeeAlso []
2595
2596 ******************************************************************************/
extraBddTuples(DdManager * dd,DdNode * bVarsK,DdNode * bVarsN)2597 DdNode * extraBddTuples(
2598 DdManager * dd, /* the DD manager */
2599 DdNode * bVarsK, /* the number of variables in tuples */
2600 DdNode * bVarsN) /* the set of all variables */
2601 {
2602 DdNode *bRes, *bRes0, *bRes1;
2603 statLine(dd);
2604
2605 /* terminal cases */
2606 /* if ( k < 0 || k > n )
2607 * return dd->zero;
2608 * if ( n == 0 )
2609 * return dd->one;
2610 */
2611 if ( cuddI( dd, bVarsK->index ) < cuddI( dd, bVarsN->index ) )
2612 return b0;
2613 if ( bVarsN == b1 )
2614 return b1;
2615
2616 /* check cache */
2617 bRes = cuddCacheLookup2(dd, extraBddTuples, bVarsK, bVarsN);
2618 if (bRes)
2619 return(bRes);
2620
2621 /* ZDD in which is variable is 0 */
2622 /* bRes0 = extraBddTuples( dd, k, n-1 ); */
2623 bRes0 = extraBddTuples( dd, bVarsK, cuddT(bVarsN) );
2624 if ( bRes0 == NULL )
2625 return NULL;
2626 cuddRef( bRes0 );
2627
2628 /* ZDD in which is variable is 1 */
2629 /* bRes1 = extraBddTuples( dd, k-1, n-1 ); */
2630 if ( bVarsK == b1 )
2631 {
2632 bRes1 = b0;
2633 cuddRef( bRes1 );
2634 }
2635 else
2636 {
2637 bRes1 = extraBddTuples( dd, cuddT(bVarsK), cuddT(bVarsN) );
2638 if ( bRes1 == NULL )
2639 {
2640 Cudd_RecursiveDeref( dd, bRes0 );
2641 return NULL;
2642 }
2643 cuddRef( bRes1 );
2644 }
2645
2646 /* consider the case when Res0 and Res1 are the same node */
2647 if ( bRes0 == bRes1 )
2648 bRes = bRes1;
2649 /* consider the case when Res1 is complemented */
2650 else if ( Cudd_IsComplement(bRes1) )
2651 {
2652 bRes = cuddUniqueInter(dd, bVarsN->index, Cudd_Not(bRes1), Cudd_Not(bRes0));
2653 if ( bRes == NULL )
2654 {
2655 Cudd_RecursiveDeref(dd,bRes0);
2656 Cudd_RecursiveDeref(dd,bRes1);
2657 return NULL;
2658 }
2659 bRes = Cudd_Not(bRes);
2660 }
2661 else
2662 {
2663 bRes = cuddUniqueInter( dd, bVarsN->index, bRes1, bRes0 );
2664 if ( bRes == NULL )
2665 {
2666 Cudd_RecursiveDeref(dd,bRes0);
2667 Cudd_RecursiveDeref(dd,bRes1);
2668 return NULL;
2669 }
2670 }
2671 cuddDeref( bRes0 );
2672 cuddDeref( bRes1 );
2673
2674 /* insert the result into cache */
2675 cuddCacheInsert2(dd, extraBddTuples, bVarsK, bVarsN, bRes);
2676 return bRes;
2677
2678 } /* end of extraBddTuples */
2679
2680 /**Function********************************************************************
2681
2682 Synopsis [Builds BDD representing the set of fixed-size variable tuples.]
2683
2684 Description [Creates BDD of all combinations of variables in Support that have k vars in them.]
2685
2686 SideEffects []
2687
2688 SeeAlso []
2689
2690 ******************************************************************************/
Extra_bddTuples(DdManager * dd,int K,DdNode * VarsN)2691 DdNode * Extra_bddTuples(
2692 DdManager * dd, /* the DD manager */
2693 int K, /* the number of variables in tuples */
2694 DdNode * VarsN) /* the set of all variables represented as a BDD */
2695 {
2696 DdNode *res;
2697 int autoDyn;
2698
2699 /* it is important that reordering does not happen,
2700 otherwise, this methods will not work */
2701
2702 autoDyn = dd->autoDyn;
2703 dd->autoDyn = 0;
2704
2705 do {
2706 /* transform the numeric arguments (K) into a DdNode * argument;
2707 * this allows us to use the standard internal CUDD cache */
2708 DdNode *VarSet = VarsN, *VarsK = VarsN;
2709 int nVars = 0, i;
2710
2711 /* determine the number of variables in VarSet */
2712 while ( VarSet != b1 )
2713 {
2714 nVars++;
2715 /* make sure that the VarSet is a cube */
2716 if ( cuddE( VarSet ) != b0 )
2717 return NULL;
2718 VarSet = cuddT( VarSet );
2719 }
2720 /* make sure that the number of variables in VarSet is less or equal
2721 that the number of variables that should be present in the tuples
2722 */
2723 if ( K > nVars )
2724 return NULL;
2725
2726 /* the second argument in the recursive call stands for <n>;
2727 * create the first argument, which stands for <k>
2728 * as when we are talking about the tuple of <k> out of <n> */
2729 for ( i = 0; i < nVars-K; i++ )
2730 VarsK = cuddT( VarsK );
2731
2732 dd->reordered = 0;
2733 res = extraBddTuples(dd, VarsK, VarsN );
2734
2735 } while (dd->reordered == 1);
2736 dd->autoDyn = autoDyn;
2737 return(res);
2738
2739 } /* end of Extra_bddTuples */
2740
2741
2742 ////////////////////////////////////////////////////////////////////////
2743 /// END OF FILE ///
2744 ////////////////////////////////////////////////////////////////////////
2745
2746
2747 ABC_NAMESPACE_IMPL_END
2748
2749