bbrImage.c File Reference

#include "bbr.h"
#include "bdd/mtr/mtr.h"

Go to the source code of this file.

Data Structures
struct	Bbr_ImageTree_t_
struct	Bbr_ImageNode_t_
struct	Bbr_ImagePart_t_
struct	Bbr_ImageVar_t_
struct	Bbr_ImageTree2_t_

Macros
#define	b0   Cudd_Not((dd)->one)
#define	b1   (dd)->one
#define	ABC_PRB(dd, f)   printf("%s = ", #f); Bbr_bddPrint(dd,f); printf("\n")

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Bbr_ImageNode_t_	Bbr_ImageNode_t
typedef struct Bbr_ImagePart_t_	Bbr_ImagePart_t
typedef struct Bbr_ImageVar_t_	Bbr_ImageVar_t

Functions
static Bbr_ImagePart_t **	Bbr_CreateParts (DdManager *dd, int nParts, DdNode **pbParts, DdNode *bCare)
static Bbr_ImageVar_t **	Bbr_CreateVars (DdManager *dd, int nParts, Bbr_ImagePart_t **pParts, int nVars, DdNode **pbVarsNs)
static Bbr_ImageNode_t **	Bbr_CreateNodes (DdManager *dd, int nParts, Bbr_ImagePart_t **pParts, int nVars, Bbr_ImageVar_t **pVars)
static void	Bbr_DeleteParts_rec (Bbr_ImageNode_t *pNode)
static int	Bbr_BuildTreeNode (DdManager *dd, int nNodes, Bbr_ImageNode_t **pNodes, int nVars, Bbr_ImageVar_t **pVars, int *pfStop, int nBddMax)
static Bbr_ImageNode_t *	Bbr_MergeTopNodes (DdManager *dd, int nNodes, Bbr_ImageNode_t **pNodes)
static void	Bbr_bddImageTreeDelete_rec (Bbr_ImageNode_t *pNode)
static int	Bbr_bddImageCompute_rec (Bbr_ImageTree_t *pTree, Bbr_ImageNode_t *pNode)
static int	Bbr_FindBestVariable (DdManager *dd, int nNodes, Bbr_ImageNode_t **pNodes, int nVars, Bbr_ImageVar_t **pVars)
static void	Bbr_FindBestPartitions (DdManager *dd, DdNode *bParts, int nNodes, Bbr_ImageNode_t **pNodes, int *piNode1, int *piNode2)
static Bbr_ImageNode_t *	Bbr_CombineTwoNodes (DdManager *dd, DdNode *bCube, Bbr_ImageNode_t *pNode1, Bbr_ImageNode_t *pNode2)
static void	Bbr_bddImagePrintLatchDependency (DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars)
static void	Bbr_bddImagePrintLatchDependencyOne (DdManager *dd, DdNode *bFunc, DdNode *bVarsCs, DdNode *bVarsNs, int iPart)
static void	Bbr_bddImagePrintTree (Bbr_ImageTree_t *pTree)
static void	Bbr_bddImagePrintTree_rec (Bbr_ImageNode_t *pNode, int nOffset)
static void	Bbr_bddPrint (DdManager *dd, DdNode *F)
Bbr_ImageTree_t *	Bbr_bddImageStart (DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int nBddMax, int fVerbose)
DdNode *	Bbr_bddImageCompute (Bbr_ImageTree_t *pTree, DdNode *bCare)
void	Bbr_bddImageTreeDelete (Bbr_ImageTree_t *pTree)
DdNode *	Bbr_bddImageRead (Bbr_ImageTree_t *pTree)
DdNode *	Bbr_bddComputeCube (DdManager *dd, DdNode **bXVars, int nVars)
Bbr_ImageTree2_t *	Bbr_bddImageStart2 (DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int fVerbose)
DdNode *	Bbr_bddImageCompute2 (Bbr_ImageTree2_t *pTree, DdNode *bCare)
void	Bbr_bddImageTreeDelete2 (Bbr_ImageTree2_t *pTree)
DdNode *	Bbr_bddImageRead2 (Bbr_ImageTree2_t *pTree)

