extraBddImage.c

Go to the documentation of this file.

 
#include "extraBdd.h"
 
ABC_NAMESPACE_IMPL_START
 
 
/* 
    The ideas implemented in this file are inspired by the paper:
    Pankaj Chauhan, Edmund Clarke, Somesh Jha, Jim Kukula, Tom Shiple, 
    Helmut Veith, Dong Wang. Non-linear Quantification Scheduling in 
    Image Computation. ICCAD, 2001.
*/
 
/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/
 
/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/
 
typedef struct Extra_ImageNode_t_  Extra_ImageNode_t;
typedef struct Extra_ImagePart_t_  Extra_ImagePart_t;
typedef struct Extra_ImageVar_t_   Extra_ImageVar_t;
 
struct Extra_ImageTree_t_
{
    Extra_ImageNode_t * pRoot;      // the root of quantification tree
    Extra_ImageNode_t * pCare;      // the leaf node with the care set
    DdNode *            bCareSupp;  // the cube to quantify from the care
    int                 fVerbose;   // the verbosity flag
    int                 nNodesMax;  // the max number of nodes in one iter
    int                 nNodesMaxT; // the overall max number of nodes
    int                 nIter;      // the number of iterations with this tree
};
 
struct Extra_ImageNode_t_
{
    DdManager *         dd;         // the manager 
    DdNode *            bCube;      // the cube to quantify
    DdNode *            bImage;     // the partial image
    Extra_ImageNode_t * pNode1;     // the first branch
    Extra_ImageNode_t * pNode2;     // the second branch
    Extra_ImagePart_t * pPart;      // the partition (temporary)
};
 
struct Extra_ImagePart_t_
{
    DdNode *            bFunc;      // the partition
    DdNode *            bSupp;      // the support of this partition
    int                 nNodes;     // the number of BDD nodes
    short               nSupp;      // the number of support variables
    short               iPart;      // the number of this partition
};
 
struct Extra_ImageVar_t_
{
    int                 iNum;       // the BDD index of this variable
    DdNode *            bParts;     // the partition numbers
    int                 nParts;     // the number of partitions
};
 
/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
 
/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
 
/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

 
 
/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/
 
static Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
    int nParts, DdNode ** pbParts, DdNode * bCare );
static Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
    int nParts, Extra_ImagePart_t ** pParts,
    int nVars, DdNode ** pbVarsNs );
static Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd, 
    int nParts, Extra_ImagePart_t ** pParts, 
    int nVars,  Extra_ImageVar_t ** pVars );
static void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode );
static int Extra_BuildTreeNode( DdManager * dd, 
    int nNodes, Extra_ImageNode_t ** pNodes, 
    int nVars,  Extra_ImageVar_t ** pVars );
static Extra_ImageNode_t * Extra_MergeTopNodes( DdManager * dd, 
    int nNodes, Extra_ImageNode_t ** pNodes );
static void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode );
static void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode );
static int Extra_FindBestVariable( DdManager * dd,
    int nNodes, Extra_ImageNode_t ** pNodes, 
    int nVars,  Extra_ImageVar_t ** pVars );
static void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts, 
    int nNodes, Extra_ImageNode_t ** pNodes, 
    int * piNode1, int * piNode2 );
static Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
    Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 );
 
static void Extra_bddImagePrintLatchDependency( DdManager * dd, DdNode * bCare,
    int nParts, DdNode ** pbParts,
    int nVars, DdNode ** pbVars );
static void Extra_bddImagePrintLatchDependencyOne( DdManager * dd, DdNode * bFunc, 
    DdNode * bVarsCs, DdNode * bVarsNs, int iPart );
 
static void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree );
static void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int nOffset );
 

 
 
/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

