src/bdd/reo/reoCore.c

Go to the documentation of this file.

#include "reo.h"


#define CALLOC(type, num)  ((type *) calloc((long)(num), (long)sizeof(type)))

static int  reoRecursiveDeref( reo_unit * pUnit );
static int  reoCheckZeroRefs( reo_plane * pPlane );
static int  reoCheckLevels( reo_man * p );

double s_AplBefore;
double s_AplAfter;


void reoReorderArray( reo_man * p, DdManager * dd, DdNode * Funcs[], DdNode * FuncsRes[], int nFuncs, int * pOrder )
{
        int Counter, i;

        // set the initial parameters
        p->dd     = dd;
        p->pOrder = pOrder;
        p->nTops  = nFuncs;
        // get the initial number of nodes
        p->nNodesBeg = Cudd_SharingSize( Funcs, nFuncs );     
        // resize the internal data structures of the manager if necessary
        reoResizeStructures( p, ddMax(dd->size,dd->sizeZ), p->nNodesBeg, nFuncs );
        // compute the support
        p->pSupp = Extra_VectorSupportArray( dd, Funcs, nFuncs, p->pSupp );
        // get the number of support variables
        p->nSupp = 0;
        for ( i = 0; i < dd->size; i++ )
                p->nSupp += p->pSupp[i];

        // if it is the constant function, no need to reorder
        if ( p->nSupp == 0 )
        {
                for ( i = 0; i < nFuncs; i++ )
                {
                        FuncsRes[i] = Funcs[i]; Cudd_Ref( FuncsRes[i] );
                }
                return;
        }

        // create the internal variable maps
        // go through variable levels in the manager
        Counter = 0;
        for ( i = 0; i < dd->size; i++ )
                if ( p->pSupp[ dd->invperm[i] ] )
                {
                        p->pMapToPlanes[ dd->invperm[i] ] = Counter;
                        p->pMapToDdVarsOrig[Counter]      = dd->invperm[i];
                        if ( !p->fRemapUp )
                                p->pMapToDdVarsFinal[Counter] = dd->invperm[i];
                        else
                                p->pMapToDdVarsFinal[Counter] = dd->invperm[Counter];
                        p->pOrderInt[Counter]        = Counter;
                        Counter++;
                }

        // set the initial parameters
        p->nUnitsUsed = 0;
        p->nNodesCur  = 0;
        p->fThisIsAdd = 0;
        p->Signature++;
        // transfer the function from the CUDD package into REO"s internal data structure
        for ( i = 0; i < nFuncs; i++ )
                p->pTops[i] = reoTransferNodesToUnits_rec( p, Funcs[i] );
        assert( p->nNodesBeg == p->nNodesCur );

        if ( !p->fThisIsAdd && p->fMinWidth )
        {
                printf( "An important message from the REO reordering engine:\n" );
                printf( "The BDD given to the engine for reordering contains complemented edges.\n" );
                printf( "Currently, such BDDs cannot be reordered for the minimum width.\n" );
                printf( "Therefore, minimization for the number of BDD nodes is performed.\n" );
                fflush( stdout );
                p->fMinApl   = 0;
                p->fMinWidth = 0;
        }

        if ( p->fMinWidth )
                reoProfileWidthStart(p);
        else if ( p->fMinApl )
                reoProfileAplStart(p);
        else 
                reoProfileNodesStart(p);

        if ( p->fVerbose )
        {
                printf( "INITIAL: " );
                if ( p->fMinWidth )
                        reoProfileWidthPrint(p);
                else if ( p->fMinApl )
                        reoProfileAplPrint(p);
                else
                        reoProfileNodesPrint(p);
        }
 
        // performs the reordering
        p->nSwaps   = 0;
        p->nNISwaps = 0;
        for ( i = 0; i < p->nIters; i++ )
        {
                reoReorderSift( p );
                // print statistics after each iteration
                if ( p->fVerbose )
                {
                        printf( "ITER #%d: ", i+1 );
                        if ( p->fMinWidth )
                                reoProfileWidthPrint(p);
                        else if ( p->fMinApl )
                                reoProfileAplPrint(p);
                        else
                                reoProfileNodesPrint(p);
                }
                // if the cost function did not change, stop iterating
                if ( p->fMinWidth )
                {
                        p->nWidthEnd = p->nWidthCur;
                        assert( p->nWidthEnd <= p->nWidthBeg );
                        if ( p->nWidthEnd == p->nWidthBeg )
                                break;
                }
                else if ( p->fMinApl )
                {
                        p->nAplEnd = p->nAplCur;
                        assert( p->nAplEnd <= p->nAplBeg );
                        if ( p->nAplEnd == p->nAplBeg )
                                break;
                }
                else
                {
                        p->nNodesEnd = p->nNodesCur;
                        assert( p->nNodesEnd <= p->nNodesBeg );
                        if ( p->nNodesEnd == p->nNodesBeg )
                                break;
                }
        }
        assert( reoCheckLevels( p ) );

s_AplBefore = p->nAplBeg;
s_AplAfter  = p->nAplEnd;

        // set the initial parameters
        p->nRefNodes  = 0;
        p->nNodesCur  = 0;
        p->Signature++;
        // transfer the BDDs from REO's internal data structure to CUDD
        for ( i = 0; i < nFuncs; i++ )
        {
                FuncsRes[i] = reoTransferUnitsToNodes_rec( p, p->pTops[i] ); Cudd_Ref( FuncsRes[i] );
        }
        // undo the DDs referenced for storing in the cache
        for ( i = 0; i < p->nRefNodes; i++ )
                Cudd_RecursiveDeref( dd, p->pRefNodes[i] );
        // verify zero refs of the terminal nodes
        for ( i = 0; i < nFuncs; i++ )
        {
                assert( reoRecursiveDeref( p->pTops[i] ) );
        }
        assert( reoCheckZeroRefs( &(p->pPlanes[p->nSupp]) ) );

        // prepare the variable map to return to the user
        if ( p->pOrder )
        {
                // i is the current level in the planes data structure
                // p->pOrderInt[i] is the original level in the planes data structure
                // p->pMapToDdVarsOrig[i] is the variable, into which we remap when we construct the BDD from planes
                // p->pMapToDdVarsOrig[ p->pOrderInt[i] ] is the original BDD variable corresponding to this level
                // Therefore, p->pOrder[ p->pMapToDdVarsFinal[i] ] = p->pMapToDdVarsOrig[ p->pOrderInt[i] ]
                // creates the permutation, which remaps the resulting BDD variable into the original BDD variable
                for ( i = 0; i < p->nSupp; i++ )
                        p->pOrder[ p->pMapToDdVarsFinal[i] ] = p->pMapToDdVarsOrig[ p->pOrderInt[i] ]; 
        }

        if ( p->fVerify )
        {
                int fVerification;
                DdNode * FuncRemapped;
                int * pOrder;

                if ( p->pOrder == NULL )
                {
                        pOrder = ALLOC( int, p->nSupp );
                        for ( i = 0; i < p->nSupp; i++ )
                                pOrder[ p->pMapToDdVarsFinal[i] ] = p->pMapToDdVarsOrig[ p->pOrderInt[i] ]; 
                }
                else
                        pOrder = p->pOrder;

                fVerification = 1;
                for ( i = 0; i < nFuncs; i++ )
                {
                        // verify the result
                        if ( p->fThisIsAdd )
                                FuncRemapped = Cudd_addPermute( dd, FuncsRes[i], pOrder );
                        else
                                FuncRemapped = Cudd_bddPermute( dd, FuncsRes[i], pOrder );
                        Cudd_Ref( FuncRemapped );

                        if ( FuncRemapped != Funcs[i] )
                        {
                                fVerification = 0;
                                printf( "REO: Internal verification has failed!\n" );
                                fflush( stdout );
                        }
                        Cudd_RecursiveDeref( dd, FuncRemapped );
                }
                if ( fVerification )
                        printf( "REO: Internal verification is okay!\n" );

                if ( p->pOrder == NULL )
                        free( pOrder );
        }

        // recycle the data structure
        for ( i = 0; i <= p->nSupp; i++ )
                reoUnitsRecycleUnitList( p, p->pPlanes + i );
}

