summaryrefslogtreecommitdiffstats
path: root/src/opt/res
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/res')
-rw-r--r--src/opt/res/resCore.c73
-rw-r--r--src/opt/res/resDivs.c170
-rw-r--r--src/opt/res/resFilter.c10
-rw-r--r--src/opt/res/resInt.h70
-rw-r--r--src/opt/res/resSat.c62
-rw-r--r--src/opt/res/resSim.c6
-rw-r--r--src/opt/res/resStrash.c22
-rw-r--r--src/opt/res/resUpdate.c8
-rw-r--r--src/opt/res/resWin.c358
9 files changed, 519 insertions, 260 deletions
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index 5f814c3a..609addf9 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -39,15 +39,19 @@ struct Res_Man_t_
Sto_Man_t * pCnf; // the CNF of the SAT problem
Int_Man_t * pMan; // interpolation manager;
Vec_Int_t * vMem; // memory for intermediate SOPs
- Vec_Vec_t * vResubs; // resubstitution candidates
+ Vec_Vec_t * vResubs; // resubstitution candidates of the AIG
+ Vec_Vec_t * vResubsW; // resubstitution candidates of the window
Vec_Vec_t * vLevels; // levelized structure for updating
// statistics
int nWins; // the number of windows tried
int nWinNodes; // the total number of window nodes
int nDivNodes; // the total number of divisors
+ int nWinsTriv; // the total number of trivial windows
+ int nWinsUsed; // the total number of useful windows (with at least one candidate)
int nCandSets; // the total number of candidates
int nProvedSets; // the total number of proved groups
int nSimEmpty; // the empty simulation info
+ int nTotalNets; // the total number of nets
// runtime
int timeWin; // windowing
int timeDiv; // divisors
@@ -90,6 +94,7 @@ Res_Man_t * Res_ManAlloc( Res_Par_t * pPars )
p->pMan = Int_ManAlloc( 512 );
p->vMem = Vec_IntAlloc( 0 );
p->vResubs = Vec_VecStart( pPars->nCands );
+ p->vResubsW = Vec_VecStart( pPars->nCands );
p->vLevels = Vec_VecStart( 32 );
return p;
}
@@ -113,9 +118,11 @@ void Res_ManFree( Res_Man_t * p )
printf( "Nodes = %d. (Ave = %5.1f) ", p->nWinNodes, 1.0*p->nWinNodes/p->nWins );
printf( "Divs = %d. (Ave = %5.1f) ", p->nDivNodes, 1.0*p->nDivNodes/p->nWins );
printf( "\n" );
- printf( "SimEmpt = %d. ", p->nSimEmpty );
+ printf( "WinsTriv = %d. ", p->nWinsTriv );
+ printf( "SimsEmpt = %d. ", p->nSimEmpty );
+ printf( "WindUsed = %d. ", p->nWinsUsed );
printf( "Cands = %d. ", p->nCandSets );
- printf( "Proved = %d. ", p->nProvedSets );
+ printf( "Proved = %d. (%.2f %%)", p->nProvedSets, 100.0*p->nProvedSets/p->nTotalNets );
printf( "\n" );
PRT( "Windowing ", p->timeWin );
@@ -135,6 +142,7 @@ void Res_ManFree( Res_Man_t * p )
Int_ManFree( p->pMan );
Vec_IntFree( p->vMem );
Vec_VecFree( p->vResubs );
+ Vec_VecFree( p->vResubsW );
Vec_VecFree( p->vLevels );
free( p );
}
@@ -164,6 +172,7 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
// start the manager
p = Res_ManAlloc( pPars );
+ p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
// set the number of levels
Abc_NtkLevel( pNtk );
@@ -182,15 +191,32 @@ clk = clock();
p->timeWin += clock() - clk;
if ( !RetValue )
continue;
+ p->nWinsTriv += Res_WinIsTrivial( p->pWin );
- p->nWins++;
- p->nWinNodes += Vec_VecSizeSize( p->pWin->vLevels );
+ if ( p->pPars->fVeryVerbose )
+ {
+ printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level );
+ printf( "Win = %3d/%3d/%4d/%3d ",
+ Vec_PtrSize(p->pWin->vLeaves),
+ Vec_PtrSize(p->pWin->vBranches),
+ Vec_PtrSize(p->pWin->vNodes),
+ Vec_PtrSize(p->pWin->vRoots) );
+ }
// collect the divisors
clk = clock();
Res_WinDivisors( p->pWin, pObj->Level - 1 );
p->timeDiv += clock() - clk;
- p->nDivNodes += Vec_PtrSize( p->pWin->vDivs );
+
+ p->nWins++;
+ p->nWinNodes += Vec_PtrSize(p->pWin->vNodes);
+ p->nDivNodes += Vec_PtrSize( p->pWin->vDivs);
+
+ if ( p->pPars->fVeryVerbose )
+ {
+ printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) );
+ printf( "D+ = %3d ", p->pWin->nDivsPlus );
+ }
// create the AIG for the window
clk = clock();
@@ -200,13 +226,6 @@ p->timeAig += clock() - clk;
if ( p->pPars->fVeryVerbose )
{
- printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level );
- printf( "Win = %3d/%3d/%4d/%3d ",
- Vec_PtrSize(p->pWin->vLeaves) - p->pWin->nLeavesPlus,
- p->pWin->nLeavesPlus, Vec_VecSizeSize(p->pWin->vLevels),
- Vec_PtrSize(p->pWin->vRoots) );
- printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) );
- printf( "D+ = %3d ", p->pWin->nDivsPlus );
printf( "AIG = %4d ", Abc_NtkNodeNum(p->pAig) );
printf( "\n" );
}
@@ -223,12 +242,14 @@ p->timeSim += clock() - clk;
// find resub candidates for the node
clk = clock();
- RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs );
+ RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW );
p->timeCand += clock() - clk;
p->nCandSets += RetValue;
if ( RetValue == 0 )
continue;
+ p->nWinsUsed++;
+
// iterate through candidate resubstitutions
Vec_VecForEachLevel( p->vResubs, vFanins, k )
{
@@ -247,26 +268,19 @@ p->timeSat += clock() - clk;
}
p->nProvedSets++;
// printf( " Unsat\n" );
- continue;
+// continue;
// write it into a file
// Sto_ManDumpClauses( p->pCnf, "trace.cnf" );
-
- // interplate the problem if it was UNSAT
+ // interpolate the problem if it was UNSAT
clk = clock();
- RetValue = Int_ManInterpolate( p->pMan, p->pCnf, p->pPars->fVerbose, &puTruth );
+ nFanins = Int_ManInterpolate( p->pMan, p->pCnf, 0, &puTruth );
p->timeInt += clock() - clk;
- assert( RetValue == Vec_PtrSize(vFanins) - 2 );
-
- if ( puTruth )
- {
- Extra_PrintBinary( stdout, puTruth, 1 << RetValue );
- printf( "\n" );
- }
-
- continue;
-
+ assert( nFanins == Vec_PtrSize(vFanins) - 2 );
+ assert( puTruth );
+// Extra_PrintBinary( stdout, puTruth, 1 << nFanins ); printf( "\n" );
+
// transform interpolant into the AIG
pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
@@ -276,10 +290,11 @@ p->timeInt += clock() - clk;
// update the network
clk = clock();
- Res_UpdateNetwork( pObj, vFanins, pFunc, p->vLevels );
+ Res_UpdateNetwork( pObj, Vec_VecEntry(p->vResubsW, k), pFunc, p->vLevels );
p->timeUpd += clock() - clk;
break;
}
+
}
// quit resubstitution manager
diff --git a/src/opt/res/resDivs.c b/src/opt/res/resDivs.c
index bff91983..af30592c 100644
--- a/src/opt/res/resDivs.c
+++ b/src/opt/res/resDivs.c
@@ -25,6 +25,9 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+static void Res_WinMarkTfi( Res_Win_t * p );
+static int Res_WinVisitMffc( Res_Win_t * p );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -43,84 +46,155 @@
void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
{
Abc_Obj_t * pObj, * pFanout, * pFanin;
- int i, k, f, m;
+ int k, f, m;
+ // set the maximum level of the divisors
p->nLevDivMax = nLevDivMax;
- // mark the leaves and the internal nodes
- Vec_PtrForEachEntry( p->vLeaves, pObj, i )
- pObj->fMarkA = 1;
- Vec_VecForEachEntry( p->vLevels, pObj, i, k )
- pObj->fMarkA = 1;
+ // mark the TFI with the current trav ID
+ Abc_NtkIncrementTravId( p->pNode->pNtk );
+ Res_WinMarkTfi( p );
- // prepare the new trav ID
+ // mark with the current trav ID those nodes that should not be divisors:
+ // (1) the node and its TFO
+ // (2) the MFFC of the node
+ // (3) the node's fanins (these are treated as a special case)
Abc_NtkIncrementTravId( p->pNode->pNtk );
- // mark the TFO of the node (does not increment trav ID)
- Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax, NULL );
- // mark the MFFC of the node (does not increment trav ID)
+ Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax );
Res_WinVisitMffc( p );
+ Abc_ObjForEachFanin( p->pNode, pObj, k )
+ Abc_NodeSetTravIdCurrent( pObj );
- // what about the fanouts of the leaves!!!
+ // at this point the nodes are marked with two trav IDs:
+ // nodes to be collected as divisors are marked with previous trav ID
+ // nodes to be avoided as divisors are marked with current trav ID
- // go through all the legal levels and check if their fanouts can be divisors
- p->nDivsPlus = 0;
- Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevDivMax - 1 )
+ // start collecting the divisors
+ Vec_PtrClear( p->vDivs );
+ Vec_PtrForEachEntry( p->vLeaves, pObj, k )
+ {
+ assert( (int)pObj->Level >= p->nLevLeafMin );
+ if ( !Abc_NodeIsTravIdPrevious(pObj) )
+ continue;
+ if ( (int)pObj->Level > p->nLevDivMax )
+ continue;
+ Vec_PtrPush( p->vDivs, pObj );
+ }
+ // add the internal nodes to the data structure
+ Vec_PtrForEachEntry( p->vNodes, pObj, k )
{
- // skip nodes in the TFO or in the MFFC of node
- if ( Abc_NodeIsTravIdCurrent(pObj) )
+ if ( !Abc_NodeIsTravIdPrevious(pObj) )
+ continue;
+ if ( (int)pObj->Level > p->nLevDivMax )
continue;
+ Vec_PtrPush( p->vDivs, pObj );
+ }
+
+ // explore the fanouts of already collected divisors
+ p->nDivsPlus = 0;
+ Vec_PtrForEachEntry( p->vDivs, pObj, k )
+ {
// consider fanouts of this node
Abc_ObjForEachFanout( pObj, pFanout, f )
{
+ // stop if there are too many fanouts
+ if ( f > 20 )
+ break;
// skip nodes that are already added
- if ( pFanout->fMarkA )
- continue;
- // skip COs
- if ( !Abc_ObjIsNode(pFanout) )
+ if ( Abc_NodeIsTravIdPrevious(pFanout) )
continue;
// skip nodes in the TFO or in the MFFC of node
if ( Abc_NodeIsTravIdCurrent(pFanout) )
continue;
+ // skip COs
+ if ( !Abc_ObjIsNode(pFanout) )
+ continue;
// skip nodes with large level
- if ( (int)pFanout->Level > p->nLevDivMax )
+ if ( (int)pFanout->Level >= p->nLevDivMax )
continue;
- // skip nodes whose fanins are not in the cone
+ // skip nodes whose fanins are not divisors
Abc_ObjForEachFanin( pFanout, pFanin, m )
- if ( !pFanin->fMarkA )
+ if ( !Abc_NodeIsTravIdPrevious(pFanin) )
break;
if ( m < Abc_ObjFaninNum(pFanout) )
continue;
- // add the node
- Res_WinAddNode( p, pFanout );
+ // add the node to the divisors
+ Vec_PtrPush( p->vDivs, pFanout );
+ Vec_PtrPush( p->vNodes, pFanout );
+ Abc_NodeSetTravIdPrevious( pFanout );
p->nDivsPlus++;
}
}
+}
- // unmark the leaves and the internal nodes
- Vec_PtrForEachEntry( p->vLeaves, pObj, i )
- pObj->fMarkA = 0;
- Vec_VecForEachEntry( p->vLevels, pObj, i, k )
- pObj->fMarkA = 0;
+/**Function*************************************************************
- // collect the divisors below the line
- Vec_PtrClear( p->vDivs );
- // collect the node fanins first and mark the fanins
- Abc_ObjForEachFanin( p->pNode, pFanin, m )
- {
- Vec_PtrPush( p->vDivs, pFanin );
- Abc_NodeSetTravIdCurrent( pFanin );
- }
- // collect the remaining leaves
+ Synopsis [Marks the TFI cone of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_WinMarkTfi_rec( Res_Win_t * p, Abc_Obj_t * pObj )
+{
+ Abc_Obj_t * pFanin;
+ int i;
+ if ( Abc_NodeIsTravIdCurrent(pObj) )
+ return;
+ Abc_NodeSetTravIdCurrent( pObj );
+ assert( Abc_ObjIsNode(pObj) );
+ // visit the fanins of the node
+ Abc_ObjForEachFanin( pObj, pFanin, i )
+ Res_WinMarkTfi_rec( p, pFanin );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks the TFI cone of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_WinMarkTfi( Res_Win_t * p )
+{
+ Abc_Obj_t * pObj;
+ int i;
+ // mark the leaves
Vec_PtrForEachEntry( p->vLeaves, pObj, i )
- if ( !Abc_NodeIsTravIdCurrent(pObj) )
- Vec_PtrPush( p->vDivs, pObj );
- // collect remaining unvisited divisors
- Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves, p->nLevDivMax )
- if ( !Abc_NodeIsTravIdCurrent(pObj) )
- Vec_PtrPush( p->vDivs, pObj );
-
- // verify the resulting window
-// Res_WinVerify( p );
+ Abc_NodeSetTravIdCurrent( pObj );
+ // start from the node
+ Res_WinMarkTfi_rec( p, p->pNode );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks the TFO of the collected nodes up to the given level.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit )
+{
+ Abc_Obj_t * pFanout;
+ int i;
+ if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit )
+ return;
+ if ( Abc_NodeIsTravIdCurrent(pObj) )
+ return;
+ Abc_NodeSetTravIdCurrent( pObj );
+ Abc_ObjForEachFanout( pObj, pFanout, i )
+ Res_WinSweepLeafTfo_rec( pFanout, nLevelLimit );
}
/**Function*************************************************************
diff --git a/src/opt/res/resFilter.c b/src/opt/res/resFilter.c
index 4f1be833..38f64815 100644
--- a/src/opt/res/resFilter.c
+++ b/src/opt/res/resFilter.c
@@ -42,7 +42,7 @@ static unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim
SeeAlso []
***********************************************************************/
-int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs )
+int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW )
{
Abc_Obj_t * pFanin, * pFanin2;
unsigned * pInfo;
@@ -52,18 +52,19 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim,
pInfo = Vec_PtrEntry( pSim->vOuts, 1 );
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue == 0 )
- printf( "Failed 1!" );
+ printf( "Failed 1!\n" );
// collect the fanin info
pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 );
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue == 0 )
- printf( "Failed 2!" );
+ printf( "Failed 2!\n" );
// try removing fanins
// printf( "Fanins: " );
Counter = 0;
Vec_VecClear( vResubs );
+ Vec_VecClear( vResubsW );
Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
{
pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) );
@@ -78,7 +79,10 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim,
Abc_ObjForEachFanin( pWin->pNode, pFanin2, k )
{
if ( k != i )
+ {
Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
+ Vec_VecPush( vResubsW, Counter, pFanin2 );
+ }
}
Counter++;
}
diff --git a/src/opt/res/resInt.h b/src/opt/res/resInt.h
index 54251722..9d17cb1c 100644
--- a/src/opt/res/resInt.h
+++ b/src/opt/res/resInt.h
@@ -42,49 +42,48 @@ extern "C" {
typedef struct Res_Win_t_ Res_Win_t;
struct Res_Win_t_
{
- // the general data
- int nWinTfiMax; // the fanin levels
- int nWinTfoMax; // the fanout levels
- int nLevLeaves; // the level where leaves begin
- int nLevDivMax; // the maximum divisor level
- int nDivsPlus; // the number of additional divisors
- int nLeavesPlus;// the number of additional leaves
- Abc_Obj_t * pNode; // the node in the center
+ // windowing parameters
+ Abc_Obj_t * pNode; // the node in the center
+ int nWinTfiMax; // the fanin levels
+ int nWinTfoMax; // the fanout levels
+ int nLevDivMax; // the maximum divisor level
+ // internal windowing parameters
+ int nFanoutLimit; // the limit on the fanout count of a TFO node (if more, the node is treated as a root)
+ int nLevTfiMinus; // the number of additional levels to search from TFO below the level of leaves
+ // derived windowing parameters
+ int nLevLeafMin; // the minimum level of a leaf
+ int nLevTravMin; // the minimum level to search from TFO
+ int nDivsPlus; // the number of additional divisors
// the window data
- Vec_Vec_t * vLevels; // nodes by level
- Vec_Ptr_t * vLeaves; // leaves of the window
- Vec_Ptr_t * vRoots; // roots of the window
- Vec_Ptr_t * vDivs; // the candidate divisors of the node
+ Vec_Ptr_t * vRoots; // outputs of the window
+ Vec_Ptr_t * vLeaves; // inputs of the window
+ Vec_Ptr_t * vBranches; // side nodes of the window
+ Vec_Ptr_t * vNodes; // internal nodes of the window
+ Vec_Ptr_t * vDivs; // candidate divisors of the node
+ // temporary data
+ Vec_Vec_t * vMatrix; // TFI nodes below the given node
};
typedef struct Res_Sim_t_ Res_Sim_t;
struct Res_Sim_t_
{
- Abc_Ntk_t * pAig; // AIG for simulation
+ Abc_Ntk_t * pAig; // AIG for simulation
// simulation parameters
- int nWords; // the number of simulation words
- int nPats; // the number of patterns
- int nWordsOut; // the number of simulation words in the output patterns
- int nPatsOut; // the number of patterns in the output patterns
+ int nWords; // the number of simulation words
+ int nPats; // the number of patterns
+ int nWordsOut; // the number of simulation words in the output patterns
+ int nPatsOut; // the number of patterns in the output patterns
// simulation info
- Vec_Ptr_t * vPats; // input simulation patterns
- Vec_Ptr_t * vPats0; // input simulation patterns
- Vec_Ptr_t * vPats1; // input simulation patterns
- Vec_Ptr_t * vOuts; // output simulation info
- int nPats0; // the number of 0-patterns accumulated
- int nPats1; // the number of 1-patterns accumulated
+ Vec_Ptr_t * vPats; // input simulation patterns
+ Vec_Ptr_t * vPats0; // input simulation patterns
+ Vec_Ptr_t * vPats1; // input simulation patterns
+ Vec_Ptr_t * vOuts; // output simulation info
+ int nPats0; // the number of 0-patterns accumulated
+ int nPats1; // the number of 1-patterns accumulated
// resub candidates
- Vec_Vec_t * vCands; // resubstitution candidates
+ Vec_Vec_t * vCands; // resubstitution candidates
};
-// adds one node to the window
-static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj )
-{
- assert( !pObj->fMarkA );
- pObj->fMarkA = 1;
- Vec_VecPush( p->vLevels, pObj->Level, pObj );
-}
-
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -95,11 +94,12 @@ static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj )
/*=== resDivs.c ==========================================================*/
extern void Res_WinDivisors( Res_Win_t * p, int nLevDivMax );
-extern int Res_WinVisitMffc( Res_Win_t * p );
+extern void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit );
/*=== resFilter.c ==========================================================*/
-extern int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs );
+extern int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW );
/*=== resSat.c ==========================================================*/
extern void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
+extern void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
/*=== resSim.c ==========================================================*/
extern Res_Sim_t * Res_SimAlloc( int nWords );
extern void Res_SimFree( Res_Sim_t * p );
@@ -111,7 +111,7 @@ extern void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, H
/*=== resWnd.c ==========================================================*/
extern Res_Win_t * Res_WinAlloc();
extern void Res_WinFree( Res_Win_t * p );
-extern void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode );
+extern int Res_WinIsTrivial( Res_Win_t * p );
extern int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p );
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c
index ec609445..f9558c97 100644
--- a/src/opt/res/resSat.c
+++ b/src/opt/res/resSat.c
@@ -37,7 +37,7 @@ extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int
/**Function*************************************************************
- Synopsis [Loads AIG into the SAT solver.]
+ Synopsis [Loads AIG into the SAT solver for checking resubstitution.]
Description []
@@ -126,6 +126,66 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
/**Function*************************************************************
+ Synopsis [Loads AIG into the SAT solver for constrained simulation.]
+
+ Description [The array of fanins contains exactly two entries: the
+ care set and the functions.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
+{
+ sat_solver * pSat;
+ Vec_Ptr_t * vNodes;
+ Abc_Obj_t * pObj;
+ int i, nNodes;
+
+ // make sure fanins contain POs of the AIG
+ pObj = Vec_PtrEntry( vFanins, 0 );
+ assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) );
+ assert( Vec_PtrSize(vFanins) == 2 );
+
+ // collect reachable nodes
+ vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );
+
+ // assign unique numbers to each node
+ nNodes = 0;
+ Abc_AigConst1(pAig)->pCopy = (void *)nNodes++;
+ Abc_NtkForEachPi( pAig, pObj, i )
+ pObj->pCopy = (void *)nNodes++;
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ pObj->pCopy = (void *)nNodes++;
+ Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
+ pObj->pCopy = (void *)nNodes++;
+
+ // start the solver
+ pSat = sat_solver_new();
+
+ // add clause for the constant node
+ Res_SatAddConst1( pSat, (int)Abc_AigConst1(pAig)->pCopy, 0 );
+ // add clauses for AND gates
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ Res_SatAddAnd( pSat, (int)pObj->pCopy,
+ (int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+ Vec_PtrFree( vNodes );
+ // add clauses for POs
+ Vec_PtrForEachEntry( vFanins, pObj, i )
+ Res_SatAddEqual( pSat, (int)pObj->pCopy,
+ (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+
+ // add trivial clauses
+ pObj = Vec_PtrEntry(vFanins, 0);
+ Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set
+ pObj = Vec_PtrEntry(vFanins, 1);
+ Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // on-set
+ return pSat;
+}
+
+/**Function*************************************************************
+
Synopsis [Asserts equality of the variable to a constant.]
Description []
diff --git a/src/opt/res/resSim.c b/src/opt/res/resSim.c
index 81267540..cc896ec0 100644
--- a/src/opt/res/resSim.c
+++ b/src/opt/res/resSim.c
@@ -484,13 +484,13 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
Res_SimProcessPats( p );
if ( !(p->nPats0 < p->nPats || p->nPats1 < p->nPats) )
break;
-
}
// printf( "%d ", Limit );
// report the last set of patterns
- Res_SimReportOne( p );
- printf( "\n" );
+// Res_SimReportOne( p );
+// printf( "\n" );
// quit if there is not enough
+// if ( p->nPats0 < 4 || p->nPats1 < 4 )
if ( p->nPats0 < 4 || p->nPats1 < 4 )
{
// Res_SimReportOne( p );
diff --git a/src/opt/res/resStrash.c b/src/opt/res/resStrash.c
index d3a8efa8..fde842a4 100644
--- a/src/opt/res/resStrash.c
+++ b/src/opt/res/resStrash.c
@@ -48,22 +48,25 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
Vec_Ptr_t * vPairs;
Abc_Ntk_t * pAig;
Abc_Obj_t * pObj, * pMiter;
- int i, k;
+ int i;
assert( Abc_NtkHasAig(p->pNode->pNtk) );
+// Abc_NtkCleanCopy( p->pNode->pNtk );
// create the network
pAig = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
pAig->pName = Extra_UtilStrsav( "window" );
// create the inputs
Vec_PtrForEachEntry( p->vLeaves, pObj, i )
pObj->pCopy = Abc_NtkCreatePi( pAig );
+ Vec_PtrForEachEntry( p->vBranches, pObj, i )
+ pObj->pCopy = Abc_NtkCreatePi( pAig );
// go through the nodes in the topological order
- Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves + 1, (int)p->pNode->Level + p->nWinTfoMax )
+ Vec_PtrForEachEntry( p->vNodes, pObj, i )
{
pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj );
if ( pObj == p->pNode )
pObj->pCopy = Abc_ObjNot( pObj->pCopy );
}
- // collect the PO outputs
+ // collect the POs
vPairs = Vec_PtrAlloc( 2 * Vec_PtrSize(p->vRoots) );
Vec_PtrForEachEntry( p->vRoots, pObj, i )
{
@@ -72,15 +75,17 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
}
// mark the TFO of the node
Abc_NtkIncrementTravId( p->pNode->pNtk );
- Res_WinSweepLeafTfo_rec( p->pNode, (int)p->pNode->Level + p->nWinTfoMax, NULL );
- // redo strashing in the TFO
+ Res_WinSweepLeafTfo_rec( p->pNode, (int)p->pNode->Level + p->nWinTfoMax );
+ // update strashing of the node
p->pNode->pCopy = Abc_ObjNot( p->pNode->pCopy );
- Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->pNode->Level + 1, (int)p->pNode->Level + p->nWinTfoMax )
+ Abc_NodeSetTravIdPrevious( p->pNode );
+ // redo strashing in the TFO
+ Vec_PtrForEachEntry( p->vNodes, pObj, i )
{
if ( Abc_NodeIsTravIdCurrent(pObj) )
pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj );
}
- // collect the PO outputs
+ // collect the POs
Vec_PtrForEachEntry( p->vRoots, pObj, i )
Vec_PtrWriteEntry( vPairs, 2 * i + 1, pObj->pCopy );
// add the miter
@@ -89,6 +94,9 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
Vec_PtrFree( vPairs );
// add the node
Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), p->pNode->pCopy );
+ // add the fanins
+ Abc_ObjForEachFanin( p->pNode, pObj, i )
+ Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy );
// add the divisors
Vec_PtrForEachEntry( p->vDivs, pObj, i )
Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy );
diff --git a/src/opt/res/resUpdate.c b/src/opt/res/resUpdate.c
index 06704b1c..01400ead 100644
--- a/src/opt/res/resUpdate.c
+++ b/src/opt/res/resUpdate.c
@@ -45,11 +45,11 @@ static int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj );
void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels )
{
Abc_Obj_t * pObjNew, * pFanin, * pFanout, * pTemp;
- int i, k, m;
+ int Lev, k, m;
// create the new node
pObjNew = Abc_NtkCreateNode( pObj->pNtk );
pObjNew->pData = pFunc;
- Vec_PtrForEachEntry( vFanins, pFanin, i )
+ Vec_PtrForEachEntry( vFanins, pFanin, k )
Abc_ObjAddFanin( pObjNew, pFanin );
// replace the old node by the new node
pObjNew->Level = pObj->Level;
@@ -62,12 +62,12 @@ void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc
Vec_VecPush( vLevels, pObjNew->Level, pObjNew );
pObjNew->fMarkA = 1;
// recursively update level
- Vec_VecForEachEntryStart( vLevels, pTemp, i, k, pObjNew->Level )
+ Vec_VecForEachEntryStart( vLevels, pTemp, Lev, k, pObjNew->Level )
{
pTemp->fMarkA = 0;
pTemp->Level = Res_UpdateNetworkLevelNew( pTemp );
// if the level did not change, to need to check the fanout levels
- if ( (int)pTemp->Level == i )
+ if ( (int)pTemp->Level == Lev )
continue;
// schedule fanout for level update
Abc_ObjForEachFanout( pTemp, pFanout, m )
diff --git a/src/opt/res/resWin.c b/src/opt/res/resWin.c
index fa74b219..80a65ea8 100644
--- a/src/opt/res/resWin.c
+++ b/src/opt/res/resWin.c
@@ -43,12 +43,19 @@
Res_Win_t * Res_WinAlloc()
{
Res_Win_t * p;
+ // start the manager
p = ALLOC( Res_Win_t, 1 );
memset( p, 0, sizeof(Res_Win_t) );
- p->vLevels = Vec_VecStart( 128 );
- p->vLeaves = Vec_PtrAlloc( 512 );
- p->vRoots = Vec_PtrAlloc( 512 );
- p->vDivs = Vec_PtrAlloc( 512 );
+ // set internal parameters
+ p->nFanoutLimit = 10;
+ p->nLevTfiMinus = 3;
+ // allocate storage
+ p->vRoots = Vec_PtrAlloc( 256 );
+ p->vLeaves = Vec_PtrAlloc( 256 );
+ p->vBranches = Vec_PtrAlloc( 256 );
+ p->vNodes = Vec_PtrAlloc( 256 );
+ p->vDivs = Vec_PtrAlloc( 256 );
+ p->vMatrix = Vec_VecStart( 128 );
return p;
}
@@ -65,48 +72,87 @@ Res_Win_t * Res_WinAlloc()
***********************************************************************/
void Res_WinFree( Res_Win_t * p )
{
- Vec_VecFree( p->vLevels );
- Vec_PtrFree( p->vLeaves );
Vec_PtrFree( p->vRoots );
+ Vec_PtrFree( p->vLeaves );
+ Vec_PtrFree( p->vBranches );
+ Vec_PtrFree( p->vNodes );
Vec_PtrFree( p->vDivs );
+ Vec_VecFree( p->vMatrix );
free( p );
}
+
+
/**Function*************************************************************
- Synopsis [Collects nodes in the limited TFI of the node.]
+ Synopsis [Collect the limited TFI cone of the node.]
- Description [Marks the collected nodes.]
+ Description []
SideEffects []
SeeAlso []
***********************************************************************/
-void Res_WinCollectNodeTfi( Res_Win_t * p )
+void Res_WinCollectLeavesAndNodes( Res_Win_t * p )
{
Vec_Ptr_t * vFront;
- Abc_Obj_t * pObj, * pFanin;
+ Abc_Obj_t * pObj, * pTemp;
int i, k, m;
- // expand storage for levels
- if ( Vec_VecSize( p->vLevels ) <= (int)p->pNode->Level + p->nWinTfoMax )
- Vec_VecExpand( p->vLevels, (int)p->pNode->Level + p->nWinTfoMax );
- // start the frontier
- Vec_VecClear( p->vLevels );
- Res_WinAddNode( p, p->pNode );
- // add one level at a time
- Vec_VecForEachLevelReverseStartStop( p->vLevels, vFront, i, p->pNode->Level, p->nLevLeaves + 1 )
+
+ assert( p->nWinTfiMax > 0 );
+ assert( Vec_VecSize(p->vMatrix) > p->nWinTfiMax );
+
+ // start matrix with the node
+ Vec_VecClear( p->vMatrix );
+ Vec_VecPush( p->vMatrix, 0, p->pNode );
+ Abc_NtkIncrementTravId( p->pNode->pNtk );
+ Abc_NodeSetTravIdCurrent( p->pNode );
+
+ // collect the leaves (nodes pTemp such that "p->pNode->Level - pTemp->Level > p->nWinTfiMax")
+ Vec_PtrClear( p->vLeaves );
+ Vec_VecForEachLevelStartStop( p->vMatrix, vFront, i, 0, p->nWinTfiMax )
{
Vec_PtrForEachEntry( vFront, pObj, k )
- Abc_ObjForEachFanin( pObj, pFanin, m )
- if ( !pFanin->fMarkA )
- Res_WinAddNode( p, pFanin );
+ {
+ Abc_ObjForEachFanin( pObj, pTemp, m )
+ {
+ if ( Abc_NodeIsTravIdCurrent( pTemp ) )
+ continue;
+ Abc_NodeSetTravIdCurrent( pTemp );
+ if ( Abc_ObjIsCi(pTemp) || (int)(p->pNode->Level - pTemp->Level) > p->nWinTfiMax )
+ Vec_PtrPush( p->vLeaves, pTemp );
+ else
+ Vec_VecPush( p->vMatrix, p->pNode->Level - pTemp->Level, pTemp );
+ }
+ }
}
+ assert( Vec_PtrSize(p->vLeaves) > 0 );
+
+ // collect the nodes in the reverse order
+ Vec_PtrClear( p->vNodes );
+ Vec_VecForEachLevelReverseStartStop( p->vMatrix, vFront, i, p->nWinTfiMax, 0 )
+ {
+ Vec_PtrForEachEntry( vFront, pObj, k )
+ Vec_PtrPush( p->vNodes, pObj );
+ Vec_PtrClear( vFront );
+ }
+
+ // get the lowest leaf level
+ p->nLevLeafMin = ABC_INFINITY;
+ Vec_PtrForEachEntry( p->vLeaves, pObj, k )
+ p->nLevLeafMin = ABC_MIN( p->nLevLeafMin, (int)pObj->Level );
+
+ // set minimum traversal level
+ p->nLevTravMin = ABC_MAX( ((int)p->pNode->Level) - p->nWinTfiMax - p->nLevTfiMinus, p->nLevLeafMin );
+ assert( p->nLevTravMin >= 0 );
}
+
+
/**Function*************************************************************
- Synopsis [Collect all the nodes that fanin into the window nodes.]
+ Synopsis [Returns 1 if the node should be a root.]
Description []
@@ -115,24 +161,25 @@ void Res_WinCollectNodeTfi( Res_Win_t * p )
SeeAlso []
***********************************************************************/
-void Res_WinCollectLeaves( Res_Win_t * p )
+static inline int Res_WinComputeRootsCheck( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit )
{
- Vec_Ptr_t * vLevel;
- Abc_Obj_t * pObj;
- int i, k;
- // add the leaves
- Vec_PtrClear( p->vLeaves );
- // collect the nodes below the given level
- Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevLeaves )
- Vec_PtrPush( p->vLeaves, pObj );
- // remove leaves from the set
- Vec_VecForEachLevelStartStop( p->vLevels, vLevel, i, 0, p->nLevLeaves )
- Vec_PtrClear( vLevel );
+ Abc_Obj_t * pFanout;
+ int i;
+ // the node is the root if one of the following is true:
+ // (1) the node has more than fanouts than the limit
+ if ( Abc_ObjFanoutNum(pNode) > nFanoutLimit )
+ return 1;
+ // (2) the node has CO fanouts
+ // (3) the node has fanouts above the cutoff level
+ Abc_ObjForEachFanout( pNode, pFanout, i )
+ if ( Abc_ObjIsCo(pFanout) || (int)pFanout->Level > nLevelMax )
+ return 1;
+ return 0;
}
/**Function*************************************************************
- Synopsis [Marks the TFO of the collected nodes up to the given level.]
+ Synopsis [Recursively collects the root candidates.]
Description []
@@ -141,22 +188,85 @@ void Res_WinCollectLeaves( Res_Win_t * p )
SeeAlso []
***********************************************************************/
-void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode )
+void Res_WinComputeRoots_rec( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit, Vec_Ptr_t * vRoots )
{
Abc_Obj_t * pFanout;
int i;
- if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit || pObj == pNode )
- return;
- if ( Abc_NodeIsTravIdCurrent(pObj) )
+ assert( Abc_ObjIsNode(pNode) );
+ if ( Abc_NodeIsTravIdCurrent(pNode) )
return;
- Abc_NodeSetTravIdCurrent( pObj );
- Abc_ObjForEachFanout( pObj, pFanout, i )
- Res_WinSweepLeafTfo_rec( pFanout, nLevelLimit, pNode );
+ Abc_NodeSetTravIdCurrent( pNode );
+ // check if the node should be the root
+ if ( Res_WinComputeRootsCheck( pNode, nLevelMax, nFanoutLimit ) )
+ Vec_PtrPush( vRoots, pNode );
+ else // if not, explore its fanouts
+ Abc_ObjForEachFanout( pNode, pFanout, i )
+ Res_WinComputeRoots_rec( pFanout, nLevelMax, nFanoutLimit, vRoots );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Recursively collects the root candidates.]
+
+ Description [Returns 1 if the only root is this node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Res_WinComputeRoots( Res_Win_t * p )
+{
+ Vec_PtrClear( p->vRoots );
+ Abc_NtkIncrementTravId( p->pNode->pNtk );
+ Res_WinComputeRoots_rec( p->pNode, p->pNode->Level + p->nWinTfoMax, p->nFanoutLimit, p->vRoots );
+ assert( Vec_PtrSize(p->vRoots) > 0 );
+ if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode )
+ return 0;
+ return 1;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Marks the paths from the roots to the leaves.]
+
+ Description [Returns 1 if the the node can reach a leaf.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Res_WinMarkPaths_rec( Abc_Obj_t * pNode, Abc_Obj_t * pPivot, int nLevelMin )
+{
+ Abc_Obj_t * pFanin;
+ int i, RetValue;
+ // skip visited nodes
+ if ( Abc_NodeIsTravIdCurrent(pNode) )
+ return 1;
+ if ( Abc_NodeIsTravIdPrevious(pNode) )
+ return 0;
+ // assume that the node does not have access to the leaves
+ Abc_NodeSetTravIdPrevious( pNode );
+ // skip nodes below the given level
+ if ( pNode == pPivot || (int)pNode->Level <= nLevelMin )
+ return 0;
+ assert( Abc_ObjIsNode(pNode) );
+ // check if the fanins have access to the leaves
+ RetValue = 0;
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ RetValue |= Res_WinMarkPaths_rec( pFanin, pPivot, nLevelMin );
+ // relabel the node if it has access to the leaves
+ if ( RetValue )
+ Abc_NodeSetTravIdCurrent( pNode );
+ return RetValue;
}
/**Function*************************************************************
- Synopsis [Marks the TFO of the collected nodes up to the given level.]
+ Synopsis [Marks the paths from the roots to the leaves.]
Description []
@@ -165,15 +275,25 @@ void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNo
SeeAlso []
***********************************************************************/
-void Res_WinSweepLeafTfo( Res_Win_t * p )
+void Res_WinMarkPaths( Res_Win_t * p )
{
Abc_Obj_t * pObj;
int i;
+ // mark the leaves
+ Abc_NtkIncrementTravId( p->pNode->pNtk );
Abc_NtkIncrementTravId( p->pNode->pNtk );
Vec_PtrForEachEntry( p->vLeaves, pObj, i )
- Res_WinSweepLeafTfo_rec( pObj, p->pNode->Level + p->nWinTfoMax, p->pNode );
+ Abc_NodeSetTravIdCurrent( pObj );
+ // traverse from the roots and mark the nodes that can reach leaves
+ // the nodes that do not reach leaves have previous trav ID
+ // the nodes that reach leaves have current trav ID
+ Vec_PtrForEachEntry( p->vRoots, pObj, i )
+ Res_WinMarkPaths_rec( pObj, p->pNode, p->nLevTravMin );
}
+
+
+
/**Function*************************************************************
Synopsis [Recursively collects the roots.]
@@ -185,29 +305,27 @@ void Res_WinSweepLeafTfo( Res_Win_t * p )
SeeAlso []
***********************************************************************/
-void Res_WinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
+void Res_WinFinalizeRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
{
Abc_Obj_t * pFanout;
int i;
assert( Abc_ObjIsNode(pObj) );
+ assert( Abc_NodeIsTravIdCurrent(pObj) );
// check if the node has all fanouts marked
Abc_ObjForEachFanout( pObj, pFanout, i )
if ( !Abc_NodeIsTravIdCurrent(pFanout) )
break;
- // if some of the fanouts are unmarked, add the node to the root
+ // if some of the fanouts are unmarked, add the node to the roots
if ( i < Abc_ObjFanoutNum(pObj) )
- {
Vec_PtrPushUnique( vRoots, pObj );
- return;
- }
- // otherwise, call recursively
- Abc_ObjForEachFanout( pObj, pFanout, i )
- Res_WinCollectRoots_rec( pFanout, vRoots );
+ else // otherwise, call recursively
+ Abc_ObjForEachFanout( pObj, pFanout, i )
+ Res_WinFinalizeRoots_rec( pFanout, vRoots );
}
/**Function*************************************************************
- Synopsis [Collects the roots of the window.]
+ Synopsis [Finalizes the roots of the window.]
Description [Roots of the window are the nodes that have at least
one fanout that it not in the TFO of the leaves.]
@@ -217,13 +335,21 @@ void Res_WinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
SeeAlso []
***********************************************************************/
-void Res_WinCollectRoots( Res_Win_t * p )
+int Res_WinFinalizeRoots( Res_Win_t * p )
{
assert( !Abc_NodeIsTravIdCurrent(p->pNode) );
+ // mark the node with the old traversal ID
+ Abc_NodeSetTravIdCurrent( p->pNode );
+ // recollect the roots
Vec_PtrClear( p->vRoots );
- Res_WinCollectRoots_rec( p->pNode, p->vRoots );
+ Res_WinFinalizeRoots_rec( p->pNode, p->vRoots );
+ assert( Vec_PtrSize(p->vRoots) > 0 );
+ if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode )
+ return 0;
+ return 1;
}
+
/**Function*************************************************************
Synopsis [Recursively adds missing nodes and leaves.]
@@ -235,23 +361,27 @@ void Res_WinCollectRoots( Res_Win_t * p )
SeeAlso []
***********************************************************************/
-void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj )
+void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj, int nLevTravMin )
{
Abc_Obj_t * pFanin;
int i;
- if ( pObj->fMarkA )
+ // skip the already collected leaves, nodes, and branches
+ if ( Abc_NodeIsTravIdCurrent(pObj) )
return;
- if ( !Abc_NodeIsTravIdCurrent(pObj) || (int)pObj->Level <= p->nLevLeaves )
+ // if this is not an internal node - make it a new branch
+ if ( !Abc_NodeIsTravIdPrevious(pObj) )
{
- p->nLeavesPlus++;
- Vec_PtrPush( p->vLeaves, pObj );
- pObj->fMarkA = 1;
+ Abc_NodeSetTravIdCurrent( pObj );
+ Vec_PtrPush( p->vBranches, pObj );
return;
}
- Res_WinAddNode( p, pObj );
+ assert( Abc_ObjIsNode(pObj) ); // if this is a CI, then the window is incorrect!
+ Abc_NodeSetTravIdCurrent( pObj );
// visit the fanins of the node
Abc_ObjForEachFanin( pObj, pFanin, i )
- Res_WinAddMissing_rec( p, pFanin );
+ Res_WinAddMissing_rec( p, pFanin, nLevTravMin );
+ // collect the node
+ Vec_PtrPush( p->vNodes, pObj );
}
/**Function*************************************************************
@@ -269,34 +399,25 @@ void Res_WinAddMissing( Res_Win_t * p )
{
Abc_Obj_t * pObj;
int i;
+ // mark the leaves
+ Abc_NtkIncrementTravId( p->pNode->pNtk );
+ Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+ Abc_NodeSetTravIdCurrent( pObj );
+ // mark the already collected nodes
+ Vec_PtrForEachEntry( p->vNodes, pObj, i )
+ Abc_NodeSetTravIdCurrent( pObj );
+ // explore from the roots
+ Vec_PtrClear( p->vBranches );
Vec_PtrForEachEntry( p->vRoots, pObj, i )
- Res_WinAddMissing_rec( p, pObj );
+ Res_WinAddMissing_rec( p, pObj, p->nLevTravMin );
}
-/**Function*************************************************************
-
- Synopsis [Unmarks the leaves and nodes of the window.]
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Res_WinUnmark( Res_Win_t * p )
-{
- Abc_Obj_t * pObj;
- int i, k;
- Vec_VecForEachEntry( p->vLevels, pObj, i, k )
- pObj->fMarkA = 0;
- Vec_PtrForEachEntry( p->vLeaves, pObj, i )
- pObj->fMarkA = 0;
-}
+
/**Function*************************************************************
- Synopsis [Verifies the window.]
+ Synopsis [Returns 1 if the window is trivial (without TFO).]
Description []
@@ -305,30 +426,9 @@ void Res_WinUnmark( Res_Win_t * p )
SeeAlso []
***********************************************************************/
-void Res_WinVerify( Res_Win_t * p )
+int Res_WinIsTrivial( Res_Win_t * p )
{
- Abc_Obj_t * pObj, * pFanin;
- int i, k, f;
- // make sure the nodes are not marked
- Abc_NtkForEachObj( p->pNode->pNtk, pObj, i )
- assert( !pObj->fMarkA );
- // mark the leaves
- Vec_PtrForEachEntry( p->vLeaves, pObj, i )
- pObj->fMarkA = 1;
- // make sure all nodes in the topological order have their fanins in the set
- Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves + 1, (int)p->pNode->Level + p->nWinTfoMax )
- {
- assert( (int)pObj->Level == i );
- assert( !pObj->fMarkA );
- Abc_ObjForEachFanin( pObj, pFanin, f )
- assert( pFanin->fMarkA );
- pObj->fMarkA = 1;
- }
- // make sure the roots are marked
- Vec_PtrForEachEntry( p->vRoots, pObj, i )
- assert( pObj->fMarkA );
- // unmark
- Res_WinUnmark( p );
+ return Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode;
}
/**Function*************************************************************
@@ -345,31 +445,29 @@ void Res_WinVerify( Res_Win_t * p )
int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p )
{
assert( Abc_ObjIsNode(pNode) );
- assert( nWinTfiMax > 0 && nWinTfoMax > 0 );
+ assert( nWinTfiMax > 0 && nWinTfiMax < 10 );
+ assert( nWinTfoMax >= 0 && nWinTfoMax < 10 );
+
// initialize the window
- p->pNode = pNode;
+ p->pNode = pNode;
p->nWinTfiMax = nWinTfiMax;
p->nWinTfoMax = nWinTfoMax;
- p->nLeavesPlus = 0;
- p->nLevLeaves = ABC_MAX( 0, ((int)p->pNode->Level) - p->nWinTfiMax - 1 );
- // collect the nodes in TFI cone of pNode above the level of leaves (p->nLevLeaves)
- Res_WinCollectNodeTfi( p );
- // find the leaves of the window
- Res_WinCollectLeaves( p );
- // mark the TFO of the collected nodes up to the given level (p->pNode->Level + p->nWinTfoMax)
- Res_WinSweepLeafTfo( p );
- // find the roots of the window
- Res_WinCollectRoots( p );
- // add the nodes in the TFI of the roots that are not yet in the window
- Res_WinAddMissing( p );
- // unmark window nodes
- Res_WinUnmark( p );
- // clear the divisor information
- p->nLevDivMax = 0;
- p->nDivsPlus = 0;
- Vec_PtrClear( p->vDivs );
- // verify the resulting window
-// Res_WinVerify( p );
+ Vec_PtrClear( p->vRoots );
+ Vec_PtrPush( p->vRoots, pNode );
+
+ // compute the leaves
+ Res_WinCollectLeavesAndNodes( p );
+
+ // compute the candidate roots
+ if ( p->nWinTfoMax > 0 && Res_WinComputeRoots(p) )
+ {
+ // mark the paths from the roots to the leaves
+ Res_WinMarkPaths( p );
+ // refine the roots and add branches and missing nodes
+ if ( Res_WinFinalizeRoots( p ) )
+ Res_WinAddMissing( p );
+ }
+
return 1;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 07:53:07 +0000