Extra_ImageTree_t * Extra_bddImageStart( 
    DdManager * dd, DdNode * bCare, // the care set
    int nParts, DdNode ** pbParts,  // the partitions for image computation
    int nVars, DdNode ** pbVars, int fVerbose )   // the NS and parameter variables (not quantified!)
{
    Extra_ImageTree_t * pTree;
    Extra_ImagePart_t ** pParts;
    Extra_ImageVar_t ** pVars;
    Extra_ImageNode_t ** pNodes;
    int v;
 
    if ( fVerbose && dd->size <= 80 )
        Extra_bddImagePrintLatchDependency( dd, bCare, nParts, pbParts, nVars, pbVars );
 
    // create variables, partitions and leaf nodes
    pParts = Extra_CreateParts( dd, nParts, pbParts, bCare );
    pVars  = Extra_CreateVars( dd, nParts + 1, pParts, nVars, pbVars );
    pNodes = Extra_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars );
    
    // create the tree
    pTree = ABC_ALLOC( Extra_ImageTree_t, 1 );
    memset( pTree, 0, sizeof(Extra_ImageTree_t) );
    pTree->pCare = pNodes[nParts];
    pTree->fVerbose = fVerbose;
 
    // process the nodes
    while ( Extra_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars ) );
 
    // make sure the variables are gone
    for ( v = 0; v < dd->size; v++ )
        assert( pVars[v] == NULL );
    ABC_FREE( pVars );
 
    // merge the topmost nodes
    while ( (pTree->pRoot = Extra_MergeTopNodes( dd, nParts + 1, pNodes )) == NULL );
 
    // make sure the nodes are gone
    for ( v = 0; v < nParts + 1; v++ )
        assert( pNodes[v] == NULL );
    ABC_FREE( pNodes );
 
//    if ( fVerbose )
//        Extra_bddImagePrintTree( pTree );
 
    // set the support of the care set
    pTree->bCareSupp = Cudd_Support( dd, bCare );  Cudd_Ref( pTree->bCareSupp );
 
    // clean the partitions
    Extra_DeleteParts_rec( pTree->pRoot );
    ABC_FREE( pParts );
    return pTree;
}

DdNode * Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare )
{
    DdManager * dd = pTree->pCare->dd;
    DdNode * bSupp, * bRem;
 
    pTree->nIter++;
 
    // make sure the supports are okay
    bSupp = Cudd_Support( dd, bCare );        Cudd_Ref( bSupp );
    if ( bSupp != pTree->bCareSupp )
    {
        bRem = Cudd_bddExistAbstract( dd, bSupp, pTree->bCareSupp );  Cudd_Ref( bRem );
        if ( bRem != b1 )
        {
printf( "Original care set support: " );
ABC_PRB( dd, pTree->bCareSupp );
printf( "Current care set support: " );
ABC_PRB( dd, bSupp );
            Cudd_RecursiveDeref( dd, bSupp );
            Cudd_RecursiveDeref( dd, bRem );
            printf( "The care set depends on some vars that were not in the care set during scheduling.\n" );
            return NULL;
        }
        Cudd_RecursiveDeref( dd, bRem );
    }
    Cudd_RecursiveDeref( dd, bSupp );
 
    // remove the previous image
    Cudd_RecursiveDeref( dd, pTree->pCare->bImage );
    pTree->pCare->bImage = bCare;   Cudd_Ref( bCare );
 
    // compute the image
    pTree->nNodesMax = 0;
    Extra_bddImageCompute_rec( pTree, pTree->pRoot );
    if ( pTree->nNodesMaxT < pTree->nNodesMax )
        pTree->nNodesMaxT = pTree->nNodesMax;
 
//    if ( pTree->fVerbose )
//        printf( "Iter %2d : Max nodes = %5d.\n", pTree->nIter, pTree->nNodesMax );
    return pTree->pRoot->bImage;
}

void Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree )
{
    if ( pTree->bCareSupp )
        Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp );
    Extra_bddImageTreeDelete_rec( pTree->pRoot );
    ABC_FREE( pTree );
}

DdNode * Extra_bddImageRead( Extra_ImageTree_t * pTree )
{
    return pTree->pRoot->bImage;
}
 
/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/
 
/*---------------------------------------------------------------------------*/
/* Definition of static Functions                                            */
/*---------------------------------------------------------------------------*/

Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
    int nParts, DdNode ** pbParts, DdNode * bCare )
{
    Extra_ImagePart_t ** pParts;
    int i;
 
    // start the partitions
    pParts = ABC_ALLOC( Extra_ImagePart_t *, nParts + 1 );
    // create structures for each variable
    for ( i = 0; i < nParts; i++ )
    {
        pParts[i] = ABC_ALLOC( Extra_ImagePart_t, 1 );
        pParts[i]->bFunc  = pbParts[i];                           Cudd_Ref( pParts[i]->bFunc );
        pParts[i]->bSupp  = Cudd_Support( dd, pParts[i]->bFunc ); Cudd_Ref( pParts[i]->bSupp );
        pParts[i]->nSupp  = Extra_bddSuppSize( dd, pParts[i]->bSupp );
        pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
        pParts[i]->iPart  = i;
    }
    // add the care set as the last partition
    pParts[nParts] = ABC_ALLOC( Extra_ImagePart_t, 1 );
    pParts[nParts]->bFunc = bCare;                                     Cudd_Ref( pParts[nParts]->bFunc );
    pParts[nParts]->bSupp = Cudd_Support( dd, pParts[nParts]->bFunc ); Cudd_Ref( pParts[nParts]->bSupp );
    pParts[nParts]->nSupp = Extra_bddSuppSize( dd, pParts[nParts]->bSupp );
    pParts[nParts]->nNodes = Cudd_DagSize( pParts[nParts]->bFunc );
    pParts[nParts]->iPart  = nParts;
    return pParts;
}

Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
    int nParts, Extra_ImagePart_t ** pParts,
    int nVars, DdNode ** pbVars )
{
    Extra_ImageVar_t ** pVars;
    DdNode ** pbFuncs;
    DdNode * bCubeNs, * bSupp, * bParts, * bTemp, * bSuppTemp;
    int nVarsTotal, iVar, p, Counter;
 
    // put all the functions into one array
    pbFuncs = ABC_ALLOC( DdNode *, nParts );
    for ( p = 0; p < nParts; p++ )
        pbFuncs[p] = pParts[p]->bSupp;
    bSupp = Cudd_VectorSupport( dd, pbFuncs, nParts );  Cudd_Ref( bSupp );
    ABC_FREE( pbFuncs );
 
    // remove the NS vars
    bCubeNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars );        Cudd_Ref( bCubeNs );
    bSupp = Cudd_bddExistAbstract( dd, bTemp = bSupp, bCubeNs );     Cudd_Ref( bSupp );
    Cudd_RecursiveDeref( dd, bTemp );
    Cudd_RecursiveDeref( dd, bCubeNs );
 
    // get the number of I and CS variables to be quantified
    nVarsTotal = Extra_bddSuppSize( dd, bSupp );
 
    // start the variables
    pVars = ABC_ALLOC( Extra_ImageVar_t *, dd->size );
    memset( pVars, 0, sizeof(Extra_ImageVar_t *) * dd->size );
    // create structures for each variable
    for ( bSuppTemp = bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
    {
        iVar = bSuppTemp->index;
        pVars[iVar] = ABC_ALLOC( Extra_ImageVar_t, 1 );
        pVars[iVar]->iNum = iVar;
        // collect all the parts this var belongs to
        Counter = 0;
        bParts = b1; Cudd_Ref( bParts );
        for ( p = 0; p < nParts; p++ )
            if ( Cudd_bddLeq( dd, pParts[p]->bSupp, dd->vars[bSuppTemp->index] ) )
            {
                bParts = Cudd_bddAnd( dd, bTemp = bParts, dd->vars[p] );  Cudd_Ref( bParts );
                Cudd_RecursiveDeref( dd, bTemp );
                Counter++;
            }
        pVars[iVar]->bParts = bParts; // takes ref
        pVars[iVar]->nParts = Counter;
    }
    Cudd_RecursiveDeref( dd, bSupp );
    return pVars;
}

Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd, 
    int nParts, Extra_ImagePart_t ** pParts, 
    int nVars,  Extra_ImageVar_t ** pVars )
{
    Extra_ImageNode_t ** pNodes;
    Extra_ImageNode_t * pNode;
    DdNode * bTemp;
    int i, v, iPart;
/*
    DdManager *         dd;       // the manager 
    DdNode *            bCube;    // the cube to quantify
    DdNode *            bImage;   // the partial image
    Extra_ImageNode_t * pNode1;   // the first branch
    Extra_ImageNode_t * pNode2;   // the second branch
    Extra_ImagePart_t * pPart;    // the partition (temporary)
*/
    // start the partitions
    pNodes = ABC_ALLOC( Extra_ImageNode_t *, nParts );
    // create structures for each leaf nodes
    for ( i = 0; i < nParts; i++ )
    {
        pNodes[i] = ABC_ALLOC( Extra_ImageNode_t, 1 );
        memset( pNodes[i], 0, sizeof(Extra_ImageNode_t) );
        pNodes[i]->dd    = dd;
        pNodes[i]->pPart = pParts[i];
    }
    // find the quantification cubes for each leaf node
    for ( v = 0; v < nVars; v++ )
    {
        if ( pVars[v] == NULL )
            continue;
        assert( pVars[v]->nParts > 0 );
        if ( pVars[v]->nParts > 1 )
            continue;
        iPart = pVars[v]->bParts->index;
        if ( pNodes[iPart]->bCube == NULL )
        {
            pNodes[iPart]->bCube = dd->vars[v];   
            Cudd_Ref( dd->vars[v] );
        }
        else
        {
            pNodes[iPart]->bCube = Cudd_bddAnd( dd, bTemp = pNodes[iPart]->bCube, dd->vars[v] );  
            Cudd_Ref( pNodes[iPart]->bCube );
            Cudd_RecursiveDeref( dd, bTemp );
        }
        // remove these  variables
        Cudd_RecursiveDeref( dd, pVars[v]->bParts );
        ABC_FREE( pVars[v] );
    }
 
    // assign the leaf node images
    for ( i = 0; i < nParts; i++ )
    {
        pNode = pNodes[i];
        if ( pNode->bCube )
        {
            // update the partition
            pParts[i]->bFunc = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bFunc, pNode->bCube );
            Cudd_Ref( pParts[i]->bFunc );
            Cudd_RecursiveDeref( dd, bTemp );
            // update the support the partition
            pParts[i]->bSupp = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bSupp, pNode->bCube ); 
            Cudd_Ref( pParts[i]->bSupp );
            Cudd_RecursiveDeref( dd, bTemp );
            // update the numbers
            pParts[i]->nSupp  = Extra_bddSuppSize( dd, pParts[i]->bSupp );
            pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
            // get rid of the cube
            // save the last (care set) quantification cube
            if ( i < nParts - 1 )
            {
                Cudd_RecursiveDeref( dd, pNode->bCube );
                pNode->bCube = NULL;
            }
        }
        // copy the function
        pNode->bImage = pParts[i]->bFunc;   Cudd_Ref( pNode->bImage );
    }
