summaryrefslogtreecommitdiffstats
path: root/src/opt/sfm/sfmNtk.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/sfm/sfmNtk.c')
-rw-r--r--src/opt/sfm/sfmNtk.c144
1 files changed, 102 insertions, 42 deletions
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index d9b17799..3098d72f 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -107,46 +107,21 @@ void Sfm_CreateFanout( Vec_Wec_t * vFanins, Vec_Wec_t * vFanouts )
SeeAlso []
***********************************************************************/
-void Sfm_CreateLevel( Vec_Wec_t * vFanins, Vec_Int_t * vLevels )
+static inline int Sfm_ObjCreateLevel( Vec_Int_t * vArray, Vec_Int_t * vLevels )
{
- Vec_Int_t * vArray;
- int i, k, Fanin, * pLevels;
- Vec_IntFill( vLevels, Vec_WecSize(vFanins), 0 );
- pLevels = Vec_IntArray( vLevels );
- Vec_WecForEachLevel( vFanins, vArray, i )
- Vec_IntForEachEntry( vArray, Fanin, k )
- pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[Fanin] + 1 );
+ int k, Fanin, Level = 0;
+ Vec_IntForEachEntry( vArray, Fanin, k )
+ Level = Abc_MaxInt( Level, Vec_IntEntry(vLevels, Fanin) + 1 );
+ return Level;
}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
+void Sfm_CreateLevel( Vec_Wec_t * vFanins, Vec_Int_t * vLevels )
{
- Vec_Wec_t * vCnfs;
- Vec_Str_t * vCnf, * vCnfBase;
- word uTruth;
+ Vec_Int_t * vArray;
int i;
- vCnf = Vec_StrAlloc( 100 );
- vCnfs = Vec_WecStart( p->nObjs );
- Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos )
- {
- Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
- vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i );
- Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
- memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) );
- vCnfBase->nSize = Vec_StrSize(vCnf);
- }
- Vec_StrFree( vCnf );
- return vCnfs;
+ assert( Vec_IntSize(vLevels) == 0 );
+ Vec_IntGrow( vLevels, Vec_WecSize(vFanins) );
+ Vec_WecForEachLevel( vFanins, vArray, i )
+ Vec_IntPush( vLevels, Sfm_ObjCreateLevel(vArray, vLevels) );
}
/**Function*************************************************************
@@ -177,15 +152,31 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
// attributes
Sfm_CreateFanout( &p->vFanins, &p->vFanouts );
Sfm_CreateLevel( &p->vFanins, &p->vLevels );
- 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, p->nObjs, -1 );
- Vec_IntFill( &p->vVar2Id, p->nObjs, -1 );
+ 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, p->nObjs, -1 );
+ Vec_IntFill( &p->vVar2Id, p->nObjs, -1 );
p->vCover = Vec_IntAlloc( 1 << 16 );
p->vCnfs = Sfm_CreateCnf( p );
return p;
}
+void Sfm_NtkPrepare( Sfm_Ntk_t * p )
+{
+ p->vDivCexes = Vec_WrdStart( p->pPars->nDivNumMax );
+ p->vLeaves = Vec_IntAlloc( 1000 );
+ p->vRoots = Vec_IntAlloc( 1000 );
+ p->vNodes = Vec_IntAlloc( 1000 );
+ p->vTfo = Vec_IntAlloc( 1000 );
+ p->vFans = Vec_IntAlloc( 100 );
+ p->vOrder = Vec_IntAlloc( 100 );
+ p->vDivVars = Vec_IntAlloc( 100 );
+ p->vDivs = Vec_IntAlloc( 100 );
+ p->vDivIds = Vec_IntAlloc( 1000 );
+ p->vLits = Vec_IntAlloc( 100 );
+ p->vClauses = Vec_WecAlloc( 100 );
+ p->vFaninMap = Vec_IntAlloc( 10 );
+}
void Sfm_NtkFree( Sfm_Ntk_t * p )
{
// user data
@@ -203,14 +194,17 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
Vec_WecFree( p->vCnfs );
Vec_IntFree( p->vCover );
// other data
+ Vec_WrdFreeP( &p->vDivCexes );
Vec_IntFreeP( &p->vLeaves );
Vec_IntFreeP( &p->vRoots );
Vec_IntFreeP( &p->vNodes );
Vec_IntFreeP( &p->vTfo );
+ Vec_IntFreeP( &p->vFans );
+ Vec_IntFreeP( &p->vOrder );
+ Vec_IntFreeP( &p->vDivVars );
Vec_IntFreeP( &p->vDivs );
Vec_IntFreeP( &p->vDivIds );
Vec_IntFreeP( &p->vLits );
- Vec_IntFreeP( &p->vDiffs );
Vec_WecFreeP( &p->vClauses );
Vec_IntFreeP( &p->vFaninMap );
if ( p->pSat0 ) sat_solver_delete( p->pSat0 );
@@ -220,6 +214,72 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
/**Function*************************************************************
+ Synopsis [Performs resubstitution for the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sfm_NtkRemoveFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
+{
+ int RetValue;
+ 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( 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 )
+ return;
+ Sfm_ObjForEachFanin( p, iNode, iFanin, i )
+ {
+ int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode ); assert( RetValue );
+ if ( Sfm_ObjFanoutNum(p, iFanin) == 0 )
+ Sfm_NtkDeleteObj_rec( p, iFanin );
+ }
+ Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
+}
+void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode )
+{
+ int i, iFanout;
+ int LevelNew = Sfm_ObjCreateLevel( Sfm_ObjFiArray(p, iNode), &p->vLevels );
+ 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_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth )
+{
+ int iFanin = Sfm_ObjFanin( p, iNode, f );
+ // 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 );
+ // 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 []