From 7a78e3039087b35344a6f87bb4fcf1891ed4a02f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 5 May 2013 14:33:28 -0700 Subject: New fast extract. --- src/base/abc/abcUtil.c | 47 +++++ src/base/abci/abc.c | 2 +- src/base/abci/abcFx.c | 543 ++++++++++++++++++++++++++----------------------- 3 files changed, 332 insertions(+), 260 deletions(-) (limited to 'src') diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 8909a15d..08b6eb43 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -2684,6 +2684,53 @@ int Abc_NtkIsTopo( Abc_Ntk_t * pNtk ) return (int)(Counter == 0); } +/**Function************************************************************* + + Synopsis [Reroders fanins of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkOrderFanins( Abc_Ntk_t * pNtk ) +{ + Vec_Int_t * vOrder; + Abc_Obj_t * pNode; + char * pSop, * pSopNew; + char * pCube, * pCubeNew; + int nVars, i, v, * pOrder; + assert( Abc_NtkIsSopLogic(pNtk) ); + vOrder = Vec_IntAlloc( 100 ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + pSop = (char *)pNode->pData; + nVars = Abc_SopGetVarNum(pSop); + assert( nVars == Abc_ObjFaninNum(pNode) ); + Vec_IntClear( vOrder ); + for ( v = 0; v < nVars; v++ ) + Vec_IntPush( vOrder, v ); + pOrder = Vec_IntArray(vOrder); + Vec_IntSelectSortCost( pOrder, nVars, &pNode->vFanins ); + pSopNew = pCubeNew = Abc_SopStart( (Mem_Flex_t *)pNtk->pManFunc, Abc_SopGetCubeNum(pSop), nVars ); + Abc_SopForEachCube( pSop, nVars, pCube ) + { + for ( v = 0; v < nVars; v++ ) + if ( pCube[pOrder[v]] == '0' ) + pCubeNew[v] = '0'; + else if ( pCube[pOrder[v]] == '1' ) + pCubeNew[v] = '1'; + pCubeNew += nVars + 3; + } + pNode->pData = pSopNew; + Vec_IntSort( &pNode->vFanins, 0 ); +// Vec_IntPrint( vOrder ); + } + Vec_IntFree( vOrder ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 47196ad3..f555bbf8 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3530,7 +3530,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int fVerbose ); Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); Fxu_Data_t Params, * p = &Params; - int c, fNewAlgo = 0; + int c, fNewAlgo = 1; // set the defaults Abc_NtkSetDefaultParams( p ); Extra_UtilGetoptReset(); diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c index b337c6ca..727bf263 100644 --- a/src/base/abci/abcFx.c +++ b/src/base/abci/abcFx.c @@ -29,62 +29,49 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern int Fx_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* +typedef struct Fx_Man_t_ Fx_Man_t; +struct Fx_Man_t_ +{ + // user's data + Vec_Wec_t * vCubes; // cube -> lit + // internal data + Vec_Wec_t * vLits; // lit -> cube + Vec_Int_t * vCounts; // literal counts (currently unused) + Hsh_VecMan_t * pHash; // hash table of 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 data-structure after one extraction + Vec_Int_t * vCubesS; // single cubes for the given divisor + Vec_Int_t * vCubesD; // cube pairs for the given divisor + Vec_Int_t * vCompls; // complements of cube pairs + Vec_Int_t * vCubeFree; // cube-free divisor + Vec_Int_t * vDiv; // divisor + // statistics + clock_t timeStart; // starting time + int nVars; // original problem variables + int nLits; // the number of SOP literals + int nDivs; // the number of extracted divisors + int nPairsS; // number of lit pairs + int nPairsD; // number of cube pairs + int nDivsS; // single cube divisors + int nDivMux[3]; // 0 = mux, 1 = compl mux, 2 = no mux +}; - Synopsis [Reroders fanins of the network.] +static inline int Fx_ManGetFirstVarCube( Fx_Man_t * p, Vec_Int_t * vCube ) { return Vec_IntEntry( p->vVarCube, Vec_IntEntry(vCube, 0) ); } - Description [] - - SideEffects [] +#define Fx_ManForEachCubeVec( vVec, vCubes, vCube, i ) \ + for ( i = 0; (i < Vec_IntSize(vVec)) && ((vCube) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i))); i++ ) - SeeAlso [] +static int Fx_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose ); -***********************************************************************/ -void Abc_NtkOrderFanins( Abc_Ntk_t * pNtk ) -{ - Vec_Int_t * vOrder; - Abc_Obj_t * pNode; - char * pSop, * pSopNew; - char * pCube, * pCubeNew; - int nVars, i, v, * pOrder; - assert( Abc_NtkIsSopLogic(pNtk) ); - vOrder = Vec_IntAlloc( 100 ); - Abc_NtkForEachNode( pNtk, pNode, i ) - { - pSop = (char *)pNode->pData; - nVars = Abc_SopGetVarNum(pSop); - assert( nVars == Abc_ObjFaninNum(pNode) ); - Vec_IntClear( vOrder ); - for ( v = 0; v < nVars; v++ ) - Vec_IntPush( vOrder, v ); - pOrder = Vec_IntArray(vOrder); - Vec_IntSelectSortCost( pOrder, nVars, &pNode->vFanins ); - pSopNew = pCubeNew = Abc_SopStart( (Mem_Flex_t *)pNtk->pManFunc, Abc_SopGetCubeNum(pSop), nVars ); - Abc_SopForEachCube( pSop, nVars, pCube ) - { - for ( v = 0; v < nVars; v++ ) - if ( pCube[pOrder[v]] == '0' ) - pCubeNew[v] = '0'; - else if ( pCube[pOrder[v]] == '1' ) - pCubeNew[v] = '1'; - pCubeNew += nVars + 3; - } - pNode->pData = pSopNew; - Vec_IntSort( &pNode->vFanins, 0 ); -// Vec_IntPrint( vOrder ); - } - Vec_IntFree( vOrder ); -} +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Extracts SOP information.] + Synopsis [Retrieves SOP information for fast_extract.] Description [] @@ -93,7 +80,7 @@ void Abc_NtkOrderFanins( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Vec_Wec_t * Abc_NtkFxExtract( Abc_Ntk_t * pNtk ) +Vec_Wec_t * Abc_NtkFxRetrieve( Abc_Ntk_t * pNtk ) { Vec_Wec_t * vCubes; Vec_Int_t * vCube; @@ -107,8 +94,7 @@ Vec_Wec_t * Abc_NtkFxExtract( Abc_Ntk_t * pNtk ) pSop = (char *)pNode->pData; nVars = Abc_SopGetVarNum(pSop); assert( nVars == Abc_ObjFaninNum(pNode) ); - if ( nVars < 2 ) - continue; +// if ( nVars < 2 ) continue; Abc_SopForEachCube( pSop, nVars, pCube ) { vCube = Vec_WecPushLevel( vCubes ); @@ -128,7 +114,7 @@ Vec_Wec_t * Abc_NtkFxExtract( Abc_Ntk_t * pNtk ) /**Function************************************************************* - Synopsis [Inserts SOP information.] + Synopsis [Inserts SOP information after fast_extract.] Description [] @@ -155,14 +141,12 @@ void Abc_NtkFxInsert( Abc_Ntk_t * pNtk, Vec_Wec_t * vCubes ) // find the largest index Vec_WecForEachLevel( vCubes, vCube, i ) iNodeMax = Abc_MaxInt( iNodeMax, Vec_IntEntry(vCube, 0) ); - // quit if nothing new -/* + // quit if nothing changes if ( iNodeMax < Abc_NtkObjNumMax(pNtk) ) { printf( "The network is unchanged by fast extract.\n" ); return; } -*/ // create new nodes for ( i = Abc_NtkObjNumMax(pNtk); i <= iNodeMax; i++ ) { @@ -183,11 +167,7 @@ void Abc_NtkFxInsert( Abc_Ntk_t * pNtk, Vec_Wec_t * vCubes ) vPres = Vec_IntStartFull( Abc_NtkObjNumMax(pNtk) ); Abc_NtkForEachNode( pNtk, pNode, i ) { - if ( Vec_IntEntry(vCount, i) == 0 ) - { - assert( Abc_ObjFaninNum(pNode) < 2 ); - continue; - } +// if ( Vec_IntEntry(vCount, i) == 0 ) continue; Abc_ObjRemoveFanins( pNode ); // create fanins assert( Vec_IntEntry(vCount, i) > 0 ); @@ -219,6 +199,7 @@ void Abc_NtkFxInsert( Abc_Ntk_t * pNtk, Vec_Wec_t * vCubes ) } pCube += Abc_ObjFaninNum(pNode) + 3; } + // complement SOP if the original one was complemented if ( pNode->pData && Abc_SopIsComplement((char *)pNode->pData) ) Abc_SopComplement( pSop ); pNode->pData = pSop; @@ -279,7 +260,7 @@ int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int fVerbose ) Abc_NtkCleanup( pNtk, 0 ); // Abc_NtkOrderFanins( pNtk ); // collect information about the covers - vCubes = Abc_NtkFxExtract( pNtk ); + vCubes = Abc_NtkFxRetrieve( pNtk ); // call the fast extract procedure if ( Fx_FastExtract( vCubes, Abc_NtkObjNumMax(pNtk), fVerbose ) > 0 ) { @@ -298,43 +279,9 @@ int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int fVerbose ) - -typedef struct Fx_Man_t_ Fx_Man_t; -struct Fx_Man_t_ -{ - 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.] + Synopsis [Starting the manager.] Description [] @@ -343,60 +290,40 @@ static inline int Fx_ManGetFirstVarCube( Fx_Man_t * p, Vec_Int_t * vCube ) { ret SeeAlso [] ***********************************************************************/ -int Fx_ManDivCanonicize( Vec_Int_t * vFree ) // return 1 if complemented +Fx_Man_t * Fx_ManStart( Vec_Wec_t * vCubes ) { - int * A = Vec_IntArray(vFree); - int C[4] = { Abc_Lit2Var(A[0]), Abc_Lit2Var(A[1]), Abc_Lit2Var(A[2]), Abc_Lit2Var(A[3]) }; - int L[4] = { Abc_Lit2Var(A[0]), Abc_Lit2Var(A[1]), Abc_Lit2Var(A[2]), Abc_Lit2Var(A[3]) }; - int V[4] = { Abc_Lit2Var(L[0]), Abc_Lit2Var(L[1]), Abc_Lit2Var(L[2]), Abc_Lit2Var(L[3]) }; - assert( Vec_IntSize(vFree) == 4 ); - if ( V[0] == V[1] && V[2] == V[3] ) // 2,2,2 - { - assert( !Abc_LitIsCompl(L[0]) ); - assert( Abc_LitIsCompl(L[1]) ); - if ( !Abc_LitIsCompl(L[2]) ) - { - C[2] ^= 2; - C[3] ^= 2; - return 1; - } - return 0; - } - if ( V[0] == V[1] ) - { - assert( V[0] != V[2] && V[0] != V[3] ); - if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[2]) && Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[3]) ) // 2,2,3 - { - if ( Abc_LitIsCompl(Abc_Lit2Var(L[0])) == Abc_LitIsCompl(Abc_Lit2Var(L[2])) ) - { - L[2] = Abc_LitNot(L[2]); - L[3] = Abc_LitNot(L[3]); - return 1; - } - return 0; - } - } - if ( V[0] == V[2] ) - { - } - if ( V[0] == V[3] ) - { - } - if ( V[1] == V[2] ) - { - } - if ( V[1] == V[3] ) - { - } - if ( V[2] == V[3] ) - { - } - return 0; + Fx_Man_t * p; + p = ABC_CALLOC( Fx_Man_t, 1 ); + p->vCubes = vCubes; + // temporary data + p->vCubesS = Vec_IntAlloc( 100 ); + p->vCubesD = Vec_IntAlloc( 100 ); + p->vCompls = Vec_IntAlloc( 100 ); + p->vCubeFree = Vec_IntAlloc( 100 ); + p->vDiv = Vec_IntAlloc( 100 ); + return p; +} +void Fx_ManStop( Fx_Man_t * p ) +{ +// Vec_WecFree( p->vCubes ); + Vec_WecFree( p->vLits ); + Vec_IntFree( p->vCounts ); + 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->vCompls ); + Vec_IntFree( p->vCubeFree ); + Vec_IntFree( p->vDiv ); + ABC_FREE( p ); } /**Function************************************************************* - Synopsis [] + Synopsis [Printing procedures.] Description [] @@ -406,7 +333,7 @@ int Fx_ManDivCanonicize( Vec_Int_t * vFree ) // return 1 if complemented ***********************************************************************/ 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 ) +static inline void Fx_PrintDivOneReal( Vec_Int_t * vDiv ) { int i, Lit; Vec_IntForEachEntry( vDiv, Lit, i ) @@ -417,12 +344,40 @@ static inline void Fx_PrintDivOne( Vec_Int_t * vDiv ) if ( Abc_LitIsCompl(Lit) ) printf( "%c", Fx_PrintDivLit(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_Var2Lit(i, Abc_LitIsCompl(Lit)) ) ); + printf( " + " ); + Vec_IntForEachEntry( vDiv, Lit, i ) + if ( Abc_LitIsCompl(Lit) ) + printf( "%c", Fx_PrintDivLit( Abc_Var2Lit(i, Abc_LitIsCompl(Lit)) ) ); +} +static inline void Fx_PrintDivArray( Vec_Int_t * vDiv ) +{ + int i, Lit; + Vec_IntForEachEntry( vDiv, Lit, i ) + if ( !Abc_LitIsCompl(Lit) ) + printf( "%d(1) ", Abc_Lit2Var(Lit) ); + printf( " + " ); + Vec_IntForEachEntry( vDiv, Lit, i ) + if ( Abc_LitIsCompl(Lit) ) + printf( "%d(2) ", 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) ); + int i; + printf( "%4d : ", p->nDivs ); + printf( "Div %7d : ", iDiv ); + printf( "Weight %5d ", (int)Vec_FltEntry(p->vWeights, iDiv) ); Fx_PrintDivOne( Hsh_VecReadEntry(p->pHash, iDiv) ); - printf( "\n" ); + for ( i = Vec_IntSize(Hsh_VecReadEntry(p->pHash, iDiv)) + 3; i < 20; i++ ) + printf( " " ); + printf( "Lits =%7d ", p->nLits ); + printf( "Divs =%8d ", Hsh_VecSize(p->pHash) ); + Abc_PrintTime( 1, "Time", clock() - p->timeStart ); } static void Fx_PrintDivisors( Fx_Man_t * p ) { @@ -469,20 +424,103 @@ static void Fx_PrintMatrix( Fx_Man_t * 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 ); + printf( "Cubes =%7d ", Vec_WecSizeUsed(p->vCubes) ); + printf( "Lits =%7d ", Vec_WecSizeUsed(p->vLits) ); + printf( "Divs =%7d ", Hsh_VecSize(p->pHash) ); + printf( "Divs+ =%7d ", Vec_QueSize(p->vPrio) ); + printf( "Compl =%6d ", p->nDivMux[1] ); +// printf( "DivsS =%6d ", p->nDivsS ); +// printf( "PairS =%6d ", p->nPairsS ); +// printf( "PairD =%6d ", p->nPairsD ); Abc_PrintTime( 1, "Time", clk ); // printf( "\n" ); } /**Function************************************************************* - Synopsis [] + Synopsis [Returns 1 if the divisor should be complemented.] + + Description [Normalizes the divisor by putting, first, positive control + literal first and, second, positive data1 literal. As the result, + a MUX divisor is (ab + !ac) and an XOR divisor is (ab + !a!b).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int Fx_ManDivNormalize( Vec_Int_t * vCubeFree ) // return 1 if complemented +{ + int * L = Vec_IntArray(vCubeFree); + int RetValue = 0, LitA0 = -1, LitB0 = -1, LitA1 = -1, LitB1 = -1; + assert( Vec_IntSize(vCubeFree) == 4 ); + if ( Abc_LitIsCompl(L[0]) != Abc_LitIsCompl(L[1]) && (L[0] >> 2) == (L[1] >> 2) ) // diff cubes, same vars + { + if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[3]) ) + return -1; + LitA0 = Abc_Lit2Var(L[0]), LitB0 = Abc_Lit2Var(L[1]); + if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[2]) ) + { + assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[3]) ); + LitA1 = Abc_Lit2Var(L[2]), LitB1 = Abc_Lit2Var(L[3]); + } + else + { + assert( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) ); + assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[2]) ); + LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[2]); + } + } + else if ( Abc_LitIsCompl(L[1]) != Abc_LitIsCompl(L[2]) && (L[1] >> 2) == (L[2] >> 2) ) + { + if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) ) + return -1; + LitA0 = Abc_Lit2Var(L[1]), LitB0 = Abc_Lit2Var(L[2]); + if ( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[0]) ) + LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[3]); + else + LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[0]); + } + else if ( Abc_LitIsCompl(L[2]) != Abc_LitIsCompl(L[3]) && (L[2] >> 2) == (L[3] >> 2) ) + { + if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[1]) ) + return -1; + LitA0 = Abc_Lit2Var(L[2]), LitB0 = Abc_Lit2Var(L[3]); + if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[0]) ) + LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[1]); + else + LitA1 = Abc_Lit2Var(L[1]), LitB1 = Abc_Lit2Var(L[0]); + } + else + return -1; + assert( LitA0 == Abc_LitNot(LitB0) ); + if ( Abc_LitIsCompl(LitA0) ) + { + ABC_SWAP( int, LitA0, LitB0 ); + ABC_SWAP( int, LitA1, LitB1 ); + } + assert( !Abc_LitIsCompl(LitA0) ); + if ( Abc_LitIsCompl(LitA1) ) + { + LitA1 = Abc_LitNot(LitA1); + LitB1 = Abc_LitNot(LitB1); + RetValue = 1; + } + assert( !Abc_LitIsCompl(LitA1) ); + // arrange literals in such as a way that + // - the first two literals are control literals from different cubes + // - the third literal is non-complented data input + // - the forth literal is possibly complemented data input + L[0] = Abc_Var2Lit( LitA0, 0 ); + L[1] = Abc_Var2Lit( LitB0, 1 ); + L[2] = Abc_Var2Lit( LitA1, 0 ); + L[3] = Abc_Var2Lit( LitB1, 1 ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Find a cube-free divisor of the two cubes.] Description [] @@ -491,39 +529,39 @@ static void Fx_PrintStats( Fx_Man_t * p, clock_t clk ) SeeAlso [] ***********************************************************************/ -int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vFree ) +int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vCubeFree ) { - int * pBeg1 = vArr1->pArray + 1; - int * pBeg2 = vArr2->pArray + 1; + int * pBeg1 = vArr1->pArray + 1; // skip variable ID + int * pBeg2 = vArr2->pArray + 1; // skip variable ID int * pEnd1 = vArr1->pArray + vArr1->nSize; int * pEnd2 = vArr2->pArray + vArr2->nSize; int Counter = 0, fAttr0 = 0, fAttr1 = 1; - Vec_IntClear( vFree ); + Vec_IntClear( vCubeFree ); while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) { if ( *pBeg1 == *pBeg2 ) pBeg1++, pBeg2++, Counter++; else if ( *pBeg1 < *pBeg2 ) - Vec_IntPush( vFree, Abc_Var2Lit(*pBeg1++, fAttr0) ); + Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) ); else { - if ( Vec_IntSize(vFree) == 0 ) + if ( Vec_IntSize(vCubeFree) == 0 ) fAttr0 = 1, fAttr1 = 0; - Vec_IntPush( vFree, Abc_Var2Lit(*pBeg2++, fAttr1) ); + Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg2++, fAttr1) ); } } while ( pBeg1 < pEnd1 ) - Vec_IntPush( vFree, Abc_Var2Lit(*pBeg1++, fAttr0) ); + Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) ); while ( pBeg2 < pEnd2 ) - Vec_IntPush( vFree, Abc_Var2Lit(*pBeg2++, fAttr1) ); - assert( Vec_IntSize(vFree) > 1 ); // the cover is not SCC-free - assert( !Abc_LitIsCompl(Vec_IntEntry(vFree, 0)) ); + Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg2++, fAttr1) ); + assert( Vec_IntSize(vCubeFree) > 1 ); // the cover is not SCC-free + assert( !Abc_LitIsCompl(Vec_IntEntry(vCubeFree, 0)) ); return Counter; } /**Function************************************************************* - Synopsis [] + Synopsis [Procedures operating on a two-cube divisor.] Description [] @@ -553,16 +591,17 @@ static inline void Fx_ManDivFindPivots( Vec_Int_t * vDiv, int * pLit0, int * pLi return; } } -static inline int Fx_ManDivRemoveLits( Vec_Int_t * vCube, Vec_Int_t * vDiv ) +static inline int Fx_ManDivRemoveLits( Vec_Int_t * vCube, Vec_Int_t * vDiv, int fCompl ) { int i, Lit, Count = 0; + assert( !fCompl || Vec_IntSize(vDiv) == 4 ); Vec_IntForEachEntry( vDiv, Lit, i ) - Count += Vec_IntRemove1( vCube, Abc_Lit2Var(Lit) ); + Count += Vec_IntRemove1( vCube, Abc_Lit2Var(Lit) ^ (fCompl && i > 1) ); // the last two lits can be complemented return Count; } static inline void Fx_ManDivAddLits( Vec_Int_t * vCube, Vec_Int_t * vCube2, Vec_Int_t * vDiv ) { - int i, Lit; + int i, Lit, * pArray; // Vec_IntClear( vCube ); // Vec_IntClear( vCube2 ); Vec_IntForEachEntry( vDiv, Lit, i ) @@ -570,11 +609,21 @@ static inline void Fx_ManDivAddLits( Vec_Int_t * vCube, Vec_Int_t * vCube2, Vec_ Vec_IntPush( vCube2, Abc_Lit2Var(Lit) ); else Vec_IntPush( vCube, Abc_Lit2Var(Lit) ); + if ( Vec_IntSize(vDiv) == 4 && Vec_IntSize(vCube) == 3 ) + { + assert( Vec_IntSize(vCube2) == 3 ); + pArray = Vec_IntArray(vCube); + if ( pArray[1] > pArray[2] ) + ABC_SWAP( int, pArray[1], pArray[2] ); + pArray = Vec_IntArray(vCube2); + if ( pArray[1] > pArray[2] ) + ABC_SWAP( int, pArray[1], pArray[2] ); + } } /**Function************************************************************* - Synopsis [] + Synopsis [Setting up the data-structure.] Description [] @@ -628,10 +677,10 @@ int Fx_ManCubeSingleCubeDivisors( Fx_Man_t * p, Vec_Int_t * vPivot, int fRemove, 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 ); + Vec_IntClear( p->vCubeFree ); + Vec_IntPush( p->vCubeFree, Abc_Var2Lit(Abc_LitNot(Lit), 0) ); + Vec_IntPush( p->vCubeFree, Abc_Var2Lit(Abc_LitNot(Lit2), 1) ); + iDiv = Hsh_VecManAdd( p->pHash, p->vCubeFree ); if ( !fRemove ) { if ( Vec_FltSize(p->vWeights) == iDiv ) @@ -671,33 +720,30 @@ void Fx_ManCubeDoubleCubeDivisors( Fx_Man_t * p, int iFirst, Vec_Int_t * 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 " ); + Base = Fx_ManDivFindCubeFree( vCube, vPivot, p->vCubeFree ); + if ( Vec_IntSize(p->vCubeFree) == 4 ) + { + int Value = Fx_ManDivNormalize( p->vCubeFree ); + if ( Value == 0 ) + p->nDivMux[0]++; + else if ( Value == 1 ) + p->nDivMux[1]++; else - printf( "Add " ); - Fx_PrintDivOne( p->vFree ); printf( "\n" ); + p->nDivMux[2]++; } -*/ -// if ( Vec_IntSize(p->vFree) == 4 ) -// Fx_ManDivCanonicize( p->vFree ); - iDiv = Hsh_VecManAdd( p->pHash, p->vFree ); + iDiv = Hsh_VecManAdd( p->pHash, p->vCubeFree ); if ( !fRemove ) { if ( iDiv == Vec_FltSize(p->vWeights) ) - Vec_FltPush(p->vWeights, -Vec_IntSize(p->vFree)); + Vec_FltPush(p->vWeights, -Vec_IntSize(p->vCubeFree)); assert( iDiv < Vec_FltSize(p->vWeights) ); - Vec_FltAddToEntry( p->vWeights, iDiv, Base + Vec_IntSize(p->vFree) - 1 ); + Vec_FltAddToEntry( p->vWeights, iDiv, Base + Vec_IntSize(p->vCubeFree) - 1 ); p->nPairsD++; } else { assert( iDiv < Vec_FltSize(p->vWeights) ); - Vec_FltAddToEntry( p->vWeights, iDiv, -(Base + Vec_IntSize(p->vFree) - 1) ); + Vec_FltAddToEntry( p->vWeights, iDiv, -(Base + Vec_IntSize(p->vCubeFree) - 1) ); p->nPairsD--; } if ( fUpdate ) @@ -736,7 +782,7 @@ void Fx_ManCreateDivisors( Fx_Man_t * p ) /**Function************************************************************* - Synopsis [] + Synopsis [Compress the cubes by removing unused ones.] Description [] @@ -745,44 +791,19 @@ void Fx_ManCreateDivisors( Fx_Man_t * p ) SeeAlso [] ***********************************************************************/ -Fx_Man_t * Fx_ManStart( Vec_Wec_t * vCubes ) -{ - Fx_Man_t * p; - p = ABC_CALLOC( Fx_Man_t, 1 ); - 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 ) +static inline void Fx_ManCompressCubes( Vec_Wec_t * vCubes, Vec_Int_t * vLit2Cube ) { -// Vec_WecFree( p->vCubes ); - Vec_WecFree( p->vLits ); - Vec_IntFree( p->vCounts ); - 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 ); + 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 ); } + /**Function************************************************************* - Synopsis [] + Synopsis [Find command cube pairs.] Description [] @@ -791,27 +812,20 @@ void Fx_ManStop( Fx_Man_t * p ) SeeAlso [] ***********************************************************************/ -static inline void Fx_ManCompressCubes( Vec_Wec_t * vCubes, Vec_Int_t * vLit2Cube ) -{ - 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 ) +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 * vCompls, Vec_Int_t * vDiv, Vec_Int_t * vCubeFree ) { 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_; + int i, k, i_, k_, fCompl, CubeId1, CubeId2; Vec_IntClear( vPairs ); + Vec_IntClear( vCompls ); while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) { - int CubeId1 = Fx_ManGetCubeVar(vCubes, *pBeg1); - int CubeId2 = Fx_ManGetCubeVar(vCubes, *pBeg2); + CubeId1 = Fx_ManGetCubeVar(vCubes, *pBeg1); + CubeId2 = Fx_ManGetCubeVar(vCubes, *pBeg2); if ( CubeId1 == CubeId2 ) { for ( i = 1; pBeg1+i < pEnd1; i++ ) @@ -825,11 +839,13 @@ void Fx_ManFindCommonPairs( Vec_Wec_t * vCubes, Vec_Int_t * vPart0, Vec_Int_t * { if ( pBeg1[i_] == pBeg2[k_] ) continue; - Fx_ManDivFindCubeFree( Vec_WecEntry(vCubes, pBeg1[i_]), Vec_WecEntry(vCubes, pBeg2[k_]), vFree ); - if ( !Vec_IntEqual( vDiv, vFree ) ) + Fx_ManDivFindCubeFree( Vec_WecEntry(vCubes, pBeg1[i_]), Vec_WecEntry(vCubes, pBeg2[k_]), vCubeFree ); + fCompl = (Vec_IntSize(vCubeFree) == 4 && Fx_ManDivNormalize(vCubeFree) == 1); + if ( !Vec_IntEqual( vDiv, vCubeFree ) ) continue; Vec_IntPush( vPairs, pBeg1[i_] ); Vec_IntPush( vPairs, pBeg2[k_] ); + Vec_IntPush( vCompls, fCompl ); } pBeg1 += i; pBeg2 += k; @@ -843,7 +859,7 @@ void Fx_ManFindCommonPairs( Vec_Wec_t * vCubes, Vec_Int_t * vPart0, Vec_Int_t * /**Function************************************************************* - Synopsis [Updates the data-structure when divisor is selected.] + Synopsis [Updates the data-structure when one divisor is selected.] Description [] @@ -857,11 +873,12 @@ 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; - // get the divisor + int i, k, Lit0, Lit1, iVarNew, fComplAny, RetValue; + + // get the divisor and select pivot variables + p->nDivs++; Vec_IntClear( vDiv ); Vec_IntAppend( vDiv, Hsh_VecReadEntry(p->pHash, iDiv) ); - // select pivot variables Fx_ManDivFindPivots( vDiv, &Lit0, &Lit1 ); assert( Lit0 >= 0 && Lit1 >= 0 ); @@ -873,13 +890,11 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) 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 ); + Fx_ManFindCommonPairs( p->vCubes, Vec_WecEntry(p->vLits, Lit0), Vec_WecEntry(p->vLits, Lit1), p->vCubesD, p->vCompls, vDiv, p->vCubeFree ); // subtract cost of single-cube divisors Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i ) @@ -937,18 +952,24 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) } // create updated double-cube divisor cube pairs k = 0; + fComplAny = 0; assert( Vec_IntSize(p->vCubesD) % 2 == 0 ); - Fx_ManForEachPairVec( p->vCubesD, p->vCubes, vCube, vCube2, i ) + assert( Vec_IntSize(p->vCubesD) == 2 * Vec_IntSize(p->vCompls) ); + for ( i = 0; i < Vec_IntSize(p->vCubesD); i += 2 ) { - RetValue = Fx_ManDivRemoveLits( vCube, vDiv ); // cube 2*i - RetValue += Fx_ManDivRemoveLits( vCube2, vDiv ); // cube 2*i+1 + int fCompl = Vec_IntEntry(p->vCompls, i/2); + fComplAny |= fCompl; + vCube = Vec_WecEntry( p->vCubes, Vec_IntEntry(p->vCubesD, i) ); + vCube2 = Vec_WecEntry( p->vCubes, Vec_IntEntry(p->vCubesD, i+1) ); + RetValue = Fx_ManDivRemoveLits( vCube, vDiv, fCompl ); // cube 2*i + RetValue += Fx_ManDivRemoveLits( vCube2, vDiv, fCompl ); // cube 2*i+1 assert( RetValue == Vec_IntSize(vDiv) ); - if ( Vec_IntSize(vDiv) == 2 ) + if ( Vec_IntSize(vDiv) == 2 || fCompl ) { Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 1) ); Vec_IntPush( vLitN, Vec_WecLevelId(p->vCubes, vCube) ); } - else + else { Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 0) ); Vec_IntPush( vLitP, Vec_WecLevelId(p->vCubes, vCube) ); @@ -997,9 +1018,14 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) // 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 + if ( fComplAny && i > 1 ) // the last two lits are possibly complemented + Vec_IntTwoRemove( Vec_WecEntry(p->vLits, Abc_LitNot(Abc_Lit2Var(Lit0))), p->vCubesD ); + } + + // check predicted improvement: (new SOP lits == old SOP lits - divisor weight) + assert( p->nLits == nLitsNew ); } /**Function************************************************************* @@ -1029,6 +1055,7 @@ int Fx_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose ) if ( fVerbose ) Fx_PrintStats( p, clock() - clk ); // perform extraction + p->timeStart = clock(); while ( Vec_QueTopCost(p->vPrio) > 0.0 ) { int iDiv = Vec_QuePop(p->vPrio); @@ -1037,8 +1064,6 @@ int Fx_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose ) Fx_ManUpdate( p, iDiv ); if ( fVeryVerbose ) Fx_PrintMatrix( p ); - if ( fVerbose ) - Fx_PrintStats( p, clock() - clk ); } Fx_ManStop( p ); // return the result -- cgit v1.2.3