/*
    for ( i = 0; i < nParts; i++ )
    {
        pNode = pNodes[i];
ABC_PRB( dd, pNode->bCube );
ABC_PRB( dd, pNode->pPart->bFunc );
ABC_PRB( dd, pNode->pPart->bSupp );
printf( "\n" );
    }
*/
    return pNodes;
}
 

void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode )
{
    Extra_ImagePart_t * pPart;
    if ( pNode->pNode1 )
        Extra_DeleteParts_rec( pNode->pNode1 );
    if ( pNode->pNode2 )
        Extra_DeleteParts_rec( pNode->pNode2 );
    pPart = pNode->pPart;
    Cudd_RecursiveDeref( pNode->dd, pPart->bFunc );
    Cudd_RecursiveDeref( pNode->dd, pPart->bSupp );
    ABC_FREE( pNode->pPart );
}

void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode )
{
    if ( pNode->pNode1 )
        Extra_bddImageTreeDelete_rec( pNode->pNode1 );
    if ( pNode->pNode2 )
        Extra_bddImageTreeDelete_rec( pNode->pNode2 );
    if ( pNode->bCube )
        Cudd_RecursiveDeref( pNode->dd, pNode->bCube );
    if ( pNode->bImage )
        Cudd_RecursiveDeref( pNode->dd, pNode->bImage );
    assert( pNode->pPart == NULL );
    ABC_FREE( pNode );
}