void reoResizeStructures( reo_man * p, int nDdVarsMax, int nNodesMax, int nFuncs )
{
        // resize data structures depending on the number of variables in the DD manager
        if ( p->nSuppAlloc == 0 )
        {
                p->pSupp             = ALLOC( int,        nDdVarsMax + 1 );
                p->pOrderInt         = ALLOC( int,        nDdVarsMax + 1 );
                p->pMapToPlanes      = ALLOC( int,        nDdVarsMax + 1 );
                p->pMapToDdVarsOrig  = ALLOC( int,        nDdVarsMax + 1 );
                p->pMapToDdVarsFinal = ALLOC( int,        nDdVarsMax + 1 );
                p->pPlanes           = CALLOC( reo_plane, nDdVarsMax + 1 );
                p->pVarCosts         = ALLOC( double,     nDdVarsMax + 1 );
                p->pLevelOrder       = ALLOC( int,        nDdVarsMax + 1 );
                p->nSuppAlloc        = nDdVarsMax + 1;
        }
        else if ( p->nSuppAlloc < nDdVarsMax )
        {
                free( p->pSupp );
                free( p->pOrderInt );
                free( p->pMapToPlanes );
                free( p->pMapToDdVarsOrig );
                free( p->pMapToDdVarsFinal );
                free( p->pPlanes );
                free( p->pVarCosts );
                free( p->pLevelOrder );

                p->pSupp             = ALLOC( int,        nDdVarsMax + 1 );
                p->pOrderInt         = ALLOC( int,        nDdVarsMax + 1 );
                p->pMapToPlanes      = ALLOC( int,        nDdVarsMax + 1 );
                p->pMapToDdVarsOrig  = ALLOC( int,        nDdVarsMax + 1 );
                p->pMapToDdVarsFinal = ALLOC( int,        nDdVarsMax + 1 );
                p->pPlanes           = CALLOC( reo_plane, nDdVarsMax + 1 );
                p->pVarCosts         = ALLOC( double,     nDdVarsMax + 1 );
                p->pLevelOrder       = ALLOC( int,        nDdVarsMax + 1 );
                p->nSuppAlloc        = nDdVarsMax + 1;
        }

        // resize the data structures depending on the number of nodes
        if ( p->nRefNodesAlloc == 0 )
        {
                p->nNodesMaxAlloc  = nNodesMax;
                p->nTableSize      = 3*nNodesMax + 1;
                p->nRefNodesAlloc  = 3*nNodesMax + 1;
                p->nMemChunksAlloc = (10*nNodesMax + 1)/REO_CHUNK_SIZE + 1;

                p->HTable          = CALLOC( reo_hash,  p->nTableSize );
                p->pRefNodes       = ALLOC( DdNode *,   p->nRefNodesAlloc );
                p->pWidthCofs      = ALLOC( reo_unit *, p->nRefNodesAlloc );
                p->pMemChunks      = ALLOC( reo_unit *, p->nMemChunksAlloc );
        }
        else if ( p->nNodesMaxAlloc < nNodesMax )
        {
                void * pTemp;
                int nMemChunksAllocPrev = p->nMemChunksAlloc;

                p->nNodesMaxAlloc  = nNodesMax;
                p->nTableSize      = 3*nNodesMax + 1;
                p->nRefNodesAlloc  = 3*nNodesMax + 1;
                p->nMemChunksAlloc = (10*nNodesMax + 1)/REO_CHUNK_SIZE + 1;

                free( p->HTable );
                free( p->pRefNodes );
                free( p->pWidthCofs );
                p->HTable          = CALLOC( reo_hash,    p->nTableSize );
                p->pRefNodes       = ALLOC(  DdNode *,    p->nRefNodesAlloc );
                p->pWidthCofs      = ALLOC(  reo_unit *,  p->nRefNodesAlloc );
                // p->pMemChunks should be reallocated because it contains pointers currently in use
                pTemp              = ALLOC(  reo_unit *,  p->nMemChunksAlloc );
                memmove( pTemp, p->pMemChunks, sizeof(reo_unit *) * nMemChunksAllocPrev );
                free( p->pMemChunks );
                p->pMemChunks      = pTemp;
        }

        // resize the data structures depending on the number of functions
        if ( p->nTopsAlloc == 0 )
        {
                p->pTops      = ALLOC( reo_unit *, nFuncs );
                p->nTopsAlloc = nFuncs;
        }
        else if ( p->nTopsAlloc < nFuncs )
        {
                free( p->pTops );
                p->pTops      = ALLOC( reo_unit *, nFuncs );
                p->nTopsAlloc = nFuncs;
        }
}


int reoRecursiveDeref( reo_unit * pUnit )
{
        reo_unit * pUnitR;
        pUnitR = Unit_Regular(pUnit);
        pUnitR->n--;
        if ( Unit_IsConstant(pUnitR) )
                return 1;
        if ( pUnitR->n == 0 )
        {
                reoRecursiveDeref( pUnitR->pE );
                reoRecursiveDeref( pUnitR->pT );
        }
        return 1;
}

int reoCheckZeroRefs( reo_plane * pPlane )
{
        reo_unit * pUnit;
        for ( pUnit = pPlane->pHead; pUnit; pUnit = pUnit->Next )
        {
                if ( pUnit->n != 0 )
                {
                        assert( 0 );
                }
        }
        return 1;
}

int reoCheckLevels( reo_man * p )
{
        reo_unit * pUnit;
        int i;

        for ( i = 0; i < p->nSupp; i++ )
        {
                // there are some nodes left on each level
                assert( p->pPlanes[i].statsNodes );
                for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next )
                {
                        // the level is properly set
                        assert( pUnit->lev == i );
                }
        }
        return 1;
}

---