diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-30 13:33:39 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-30 13:33:39 -0700 |
commit | 846da1d2c73c5fe63f461ed1cfe6d0036cc521c9 (patch) | |
tree | 73e3d93ac479ecf7fdb681020fc39af0bbb25a4a /src/base/abci | |
parent | 3d5744f8477496fad439d31f2cc63ea2a3e31f37 (diff) | |
download | abc-846da1d2c73c5fe63f461ed1cfe6d0036cc521c9.tar.gz abc-846da1d2c73c5fe63f461ed1cfe6d0036cc521c9.tar.bz2 abc-846da1d2c73c5fe63f461ed1cfe6d0036cc521c9.zip |
Changing default values.
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abcFx.c | 56 |
1 files changed, 53 insertions, 3 deletions
diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c index aa021efe..f54a9cd2 100644 --- a/src/base/abci/abcFx.c +++ b/src/base/abci/abcFx.c @@ -95,6 +95,7 @@ struct Fx_Man_t_ Vec_Flt_t * vWeights; // divisor weights Vec_Que_t * vPrio; // priority queue for divisors by weight Vec_Int_t * vVarCube; // mapping ObjId into its first cube + Vec_Int_t * vLevels; // variable levels // temporary data to update the data-structure when a divisor is extracted Vec_Int_t * vCubesS; // single cubes for the given divisor Vec_Int_t * vCubesD; // cube pairs for the given divisor @@ -368,6 +369,7 @@ void Fx_ManStop( Fx_Man_t * p ) Vec_FltFree( p->vWeights ); Vec_QueFree( p->vPrio ); Vec_IntFree( p->vVarCube ); + Vec_IntFree( p->vLevels ); // temporary data Vec_IntFree( p->vCubesS ); Vec_IntFree( p->vCubesD ); @@ -379,6 +381,49 @@ void Fx_ManStop( Fx_Man_t * p ) /**Function************************************************************* + Synopsis [Compute levels of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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 ); +} +static inline int Fx_ManComputeLevelCube( Fx_Man_t * p, Vec_Int_t * vCube ) +{ + int k, Lit, Level = 0; + Vec_IntForEachEntryStart( vCube, Lit, k, 1 ) + Level = Abc_MaxInt( Level, Vec_IntEntry(p->vLevels, Abc_Lit2Var(Lit)) ); + return Level; +} +void Fx_ManComputeLevel( Fx_Man_t * p ) +{ + Vec_Int_t * vCube; + int i, iVar, iFirst = 0; + iVar = Vec_IntEntry( Vec_WecEntry(p->vCubes,0), 0 ); + p->vLevels = Vec_IntStart( p->nVars ); + Vec_WecForEachLevel( p->vCubes, vCube, i ) + { + Vec_IntUpdateEntry( p->vLevels, Vec_IntEntry(vCube, 0), Fx_ManComputeLevelCube(p, vCube) ); + if ( iVar == Vec_IntEntry(vCube, 0) ) + continue; + // add the number of cubes + Vec_IntAddToEntry( p->vLevels, iVar, i - iFirst ); + iVar = Vec_IntEntry(vCube, 0); + iFirst = i; + } +} + +/**Function************************************************************* + Synopsis [Printing procedures.] Description [] @@ -748,7 +793,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); + Vec_FltPush(p->vWeights, -2 -0.001 * Fx_ManComputeLevelDiv(p, p->vCubeFree)); p->nDivsS++; } assert( iDiv < Vec_FltSize(p->vWeights) ); @@ -800,7 +845,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)); + Vec_FltPush(p->vWeights, -Vec_IntSize(p->vCubeFree) -0.001 * Fx_ManComputeLevelDiv(p, p->vCubeFree)); assert( iDiv < Vec_FltSize(p->vWeights) ); Vec_FltAddToEntry( p->vWeights, iDiv, Base + Vec_IntSize(p->vCubeFree) - 1 ); p->nPairsD++; @@ -938,7 +983,7 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) Vec_Int_t * vCube, * vCube2, * vLitP, * vLitN; Vec_Int_t * vDiv = p->vDiv; int nLitsNew = p->nLits - (int)Vec_FltEntry(p->vWeights, iDiv); - int i, k, Lit0, Lit1, iVarNew, RetValue; + int i, k, Lit0, Lit1, iVarNew, RetValue, Level; // get the divisor and select pivot variables p->nDivs++; @@ -996,6 +1041,7 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) { Vec_IntPush( vCube, Abc_LitNot(Lit0) ); Vec_IntPush( vCube, Abc_LitNot(Lit1) ); + Level = 1 + Fx_ManComputeLevelCube( p, vCube ); } else { @@ -1003,7 +1049,10 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) vCube = Vec_WecEntry( p->vCubes, Vec_WecSize(p->vCubes) - 2 ); Vec_IntPush( vCube2, iVarNew ); Fx_ManDivAddLits( vCube, vCube2, vDiv ); + Level = 2 + Abc_MaxInt( Fx_ManComputeLevelCube(p, vCube), Fx_ManComputeLevelCube(p, vCube2) ); } + assert( Vec_IntSize(p->vLevels) == iVarNew ); + Vec_IntPush( p->vLevels, Level ); // do not add new cubes to the matrix p->nLits += Vec_IntSize( vDiv ); // create new literals @@ -1121,6 +1170,7 @@ int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitC p = Fx_ManStart( vCubes ); p->LitCountMax = LitCountMax; Fx_ManCreateLiterals( p, ObjIdMax ); + Fx_ManComputeLevel( p ); Fx_ManCreateDivisors( p ); if ( fVeryVerbose ) Fx_PrintMatrix( p ); |