summaryrefslogtreecommitdiffstats
path: root/src/misc/extra/extraBddAuto.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc/extra/extraBddAuto.c')
-rw-r--r--src/misc/extra/extraBddAuto.c1558
1 files changed, 1558 insertions, 0 deletions
diff --git a/src/misc/extra/extraBddAuto.c b/src/misc/extra/extraBddAuto.c
new file mode 100644
index 00000000..21a969ba
--- /dev/null
+++ b/src/misc/extra/extraBddAuto.c
@@ -0,0 +1,1558 @@
+/**CFile****************************************************************
+
+ FileName [extraBddAuto.c]
+
+ PackageName [extra]
+
+ Synopsis [Computation of autosymmetries.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 2.0. Started - September 1, 2003.]
+
+ Revision [$Id: extraBddAuto.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticEnd***************************************************************/
+
+
+/*
+ LinearSpace(f) = Space(f,f)
+
+ Space(f,g)
+ {
+ if ( f = const )
+ {
+ if ( f = g ) return 1;
+ else return 0;
+ }
+ if ( g = const ) return 0;
+ return x' * Space(fx',gx') * Space(fx,gx) + x * Space(fx',gx) * Space(fx,gx');
+ }
+
+ Equations(s) = Pos(s) + Neg(s);
+
+ Pos(s)
+ {
+ if ( s = 0 ) return 1;
+ if ( s = 1 ) return 0;
+ if ( sx'= 0 ) return Pos(sx) + x;
+ if ( sx = 0 ) return Pos(sx');
+ return 1 * [Pos(sx') & Pos(sx)] + x * [Pos(sx') & Neg(sx)];
+ }
+
+ Neg(s)
+ {
+ if ( s = 0 ) return 1;
+ if ( s = 1 ) return 0;
+ if ( sx'= 0 ) return Neg(sx);
+ if ( sx = 0 ) return Neg(sx') + x;
+ return 1 * [Neg(sx') & Neg(sx)] + x * [Neg(sx') & Pos(sx)];
+ }
+
+
+ SpaceP(A)
+ {
+ if ( A = 0 ) return 1;
+ if ( A = 1 ) return 1;
+ return x' * SpaceP(Ax') * SpaceP(Ax) + x * SpaceP(Ax') * SpaceN(Ax);
+ }
+
+ SpaceN(A)
+ {
+ if ( A = 0 ) return 1;
+ if ( A = 1 ) return 0;
+ return x' * SpaceN(Ax') * SpaceN(Ax) + x * SpaceN(Ax') * SpaceP(Ax);
+ }
+
+
+ LinInd(A)
+ {
+ if ( A = const ) return 1;
+ if ( !LinInd(Ax') ) return 0;
+ if ( !LinInd(Ax) ) return 0;
+ if ( LinSumOdd(Ax') & LinSumEven(Ax) != 0 ) return 0;
+ if ( LinSumEven(Ax') & LinSumEven(Ax) != 0 ) return 0;
+ return 1;
+ }
+
+ LinSumOdd(A)
+ {
+ if ( A = 0 ) return 0; // Odd0 ---e-- Odd1
+ if ( A = 1 ) return 1; // \ o
+ Odd0 = LinSumOdd(Ax'); // x is absent // \
+ Even0 = LinSumEven(Ax'); // x is absent // / o
+ Odd1 = LinSumOdd(Ax); // x is present // Even0 ---e-- Even1
+ Even1 = LinSumEven(Ax); // x is absent
+ return 1 * [Odd0 + ExorP(Odd0, Even1)] + x * [Odd1 + ExorP(Odd1, Even0)];
+ }
+
+ LinSumEven(A)
+ {
+ if ( A = 0 ) return 0;
+ if ( A = 1 ) return 0;
+ Odd0 = LinSumOdd(Ax'); // x is absent
+ Even0 = LinSumEven(Ax'); // x is absent
+ Odd1 = LinSumOdd(Ax); // x is present
+ Even1 = LinSumEven(Ax); // x is absent
+ return 1 * [Even0 + Even1 + ExorP(Even0, Even1)] + x * [ExorP(Odd0, Odd1)];
+ }
+
+*/
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions */
+/*---------------------------------------------------------------------------*/
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc )
+{
+ int * pSupport;
+ int * pPermute;
+ int * pPermuteBack;
+ DdNode ** pCompose;
+ DdNode * bCube, * bTemp;
+ DdNode * bSpace, * bFunc1, * bFunc2, * bSpaceShift;
+ int nSupp, Counter;
+ int i, lev;
+
+ // get the support
+ pSupport = ALLOC( int, ddMax(dd->size,dd->sizeZ) );
+ Extra_SupportArray( dd, bFunc, pSupport );
+ nSupp = 0;
+ for ( i = 0; i < dd->size; i++ )
+ if ( pSupport[i] )
+ nSupp++;
+
+ // make sure the manager has enough variables
+ if ( 2*nSupp > dd->size )
+ {
+ printf( "Cannot derive linear space, because DD manager does not have enough variables.\n" );
+ fflush( stdout );
+ free( pSupport );
+ return NULL;
+ }
+
+ // create the permutation arrays
+ pPermute = ALLOC( int, dd->size );
+ pPermuteBack = ALLOC( int, dd->size );
+ pCompose = ALLOC( DdNode *, dd->size );
+ for ( i = 0; i < dd->size; i++ )
+ {
+ pPermute[i] = i;
+ pPermuteBack[i] = i;
+ pCompose[i] = dd->vars[i]; Cudd_Ref( pCompose[i] );
+ }
+
+ // remap the function in such a way that the variables are interleaved
+ Counter = 0;
+ bCube = b1; Cudd_Ref( bCube );
+ for ( lev = 0; lev < dd->size; lev++ )
+ if ( pSupport[ dd->invperm[lev] ] )
+ { // var "dd->invperm[lev]" on level "lev" should go to level 2*Counter;
+ pPermute[ dd->invperm[lev] ] = dd->invperm[2*Counter];
+ // var from level 2*Counter+1 should go back to the place of this var
+ pPermuteBack[ dd->invperm[2*Counter+1] ] = dd->invperm[lev];
+ // the permutation should be defined in such a way that variable
+ // on level 2*Counter is replaced by an EXOR of itself and var on the next level
+ Cudd_Deref( pCompose[ dd->invperm[2*Counter] ] );
+ pCompose[ dd->invperm[2*Counter] ] =
+ Cudd_bddXor( dd, dd->vars[ dd->invperm[2*Counter] ], dd->vars[ dd->invperm[2*Counter+1] ] );
+ Cudd_Ref( pCompose[ dd->invperm[2*Counter] ] );
+ // add this variable to the cube
+ bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[ dd->invperm[2*Counter] ] ); Cudd_Ref( bCube );
+ Cudd_RecursiveDeref( dd, bTemp );
+ // increment the counter
+ Counter ++;
+ }
+
+ // permute the functions
+ bFunc1 = Cudd_bddPermute( dd, bFunc, pPermute ); Cudd_Ref( bFunc1 );
+ // compose to gate the function depending on both vars
+ bFunc2 = Cudd_bddVectorCompose( dd, bFunc1, pCompose ); Cudd_Ref( bFunc2 );
+ // gate the vector space
+ // L(a) = ForAll x [ F(x) = F(x+a) ] = Not( Exist x [ F(x) (+) F(x+a) ] )
+ bSpaceShift = Cudd_bddXorExistAbstract( dd, bFunc1, bFunc2, bCube ); Cudd_Ref( bSpaceShift );
+ bSpaceShift = Cudd_Not( bSpaceShift );
+ // permute the space back into the original mapping
+ bSpace = Cudd_bddPermute( dd, bSpaceShift, pPermuteBack ); Cudd_Ref( bSpace );
+ Cudd_RecursiveDeref( dd, bFunc1 );
+ Cudd_RecursiveDeref( dd, bFunc2 );
+ Cudd_RecursiveDeref( dd, bSpaceShift );
+ Cudd_RecursiveDeref( dd, bCube );
+
+ for ( i = 0; i < dd->size; i++ )
+ Cudd_RecursiveDeref( dd, pCompose[i] );
+ free( pPermute );
+ free( pPermuteBack );
+ free( pCompose );
+ free( pSupport );
+
+ Cudd_Deref( bSpace );
+ return bSpace;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG )
+{
+ DdNode * bRes;
+ do {
+ dd->reordered = 0;
+ bRes = extraBddSpaceFromFunction( dd, bF, bG );
+ } while (dd->reordered == 1);
+ return bRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc )
+{
+ DdNode * bRes;
+ do {
+ dd->reordered = 0;
+ bRes = extraBddSpaceFromFunctionPos( dd, bFunc );
+ } while (dd->reordered == 1);
+ return bRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc )
+{
+ DdNode * bRes;
+ do {
+ dd->reordered = 0;
+ bRes = extraBddSpaceFromFunctionNeg( dd, bFunc );
+ } while (dd->reordered == 1);
+ return bRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace )
+{
+ DdNode * bRes;
+ do {
+ dd->reordered = 0;
+ bRes = extraBddSpaceCanonVars( dd, bSpace );
+ } while (dd->reordered == 1);
+ return bRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars )
+{
+ DdNode * bNegCube;
+ DdNode * bResult;
+ bNegCube = Extra_bddSupportNegativeCube( dd, bCanonVars ); Cudd_Ref( bNegCube );
+ bResult = Cudd_Cofactor( dd, bFunc, bNegCube ); Cudd_Ref( bResult );
+ Cudd_RecursiveDeref( dd, bNegCube );
+ Cudd_Deref( bResult );
+ return bResult;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace )
+{
+ DdNode * zRes;
+ DdNode * zEquPos;
+ DdNode * zEquNeg;
+ zEquPos = Extra_bddSpaceEquationsPos( dd, bSpace ); Cudd_Ref( zEquPos );
+ zEquNeg = Extra_bddSpaceEquationsNeg( dd, bSpace ); Cudd_Ref( zEquNeg );
+ zRes = Cudd_zddUnion( dd, zEquPos, zEquNeg ); Cudd_Ref( zRes );
+ Cudd_RecursiveDerefZdd( dd, zEquPos );
+ Cudd_RecursiveDerefZdd( dd, zEquNeg );
+ Cudd_Deref( zRes );
+ return zRes;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace )
+{
+ DdNode * zRes;
+ do {
+ dd->reordered = 0;
+ zRes = extraBddSpaceEquationsPos( dd, bSpace );
+ } while (dd->reordered == 1);
+ return zRes;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace )
+{
+ DdNode * zRes;
+ do {
+ dd->reordered = 0;
+ zRes = extraBddSpaceEquationsNeg( dd, bSpace );
+ } while (dd->reordered == 1);
+ return zRes;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA )
+{
+ DdNode * bRes;
+ do {
+ dd->reordered = 0;
+ bRes = extraBddSpaceFromMatrixPos( dd, zA );
+ } while (dd->reordered == 1);
+ return bRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA )
+{
+ DdNode * bRes;
+ do {
+ dd->reordered = 0;
+ bRes = extraBddSpaceFromMatrixNeg( dd, zA );
+ } while (dd->reordered == 1);
+ return bRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of literals in one combination.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Extra_zddLitCountComb( DdManager * dd, DdNode * zComb )
+{
+ int Counter;
+ if ( zComb == z0 )
+ return 0;
+ Counter = 0;
+ for ( ; zComb != z1; zComb = cuddT(zComb) )
+ Counter++;
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description [Returns the array of ZDDs with the number equal to the number of
+ vars in the DD manager. If the given var is non-canonical, this array contains
+ the referenced ZDD representing literals in the corresponding EXOR equation.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations )
+{
+ DdNode ** pzRes;
+ int * pVarsNonCan;
+ DdNode * zEquRem;
+ int iVarNonCan;
+ DdNode * zExor, * zTemp;
+
+ // get the set of non-canonical variables
+ pVarsNonCan = ALLOC( int, ddMax(dd->size,dd->sizeZ) );
+ Extra_SupportArray( dd, bFuncRed, pVarsNonCan );
+
+ // allocate storage for the EXOR sets
+ pzRes = ALLOC( DdNode *, dd->size );
+ memset( pzRes, 0, sizeof(DdNode *) * dd->size );
+
+ // go through all the equations
+ zEquRem = zEquations; Cudd_Ref( zEquRem );
+ while ( zEquRem != z0 )
+ {
+ // extract one product
+ zExor = Extra_zddSelectOneSubset( dd, zEquRem ); Cudd_Ref( zExor );
+ // remove it from the set
+ zEquRem = Cudd_zddDiff( dd, zTemp = zEquRem, zExor ); Cudd_Ref( zEquRem );
+ Cudd_RecursiveDerefZdd( dd, zTemp );
+
+ // locate the non-canonical variable
+ iVarNonCan = -1;
+ for ( zTemp = zExor; zTemp != z1; zTemp = cuddT(zTemp) )
+ {
+ if ( pVarsNonCan[zTemp->index/2] == 1 )
+ {
+ assert( iVarNonCan == -1 );
+ iVarNonCan = zTemp->index/2;
+ }
+ }
+ assert( iVarNonCan != -1 );
+
+ if ( Extra_zddLitCountComb( dd, zExor ) > 1 )
+ pzRes[ iVarNonCan ] = zExor; // takes ref
+ else
+ Cudd_RecursiveDerefZdd( dd, zExor );
+ }
+ Cudd_RecursiveDerefZdd( dd, zEquRem );
+
+ free( pVarsNonCan );
+ return pzRes;
+}
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+ Synopsis [Performs the recursive steps of Extra_bddSpaceFromFunction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG )
+{
+ DdNode * bRes;
+ DdNode * bFR, * bGR;
+
+ bFR = Cudd_Regular( bF );
+ bGR = Cudd_Regular( bG );
+ if ( cuddIsConstant(bFR) )
+ {
+ if ( bF == bG )
+ return b1;
+ else
+ return b0;
+ }
+ if ( cuddIsConstant(bGR) )
+ return b0;
+ // both bFunc and bCore are not constants
+
+ // the operation is commutative - normalize the problem
+ if ( (unsigned)bF > (unsigned)bG )
+ return extraBddSpaceFromFunction(dd, bG, bF);
+
+
+ if ( bRes = cuddCacheLookup2(dd, extraBddSpaceFromFunction, bF, bG) )
+ return bRes;
+ else
+ {
+ DdNode * bF0, * bF1;
+ DdNode * bG0, * bG1;
+ DdNode * bTemp1, * bTemp2;
+ DdNode * bRes0, * bRes1;
+ int LevelF, LevelG;
+ int index;
+
+ LevelF = dd->perm[bFR->index];
+ LevelG = dd->perm[bGR->index];
+ if ( LevelF <= LevelG )
+ {
+ index = dd->invperm[LevelF];
+ if ( bFR != bF )
+ {
+ bF0 = Cudd_Not( cuddE(bFR) );
+ bF1 = Cudd_Not( cuddT(bFR) );
+ }
+ else
+ {
+ bF0 = cuddE(bFR);
+ bF1 = cuddT(bFR);
+ }
+ }
+ else
+ {
+ index = dd->invperm[LevelG];
+ bF0 = bF1 = bF;
+ }
+
+ if ( LevelG <= LevelF )
+ {
+ if ( bGR != bG )
+ {
+ bG0 = Cudd_Not( cuddE(bGR) );
+ bG1 = Cudd_Not( cuddT(bGR) );
+ }
+ else
+ {
+ bG0 = cuddE(bGR);
+ bG1 = cuddT(bGR);
+ }
+ }
+ else
+ bG0 = bG1 = bG;
+
+ bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG0 );
+ if ( bTemp1 == NULL )
+ return NULL;
+ cuddRef( bTemp1 );
+
+ bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG1 );
+ if ( bTemp2 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bTemp1 );
+ return NULL;
+ }
+ cuddRef( bTemp2 );
+
+
+ bRes0 = cuddBddAndRecur( dd, bTemp1, bTemp2 );
+ if ( bRes0 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bTemp1 );
+ Cudd_RecursiveDeref( dd, bTemp2 );
+ return NULL;
+ }
+ cuddRef( bRes0 );
+ Cudd_RecursiveDeref( dd, bTemp1 );
+ Cudd_RecursiveDeref( dd, bTemp2 );
+
+
+ bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG1 );
+ if ( bTemp1 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ return NULL;
+ }
+ cuddRef( bTemp1 );
+
+ bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG0 );
+ if ( bTemp2 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ Cudd_RecursiveDeref( dd, bTemp1 );
+ return NULL;
+ }
+ cuddRef( bTemp2 );
+
+ bRes1 = cuddBddAndRecur( dd, bTemp1, bTemp2 );
+ if ( bRes1 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ Cudd_RecursiveDeref( dd, bTemp1 );
+ Cudd_RecursiveDeref( dd, bTemp2 );
+ return NULL;
+ }
+ cuddRef( bRes1 );
+ Cudd_RecursiveDeref( dd, bTemp1 );
+ Cudd_RecursiveDeref( dd, bTemp2 );
+
+
+
+ // consider the case when Res0 and Res1 are the same node
+ if ( bRes0 == bRes1 )
+ bRes = bRes1;
+ // consider the case when Res1 is complemented
+ else if ( Cudd_IsComplement(bRes1) )
+ {
+ bRes = cuddUniqueInter(dd, index, Cudd_Not(bRes1), Cudd_Not(bRes0));
+ if ( bRes == NULL )
+ {
+ Cudd_RecursiveDeref(dd,bRes0);
+ Cudd_RecursiveDeref(dd,bRes1);
+ return NULL;
+ }
+ bRes = Cudd_Not(bRes);
+ }
+ else
+ {
+ bRes = cuddUniqueInter( dd, index, bRes1, bRes0 );
+ if ( bRes == NULL )
+ {
+ Cudd_RecursiveDeref(dd,bRes0);
+ Cudd_RecursiveDeref(dd,bRes1);
+ return NULL;
+ }
+ }
+ cuddDeref( bRes0 );
+ cuddDeref( bRes1 );
+
+ // insert the result into cache
+ cuddCacheInsert2(dd, extraBddSpaceFromFunction, bF, bG, bRes);
+ return bRes;
+ }
+} /* end of extraBddSpaceFromFunction */
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bF )
+{
+ DdNode * bRes, * bFR;
+ statLine( dd );
+
+ bFR = Cudd_Regular(bF);
+ if ( cuddIsConstant(bFR) )
+ return b1;
+
+ if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionPos, bF) )
+ return bRes;
+ else
+ {
+ DdNode * bF0, * bF1;
+ DdNode * bPos0, * bPos1;
+ DdNode * bNeg0, * bNeg1;
+ DdNode * bRes0, * bRes1;
+
+ if ( bFR != bF ) // bF is complemented
+ {
+ bF0 = Cudd_Not( cuddE(bFR) );
+ bF1 = Cudd_Not( cuddT(bFR) );
+ }
+ else
+ {
+ bF0 = cuddE(bFR);
+ bF1 = cuddT(bFR);
+ }
+
+
+ bPos0 = extraBddSpaceFromFunctionPos( dd, bF0 );
+ if ( bPos0 == NULL )
+ return NULL;
+ cuddRef( bPos0 );
+
+ bPos1 = extraBddSpaceFromFunctionPos( dd, bF1 );
+ if ( bPos1 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bPos0 );
+ return NULL;
+ }
+ cuddRef( bPos1 );
+
+ bRes0 = cuddBddAndRecur( dd, bPos0, bPos1 );
+ if ( bRes0 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bPos0 );
+ Cudd_RecursiveDeref( dd, bPos1 );
+ return NULL;
+ }
+ cuddRef( bRes0 );
+ Cudd_RecursiveDeref( dd, bPos0 );
+ Cudd_RecursiveDeref( dd, bPos1 );
+
+
+ bNeg0 = extraBddSpaceFromFunctionNeg( dd, bF0 );
+ if ( bNeg0 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ return NULL;
+ }
+ cuddRef( bNeg0 );
+
+ bNeg1 = extraBddSpaceFromFunctionNeg( dd, bF1 );
+ if ( bNeg1 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ Cudd_RecursiveDeref( dd, bNeg0 );
+ return NULL;
+ }
+ cuddRef( bNeg1 );
+
+ bRes1 = cuddBddAndRecur( dd, bNeg0, bNeg1 );
+ if ( bRes1 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ Cudd_RecursiveDeref( dd, bNeg0 );
+ Cudd_RecursiveDeref( dd, bNeg1 );
+ return NULL;
+ }
+ cuddRef( bRes1 );
+ Cudd_RecursiveDeref( dd, bNeg0 );
+ Cudd_RecursiveDeref( dd, bNeg1 );
+
+
+ // consider the case when Res0 and Res1 are the same node
+ if ( bRes0 == bRes1 )
+ bRes = bRes1;
+ // consider the case when Res1 is complemented
+ else if ( Cudd_IsComplement(bRes1) )
+ {
+ bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) );
+ if ( bRes == NULL )
+ {
+ Cudd_RecursiveDeref(dd,bRes0);
+ Cudd_RecursiveDeref(dd,bRes1);
+ return NULL;
+ }
+ bRes = Cudd_Not(bRes);
+ }
+ else
+ {
+ bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
+ if ( bRes == NULL )
+ {
+ Cudd_RecursiveDeref(dd,bRes0);
+ Cudd_RecursiveDeref(dd,bRes1);
+ return NULL;
+ }
+ }
+ cuddDeref( bRes0 );
+ cuddDeref( bRes1 );
+
+ cuddCacheInsert1( dd, extraBddSpaceFromFunctionPos, bF, bRes );
+ return bRes;
+ }
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bF )
+{
+ DdNode * bRes, * bFR;
+ statLine( dd );
+
+ bFR = Cudd_Regular(bF);
+ if ( cuddIsConstant(bFR) )
+ return b0;
+
+ if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionNeg, bF) )
+ return bRes;
+ else
+ {
+ DdNode * bF0, * bF1;
+ DdNode * bPos0, * bPos1;
+ DdNode * bNeg0, * bNeg1;
+ DdNode * bRes0, * bRes1;
+
+ if ( bFR != bF ) // bF is complemented
+ {
+ bF0 = Cudd_Not( cuddE(bFR) );
+ bF1 = Cudd_Not( cuddT(bFR) );
+ }
+ else
+ {
+ bF0 = cuddE(bFR);
+ bF1 = cuddT(bFR);
+ }
+
+
+ bPos0 = extraBddSpaceFromFunctionNeg( dd, bF0 );
+ if ( bPos0 == NULL )
+ return NULL;
+ cuddRef( bPos0 );
+
+ bPos1 = extraBddSpaceFromFunctionNeg( dd, bF1 );
+ if ( bPos1 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bPos0 );
+ return NULL;
+ }
+ cuddRef( bPos1 );
+
+ bRes0 = cuddBddAndRecur( dd, bPos0, bPos1 );
+ if ( bRes0 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bPos0 );
+ Cudd_RecursiveDeref( dd, bPos1 );
+ return NULL;
+ }
+ cuddRef( bRes0 );
+ Cudd_RecursiveDeref( dd, bPos0 );
+ Cudd_RecursiveDeref( dd, bPos1 );
+
+
+ bNeg0 = extraBddSpaceFromFunctionPos( dd, bF0 );
+ if ( bNeg0 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ return NULL;
+ }
+ cuddRef( bNeg0 );
+
+ bNeg1 = extraBddSpaceFromFunctionPos( dd, bF1 );
+ if ( bNeg1 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ Cudd_RecursiveDeref( dd, bNeg0 );
+ return NULL;
+ }
+ cuddRef( bNeg1 );
+
+ bRes1 = cuddBddAndRecur( dd, bNeg0, bNeg1 );
+ if ( bRes1 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ Cudd_RecursiveDeref( dd, bNeg0 );
+ Cudd_RecursiveDeref( dd, bNeg1 );
+ return NULL;
+ }
+ cuddRef( bRes1 );
+ Cudd_RecursiveDeref( dd, bNeg0 );
+ Cudd_RecursiveDeref( dd, bNeg1 );
+
+
+ // consider the case when Res0 and Res1 are the same node
+ if ( bRes0 == bRes1 )
+ bRes = bRes1;
+ // consider the case when Res1 is complemented
+ else if ( Cudd_IsComplement(bRes1) )
+ {
+ bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) );
+ if ( bRes == NULL )
+ {
+ Cudd_RecursiveDeref(dd,bRes0);
+ Cudd_RecursiveDeref(dd,bRes1);
+ return NULL;
+ }
+ bRes = Cudd_Not(bRes);
+ }
+ else
+ {
+ bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
+ if ( bRes == NULL )
+ {
+ Cudd_RecursiveDeref(dd,bRes0);
+ Cudd_RecursiveDeref(dd,bRes1);
+ return NULL;
+ }
+ }
+ cuddDeref( bRes0 );
+ cuddDeref( bRes1 );
+
+ cuddCacheInsert1( dd, extraBddSpaceFromFunctionNeg, bF, bRes );
+ return bRes;
+ }
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs the recursive step of Extra_bddSpaceCanonVars().]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bF )
+{
+ DdNode * bRes, * bFR;
+ statLine( dd );
+
+ bFR = Cudd_Regular(bF);
+ if ( cuddIsConstant(bFR) )
+ return bF;
+
+ if ( bRes = cuddCacheLookup1(dd, extraBddSpaceCanonVars, bF) )
+ return bRes;
+ else
+ {
+ DdNode * bF0, * bF1;
+ DdNode * bRes, * bRes0;
+
+ if ( bFR != bF ) // bF is complemented
+ {
+ bF0 = Cudd_Not( cuddE(bFR) );
+ bF1 = Cudd_Not( cuddT(bFR) );
+ }
+ else
+ {
+ bF0 = cuddE(bFR);
+ bF1 = cuddT(bFR);
+ }
+
+ if ( bF0 == b0 )
+ {
+ bRes = extraBddSpaceCanonVars( dd, bF1 );
+ if ( bRes == NULL )
+ return NULL;
+ }
+ else if ( bF1 == b0 )
+ {
+ bRes = extraBddSpaceCanonVars( dd, bF0 );
+ if ( bRes == NULL )
+ return NULL;
+ }
+ else
+ {
+ bRes0 = extraBddSpaceCanonVars( dd, bF0 );
+ if ( bRes0 == NULL )
+ return NULL;
+ cuddRef( bRes0 );
+
+ bRes = cuddUniqueInter( dd, bFR->index, bRes0, b0 );
+ if ( bRes == NULL )
+ {
+ Cudd_RecursiveDeref( dd,bRes0 );
+ return NULL;
+ }
+ cuddDeref( bRes0 );
+ }
+
+ cuddCacheInsert1( dd, extraBddSpaceCanonVars, bF, bRes );
+ return bRes;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs the recursive step of Extra_bddSpaceEquationsPos().]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * extraBddSpaceEquationsPos( DdManager * dd, DdNode * bF )
+{
+ DdNode * zRes;
+ statLine( dd );
+
+ if ( bF == b0 )
+ return z1;
+ if ( bF == b1 )
+ return z0;
+
+ if ( zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsPos, bF) )
+ return zRes;
+ else
+ {
+ DdNode * bFR, * bF0, * bF1;
+ DdNode * zPos0, * zPos1, * zNeg1;
+ DdNode * zRes, * zRes0, * zRes1;
+
+ bFR = Cudd_Regular(bF);
+ if ( bFR != bF ) // bF is complemented
+ {
+ bF0 = Cudd_Not( cuddE(bFR) );
+ bF1 = Cudd_Not( cuddT(bFR) );
+ }
+ else
+ {
+ bF0 = cuddE(bFR);
+ bF1 = cuddT(bFR);
+ }
+
+ if ( bF0 == b0 )
+ {
+ zRes1 = extraBddSpaceEquationsPos( dd, bF1 );
+ if ( zRes1 == NULL )
+ return NULL;
+ cuddRef( zRes1 );
+
+ // add the current element to the set
+ zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes1 );
+ if ( zRes == NULL )
+ {
+ Cudd_RecursiveDerefZdd(dd, zRes1);
+ return NULL;
+ }
+ cuddDeref( zRes1 );
+ }
+ else if ( bF1 == b0 )
+ {
+ zRes = extraBddSpaceEquationsPos( dd, bF0 );
+ if ( zRes == NULL )
+ return NULL;
+ }
+ else
+ {
+ zPos0 = extraBddSpaceEquationsPos( dd, bF0 );
+ if ( zPos0 == NULL )
+ return NULL;
+ cuddRef( zPos0 );
+
+ zPos1 = extraBddSpaceEquationsPos( dd, bF1 );
+ if ( zPos1 == NULL )
+ {
+ Cudd_RecursiveDerefZdd(dd, zPos0);
+ return NULL;
+ }
+ cuddRef( zPos1 );
+
+ zNeg1 = extraBddSpaceEquationsNeg( dd, bF1 );
+ if ( zNeg1 == NULL )
+ {
+ Cudd_RecursiveDerefZdd(dd, zPos0);
+ Cudd_RecursiveDerefZdd(dd, zPos1);
+ return NULL;
+ }
+ cuddRef( zNeg1 );
+
+
+ zRes0 = cuddZddIntersect( dd, zPos0, zPos1 );
+ if ( zRes0 == NULL )
+ {
+ Cudd_RecursiveDerefZdd(dd, zNeg1);
+ Cudd_RecursiveDerefZdd(dd, zPos0);
+ Cudd_RecursiveDerefZdd(dd, zPos1);
+ return NULL;
+ }
+ cuddRef( zRes0 );
+
+ zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 );
+ if ( zRes1 == NULL )
+ {
+ Cudd_RecursiveDerefZdd(dd, zRes0);
+ Cudd_RecursiveDerefZdd(dd, zNeg1);
+ Cudd_RecursiveDerefZdd(dd, zPos0);
+ Cudd_RecursiveDerefZdd(dd, zPos1);
+ return NULL;
+ }
+ cuddRef( zRes1 );
+ Cudd_RecursiveDerefZdd(dd, zNeg1);
+ Cudd_RecursiveDerefZdd(dd, zPos0);
+ Cudd_RecursiveDerefZdd(dd, zPos1);
+ // only zRes0 and zRes1 are refed at this point
+
+ zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 );
+ if ( zRes == NULL )
+ {
+ Cudd_RecursiveDerefZdd(dd, zRes0);
+ Cudd_RecursiveDerefZdd(dd, zRes1);
+ return NULL;
+ }
+ cuddDeref( zRes0 );
+ cuddDeref( zRes1 );
+ }
+
+ cuddCacheInsert1( dd, extraBddSpaceEquationsPos, bF, zRes );
+ return zRes;
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs the recursive step of Extra_bddSpaceEquationsNev().]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bF )
+{
+ DdNode * zRes;
+ statLine( dd );
+
+ if ( bF == b0 )
+ return z1;
+ if ( bF == b1 )
+ return z0;
+
+ if ( zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsNeg, bF) )
+ return zRes;
+ else
+ {
+ DdNode * bFR, * bF0, * bF1;
+ DdNode * zPos0, * zPos1, * zNeg1;
+ DdNode * zRes, * zRes0, * zRes1;
+
+ bFR = Cudd_Regular(bF);
+ if ( bFR != bF ) // bF is complemented
+ {
+ bF0 = Cudd_Not( cuddE(bFR) );
+ bF1 = Cudd_Not( cuddT(bFR) );
+ }
+ else
+ {
+ bF0 = cuddE(bFR);
+ bF1 = cuddT(bFR);
+ }
+
+ if ( bF0 == b0 )
+ {
+ zRes = extraBddSpaceEquationsNeg( dd, bF1 );
+ if ( zRes == NULL )
+ return NULL;
+ }
+ else if ( bF1 == b0 )
+ {
+ zRes0 = extraBddSpaceEquationsNeg( dd, bF0 );
+ if ( zRes0 == NULL )
+ return NULL;
+ cuddRef( zRes0 );
+
+ // add the current element to the set
+ zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes0 );
+ if ( zRes == NULL )
+ {
+ Cudd_RecursiveDerefZdd(dd, zRes0);
+ return NULL;
+ }
+ cuddDeref( zRes0 );
+ }
+ else
+ {
+ zPos0 = extraBddSpaceEquationsNeg( dd, bF0 );
+ if ( zPos0 == NULL )
+ return NULL;
+ cuddRef( zPos0 );
+
+ zPos1 = extraBddSpaceEquationsNeg( dd, bF1 );
+ if ( zPos1 == NULL )
+ {
+ Cudd_RecursiveDerefZdd(dd, zPos0);
+ return NULL;
+ }
+ cuddRef( zPos1 );
+
+ zNeg1 = extraBddSpaceEquationsPos( dd, bF1 );
+ if ( zNeg1 == NULL )
+ {
+ Cudd_RecursiveDerefZdd(dd, zPos0);
+ Cudd_RecursiveDerefZdd(dd, zPos1);
+ return NULL;
+ }
+ cuddRef( zNeg1 );
+
+
+ zRes0 = cuddZddIntersect( dd, zPos0, zPos1 );
+ if ( zRes0 == NULL )
+ {
+ Cudd_RecursiveDerefZdd(dd, zNeg1);
+ Cudd_RecursiveDerefZdd(dd, zPos0);
+ Cudd_RecursiveDerefZdd(dd, zPos1);
+ return NULL;
+ }
+ cuddRef( zRes0 );
+
+ zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 );
+ if ( zRes1 == NULL )
+ {
+ Cudd_RecursiveDerefZdd(dd, zRes0);
+ Cudd_RecursiveDerefZdd(dd, zNeg1);
+ Cudd_RecursiveDerefZdd(dd, zPos0);
+ Cudd_RecursiveDerefZdd(dd, zPos1);
+ return NULL;
+ }
+ cuddRef( zRes1 );
+ Cudd_RecursiveDerefZdd(dd, zNeg1);
+ Cudd_RecursiveDerefZdd(dd, zPos0);
+ Cudd_RecursiveDerefZdd(dd, zPos1);
+ // only zRes0 and zRes1 are refed at this point
+
+ zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 );
+ if ( zRes == NULL )
+ {
+ Cudd_RecursiveDerefZdd(dd, zRes0);
+ Cudd_RecursiveDerefZdd(dd, zRes1);
+ return NULL;
+ }
+ cuddDeref( zRes0 );
+ cuddDeref( zRes1 );
+ }
+
+ cuddCacheInsert1( dd, extraBddSpaceEquationsNeg, bF, zRes );
+ return zRes;
+ }
+}
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA )
+{
+ DdNode * bRes;
+ statLine( dd );
+
+ if ( zA == z0 )
+ return b1;
+ if ( zA == z1 )
+ return b1;
+
+ if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixPos, zA) )
+ return bRes;
+ else
+ {
+ DdNode * bP0, * bP1;
+ DdNode * bN0, * bN1;
+ DdNode * bRes0, * bRes1;
+
+ bP0 = extraBddSpaceFromMatrixPos( dd, cuddE(zA) );
+ if ( bP0 == NULL )
+ return NULL;
+ cuddRef( bP0 );
+
+ bP1 = extraBddSpaceFromMatrixPos( dd, cuddT(zA) );
+ if ( bP1 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bP0 );
+ return NULL;
+ }
+ cuddRef( bP1 );
+
+ bRes0 = cuddBddAndRecur( dd, bP0, bP1 );
+ if ( bRes0 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bP0 );
+ Cudd_RecursiveDeref( dd, bP1 );
+ return NULL;
+ }
+ cuddRef( bRes0 );
+ Cudd_RecursiveDeref( dd, bP0 );
+ Cudd_RecursiveDeref( dd, bP1 );
+
+
+ bN0 = extraBddSpaceFromMatrixPos( dd, cuddE(zA) );
+ if ( bN0 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ return NULL;
+ }
+ cuddRef( bN0 );
+
+ bN1 = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) );
+ if ( bN1 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ Cudd_RecursiveDeref( dd, bN0 );
+ return NULL;
+ }
+ cuddRef( bN1 );
+
+ bRes1 = cuddBddAndRecur( dd, bN0, bN1 );
+ if ( bRes1 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ Cudd_RecursiveDeref( dd, bN0 );
+ Cudd_RecursiveDeref( dd, bN1 );
+ return NULL;
+ }
+ cuddRef( bRes1 );
+ Cudd_RecursiveDeref( dd, bN0 );
+ Cudd_RecursiveDeref( dd, bN1 );
+
+
+ // consider the case when Res0 and Res1 are the same node
+ if ( bRes0 == bRes1 )
+ bRes = bRes1;
+ // consider the case when Res1 is complemented
+ else if ( Cudd_IsComplement(bRes1) )
+ {
+ bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) );
+ if ( bRes == NULL )
+ {
+ Cudd_RecursiveDeref(dd,bRes0);
+ Cudd_RecursiveDeref(dd,bRes1);
+ return NULL;
+ }
+ bRes = Cudd_Not(bRes);
+ }
+ else
+ {
+ bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 );
+ if ( bRes == NULL )
+ {
+ Cudd_RecursiveDeref(dd,bRes0);
+ Cudd_RecursiveDeref(dd,bRes1);
+ return NULL;
+ }
+ }
+ cuddDeref( bRes0 );
+ cuddDeref( bRes1 );
+
+ cuddCacheInsert1( dd, extraBddSpaceFromMatrixPos, zA, bRes );
+ return bRes;
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA )
+{
+ DdNode * bRes;
+ statLine( dd );
+
+ if ( zA == z0 )
+ return b1;
+ if ( zA == z1 )
+ return b0;
+
+ if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixNeg, zA) )
+ return bRes;
+ else
+ {
+ DdNode * bP0, * bP1;
+ DdNode * bN0, * bN1;
+ DdNode * bRes0, * bRes1;
+
+ bP0 = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) );
+ if ( bP0 == NULL )
+ return NULL;
+ cuddRef( bP0 );
+
+ bP1 = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) );
+ if ( bP1 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bP0 );
+ return NULL;
+ }
+ cuddRef( bP1 );
+
+ bRes0 = cuddBddAndRecur( dd, bP0, bP1 );
+ if ( bRes0 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bP0 );
+ Cudd_RecursiveDeref( dd, bP1 );
+ return NULL;
+ }
+ cuddRef( bRes0 );
+ Cudd_RecursiveDeref( dd, bP0 );
+ Cudd_RecursiveDeref( dd, bP1 );
+
+
+ bN0 = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) );
+ if ( bN0 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ return NULL;
+ }
+ cuddRef( bN0 );
+
+ bN1 = extraBddSpaceFromMatrixPos( dd, cuddT(zA) );
+ if ( bN1 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ Cudd_RecursiveDeref( dd, bN0 );
+ return NULL;
+ }
+ cuddRef( bN1 );
+
+ bRes1 = cuddBddAndRecur( dd, bN0, bN1 );
+ if ( bRes1 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ Cudd_RecursiveDeref( dd, bN0 );
+ Cudd_RecursiveDeref( dd, bN1 );
+ return NULL;
+ }
+ cuddRef( bRes1 );
+ Cudd_RecursiveDeref( dd, bN0 );
+ Cudd_RecursiveDeref( dd, bN1 );
+
+
+ // consider the case when Res0 and Res1 are the same node
+ if ( bRes0 == bRes1 )
+ bRes = bRes1;
+ // consider the case when Res1 is complemented
+ else if ( Cudd_IsComplement(bRes1) )
+ {
+ bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) );
+ if ( bRes == NULL )
+ {
+ Cudd_RecursiveDeref(dd,bRes0);
+ Cudd_RecursiveDeref(dd,bRes1);
+ return NULL;
+ }
+ bRes = Cudd_Not(bRes);
+ }
+ else
+ {
+ bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 );
+ if ( bRes == NULL )
+ {
+ Cudd_RecursiveDeref(dd,bRes0);
+ Cudd_RecursiveDeref(dd,bRes1);
+ return NULL;
+ }
+ }
+ cuddDeref( bRes0 );
+ cuddDeref( bRes1 );
+
+ cuddCacheInsert1( dd, extraBddSpaceFromMatrixNeg, zA, bRes );
+ return bRes;
+ }
+}
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions */
+/*---------------------------------------------------------------------------*/
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 15:55:08 +0000