extraBddImage.c File Reference

#include "extraBdd.h"

Include dependency graph for extraBddImage.c:

Go to the source code of this file.

Classes
struct	Extra_ImageTree_t_
struct	Extra_ImageNode_t_
struct	Extra_ImagePart_t_
struct	Extra_ImageVar_t_
struct	Extra_ImageTree2_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Extra_ImageNode_t_	Extra_ImageNode_t
typedef struct Extra_ImagePart_t_	Extra_ImagePart_t
typedef struct Extra_ImageVar_t_	Extra_ImageVar_t

Functions
Extra_ImageTree_t *	Extra_bddImageStart (DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int fVerbose)
DdNode *	Extra_bddImageCompute (Extra_ImageTree_t *pTree, DdNode *bCare)
void	Extra_bddImageTreeDelete (Extra_ImageTree_t *pTree)
DdNode *	Extra_bddImageRead (Extra_ImageTree_t *pTree)
Extra_ImageTree2_t *	Extra_bddImageStart2 (DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int fVerbose)
DdNode *	Extra_bddImageCompute2 (Extra_ImageTree2_t *pTree, DdNode *bCare)
void	Extra_bddImageTreeDelete2 (Extra_ImageTree2_t *pTree)
DdNode *	Extra_bddImageRead2 (Extra_ImageTree2_t *pTree)

Typedef Documentation

Extra_ImageNode_t

typedef typedefABC_NAMESPACE_IMPL_START struct Extra_ImageNode_t_ Extra_ImageNode_t

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

FileName [extraBddImage.c]

PackageName [extra]

Synopsis [Various reusable software utilities.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2003.]

Revision [

Id

extraBddImage.c,v 1.0 2003/09/01 00:00:00 alanmi Exp

]

Definition at line 39 of file extraBddImage.c.

Extra_ImagePart_t

typedef struct Extra_ImagePart_t_ Extra_ImagePart_t

Definition at line 40 of file extraBddImage.c.

Extra_ImageVar_t

typedef struct Extra_ImageVar_t_ Extra_ImageVar_t

Definition at line 41 of file extraBddImage.c.

Function Documentation

Extra_bddImageCompute()

DdNode * Extra_bddImageCompute	(	Extra_ImageTree_t *	pTree,
		DdNode *	bCare )

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

Synopsis [Compute the image.]

Description []

SideEffects []

SeeAlso []

Definition at line 220 of file extraBddImage.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;
    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;
}

Extra_bddImageCompute2()

DdNode * Extra_bddImageCompute2	(	Extra_ImageTree2_t *	pTree,
		DdNode *	bCare )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1108 of file extraBddImage.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;
}

Here is the caller graph for this function:

Extra_bddImageRead()

DdNode * Extra_bddImageRead

(

Extra_ImageTree_t *

pTree

)

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

Synopsis [Reads the image from the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 292 of file extraBddImage.c.

{
    return pTree->pRoot->bImage;
}

Extra_bddImageRead2()

DdNode * Extra_bddImageRead2

(

Extra_ImageTree2_t *

pTree

)

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

Synopsis [Returns the previously computed image.]

Description []

SideEffects []

SeeAlso []

Definition at line 1150 of file extraBddImage.c.

{
    return pTree->bImage;
}

Extra_bddImageStart()

Extra_ImageTree_t * Extra_bddImageStart	(	DdManager *	dd,
		DdNode *	bCare,
		int	nParts,
		DdNode **	pbParts,
		int	nVars,
		DdNode **	pbVars,
		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, Extra_bddImageCompute() should be called.]

SideEffects []

SeeAlso []

Definition at line 156 of file extraBddImage.c.

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

Here is the call graph for this function:

Extra_bddImageStart2()

Extra_ImageTree2_t * Extra_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 1066 of file extraBddImage.c.

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

Here is the call graph for this function:

Extra_bddImageTreeDelete()

void Extra_bddImageTreeDelete

(

Extra_ImageTree_t *

pTree

)

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

Synopsis [Delete the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 273 of file extraBddImage.c.

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

Extra_bddImageTreeDelete2()

void Extra_bddImageTreeDelete2

(

Extra_ImageTree2_t *

pTree

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1128 of file extraBddImage.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 );
}