abc/src/opt/sfm/sfmNtk.c - third_party/vtr-verilog-to-routing - Git at Google

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

   FileName    [sfmNtk.c]

   SystemName  [ABC: Logic synthesis and verification system.]

   PackageName [SAT-based optimization using internal don't-cares.]

   Synopsis    [Logic network.]

   Author      [Alan Mishchenko]

   Affiliation [UC Berkeley]

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

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

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

 #include "sfmInt.h"

 ABC_NAMESPACE_IMPL_START


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

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

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

   Synopsis    []

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed )
 {
     Vec_Int_t * vArray;
     int i, k, Fanin;
     // check entries
     Vec_WecForEachLevel( vFanins, vArray, i )
     {
         // PIs have no fanins
         if ( i < nPis )
             assert( Vec_IntSize(vArray) == 0 && Vec_StrEntry(vFixed, i) == (char)0 );
         // nodes are in a topo order; POs cannot be fanins
         Vec_IntForEachEntry( vArray, Fanin, k )
 //            assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) );
             assert( Fanin + nPos < Vec_WecSize(vFanins) );
         // POs have one fanout
         if ( i + nPos >= Vec_WecSize(vFanins) )
             assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 );
     }
 }

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

   Synopsis    []

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 void Sfm_CreateFanout( Vec_Wec_t * vFanins, Vec_Wec_t * vFanouts )
 {
     Vec_Int_t * vArray;
     int i, k, Fanin;
     // count fanouts
     Vec_WecInit( vFanouts, Vec_WecSize(vFanins) );
     Vec_WecForEachLevel( vFanins, vArray, i )
         Vec_IntForEachEntry( vArray, Fanin, k )
             Vec_WecEntry( vFanouts, Fanin )->nSize++;
     // allocate fanins
     Vec_WecForEachLevel( vFanouts, vArray, i )
     {
         k = vArray->nSize; vArray->nSize = 0;
         Vec_IntGrow( vArray, k );
     }
     // add fanouts
     Vec_WecForEachLevel( vFanins, vArray, i )
         Vec_IntForEachEntry( vArray, Fanin, k )
             Vec_IntPush( Vec_WecEntry( vFanouts, Fanin ), i );
     // verify
     Vec_WecForEachLevel( vFanouts, vArray, i )
         assert( Vec_IntSize(vArray) == Vec_IntCap(vArray) );
 }

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

   Synopsis    []

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 static inline int Sfm_ObjLevelNew( Vec_Int_t * vArray, Vec_Int_t * vLevels, int fAddLevel )
 {
     int k, Fanin, Level = 0;
     Vec_IntForEachEntry( vArray, Fanin, k )
         Level = Abc_MaxInt( Level, Vec_IntEntry(vLevels, Fanin) );
     return Level + fAddLevel;
 }
 void Sfm_CreateLevel( Vec_Wec_t * vFanins, Vec_Int_t * vLevels, Vec_Str_t * vEmpty )
 {
     Vec_Int_t * vArray;
     int i;
     assert( Vec_IntSize(vLevels) == 0 );
     Vec_IntFill( vLevels, Vec_WecSize(vFanins), 0 );
     Vec_WecForEachLevel( vFanins, vArray, i )
         Vec_IntWriteEntry( vLevels, i, Sfm_ObjLevelNew(vArray, vLevels, Sfm_ObjAddsLevelArray(vEmpty, i)) );
 }

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

   Synopsis    []

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 static inline int Sfm_ObjLevelNewR( Vec_Int_t * vArray, Vec_Int_t * vLevelsR, int fAddLevel )
 {
     int k, Fanout, LevelR = 0;
     Vec_IntForEachEntry( vArray, Fanout, k )
         LevelR = Abc_MaxInt( LevelR, Vec_IntEntry(vLevelsR, Fanout) );
     return LevelR + fAddLevel;
 }
 void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR, Vec_Str_t * vEmpty )
 {
     Vec_Int_t * vArray;
     int i;
     assert( Vec_IntSize(vLevelsR) == 0 );
     Vec_IntFill( vLevelsR, Vec_WecSize(vFanouts), 0 );
     Vec_WecForEachLevelReverse( vFanouts, vArray, i )
         Vec_IntWriteEntry( vLevelsR, i, Sfm_ObjLevelNewR(vArray, vLevelsR, Sfm_ObjAddsLevelArray(vEmpty, i)) );
 }

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

   Synopsis    []

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths )
 {
     Sfm_Ntk_t * p;
     Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed );
     p = ABC_CALLOC( Sfm_Ntk_t, 1 );
     p->nObjs    = Vec_WecSize( vFanins );
     p->nPis     = nPis;
     p->nPos     = nPos;
     p->nNodes   = p->nObjs - p->nPis - p->nPos;
     // user data
     p->vFixed   = vFixed;
     p->vEmpty   = vEmpty;
     p->vTruths  = vTruths;
     p->vFanins  = *vFanins;
     ABC_FREE( vFanins );
     // attributes
     Sfm_CreateFanout( &p->vFanins, &p->vFanouts );
     Sfm_CreateLevel( &p->vFanins, &p->vLevels, vEmpty );
     Sfm_CreateLevelR( &p->vFanouts, &p->vLevelsR, vEmpty );
     Vec_IntFill( &p->vCounts,   p->nObjs,  0 );
     Vec_IntFill( &p->vTravIds,  p->nObjs,  0 );
     Vec_IntFill( &p->vTravIds2, p->nObjs,  0 );
     Vec_IntFill( &p->vId2Var,   2*p->nObjs, -1 );
     Vec_IntFill( &p->vVar2Id,   2*p->nObjs, -1 );
     p->vCover   = Vec_IntAlloc( 1 << 16 );
     p->vCnfs    = Sfm_CreateCnf( p );
     return p;
 }
 void Sfm_NtkPrepare( Sfm_Ntk_t * p )
 {
     p->nLevelMax = Vec_IntFindMax(&p->vLevels) + p->pPars->nGrowthLevel;
     p->vNodes    = Vec_IntAlloc( 1000 );
     p->vDivs     = Vec_IntAlloc( 100 );
     p->vRoots    = Vec_IntAlloc( 1000 );
     p->vTfo      = Vec_IntAlloc( 1000 );
     p->vDivCexes = Vec_WrdStart( p->pPars->nWinSizeMax );
     p->vOrder    = Vec_IntAlloc( 100 );
     p->vDivVars  = Vec_IntAlloc( 100 );
     p->vDivIds   = Vec_IntAlloc( 1000 );
     p->vLits     = Vec_IntAlloc( 100 );
     p->vValues   = Vec_IntAlloc( 100 );
     p->vClauses  = Vec_WecAlloc( 100 );
     p->vFaninMap = Vec_IntAlloc( 10 );
     p->pSat      = sat_solver_new();
     sat_solver_setnvars( p->pSat, p->pPars->nWinSizeMax );
 }
 void Sfm_NtkFree( Sfm_Ntk_t * p )
 {
     // user data
     Vec_StrFree( p->vFixed );
     Vec_StrFreeP( &p->vEmpty );
     Vec_WrdFree( p->vTruths );
     Vec_WecErase( &p->vFanins );
     // attributes
     Vec_WecErase( &p->vFanouts );
     ABC_FREE( p->vLevels.pArray );
     ABC_FREE( p->vLevelsR.pArray );
     ABC_FREE( p->vCounts.pArray );
     ABC_FREE( p->vTravIds.pArray );
     ABC_FREE( p->vTravIds2.pArray );
     ABC_FREE( p->vId2Var.pArray );
     ABC_FREE( p->vVar2Id.pArray );
     Vec_WecFree( p->vCnfs );
     Vec_IntFree( p->vCover );
     // other data
     Vec_IntFreeP( &p->vNodes );
     Vec_IntFreeP( &p->vDivs  );
     Vec_IntFreeP( &p->vRoots );
     Vec_IntFreeP( &p->vTfo   );
     Vec_WrdFreeP( &p->vDivCexes );
     Vec_IntFreeP( &p->vOrder );
     Vec_IntFreeP( &p->vDivVars );
     Vec_IntFreeP( &p->vDivIds );
     Vec_IntFreeP( &p->vLits  );
     Vec_IntFreeP( &p->vValues );
     Vec_WecFreeP( &p->vClauses );
     Vec_IntFreeP( &p->vFaninMap );
     if ( p->pSat  ) sat_solver_delete( p->pSat );
     ABC_FREE( p );
 }

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

   Synopsis    [Performs resubstitution for the node.]

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 void Sfm_NtkRemoveFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
 {
     int RetValue;
     assert( Sfm_ObjIsNode(p, iNode) );
     assert( !Sfm_ObjIsPo(p, iFanin) );
     RetValue = Vec_IntRemove( Sfm_ObjFiArray(p, iNode), iFanin );
     assert( RetValue );
     RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );
     assert( RetValue );
 }
 void Sfm_NtkAddFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
 {
     if ( iFanin < 0 )
         return;
     assert( Sfm_ObjIsNode(p, iNode) );
     assert( !Sfm_ObjIsPo(p, iFanin) );
     assert( Vec_IntFind( Sfm_ObjFiArray(p, iNode), iFanin ) == -1 );
     assert( Vec_IntFind( Sfm_ObjFoArray(p, iFanin), iNode ) == -1 );
     Vec_IntPush( Sfm_ObjFiArray(p, iNode), iFanin );
     Vec_IntPush( Sfm_ObjFoArray(p, iFanin), iNode );
 }
 void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
 {
     int i, iFanin;
     if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) || Sfm_ObjIsFixed(p, iNode) )
         return;
     assert( Sfm_ObjIsNode(p, iNode) );
     Sfm_ObjForEachFanin( p, iNode, iFanin, i )
     {
         int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );  assert( RetValue );
         Sfm_NtkDeleteObj_rec( p, iFanin );
     }
     Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
     Vec_WrdWriteEntry( p->vTruths, iNode, (word)0 );
 }
 void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode )
 {
     int i, iFanout;
     int LevelNew = Sfm_ObjLevelNew( Sfm_ObjFiArray(p, iNode), &p->vLevels, Sfm_ObjAddsLevel(p, iNode) );
     if ( LevelNew == Sfm_ObjLevel(p, iNode) )
         return;
     Sfm_ObjSetLevel( p, iNode, LevelNew );
     Sfm_ObjForEachFanout( p, iNode, iFanout, i )
         Sfm_NtkUpdateLevel_rec( p, iFanout );
 }
 void Sfm_NtkUpdateLevelR_rec( Sfm_Ntk_t * p, int iNode )
 {
     int i, iFanin;
     int LevelNew = Sfm_ObjLevelNewR( Sfm_ObjFoArray(p, iNode), &p->vLevelsR, Sfm_ObjAddsLevel(p, iNode) );
     if ( LevelNew == Sfm_ObjLevelR(p, iNode) )
         return;
     Sfm_ObjSetLevelR( p, iNode, LevelNew );
     Sfm_ObjForEachFanin( p, iNode, iFanin, i )
         Sfm_NtkUpdateLevelR_rec( p, iFanin );
 }
 void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth )
 {
     int iFanin = Sfm_ObjFanin( p, iNode, f );
     assert( Sfm_ObjIsNode(p, iNode) );
     assert( iFanin != iFaninNew );
     if ( uTruth == 0 || ~uTruth == 0 )
     {
         Sfm_ObjForEachFanin( p, iNode, iFanin, f )
         {
             int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );  assert( RetValue );
             Sfm_NtkDeleteObj_rec( p, iFanin );
         }
         Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
     }
     else
     {
         // replace old fanin by new fanin
         Sfm_NtkRemoveFanin( p, iNode, iFanin );
         Sfm_NtkAddFanin( p, iNode, iFaninNew );
         // recursively remove MFFC
         Sfm_NtkDeleteObj_rec( p, iFanin );
     }
     // update logic level
     Sfm_NtkUpdateLevel_rec( p, iNode );
     if ( iFaninNew != -1 )
         Sfm_NtkUpdateLevelR_rec( p, iFaninNew );
     if ( Sfm_ObjFanoutNum(p, iFanin) > 0 )
         Sfm_NtkUpdateLevelR_rec( p, iFanin );
     // update truth table
     Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
     Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
 }

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

   Synopsis    [Public APIs of this network.]

   Description []

   SideEffects []

   SeeAlso     []

 ***********************************************************************/
 Vec_Int_t *  Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i )
 {
     return Vec_WecEntry( &p->vFanins, i );
 }
 word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i )
 {
     return Vec_WrdEntryP( p->vTruths, i );
 }
 int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i )
 {
     return (int)Vec_StrEntry( p->vFixed, i );
 }
 int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i )
 {
     return (Sfm_ObjFaninNum(p, i) > 0) || (Sfm_ObjFanoutNum(p, i) > 0);
 }

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


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

	FileName [sfmNtk.c]

	SystemName [ABC: Logic synthesis and verification system.]

	PackageName [SAT-based optimization using internal don't-cares.]

	Synopsis [Logic network.]

	Author [Alan Mishchenko]

	Affiliation [UC Berkeley]

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

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

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

	#include "sfmInt.h"

	ABC_NAMESPACE_IMPL_START


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

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

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

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed )
	{
	Vec_Int_t * vArray;
	int i, k, Fanin;
	// check entries
	Vec_WecForEachLevel( vFanins, vArray, i )
	{
	// PIs have no fanins
	if ( i < nPis )
	assert( Vec_IntSize(vArray) == 0 && Vec_StrEntry(vFixed, i) == (char)0 );
	// nodes are in a topo order; POs cannot be fanins
	Vec_IntForEachEntry( vArray, Fanin, k )
	// assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) );
	assert( Fanin + nPos < Vec_WecSize(vFanins) );
	// POs have one fanout
	if ( i + nPos >= Vec_WecSize(vFanins) )
	assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 );
	}
	}

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

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Sfm_CreateFanout( Vec_Wec_t * vFanins, Vec_Wec_t * vFanouts )
	{
	Vec_Int_t * vArray;
	int i, k, Fanin;
	// count fanouts
	Vec_WecInit( vFanouts, Vec_WecSize(vFanins) );
	Vec_WecForEachLevel( vFanins, vArray, i )
	Vec_IntForEachEntry( vArray, Fanin, k )
	Vec_WecEntry( vFanouts, Fanin )->nSize++;
	// allocate fanins
	Vec_WecForEachLevel( vFanouts, vArray, i )
	{
	k = vArray->nSize; vArray->nSize = 0;
	Vec_IntGrow( vArray, k );
	}
	// add fanouts
	Vec_WecForEachLevel( vFanins, vArray, i )
	Vec_IntForEachEntry( vArray, Fanin, k )
	Vec_IntPush( Vec_WecEntry( vFanouts, Fanin ), i );
	// verify
	Vec_WecForEachLevel( vFanouts, vArray, i )
	assert( Vec_IntSize(vArray) == Vec_IntCap(vArray) );
	}

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

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	static inline int Sfm_ObjLevelNew( Vec_Int_t * vArray, Vec_Int_t * vLevels, int fAddLevel )
	{
	int k, Fanin, Level = 0;
	Vec_IntForEachEntry( vArray, Fanin, k )
	Level = Abc_MaxInt( Level, Vec_IntEntry(vLevels, Fanin) );
	return Level + fAddLevel;
	}
	void Sfm_CreateLevel( Vec_Wec_t * vFanins, Vec_Int_t * vLevels, Vec_Str_t * vEmpty )
	{
	Vec_Int_t * vArray;
	int i;
	assert( Vec_IntSize(vLevels) == 0 );
	Vec_IntFill( vLevels, Vec_WecSize(vFanins), 0 );
	Vec_WecForEachLevel( vFanins, vArray, i )
	Vec_IntWriteEntry( vLevels, i, Sfm_ObjLevelNew(vArray, vLevels, Sfm_ObjAddsLevelArray(vEmpty, i)) );
	}

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

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	static inline int Sfm_ObjLevelNewR( Vec_Int_t * vArray, Vec_Int_t * vLevelsR, int fAddLevel )
	{
	int k, Fanout, LevelR = 0;
	Vec_IntForEachEntry( vArray, Fanout, k )
	LevelR = Abc_MaxInt( LevelR, Vec_IntEntry(vLevelsR, Fanout) );
	return LevelR + fAddLevel;
	}
	void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR, Vec_Str_t * vEmpty )
	{
	Vec_Int_t * vArray;
	int i;
	assert( Vec_IntSize(vLevelsR) == 0 );
	Vec_IntFill( vLevelsR, Vec_WecSize(vFanouts), 0 );
	Vec_WecForEachLevelReverse( vFanouts, vArray, i )
	Vec_IntWriteEntry( vLevelsR, i, Sfm_ObjLevelNewR(vArray, vLevelsR, Sfm_ObjAddsLevelArray(vEmpty, i)) );
	}

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

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths )
	{
	Sfm_Ntk_t * p;
	Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed );
	p = ABC_CALLOC( Sfm_Ntk_t, 1 );
	p->nObjs = Vec_WecSize( vFanins );
	p->nPis = nPis;
	p->nPos = nPos;
	p->nNodes = p->nObjs - p->nPis - p->nPos;
	// user data
	p->vFixed = vFixed;
	p->vEmpty = vEmpty;
	p->vTruths = vTruths;
	p->vFanins = *vFanins;
	ABC_FREE( vFanins );
	// attributes
	Sfm_CreateFanout( &p->vFanins, &p->vFanouts );
	Sfm_CreateLevel( &p->vFanins, &p->vLevels, vEmpty );
	Sfm_CreateLevelR( &p->vFanouts, &p->vLevelsR, vEmpty );
	Vec_IntFill( &p->vCounts, p->nObjs, 0 );
	Vec_IntFill( &p->vTravIds, p->nObjs, 0 );
	Vec_IntFill( &p->vTravIds2, p->nObjs, 0 );
	Vec_IntFill( &p->vId2Var, 2*p->nObjs, -1 );
	Vec_IntFill( &p->vVar2Id, 2*p->nObjs, -1 );
	p->vCover = Vec_IntAlloc( 1 << 16 );
	p->vCnfs = Sfm_CreateCnf( p );
	return p;
	}
	void Sfm_NtkPrepare( Sfm_Ntk_t * p )
	{
	p->nLevelMax = Vec_IntFindMax(&p->vLevels) + p->pPars->nGrowthLevel;
	p->vNodes = Vec_IntAlloc( 1000 );
	p->vDivs = Vec_IntAlloc( 100 );
	p->vRoots = Vec_IntAlloc( 1000 );
	p->vTfo = Vec_IntAlloc( 1000 );
	p->vDivCexes = Vec_WrdStart( p->pPars->nWinSizeMax );
	p->vOrder = Vec_IntAlloc( 100 );
	p->vDivVars = Vec_IntAlloc( 100 );
	p->vDivIds = Vec_IntAlloc( 1000 );
	p->vLits = Vec_IntAlloc( 100 );
	p->vValues = Vec_IntAlloc( 100 );
	p->vClauses = Vec_WecAlloc( 100 );
	p->vFaninMap = Vec_IntAlloc( 10 );
	p->pSat = sat_solver_new();
	sat_solver_setnvars( p->pSat, p->pPars->nWinSizeMax );
	}
	void Sfm_NtkFree( Sfm_Ntk_t * p )
	{
	// user data
	Vec_StrFree( p->vFixed );
	Vec_StrFreeP( &p->vEmpty );
	Vec_WrdFree( p->vTruths );
	Vec_WecErase( &p->vFanins );
	// attributes
	Vec_WecErase( &p->vFanouts );
	ABC_FREE( p->vLevels.pArray );
	ABC_FREE( p->vLevelsR.pArray );
	ABC_FREE( p->vCounts.pArray );
	ABC_FREE( p->vTravIds.pArray );
	ABC_FREE( p->vTravIds2.pArray );
	ABC_FREE( p->vId2Var.pArray );
	ABC_FREE( p->vVar2Id.pArray );
	Vec_WecFree( p->vCnfs );
	Vec_IntFree( p->vCover );
	// other data
	Vec_IntFreeP( &p->vNodes );
	Vec_IntFreeP( &p->vDivs );
	Vec_IntFreeP( &p->vRoots );
	Vec_IntFreeP( &p->vTfo );
	Vec_WrdFreeP( &p->vDivCexes );
	Vec_IntFreeP( &p->vOrder );
	Vec_IntFreeP( &p->vDivVars );
	Vec_IntFreeP( &p->vDivIds );
	Vec_IntFreeP( &p->vLits );
	Vec_IntFreeP( &p->vValues );
	Vec_WecFreeP( &p->vClauses );
	Vec_IntFreeP( &p->vFaninMap );
	if ( p->pSat ) sat_solver_delete( p->pSat );
	ABC_FREE( p );
	}

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

	Synopsis [Performs resubstitution for the node.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Sfm_NtkRemoveFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
	{
	int RetValue;
	assert( Sfm_ObjIsNode(p, iNode) );
	assert( !Sfm_ObjIsPo(p, iFanin) );
	RetValue = Vec_IntRemove( Sfm_ObjFiArray(p, iNode), iFanin );
	assert( RetValue );
	RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );
	assert( RetValue );
	}
	void Sfm_NtkAddFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
	{
	if ( iFanin < 0 )
	return;
	assert( Sfm_ObjIsNode(p, iNode) );
	assert( !Sfm_ObjIsPo(p, iFanin) );
	assert( Vec_IntFind( Sfm_ObjFiArray(p, iNode), iFanin ) == -1 );
	assert( Vec_IntFind( Sfm_ObjFoArray(p, iFanin), iNode ) == -1 );
	Vec_IntPush( Sfm_ObjFiArray(p, iNode), iFanin );
	Vec_IntPush( Sfm_ObjFoArray(p, iFanin), iNode );
	}
	void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
	{
	int i, iFanin;
	if ( Sfm_ObjFanoutNum(p, iNode) > 0 \|\| Sfm_ObjIsPi(p, iNode) \|\| Sfm_ObjIsFixed(p, iNode) )
	return;
	assert( Sfm_ObjIsNode(p, iNode) );
	Sfm_ObjForEachFanin( p, iNode, iFanin, i )
	{
	int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode ); assert( RetValue );
	Sfm_NtkDeleteObj_rec( p, iFanin );
	}
	Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
	Vec_WrdWriteEntry( p->vTruths, iNode, (word)0 );
	}
	void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode )
	{
	int i, iFanout;
	int LevelNew = Sfm_ObjLevelNew( Sfm_ObjFiArray(p, iNode), &p->vLevels, Sfm_ObjAddsLevel(p, iNode) );
	if ( LevelNew == Sfm_ObjLevel(p, iNode) )
	return;
	Sfm_ObjSetLevel( p, iNode, LevelNew );
	Sfm_ObjForEachFanout( p, iNode, iFanout, i )
	Sfm_NtkUpdateLevel_rec( p, iFanout );
	}
	void Sfm_NtkUpdateLevelR_rec( Sfm_Ntk_t * p, int iNode )
	{
	int i, iFanin;
	int LevelNew = Sfm_ObjLevelNewR( Sfm_ObjFoArray(p, iNode), &p->vLevelsR, Sfm_ObjAddsLevel(p, iNode) );
	if ( LevelNew == Sfm_ObjLevelR(p, iNode) )
	return;
	Sfm_ObjSetLevelR( p, iNode, LevelNew );
	Sfm_ObjForEachFanin( p, iNode, iFanin, i )
	Sfm_NtkUpdateLevelR_rec( p, iFanin );
	}
	void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth )
	{
	int iFanin = Sfm_ObjFanin( p, iNode, f );
	assert( Sfm_ObjIsNode(p, iNode) );
	assert( iFanin != iFaninNew );
	if ( uTruth == 0 \|\| ~uTruth == 0 )
	{
	Sfm_ObjForEachFanin( p, iNode, iFanin, f )
	{
	int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode ); assert( RetValue );
	Sfm_NtkDeleteObj_rec( p, iFanin );
	}
	Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
	}
	else
	{
	// replace old fanin by new fanin
	Sfm_NtkRemoveFanin( p, iNode, iFanin );
	Sfm_NtkAddFanin( p, iNode, iFaninNew );
	// recursively remove MFFC
	Sfm_NtkDeleteObj_rec( p, iFanin );
	}
	// update logic level
	Sfm_NtkUpdateLevel_rec( p, iNode );
	if ( iFaninNew != -1 )
	Sfm_NtkUpdateLevelR_rec( p, iFaninNew );
	if ( Sfm_ObjFanoutNum(p, iFanin) > 0 )
	Sfm_NtkUpdateLevelR_rec( p, iFanin );
	// update truth table
	Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
	Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
	}

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

	Synopsis [Public APIs of this network.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i )
	{
	return Vec_WecEntry( &p->vFanins, i );
	}
	word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i )
	{
	return Vec_WrdEntryP( p->vTruths, i );
	}
	int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i )
	{
	return (int)Vec_StrEntry( p->vFixed, i );
	}
	int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i )
	{
	return (Sfm_ObjFaninNum(p, i) > 0) \|\| (Sfm_ObjFanoutNum(p, i) > 0);
	}

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


	ABC_NAMESPACE_IMPL_END