void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode )
{
    DdManager * dd = pNode->dd;
    DdNode * bTemp;
    int nNodes;
 
    // trivial case
    if ( pNode->pNode1 == NULL )
    {
        if ( pNode->bCube )
        {
            pNode->bImage = Cudd_bddExistAbstract( dd, bTemp = pNode->bImage, pNode->bCube ); 
            Cudd_Ref( pNode->bImage );
            Cudd_RecursiveDeref( dd, bTemp );
        }
        return;
    }
 
    // compute the children
    if ( pNode->pNode1 )
        Extra_bddImageCompute_rec( pTree, pNode->pNode1 );
    if ( pNode->pNode2 )
        Extra_bddImageCompute_rec( pTree, pNode->pNode2 );
 
    // clean the old image
    if ( pNode->bImage )
        Cudd_RecursiveDeref( dd, pNode->bImage );
    pNode->bImage = NULL;
 
    // compute the new image
    if ( pNode->bCube )
        pNode->bImage = Cudd_bddAndAbstract( dd, 
            pNode->pNode1->bImage, pNode->pNode2->bImage, pNode->bCube );
    else
        pNode->bImage = Cudd_bddAnd( dd, pNode->pNode1->bImage, pNode->pNode2->bImage );
    Cudd_Ref( pNode->bImage );
 
    if ( pTree->fVerbose )
    {
        nNodes = Cudd_DagSize( pNode->bImage );
        if ( pTree->nNodesMax < nNodes )
            pTree->nNodesMax = nNodes;
    }
}

int Extra_BuildTreeNode( DdManager * dd, 
    int nNodes, Extra_ImageNode_t ** pNodes, 
    int nVars,  Extra_ImageVar_t ** pVars )
{
    Extra_ImageNode_t * pNode1, * pNode2;
    Extra_ImageVar_t * pVar;
    Extra_ImageNode_t * pNode;
    DdNode * bCube, * bTemp, * bSuppTemp, * bParts;
    int iNode1, iNode2;
    int iVarBest, nSupp, v;
 
    // find the best variable
    iVarBest = Extra_FindBestVariable( dd, nNodes, pNodes, nVars, pVars );
    if ( iVarBest == -1 )
        return 0;
 
    pVar = pVars[iVarBest];
 
    // this var cannot appear in one partition only
    nSupp = Extra_bddSuppSize( dd, pVar->bParts );
    assert( nSupp == pVar->nParts );
    assert( nSupp != 1 );
 
    // if it appears in only two partitions, quantify it
    if ( pVar->nParts == 2 )
    {
        // get the nodes
        iNode1 = pVar->bParts->index;
        iNode2 = cuddT(pVar->bParts)->index;
        pNode1 = pNodes[iNode1];
        pNode2 = pNodes[iNode2];
 
        // get the quantification cube
        bCube = dd->vars[pVar->iNum];    Cudd_Ref( bCube );
        // add the variables that appear only in these partitions
        for ( v = 0; v < nVars; v++ )
            if ( pVars[v] && v != iVarBest && pVars[v]->bParts == pVars[iVarBest]->bParts )
            {
                // add this var
                bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[pVars[v]->iNum] );   Cudd_Ref( bCube );
                Cudd_RecursiveDeref( dd, bTemp );
                // clean this var
                Cudd_RecursiveDeref( dd, pVars[v]->bParts );
                ABC_FREE( pVars[v] );
            }
        // clean the best var
        Cudd_RecursiveDeref( dd, pVars[iVarBest]->bParts );
        ABC_FREE( pVars[iVarBest] );
 
        // combines two nodes
        pNode = Extra_CombineTwoNodes( dd, bCube, pNode1, pNode2 );
        Cudd_RecursiveDeref( dd, bCube );
    }
    else // if ( pVar->nParts > 2 )
    {
        // find two smallest BDDs that have this var
        Extra_FindBestPartitions( dd, pVar->bParts, nNodes, pNodes, &iNode1, &iNode2 );
        pNode1 = pNodes[iNode1];
        pNode2 = pNodes[iNode2];
 
        // it is not possible that a var appears only in these two
        // otherwise, it would have a different cost
        bParts = Cudd_bddAnd( dd, dd->vars[iNode1], dd->vars[iNode2] ); Cudd_Ref( bParts );
        for ( v = 0; v < nVars; v++ )
            if ( pVars[v] && pVars[v]->bParts == bParts )
                assert( 0 );
        Cudd_RecursiveDeref( dd, bParts );
 
        // combines two nodes
        pNode = Extra_CombineTwoNodes( dd, b1, pNode1, pNode2 );
    }
 
    // clean the old nodes
    pNodes[iNode1] = pNode;
    pNodes[iNode2] = NULL;
    
    // update the variables that appear in pNode[iNode2]
    for ( bSuppTemp = pNode2->pPart->bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
    {
        pVar = pVars[bSuppTemp->index];
        if ( pVar == NULL ) // this variable is not be quantified
            continue;
        // quantify this var
        assert( Cudd_bddLeq( dd, pVar->bParts, dd->vars[iNode2] ) );
        pVar->bParts = Cudd_bddExistAbstract( dd, bTemp = pVar->bParts, dd->vars[iNode2] ); Cudd_Ref( pVar->bParts );
        Cudd_RecursiveDeref( dd, bTemp );
        // add the new var
        pVar->bParts = Cudd_bddAnd( dd, bTemp = pVar->bParts, dd->vars[iNode1] ); Cudd_Ref( pVar->bParts );
        Cudd_RecursiveDeref( dd, bTemp );
        // update the score
        pVar->nParts = Extra_bddSuppSize( dd, pVar->bParts );
    }
    return 1;
}
 

