diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 608d676f0..5cf7a0f59 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -878,7 +878,7 @@ extern ABC_DLL void Abc_NodeMffcConeSupp( Abc_Obj_t * pNode, Vec_P extern ABC_DLL int Abc_NodeDeref_rec( Abc_Obj_t * pNode ); extern ABC_DLL int Abc_NodeRef_rec( Abc_Obj_t * pNode ); /*=== abcRefactor.c ==========================================================*/ -extern ABC_DLL int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose ); +extern ABC_DLL int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nMinSaved, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose ); /*=== abcRewrite.c ==========================================================*/ extern ABC_DLL int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable ); /*=== abcSat.c ==========================================================*/ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index af80744bd..4ff6088b1 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7464,22 +7464,24 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pDup; int c, RetValue; int nNodeSizeMax; + int nMinSaved; int nConeSizeMax; int fUpdateLevel; int fUseZeros; int fUseDcs; int fVerbose; - extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose ); + extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nMinSaved, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose ); // set defaults nNodeSizeMax = 10; + nMinSaved = 1; nConeSizeMax = 16; fUpdateLevel = 1; fUseZeros = 0; fUseDcs = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Nlzvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "NMClzvh" ) ) != EOF ) { switch ( c ) { @@ -7494,6 +7496,17 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nNodeSizeMax < 0 ) goto usage; break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + nMinSaved = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nMinSaved < 0 ) + goto usage; + break; case 'C': if ( globalUtilOptind >= argc ) { @@ -7523,6 +7536,10 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } + if ( fUseZeros ) + nMinSaved = 0; + if ( nMinSaved == 0 ) + fUseZeros = 1; if ( pNtk == NULL ) { @@ -7553,7 +7570,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) // modify the current network pDup = Abc_NtkDup( pNtk ); - RetValue = Abc_NtkRefactor( pNtk, nNodeSizeMax, nConeSizeMax, fUpdateLevel, fUseZeros, fUseDcs, fVerbose ); + RetValue = Abc_NtkRefactor( pNtk, nNodeSizeMax, nMinSaved, nConeSizeMax, fUpdateLevel, fUseZeros, fUseDcs, fVerbose ); if ( RetValue == -1 ) { Abc_FrameReplaceCurrentNetwork( pAbc, pDup ); @@ -7571,9 +7588,10 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: refactor [-N ] [-lzvh]\n" ); + Abc_Print( -2, "usage: refactor [-NM ] [-lzvh]\n" ); Abc_Print( -2, "\t performs technology-independent refactoring of the AIG\n" ); Abc_Print( -2, "\t-N : the max support of the collapsed node [default = %d]\n", nNodeSizeMax ); + Abc_Print( -2, "\t-M : the min number of nodes saved after one step (0 <= num) [default = %d]\n", nMinSaved ); // Abc_Print( -2, "\t-C : the max support of the containing cone [default = %d]\n", nConeSizeMax ); Abc_Print( -2, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); Abc_Print( -2, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" ); @@ -7701,22 +7719,24 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv ) int nCutsMax; int nNodesMax; int nLevelsOdc; + int nMinSaved; int fUpdateLevel; int fUseZeros; int fVerbose; int fVeryVerbose; - extern int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutsMax, int nNodesMax, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose ); + extern int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutsMax, int nNodesMax, int nMinSaved, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose ); // set defaults nCutsMax = 8; nNodesMax = 1; nLevelsOdc = 0; + nMinSaved = 1; fUpdateLevel = 1; fUseZeros = 0; fVerbose = 0; fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KNFlzvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KNMFlzvwh" ) ) != EOF ) { switch ( c ) { @@ -7742,6 +7762,17 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nNodesMax < 0 ) goto usage; break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + nMinSaved = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nMinSaved < 0 ) + goto usage; + break; case 'F': if ( globalUtilOptind >= argc ) { @@ -7771,6 +7802,10 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } + if ( fUseZeros ) + nMinSaved = 0; + if ( nMinSaved == 0 ) + fUseZeros = 1; if ( pNtk == NULL ) { @@ -7799,7 +7834,7 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv ) } // modify the current network - if ( !Abc_NtkResubstitute( pNtk, nCutsMax, nNodesMax, nLevelsOdc, fUpdateLevel, fVerbose, fVeryVerbose ) ) + if ( !Abc_NtkResubstitute( pNtk, nCutsMax, nNodesMax, nMinSaved, nLevelsOdc, fUpdateLevel, fVerbose, fVeryVerbose ) ) { Abc_Print( -1, "Refactoring has failed.\n" ); return 1; @@ -7807,10 +7842,11 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: resub [-KN ] [-lzvwh]\n" ); + Abc_Print( -2, "usage: resub [-KNMF ] [-lzvwh]\n" ); Abc_Print( -2, "\t performs technology-independent restructuring of the AIG\n" ); Abc_Print( -2, "\t-K : the max cut size (%d <= num <= %d) [default = %d]\n", RS_CUT_MIN, RS_CUT_MAX, nCutsMax ); Abc_Print( -2, "\t-N : the max number of nodes to add (0 <= num <= 3) [default = %d]\n", nNodesMax ); + Abc_Print( -2, "\t-M : the min number of nodes saved after one step (0 <= num) [default = %d]\n", nMinSaved ); Abc_Print( -2, "\t-F : the number of fanout levels for ODC computation [default = %d]\n", nLevelsOdc ); Abc_Print( -2, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); Abc_Print( -2, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" ); @@ -14788,7 +14824,7 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Dar_ManDefaultRwrParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CNflzrvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CNMflzrvwh" ) ) != EOF ) { switch ( c ) { @@ -14814,6 +14850,17 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nSubgMax < 0 ) goto usage; break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMinSaved = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nMinSaved < 0 ) + goto usage; + break; case 'f': pPars->fFanout ^= 1; break; @@ -14838,6 +14885,10 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } + if ( pPars->fUseZeros ) + pPars->nMinSaved = 0; + if ( pPars->nMinSaved == 0 ) + pPars->fUseZeros = 1; if ( pNtk == NULL ) { Abc_Print( -1, "Empty network.\n" ); @@ -14859,10 +14910,11 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: drw [-C num] [-N num] [-lfzrvwh]\n" ); + Abc_Print( -2, "usage: drw [-C num] [-NM num] [-lfzrvwh]\n" ); Abc_Print( -2, "\t performs combinational AIG rewriting\n" ); Abc_Print( -2, "\t-C num : the max number of cuts at a node [default = %d]\n", pPars->nCutsMax ); Abc_Print( -2, "\t-N num : the max number of subgraphs tried [default = %d]\n", pPars->nSubgMax ); + Abc_Print( -2, "\t-M num : the min number of nodes saved after one step (0 <= num) [default = %d]\n", pPars->nMinSaved ); Abc_Print( -2, "\t-l : toggle preserving the number of levels [default = %s]\n", pPars->fUpdateLevel? "yes": "no" ); Abc_Print( -2, "\t-f : toggle representing fanouts [default = %s]\n", pPars->fFanout? "yes": "no" ); Abc_Print( -2, "\t-z : toggle using zero-cost replacements [default = %s]\n", pPars->fUseZeros? "yes": "no" ); diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 504ec477e..ac526a90d 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -557,7 +557,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars ) pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp ); Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); - Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); + Abc_NtkRefactor( pNtk, 10, 1, 16, 0, 0, 0, 0 ); //printf( "After rwsat = %d. ", Abc_NtkNodeNum(pNtk) ); //ABC_PRT( "Time", Abc_Clock() - clk ); } diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c index b14c08273..c95b66863 100644 --- a/src/base/abci/abcProve.c +++ b/src/base/abci/abcProve.c @@ -34,7 +34,7 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose ); +extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nMinSaved, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose ); extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, ABC_INT64_T nInspLimit, int * pRetValue, int * pNumFails, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects ); @@ -151,7 +151,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars ) break; if ( --Counter == 0 ) break; - Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); + Abc_NtkRefactor( pNtk, 10, 1, 16, 0, 0, 0, 0 ); if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) break; if ( --Counter == 0 ) @@ -340,7 +340,7 @@ Abc_Ntk_t * Abc_NtkMiterRwsat( Abc_Ntk_t * pNtk ) Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp ); Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); - Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); + Abc_NtkRefactor( pNtk, 10, 1, 16, 0, 0, 0, 0 ); return pNtk; } diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c index 02f7b8384..858dcabef 100644 --- a/src/base/abci/abcQuant.c +++ b/src/base/abci/abcQuant.c @@ -51,14 +51,14 @@ void Abc_NtkSynthesize( Abc_Ntk_t ** ppNtk, int fMoreEffort ) pNtk = *ppNtk; Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); - Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); + Abc_NtkRefactor( pNtk, 10, 1, 16, 0, 0, 0, 0 ); pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp ); if ( fMoreEffort ) { Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); - Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); + Abc_NtkRefactor( pNtk, 10, 1, 16, 0, 0, 0, 0 ); pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp ); diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c index 8ec5944fa..ec6756aa1 100644 --- a/src/base/abci/abcRefactor.c +++ b/src/base/abci/abcRefactor.c @@ -149,7 +149,7 @@ int Abc_NodeConeIsConst1( word * pTruth, int nVars ) SeeAlso [] ***********************************************************************/ -Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose ) +Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, int nMinSaved, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose ) { extern int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax ); int fVeryVerbose = 0; @@ -205,7 +205,8 @@ clk = Abc_Clock(); nNodesAdded = Dec_GraphToNetworkCount( pNode, pFForm, nNodesSaved, Required ); p->timeEval += Abc_Clock() - clk; // quit if there is no improvement - if ( nNodesAdded == -1 || (nNodesAdded == nNodesSaved && !fUseZeros) ) + //if ( nNodesAdded == -1 || (nNodesAdded == nNodesSaved && !fUseZeros) ) + if ( nNodesAdded == -1 || nNodesSaved - nNodesAdded < nMinSaved ) { Dec_GraphFree( pFForm ); return NULL; @@ -323,7 +324,7 @@ void Abc_NtkManRefPrintStats( Abc_ManRef_t * p ) SeeAlso [] ***********************************************************************/ -int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose ) +int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nMinSaved, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose ) { extern int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain ); ProgressBar * pProgress; @@ -371,7 +372,7 @@ clk = Abc_Clock(); pManRef->timeCut += Abc_Clock() - clk; // evaluate this cut clk = Abc_Clock(); - pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUpdateLevel, fUseZeros, fUseDcs, fVerbose ); + pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, nMinSaved, fUpdateLevel, fUseZeros, fUseDcs, fVerbose ); pManRef->timeRes += Abc_Clock() - clk; if ( pFForm == NULL ) continue; diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c index dc1b60368..2b28e7cc7 100644 --- a/src/base/abci/abcResub.c +++ b/src/base/abci/abcResub.c @@ -134,7 +134,7 @@ extern abctime s_ResubTime; SeeAlso [] ***********************************************************************/ -int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose ) +int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nMinSaved, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose ) { extern int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain ); ProgressBar * pProgress; @@ -214,6 +214,11 @@ clk = Abc_Clock(); pManRes->timeRes += Abc_Clock() - clk; if ( pFForm == NULL ) continue; + if ( pManRes->nLastGain < nMinSaved ) + { + Dec_GraphFree( pFForm ); + continue; + } pManRes->nTotalGain += pManRes->nLastGain; /* if ( pManRes->nLeaves == 4 && pManRes->nMffc == 2 && pManRes->nLastGain == 1 ) diff --git a/src/opt/dar/dar.h b/src/opt/dar/dar.h index ed1f4e743..4faee320c 100644 --- a/src/opt/dar/dar.h +++ b/src/opt/dar/dar.h @@ -46,6 +46,7 @@ struct Dar_RwrPar_t_ { int nCutsMax; // the maximum number of cuts to try int nSubgMax; // the maximum number of subgraphs to try + int nMinSaved; // the minumum number of nodes saved int fFanout; // support fanout representation int fUpdateLevel; // update level int fUseZeros; // performs zero-cost replacement diff --git a/src/opt/dar/darCore.c b/src/opt/dar/darCore.c index 24e5a7419..9d877699a 100644 --- a/src/opt/dar/darCore.c +++ b/src/opt/dar/darCore.c @@ -53,6 +53,7 @@ void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars ) memset( pPars, 0, sizeof(Dar_RwrPar_t) ); pPars->nCutsMax = 8; // 8 pPars->nSubgMax = 5; // 5 is a "magic number" + pPars->nMinSaved = 1; pPars->fFanout = 1; pPars->fUpdateLevel = 0; pPars->fUseZeros = 0; @@ -177,7 +178,8 @@ p->timeCuts += Abc_Clock() - clk; pCut->nLeaves = nLeavesOld; } // check the best gain - if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) ) + //if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) ) + if ( p->GainBest < p->pPars->nMinSaved ) { // Aig_ObjOrderAdvance( pAig ); continue;