From a762c695d7c0d953d644c0c77a2948d378d0d624 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 5 May 2013 01:54:11 -0700 Subject: New fast extract. --- src/base/abc/abcMinBase.c | 2 +- src/base/abci/abcFx.c | 750 +++++++++++++++++++++++++++++++++------------- src/base/abci/abcFxu.c | 4 +- src/bool/kit/kitSop.c | 4 +- src/misc/vec/vecInt.h | 99 +++++- src/misc/vec/vecQue.h | 11 +- src/misc/vec/vecWec.h | 95 +++++- src/opt/fxu/fxu.c | 2 +- src/opt/fxu/fxuPair.c | 6 +- src/opt/fxu/fxuSelect.c | 2 +- 10 files changed, 749 insertions(+), 226 deletions(-) diff --git a/src/base/abc/abcMinBase.c b/src/base/abc/abcMinBase.c index 7f43e24f..1c913eea 100644 --- a/src/base/abc/abcMinBase.c +++ b/src/base/abc/abcMinBase.c @@ -104,7 +104,7 @@ int Abc_NodeMinimumBase( Abc_Obj_t * pNode ) /**Function************************************************************* - Synopsis [Makes nodes of the network fanin-dup-ABC_FREE.] + Synopsis [Makes nodes of the network fanin-dup-free.] Description [Returns the number of pairs of duplicated fanins.] diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c index 69cfb352..0d58ac9e 100644 --- a/src/base/abci/abcFx.c +++ b/src/base/abci/abcFx.c @@ -6,7 +6,7 @@ PackageName [Network and node package.] - Synopsis [Interface with the fast extract package.] + Synopsis [Interface with the fast_extract package.] Author [Alan Mishchenko] @@ -219,7 +219,7 @@ void Abc_NtkFxInsert( Abc_Ntk_t * pNtk, Vec_Wec_t * vCubes ) } pCube += Abc_ObjFaninNum(pNode) + 3; } - if ( Abc_SopIsComplement((char *)pNode->pData) ) + if ( pNode->pData && Abc_SopIsComplement((char *)pNode->pData) ) Abc_SopComplement( pSop ); pNode->pData = pSop; // clean fanins @@ -302,20 +302,36 @@ int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int fVerbose ) typedef struct Fx_Man_t_ Fx_Man_t; struct Fx_Man_t_ { - int nVars; // original problem variables - int nPairsS; // number of lit pairs - int nPairsD; // number of cube pairs - int nDivsS; // single cube divisors - Vec_Wec_t * vCubes; // cube -> lit (user data) - Vec_Wec_t * vLits; // lit -> cube - Vec_Int_t * vCounts; // literal counts - Hsh_VecMan_t * pHash; // divisors - Vec_Flt_t * vWeights;// divisor weights - Vec_Que_t * vPrio; // priority queue - // temporary variables - Vec_Int_t * vCube; + Vec_Wec_t * vCubes; // cube -> lit (user data) + Vec_Wec_t * vLits; // lit -> cube + Vec_Int_t * vCounts; // literal counts + Hsh_VecMan_t * pHash; // divisors + Vec_Flt_t * vWeights; // divisor weights + Vec_Que_t * vPrio; // priority queue + Vec_Int_t * vVarCube; // mapping var into its first cube + // temporary arrays used for updating + Vec_Int_t * vCubesS; // single cube divisors + Vec_Int_t * vCubesD; // double cube divisors + Vec_Int_t * vPart0; // cubes of given literal + Vec_Int_t * vPart1; // cubes of given literal + Vec_Int_t * vFree; // cube-free divisor + Vec_Int_t * vCube; // one cube + Vec_Int_t * vDiv; // divisor + // statistics + int nVars; // original problem variables + int nLits; // the number of SOP literals + int nPairsS; // number of lit pairs + int nPairsD; // number of cube pairs + int nDivsS; // single cube divisors }; +static inline int Fx_ManGetFirstVarCube( Fx_Man_t * p, Vec_Int_t * vCube ) { return Vec_IntEntry( p->vVarCube, Vec_IntEntry(vCube, 0) ); } + +#define Fx_ManForEachCubeVec( vVec, vCubes, vCube, i ) \ + for ( i = 0; (i < Vec_IntSize(vVec)) && ((vCube) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i))); i++ ) +#define Fx_ManForEachPairVec( vVec, vCubes, vCube1, vCube2, i ) \ + for ( i = 0; (i+1 < Vec_IntSize(vVec)) && ((vCube) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i))) && ((vCube2) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i+1))); i += 2 ) + /**Function************************************************************* Synopsis [Create literals.] @@ -378,6 +394,92 @@ int Fx_ManDivCanonicize( Vec_Int_t * vFree ) // return 1 if complemented return 0; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline char Fx_PrintDivLit( int Lit ) { return (Abc_LitIsCompl(Lit) ? 'A' : 'a') + Abc_Lit2Var(Lit); } +static inline void Fx_PrintDivOne( Vec_Int_t * vDiv ) +{ + int i, Lit; + Vec_IntForEachEntry( vDiv, Lit, i ) + if ( !Abc_LitIsCompl(Lit) ) + printf( "%c", Fx_PrintDivLit(Abc_Lit2Var(Lit)) ); + printf( " + " ); + Vec_IntForEachEntry( vDiv, Lit, i ) + if ( Abc_LitIsCompl(Lit) ) + printf( "%c", Fx_PrintDivLit(Abc_Lit2Var(Lit)) ); +} +static inline void Fx_PrintDiv( Fx_Man_t * p, int iDiv ) +{ + printf( "Div %6d : ", iDiv ); + printf( "Cost %4d ", (int)Vec_FltEntry(p->vWeights, iDiv) ); + Fx_PrintDivOne( Hsh_VecReadEntry(p->pHash, iDiv) ); + printf( "\n" ); +} +static void Fx_PrintDivisors( Fx_Man_t * p ) +{ + int iDiv; + for ( iDiv = 0; iDiv < Vec_FltSize(p->vWeights); iDiv++ ) + Fx_PrintDiv( p, iDiv ); +} +static void Fx_PrintLiterals( Fx_Man_t * p ) +{ + Vec_Int_t * vTemp; + int i; + Vec_WecForEachLevel( p->vLits, vTemp, i ) + { + printf( "%c : ", Fx_PrintDivLit(i) ); + Vec_IntPrint( vTemp ); + } +} +static void Fx_PrintMatrix( Fx_Man_t * p ) +{ + Vec_Int_t * vCube; + int i, v, Lit, nObjs; + char * pLine; + printf( " " ); + nObjs = Vec_WecSize(p->vLits)/2; + for ( i = 0; i < Abc_MinInt(nObjs, 26); i++ ) + printf( "%c", 'a' + i ); + printf( "\n" ); + pLine = ABC_CALLOC( char, nObjs+1 ); + Vec_WecForEachLevel( p->vCubes, vCube, i ) + { + if ( Vec_IntSize(vCube) == 0 ) + continue; + memset( pLine, '-', nObjs ); + Vec_IntForEachEntryStart( vCube, Lit, v, 1 ) + { + assert( Abc_Lit2Var(Lit) < nObjs ); + pLine[Abc_Lit2Var(Lit)] = Abc_LitIsCompl(Lit) ? '0' : '1'; + } + printf( "%6d : %s %4d\n", i, pLine, Vec_IntEntry(vCube, 0) ); + } + ABC_FREE( pLine ); + Fx_PrintLiterals( p ); + Fx_PrintDivisors( p ); +} +static void Fx_PrintStats( Fx_Man_t * p, clock_t clk ) +{ + printf( "Cubes =%6d ", Vec_WecSizeUsed(p->vCubes) ); + printf( "Lits =%6d ", Vec_WecSizeUsed(p->vLits) ); + printf( "Divs =%6d ", Hsh_VecSize(p->pHash) ); + printf( "Divs+ =%6d ", Vec_QueSize(p->vPrio) ); + printf( "DivsS =%6d ", p->nDivsS ); + printf( "PairS =%6d ", p->nPairsS ); + printf( "PairD =%6d ", p->nPairsD ); + Abc_PrintTime( 1, "Time", clk ); +// printf( "\n" ); +} + /**Function************************************************************* Synopsis [] @@ -414,7 +516,7 @@ int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vFr Vec_IntPush( vFree, Abc_Var2Lit(*pBeg1++, fAttr0) ); while ( pBeg2 < pEnd2 ) Vec_IntPush( vFree, Abc_Var2Lit(*pBeg2++, fAttr1) ); - assert( Vec_IntSize(vFree) > 1 ); + assert( Vec_IntSize(vFree) > 1 ); // the cover is not SCC-free assert( !Abc_LitIsCompl(Vec_IntEntry(vFree, 0)) ); return Counter; } @@ -430,100 +532,49 @@ int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vFr SeeAlso [] ***********************************************************************/ -Vec_Wec_t * Fx_ManCreateLiterals( Vec_Wec_t * vCubes, Vec_Int_t ** pvCounts ) +static inline void Fx_ManDivFindPivots( Vec_Int_t * vDiv, int * pLit0, int * pLit1 ) { - Vec_Wec_t * vLits; - Vec_Int_t * vCube, * vCounts; - int i, k, Count, Lit, LitMax = 0; - // find max literal - Vec_WecForEachLevel( vCubes, vCube, i ) - Vec_IntForEachEntry( vCube, Lit, k ) - LitMax = Abc_MaxInt( LitMax, Lit ); - // count literals - vCounts = Vec_IntStart( LitMax + 2 ); - Vec_WecForEachLevel( vCubes, vCube, i ) - Vec_IntForEachEntryStart( vCube, Lit, k, 1 ) - Vec_IntAddToEntry( vCounts, Lit, 1 ); - // start literals - vLits = Vec_WecStart( 2 * LitMax ); - Vec_IntForEachEntry( vCounts, Count, Lit ) - Vec_IntGrow( Vec_WecEntry(vLits, Lit), Count ); - // fill out literals - Vec_WecForEachLevel( vCubes, vCube, i ) - Vec_IntForEachEntryStart( vCube, Lit, k, 1 ) - Vec_WecPush( vLits, Lit, i ); - *pvCounts = vCounts; - return vLits; -} -Hsh_VecMan_t * Fx_ManCreateDivisors( Vec_Wec_t * vCubes, Vec_Flt_t ** pvWeights, int * pnPairsS, int * pnPairsD, int * pnDivsS ) -{ - Hsh_VecMan_t * p; - Vec_Flt_t * vWeights; - Vec_Int_t * vCube, * vCube2, * vFree; - int i, k, n, Lit, Lit2, iDiv, Base; - p = Hsh_VecManStart( 10000 ); - vWeights = Vec_FltAlloc( 10000 ); - vFree = Vec_IntAlloc( 100 ); - // create two-literal divisors - Vec_WecForEachLevel( vCubes, vCube, i ) - Vec_IntForEachEntryStart( vCube, Lit, k, 1 ) - Vec_IntForEachEntryStart( vCube, Lit2, n, k+1 ) - { - assert( Lit < Lit2 ); - Vec_IntClear( vFree ); - Vec_IntPush( vFree, Abc_Var2Lit(Abc_LitNot(Lit), 0) ); - Vec_IntPush( vFree, Abc_Var2Lit(Abc_LitNot(Lit2), 1) ); - iDiv = Hsh_VecManAdd( p, vFree ); - if ( Vec_FltSize(vWeights) == iDiv ) - Vec_FltPush(vWeights, -2); - assert( iDiv < Vec_FltSize(vWeights) ); - Vec_FltAddToEntry( vWeights, iDiv, 1 ); - (*pnPairsS)++; - } - *pnDivsS = Vec_FltSize(vWeights); - // create two-cube divisors - Vec_WecForEachLevel( vCubes, vCube, i ) + int i, Lit; + *pLit0 = -1; + *pLit1 = -1; + Vec_IntForEachEntry( vDiv, Lit, i ) { - Vec_WecForEachLevelStart( vCubes, vCube2, k, i+1 ) - if ( Vec_IntEntry(vCube, 0) == Vec_IntEntry(vCube2, 0) ) - { -// extern void Fx_PrintDivOne( Vec_Int_t * p ); - Base = Fx_ManDivFindCubeFree( vCube, vCube2, vFree ); -// printf( "Cubes %2d %2d : ", i, k ); -// Fx_PrintDivOne( vFree ); printf( "\n" ); - -// if ( Vec_IntSize(vFree) == 4 ) -// Fx_ManDivCanonicize( vFree ); - iDiv = Hsh_VecManAdd( p, vFree ); - if ( Vec_FltSize(vWeights) == iDiv ) - Vec_FltPush(vWeights, -Vec_IntSize(vFree)); - assert( iDiv < Vec_FltSize(vWeights) ); - Vec_FltAddToEntry( vWeights, iDiv, Base + Vec_IntSize(vFree) - 1 ); - (*pnPairsD)++; - } - else - break; + if ( Abc_LitIsCompl(Lit) ) + { + if ( *pLit1 == -1 ) + *pLit1 = Abc_Lit2Var(Lit); + } + else + { + if ( *pLit0 == -1 ) + *pLit0 = Abc_Lit2Var(Lit); + } + if ( *pLit0 >= 0 && *pLit1 >= 0 ) + return; } - Vec_IntFree( vFree ); - *pvWeights = vWeights; - return p; } -Vec_Que_t * Fx_ManCreateQueue( Vec_Flt_t * vWeights ) +static inline int Fx_ManDivRemoveLits( Vec_Int_t * vCube, Vec_Int_t * vDiv ) { - Vec_Que_t * p; - float Weight; - int i; - p = Vec_QueAlloc( Vec_FltSize(vWeights) ); - Vec_QueSetCosts( p, Vec_FltArray(vWeights) ); - Vec_FltForEachEntry( vWeights, Weight, i ) - if ( Weight > 0.0 ) - Vec_QuePush( p, i ); - return p; + int i, Lit, Count = 0; + Vec_IntForEachEntry( vDiv, Lit, i ) + Count += Vec_IntRemove1( vCube, Abc_Lit2Var(Lit) ); + return Count; +} +static inline void Fx_ManDivAddLits( Vec_Int_t * vCube, Vec_Int_t * vCube2, Vec_Int_t * vDiv ) +{ + int i, Lit; +// Vec_IntClear( vCube ); +// Vec_IntClear( vCube2 ); + Vec_IntForEachEntry( vDiv, Lit, i ) + if ( Abc_LitIsCompl(Lit) ) + Vec_IntPush( vCube2, Abc_Lit2Var(Lit) ); + else + Vec_IntPush( vCube, Abc_Lit2Var(Lit) ); } /**Function************************************************************* - Synopsis [Removes 0-size cubes and sorts them by the first entry.] + Synopsis [] Description [] @@ -532,50 +583,162 @@ Vec_Que_t * Fx_ManCreateQueue( Vec_Flt_t * vWeights ) SeeAlso [] ***********************************************************************/ -void Vec_WecSortSpecial( Vec_Wec_t * vCubes ) +void Fx_ManCreateLiterals( Fx_Man_t * p, int nVars ) { Vec_Int_t * vCube; - int i, k = 0; - Vec_WecForEachLevel( vCubes, vCube, i ) - if ( Vec_IntSize(vCube) > 0 ) - vCubes->pArray[k++] = *vCube; + int i, k, Lit, Count; + // find the number of variables + p->nVars = p->nLits = 0; + Vec_WecForEachLevel( p->vCubes, vCube, i ) + { + assert( Vec_IntSize(vCube) > 0 ); + p->nVars = Abc_MaxInt( p->nVars, Vec_IntEntry(vCube, 0) ); + p->nLits += Vec_IntSize(vCube) - 1; + Vec_IntForEachEntryStart( vCube, Lit, k, 1 ) + p->nVars = Abc_MaxInt( p->nVars, Abc_Lit2Var(Lit) ); + } +// p->nVars++; + assert( p->nVars < nVars ); + p->nVars = nVars; + // count literals + p->vCounts = Vec_IntStart( 2*p->nVars ); + Vec_WecForEachLevel( p->vCubes, vCube, i ) + Vec_IntForEachEntryStart( vCube, Lit, k, 1 ) + Vec_IntAddToEntry( p->vCounts, Lit, 1 ); + // start literals + p->vLits = Vec_WecStart( 2*p->nVars ); + Vec_IntForEachEntry( p->vCounts, Count, Lit ) + Vec_IntGrow( Vec_WecEntry(p->vLits, Lit), Count ); + // fill out literals + Vec_WecForEachLevel( p->vCubes, vCube, i ) + Vec_IntForEachEntryStart( vCube, Lit, k, 1 ) + Vec_WecPush( p->vLits, Lit, i ); + // create mapping of variable into the first cube + p->vVarCube = Vec_IntStartFull( p->nVars ); + Vec_WecForEachLevel( p->vCubes, vCube, i ) + if ( Vec_IntEntry(p->vVarCube, Vec_IntEntry(vCube, 0)) == -1 ) + Vec_IntWriteEntry( p->vVarCube, Vec_IntEntry(vCube, 0), i ); +} +int Fx_ManCubeSingleCubeDivisors( Fx_Man_t * p, Vec_Int_t * vPivot, int fRemove, int fUpdate ) +{ + int k, n, Lit, Lit2, iDiv; + if ( Vec_IntSize(vPivot) < 2 ) + return 0; + Vec_IntForEachEntryStart( vPivot, Lit, k, 1 ) + Vec_IntForEachEntryStart( vPivot, Lit2, n, k+1 ) + { + assert( Lit < Lit2 ); + Vec_IntClear( p->vFree ); + Vec_IntPush( p->vFree, Abc_Var2Lit(Abc_LitNot(Lit), 0) ); + Vec_IntPush( p->vFree, Abc_Var2Lit(Abc_LitNot(Lit2), 1) ); + iDiv = Hsh_VecManAdd( p->pHash, p->vFree ); + if ( !fRemove ) + { + if ( Vec_FltSize(p->vWeights) == iDiv ) + { + float * pArray = Vec_FltArray(p->vWeights); + Vec_FltPush(p->vWeights, -2); + if ( p->vPrio && pArray != Vec_FltArray(p->vWeights) ) + Vec_QueSetCosts( p->vPrio, Vec_FltArray(p->vWeights) ); + p->nDivsS++; + } + assert( iDiv < Vec_FltSize(p->vWeights) ); + Vec_FltAddToEntry( p->vWeights, iDiv, 1 ); + p->nPairsS++; + } else - ABC_FREE( vCube->pArray ); - Vec_WecShrink( vCubes, k ); - Vec_WecSortByFirstInt( vCubes, 0 ); + { + assert( iDiv < Vec_FltSize(p->vWeights) ); + Vec_FltAddToEntry( p->vWeights, iDiv, -1 ); + p->nPairsS--; + } + if ( fUpdate ) + { + if ( Vec_QueIsMember(p->vPrio, iDiv) ) + Vec_QueUpdate( p->vPrio, iDiv ); + else if ( !fRemove ) + Vec_QuePush( p->vPrio, iDiv ); + } + } + return Vec_IntSize(vPivot) * (Vec_IntSize(vPivot) - 1) / 2; } - - -/**Function************************************************************* - - Synopsis [Updates the data-structure when divisor is selected.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) +void Fx_ManCubeDoubleCubeDivisors( Fx_Man_t * p, int iFirst, Vec_Int_t * vPivot, int fRemove, int fUpdate ) { -// Vec_Int_t * vDiv = Hsh_VecReadEntry( p->pHash, iDiv ); - - // select pivot variables - - // collect single-cube-divisor cubes - - // collect double-cube-divisor cube pairs - - // subtract old costs - - // create updated single-cube divisor cubes - - // create updated double-cube-divisor cube pairs - - // add new costs - - // assert (divisor weight == old cost - new cost) + Vec_Int_t * vCube; + int i, iDiv, Base; + Vec_WecForEachLevelStart( p->vCubes, vCube, i, iFirst ) + { + if ( Vec_IntSize(vCube) == 0 || vCube == vPivot ) + continue; + if ( Vec_WecIntHasMark(vCube) && Vec_WecIntHasMark(vPivot) && vCube > vPivot ) + continue; + if ( Vec_IntEntry(vCube, 0) != Vec_IntEntry(vPivot, 0) ) + break; + Base = Fx_ManDivFindCubeFree( vCube, vPivot, p->vFree ); +/* + if ( fUpdate ) + { + printf( "Cubes %2d %2d : ", Vec_WecLevelId(p->vCubes, vCube), Vec_WecLevelId(p->vCubes, vPivot) ); + if ( fRemove ) + printf( "Rem " ); + else + printf( "Add " ); + Fx_PrintDivOne( p->vFree ); printf( "\n" ); + } +*/ +// if ( Vec_IntSize(p->vFree) == 4 ) +// Fx_ManDivCanonicize( p->vFree ); + iDiv = Hsh_VecManAdd( p->pHash, p->vFree ); + if ( !fRemove ) + { + if ( iDiv == Vec_FltSize(p->vWeights) ) + { + float * pArray = Vec_FltArray(p->vWeights); + Vec_FltPush(p->vWeights, -Vec_IntSize(p->vFree)); + if ( p->vPrio && pArray != Vec_FltArray(p->vWeights) ) + Vec_QueSetCosts( p->vPrio, Vec_FltArray(p->vWeights) ); + } + assert( iDiv < Vec_FltSize(p->vWeights) ); + Vec_FltAddToEntry( p->vWeights, iDiv, Base + Vec_IntSize(p->vFree) - 1 ); + p->nPairsD++; + } + else + { + assert( iDiv < Vec_FltSize(p->vWeights) ); + Vec_FltAddToEntry( p->vWeights, iDiv, -(Base + Vec_IntSize(p->vFree) - 1) ); + p->nPairsD--; + } + if ( fUpdate ) + { + if ( Vec_QueIsMember(p->vPrio, iDiv) ) + Vec_QueUpdate( p->vPrio, iDiv ); + else if ( !fRemove ) + Vec_QuePush( p->vPrio, iDiv ); + } + } +} +void Fx_ManCreateDivisors( Fx_Man_t * p ) +{ + Vec_Int_t * vCube; + float Weight; + int i; + // alloc hash table + assert( p->pHash == NULL ); + p->pHash = Hsh_VecManStart( 1000 ); + p->vWeights = Vec_FltAlloc( 1000 ); + // create single-cube two-literal divisors + Vec_WecForEachLevel( p->vCubes, vCube, i ) + Fx_ManCubeSingleCubeDivisors( p, vCube, 0, 0 ); // add - no update + assert( p->nDivsS == Vec_FltSize(p->vWeights) ); + // create two-cube divisors + Vec_WecForEachLevel( p->vCubes, vCube, i ) + 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_FltArray(p->vWeights) ); + Vec_FltForEachEntry( p->vWeights, Weight, i ) + if ( Weight > 0.0 ) + Vec_QuePush( p->vPrio, i ); } @@ -590,16 +753,19 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) SeeAlso [] ***********************************************************************/ -Fx_Man_t * Fx_ManStart( Vec_Wec_t * vCubes, int nVars ) +Fx_Man_t * Fx_ManStart( Vec_Wec_t * vCubes ) { Fx_Man_t * p; p = ABC_CALLOC( Fx_Man_t, 1 ); - p->nVars = nVars; - p->vCubes = vCubes; - p->vLits = Fx_ManCreateLiterals( vCubes, &p->vCounts ); - p->pHash = Fx_ManCreateDivisors( vCubes, &p->vWeights, &p->nPairsS, &p->nPairsD, &p->nDivsS ); - p->vPrio = Fx_ManCreateQueue( p->vWeights ); - p->vCube = Vec_IntAlloc( 100 ); + p->vCubes = vCubes; + // temporary data + p->vCubesS = Vec_IntAlloc( 100 ); + p->vCubesD = Vec_IntAlloc( 100 ); + p->vPart0 = Vec_IntAlloc( 100 ); + p->vPart1 = Vec_IntAlloc( 100 ); + p->vFree = Vec_IntAlloc( 100 ); + p->vCube = Vec_IntAlloc( 100 ); + p->vDiv = Vec_IntAlloc( 100 ); return p; } void Fx_ManStop( Fx_Man_t * p ) @@ -610,7 +776,15 @@ void Fx_ManStop( Fx_Man_t * p ) Hsh_VecManStop( p->pHash ); Vec_FltFree( p->vWeights ); Vec_QueFree( p->vPrio ); + Vec_IntFree( p->vVarCube ); + // temporary data + Vec_IntFree( p->vCubesS ); + Vec_IntFree( p->vCubesD ); + Vec_IntFree( p->vPart0 ); + Vec_IntFree( p->vPart1 ); + Vec_IntFree( p->vFree ); Vec_IntFree( p->vCube ); + Vec_IntFree( p->vDiv ); ABC_FREE( p ); } @@ -625,71 +799,224 @@ void Fx_ManStop( Fx_Man_t * p ) SeeAlso [] ***********************************************************************/ -static void Fx_PrintMatrix( Vec_Wec_t * vCubes, int nObjs ) +static inline void Fx_ManCompressCubes( Vec_Wec_t * vCubes, Vec_Int_t * vLit2Cube ) { - Vec_Int_t * vCube; - char * pLine; - int i, v, Lit; - printf( " " ); - for ( i = 0; i < Abc_MinInt(nObjs, 26); i++ ) - printf( "%c", 'a' + i ); - printf( "\n" ); - pLine = ABC_CALLOC( char, nObjs + 1 ); - Vec_WecForEachLevel( vCubes, vCube, i ) + int i, CubeId, k = 0; + Vec_IntForEachEntry( vLit2Cube, CubeId, i ) + if ( Vec_IntSize(Vec_WecEntry(vCubes, CubeId)) > 0 ) + Vec_IntWriteEntry( vLit2Cube, k++, CubeId ); + Vec_IntShrink( vLit2Cube, k ); +} +static inline int Fx_ManGetCubeVar( Vec_Wec_t * vCubes, int iCube ) { return Vec_IntEntry( Vec_WecEntry(vCubes, iCube), 0 ); } +void Fx_ManFindCommonPairs( Vec_Wec_t * vCubes, Vec_Int_t * vPart0, Vec_Int_t * vPart1, Vec_Int_t * vPairs, Vec_Int_t * vDiv, Vec_Int_t * vFree ) +{ + int * pBeg1 = vPart0->pArray; + int * pBeg2 = vPart1->pArray; + int * pEnd1 = vPart0->pArray + vPart0->nSize; + int * pEnd2 = vPart1->pArray + vPart1->nSize; + int i, k, i_, k_, Counter = 0; + Vec_IntClear( vPairs ); + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) { - memset( pLine, '-', nObjs ); - Vec_IntForEachEntryStart( vCube, Lit, v, 1 ) + int CubeId1 = Fx_ManGetCubeVar(vCubes, *pBeg1); + int CubeId2 = Fx_ManGetCubeVar(vCubes, *pBeg2); + if ( CubeId1 == CubeId2 ) { - assert( Abc_Lit2Var(Lit) < nObjs ); - pLine[Abc_Lit2Var(Lit)] = Abc_LitIsCompl(Lit) ? '0' : '1'; + for ( i = 1; pBeg1+i < pEnd1; i++ ) + if ( CubeId1 != Fx_ManGetCubeVar(vCubes, pBeg1[i]) ) + break; + for ( k = 1; pBeg2+k < pEnd2; k++ ) + if ( CubeId1 != Fx_ManGetCubeVar(vCubes, pBeg2[k]) ) + break; + for ( i_ = 0; i_ < i; i_++ ) + for ( k_ = 0; k_ < k; k_++ ) + { + if ( pBeg1[i_] == pBeg2[k_] ) + continue; + Fx_ManDivFindCubeFree( Vec_WecEntry(vCubes, pBeg1[i_]), Vec_WecEntry(vCubes, pBeg2[k_]), vFree ); + if ( !Vec_IntEqual( vDiv, vFree ) ) + continue; + Vec_IntPush( vPairs, pBeg1[i_] ); + Vec_IntPush( vPairs, pBeg2[k_] ); + } + pBeg1 += i; + pBeg2 += k; } - printf( "%6d : %s %4d\n", i, pLine, Vec_IntEntry(vCube, 0) ); + else if ( CubeId1 < CubeId2 ) + pBeg1++; + else + pBeg2++; } - ABC_FREE( pLine ); } -static inline char Fx_PrintDivLit( int Lit ) { return (Abc_LitIsCompl(Abc_Lit2Var(Lit)) ? 'A' : 'a') + Abc_Lit2Var(Abc_Lit2Var(Lit)); } -static inline void Fx_PrintDivOne( Vec_Int_t * vDiv ) -{ - int i, Lit; - Vec_IntForEachEntry( vDiv, Lit, i ) - if ( !Abc_LitIsCompl(Lit) ) - printf( "%c", Fx_PrintDivLit(Lit) ); - printf( " + " ); - Vec_IntForEachEntry( vDiv, Lit, i ) - if ( Abc_LitIsCompl(Lit) ) - printf( "%c", Fx_PrintDivLit(Lit) ); -} -static inline void Fx_PrintDiv( Fx_Man_t * p, int iDiv ) -{ - printf( "Div %6d : ", iDiv ); - printf( "Cost %4d ", (int)Vec_FltEntry(p->vWeights, iDiv) ); - Fx_PrintDivOne( Hsh_VecReadEntry(p->pHash, iDiv) ); - printf( "\n" ); -} -static void Fx_PrintDivisors( Fx_Man_t * p ) -{ - int iDiv; - for ( iDiv = 0; iDiv < Vec_FltSize(p->vWeights); iDiv++ ) - Fx_PrintDiv( p, iDiv ); -} -static void Fx_PrintStats( Fx_Man_t * p, clock_t clk ) + +/**Function************************************************************* + + Synopsis [Updates the data-structure when divisor is selected.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) { - printf( "Cubes =%6d ", Vec_WecSizeUsed(p->vCubes) ); - printf( "Lits =%6d ", Vec_WecSizeUsed(p->vLits) ); - printf( "Divs =%6d ", Hsh_VecSize(p->pHash) ); - printf( "Divs+ =%6d ", Vec_QueSize(p->vPrio) ); - printf( "DivsS =%6d ", p->nDivsS ); - printf( "PairS =%6d ", p->nPairsS ); - printf( "PairD =%6d ", p->nPairsD ); - Abc_PrintTime( 1, "Time", clk ); -// printf( "\n" ); + 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; + // get the divisor + Vec_IntClear( vDiv ); + Vec_IntAppend( vDiv, Hsh_VecReadEntry(p->pHash, iDiv) ); + // select pivot variables + Fx_ManDivFindPivots( vDiv, &Lit0, &Lit1 ); + assert( Lit0 >= 0 && Lit1 >= 0 ); + + // collect single-cube-divisor cubes + Vec_IntClear( p->vCubesS ); + if ( Vec_IntSize(vDiv) == 2 ) + { + Fx_ManCompressCubes( p->vCubes, Vec_WecEntry(p->vLits, Abc_LitNot(Lit0)) ); + Fx_ManCompressCubes( p->vCubes, Vec_WecEntry(p->vLits, Abc_LitNot(Lit1)) ); + Vec_IntTwoRemoveCommon( Vec_WecEntry(p->vLits, Abc_LitNot(Lit0)), Vec_WecEntry(p->vLits, Abc_LitNot(Lit1)), p->vCubesS ); + } +//Vec_IntPrint( p->vCubesS ); + + // collect double-cube-divisor cube pairs + Fx_ManCompressCubes( p->vCubes, Vec_WecEntry(p->vLits, Lit0) ); + Fx_ManCompressCubes( p->vCubes, Vec_WecEntry(p->vLits, Lit1) ); + Fx_ManFindCommonPairs( p->vCubes, Vec_WecEntry(p->vLits, Lit0), Vec_WecEntry(p->vLits, Lit1), p->vCubesD, vDiv, p->vFree ); +//Vec_IntPrint( p->vCubesD ); + + // subtract cost of single-cube divisors + Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i ) + Fx_ManCubeSingleCubeDivisors( p, vCube, 1, 1 ); // remove - update + Fx_ManForEachCubeVec( p->vCubesD, p->vCubes, vCube, i ) + Fx_ManCubeSingleCubeDivisors( p, vCube, 1, 1 ); // remove - update + + // mark the cubes to be removed + Vec_WecMarkLevels( p->vCubes, p->vCubesS ); + Vec_WecMarkLevels( p->vCubes, p->vCubesD ); + + // subtract cost of double-cube divisors + Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i ) + Fx_ManCubeDoubleCubeDivisors( p, Fx_ManGetFirstVarCube(p, vCube), vCube, 1, 1 ); // remove - update + Fx_ManForEachCubeVec( p->vCubesD, p->vCubes, vCube, i ) + Fx_ManCubeDoubleCubeDivisors( p, Fx_ManGetFirstVarCube(p, vCube), vCube, 1, 1 ); // remove - update + + // unmark the cubes to be removed + Vec_WecUnmarkLevels( p->vCubes, p->vCubesS ); + Vec_WecUnmarkLevels( p->vCubes, p->vCubesD ); + + // create new divisor + iVarNew = Vec_WecSize( p->vLits ) / 2; + assert( Vec_IntSize(p->vVarCube) == iVarNew ); + Vec_IntPush( p->vVarCube, Vec_WecSize(p->vCubes) ); + vCube = Vec_WecPushLevel( p->vCubes ); + Vec_IntPush( vCube, iVarNew ); + if ( Vec_IntSize(vDiv) == 2 ) + { + Vec_IntPush( vCube, Abc_LitNot(Lit0) ); + Vec_IntPush( vCube, Abc_LitNot(Lit1) ); + } + else + { + vCube2 = Vec_WecPushLevel( p->vCubes ); + vCube = Vec_WecEntry( p->vCubes, Vec_WecSize(p->vCubes) - 2 ); + Vec_IntPush( vCube2, iVarNew ); + Fx_ManDivAddLits( vCube, vCube2, vDiv ); + } + // do not add new cubes to the matrix + p->nLits += Vec_IntSize( vDiv ); + // create new literals + vLitP = Vec_WecPushLevel( p->vLits ); + vLitN = Vec_WecPushLevel( p->vLits ); + vLitP = Vec_WecEntry( p->vLits, Vec_WecSize(p->vLits) - 2 ); + // create updated single-cube divisor cubes + Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i ) + { + RetValue = Vec_IntRemove1( vCube, Abc_LitNot(Lit0) ); + RetValue += Vec_IntRemove1( vCube, Abc_LitNot(Lit1) ); + assert( RetValue == 2 ); + Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 0) ); + Vec_IntPush( vLitP, Vec_WecLevelId(p->vCubes, vCube) ); + p->nLits--; + } + // create updated double-cube divisor cube pairs + k = 0; + assert( Vec_IntSize(p->vCubesD) % 2 == 0 ); + Fx_ManForEachPairVec( p->vCubesD, p->vCubes, vCube, vCube2, i ) + { + RetValue = Fx_ManDivRemoveLits( vCube, vDiv ); // cube 2*i + RetValue += Fx_ManDivRemoveLits( vCube2, vDiv ); // cube 2*i+1 + assert( RetValue == Vec_IntSize(vDiv) ); + if ( Vec_IntSize(vDiv) == 2 ) + { + Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 1) ); + Vec_IntPush( vLitN, Vec_WecLevelId(p->vCubes, vCube) ); + } + else + { + Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 0) ); + Vec_IntPush( vLitP, Vec_WecLevelId(p->vCubes, vCube) ); + } + p->nLits -= Vec_IntSize(vDiv) + Vec_IntSize(vCube2) - 2; + // remove second cube + Vec_IntWriteEntry( p->vCubesD, k++, Vec_WecLevelId(p->vCubes, vCube) ); + Vec_IntClear( vCube2 ); + } + assert( k == Vec_IntSize(p->vCubesD) / 2 ); + Vec_IntShrink( p->vCubesD, k ); + Vec_IntSort( p->vCubesD, 0 ); + + // add cost of single-cube divisors + Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i ) + Fx_ManCubeSingleCubeDivisors( p, vCube, 0, 1 ); // add - update + Fx_ManForEachCubeVec( p->vCubesD, p->vCubes, vCube, i ) + Fx_ManCubeSingleCubeDivisors( p, vCube, 0, 1 ); // add - update + + // mark the cubes to be removed + Vec_WecMarkLevels( p->vCubes, p->vCubesS ); + Vec_WecMarkLevels( p->vCubes, p->vCubesD ); + + // add cost of double-cube divisors + Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i ) + Fx_ManCubeDoubleCubeDivisors( p, Fx_ManGetFirstVarCube(p, vCube), vCube, 0, 1 ); // add - update + Fx_ManForEachCubeVec( p->vCubesD, p->vCubes, vCube, i ) + Fx_ManCubeDoubleCubeDivisors( p, Fx_ManGetFirstVarCube(p, vCube), vCube, 0, 1 ); // add - update + + // unmark the cubes to be removed + Vec_WecUnmarkLevels( p->vCubes, p->vCubesS ); + Vec_WecUnmarkLevels( p->vCubes, p->vCubesD ); + + // add cost of the new divisor + if ( Vec_IntSize(vDiv) > 2 ) + { + vCube = Vec_WecEntry( p->vCubes, Vec_WecSize(p->vCubes) - 2 ); + vCube2 = Vec_WecEntry( p->vCubes, Vec_WecSize(p->vCubes) - 1 ); + Fx_ManCubeSingleCubeDivisors( p, vCube, 0, 1 ); // add - update + Fx_ManCubeSingleCubeDivisors( p, vCube2, 0, 1 ); // add - update + Vec_IntForEachEntryStart( vCube, Lit0, i, 1 ) + Vec_WecPush( p->vLits, Lit0, Vec_WecLevelId(p->vCubes, vCube) ); + Vec_IntForEachEntryStart( vCube2, Lit0, i, 1 ) + Vec_WecPush( p->vLits, Lit0, Vec_WecLevelId(p->vCubes, vCube2) ); + } + + // remove these cubes from the lit array of the divisor + Vec_IntForEachEntry( vDiv, Lit0, i ) + Vec_IntTwoRemove( Vec_WecEntry(p->vLits, Abc_Lit2Var(Lit0)), p->vCubesD ); + + assert( p->nLits == nLitsNew ); // new SOP lits == old SOP lits - divisor weight } /**Function************************************************************* - Synopsis [] + Synopsis [Implements the traditional fast_extract algorithm.] - Description [] + Description [J. Rajski and J. Vasudevamurthi, "The testability- + preserving concurrent decomposition and factorization of Boolean + expressions", IEEE TCAD, Vol. 11, No. 6, June 1992, pp. 778-793.] SideEffects [] @@ -698,27 +1025,32 @@ static void Fx_PrintStats( Fx_Man_t * p, clock_t clk ) ***********************************************************************/ int Fx_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose ) { + int fVeryVerbose = 0; Fx_Man_t * p; clock_t clk = clock(); - p = Fx_ManStart( vCubes, nVars ); - + // initialize the data-structure + p = Fx_ManStart( vCubes ); + Fx_ManCreateLiterals( p, nVars ); + Fx_ManCreateDivisors( p ); + if ( fVeryVerbose ) + Fx_PrintMatrix( p ); if ( fVerbose ) - { - Fx_PrintMatrix( vCubes, nVars ); - Fx_PrintDivisors( p ); - printf( "Selecting divisors:\n" ); - } - - Fx_PrintStats( p, clock() - clk ); + Fx_PrintStats( p, clock() - clk ); + // perform extraction while ( Vec_QueTopCost(p->vPrio) > 0.0 ) { int iDiv = Vec_QuePop(p->vPrio); if ( fVerbose ) Fx_PrintDiv( p, iDiv ); Fx_ManUpdate( p, iDiv ); + if ( fVeryVerbose ) + Fx_PrintMatrix( p ); + if ( fVerbose ) + Fx_PrintStats( p, clock() - clk ); } - Fx_ManStop( p ); + // return the result + Vec_WecRemoveEmpty( vCubes ); return 1; } diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c index d6744536..b2a56a7d 100644 --- a/src/base/abci/abcFxu.c +++ b/src/base/abci/abcFxu.c @@ -83,9 +83,9 @@ int Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p ) { assert( Abc_NtkIsLogic(pNtk) ); // if the network is already in the SOP form, it may come from BLIF file - // and it may not be SCC-ABC_FREE, in which case FXU will not work correctly + // and it may not be SCC-free, in which case FXU will not work correctly if ( Abc_NtkIsSopLogic(pNtk) ) - { // to make sure the SOPs are SCC-ABC_FREE + { // to make sure the SOPs are SCC-free // Abc_NtkSopToBdd(pNtk); // Abc_NtkBddToSop(pNtk); } diff --git a/src/bool/kit/kitSop.c b/src/bool/kit/kitSop.c index 21ea69b8..f6e33496 100644 --- a/src/bool/kit/kitSop.c +++ b/src/bool/kit/kitSop.c @@ -299,7 +299,7 @@ static inline unsigned Kit_SopCommonCube( Kit_Sop_t * cSop ) /**Function************************************************************* - Synopsis [Makes the cover cube-ABC_FREE.] + Synopsis [Makes the cover cube-free.] Description [] @@ -322,7 +322,7 @@ void Kit_SopMakeCubeFree( Kit_Sop_t * cSop ) /**Function************************************************************* - Synopsis [Checks if the cover is cube-ABC_FREE.] + Synopsis [Checks if the cover is cube-free.] Description [] diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 03427a0b..2fe15792 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -885,6 +885,20 @@ static inline int Vec_IntRemove( Vec_Int_t * p, int Entry ) p->nSize--; return 1; } +static inline int Vec_IntRemove1( Vec_Int_t * p, int Entry ) +{ + int i; + for ( i = 1; i < p->nSize; i++ ) + if ( p->pArray[i] == Entry ) + break; + if ( i >= p->nSize ) + return 0; + assert( i < p->nSize ); + for ( i++; i < p->nSize; i++ ) + p->pArray[i-1] = p->pArray[i]; + p->nSize--; + return 1; +} /**Function************************************************************* @@ -1298,6 +1312,18 @@ static inline int Vec_IntTwoCountCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2 ) } return Counter; } + +/**Function************************************************************* + + Synopsis [Collects common entries.] + + Description [Assumes that the vectors are sorted in the increasing order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ static inline int Vec_IntTwoFindCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vArr ) { int * pBeg1 = vArr1->pArray; @@ -1317,6 +1343,77 @@ static inline int Vec_IntTwoFindCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Ve return Vec_IntSize(vArr); } +/**Function************************************************************* + + Synopsis [Collects and removes common entries] + + Description [Assumes that the vectors are sorted in the increasing order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_IntTwoRemoveCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vArr ) +{ + int * pBeg1 = vArr1->pArray; + int * pBeg2 = vArr2->pArray; + int * pEnd1 = vArr1->pArray + vArr1->nSize; + int * pEnd2 = vArr2->pArray + vArr2->nSize; + int * pBeg1New = vArr1->pArray; + int * pBeg2New = vArr2->pArray; + Vec_IntClear( vArr ); + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + if ( *pBeg1 == *pBeg2 ) + Vec_IntPush( vArr, *pBeg1 ), pBeg1++, pBeg2++; + else if ( *pBeg1 < *pBeg2 ) + *pBeg1New++ = *pBeg1++; + else + *pBeg2New++ = *pBeg2++; + } + while ( pBeg1 < pEnd1 ) + *pBeg1New++ = *pBeg1++; + while ( pBeg2 < pEnd2 ) + *pBeg2New++ = *pBeg2++; + Vec_IntShrink( vArr1, pBeg1New - vArr1->pArray ); + Vec_IntShrink( vArr2, pBeg2New - vArr2->pArray ); + return Vec_IntSize(vArr); +} + +/**Function************************************************************* + + Synopsis [Removes entries of the second one from the first one.] + + Description [Assumes that the vectors are sorted in the increasing order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_IntTwoRemove( Vec_Int_t * vArr1, Vec_Int_t * vArr2 ) +{ + int * pBeg1 = vArr1->pArray; + int * pBeg2 = vArr2->pArray; + int * pEnd1 = vArr1->pArray + vArr1->nSize; + int * pEnd2 = vArr2->pArray + vArr2->nSize; + int * pBeg1New = vArr1->pArray; + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + if ( *pBeg1 == *pBeg2 ) + pBeg1++, pBeg2++; + else if ( *pBeg1 < *pBeg2 ) + *pBeg1New++ = *pBeg1++; + else + pBeg2++; + } + while ( pBeg1 < pEnd1 ) + *pBeg1New++ = *pBeg1++; + Vec_IntShrink( vArr1, pBeg1New - vArr1->pArray ); + return Vec_IntSize(vArr1); +} + /**Function************************************************************* Synopsis [Returns the result of merging the two vectors.] @@ -1358,7 +1455,7 @@ static inline Vec_Int_t * Vec_IntTwoMerge( Vec_Int_t * vArr1, Vec_Int_t * vArr2 /**Function************************************************************* - Synopsis [Returns the result of merging the two vectors.] + Synopsis [Returns the result of splitting of the two vectors.] Description [Assumes that the vectors are sorted in the increasing order.] diff --git a/src/misc/vec/vecQue.h b/src/misc/vec/vecQue.h index 83be97a8..445c6fb3 100644 --- a/src/misc/vec/vecQue.h +++ b/src/misc/vec/vecQue.h @@ -94,7 +94,7 @@ static inline void Vec_QueFreeP( Vec_Que_t ** p ) } static inline void Vec_QueSetCosts( Vec_Que_t * p, float * pCosts ) { - assert( p->pCostsFlt == NULL ); +// assert( p->pCostsFlt == NULL ); p->pCostsFlt = pCosts; } static inline void Vec_QueGrow( Vec_Que_t * p, int nCapMin ) @@ -215,12 +215,15 @@ static inline void Vec_QueUpdate( Vec_Que_t * p, int v ) ***********************************************************************/ static inline int Vec_QueIsMember( Vec_Que_t * p, int v ) { - return (int)( p->pOrder[v] >= 0 ); + assert( v >= 0 ); + return (int)( v < p->nCap && p->pOrder[v] >= 0 ); } static inline void Vec_QuePush( Vec_Que_t * p, int v ) { - if ( p->nSize == p->nCap ) - Vec_QueGrow( p, 2 * p->nCap ); + if ( p->nSize >= p->nCap ) + Vec_QueGrow( p, Abc_MaxInt(p->nSize+1, 2*p->nCap) ); + if ( v >= p->nCap ) + Vec_QueGrow( p, Abc_MaxInt(v+1, 2*p->nCap) ); assert( p->nSize < p->nCap ); assert( p->pOrder[v] == -1 ); assert( p->pHeap[p->nSize] == -1 ); diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h index 34d5d956..8a924f90 100644 --- a/src/misc/vec/vecWec.h +++ b/src/misc/vec/vecWec.h @@ -54,6 +54,8 @@ struct Vec_Wec_t_ // iterators through levels #define Vec_WecForEachLevel( vGlob, vVec, i ) \ for ( i = 0; (i < Vec_WecSize(vGlob)) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i++ ) +#define Vec_WecForEachLevelVec( vLevels, vGlob, vVec, i ) \ + for ( i = 0; (i < Vec_IntSize(vLevels)) && (((vVec) = Vec_WecEntry(vGlob, Vec_IntEntry(vLevels, i))), 1); i++ ) #define Vec_WecForEachLevelStart( vGlob, vVec, i, LevelStart ) \ for ( i = LevelStart; (i < Vec_WecSize(vGlob)) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i++ ) #define Vec_WecForEachLevelStop( vGlob, vVec, i, LevelStop ) \ @@ -147,6 +149,27 @@ static inline int Vec_WecEntryEntry( Vec_Wec_t * p, int i, int k ) return Vec_IntEntry( Vec_WecEntry(p, i), k ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Int_t * Vec_WecArray( Vec_Wec_t * p ) +{ + return p->pArray; +} +static inline int Vec_WecLevelId( Vec_Wec_t * p, Vec_Int_t * vLevel ) +{ + assert( p->pArray <= vLevel && vLevel < p->pArray + p->nSize ); + return vLevel - p->pArray; +} + /**Function************************************************************* Synopsis [] @@ -239,14 +262,21 @@ static inline void Vec_WecPush( Vec_Wec_t * p, int Level, int Entry ) { if ( p->nSize < Level + 1 ) { - Vec_WecGrow( p, Level + 1 ); + Vec_WecGrow( p, Abc_MaxInt(2*p->nCap, Level + 1) ); p->nSize = Level + 1; } Vec_IntPush( Vec_WecEntry(p, Level), Entry ); } static inline Vec_Int_t * Vec_WecPushLevel( Vec_Wec_t * p ) { - Vec_WecGrow( p, ++p->nSize ); + if ( p->nSize == p->nCap ) + { + if ( p->nCap < 16 ) + Vec_WecGrow( p, 16 ); + else + Vec_WecGrow( p, 2 * p->nCap ); + } + ++p->nSize; return Vec_WecEntryLast( p ); } @@ -557,6 +587,67 @@ static inline Vec_Ptr_t * Vec_WecConvertToVecPtr( Vec_Wec_t * p ) return vCopy; } + +/**Function************************************************************* + + Synopsis [Temporary vector marking.] + + Description [The vector should be static when the marking is used.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_WecIntHasMark( Vec_Int_t * vVec ) { return (vVec->nCap >> 30) & 1; } +static inline void Vec_WecIntSetMark( Vec_Int_t * vVec ) { vVec->nCap |= (1<<30); } +static inline void Vec_WecIntXorMark( Vec_Int_t * vVec ) { vVec->nCap ^= (1<<30); } +static inline void Vec_WecMarkLevels( Vec_Wec_t * vCubes, Vec_Int_t * vLevels ) +{ + Vec_Int_t * vCube; + int i; + Vec_WecForEachLevelVec( vLevels, vCubes, vCube, i ) + { + assert( !Vec_WecIntHasMark( vCube ) ); + Vec_WecIntXorMark( vCube ); + } +} +static inline void Vec_WecUnmarkLevels( Vec_Wec_t * vCubes, Vec_Int_t * vLevels ) +{ + Vec_Int_t * vCube; + int i; + Vec_WecForEachLevelVec( vLevels, vCubes, vCube, i ) + { + assert( Vec_WecIntHasMark( vCube ) ); + Vec_WecIntXorMark( vCube ); + } +} + +/**Function************************************************************* + + Synopsis [Removes 0-size vectors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_WecRemoveEmpty( Vec_Wec_t * vCubes ) +{ + Vec_Int_t * vCube; + int i, k = 0; + Vec_WecForEachLevel( vCubes, vCube, i ) + if ( Vec_IntSize(vCube) > 0 ) + vCubes->pArray[k++] = *vCube; + else + ABC_FREE( vCube->pArray ); + Vec_WecShrink( vCubes, k ); +// Vec_WecSortByFirstInt( vCubes, 0 ); +} + + ABC_NAMESPACE_HEADER_END #endif diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c index c6fb5796..0095abf9 100644 --- a/src/opt/fxu/fxu.c +++ b/src/opt/fxu/fxu.c @@ -47,7 +47,7 @@ static int s_MemoryPeak; The entries corresponding to the PI and objects with trivial covers are NULL. The number of extracted covers (not exceeding p->nNodesExt) is returned. Two other things are important for the correct operation of this procedure: - (1) The input covers do not have duplicated fanins and are SCC-ABC_FREE. + (1) The input covers do not have duplicated fanins and are SCC-free. (2) The fanins array contains the numbers of the fanin objects.] SideEffects [] diff --git a/src/opt/fxu/fxuPair.c b/src/opt/fxu/fxuPair.c index d040abe9..32822592 100644 --- a/src/opt/fxu/fxuPair.c +++ b/src/opt/fxu/fxuPair.c @@ -89,7 +89,7 @@ void Fxu_PairCanonicize( Fxu_Cube ** ppCube1, Fxu_Cube ** ppCube2 ) pLit2 = pLit2->pHNext; continue; } - assert( pLit1 && pLit2 ); // this is true if the covers are SCC-ABC_FREE + assert( pLit1 && pLit2 ); // this is true if the covers are SCC-free if ( pLit1->iVar > pLit2->iVar ) { // swap the cubes pCubeTemp = *ppCube1; @@ -152,7 +152,7 @@ unsigned Fxu_PairHashKeyArray( Fxu_Matrix * p, int piVarsC1[], int piVarsC2[], i Synopsis [Computes the hash key of the divisor represented by the pair of cubes.] Description [Goes through the variables in both cubes. Skips the identical - ones (this corresponds to making the cubes cube-ABC_FREE). Computes the hash + ones (this corresponds to making the cubes cube-free). Computes the hash value of the cubes. Assigns the number of literals in the base and in the cubes without base.] @@ -181,7 +181,7 @@ unsigned Fxu_PairHashKey( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2, if ( pLit1 && pLit2 ) { if ( pLit1->iVar == pLit2->iVar ) - { // ensure cube-ABC_FREE + { // ensure cube-free pLit1 = pLit1->pHNext; pLit2 = pLit2->pHNext; // add this literal to the base diff --git a/src/opt/fxu/fxuSelect.c b/src/opt/fxu/fxuSelect.c index c9945926..da55eb82 100644 --- a/src/opt/fxu/fxuSelect.c +++ b/src/opt/fxu/fxuSelect.c @@ -419,7 +419,7 @@ void Fxu_MatrixGetDoubleVars( Fxu_Matrix * p, Fxu_Double * pDouble, if ( pLit1 && pLit2 ) { if ( pLit1->iVar == pLit2->iVar ) - { // ensure cube-ABC_FREE + { // ensure cube-free pLit1 = pLit1->pHNext; pLit2 = pLit2->pHNext; } -- cgit v1.2.3