Extra_ImageNode_t * Extra_MergeTopNodes(
    DdManager * dd, int nNodes, Extra_ImageNode_t ** pNodes )
{
    Extra_ImageNode_t * pNode;
    int n1 = -1, n2 = -1, n;
 
    // find the first and the second non-empty spots
    for ( n = 0; n < nNodes; n++ )
        if ( pNodes[n] )
        {
            if ( n1 == -1 )
                n1 = n;
            else if ( n2 == -1 )
            {
                n2 = n;
                break;
            }
        }
    assert( n1 != -1 );
    // check the situation when only one such node is detected
    if ( n2 == -1 )
    {
        // save the node
        pNode = pNodes[n1];
        // clean the node
        pNodes[n1] = NULL;
        return pNode;
    }
  
    // combines two nodes
    pNode = Extra_CombineTwoNodes( dd, b1, pNodes[n1], pNodes[n2] );
 
    // clean the old nodes
    pNodes[n1] = pNode;
    pNodes[n2] = NULL;
    return NULL;
}

Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
    Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 )
{
    Extra_ImageNode_t * pNode;
    Extra_ImagePart_t * pPart;
 
    // create a new partition
    pPart = ABC_ALLOC( Extra_ImagePart_t, 1 );
    memset( pPart, 0, sizeof(Extra_ImagePart_t) );
    // create the function
    pPart->bFunc = Cudd_bddAndAbstract( dd, pNode1->pPart->bFunc, pNode2->pPart->bFunc, bCube );
    Cudd_Ref( pPart->bFunc );
    // update the support the partition
    pPart->bSupp = Cudd_bddAndAbstract( dd, pNode1->pPart->bSupp, pNode2->pPart->bSupp, bCube );
    Cudd_Ref( pPart->bSupp );
    // update the numbers
    pPart->nSupp  = Extra_bddSuppSize( dd, pPart->bSupp );
    pPart->nNodes = Cudd_DagSize( pPart->bFunc );
    pPart->iPart = -1;
/*
ABC_PRB( dd, pNode1->pPart->bSupp );
ABC_PRB( dd, pNode2->pPart->bSupp );
ABC_PRB( dd, pPart->bSupp );
*/
    // create a new node
    pNode = ABC_ALLOC( Extra_ImageNode_t, 1 );
    memset( pNode, 0, sizeof(Extra_ImageNode_t) );
    pNode->dd     = dd;
    pNode->pPart  = pPart;
    pNode->pNode1 = pNode1;
    pNode->pNode2 = pNode2;
    // compute the image
    pNode->bImage = Cudd_bddAndAbstract( dd, pNode1->bImage, pNode2->bImage, bCube ); 
    Cudd_Ref( pNode->bImage );
    // save the cube
    if ( bCube != b1 )
    {
        pNode->bCube = bCube;   Cudd_Ref( bCube );
    }
    return pNode;
}

