extraBddAuto.c File Reference

#include "extraBdd.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START DdNode *	Extra_bddSpaceFromFunctionFast (DdManager *dd, DdNode *bFunc)
DdNode *	Extra_bddSpaceFromFunction (DdManager *dd, DdNode *bF, DdNode *bG)
DdNode *	Extra_bddSpaceFromFunctionPos (DdManager *dd, DdNode *bFunc)
DdNode *	Extra_bddSpaceFromFunctionNeg (DdManager *dd, DdNode *bFunc)
DdNode *	Extra_bddSpaceCanonVars (DdManager *dd, DdNode *bSpace)
DdNode *	Extra_bddSpaceReduce (DdManager *dd, DdNode *bFunc, DdNode *bCanonVars)
DdNode *	Extra_bddSpaceEquations (DdManager *dd, DdNode *bSpace)
DdNode *	Extra_bddSpaceEquationsPos (DdManager *dd, DdNode *bSpace)
DdNode *	Extra_bddSpaceEquationsNeg (DdManager *dd, DdNode *bSpace)
DdNode *	Extra_bddSpaceFromMatrixPos (DdManager *dd, DdNode *zA)
DdNode *	Extra_bddSpaceFromMatrixNeg (DdManager *dd, DdNode *zA)
int	Extra_zddLitCountComb (DdManager *dd, DdNode *zComb)
DdNode **	Extra_bddSpaceExorGates (DdManager *dd, DdNode *bFuncRed, DdNode *zEquations)
DdNode *	extraBddSpaceFromFunction (DdManager *dd, DdNode *bF, DdNode *bG)
DdNode *	extraBddSpaceFromFunctionPos (DdManager *dd, DdNode *bF)
DdNode *	extraBddSpaceFromFunctionNeg (DdManager *dd, DdNode *bF)
DdNode *	extraBddSpaceCanonVars (DdManager *dd, DdNode *bF)
DdNode *	extraBddSpaceEquationsPos (DdManager *dd, DdNode *bF)
DdNode *	extraBddSpaceEquationsNeg (DdManager *dd, DdNode *bF)
DdNode *	extraBddSpaceFromMatrixPos (DdManager *dd, DdNode *zA)
DdNode *	extraBddSpaceFromMatrixNeg (DdManager *dd, DdNode *zA)

Function Documentation

DdNode* Extra_bddSpaceCanonVars	(	DdManager *	dd,
		DdNode *	bSpace
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 316 of file extraBddAuto.c.

{
    DdNode * bRes;
    do {
        dd->reordered = 0;
        bRes = extraBddSpaceCanonVars( dd, bSpace );
    } while (dd->reordered == 1);
    return bRes;
}

DdNode* Extra_bddSpaceEquations	(	DdManager *	dd,
		DdNode *	bSpace
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 361 of file extraBddAuto.c.

{
    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;
}

DdNode* Extra_bddSpaceEquationsNeg	(	DdManager *	dd,
		DdNode *	bSpace
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 409 of file extraBddAuto.c.

{
    DdNode * zRes;
    do {
        dd->reordered = 0;
        zRes = extraBddSpaceEquationsNeg( dd, bSpace );
    } while (dd->reordered == 1);
    return zRes;
}

DdNode* Extra_bddSpaceEquationsPos	(	DdManager *	dd,
		DdNode *	bSpace
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 387 of file extraBddAuto.c.

{
    DdNode * zRes;
    do {
        dd->reordered = 0;
        zRes = extraBddSpaceEquationsPos( dd, bSpace );
    } while (dd->reordered == 1);
    return zRes;
}

DdNode** Extra_bddSpaceExorGates	(	DdManager *	dd,
		DdNode *	bFuncRed,
		DdNode *	zEquations
	)

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 []

Definition at line 497 of file extraBddAuto.c.

{
    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;
}

DdNode* Extra_bddSpaceFromFunction	(	DdManager *	dd,
		DdNode *	bF,
		DdNode *	bG
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 253 of file extraBddAuto.c.

{
    DdNode * bRes;
    do {
        dd->reordered = 0;
        bRes = extraBddSpaceFromFunction( dd, bF, bG );
    } while (dd->reordered == 1);
    return bRes;
}

ABC_NAMESPACE_IMPL_START DdNode* Extra_bddSpaceFromFunctionFast	(	DdManager *	dd,
		DdNode *	bFunc
	)

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

]AutomaticStart AutomaticEnd Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 153 of file extraBddAuto.c.

{
    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;
}

DdNode* Extra_bddSpaceFromFunctionNeg	(	DdManager *	dd,
		DdNode *	bFunc
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 295 of file extraBddAuto.c.

{
    DdNode * bRes;
    do {
        dd->reordered = 0;
        bRes = extraBddSpaceFromFunctionNeg( dd, bFunc );
    } while (dd->reordered == 1);
    return bRes;
}

DdNode* Extra_bddSpaceFromFunctionPos	(	DdManager *	dd,
		DdNode *	bFunc
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 274 of file extraBddAuto.c.

{
    DdNode * bRes;
    do {
        dd->reordered = 0;
        bRes = extraBddSpaceFromFunctionPos( dd, bFunc );
    } while (dd->reordered == 1);
    return bRes;
}

DdNode* Extra_bddSpaceFromMatrixNeg	(	DdManager *	dd,
		DdNode *	zA
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 452 of file extraBddAuto.c.

{
    DdNode * bRes;
    do {
        dd->reordered = 0;
        bRes = extraBddSpaceFromMatrixNeg( dd, zA );
    } while (dd->reordered == 1);
    return bRes;
}

DdNode* Extra_bddSpaceFromMatrixPos	(	DdManager *	dd,
		DdNode *	zA
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 431 of file extraBddAuto.c.

{
    DdNode * bRes;
    do {
        dd->reordered = 0;
        bRes = extraBddSpaceFromMatrixPos( dd, zA );
    } while (dd->reordered == 1);
    return bRes;
}

DdNode* Extra_bddSpaceReduce	(	DdManager *	dd,
		DdNode *	bFunc,
		DdNode *	bCanonVars
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 337 of file extraBddAuto.c.

{
    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;
}

int Extra_zddLitCountComb	(	DdManager *	dd,
		DdNode *	zComb
	)

Function*************************************************************

Synopsis [Counts the number of literals in one combination.]

Description []

SideEffects []

SeeAlso []

Definition at line 473 of file extraBddAuto.c.

{
    int Counter;
    if ( zComb == z0 )
        return 0;
    Counter = 0;
    for ( ; zComb != z1; zComb = cuddT(zComb) )
        Counter++;
    return Counter;
}

DdNode* extraBddSpaceCanonVars	(	DdManager *	dd,
		DdNode *	bF
	)

Function*************************************************************

Synopsis [Performs the recursive step of Extra_bddSpaceCanonVars().]

Description []

SideEffects []

SeeAlso []

Definition at line 1000 of file extraBddAuto.c.

{
    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;
    }
}

DdNode* extraBddSpaceEquationsNeg	(	DdManager *	dd,
		DdNode *	bF
	)

Function*************************************************************

Synopsis [Performs the recursive step of Extra_bddSpaceEquationsNev().]

Description []

SideEffects []

SeeAlso []

Definition at line 1201 of file extraBddAuto.c.

{
    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;
    }
}

DdNode* extraBddSpaceEquationsPos	(	DdManager *	dd,
		DdNode *	bF
	)

Function*************************************************************

Synopsis [Performs the recursive step of Extra_bddSpaceEquationsPos().]

Description []

SideEffects []

SeeAlso []

Definition at line 1071 of file extraBddAuto.c.

{
    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;
    }
}

DdNode* extraBddSpaceFromFunction	(	DdManager *	dd,
		DdNode *	bF,
		DdNode *	bG
	)

Function********************************************************************

Synopsis [Performs the recursive steps of Extra_bddSpaceFromFunction.]

Description []

SideEffects []

SeeAlso []

Definition at line 562 of file extraBddAuto.c.

{
    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 */

DdNode* extraBddSpaceFromFunctionNeg	(	DdManager *	dd,
		DdNode *	bF
	)

Function*************************************************************

Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]

Description []

SideEffects []

SeeAlso []

Definition at line 869 of file extraBddAuto.c.

{
    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;
    }
}

DdNode* extraBddSpaceFromFunctionPos	(	DdManager *	dd,
		DdNode *	bF
	)

Function*************************************************************

Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]

Description []

SideEffects []

SeeAlso []

Definition at line 738 of file extraBddAuto.c.

{
    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;
    }
}

DdNode* extraBddSpaceFromMatrixNeg	(	DdManager *	dd,
		DdNode *	zA
	)

Function*************************************************************

Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]

Description []

SideEffects []

SeeAlso []

Definition at line 1451 of file extraBddAuto.c.

{
    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;
    }
}

DdNode* extraBddSpaceFromMatrixPos	(	DdManager *	dd,
		DdNode *	zA
	)

Function*************************************************************

Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]

Description []

SideEffects []

SeeAlso []

Definition at line 1333 of file extraBddAuto.c.

{
    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;
    }
}