From 755935a6df4c84377aff1c67a5d802062cf925e6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 27 May 2013 13:34:22 -0700 Subject: Added switch -M to set max size of two-cube divisors to extract (often helps both runtime and quality). --- src/base/abci/abc.c | 26 +++++++++++++++++++------- src/base/abci/abcFx.c | 15 ++++++++++----- src/base/abci/abcFxu.c | 3 ++- src/opt/fxu/fxu.c | 10 +++++----- src/opt/fxu/fxu.h | 3 ++- 5 files changed, 38 insertions(+), 19 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c51c53c5..4493c361 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3582,14 +3582,14 @@ usage: ***********************************************************************/ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int fVerbose ); + extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int nLitCountMax, int fVerbose ); Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); Fxu_Data_t Params, * p = &Params; int c, fNewAlgo = 1; // set the defaults Abc_NtkSetDefaultParams( p ); Extra_UtilGetoptReset(); - while ( (c = Extra_UtilGetopt(argc, argv, "SDNWsdzcnvh")) != EOF ) + while ( (c = Extra_UtilGetopt(argc, argv, "SDNWMsdzcnvh")) != EOF ) { switch (c) { @@ -3632,9 +3632,20 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); goto usage; } - p->WeightMax = atoi(argv[globalUtilOptind]); + p->WeightMin = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( p->WeightMax < 0 ) + if ( p->WeightMin < 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; + } + p->LitCountMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( p->LitCountMax < 0 ) goto usage; break; case 's': @@ -3685,19 +3696,20 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) // the nodes to be merged are linked into the special linked list if ( fNewAlgo ) - Abc_NtkFxPerform( pNtk, p->nNodesExt, p->fVerbose ); + Abc_NtkFxPerform( pNtk, p->nNodesExt, p->LitCountMax, p->fVerbose ); else Abc_NtkFastExtract( pNtk, p ); Abc_NtkFxuFreeInfo( p ); return 0; usage: - Abc_Print( -2, "usage: fx [-SDNW ] [-sdzcnvh]\n"); + Abc_Print( -2, "usage: fx [-SDNWM ] [-sdzcnvh]\n"); Abc_Print( -2, "\t performs unate fast extract on the current network\n"); Abc_Print( -2, "\t-S : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax ); Abc_Print( -2, "\t-D : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax ); Abc_Print( -2, "\t-N : max number of divisors to extract during this run [default = %d]\n", p->nNodesExt ); - Abc_Print( -2, "\t-W : only extract divisors with weight more than this [default = %d]\n", p->WeightMax ); + Abc_Print( -2, "\t-W : lower bound on the weight of divisors to extract [default = %d]\n", p->WeightMin ); + Abc_Print( -2, "\t-M : upper bound on literal count of divisors to extract [default = %d]\n", p->LitCountMax ); Abc_Print( -2, "\t-s : use only single-cube divisors [default = %s]\n", p->fOnlyS? "yes": "no" ); Abc_Print( -2, "\t-d : use only double-cube divisors [default = %s]\n", p->fOnlyD? "yes": "no" ); Abc_Print( -2, "\t-z : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" ); diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c index 953f87f3..83136118 100644 --- a/src/base/abci/abcFx.c +++ b/src/base/abci/abcFx.c @@ -87,6 +87,7 @@ struct Fx_Man_t_ { // user's data Vec_Wec_t * vCubes; // cube -> lit + int LitCountMax;// max size of divisor to extract // internal data Vec_Wec_t * vLits; // lit -> cube Vec_Int_t * vCounts; // literal counts (currently not used) @@ -141,7 +142,6 @@ Vec_Wec_t * Abc_NtkFxRetrieve( Abc_Ntk_t * pNtk ) char * pCube, * pSop; int nVars, i, v, Lit; assert( Abc_NtkIsSopLogic(pNtk) ); - Abc_NtkMakeLegit( pNtk ); vCubes = Vec_WecAlloc( 1000 ); Abc_NtkForEachNode( pNtk, pNode, i ) { @@ -300,9 +300,9 @@ int Abc_NtkFxCheck( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int fVerbose ) +int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int LitCountMax, int fVerbose ) { - extern int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int fVerbose ); + extern int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fVerbose ); Vec_Wec_t * vCubes; assert( Abc_NtkIsSopLogic(pNtk) ); // check unique fanins @@ -314,10 +314,12 @@ int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int fVerbose ) // sweep removes useless nodes Abc_NtkCleanup( pNtk, 0 ); // Abc_NtkOrderFanins( pNtk ); + // makes sure the SOPs are SCC-free and D1C-free + Abc_NtkMakeLegit( pNtk ); // collect information about the covers vCubes = Abc_NtkFxRetrieve( pNtk ); // call the fast extract procedure - if ( Fx_FastExtract( vCubes, Abc_NtkObjNumMax(pNtk), nNewNodesMax, fVerbose ) > 0 ) + if ( Fx_FastExtract( vCubes, Abc_NtkObjNumMax(pNtk), nNewNodesMax, LitCountMax, fVerbose ) > 0 ) { // update the network Abc_NtkFxInsert( pNtk, vCubes ); @@ -792,6 +794,8 @@ void Fx_ManCubeDoubleCubeDivisors( Fx_Man_t * p, int iFirst, Vec_Int_t * vPivot, else p->nDivMux[2]++; } + if ( p->LitCountMax && p->LitCountMax < Vec_IntSize(p->vCubeFree) ) + continue; iDiv = Hsh_VecManAdd( p->pHash, p->vCubeFree ); if ( !fRemove ) { @@ -1107,7 +1111,7 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) SeeAlso [] ***********************************************************************/ -int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int fVerbose ) +int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fVerbose ) { int fVeryVerbose = 0; int i, iDiv; @@ -1115,6 +1119,7 @@ int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int fVer clock_t clk = clock(); // initialize the data-structure p = Fx_ManStart( vCubes ); + p->LitCountMax = LitCountMax; Fx_ManCreateLiterals( p, ObjIdMax ); Fx_ManCreateDivisors( p ); if ( fVeryVerbose ) diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c index b2a56a7d..b0106636 100644 --- a/src/base/abci/abcFxu.c +++ b/src/base/abci/abcFxu.c @@ -55,7 +55,8 @@ void Abc_NtkSetDefaultParams( Fxu_Data_t * p ) p->nSingleMax = 20000; p->nPairsMax = 30000; p->nNodesExt = 100000; - p->WeightMax = 0; + p->WeightMin = 0; + p->LitCountMax= 0; p->fOnlyS = 0; p->fOnlyD = 0; p->fUse0 = 0; diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c index 0095abf9..2b078120 100644 --- a/src/opt/fxu/fxu.c +++ b/src/opt/fxu/fxu.c @@ -83,7 +83,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle ); if ( pData->fVerbose ) printf( "Div %5d : Best single = %5d.%s", Counter++, Weight1, fScrollLines?"\n":"\r" ); - if ( Weight1 > pData->WeightMax || (Weight1 == 0 && pData->fUse0) ) + if ( Weight1 > pData->WeightMin || (Weight1 == 0 && pData->fUse0) ) Fxu_UpdateSingle( p ); else break; @@ -98,7 +98,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble ); if ( pData->fVerbose ) printf( "Div %5d : Best double = %5d.%s", Counter++, Weight2, fScrollLines?"\n":"\r" ); - if ( Weight2 > pData->WeightMax || (Weight2 == 0 && pData->fUse0) ) + if ( Weight2 > pData->WeightMin || (Weight2 == 0 && pData->fUse0) ) Fxu_UpdateDouble( p ); else break; @@ -119,14 +119,14 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) if ( Weight1 >= Weight2 ) { - if ( Weight1 > pData->WeightMax || (Weight1 == 0 && pData->fUse0) ) + if ( Weight1 > pData->WeightMin || (Weight1 == 0 && pData->fUse0) ) Fxu_UpdateSingle( p ); else break; } else { - if ( Weight2 > pData->WeightMax || (Weight2 == 0 && pData->fUse0) ) + if ( Weight2 > pData->WeightMin || (Weight2 == 0 && pData->fUse0) ) Fxu_UpdateDouble( p ); else break; @@ -148,7 +148,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) printf( "Div %5d : Best double = %5d. Best single = %5d. Best complement = %5d.%s", Counter++, Weight2, Weight1, Weight3, fScrollLines?"\n":"\r" ); - if ( Weight3 > pData->WeightMax || (Weight3 == 0 && pData->fUse0) ) + if ( Weight3 > pData->WeightMin || (Weight3 == 0 && pData->fUse0) ) Fxu_Update( p, pSingle, pDouble ); else break; diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h index 3c6384dc..e8ef6586 100644 --- a/src/opt/fxu/fxu.h +++ b/src/opt/fxu/fxu.h @@ -53,7 +53,8 @@ struct FxuDataStruct int nNodesExt; // the number of divisors to extract int nSingleMax; // the max number of single-cube divisors to consider int nPairsMax; // the max number of double-cube divisors to consider - int WeightMax; // the max weight of a divisor to extract + int WeightMin; // the min weight of a divisor to extract + int LitCountMax; // the max literal count of a divisor to consider // the input information Vec_Ptr_t * vSops; // the SOPs for each node in the network Vec_Ptr_t * vFanins; // the fanins of each node in the network -- cgit v1.2.3