diff options
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 6 | ||||
-rw-r--r-- | src/base/abci/abcFx.c | 16 |
2 files changed, 15 insertions, 7 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3d7ea939..f65eaf85 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27436,7 +27436,7 @@ int Abc_CommandAbc9Fx( Abc_Frame_t * pAbc, int argc, char ** argv ) int fVeryVerbose = 0; // set the defaults Extra_UtilGetoptReset(); - while ( (c = Extra_UtilGetopt(argc, argv, "NMrvh")) != EOF ) + while ( (c = Extra_UtilGetopt(argc, argv, "NMrvwh")) != EOF ) { switch (c) { @@ -27468,6 +27468,9 @@ int Abc_CommandAbc9Fx( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'v': fVerbose ^= 1; break; + case 'w': + fVeryVerbose ^= 1; + break; case 'h': goto usage; break; @@ -27499,6 +27502,7 @@ usage: Abc_Print( -2, "\t-M <num> : upper bound on literal count of divisors to extract [default = %d]\n", LitCountMax ); Abc_Print( -2, "\t-r : reversing variable order during ISOP computation [default = %s]\n", fReverse? "yes": "no" ); Abc_Print( -2, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c index dd1128e9..1e2eba83 100644 --- a/src/base/abci/abcFx.c +++ b/src/base/abci/abcFx.c @@ -395,7 +395,7 @@ static inline int Fx_ManComputeLevelDiv( Fx_Man_t * p, Vec_Int_t * vCubeFree ) int i, Lit, Level = 0; Vec_IntForEachEntry( vCubeFree, Lit, i ) Level = Abc_MaxInt( Level, Vec_IntEntry(p->vLevels, Abc_Lit2Var(Abc_Lit2Var(Lit))) ); - return Abc_MinInt( Level, 200 ); + return Abc_MinInt( Level, 800 ); } static inline int Fx_ManComputeLevelCube( Fx_Man_t * p, Vec_Int_t * vCube ) { @@ -473,7 +473,7 @@ static inline void Fx_PrintDiv( Fx_Man_t * p, int iDiv ) int i; printf( "%4d : ", p->nDivs ); printf( "Div %7d : ", iDiv ); - printf( "Weight %5d ", (int)Vec_FltEntry(p->vWeights, iDiv) ); + printf( "Weight %12.5f ", Vec_FltEntry(p->vWeights, iDiv) ); // printf( "Compl %4d ", p->nCompls ); Fx_PrintDivOne( Hsh_VecReadEntry(p->pHash, iDiv) ); for ( i = Vec_IntSize(Hsh_VecReadEntry(p->pHash, iDiv)) + 3; i < 16; i++ ) @@ -503,6 +503,8 @@ static void Fx_PrintMatrix( Fx_Man_t * p ) Vec_Int_t * vCube; int i, v, Lit, nObjs; char * pLine; + if ( Vec_WecSize(p->vLits)/2 > 26 ) + return; printf( " " ); nObjs = Vec_WecSize(p->vLits)/2; for ( i = 0; i < Abc_MinInt(nObjs, 26); i++ ) @@ -794,7 +796,7 @@ int Fx_ManCubeSingleCubeDivisors( Fx_Man_t * p, Vec_Int_t * vPivot, int fRemove, { if ( Vec_FltSize(p->vWeights) == iDiv ) { - Vec_FltPush(p->vWeights, -2 -0.001 * Fx_ManComputeLevelDiv(p, p->vCubeFree)); + Vec_FltPush(p->vWeights, -2 + 0.9 - 0.001 * Fx_ManComputeLevelDiv(p, p->vCubeFree)); p->nDivsS++; } assert( iDiv < Vec_FltSize(p->vWeights) ); @@ -846,7 +848,7 @@ void Fx_ManCubeDoubleCubeDivisors( Fx_Man_t * p, int iFirst, Vec_Int_t * vPivot, if ( !fRemove ) { if ( iDiv == Vec_FltSize(p->vWeights) ) - Vec_FltPush(p->vWeights, -Vec_IntSize(p->vCubeFree) -0.001 * Fx_ManComputeLevelDiv(p, p->vCubeFree)); + Vec_FltPush(p->vWeights, -Vec_IntSize(p->vCubeFree) + 0.9 - 0.0009 * Fx_ManComputeLevelDiv(p, p->vCubeFree)); assert( iDiv < Vec_FltSize(p->vWeights) ); Vec_FltAddToEntry( p->vWeights, iDiv, Base + Vec_IntSize(p->vCubeFree) - 1 ); p->nPairsD++; @@ -884,7 +886,7 @@ void Fx_ManCreateDivisors( Fx_Man_t * p ) Fx_ManCubeDoubleCubeDivisors( p, i+1, vCube, 0, 0 ); // add - no update // create queue with all divisors p->vPrio = Vec_QueAlloc( Vec_FltSize(p->vWeights) ); - Vec_QueSetCosts( p->vPrio, Vec_FltArrayP(p->vWeights) ); + Vec_QueSetPriority( p->vPrio, Vec_FltArrayP(p->vWeights) ); Vec_FltForEachEntry( p->vWeights, Weight, i ) if ( Weight > 0.0 ) Vec_QuePush( p->vPrio, i ); @@ -985,6 +987,8 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) Vec_Int_t * vDiv = p->vDiv; int nLitsNew = p->nLits - (int)Vec_FltEntry(p->vWeights, iDiv); int i, k, Lit0, Lit1, iVarNew, RetValue, Level; + float Diff = Vec_FltEntry(p->vWeights, iDiv) - (float)((int)Vec_FltEntry(p->vWeights, iDiv)); + assert( Diff > 0.0 && Diff < 1.0 ); // get the divisor and select pivot variables p->nDivs++; @@ -1179,7 +1183,7 @@ int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitC Fx_PrintStats( p, Abc_Clock() - clk ); // perform extraction p->timeStart = Abc_Clock(); - for ( i = 0; i < nNewNodesMax && Vec_QueTopCost(p->vPrio) > 0.0; i++ ) + for ( i = 0; i < nNewNodesMax && Vec_QueTopPriority(p->vPrio) > 0.0; i++ ) { iDiv = Vec_QuePop(p->vPrio); if ( fVeryVerbose ) |