/**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 "extraBdd.h"
ABC_NAMESPACE_IMPL_START
/*---------------------------------------------------------------------------*/
/* 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 = ABC_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 );
ABC_FREE( pSupport );
return NULL;
}
// create the permutation arrays
pPermute = ABC_ALLOC( int, dd->size );
pPermuteBack = ABC_ALLOC( int, dd->size );
pCompose = ABC_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] );
ABC_FREE( pPermute );
ABC_FREE( pPermuteBack );
ABC_FREE( pCompose );
ABC_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 = ABC_ALLOC( int, ddMax(dd->size,dd->sizeZ) );
Extra_SupportArray( dd, bFuncRed, pVarsNonCan );
// allocate storage for the EXOR sets
pzRes = ABC_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 );
ABC_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)(ABC_PTRUINT_T)bF > (unsigned)(ABC_PTRUINT_T)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 */
/*---------------------------------------------------------------------------*/
ABC_NAMESPACE_IMPL_END