int Extra_FindBestVariable( DdManager * dd,
    int nNodes, Extra_ImageNode_t ** pNodes, 
    int nVars,  Extra_ImageVar_t ** pVars )
{
    DdNode * bTemp;
    int iVarBest, v;
    double CostBest, CostCur;
 
    CostBest = 100000000000000.0;
    iVarBest = -1;
    for ( v = 0; v < nVars; v++ )
        if ( pVars[v] )
        {
            CostCur = 0;
            for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) )
                CostCur += pNodes[bTemp->index]->pPart->nNodes * 
                           pNodes[bTemp->index]->pPart->nNodes;
            if ( CostBest > CostCur )
            {
                CostBest = CostCur;
                iVarBest = v;
            }
        }
    return iVarBest;
}

void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts, 
    int nNodes, Extra_ImageNode_t ** pNodes, 
    int * piNode1, int * piNode2 )
{
    DdNode * bTemp;
    int iPart1, iPart2;
    int CostMin1, CostMin2, Cost;
 
    // go through the partitions
    iPart1 = iPart2 = -1;
    CostMin1 = CostMin2 = 1000000;
    for ( bTemp = bParts; bTemp != b1; bTemp = cuddT(bTemp) )
    {
        Cost = pNodes[bTemp->index]->pPart->nNodes;
        if ( CostMin1 > Cost )
        {
            CostMin2 = CostMin1;    iPart2 = iPart1;
            CostMin1 = Cost;        iPart1 = bTemp->index;
        }
        else if ( CostMin2 > Cost )
        {
            CostMin2 = Cost;        iPart2 = bTemp->index;
        }
    }
 
    *piNode1 = iPart1;
    *piNode2 = iPart2;
}

void Extra_bddImagePrintLatchDependency( 
    DdManager * dd, DdNode * bCare, // the care set
    int nParts, DdNode ** pbParts,  // the partitions for image computation
    int nVars, DdNode ** pbVars )   // the NS and parameter variables (not quantified!)
{
    int i;
    DdNode * bVarsCs, * bVarsNs;
 
    bVarsCs = Cudd_Support( dd, bCare );                       Cudd_Ref( bVarsCs );
    bVarsNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars );  Cudd_Ref( bVarsNs );
 
    printf( "The latch dependency matrix:\n" );
    printf( "Partitions = %d   Variables: total = %d  non-quantifiable = %d\n",
        nParts, dd->size, nVars );
    printf( "     : " );
    for ( i = 0; i < dd->size; i++ )
        printf( "%d", i % 10 );
    printf( "\n" );
 
    for ( i = 0; i < nParts; i++ )
        Extra_bddImagePrintLatchDependencyOne( dd, pbParts[i], bVarsCs, bVarsNs, i );
    Extra_bddImagePrintLatchDependencyOne( dd, bCare, bVarsCs, bVarsNs, nParts );
 
    Cudd_RecursiveDeref( dd, bVarsCs );
    Cudd_RecursiveDeref( dd, bVarsNs );
}

