1 /**CFile****************************************************************
2 
3   FileName    [extraBddAuto.c]
4 
5   PackageName [extra]
6 
7   Synopsis    [Computation of autosymmetries.]
8 
9   Author      [Alan Mishchenko]
10 
11   Affiliation [UC Berkeley]
12 
13   Date        [Ver. 2.0. Started - September 1, 2003.]
14 
15   Revision    [$Id: extraBddAuto.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $]
16 
17 ***********************************************************************/
18 
19 #include "extraBdd.h"
20 
21 ABC_NAMESPACE_IMPL_START
22 
23 
24 /*---------------------------------------------------------------------------*/
25 /* Constant declarations                                                     */
26 /*---------------------------------------------------------------------------*/
27 
28 /*---------------------------------------------------------------------------*/
29 /* Stucture declarations                                                     */
30 /*---------------------------------------------------------------------------*/
31 
32 /*---------------------------------------------------------------------------*/
33 /* Type declarations                                                         */
34 /*---------------------------------------------------------------------------*/
35 
36 /*---------------------------------------------------------------------------*/
37 /* Variable declarations                                                     */
38 /*---------------------------------------------------------------------------*/
39 
40 /*---------------------------------------------------------------------------*/
41 /* Macro declarations                                                        */
42 /*---------------------------------------------------------------------------*/
43 
44 
45 /**AutomaticStart*************************************************************/
46 
47 /*---------------------------------------------------------------------------*/
48 /* Static function prototypes                                                */
49 /*---------------------------------------------------------------------------*/
50 
51 /**AutomaticEnd***************************************************************/
52 
53 
54 /*
55     LinearSpace(f) = Space(f,f)
56 
57     Space(f,g)
58     {
59         if ( f = const )
60         {
61             if ( f = g )  return 1;
62             else          return 0;
63         }
64         if ( g = const )  return 0;
65         return x' * Space(fx',gx') * Space(fx,gx) + x * Space(fx',gx) * Space(fx,gx');
66     }
67 
68     Equations(s) = Pos(s) + Neg(s);
69 
70     Pos(s)
71     {
72         if ( s  = 0 )   return 1;
73         if ( s  = 1 )   return 0;
74         if ( sx'= 0 )   return Pos(sx) + x;
75         if ( sx = 0 )   return Pos(sx');
76         return 1 * [Pos(sx') & Pos(sx)] + x * [Pos(sx') & Neg(sx)];
77     }
78 
79     Neg(s)
80     {
81         if ( s  = 0 )   return 1;
82         if ( s  = 1 )   return 0;
83         if ( sx'= 0 )   return Neg(sx);
84         if ( sx = 0 )   return Neg(sx') + x;
85         return 1 * [Neg(sx') & Neg(sx)] + x * [Neg(sx') & Pos(sx)];
86     }
87 
88 
89     SpaceP(A)
90     {
91         if ( A = 0 )    return 1;
92         if ( A = 1 )    return 1;
93         return x' * SpaceP(Ax') * SpaceP(Ax) + x * SpaceP(Ax') * SpaceN(Ax);
94     }
95 
96     SpaceN(A)
97     {
98         if ( A = 0 )    return 1;
99         if ( A = 1 )    return 0;
100         return x' * SpaceN(Ax') * SpaceN(Ax) + x * SpaceN(Ax') * SpaceP(Ax);
101     }
102 
103 
104     LinInd(A)
105     {
106         if ( A = const )     return 1;
107         if ( !LinInd(Ax') )  return 0;
108         if ( !LinInd(Ax)  )  return 0;
109         if (  LinSumOdd(Ax')  & LinSumEven(Ax) != 0 )  return 0;
110         if (  LinSumEven(Ax') & LinSumEven(Ax) != 0 )  return 0;
111         return 1;
112     }
113 
114     LinSumOdd(A)
115     {
116         if ( A = 0 )    return 0;                 // Odd0  ---e-- Odd1
117         if ( A = 1 )    return 1;                 //       \   o
118         Odd0  = LinSumOdd(Ax');  // x is absent   //         \
119         Even0 = LinSumEven(Ax'); // x is absent   //       /   o
120         Odd1  = LinSumOdd(Ax);   // x is present  // Even0 ---e-- Even1
121         Even1 = LinSumEven(Ax);  // x is absent
122         return 1 * [Odd0 + ExorP(Odd0, Even1)] + x * [Odd1 + ExorP(Odd1, Even0)];
123     }
124 
125     LinSumEven(A)
126     {
127         if ( A = 0 )    return 0;
128         if ( A = 1 )    return 0;
129         Odd0  = LinSumOdd(Ax');  // x is absent
130         Even0 = LinSumEven(Ax'); // x is absent
131         Odd1  = LinSumOdd(Ax);   // x is present
132         Even1 = LinSumEven(Ax);  // x is absent
133         return 1 * [Even0 + Even1 + ExorP(Even0, Even1)] + x * [ExorP(Odd0, Odd1)];
134     }
135 
136 */
137 
138 /*---------------------------------------------------------------------------*/
139 /* Definition of exported functions                                          */
140 /*---------------------------------------------------------------------------*/
141 
142 /**Function*************************************************************
143 
144   Synopsis    []
145 
146   Description []
147 
148   SideEffects []
149 
150   SeeAlso     []
151 
152 ***********************************************************************/
Extra_bddSpaceFromFunctionFast(DdManager * dd,DdNode * bFunc)153 DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc )
154 {
155     int * pSupport;
156     int * pPermute;
157     int * pPermuteBack;
158     DdNode ** pCompose;
159     DdNode * bCube, * bTemp;
160     DdNode * bSpace, * bFunc1, * bFunc2, * bSpaceShift;
161     int nSupp, Counter;
162     int i, lev;
163 
164     // get the support
165     pSupport = ABC_ALLOC( int, ddMax(dd->size,dd->sizeZ) );
166     Extra_SupportArray( dd, bFunc, pSupport );
167     nSupp = 0;
168     for ( i = 0; i < dd->size; i++ )
169         if ( pSupport[i] )
170             nSupp++;
171 
172     // make sure the manager has enough variables
173     if ( 2*nSupp > dd->size )
174     {
175         printf( "Cannot derive linear space, because DD manager does not have enough variables.\n" );
176         fflush( stdout );
177         ABC_FREE( pSupport );
178         return NULL;
179     }
180 
181     // create the permutation arrays
182     pPermute     = ABC_ALLOC( int, dd->size );
183     pPermuteBack = ABC_ALLOC( int, dd->size );
184     pCompose     = ABC_ALLOC( DdNode *, dd->size );
185     for ( i = 0; i < dd->size; i++ )
186     {
187         pPermute[i]     = i;
188         pPermuteBack[i] = i;
189         pCompose[i]     = dd->vars[i];   Cudd_Ref( pCompose[i] );
190     }
191 
192     // remap the function in such a way that the variables are interleaved
193     Counter = 0;
194     bCube = b1;  Cudd_Ref( bCube );
195     for ( lev = 0; lev < dd->size; lev++ )
196         if ( pSupport[ dd->invperm[lev] ] )
197         {   // var "dd->invperm[lev]" on level "lev" should go to level 2*Counter;
198             pPermute[ dd->invperm[lev] ] = dd->invperm[2*Counter];
199             // var from level 2*Counter+1 should go back to the place of this var
200             pPermuteBack[ dd->invperm[2*Counter+1] ] = dd->invperm[lev];
201             // the permutation should be defined in such a way that variable
202             // on level 2*Counter is replaced by an EXOR of itself and var on the next level
203             Cudd_Deref( pCompose[ dd->invperm[2*Counter] ] );
204             pCompose[ dd->invperm[2*Counter] ] =
205                 Cudd_bddXor( dd, dd->vars[ dd->invperm[2*Counter] ], dd->vars[ dd->invperm[2*Counter+1] ] );
206             Cudd_Ref( pCompose[ dd->invperm[2*Counter] ] );
207             // add this variable to the cube
208             bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[ dd->invperm[2*Counter] ] );  Cudd_Ref( bCube );
209             Cudd_RecursiveDeref( dd, bTemp );
210             // increment the counter
211             Counter ++;
212         }
213 
214     // permute the functions
215     bFunc1 = Cudd_bddPermute( dd, bFunc, pPermute );         Cudd_Ref( bFunc1 );
216     // compose to gate the function depending on both vars
217     bFunc2 = Cudd_bddVectorCompose( dd, bFunc1, pCompose );  Cudd_Ref( bFunc2 );
218     // gate the vector space
219     // L(a) = ForAll x [ F(x) = F(x+a) ] = Not( Exist x [ F(x) (+) F(x+a) ] )
220     bSpaceShift = Cudd_bddXorExistAbstract( dd, bFunc1, bFunc2, bCube );  Cudd_Ref( bSpaceShift );
221     bSpaceShift = Cudd_Not( bSpaceShift );
222     // permute the space back into the original mapping
223     bSpace = Cudd_bddPermute( dd, bSpaceShift, pPermuteBack ); Cudd_Ref( bSpace );
224     Cudd_RecursiveDeref( dd, bFunc1 );
225     Cudd_RecursiveDeref( dd, bFunc2 );
226     Cudd_RecursiveDeref( dd, bSpaceShift );
227     Cudd_RecursiveDeref( dd, bCube );
228 
229     for ( i = 0; i < dd->size; i++ )
230         Cudd_RecursiveDeref( dd, pCompose[i] );
231     ABC_FREE( pPermute );
232     ABC_FREE( pPermuteBack );
233     ABC_FREE( pCompose );
234     ABC_FREE( pSupport );
235 
236     Cudd_Deref( bSpace );
237     return bSpace;
238 }
239 
240 
241 
242 /**Function*************************************************************
243 
244   Synopsis    []
245 
246   Description []
247 
248   SideEffects []
249 
250   SeeAlso     []
251 
252 ***********************************************************************/
Extra_bddSpaceFromFunction(DdManager * dd,DdNode * bF,DdNode * bG)253 DdNode * Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG )
254 {
255     DdNode * bRes;
256     do {
257         dd->reordered = 0;
258         bRes = extraBddSpaceFromFunction( dd, bF, bG );
259     } while (dd->reordered == 1);
260     return bRes;
261 }
262 
263 /**Function*************************************************************
264 
265   Synopsis    []
266 
267   Description []
268 
269   SideEffects []
270 
271   SeeAlso     []
272 
273 ***********************************************************************/
Extra_bddSpaceFromFunctionPos(DdManager * dd,DdNode * bFunc)274 DdNode * Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc )
275 {
276     DdNode * bRes;
277     do {
278         dd->reordered = 0;
279         bRes = extraBddSpaceFromFunctionPos( dd, bFunc );
280     } while (dd->reordered == 1);
281     return bRes;
282 }
283 
284 /**Function*************************************************************
285 
286   Synopsis    []
287 
288   Description []
289 
290   SideEffects []
291 
292   SeeAlso     []
293 
294 ***********************************************************************/
Extra_bddSpaceFromFunctionNeg(DdManager * dd,DdNode * bFunc)295 DdNode * Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc )
296 {
297     DdNode * bRes;
298     do {
299         dd->reordered = 0;
300         bRes = extraBddSpaceFromFunctionNeg( dd, bFunc );
301     } while (dd->reordered == 1);
302     return bRes;
303 }
304 
305 /**Function*************************************************************
306 
307   Synopsis    []
308 
309   Description []
310 
311   SideEffects []
312 
313   SeeAlso     []
314 
315 ***********************************************************************/
Extra_bddSpaceCanonVars(DdManager * dd,DdNode * bSpace)316 DdNode * Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace )
317 {
318     DdNode * bRes;
319     do {
320         dd->reordered = 0;
321         bRes = extraBddSpaceCanonVars( dd, bSpace );
322     } while (dd->reordered == 1);
323     return bRes;
324 }
325 
326 /**Function*************************************************************
327 
328   Synopsis    []
329 
330   Description []
331 
332   SideEffects []
333 
334   SeeAlso     []
335 
336 ***********************************************************************/
Extra_bddSpaceReduce(DdManager * dd,DdNode * bFunc,DdNode * bCanonVars)337 DdNode * Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars )
338 {
339     DdNode * bNegCube;
340     DdNode * bResult;
341     bNegCube = Extra_bddSupportNegativeCube( dd, bCanonVars );  Cudd_Ref( bNegCube );
342     bResult  = Cudd_Cofactor( dd, bFunc, bNegCube );            Cudd_Ref( bResult );
343     Cudd_RecursiveDeref( dd, bNegCube );
344     Cudd_Deref( bResult );
345     return bResult;
346 }
347 
348 
349 
350 /**Function*************************************************************
351 
352   Synopsis    []
353 
354   Description []
355 
356   SideEffects []
357 
358   SeeAlso     []
359 
360 ***********************************************************************/
Extra_bddSpaceEquations(DdManager * dd,DdNode * bSpace)361 DdNode * Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace )
362 {
363     DdNode * zRes;
364     DdNode * zEquPos;
365     DdNode * zEquNeg;
366     zEquPos = Extra_bddSpaceEquationsPos( dd, bSpace );  Cudd_Ref( zEquPos );
367     zEquNeg = Extra_bddSpaceEquationsNeg( dd, bSpace );  Cudd_Ref( zEquNeg );
368     zRes    = Cudd_zddUnion( dd, zEquPos, zEquNeg );     Cudd_Ref( zRes );
369     Cudd_RecursiveDerefZdd( dd, zEquPos );
370     Cudd_RecursiveDerefZdd( dd, zEquNeg );
371     Cudd_Deref( zRes );
372     return zRes;
373 }
374 
375 
376 /**Function*************************************************************
377 
378   Synopsis    []
379 
380   Description []
381 
382   SideEffects []
383 
384   SeeAlso     []
385 
386 ***********************************************************************/
Extra_bddSpaceEquationsPos(DdManager * dd,DdNode * bSpace)387 DdNode * Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace )
388 {
389     DdNode * zRes;
390     do {
391         dd->reordered = 0;
392         zRes = extraBddSpaceEquationsPos( dd, bSpace );
393     } while (dd->reordered == 1);
394     return zRes;
395 }
396 
397 
398 /**Function*************************************************************
399 
400   Synopsis    []
401 
402   Description []
403 
404   SideEffects []
405 
406   SeeAlso     []
407 
408 ***********************************************************************/
Extra_bddSpaceEquationsNeg(DdManager * dd,DdNode * bSpace)409 DdNode * Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace )
410 {
411     DdNode * zRes;
412     do {
413         dd->reordered = 0;
414         zRes = extraBddSpaceEquationsNeg( dd, bSpace );
415     } while (dd->reordered == 1);
416     return zRes;
417 }
418 
419 
420 /**Function*************************************************************
421 
422   Synopsis    []
423 
424   Description []
425 
426   SideEffects []
427 
428   SeeAlso     []
429 
430 ***********************************************************************/
Extra_bddSpaceFromMatrixPos(DdManager * dd,DdNode * zA)431 DdNode * Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA )
432 {
433     DdNode * bRes;
434     do {
435         dd->reordered = 0;
436         bRes = extraBddSpaceFromMatrixPos( dd, zA );
437     } while (dd->reordered == 1);
438     return bRes;
439 }
440 
441 /**Function*************************************************************
442 
443   Synopsis    []
444 
445   Description []
446 
447   SideEffects []
448 
449   SeeAlso     []
450 
451 ***********************************************************************/
Extra_bddSpaceFromMatrixNeg(DdManager * dd,DdNode * zA)452 DdNode * Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA )
453 {
454     DdNode * bRes;
455     do {
456         dd->reordered = 0;
457         bRes = extraBddSpaceFromMatrixNeg( dd, zA );
458     } while (dd->reordered == 1);
459     return bRes;
460 }
461 
462 /**Function*************************************************************
463 
464   Synopsis    [Counts the number of literals in one combination.]
465 
466   Description []
467 
468   SideEffects []
469 
470   SeeAlso     []
471 
472 ***********************************************************************/
Extra_zddLitCountComb(DdManager * dd,DdNode * zComb)473 int Extra_zddLitCountComb( DdManager * dd, DdNode * zComb )
474 {
475     int Counter;
476     if ( zComb == z0 )
477         return 0;
478     Counter = 0;
479     for ( ; zComb != z1; zComb = cuddT(zComb) )
480         Counter++;
481     return Counter;
482 }
483 
484 /**Function*************************************************************
485 
486   Synopsis    []
487 
488   Description [Returns the array of ZDDs with the number equal to the number of
489   vars in the DD manager. If the given var is non-canonical, this array contains
490   the referenced ZDD representing literals in the corresponding EXOR equation.]
491 
492   SideEffects []
493 
494   SeeAlso     []
495 
496 ***********************************************************************/
Extra_bddSpaceExorGates(DdManager * dd,DdNode * bFuncRed,DdNode * zEquations)497 DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations )
498 {
499     DdNode ** pzRes;
500     int * pVarsNonCan;
501     DdNode * zEquRem;
502     int iVarNonCan;
503     DdNode * zExor, * zTemp;
504 
505     // get the set of non-canonical variables
506     pVarsNonCan = ABC_ALLOC( int, ddMax(dd->size,dd->sizeZ) );
507     Extra_SupportArray( dd, bFuncRed, pVarsNonCan );
508 
509     // allocate storage for the EXOR sets
510     pzRes = ABC_ALLOC( DdNode *, dd->size );
511     memset( pzRes, 0, sizeof(DdNode *) * dd->size );
512 
513     // go through all the equations
514     zEquRem = zEquations;  Cudd_Ref( zEquRem );
515     while ( zEquRem != z0 )
516     {
517         // extract one product
518         zExor = Extra_zddSelectOneSubset( dd, zEquRem );   Cudd_Ref( zExor );
519         // remove it from the set
520         zEquRem = Cudd_zddDiff( dd, zTemp = zEquRem, zExor );  Cudd_Ref( zEquRem );
521         Cudd_RecursiveDerefZdd( dd, zTemp );
522 
523         // locate the non-canonical variable
524         iVarNonCan = -1;
525         for ( zTemp = zExor; zTemp != z1; zTemp = cuddT(zTemp) )
526         {
527             if ( pVarsNonCan[zTemp->index/2] == 1 )
528             {
529                 assert( iVarNonCan == -1 );
530                 iVarNonCan = zTemp->index/2;
531             }
532         }
533         assert( iVarNonCan != -1 );
534 
535         if ( Extra_zddLitCountComb( dd, zExor ) > 1 )
536             pzRes[ iVarNonCan ] = zExor; // takes ref
537         else
538             Cudd_RecursiveDerefZdd( dd, zExor );
539     }
540     Cudd_RecursiveDerefZdd( dd, zEquRem );
541 
542     ABC_FREE( pVarsNonCan );
543     return pzRes;
544 }
545 
546 
547 /*---------------------------------------------------------------------------*/
548 /* Definition of internal functions                                          */
549 /*---------------------------------------------------------------------------*/
550 
551 /**Function********************************************************************
552 
553   Synopsis    [Performs the recursive steps of Extra_bddSpaceFromFunction.]
554 
555   Description []
556 
557   SideEffects []
558 
559   SeeAlso     []
560 
561 ******************************************************************************/
extraBddSpaceFromFunction(DdManager * dd,DdNode * bF,DdNode * bG)562 DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG )
563 {
564     DdNode * bRes;
565     DdNode * bFR, * bGR;
566 
567     bFR = Cudd_Regular( bF );
568     bGR = Cudd_Regular( bG );
569     if ( cuddIsConstant(bFR) )
570     {
571         if ( bF == bG )
572             return b1;
573         else
574             return b0;
575     }
576     if ( cuddIsConstant(bGR) )
577         return b0;
578     // both bFunc and bCore are not constants
579 
580     // the operation is commutative - normalize the problem
581     if ( (unsigned)(ABC_PTRUINT_T)bF > (unsigned)(ABC_PTRUINT_T)bG )
582         return extraBddSpaceFromFunction(dd, bG, bF);
583 
584 
585     if ( (bRes = cuddCacheLookup2(dd, extraBddSpaceFromFunction, bF, bG)) )
586         return bRes;
587     else
588     {
589         DdNode * bF0, * bF1;
590         DdNode * bG0, * bG1;
591         DdNode * bTemp1, * bTemp2;
592         DdNode * bRes0, * bRes1;
593         int LevelF, LevelG;
594         int index;
595 
596         LevelF = dd->perm[bFR->index];
597         LevelG = dd->perm[bGR->index];
598         if ( LevelF <= LevelG )
599         {
600             index = dd->invperm[LevelF];
601             if ( bFR != bF )
602             {
603                 bF0 = Cudd_Not( cuddE(bFR) );
604                 bF1 = Cudd_Not( cuddT(bFR) );
605             }
606             else
607             {
608                 bF0 = cuddE(bFR);
609                 bF1 = cuddT(bFR);
610             }
611         }
612         else
613         {
614             index = dd->invperm[LevelG];
615             bF0 = bF1 = bF;
616         }
617 
618         if ( LevelG <= LevelF )
619         {
620             if ( bGR != bG )
621             {
622                 bG0 = Cudd_Not( cuddE(bGR) );
623                 bG1 = Cudd_Not( cuddT(bGR) );
624             }
625             else
626             {
627                 bG0 = cuddE(bGR);
628                 bG1 = cuddT(bGR);
629             }
630         }
631         else
632             bG0 = bG1 = bG;
633 
634         bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG0 );
635         if ( bTemp1 == NULL )
636             return NULL;
637         cuddRef( bTemp1 );
638 
639         bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG1 );
640         if ( bTemp2 == NULL )
641         {
642             Cudd_RecursiveDeref( dd, bTemp1 );
643             return NULL;
644         }
645         cuddRef( bTemp2 );
646 
647 
648         bRes0  = cuddBddAndRecur( dd, bTemp1, bTemp2 );
649         if ( bRes0 == NULL )
650         {
651             Cudd_RecursiveDeref( dd, bTemp1 );
652             Cudd_RecursiveDeref( dd, bTemp2 );
653             return NULL;
654         }
655         cuddRef( bRes0 );
656         Cudd_RecursiveDeref( dd, bTemp1 );
657         Cudd_RecursiveDeref( dd, bTemp2 );
658 
659 
660         bTemp1  = extraBddSpaceFromFunction( dd, bF0, bG1 );
661         if ( bTemp1 == NULL )
662         {
663             Cudd_RecursiveDeref( dd, bRes0 );
664             return NULL;
665         }
666         cuddRef( bTemp1 );
667 
668         bTemp2  = extraBddSpaceFromFunction( dd, bF1, bG0 );
669         if ( bTemp2 == NULL )
670         {
671             Cudd_RecursiveDeref( dd, bRes0 );
672             Cudd_RecursiveDeref( dd, bTemp1 );
673             return NULL;
674         }
675         cuddRef( bTemp2 );
676 
677         bRes1  = cuddBddAndRecur( dd, bTemp1, bTemp2 );
678         if ( bRes1 == NULL )
679         {
680             Cudd_RecursiveDeref( dd, bRes0 );
681             Cudd_RecursiveDeref( dd, bTemp1 );
682             Cudd_RecursiveDeref( dd, bTemp2 );
683             return NULL;
684         }
685         cuddRef( bRes1 );
686         Cudd_RecursiveDeref( dd, bTemp1 );
687         Cudd_RecursiveDeref( dd, bTemp2 );
688 
689 
690 
691         // consider the case when Res0 and Res1 are the same node
692         if ( bRes0 == bRes1 )
693             bRes = bRes1;
694         // consider the case when Res1 is complemented
695         else if ( Cudd_IsComplement(bRes1) )
696         {
697             bRes = cuddUniqueInter(dd, index, Cudd_Not(bRes1), Cudd_Not(bRes0));
698             if ( bRes == NULL )
699             {
700                 Cudd_RecursiveDeref(dd,bRes0);
701                 Cudd_RecursiveDeref(dd,bRes1);
702                 return NULL;
703             }
704             bRes = Cudd_Not(bRes);
705         }
706         else
707         {
708             bRes = cuddUniqueInter( dd, index, bRes1, bRes0 );
709             if ( bRes == NULL )
710             {
711                 Cudd_RecursiveDeref(dd,bRes0);
712                 Cudd_RecursiveDeref(dd,bRes1);
713                 return NULL;
714             }
715         }
716         cuddDeref( bRes0 );
717         cuddDeref( bRes1 );
718 
719         // insert the result into cache
720         cuddCacheInsert2(dd, extraBddSpaceFromFunction, bF, bG, bRes);
721         return bRes;
722     }
723 }  /* end of extraBddSpaceFromFunction */
724 
725 
726 
727 /**Function*************************************************************
728 
729   Synopsis    [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
730 
731   Description []
732 
733   SideEffects []
734 
735   SeeAlso     []
736 
737 ***********************************************************************/
extraBddSpaceFromFunctionPos(DdManager * dd,DdNode * bF)738 DdNode * extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bF )
739 {
740     DdNode * bRes, * bFR;
741     statLine( dd );
742 
743     bFR = Cudd_Regular(bF);
744     if ( cuddIsConstant(bFR) )
745         return b1;
746 
747     if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionPos, bF)) )
748         return bRes;
749     else
750     {
751         DdNode * bF0,   * bF1;
752         DdNode * bPos0, * bPos1;
753         DdNode * bNeg0, * bNeg1;
754         DdNode * bRes0, * bRes1;
755 
756         if ( bFR != bF ) // bF is complemented
757         {
758             bF0 = Cudd_Not( cuddE(bFR) );
759             bF1 = Cudd_Not( cuddT(bFR) );
760         }
761         else
762         {
763             bF0 = cuddE(bFR);
764             bF1 = cuddT(bFR);
765         }
766 
767 
768         bPos0  = extraBddSpaceFromFunctionPos( dd, bF0 );
769         if ( bPos0 == NULL )
770             return NULL;
771         cuddRef( bPos0 );
772 
773         bPos1  = extraBddSpaceFromFunctionPos( dd, bF1 );
774         if ( bPos1 == NULL )
775         {
776             Cudd_RecursiveDeref( dd, bPos0 );
777             return NULL;
778         }
779         cuddRef( bPos1 );
780 
781         bRes0  = cuddBddAndRecur( dd, bPos0, bPos1 );
782         if ( bRes0 == NULL )
783         {
784             Cudd_RecursiveDeref( dd, bPos0 );
785             Cudd_RecursiveDeref( dd, bPos1 );
786             return NULL;
787         }
788         cuddRef( bRes0 );
789         Cudd_RecursiveDeref( dd, bPos0 );
790         Cudd_RecursiveDeref( dd, bPos1 );
791 
792 
793         bNeg0  = extraBddSpaceFromFunctionNeg( dd, bF0 );
794         if ( bNeg0 == NULL )
795         {
796             Cudd_RecursiveDeref( dd, bRes0 );
797             return NULL;
798         }
799         cuddRef( bNeg0 );
800 
801         bNeg1  = extraBddSpaceFromFunctionNeg( dd, bF1 );
802         if ( bNeg1 == NULL )
803         {
804             Cudd_RecursiveDeref( dd, bRes0 );
805             Cudd_RecursiveDeref( dd, bNeg0 );
806             return NULL;
807         }
808         cuddRef( bNeg1 );
809 
810         bRes1  = cuddBddAndRecur( dd, bNeg0, bNeg1 );
811         if ( bRes1 == NULL )
812         {
813             Cudd_RecursiveDeref( dd, bRes0 );
814             Cudd_RecursiveDeref( dd, bNeg0 );
815             Cudd_RecursiveDeref( dd, bNeg1 );
816             return NULL;
817         }
818         cuddRef( bRes1 );
819         Cudd_RecursiveDeref( dd, bNeg0 );
820         Cudd_RecursiveDeref( dd, bNeg1 );
821 
822 
823         // consider the case when Res0 and Res1 are the same node
824         if ( bRes0 == bRes1 )
825             bRes = bRes1;
826         // consider the case when Res1 is complemented
827         else if ( Cudd_IsComplement(bRes1) )
828         {
829             bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) );
830             if ( bRes == NULL )
831             {
832                 Cudd_RecursiveDeref(dd,bRes0);
833                 Cudd_RecursiveDeref(dd,bRes1);
834                 return NULL;
835             }
836             bRes = Cudd_Not(bRes);
837         }
838         else
839         {
840             bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
841             if ( bRes == NULL )
842             {
843                 Cudd_RecursiveDeref(dd,bRes0);
844                 Cudd_RecursiveDeref(dd,bRes1);
845                 return NULL;
846             }
847         }
848         cuddDeref( bRes0 );
849         cuddDeref( bRes1 );
850 
851         cuddCacheInsert1( dd, extraBddSpaceFromFunctionPos, bF, bRes );
852         return bRes;
853     }
854 }
855 
856 
857 
858 /**Function*************************************************************
859 
860   Synopsis    [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
861 
862   Description []
863 
864   SideEffects []
865 
866   SeeAlso     []
867 
868 ***********************************************************************/
extraBddSpaceFromFunctionNeg(DdManager * dd,DdNode * bF)869 DdNode * extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bF )
870 {
871     DdNode * bRes, * bFR;
872     statLine( dd );
873 
874     bFR = Cudd_Regular(bF);
875     if ( cuddIsConstant(bFR) )
876         return b0;
877 
878     if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionNeg, bF)) )
879         return bRes;
880     else
881     {
882         DdNode * bF0,   * bF1;
883         DdNode * bPos0, * bPos1;
884         DdNode * bNeg0, * bNeg1;
885         DdNode * bRes0, * bRes1;
886 
887         if ( bFR != bF ) // bF is complemented
888         {
889             bF0 = Cudd_Not( cuddE(bFR) );
890             bF1 = Cudd_Not( cuddT(bFR) );
891         }
892         else
893         {
894             bF0 = cuddE(bFR);
895             bF1 = cuddT(bFR);
896         }
897 
898 
899         bPos0  = extraBddSpaceFromFunctionNeg( dd, bF0 );
900         if ( bPos0 == NULL )
901             return NULL;
902         cuddRef( bPos0 );
903 
904         bPos1  = extraBddSpaceFromFunctionNeg( dd, bF1 );
905         if ( bPos1 == NULL )
906         {
907             Cudd_RecursiveDeref( dd, bPos0 );
908             return NULL;
909         }
910         cuddRef( bPos1 );
911 
912         bRes0  = cuddBddAndRecur( dd, bPos0, bPos1 );
913         if ( bRes0 == NULL )
914         {
915             Cudd_RecursiveDeref( dd, bPos0 );
916             Cudd_RecursiveDeref( dd, bPos1 );
917             return NULL;
918         }
919         cuddRef( bRes0 );
920         Cudd_RecursiveDeref( dd, bPos0 );
921         Cudd_RecursiveDeref( dd, bPos1 );
922 
923 
924         bNeg0  = extraBddSpaceFromFunctionPos( dd, bF0 );
925         if ( bNeg0 == NULL )
926         {
927             Cudd_RecursiveDeref( dd, bRes0 );
928             return NULL;
929         }
930         cuddRef( bNeg0 );
931 
932         bNeg1  = extraBddSpaceFromFunctionPos( dd, bF1 );
933         if ( bNeg1 == NULL )
934         {
935             Cudd_RecursiveDeref( dd, bRes0 );
936             Cudd_RecursiveDeref( dd, bNeg0 );
937             return NULL;
938         }
939         cuddRef( bNeg1 );
940 
941         bRes1  = cuddBddAndRecur( dd, bNeg0, bNeg1 );
942         if ( bRes1 == NULL )
943         {
944             Cudd_RecursiveDeref( dd, bRes0 );
945             Cudd_RecursiveDeref( dd, bNeg0 );
946             Cudd_RecursiveDeref( dd, bNeg1 );
947             return NULL;
948         }
949         cuddRef( bRes1 );
950         Cudd_RecursiveDeref( dd, bNeg0 );
951         Cudd_RecursiveDeref( dd, bNeg1 );
952 
953 
954         // consider the case when Res0 and Res1 are the same node
955         if ( bRes0 == bRes1 )
956             bRes = bRes1;
957         // consider the case when Res1 is complemented
958         else if ( Cudd_IsComplement(bRes1) )
959         {
960             bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) );
961             if ( bRes == NULL )
962             {
963                 Cudd_RecursiveDeref(dd,bRes0);
964                 Cudd_RecursiveDeref(dd,bRes1);
965                 return NULL;
966             }
967             bRes = Cudd_Not(bRes);
968         }
969         else
970         {
971             bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
972             if ( bRes == NULL )
973             {
974                 Cudd_RecursiveDeref(dd,bRes0);
975                 Cudd_RecursiveDeref(dd,bRes1);
976                 return NULL;
977             }
978         }
979         cuddDeref( bRes0 );
980         cuddDeref( bRes1 );
981 
982         cuddCacheInsert1( dd, extraBddSpaceFromFunctionNeg, bF, bRes );
983         return bRes;
984     }
985 }
986 
987 
988 
989 /**Function*************************************************************
990 
991   Synopsis    [Performs the recursive step of Extra_bddSpaceCanonVars().]
992 
993   Description []
994 
995   SideEffects []
996 
997   SeeAlso     []
998 
999 ***********************************************************************/
extraBddSpaceCanonVars(DdManager * dd,DdNode * bF)1000 DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bF )
1001 {
1002     DdNode * bRes, * bFR;
1003     statLine( dd );
1004 
1005     bFR = Cudd_Regular(bF);
1006     if ( cuddIsConstant(bFR) )
1007         return bF;
1008 
1009     if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceCanonVars, bF)) )
1010         return bRes;
1011     else
1012     {
1013         DdNode * bF0,  * bF1;
1014         DdNode * bRes, * bRes0;
1015 
1016         if ( bFR != bF ) // bF is complemented
1017         {
1018             bF0 = Cudd_Not( cuddE(bFR) );
1019             bF1 = Cudd_Not( cuddT(bFR) );
1020         }
1021         else
1022         {
1023             bF0 = cuddE(bFR);
1024             bF1 = cuddT(bFR);
1025         }
1026 
1027         if ( bF0 == b0 )
1028         {
1029             bRes = extraBddSpaceCanonVars( dd, bF1 );
1030             if ( bRes == NULL )
1031                 return NULL;
1032         }
1033         else if ( bF1 == b0 )
1034         {
1035             bRes = extraBddSpaceCanonVars( dd, bF0 );
1036             if ( bRes == NULL )
1037                 return NULL;
1038         }
1039         else
1040         {
1041             bRes0 = extraBddSpaceCanonVars( dd, bF0 );
1042             if ( bRes0 == NULL )
1043                 return NULL;
1044             cuddRef( bRes0 );
1045 
1046             bRes = cuddUniqueInter( dd, bFR->index, bRes0, b0 );
1047             if ( bRes == NULL )
1048             {
1049                 Cudd_RecursiveDeref( dd,bRes0 );
1050                 return NULL;
1051             }
1052             cuddDeref( bRes0 );
1053         }
1054 
1055         cuddCacheInsert1( dd, extraBddSpaceCanonVars, bF, bRes );
1056         return bRes;
1057     }
1058 }
1059 
1060 /**Function*************************************************************
1061 
1062   Synopsis    [Performs the recursive step of Extra_bddSpaceEquationsPos().]
1063 
1064   Description []
1065 
1066   SideEffects []
1067 
1068   SeeAlso     []
1069 
1070 ***********************************************************************/
extraBddSpaceEquationsPos(DdManager * dd,DdNode * bF)1071 DdNode * extraBddSpaceEquationsPos( DdManager * dd, DdNode * bF )
1072 {
1073     DdNode * zRes;
1074     statLine( dd );
1075 
1076     if ( bF == b0 )
1077         return z1;
1078     if ( bF == b1 )
1079         return z0;
1080 
1081     if ( (zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsPos, bF)) )
1082         return zRes;
1083     else
1084     {
1085         DdNode * bFR, * bF0,  * bF1;
1086         DdNode * zPos0, * zPos1, * zNeg1;
1087         DdNode * zRes, * zRes0, * zRes1;
1088 
1089         bFR = Cudd_Regular(bF);
1090         if ( bFR != bF ) // bF is complemented
1091         {
1092             bF0 = Cudd_Not( cuddE(bFR) );
1093             bF1 = Cudd_Not( cuddT(bFR) );
1094         }
1095         else
1096         {
1097             bF0 = cuddE(bFR);
1098             bF1 = cuddT(bFR);
1099         }
1100 
1101         if ( bF0 == b0 )
1102         {
1103             zRes1 = extraBddSpaceEquationsPos( dd, bF1 );
1104             if ( zRes1 == NULL )
1105                 return NULL;
1106             cuddRef( zRes1 );
1107 
1108             // add the current element to the set
1109             zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes1 );
1110             if ( zRes == NULL )
1111             {
1112                 Cudd_RecursiveDerefZdd(dd, zRes1);
1113                 return NULL;
1114             }
1115             cuddDeref( zRes1 );
1116         }
1117         else if ( bF1 == b0 )
1118         {
1119             zRes = extraBddSpaceEquationsPos( dd, bF0 );
1120             if ( zRes == NULL )
1121                 return NULL;
1122         }
1123         else
1124         {
1125             zPos0 = extraBddSpaceEquationsPos( dd, bF0 );
1126             if ( zPos0 == NULL )
1127                 return NULL;
1128             cuddRef( zPos0 );
1129 
1130             zPos1 = extraBddSpaceEquationsPos( dd, bF1 );
1131             if ( zPos1 == NULL )
1132             {
1133                 Cudd_RecursiveDerefZdd(dd, zPos0);
1134                 return NULL;
1135             }
1136             cuddRef( zPos1 );
1137 
1138             zNeg1 = extraBddSpaceEquationsNeg( dd, bF1 );
1139             if ( zNeg1 == NULL )
1140             {
1141                 Cudd_RecursiveDerefZdd(dd, zPos0);
1142                 Cudd_RecursiveDerefZdd(dd, zPos1);
1143                 return NULL;
1144             }
1145             cuddRef( zNeg1 );
1146 
1147 
1148             zRes0 = cuddZddIntersect( dd, zPos0, zPos1 );
1149             if ( zRes0 == NULL )
1150             {
1151                 Cudd_RecursiveDerefZdd(dd, zNeg1);
1152                 Cudd_RecursiveDerefZdd(dd, zPos0);
1153                 Cudd_RecursiveDerefZdd(dd, zPos1);
1154                 return NULL;
1155             }
1156             cuddRef( zRes0 );
1157 
1158             zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 );
1159             if ( zRes1 == NULL )
1160             {
1161                 Cudd_RecursiveDerefZdd(dd, zRes0);
1162                 Cudd_RecursiveDerefZdd(dd, zNeg1);
1163                 Cudd_RecursiveDerefZdd(dd, zPos0);
1164                 Cudd_RecursiveDerefZdd(dd, zPos1);
1165                 return NULL;
1166             }
1167             cuddRef( zRes1 );
1168             Cudd_RecursiveDerefZdd(dd, zNeg1);
1169             Cudd_RecursiveDerefZdd(dd, zPos0);
1170             Cudd_RecursiveDerefZdd(dd, zPos1);
1171             // only zRes0 and zRes1 are refed at this point
1172 
1173             zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 );
1174             if ( zRes == NULL )
1175             {
1176                 Cudd_RecursiveDerefZdd(dd, zRes0);
1177                 Cudd_RecursiveDerefZdd(dd, zRes1);
1178                 return NULL;
1179             }
1180             cuddDeref( zRes0 );
1181             cuddDeref( zRes1 );
1182         }
1183 
1184         cuddCacheInsert1( dd, extraBddSpaceEquationsPos, bF, zRes );
1185         return zRes;
1186     }
1187 }
1188 
1189 
1190 /**Function*************************************************************
1191 
1192   Synopsis    [Performs the recursive step of Extra_bddSpaceEquationsNev().]
1193 
1194   Description []
1195 
1196   SideEffects []
1197 
1198   SeeAlso     []
1199 
1200 ***********************************************************************/
extraBddSpaceEquationsNeg(DdManager * dd,DdNode * bF)1201 DdNode * extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bF )
1202 {
1203     DdNode * zRes;
1204     statLine( dd );
1205 
1206     if ( bF == b0 )
1207         return z1;
1208     if ( bF == b1 )
1209         return z0;
1210 
1211     if ( (zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsNeg, bF)) )
1212         return zRes;
1213     else
1214     {
1215         DdNode * bFR, * bF0,  * bF1;
1216         DdNode * zPos0, * zPos1, * zNeg1;
1217         DdNode * zRes, * zRes0, * zRes1;
1218 
1219         bFR = Cudd_Regular(bF);
1220         if ( bFR != bF ) // bF is complemented
1221         {
1222             bF0 = Cudd_Not( cuddE(bFR) );
1223             bF1 = Cudd_Not( cuddT(bFR) );
1224         }
1225         else
1226         {
1227             bF0 = cuddE(bFR);
1228             bF1 = cuddT(bFR);
1229         }
1230 
1231         if ( bF0 == b0 )
1232         {
1233             zRes = extraBddSpaceEquationsNeg( dd, bF1 );
1234             if ( zRes == NULL )
1235                 return NULL;
1236         }
1237         else if ( bF1 == b0 )
1238         {
1239             zRes0 = extraBddSpaceEquationsNeg( dd, bF0 );
1240             if ( zRes0 == NULL )
1241                 return NULL;
1242             cuddRef( zRes0 );
1243 
1244             // add the current element to the set
1245             zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes0 );
1246             if ( zRes == NULL )
1247             {
1248                 Cudd_RecursiveDerefZdd(dd, zRes0);
1249                 return NULL;
1250             }
1251             cuddDeref( zRes0 );
1252         }
1253         else
1254         {
1255             zPos0 = extraBddSpaceEquationsNeg( dd, bF0 );
1256             if ( zPos0 == NULL )
1257                 return NULL;
1258             cuddRef( zPos0 );
1259 
1260             zPos1 = extraBddSpaceEquationsNeg( dd, bF1 );
1261             if ( zPos1 == NULL )
1262             {
1263                 Cudd_RecursiveDerefZdd(dd, zPos0);
1264                 return NULL;
1265             }
1266             cuddRef( zPos1 );
1267 
1268             zNeg1 = extraBddSpaceEquationsPos( dd, bF1 );
1269             if ( zNeg1 == NULL )
1270             {
1271                 Cudd_RecursiveDerefZdd(dd, zPos0);
1272                 Cudd_RecursiveDerefZdd(dd, zPos1);
1273                 return NULL;
1274             }
1275             cuddRef( zNeg1 );
1276 
1277 
1278             zRes0 = cuddZddIntersect( dd, zPos0, zPos1 );
1279             if ( zRes0 == NULL )
1280             {
1281                 Cudd_RecursiveDerefZdd(dd, zNeg1);
1282                 Cudd_RecursiveDerefZdd(dd, zPos0);
1283                 Cudd_RecursiveDerefZdd(dd, zPos1);
1284                 return NULL;
1285             }
1286             cuddRef( zRes0 );
1287 
1288             zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 );
1289             if ( zRes1 == NULL )
1290             {
1291                 Cudd_RecursiveDerefZdd(dd, zRes0);
1292                 Cudd_RecursiveDerefZdd(dd, zNeg1);
1293                 Cudd_RecursiveDerefZdd(dd, zPos0);
1294                 Cudd_RecursiveDerefZdd(dd, zPos1);
1295                 return NULL;
1296             }
1297             cuddRef( zRes1 );
1298             Cudd_RecursiveDerefZdd(dd, zNeg1);
1299             Cudd_RecursiveDerefZdd(dd, zPos0);
1300             Cudd_RecursiveDerefZdd(dd, zPos1);
1301             // only zRes0 and zRes1 are refed at this point
1302 
1303             zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 );
1304             if ( zRes == NULL )
1305             {
1306                 Cudd_RecursiveDerefZdd(dd, zRes0);
1307                 Cudd_RecursiveDerefZdd(dd, zRes1);
1308                 return NULL;
1309             }
1310             cuddDeref( zRes0 );
1311             cuddDeref( zRes1 );
1312         }
1313 
1314         cuddCacheInsert1( dd, extraBddSpaceEquationsNeg, bF, zRes );
1315         return zRes;
1316     }
1317 }
1318 
1319 
1320 
1321 
1322 /**Function*************************************************************
1323 
1324   Synopsis    [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
1325 
1326   Description []
1327 
1328   SideEffects []
1329 
1330   SeeAlso     []
1331 
1332 ***********************************************************************/
extraBddSpaceFromMatrixPos(DdManager * dd,DdNode * zA)1333 DdNode * extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA )
1334 {
1335     DdNode * bRes;
1336     statLine( dd );
1337 
1338     if ( zA == z0 )
1339         return b1;
1340     if ( zA == z1 )
1341         return b1;
1342 
1343     if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixPos, zA)) )
1344         return bRes;
1345     else
1346     {
1347         DdNode * bP0, * bP1;
1348         DdNode * bN0, * bN1;
1349         DdNode * bRes0, * bRes1;
1350 
1351         bP0  = extraBddSpaceFromMatrixPos( dd, cuddE(zA) );
1352         if ( bP0 == NULL )
1353             return NULL;
1354         cuddRef( bP0 );
1355 
1356         bP1  = extraBddSpaceFromMatrixPos( dd, cuddT(zA) );
1357         if ( bP1 == NULL )
1358         {
1359             Cudd_RecursiveDeref( dd, bP0 );
1360             return NULL;
1361         }
1362         cuddRef( bP1 );
1363 
1364         bRes0  = cuddBddAndRecur( dd, bP0, bP1 );
1365         if ( bRes0 == NULL )
1366         {
1367             Cudd_RecursiveDeref( dd, bP0 );
1368             Cudd_RecursiveDeref( dd, bP1 );
1369             return NULL;
1370         }
1371         cuddRef( bRes0 );
1372         Cudd_RecursiveDeref( dd, bP0 );
1373         Cudd_RecursiveDeref( dd, bP1 );
1374 
1375 
1376         bN0  = extraBddSpaceFromMatrixPos( dd, cuddE(zA) );
1377         if ( bN0 == NULL )
1378         {
1379             Cudd_RecursiveDeref( dd, bRes0 );
1380             return NULL;
1381         }
1382         cuddRef( bN0 );
1383 
1384         bN1  = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) );
1385         if ( bN1 == NULL )
1386         {
1387             Cudd_RecursiveDeref( dd, bRes0 );
1388             Cudd_RecursiveDeref( dd, bN0 );
1389             return NULL;
1390         }
1391         cuddRef( bN1 );
1392 
1393         bRes1  = cuddBddAndRecur( dd, bN0, bN1 );
1394         if ( bRes1 == NULL )
1395         {
1396             Cudd_RecursiveDeref( dd, bRes0 );
1397             Cudd_RecursiveDeref( dd, bN0 );
1398             Cudd_RecursiveDeref( dd, bN1 );
1399             return NULL;
1400         }
1401         cuddRef( bRes1 );
1402         Cudd_RecursiveDeref( dd, bN0 );
1403         Cudd_RecursiveDeref( dd, bN1 );
1404 
1405 
1406         // consider the case when Res0 and Res1 are the same node
1407         if ( bRes0 == bRes1 )
1408             bRes = bRes1;
1409         // consider the case when Res1 is complemented
1410         else if ( Cudd_IsComplement(bRes1) )
1411         {
1412             bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) );
1413             if ( bRes == NULL )
1414             {
1415                 Cudd_RecursiveDeref(dd,bRes0);
1416                 Cudd_RecursiveDeref(dd,bRes1);
1417                 return NULL;
1418             }
1419             bRes = Cudd_Not(bRes);
1420         }
1421         else
1422         {
1423             bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 );
1424             if ( bRes == NULL )
1425             {
1426                 Cudd_RecursiveDeref(dd,bRes0);
1427                 Cudd_RecursiveDeref(dd,bRes1);
1428                 return NULL;
1429             }
1430         }
1431         cuddDeref( bRes0 );
1432         cuddDeref( bRes1 );
1433 
1434         cuddCacheInsert1( dd, extraBddSpaceFromMatrixPos, zA, bRes );
1435         return bRes;
1436     }
1437 }
1438 
1439 
1440 /**Function*************************************************************
1441 
1442   Synopsis    [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
1443 
1444   Description []
1445 
1446   SideEffects []
1447 
1448   SeeAlso     []
1449 
1450 ***********************************************************************/
extraBddSpaceFromMatrixNeg(DdManager * dd,DdNode * zA)1451 DdNode * extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA )
1452 {
1453     DdNode * bRes;
1454     statLine( dd );
1455 
1456     if ( zA == z0 )
1457         return b1;
1458     if ( zA == z1 )
1459         return b0;
1460 
1461     if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixNeg, zA)) )
1462         return bRes;
1463     else
1464     {
1465         DdNode * bP0, * bP1;
1466         DdNode * bN0, * bN1;
1467         DdNode * bRes0, * bRes1;
1468 
1469         bP0  = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) );
1470         if ( bP0 == NULL )
1471             return NULL;
1472         cuddRef( bP0 );
1473 
1474         bP1  = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) );
1475         if ( bP1 == NULL )
1476         {
1477             Cudd_RecursiveDeref( dd, bP0 );
1478             return NULL;
1479         }
1480         cuddRef( bP1 );
1481 
1482         bRes0  = cuddBddAndRecur( dd, bP0, bP1 );
1483         if ( bRes0 == NULL )
1484         {
1485             Cudd_RecursiveDeref( dd, bP0 );
1486             Cudd_RecursiveDeref( dd, bP1 );
1487             return NULL;
1488         }
1489         cuddRef( bRes0 );
1490         Cudd_RecursiveDeref( dd, bP0 );
1491         Cudd_RecursiveDeref( dd, bP1 );
1492 
1493 
1494         bN0  = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) );
1495         if ( bN0 == NULL )
1496         {
1497             Cudd_RecursiveDeref( dd, bRes0 );
1498             return NULL;
1499         }
1500         cuddRef( bN0 );
1501 
1502         bN1  = extraBddSpaceFromMatrixPos( dd, cuddT(zA) );
1503         if ( bN1 == NULL )
1504         {
1505             Cudd_RecursiveDeref( dd, bRes0 );
1506             Cudd_RecursiveDeref( dd, bN0 );
1507             return NULL;
1508         }
1509         cuddRef( bN1 );
1510 
1511         bRes1  = cuddBddAndRecur( dd, bN0, bN1 );
1512         if ( bRes1 == NULL )
1513         {
1514             Cudd_RecursiveDeref( dd, bRes0 );
1515             Cudd_RecursiveDeref( dd, bN0 );
1516             Cudd_RecursiveDeref( dd, bN1 );
1517             return NULL;
1518         }
1519         cuddRef( bRes1 );
1520         Cudd_RecursiveDeref( dd, bN0 );
1521         Cudd_RecursiveDeref( dd, bN1 );
1522 
1523 
1524         // consider the case when Res0 and Res1 are the same node
1525         if ( bRes0 == bRes1 )
1526             bRes = bRes1;
1527         // consider the case when Res1 is complemented
1528         else if ( Cudd_IsComplement(bRes1) )
1529         {
1530             bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) );
1531             if ( bRes == NULL )
1532             {
1533                 Cudd_RecursiveDeref(dd,bRes0);
1534                 Cudd_RecursiveDeref(dd,bRes1);
1535                 return NULL;
1536             }
1537             bRes = Cudd_Not(bRes);
1538         }
1539         else
1540         {
1541             bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 );
1542             if ( bRes == NULL )
1543             {
1544                 Cudd_RecursiveDeref(dd,bRes0);
1545                 Cudd_RecursiveDeref(dd,bRes1);
1546                 return NULL;
1547             }
1548         }
1549         cuddDeref( bRes0 );
1550         cuddDeref( bRes1 );
1551 
1552         cuddCacheInsert1( dd, extraBddSpaceFromMatrixNeg, zA, bRes );
1553         return bRes;
1554     }
1555 }
1556 
1557 
1558 /*---------------------------------------------------------------------------*/
1559 /* Definition of static functions                                            */
1560 /*---------------------------------------------------------------------------*/
1561 
1562 ABC_NAMESPACE_IMPL_END
1563 
1564