summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaBalance.c7
-rw-r--r--src/base/abci/abcFx.c56
2 files changed, 57 insertions, 6 deletions
diff --git a/src/aig/gia/giaBalance.c b/src/aig/gia/giaBalance.c
index 32cba22c..6f1b615c 100644
--- a/src/aig/gia/giaBalance.c
+++ b/src/aig/gia/giaBalance.c
@@ -470,7 +470,8 @@ int Dam_ManDivSlack( Dam_Man_t * p, int iLit0, int iLit1, int LevR )
{
int Lev0 = Gia_ObjLevel(p->pGia, Gia_ManObj(p->pGia, Abc_Lit2Var(iLit0)));
int Lev1 = Gia_ObjLevel(p->pGia, Gia_ManObj(p->pGia, Abc_Lit2Var(iLit1)));
- return p->nLevelMax - LevR - Abc_MaxInt(Lev0, Lev1) - 1 - (int)(iLit0 > iLit1);
+ int Slack = p->nLevelMax - LevR - Abc_MaxInt(Lev0, Lev1) - 1 - (int)(iLit0 > iLit1);
+ return Abc_MinInt( Slack, 100 );
}
void Dam_ManCreateMultiRefs( Dam_Man_t * p, Vec_Int_t ** pvRefsAnd, Vec_Int_t ** pvRefsXor )
{
@@ -583,7 +584,7 @@ void Dam_ManCreatePairs( Dam_Man_t * p, int fVerbose )
Num = Hash_Int2ManInsert( p->vHash, Hash_IntObjData0(vHash, i), Hash_IntObjData1(vHash, i), 0 );
assert( Num == Hash_IntManEntryNum(p->vHash) );
assert( Num == Vec_FltSize(p->vCounts) );
- Vec_FltPush( p->vCounts, nRefs + 0.001*Dam_ManDivSlack(p, Hash_IntObjData0(vHash, i), Hash_IntObjData1(vHash, i), Vec_IntEntry(vLevRMax, i)) );
+ Vec_FltPush( p->vCounts, nRefs + 0.005*Dam_ManDivSlack(p, Hash_IntObjData0(vHash, i), Hash_IntObjData1(vHash, i), Vec_IntEntry(vLevRMax, i)) );
Vec_QuePush( p->vQue, Num );
// remember divisors
assert( Num == Vec_IntSize(p->vDiv2Nod) );
@@ -853,7 +854,7 @@ void Dam_ManUpdate( Dam_Man_t * p, int iDiv )
nRefs = Hash_IntObjData2(p->vHash, i);
if ( nRefs < 2 )
continue;
- Vec_FltWriteEntry( p->vCounts, i, nRefs + 0.0001*Dam_ManDivSlack(p, Hash_IntObjData0(p->vHash, i), Hash_IntObjData1(p->vHash, i), Vec_IntEntry(p->vDivLevR, i)) );
+ Vec_FltWriteEntry( p->vCounts, i, nRefs + 0.001*Dam_ManDivSlack(p, Hash_IntObjData0(p->vHash, i), Hash_IntObjData1(p->vHash, i), Vec_IntEntry(p->vDivLevR, i)) );
Vec_QuePush( p->vQue, i );
// remember divisors
Vec_IntWriteEntry( p->vDiv2Nod, i, Vec_IntSize(p->vNodStore) );
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 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 08:07:06 +0000