Macro Definition Documentation

#define ABC_PRB	(		dd,
			f
	)		printf("%s = ", #f); Bbr_bddPrint(dd,f); printf("\n")

Definition at line 100 of file bbrImage.c.

#define b0   Cudd_Not((dd)->one)

Definition at line 96 of file bbrImage.c.

#define b1   (dd)->one

Definition at line 97 of file bbrImage.c.

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Bbr_ImageNode_t_ Bbr_ImageNode_t

CFile****************************************************************

FileName [bbrImage.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD-based reachability analysis.]

Synopsis [Performs image computation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

bbrImage.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 42 of file bbrImage.c.

typedef struct Bbr_ImagePart_t_ Bbr_ImagePart_t

Definition at line 43 of file bbrImage.c.

typedef struct Bbr_ImageVar_t_ Bbr_ImageVar_t

Definition at line 44 of file bbrImage.c.

Function Documentation

DdNode* Bbr_bddComputeCube	(	DdManager *	dd,
		DdNode **	bXVars,
		int	nVars
	)

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

Synopsis [Computes the positive polarty cube composed of the first vars in the array.]

Description []

SideEffects []

SeeAlso []

Definition at line 1191 of file bbrImage.c.

{
    DdNode * bRes;
    DdNode * bTemp;
    int i;

    bRes = b1; Cudd_Ref( bRes );
    for ( i = 0; i < nVars; i++ )
    {
        bRes = Cudd_bddAnd( dd, bTemp = bRes, bXVars[i] );  Cudd_Ref( bRes );
        Cudd_RecursiveDeref( dd, bTemp );
    }

    Cudd_Deref( bRes );
    return bRes;
}

DdNode* Bbr_bddImageCompute	(	Bbr_ImageTree_t *	pTree,
		DdNode *	bCare
	)

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

Synopsis [Compute the image.]

Description []

SideEffects []

SeeAlso []

Definition at line 253 of file bbrImage.c.

{
    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;
    if ( !Bbr_bddImageCompute_rec( pTree, pTree->pRoot ) )
        return NULL;
    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;
}

DdNode* Bbr_bddImageCompute2	(	Bbr_ImageTree2_t *	pTree,
		DdNode *	bCare
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1273 of file bbrImage.c.

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

int Bbr_bddImageCompute_rec ( Bbr_ImageTree_t *  pTree, Bbr_ImageNode_t *  pNode  )

static

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

Synopsis [Recompute the image.]

Description []

SideEffects []

SeeAlso []

Definition at line 660 of file bbrImage.c.

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

    // compute the children
    if ( pNode->pNode1 )
        if ( !Bbr_bddImageCompute_rec( pTree, pNode->pNode1 ) )
            return 0;
    if ( pNode->pNode2 )
        if ( !Bbr_bddImageCompute_rec( pTree, pNode->pNode2 ) )
            return 0;

    // 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;
    }
    if ( dd->keys-dd->dead > (unsigned)pTree->nBddMax )
        return 0;
    return 1;
}

void Bbr_bddImagePrintLatchDependency ( DdManager *  dd, DdNode *  bCare, int  nParts, DdNode **  pbParts, int  nVars, DdNode **  pbVars  )

static

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

Synopsis [Prints the latch dependency matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 1050 of file bbrImage.c.

{
    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++ )
        Bbr_bddImagePrintLatchDependencyOne( dd, pbParts[i], bVarsCs, bVarsNs, i );
    Bbr_bddImagePrintLatchDependencyOne( dd, bCare, bVarsCs, bVarsNs, nParts );

    Cudd_RecursiveDeref( dd, bVarsCs );
    Cudd_RecursiveDeref( dd, bVarsNs );
}

void Bbr_bddImagePrintLatchDependencyOne ( DdManager *  dd, DdNode *  bFunc, DdNode *  bVarsCs, DdNode *  bVarsNs, int  iPart  )

static

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

Synopsis [Prints one row of the latch dependency matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 1088 of file bbrImage.c.

{
    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 Bbr_bddImagePrintTree ( Bbr_ImageTree_t *  pTree )

static

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

Synopsis [Prints the tree for quenstification scheduling.]

Description []

SideEffects []

SeeAlso []

Definition at line 1127 of file bbrImage.c.

{
    printf( "The quantification scheduling tree:\n" );
    Bbr_bddImagePrintTree_rec( pTree->pRoot, 1 );
}

void Bbr_bddImagePrintTree_rec ( Bbr_ImageNode_t *  pNode, int  Offset  )

static

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

Synopsis [Prints the tree for quenstification scheduling.]

Description []

SideEffects []

SeeAlso []

Definition at line 1144 of file bbrImage.c.

{
    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( "    " );
    Bbr_bddImagePrintTree_rec( pNode->pNode1, Offset + 1 );

    for ( i = 0; i < Offset; i++ )
        printf( "    " );
    Bbr_bddImagePrintTree_rec( pNode->pNode2, Offset + 1 );
}

DdNode* Bbr_bddImageRead

(

Bbr_ImageTree_t *

pTree

)

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

Synopsis [Reads the image from the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 326 of file bbrImage.c.

{
    return pTree->pRoot->bImage;
}

DdNode* Bbr_bddImageRead2

(

Bbr_ImageTree2_t *

pTree

)

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

Synopsis [Returns the previously computed image.]

Description []

SideEffects []

SeeAlso []

Definition at line 1315 of file bbrImage.c.

{
    return pTree->bImage;
}

Bbr_ImageTree_t* Bbr_bddImageStart	(	DdManager *	dd,
		DdNode *	bCare,
		int	nParts,
		DdNode **	pbParts,
		int	nVars,
		DdNode **	pbVars,
		int	nBddMax,
		int	fVerbose
	)

AutomaticEnd Function*************************************************************

Synopsis [Starts the image computation using tree-based scheduling.]

Description [This procedure starts the image computation. It uses the given care set to test-run the image computation and creates the quantification tree by scheduling variable quantifications. The tree can be used to compute images for other care sets without rescheduling. In this case, Bbr_bddImageCompute() should be called.]

SideEffects []

SeeAlso []

Definition at line 168 of file bbrImage.c.

{
    Bbr_ImageTree_t * pTree;
    Bbr_ImagePart_t ** pParts;
    Bbr_ImageVar_t ** pVars;
    Bbr_ImageNode_t ** pNodes, * pCare;
    int fStop, v;

    if ( fVerbose && dd->size <= 80 )
        Bbr_bddImagePrintLatchDependency( dd, bCare, nParts, pbParts, nVars, pbVars );

    // create variables, partitions and leaf nodes
    pParts = Bbr_CreateParts( dd, nParts, pbParts, bCare );
    pVars  = Bbr_CreateVars( dd, nParts + 1, pParts, nVars, pbVars );
    pNodes = Bbr_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars );
    pCare  = pNodes[nParts];

    // process the nodes
    while ( Bbr_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars, &fStop, nBddMax ) );

    // consider the case of BDD node blowup
    if ( fStop )
    {
        for ( v = 0; v < dd->size; v++ )
            if ( pVars[v] )
                ABC_FREE( pVars[v] );
        ABC_FREE( pVars );
        for ( v = 0; v <= nParts; v++ )
            if ( pNodes[v] )
            {
                Bbr_DeleteParts_rec( pNodes[v] );
                Bbr_bddImageTreeDelete_rec( pNodes[v] );
            }
        ABC_FREE( pNodes );
        ABC_FREE( pParts );
        return NULL;
    }

    // make sure the variables are gone
    for ( v = 0; v < dd->size; v++ )
        assert( pVars[v] == NULL );
    ABC_FREE( pVars );
    
    // create the tree
    pTree = ABC_ALLOC( Bbr_ImageTree_t, 1 );
    memset( pTree, 0, sizeof(Bbr_ImageTree_t) );
    pTree->pCare = pCare;
    pTree->nBddMax = nBddMax;
    pTree->fVerbose = fVerbose;

    // merge the topmost nodes
    while ( (pTree->pRoot = Bbr_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 )
//        Bbr_bddImagePrintTree( pTree );

    // set the support of the care set
    pTree->bCareSupp = Cudd_Support( dd, bCare );  Cudd_Ref( pTree->bCareSupp );

    // clean the partitions
    Bbr_DeleteParts_rec( pTree->pRoot );
    ABC_FREE( pParts );

    return pTree;
}

Bbr_ImageTree2_t* Bbr_bddImageStart2	(	DdManager *	dd,
		DdNode *	bCare,
		int	nParts,
		DdNode **	pbParts,
		int	nVars,
		DdNode **	pbVars,
		int	fVerbose
	)

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

Synopsis [Starts the monolithic image computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1231 of file bbrImage.c.

{
    Bbr_ImageTree2_t * pTree;
    DdNode * bCubeAll, * bCubeNot, * bTemp;
    int i;

    pTree = ABC_ALLOC( Bbr_ImageTree2_t, 1 );
    pTree->dd = dd;
    pTree->bImage = NULL;

    bCubeAll = Bbr_bddComputeCube( dd, dd->vars, dd->size );      Cudd_Ref( bCubeAll );
    bCubeNot = Bbr_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 );
    }
    Bbr_bddImageCompute2( pTree, bCare );
    return pTree;
}

void Bbr_bddImageTreeDelete

(

Bbr_ImageTree_t *

pTree

)

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

Synopsis [Delete the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file bbrImage.c.

{
    if ( pTree->bCareSupp )
        Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp );
    Bbr_bddImageTreeDelete_rec( pTree->pRoot );
    ABC_FREE( pTree );
}

void Bbr_bddImageTreeDelete2

(

Bbr_ImageTree2_t *

pTree

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1293 of file bbrImage.c.

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

void Bbr_bddImageTreeDelete_rec ( Bbr_ImageNode_t *  pNode )

static

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

Synopsis [Delete the partitions from the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 635 of file bbrImage.c.

{
    if ( pNode->pNode1 )
        Bbr_bddImageTreeDelete_rec( pNode->pNode1 );
    if ( pNode->pNode2 )
        Bbr_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 Bbr_bddPrint ( DdManager *  dd, DdNode *  F  )

static

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

Synopsis [Outputs the BDD in a readable format.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 346 of file bbrImage.c.

{
    DdGen * Gen;
    int * Cube;
    CUDD_VALUE_TYPE Value;
    int nVars = dd->size;
    int fFirstCube = 1;
    int i;

    if ( F == NULL )
    {
        printf("NULL");
        return;
    }
    if ( F == b0 )
    {
        printf("Constant 0");
        return;
    }
    if ( F == b1 )
    {
        printf("Constant 1");
        return;
    }

    Cudd_ForeachCube( dd, F, Gen, Cube, Value )
    {
        if ( fFirstCube )
            fFirstCube = 0;
        else
//          Output << " + ";
            printf( " + " );

        for ( i = 0; i < nVars; i++ )
            if ( Cube[i] == 0 )
                printf( "[%d]'", i );
//              printf( "%c'", (char)('a'+i) );
            else if ( Cube[i] == 1 )
                printf( "[%d]", i );
//              printf( "%c", (char)('a'+i) );
    }

//  printf("\n");
}

int Bbr_BuildTreeNode ( DdManager *  dd, int  nNodes, Bbr_ImageNode_t **  pNodes, int  nVars, Bbr_ImageVar_t **  pVars, int *  pfStop, int  nBddMax  )

static

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

Synopsis [Builds the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 721 of file bbrImage.c.

{
    Bbr_ImageNode_t * pNode1, * pNode2;
    Bbr_ImageVar_t * pVar;
    Bbr_ImageNode_t * pNode;
    DdNode * bCube, * bTemp, * bSuppTemp;//, * bParts;
    int iNode1, iNode2;
    int iVarBest, nSupp, v;

    // find the best variable
    iVarBest = Bbr_FindBestVariable( dd, nNodes, pNodes, nVars, pVars );
    if ( iVarBest == -1 )
        return 0;
/*
for ( v = 0; v < nVars; v++ )
{
    DdNode * bSupp;
    if ( pVars[v] == NULL )
        continue;
    printf( "%3d :", v );
    printf( "%3d ", pVars[v]->nParts );
    bSupp = Cudd_Support( dd, pVars[v]->bParts );  Cudd_Ref( bSupp );
    Bbr_bddPrint( dd, bSupp ); printf( "\n" );
    Cudd_RecursiveDeref( dd, bSupp );
}
*/
    pVar = pVars[iVarBest];

    // this var cannot appear in one partition only
    nSupp = Cudd_SupportSize( dd, pVar->bParts );
    assert( nSupp == pVar->nParts );
    assert( nSupp != 1 );
//printf( "var = %d  supp = %d\n\n", iVarBest, nSupp );

    // 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 = Bbr_CombineTwoNodes( dd, bCube, pNode1, pNode2 );
        Cudd_RecursiveDeref( dd, bCube );
    }
    else // if ( pVar->nParts > 2 )
    {
        // find two smallest BDDs that have this var
        Bbr_FindBestPartitions( dd, pVar->bParts, nNodes, pNodes, &iNode1, &iNode2 );
        pNode1 = pNodes[iNode1];
        pNode2 = pNodes[iNode2];
//printf( "smallest bdds with this var: %d %d\n", iNode1, 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 = Bbr_CombineTwoNodes( dd, b1, pNode1, pNode2 );
    }

    // clean the old nodes
    pNodes[iNode1] = pNode;
    pNodes[iNode2] = NULL;
//printf( "Removing node %d (leaving node %d)\n", iNode2, iNode1 );
    
    // 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 = Cudd_SupportSize( dd, pVar->bParts );
    }

    *pfStop = 0;
    if ( dd->keys-dd->dead > (unsigned)nBddMax )
    {
        *pfStop = 1;
        return 0;
    }
    return 1;
}

Bbr_ImageNode_t * Bbr_CombineTwoNodes ( DdManager *  dd, DdNode *  bCube, Bbr_ImageNode_t *  pNode1, Bbr_ImageNode_t *  pNode2  )

static

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

Synopsis [Merges two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 899 of file bbrImage.c.

{
    Bbr_ImageNode_t * pNode;
    Bbr_ImagePart_t * pPart;

    // create a new partition
    pPart = ABC_ALLOC( Bbr_ImagePart_t, 1 );
    memset( pPart, 0, sizeof(Bbr_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  = Cudd_SupportSize( 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( Bbr_ImageNode_t, 1 );
    memset( pNode, 0, sizeof(Bbr_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;
}

Bbr_ImageNode_t ** Bbr_CreateNodes ( DdManager *  dd, int  nParts, Bbr_ImagePart_t **  pParts, int  nVars, Bbr_ImageVar_t **  pVars  )

static

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

Synopsis [Creates variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 507 of file bbrImage.c.

{
    Bbr_ImageNode_t ** pNodes;
    Bbr_ImageNode_t * pNode;
    DdNode * bTemp;
    int i, v, iPart;
/*
    DdManager *         dd;       // the manager 
    DdNode *            bCube;    // the cube to quantify
    DdNode *            bImage;   // the partial image
    Bbr_ImageNode_t * pNode1;   // the first branch
    Bbr_ImageNode_t * pNode2;   // the second branch
    Bbr_ImagePart_t * pPart;    // the partition (temporary)
*/
    // start the partitions
    pNodes = ABC_ALLOC( Bbr_ImageNode_t *, nParts );
    // create structures for each leaf nodes
    for ( i = 0; i < nParts; i++ )
    {
        pNodes[i] = ABC_ALLOC( Bbr_ImageNode_t, 1 );
        memset( pNodes[i], 0, sizeof(Bbr_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  = Cudd_SupportSize( 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;
}

Bbr_ImagePart_t ** Bbr_CreateParts ( DdManager *  dd, int  nParts, DdNode **  pbParts, DdNode *  bCare  )

static

AutomaticStart

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

Synopsis [Creates partitions.]

Description []

SideEffects []

SeeAlso []

Definition at line 406 of file bbrImage.c.

{
    Bbr_ImagePart_t ** pParts;
    int i;

    // start the partitions
    pParts = ABC_ALLOC( Bbr_ImagePart_t *, nParts + 1 );
    // create structures for each variable
    for ( i = 0; i < nParts; i++ )
    {
        pParts[i] = ABC_ALLOC( Bbr_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  = Cudd_SupportSize( 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( Bbr_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 = Cudd_SupportSize( dd, pParts[nParts]->bSupp );
    pParts[nParts]->nNodes = Cudd_DagSize( pParts[nParts]->bFunc );
    pParts[nParts]->iPart  = nParts;
    return pParts;
}

Bbr_ImageVar_t ** Bbr_CreateVars ( DdManager *  dd, int  nParts, Bbr_ImagePart_t **  pParts, int  nVars, DdNode **  pbVars  )

static

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

Synopsis [Creates variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 445 of file bbrImage.c.

{
    Bbr_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 = Cudd_SupportSize( dd, bSupp );

    // start the variables
    pVars = ABC_ALLOC( Bbr_ImageVar_t *, dd->size );
    memset( pVars, 0, sizeof(Bbr_ImageVar_t *) * dd->size );
    // create structures for each variable
    for ( bSuppTemp = bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
    {
        iVar = bSuppTemp->index;
        pVars[iVar] = ABC_ALLOC( Bbr_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;
}

void Bbr_DeleteParts_rec ( Bbr_ImageNode_t *  pNode )

static

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

Synopsis [Delete the partitions from the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 611 of file bbrImage.c.

{
    Bbr_ImagePart_t * pPart;
    if ( pNode->pNode1 )
        Bbr_DeleteParts_rec( pNode->pNode1 );
    if ( pNode->pNode2 )
        Bbr_DeleteParts_rec( pNode->pNode2 );
    pPart = pNode->pPart;
    Cudd_RecursiveDeref( pNode->dd, pPart->bFunc );
    Cudd_RecursiveDeref( pNode->dd, pPart->bSupp );
    ABC_FREE( pNode->pPart );
}

void Bbr_FindBestPartitions ( DdManager *  dd, DdNode *  bParts, int  nNodes, Bbr_ImageNode_t **  pNodes, int *  piNode1, int *  piNode2  )

static

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

Synopsis [Computes two smallest partions that have this var.]

Description []

SideEffects []

SeeAlso []

Definition at line 1010 of file bbrImage.c.

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

int Bbr_FindBestVariable ( DdManager *  dd, int  nNodes, Bbr_ImageNode_t **  pNodes, int  nVars, Bbr_ImageVar_t **  pVars  )

static

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

Synopsis [Computes the best variable.]

Description [The variables is the best if the sum of squares of the BDD sizes of the partitions, in which it participates, is the minimum.]

SideEffects []

SeeAlso []

Definition at line 953 of file bbrImage.c.

{
    DdNode * bTemp;
    int iVarBest, v;
    double CostBest, CostCur;

    CostBest = 100000000000000.0;
    iVarBest = -1;

    // check if there are two-variable partitions
    for ( v = 0; v < nVars; v++ )
        if ( pVars[v] && pVars[v]->nParts == 2 )
        {
            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;
            }
        }
    if ( iVarBest >= 0 )
        return iVarBest;

    // find other partition
    for ( v = 0; v < nVars; v++ )
        if ( pVars[v] )
        {
            assert( pVars[v]->nParts > 1 );
            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;
}

Bbr_ImageNode_t * Bbr_MergeTopNodes ( DdManager *  dd, int  nNodes, Bbr_ImageNode_t **  pNodes  )

static

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

Synopsis [Merges the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 850 of file bbrImage.c.

{
    Bbr_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 = Bbr_CombineTwoNodes( dd, b1, pNodes[n1], pNodes[n2] );

    // clean the old nodes
    pNodes[n1] = pNode;
    pNodes[n2] = NULL;
    return NULL;
}