Version abc50729

1 files changed, 438 insertions, 0 deletions

diff --git a/src/bdd/reo/reoCore.c b/src/bdd/reo/reoCore.c
new file mode 100644
index 00000000..3782631c
--- /dev/null
+++ b/src/bdd/reo/reoCore.c
@@ -0,0 +1,438 @@
+/**CFile****************************************************************
+
+  FileName    [reoCore.c]
+
+  PackageName [REO: A specialized DD reordering engine.]
+
+  Synopsis    [Implementation of the core reordering procedure.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - October 15, 2002.]
+
+  Revision    [$Id: reoCore.c,v 1.0 2002/15/10 03:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "reo.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#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;
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DEFINITIONS                          ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the internal manager data structures.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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;
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Dereferences units the data structure after reordering.]
+
+  Description [This function is only useful for debugging.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks the zero references for the given plane.]
+
+  Description [This function is only useful for debugging.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int reoCheckZeroRefs( reo_plane * pPlane )
+{
+    reo_unit * pUnit;
+    for ( pUnit = pPlane->pHead; pUnit; pUnit = pUnit->Next )
+    {
+        if ( pUnit->n != 0 )
+        {
+            assert( 0 );
+        }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks the zero references for the given plane.]
+
+  Description [This function is only useful for debugging.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                         END OF FILE                              ///
+////////////////////////////////////////////////////////////////////////
+