abc/src/aig/gia/giaClp.c - third_party/vtr-verilog-to-routing - Git at Google

 /**CFile****************************************************************

   FileName    [giaClp.c]

   SystemName  [ABC: Logic synthesis and verification system.]

   PackageName [Scalable AIG package.]

   Synopsis    [Collapsing AIG.]

   Author      [Alan Mishchenko]

   Affiliation [UC Berkeley]

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

   Revision    [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

 ***********************************************************************/

 #include "gia.h"

 #ifdef ABC_USE_CUDD
 #include "bdd/extrab/extraBdd.h"
 #include "bdd/dsd/dsd.h"
 #endif

 ABC_NAMESPACE_IMPL_START

 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////

 #ifdef ABC_USE_CUDD

 extern int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase );
 extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
 extern int Abc_NtkDeriveFlatGiaSop( Gia_Man_t * pGia, int * gFanins, char * pSop );
 extern int Gia_ManFactorNode( Gia_Man_t * p, char * pSop, Vec_Int_t * vLeaves );

 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////

 /**Function*************************************************************

   Synopsis    []

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 Vec_Ptr_t * Gia_GetFakeNames( int nNames )
 {
     Vec_Ptr_t * vNames;
     char Buffer[5];
     int i;

     vNames = Vec_PtrAlloc( nNames );
     for ( i = 0; i < nNames; i++ )
     {
         if ( nNames < 26 )
         {
             Buffer[0] = 'a' + i;
             Buffer[1] = 0;
         }
         else
         {
             Buffer[0] = 'a' + i%26;
             Buffer[1] = '0' + i/26;
             Buffer[2] = 0;
         }
         Vec_PtrPush( vNames, Extra_UtilStrsav(Buffer) );
     }
     return vNames;
 }

 /**Function*************************************************************

   Synopsis    []

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 int Gia_ManRebuildIsop( DdManager * dd, DdNode * bLocal, Gia_Man_t * pNew, Vec_Int_t * vFanins, Vec_Str_t * vSop, Vec_Str_t * vCube )
 {
     char * pSop;
     DdNode * bCover, * zCover, * zCover0, * zCover1;
     int nFanins = Vec_IntSize(vFanins);
     int fPhase, nCubes, nCubes0, nCubes1;

     // get the ZDD of the negative polarity
     bCover = Cudd_zddIsop( dd, Cudd_Not(bLocal), Cudd_Not(bLocal), &zCover0 );
     Cudd_Ref( zCover0 );
     Cudd_Ref( bCover );
     Cudd_RecursiveDeref( dd, bCover );
     nCubes0 = Abc_CountZddCubes( dd, zCover0 );

     // get the ZDD of the positive polarity
     bCover = Cudd_zddIsop( dd, bLocal, bLocal, &zCover1 );
     Cudd_Ref( zCover1 );
     Cudd_Ref( bCover );
     Cudd_RecursiveDeref( dd, bCover );
     nCubes1 = Abc_CountZddCubes( dd, zCover1 );

     // compare the number of cubes
     if ( nCubes1 <= nCubes0 )
     { // use positive polarity
         nCubes = nCubes1;
         zCover = zCover1;
         Cudd_RecursiveDerefZdd( dd, zCover0 );
         fPhase = 1;
     }
     else
     { // use negative polarity
         nCubes = nCubes0;
         zCover = zCover0;
         Cudd_RecursiveDerefZdd( dd, zCover1 );
         fPhase = 0;
     }
     if ( nCubes > 1000 )
     {
         Cudd_RecursiveDerefZdd( dd, zCover );
         return -1;
     }

     // allocate memory for the cover
     Vec_StrGrow( vSop, (nFanins + 3) * nCubes + 1 );
     pSop = Vec_StrArray( vSop );
     pSop[(nFanins + 3) * nCubes] = 0;
     // create the SOP
     Vec_StrFill( vCube, nFanins, '-' );
     Vec_StrPush( vCube, '\0' );
     Abc_ConvertZddToSop( dd, zCover, pSop, nFanins, vCube, fPhase );
     Cudd_RecursiveDerefZdd( dd, zCover );

     // perform factoring
 //    return Abc_NtkDeriveFlatGiaSop( pNew, Vec_IntArray(vFanins), pSop );
     return Gia_ManFactorNode( pNew, pSop, vFanins );
 }
 int Gia_ManRebuildNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Gia_Man_t * pNew, DdManager * ddNew, Vec_Int_t * vFanins, Vec_Str_t * vSop, Vec_Str_t * vCube )
 {
     DdManager * ddDsd = Dsd_ManagerReadDd( pManDsd );
     DdNode * bLocal, * bTemp;
     Dsd_Node_t * pFaninDsd;
     Dsd_Type_t Type;
     int i, nDecs, iLit = -1;

     // add the fanins
     Type  = Dsd_NodeReadType( pNodeDsd );
     nDecs = Dsd_NodeReadDecsNum( pNodeDsd );
     assert( nDecs > 1 );
     Vec_IntClear( vFanins );
     for ( i = 0; i < nDecs; i++ )
     {
         pFaninDsd = Dsd_NodeReadDec( pNodeDsd, i );
         iLit      = Dsd_NodeReadMark( Dsd_Regular(pFaninDsd) );
         iLit      = Abc_LitNotCond( iLit, Dsd_IsComplement(pFaninDsd) );
         assert( Type == DSD_NODE_OR || !Dsd_IsComplement(pFaninDsd) );
         Vec_IntPush( vFanins, iLit );
     }

     // create the local function depending on the type of the node
     switch ( Type )
     {
         case DSD_NODE_CONST1:
         {
             iLit = 1;
             break;
         }
         case DSD_NODE_OR:
         {
             iLit = 0;
             for ( i = 0; i < nDecs; i++ )
                 iLit = Gia_ManHashOr( pNew, iLit, Vec_IntEntry(vFanins, i) );
             break;
         }
         case DSD_NODE_EXOR:
         {
             iLit = 0;
             for ( i = 0; i < nDecs; i++ )
                 iLit = Gia_ManHashXor( pNew, iLit, Vec_IntEntry(vFanins, i) );
             break;
         }
         case DSD_NODE_PRIME:
         {
             bLocal = Dsd_TreeGetPrimeFunction( ddDsd, pNodeDsd );                Cudd_Ref( bLocal );
             bLocal = Extra_TransferLevelByLevel( ddDsd, ddNew, bTemp = bLocal ); Cudd_Ref( bLocal );
             Cudd_RecursiveDeref( ddDsd, bTemp );
             // bLocal is now in the new BDD manager
             iLit = Gia_ManRebuildIsop( ddNew, bLocal, pNew, vFanins, vSop, vCube );
             Cudd_RecursiveDeref( ddNew, bLocal );
             break;
         }
         default:
         {
             assert( 0 );
             break;
         }
     }
     Dsd_NodeSetMark( pNodeDsd, iLit );
     return iLit;
 }
 Gia_Man_t * Gia_ManRebuild( Gia_Man_t * p, Dsd_Manager_t * pManDsd, DdManager * ddNew )
 {
     Gia_Man_t * pNew;
     Dsd_Node_t ** ppNodesDsd;
     Dsd_Node_t * pNodeDsd;
     int i, nNodesDsd, iLit = -1;
     Vec_Str_t * vSop, * vCube;
     Vec_Int_t * vFanins;

     vFanins = Vec_IntAlloc( 1000 );
     vSop    = Vec_StrAlloc( 10000 );
     vCube   = Vec_StrAlloc( 1000 );

     pNew = Gia_ManStart( 2*Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );

     // save the CI nodes in the DSD nodes
     Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), 1 );
     for ( i = 0; i < Gia_ManCiNum(p); i++ )
     {
         pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
         Dsd_NodeSetMark( pNodeDsd, Gia_ManAppendCi( pNew ) );
     }

     // collect DSD nodes in DFS order (leaves and const1 are not collected)
     ppNodesDsd = Dsd_TreeCollectNodesDfs( pManDsd, &nNodesDsd );
     for ( i = 0; i < nNodesDsd; i++ )
     {
         iLit = Gia_ManRebuildNode( pManDsd, ppNodesDsd[i], pNew, ddNew, vFanins, vSop, vCube );
         if ( iLit == -1 )
             break;
     }
     ABC_FREE( ppNodesDsd );
     Vec_IntFree( vFanins );
     Vec_StrFree( vSop );
     Vec_StrFree( vCube );
     if ( iLit == -1 )
     {
         Gia_ManStop( pNew );
         return Gia_ManDup(p);
     }

     // set the pointers to the CO drivers
     for ( i = 0; i < Gia_ManCoNum(p); i++ )
     {
         pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i );
         iLit = Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) );
         iLit = Abc_LitNotCond( iLit, Dsd_IsComplement(pNodeDsd) );
         Gia_ManAppendCo( pNew, iLit );
     }
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     return pNew;
 }

 /**Function*************************************************************

   Synopsis    []

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 void Gia_ManCollapseDeref( DdManager * dd, Vec_Ptr_t * vFuncs )
 {
     DdNode * bFunc; int i;
     Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
         if ( bFunc )
             Cudd_RecursiveDeref( dd, bFunc );
     Vec_PtrFree( vFuncs );
 }
 void Gia_ObjCollapseDeref( Gia_Man_t * p, DdManager * dd, Vec_Ptr_t * vFuncs, int Id )
 {
     if ( Gia_ObjRefDecId(p, Id) )
         return;
     Cudd_RecursiveDeref( dd, (DdNode *)Vec_PtrEntry(vFuncs, Id) );
     Vec_PtrWriteEntry( vFuncs, Id, NULL );
 }
 Vec_Ptr_t * Gia_ManCollapse( Gia_Man_t * p, DdManager * dd, int nBddLimit, int fVerbose )
 {
     Vec_Ptr_t * vFuncs;
     DdNode * bFunc0, * bFunc1, * bFunc;
     Gia_Obj_t * pObj;
     int i, Id;
     Gia_ManCreateRefs( p );
     // assign constant node
     vFuncs = Vec_PtrStart( Gia_ManObjNum(p) );
     if ( Gia_ObjRefNumId(p, 0) > 0 )
         Vec_PtrWriteEntry( vFuncs, 0, Cudd_ReadLogicZero(dd) ), Cudd_Ref(Cudd_ReadLogicZero(dd));
     // assign elementary variables
     Gia_ManForEachCiId( p, Id, i )
         if ( Gia_ObjRefNumId(p, Id) > 0 )
             Vec_PtrWriteEntry( vFuncs, Id, Cudd_bddIthVar(dd,i) ), Cudd_Ref(Cudd_bddIthVar(dd,i));
     // create BDD for AND nodes
     Gia_ManForEachAnd( p, pObj, i )
     {
         bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj) );
         bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj) );
         bFunc  = Cudd_bddAndLimit( dd, bFunc0, bFunc1, nBddLimit );
         if ( bFunc == NULL )
         {
             Gia_ManCollapseDeref( dd, vFuncs );
             return NULL;
         }
         Cudd_Ref( bFunc );
         Vec_PtrWriteEntry( vFuncs, i, bFunc );
         Gia_ObjCollapseDeref( p, dd, vFuncs, Gia_ObjFaninId0(pObj, i) );
         Gia_ObjCollapseDeref( p, dd, vFuncs, Gia_ObjFaninId1(pObj, i) );
     }
     // create BDD for outputs
     Gia_ManForEachCoId( p, Id, i )
     {
         pObj = Gia_ManCo( p, i );
         bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Gia_ObjFaninId0(pObj, Id)), Gia_ObjFaninC0(pObj) );
         Vec_PtrWriteEntry( vFuncs, Id, bFunc0 ); Cudd_Ref( bFunc0 );
         Gia_ObjCollapseDeref( p, dd, vFuncs, Gia_ObjFaninId0(pObj, Id) );
     }
     assert( Vec_PtrSize(vFuncs) == Vec_PtrCountZero(vFuncs) + Gia_ManCoNum(p) );
     // compact
     Gia_ManForEachCoId( p, Id, i )
         Vec_PtrWriteEntry( vFuncs, i, Vec_PtrEntry(vFuncs, Id) );
     Vec_PtrShrink( vFuncs, Gia_ManCoNum(p) );
     return vFuncs;
 }

 /**Function*************************************************************

   Synopsis    []

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
 {
     Gia_Man_t * pNew;
     DdManager * dd, * ddNew;
     Dsd_Manager_t * pManDsd;
     Vec_Ptr_t * vFuncs;
     // derive global BDDs
     dd = Cudd_Init( Gia_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
     vFuncs = Gia_ManCollapse( p, dd, 10000, 0 );
     Cudd_AutodynDisable( dd );
     if ( vFuncs == NULL )
     {
         Extra_StopManager( dd );
         return Gia_ManDup(p);
     }
     // start ISOP manager
     ddNew = Cudd_Init( Gia_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     Cudd_zddVarsFromBddVars( ddNew, 2 );
 //    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
     if ( fVerbose )
     printf( "Ins = %d. Outs = %d.  Shared BDD nodes = %d.  Peak live nodes = %d. Peak nodes = %d.\n",
         Gia_ManCiNum(p), Gia_ManCoNum(p),
         Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) ),
         Cudd_ReadPeakLiveNodeCount(dd), (int)Cudd_ReadNodeCount(dd) );
     // perform decomposition
     pManDsd = Dsd_ManagerStart( dd, Gia_ManCiNum(p), 0 );
     Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) );
     if ( fVerbose )
     {
         Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p) );
         Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) );
         char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
         char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
         Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1 );
         Vec_PtrFreeFree( vNamesCi );
         Vec_PtrFreeFree( vNamesCo );
     }

     pNew = Gia_ManRebuild( p, pManDsd, ddNew );
     Dsd_ManagerStop( pManDsd );
     // return manager
     Gia_ManCollapseDeref( dd, vFuncs );
     Extra_StopManager( dd );
     Extra_StopManager( ddNew );
     return pNew;
 }
 void Gia_ManCollapseTestTest( Gia_Man_t * p )
 {
     Gia_Man_t * pNew;
     pNew = Gia_ManCollapseTest( p, 0 );
     Gia_ManPrintStats( p, NULL );
     Gia_ManPrintStats( pNew, NULL );
     Gia_ManStop( pNew );
 }

 #else

 Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
 {
     return NULL;
 }

 #endif

 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////


 ABC_NAMESPACE_IMPL_END
	/CFile**************************************************************

	FileName [giaClp.c]

	SystemName [ABC: Logic synthesis and verification system.]

	PackageName [Scalable AIG package.]

	Synopsis [Collapsing AIG.]

	Author [Alan Mishchenko]

	Affiliation [UC Berkeley]

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

	Revision [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

	***********************************************************************/

	#include "gia.h"

	#ifdef ABC_USE_CUDD
	#include "bdd/extrab/extraBdd.h"
	#include "bdd/dsd/dsd.h"
	#endif

	ABC_NAMESPACE_IMPL_START

	////////////////////////////////////////////////////////////////////////
	/// DECLARATIONS ///
	////////////////////////////////////////////////////////////////////////

	#ifdef ABC_USE_CUDD

	extern int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase );
	extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
	extern int Abc_NtkDeriveFlatGiaSop( Gia_Man_t * pGia, int * gFanins, char * pSop );
	extern int Gia_ManFactorNode( Gia_Man_t * p, char * pSop, Vec_Int_t * vLeaves );

	////////////////////////////////////////////////////////////////////////
	/// FUNCTION DEFINITIONS ///
	////////////////////////////////////////////////////////////////////////

	/Function***********************************************************

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Vec_Ptr_t * Gia_GetFakeNames( int nNames )
	{
	Vec_Ptr_t * vNames;
	char Buffer[5];
	int i;

	vNames = Vec_PtrAlloc( nNames );
	for ( i = 0; i < nNames; i++ )
	{
	if ( nNames < 26 )
	{
	Buffer[0] = 'a' + i;
	Buffer[1] = 0;
	}
	else
	{
	Buffer[0] = 'a' + i%26;
	Buffer[1] = '0' + i/26;
	Buffer[2] = 0;
	}
	Vec_PtrPush( vNames, Extra_UtilStrsav(Buffer) );
	}
	return vNames;
	}

	/Function***********************************************************

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	int Gia_ManRebuildIsop( DdManager * dd, DdNode * bLocal, Gia_Man_t * pNew, Vec_Int_t * vFanins, Vec_Str_t * vSop, Vec_Str_t * vCube )
	{
	char * pSop;
	DdNode * bCover, * zCover, * zCover0, * zCover1;
	int nFanins = Vec_IntSize(vFanins);
	int fPhase, nCubes, nCubes0, nCubes1;

	// get the ZDD of the negative polarity
	bCover = Cudd_zddIsop( dd, Cudd_Not(bLocal), Cudd_Not(bLocal), &zCover0 );
	Cudd_Ref( zCover0 );
	Cudd_Ref( bCover );
	Cudd_RecursiveDeref( dd, bCover );
	nCubes0 = Abc_CountZddCubes( dd, zCover0 );

	// get the ZDD of the positive polarity
	bCover = Cudd_zddIsop( dd, bLocal, bLocal, &zCover1 );
	Cudd_Ref( zCover1 );
	Cudd_Ref( bCover );
	Cudd_RecursiveDeref( dd, bCover );
	nCubes1 = Abc_CountZddCubes( dd, zCover1 );

	// compare the number of cubes
	if ( nCubes1 <= nCubes0 )
	{ // use positive polarity
	nCubes = nCubes1;
	zCover = zCover1;
	Cudd_RecursiveDerefZdd( dd, zCover0 );
	fPhase = 1;
	}
	else
	{ // use negative polarity
	nCubes = nCubes0;
	zCover = zCover0;
	Cudd_RecursiveDerefZdd( dd, zCover1 );
	fPhase = 0;
	}
	if ( nCubes > 1000 )
	{
	Cudd_RecursiveDerefZdd( dd, zCover );
	return -1;
	}

	// allocate memory for the cover
	Vec_StrGrow( vSop, (nFanins + 3) * nCubes + 1 );
	pSop = Vec_StrArray( vSop );
	pSop[(nFanins + 3) * nCubes] = 0;
	// create the SOP
	Vec_StrFill( vCube, nFanins, '-' );
	Vec_StrPush( vCube, '\0' );
	Abc_ConvertZddToSop( dd, zCover, pSop, nFanins, vCube, fPhase );
	Cudd_RecursiveDerefZdd( dd, zCover );

	// perform factoring
	// return Abc_NtkDeriveFlatGiaSop( pNew, Vec_IntArray(vFanins), pSop );
	return Gia_ManFactorNode( pNew, pSop, vFanins );
	}
	int Gia_ManRebuildNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Gia_Man_t * pNew, DdManager * ddNew, Vec_Int_t * vFanins, Vec_Str_t * vSop, Vec_Str_t * vCube )
	{
	DdManager * ddDsd = Dsd_ManagerReadDd( pManDsd );
	DdNode * bLocal, * bTemp;
	Dsd_Node_t * pFaninDsd;
	Dsd_Type_t Type;
	int i, nDecs, iLit = -1;

	// add the fanins
	Type = Dsd_NodeReadType( pNodeDsd );
	nDecs = Dsd_NodeReadDecsNum( pNodeDsd );
	assert( nDecs > 1 );
	Vec_IntClear( vFanins );
	for ( i = 0; i < nDecs; i++ )
	{
	pFaninDsd = Dsd_NodeReadDec( pNodeDsd, i );
	iLit = Dsd_NodeReadMark( Dsd_Regular(pFaninDsd) );
	iLit = Abc_LitNotCond( iLit, Dsd_IsComplement(pFaninDsd) );
	assert( Type == DSD_NODE_OR \|\| !Dsd_IsComplement(pFaninDsd) );
	Vec_IntPush( vFanins, iLit );
	}

	// create the local function depending on the type of the node
	switch ( Type )
	{
	case DSD_NODE_CONST1:
	{
	iLit = 1;
	break;
	}
	case DSD_NODE_OR:
	{
	iLit = 0;
	for ( i = 0; i < nDecs; i++ )
	iLit = Gia_ManHashOr( pNew, iLit, Vec_IntEntry(vFanins, i) );
	break;
	}
	case DSD_NODE_EXOR:
	{
	iLit = 0;
	for ( i = 0; i < nDecs; i++ )
	iLit = Gia_ManHashXor( pNew, iLit, Vec_IntEntry(vFanins, i) );
	break;
	}
	case DSD_NODE_PRIME:
	{
	bLocal = Dsd_TreeGetPrimeFunction( ddDsd, pNodeDsd ); Cudd_Ref( bLocal );
	bLocal = Extra_TransferLevelByLevel( ddDsd, ddNew, bTemp = bLocal ); Cudd_Ref( bLocal );
	Cudd_RecursiveDeref( ddDsd, bTemp );
	// bLocal is now in the new BDD manager
	iLit = Gia_ManRebuildIsop( ddNew, bLocal, pNew, vFanins, vSop, vCube );
	Cudd_RecursiveDeref( ddNew, bLocal );
	break;
	}
	default:
	{
	assert( 0 );
	break;
	}
	}
	Dsd_NodeSetMark( pNodeDsd, iLit );
	return iLit;
	}
	Gia_Man_t * Gia_ManRebuild( Gia_Man_t * p, Dsd_Manager_t * pManDsd, DdManager * ddNew )
	{
	Gia_Man_t * pNew;
	Dsd_Node_t ** ppNodesDsd;
	Dsd_Node_t * pNodeDsd;
	int i, nNodesDsd, iLit = -1;
	Vec_Str_t * vSop, * vCube;
	Vec_Int_t * vFanins;

	vFanins = Vec_IntAlloc( 1000 );
	vSop = Vec_StrAlloc( 10000 );
	vCube = Vec_StrAlloc( 1000 );

	pNew = Gia_ManStart( 2*Gia_ManObjNum(p) );
	pNew->pName = Abc_UtilStrsav( p->pName );
	pNew->pSpec = Abc_UtilStrsav( p->pSpec );
	Gia_ManHashAlloc( pNew );

	// save the CI nodes in the DSD nodes
	Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), 1 );
	for ( i = 0; i < Gia_ManCiNum(p); i++ )
	{
	pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
	Dsd_NodeSetMark( pNodeDsd, Gia_ManAppendCi( pNew ) );
	}

	// collect DSD nodes in DFS order (leaves and const1 are not collected)
	ppNodesDsd = Dsd_TreeCollectNodesDfs( pManDsd, &nNodesDsd );
	for ( i = 0; i < nNodesDsd; i++ )
	{
	iLit = Gia_ManRebuildNode( pManDsd, ppNodesDsd[i], pNew, ddNew, vFanins, vSop, vCube );
	if ( iLit == -1 )
	break;
	}
	ABC_FREE( ppNodesDsd );
	Vec_IntFree( vFanins );
	Vec_StrFree( vSop );
	Vec_StrFree( vCube );
	if ( iLit == -1 )
	{
	Gia_ManStop( pNew );
	return Gia_ManDup(p);
	}

	// set the pointers to the CO drivers
	for ( i = 0; i < Gia_ManCoNum(p); i++ )
	{
	pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i );
	iLit = Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) );
	iLit = Abc_LitNotCond( iLit, Dsd_IsComplement(pNodeDsd) );
	Gia_ManAppendCo( pNew, iLit );
	}
	Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
	return pNew;
	}

	/Function***********************************************************

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Gia_ManCollapseDeref( DdManager * dd, Vec_Ptr_t * vFuncs )
	{
	DdNode * bFunc; int i;
	Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
	if ( bFunc )
	Cudd_RecursiveDeref( dd, bFunc );
	Vec_PtrFree( vFuncs );
	}
	void Gia_ObjCollapseDeref( Gia_Man_t * p, DdManager * dd, Vec_Ptr_t * vFuncs, int Id )
	{
	if ( Gia_ObjRefDecId(p, Id) )
	return;
	Cudd_RecursiveDeref( dd, (DdNode *)Vec_PtrEntry(vFuncs, Id) );
	Vec_PtrWriteEntry( vFuncs, Id, NULL );
	}
	Vec_Ptr_t * Gia_ManCollapse( Gia_Man_t * p, DdManager * dd, int nBddLimit, int fVerbose )
	{
	Vec_Ptr_t * vFuncs;
	DdNode * bFunc0, * bFunc1, * bFunc;
	Gia_Obj_t * pObj;
	int i, Id;
	Gia_ManCreateRefs( p );
	// assign constant node
	vFuncs = Vec_PtrStart( Gia_ManObjNum(p) );
	if ( Gia_ObjRefNumId(p, 0) > 0 )
	Vec_PtrWriteEntry( vFuncs, 0, Cudd_ReadLogicZero(dd) ), Cudd_Ref(Cudd_ReadLogicZero(dd));
	// assign elementary variables
	Gia_ManForEachCiId( p, Id, i )
	if ( Gia_ObjRefNumId(p, Id) > 0 )
	Vec_PtrWriteEntry( vFuncs, Id, Cudd_bddIthVar(dd,i) ), Cudd_Ref(Cudd_bddIthVar(dd,i));
	// create BDD for AND nodes
	Gia_ManForEachAnd( p, pObj, i )
	{
	bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj) );
	bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj) );
	bFunc = Cudd_bddAndLimit( dd, bFunc0, bFunc1, nBddLimit );
	if ( bFunc == NULL )
	{
	Gia_ManCollapseDeref( dd, vFuncs );
	return NULL;
	}
	Cudd_Ref( bFunc );
	Vec_PtrWriteEntry( vFuncs, i, bFunc );
	Gia_ObjCollapseDeref( p, dd, vFuncs, Gia_ObjFaninId0(pObj, i) );
	Gia_ObjCollapseDeref( p, dd, vFuncs, Gia_ObjFaninId1(pObj, i) );
	}
	// create BDD for outputs
	Gia_ManForEachCoId( p, Id, i )
	{
	pObj = Gia_ManCo( p, i );
	bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Gia_ObjFaninId0(pObj, Id)), Gia_ObjFaninC0(pObj) );
	Vec_PtrWriteEntry( vFuncs, Id, bFunc0 ); Cudd_Ref( bFunc0 );
	Gia_ObjCollapseDeref( p, dd, vFuncs, Gia_ObjFaninId0(pObj, Id) );
	}
	assert( Vec_PtrSize(vFuncs) == Vec_PtrCountZero(vFuncs) + Gia_ManCoNum(p) );
	// compact
	Gia_ManForEachCoId( p, Id, i )
	Vec_PtrWriteEntry( vFuncs, i, Vec_PtrEntry(vFuncs, Id) );
	Vec_PtrShrink( vFuncs, Gia_ManCoNum(p) );
	return vFuncs;
	}

	/Function***********************************************************

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
	{
	Gia_Man_t * pNew;
	DdManager * dd, * ddNew;
	Dsd_Manager_t * pManDsd;
	Vec_Ptr_t * vFuncs;
	// derive global BDDs
	dd = Cudd_Init( Gia_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
	Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
	vFuncs = Gia_ManCollapse( p, dd, 10000, 0 );
	Cudd_AutodynDisable( dd );
	if ( vFuncs == NULL )
	{
	Extra_StopManager( dd );
	return Gia_ManDup(p);
	}
	// start ISOP manager
	ddNew = Cudd_Init( Gia_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
	Cudd_zddVarsFromBddVars( ddNew, 2 );
	// Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
	if ( fVerbose )
	printf( "Ins = %d. Outs = %d. Shared BDD nodes = %d. Peak live nodes = %d. Peak nodes = %d.\n",
	Gia_ManCiNum(p), Gia_ManCoNum(p),
	Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) ),
	Cudd_ReadPeakLiveNodeCount(dd), (int)Cudd_ReadNodeCount(dd) );
	// perform decomposition
	pManDsd = Dsd_ManagerStart( dd, Gia_ManCiNum(p), 0 );
	Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) );
	if ( fVerbose )
	{
	Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p) );
	Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) );
	char ppNamesCi = (char )Vec_PtrArray( vNamesCi );
	char ppNamesCo = (char )Vec_PtrArray( vNamesCo );
	Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1 );
	Vec_PtrFreeFree( vNamesCi );
	Vec_PtrFreeFree( vNamesCo );
	}

	pNew = Gia_ManRebuild( p, pManDsd, ddNew );
	Dsd_ManagerStop( pManDsd );
	// return manager
	Gia_ManCollapseDeref( dd, vFuncs );
	Extra_StopManager( dd );
	Extra_StopManager( ddNew );
	return pNew;
	}
	void Gia_ManCollapseTestTest( Gia_Man_t * p )
	{
	Gia_Man_t * pNew;
	pNew = Gia_ManCollapseTest( p, 0 );
	Gia_ManPrintStats( p, NULL );
	Gia_ManPrintStats( pNew, NULL );
	Gia_ManStop( pNew );
	}

	#else

	Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
	{
	return NULL;
	}

	#endif

	////////////////////////////////////////////////////////////////////////
	/// END OF FILE ///
	////////////////////////////////////////////////////////////////////////


	ABC_NAMESPACE_IMPL_END