void Extra_bddImagePrintLatchDependencyOne(
    DdManager * dd, DdNode * bFunc,      // the function
    DdNode * bVarsCs, DdNode * bVarsNs,  // the current/next state vars
    int iPart )
{
    DdNode * bSupport;
    int v;
    bSupport = Cudd_Support( dd, bFunc );  Cudd_Ref( bSupport );
    printf( " %3d : ", iPart );
    for ( v = 0; v < dd->size; v++ )
    {
        if ( Cudd_bddLeq( dd, bSupport, dd->vars[v] ) )
        {
            if ( Cudd_bddLeq( dd, bVarsCs, dd->vars[v] ) )
                printf( "c" );
            else if ( Cudd_bddLeq( dd, bVarsNs, dd->vars[v] ) ) 
                printf( "n" );
            else
                printf( "i" );
        }
        else
            printf( "." );
    }
    printf( "\n" );
    Cudd_RecursiveDeref( dd, bSupport );
}
 

void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree )
{
    printf( "The quantification scheduling tree:\n" );
    Extra_bddImagePrintTree_rec( pTree->pRoot, 1 );
}

void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int Offset )
{
    DdNode * Cube;
    int i;
 
    Cube = pNode->bCube;
 
    if ( pNode->pNode1 == NULL )
    {
        printf( "<%d> ", pNode->pPart->iPart );
        if ( Cube != NULL )
        {
            ABC_PRB( pNode->dd, Cube );
        }
        else
            printf( "\n" );
        return;
    }
 
    printf( "<*> " );
    if ( Cube != NULL )
    {
        ABC_PRB( pNode->dd, Cube );
    }
    else
        printf( "\n" );
 
    for ( i = 0; i < Offset; i++ )
        printf( "    " );
    Extra_bddImagePrintTree_rec( pNode->pNode1, Offset + 1 );
 
    for ( i = 0; i < Offset; i++ )
        printf( "    " );
    Extra_bddImagePrintTree_rec( pNode->pNode2, Offset + 1 );
}
 
 
 
 
 
struct Extra_ImageTree2_t_
{
    DdManager * dd;
    DdNode *    bRel;
    DdNode *    bCube;
    DdNode *    bImage;
};

Extra_ImageTree2_t * Extra_bddImageStart2( 
    DdManager * dd, DdNode * bCare,
    int nParts, DdNode ** pbParts,
    int nVars, DdNode ** pbVars, int fVerbose )
{
    Extra_ImageTree2_t * pTree;
    DdNode * bCubeAll, * bCubeNot, * bTemp;
    int i;
 
    pTree = ABC_ALLOC( Extra_ImageTree2_t, 1 );
    pTree->dd = dd;
    pTree->bImage = NULL;
 
    bCubeAll = Extra_bddComputeCube( dd, dd->vars, dd->size );      Cudd_Ref( bCubeAll );
    bCubeNot = Extra_bddComputeCube( dd, pbVars,   nVars );         Cudd_Ref( bCubeNot );
    pTree->bCube = Cudd_bddExistAbstract( dd, bCubeAll, bCubeNot ); Cudd_Ref( pTree->bCube );
    Cudd_RecursiveDeref( dd, bCubeAll );
    Cudd_RecursiveDeref( dd, bCubeNot );
 
    // derive the monolithic relation
    pTree->bRel = b1;   Cudd_Ref( pTree->bRel );
    for ( i = 0; i < nParts; i++ )
    {
        pTree->bRel = Cudd_bddAnd( dd, bTemp = pTree->bRel, pbParts[i] ); Cudd_Ref( pTree->bRel );
        Cudd_RecursiveDeref( dd, bTemp );
    }
    Extra_bddImageCompute2( pTree, bCare );
    return pTree;
}
 

DdNode * Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare )
{
    if ( pTree->bImage )
        Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
    pTree->bImage = Cudd_bddAndAbstract( pTree->dd, pTree->bRel, bCare, pTree->bCube ); 
    Cudd_Ref( pTree->bImage );
    return pTree->bImage;
}

void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree )
{
    if ( pTree->bRel )
        Cudd_RecursiveDeref( pTree->dd, pTree->bRel );
    if ( pTree->bCube )
        Cudd_RecursiveDeref( pTree->dd, pTree->bCube );
    if ( pTree->bImage )
        Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
    ABC_FREE( pTree );
}

DdNode * Extra_bddImageRead2( Extra_ImageTree2_t * pTree )
{
    return pTree->bImage;
}
 

 
 
ABC_NAMESPACE_IMPL_END