diff options
Diffstat (limited to 'src/base/abci/abcFx.c')
| -rw-r--r-- | src/base/abci/abcFx.c | 733 |
1 files changed, 733 insertions, 0 deletions
diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c new file mode 100644 index 00000000..8f1c724a --- /dev/null +++ b/src/base/abci/abcFx.c @@ -0,0 +1,733 @@ +/**CFile**************************************************************** + + FileName [abcFx.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Interface with the fast extract package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 26, 2013.] + + Revision [$Id: abcFx.c,v 1.00 2013/04/26 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "base/abc/abc.h" +#include "misc/vec/vecWec.h" +#include "misc/vec/vecQue.h" +#include "misc/vec/vecHsh.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern int Fx_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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( 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************************************************************* + + Synopsis [Extracts SOP information.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wec_t * Abc_NtkFxExtract( Abc_Ntk_t * pNtk ) +{ + Vec_Wec_t * vCubes; + Vec_Int_t * vCube; + Abc_Obj_t * pNode; + char * pCube, * pSop; + int nVars, i, v, Lit; + assert( Abc_NtkIsSopLogic(pNtk) ); + vCubes = Vec_WecAlloc( 1000 ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + pSop = (char *)pNode->pData; + nVars = Abc_SopGetVarNum(pSop); + assert( nVars == Abc_ObjFaninNum(pNode) ); + if ( nVars < 2 ) + continue; + Abc_SopForEachCube( pSop, nVars, pCube ) + { + vCube = Vec_WecPushLevel( vCubes ); + Vec_IntPush( vCube, Abc_ObjId(pNode) ); + Abc_CubeForEachVar( pCube, Lit, v ) + { + if ( Lit == '0' ) + Vec_IntPush( vCube, Abc_Var2Lit(Abc_ObjFaninId(pNode, v), 1) ); + else if ( Lit == '1' ) + Vec_IntPush( vCube, Abc_Var2Lit(Abc_ObjFaninId(pNode, v), 0) ); + } + Vec_IntSelectSort( Vec_IntArray(vCube) + 1, Vec_IntSize(vCube) - 1 ); + } + } + return vCubes; +} + +/**Function************************************************************* + + Synopsis [Inserts SOP information.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFxInsert( Abc_Ntk_t * pNtk, Vec_Wec_t * vCubes ) +{ + Vec_Int_t * vCube, * vPres, * vFirst, * vCount; + Abc_Obj_t * pNode, * pFanin; + char * pCube, * pSop; + int i, k, v, Lit, iFanin, iNodeMax = 0; + assert( Abc_NtkIsSopLogic(pNtk) ); + // check that cubes have no gaps and are ordered by first node + Lit = -1; + Vec_WecForEachLevel( vCubes, vCube, i ) + { + assert( Vec_IntSize(vCube) > 0 ); + assert( Lit <= Vec_IntEntry(vCube, 0) ); + Lit = Vec_IntEntry(vCube, 0); + } + // find the largest index + Vec_WecForEachLevel( vCubes, vCube, i ) + iNodeMax = Abc_MaxInt( iNodeMax, Vec_IntEntry(vCube, 0) ); + // quit if nothing new +/* + 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++ ) + { + pNode = Abc_NtkCreateNode( pNtk ); + assert( i == (int)Abc_ObjId(pNode) ); + } + // create node fanins + vFirst = Vec_IntStart( Abc_NtkObjNumMax(pNtk) ); + vCount = Vec_IntStart( Abc_NtkObjNumMax(pNtk) ); + Vec_WecForEachLevel( vCubes, vCube, i ) + { + iFanin = Vec_IntEntry( vCube, 0 ); + if ( Vec_IntEntry(vCount, iFanin) == 0 ) + Vec_IntWriteEntry( vFirst, iFanin, i ); + Vec_IntAddToEntry( vCount, iFanin, 1 ); + } + // create node SOPs + vPres = Vec_IntStartFull( Abc_NtkObjNumMax(pNtk) ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + if ( Vec_IntEntry(vCount, i) == 0 ) + { + assert( Abc_ObjFaninNum(pNode) < 2 ); + continue; + } + Abc_ObjRemoveFanins( pNode ); + // create fanins + assert( Vec_IntEntry(vCount, i) > 0 ); + for ( k = 0; k < Vec_IntEntry(vCount, i); k++ ) + { + vCube = Vec_WecEntry( vCubes, Vec_IntEntry(vFirst, i) + k ); + assert( Vec_IntEntry( vCube, 0 ) == i ); + Vec_IntForEachEntryStart( vCube, Lit, v, 1 ) + { + pFanin = Abc_NtkObj(pNtk, Abc_Lit2Var(Lit)); + if ( Vec_IntEntry(vPres, Abc_ObjId(pFanin)) >= 0 ) + continue; + Vec_IntWriteEntry(vPres, Abc_ObjId(pFanin), Abc_ObjFaninNum(pNode)); + Abc_ObjAddFanin( pNode, pFanin ); + } + } + // create SOP + pSop = pCube = Abc_SopStart( pNtk->pManFunc, Vec_IntEntry(vCount, i), Abc_ObjFaninNum(pNode) ); + for ( k = 0; k < Vec_IntEntry(vCount, i); k++ ) + { + vCube = Vec_WecEntry( vCubes, Vec_IntEntry(vFirst, i) + k ); + assert( Vec_IntEntry( vCube, 0 ) == i ); + Vec_IntForEachEntryStart( vCube, Lit, v, 1 ) + { + pFanin = Abc_NtkObj(pNtk, Abc_Lit2Var(Lit)); + iFanin = Vec_IntEntry(vPres, Abc_ObjId(pFanin)); + assert( iFanin >= 0 && iFanin < Abc_ObjFaninNum(pNode) ); + pCube[iFanin] = Abc_LitIsCompl(Lit) ? '0' : '1'; + } + pCube += Abc_ObjFaninNum(pNode) + 3; + } + if ( Abc_SopIsComplement((char *)pNode->pData) ) + Abc_SopComplement( pSop ); + pNode->pData = pSop; + // clean fanins + Abc_ObjForEachFanin( pNode, pFanin, v ) + Vec_IntWriteEntry( vPres, Abc_ObjId(pFanin), -1 ); + } + Vec_IntFree( vFirst ); + Vec_IntFree( vCount ); + Vec_IntFree( vPres ); +} + +/**Function************************************************************* + + Synopsis [Makes sure the nodes do not have complemented and duplicated fanins.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkFxCheck( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i; +// Abc_NtkForEachObj( pNtk, pNode, i ) +// Abc_ObjPrint( stdout, pNode ); + Abc_NtkForEachNode( pNtk, pNode, i ) + if ( !Vec_IntCheckUniqueSmall( &pNode->vFanins ) ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int fVerbose ) +{ + Vec_Wec_t * vCubes; + assert( Abc_NtkIsSopLogic(pNtk) ); + // check unique fanins + if ( !Abc_NtkFxCheck(pNtk) ) + { + printf( "Abc_NtkFastExtract: Nodes have duplicated fanins. FX is not performed.\n" ); + return 0; + } + // sweep removes useless nodes + Abc_NtkCleanup( pNtk, 0 ); +// Abc_NtkOrderFanins( pNtk ); + // collect information about the covers + vCubes = Abc_NtkFxExtract( pNtk ); + // call the fast extract procedure + if ( Fx_FastExtract( vCubes, Abc_NtkObjNumMax(pNtk), fVerbose ) > 0 ) + { + // update the network + Abc_NtkFxInsert( pNtk, vCubes ); + Vec_WecFree( vCubes ); + if ( !Abc_NtkCheck( pNtk ) ) + printf( "Abc_NtkFxPerform: The network check has failed.\n" ); + return 1; + } + else + printf( "Warning: The network has not been changed by \"fx\".\n" ); + Vec_WecFree( vCubes ); + return 0; +} + + + + +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; +}; + +/**Function************************************************************* + + Synopsis [Create literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fx_ManDivCanonicize( Vec_Int_t * vFree ) // return 1 if complemented +{ + 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; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vFree ) +{ + int * pBeg1 = vArr1->pArray + 1; + int * pBeg2 = vArr2->pArray + 1; + int * pEnd1 = vArr1->pArray + vArr1->nSize; + int * pEnd2 = vArr2->pArray + vArr2->nSize; + int Counter = 0, fAttr0 = 0, fAttr1 = 1; + Vec_IntClear( vFree ); + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + if ( *pBeg1 == *pBeg2 ) + pBeg1++, pBeg2++, Counter++; + else if ( *pBeg1 < *pBeg2 ) + Vec_IntPush( vFree, Abc_Var2Lit(*pBeg1++, fAttr0) ); + else + { + if ( Vec_IntSize(vFree) == 0 ) + fAttr0 = 1, fAttr1 = 0; + Vec_IntPush( vFree, Abc_Var2Lit(*pBeg2++, fAttr1) ); + } + } + while ( pBeg1 < pEnd1 ) + Vec_IntPush( vFree, Abc_Var2Lit(*pBeg1++, fAttr0) ); + while ( pBeg2 < pEnd2 ) + Vec_IntPush( vFree, Abc_Var2Lit(*pBeg2++, fAttr1) ); + assert( Vec_IntSize(vFree) > 1 ); + assert( !Abc_LitIsCompl(Vec_IntEntry(vFree, 0)) ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wec_t * Fx_ManCreateLiterals( Vec_Wec_t * vCubes, Vec_Int_t ** pvCounts ) +{ + 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 ) + { + 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; + } + Vec_IntFree( vFree ); + *pvWeights = vWeights; + return p; +} +Vec_Que_t * Fx_ManCreateQueue( Vec_Flt_t * vWeights ) +{ + 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; +} + +/**Function************************************************************* + + Synopsis [Removes 0-size cubes and sorts them by the first entry.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Vec_WecSortSpecial( 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 ); +} + + +/**Function************************************************************* + + Synopsis [Updates the data-structure when divisor is selected.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) +{ +// 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) +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fx_Man_t * Fx_ManStart( Vec_Wec_t * vCubes, int nVars ) +{ + 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 ); + 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->vCube ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Fx_PrintMatrix( Vec_Wec_t * vCubes, int nObjs ) +{ + 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 ) + { + 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 ); +} +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 ) +{ + 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 [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fx_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose ) +{ + Fx_Man_t * p; + clock_t clk = clock(); + p = Fx_ManStart( vCubes, nVars ); + + if ( fVerbose ) + { + Fx_PrintMatrix( vCubes, nVars ); + Fx_PrintDivisors( p ); + printf( "Selecting divisors:\n" ); + } + + Fx_PrintStats( p, clock() - clk ); + while ( Vec_QueTopCost(p->vPrio) > 0.0 ) + { + int iDiv = Vec_QuePop(p->vPrio); + if ( fVerbose ) + Fx_PrintDiv( p, iDiv ); + Fx_ManUpdate( p, iDiv ); + } + + Fx_ManStop( p ); + return 1; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |