From 324d73c29a22766063df46f9e35a3cbe719a83c2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 27 Apr 2013 15:23:12 -0700 Subject: New fast extract. --- abclib.dsp | 12 + src/base/abci/abc.c | 23 +- src/base/abci/abcFx.c | 733 ++++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/module.make | 1 + src/misc/vec/vecHsh.h | 360 +++++++++++++++++++++++ src/misc/vec/vecInt.h | 18 ++ src/misc/vec/vecQue.h | 4 + src/misc/vec/vecVec.h | 3 +- src/misc/vec/vecWec.h | 476 ++++++++++++++++++++++++++++++ src/proof/abs/absGla.c | 21 -- src/proof/ssc/sscUtil.c | 100 ------- 11 files changed, 1624 insertions(+), 127 deletions(-) create mode 100644 src/base/abci/abcFx.c create mode 100644 src/misc/vec/vecHsh.h create mode 100644 src/misc/vec/vecWec.h diff --git a/abclib.dsp b/abclib.dsp index f636f2eb..c7883f1f 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -259,6 +259,10 @@ SOURCE=.\src\base\abci\abcFraig.c # End Source File # Begin Source File +SOURCE=.\src\base\abci\abcFx.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abci\abcFxu.c # End Source File # Begin Source File @@ -2651,6 +2655,10 @@ SOURCE=.\src\misc\vec\vecFlt.h # End Source File # Begin Source File +SOURCE=.\src\misc\vec\vecHsh.h +# End Source File +# Begin Source File + SOURCE=.\src\misc\vec\vecInt.h # End Source File # Begin Source File @@ -2679,6 +2687,10 @@ SOURCE=.\src\misc\vec\vecVec.h # End Source File # Begin Source File +SOURCE=.\src\misc\vec\vecWec.h +# End Source File +# Begin Source File + SOURCE=.\src\misc\vec\vecWrd.h # End Source File # End Group diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 533db448..2f785a22 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3527,13 +3527,14 @@ usage: ***********************************************************************/ 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; + int c, fNewAlgo = 0; // set the defaults Abc_NtkSetDefaultParams( p ); Extra_UtilGetoptReset(); - while ( (c = Extra_UtilGetopt(argc, argv, "SDNWsdzcvh")) != EOF ) + while ( (c = Extra_UtilGetopt(argc, argv, "SDNWsdzcnvh")) != EOF ) { switch (c) { @@ -3593,6 +3594,9 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'c': p->fUseCompl ^= 1; break; + case 'n': + fNewAlgo ^= 1; + break; case 'v': p->fVerbose ^= 1; break; @@ -3615,17 +3619,25 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Abc_NtkIsLogic(pNtk) ) { - Abc_Print( -1, "Fast extract can only be applied to a logic network (run \"renode\").\n" ); + Abc_Print( -1, "Fast extract can only be applied to a logic network (run \"renode\" or \"if\").\n" ); + return 1; + } + if ( !Abc_NtkIsSopLogic(pNtk) ) + { + Abc_Print( -1, "Fast extract can only be applied to a logic network with SOP local functions (run \"bdd; sop\").\n" ); return 1; } // the nodes to be merged are linked into the special linked list - Abc_NtkFastExtract( pNtk, p ); + if ( fNewAlgo ) + Abc_NtkFxPerform( pNtk, p->fVerbose ); + else + Abc_NtkFastExtract( pNtk, p ); Abc_NtkFxuFreeInfo( p ); return 0; usage: - Abc_Print( -2, "usage: fx [-SDNW ] [-sdzcvh]\n"); + Abc_Print( -2, "usage: fx [-SDNW ] [-sdzcnvh]\n"); Abc_Print( -2, "\t performs unate fast extract on the current network\n"); Abc_Print( -2, "\t-S : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax ); Abc_Print( -2, "\t-D : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax ); @@ -3635,6 +3647,7 @@ usage: Abc_Print( -2, "\t-d : use only double-cube divisors [default = %s]\n", p->fOnlyD? "yes": "no" ); Abc_Print( -2, "\t-z : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" ); Abc_Print( -2, "\t-c : use complement in the binary case [default = %s]\n", p->fUseCompl? "yes": "no" ); + Abc_Print( -2, "\t-n : use new implementation of fast extract [default = %s]\n", fNewAlgo? "yes": "no" ); Abc_Print( -2, "\t-v : print verbose information [default = %s]\n", p->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; 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 + diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 7846b268..89e1849b 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -17,6 +17,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcDsd.c \ src/base/abci/abcExtract.c \ src/base/abci/abcFraig.c \ + src/base/abci/abcFx.c \ src/base/abci/abcFxu.c \ src/base/abci/abcGen.c \ src/base/abci/abcHaig.c \ diff --git a/src/misc/vec/vecHsh.h b/src/misc/vec/vecHsh.h new file mode 100644 index 00000000..04f1e9f2 --- /dev/null +++ b/src/misc/vec/vecHsh.h @@ -0,0 +1,360 @@ +/**CFile**************************************************************** + + FileName [vecHsh.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Resizable arrays.] + + Synopsis [Hashing vector entries.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: vecHsh.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__misc__vec__vecHsh_h +#define ABC__misc__vec__vecHsh_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Hsh_IntObj_t_ Hsh_IntObj_t; +struct Hsh_IntObj_t_ +{ + int iData; + int iNext; +}; + +typedef struct Hsh_IntMan_t_ Hsh_IntMan_t; +struct Hsh_IntMan_t_ +{ + int nSize; // data size + Vec_Int_t * vData; // data storage + Vec_Int_t * vTable; // hash table + Vec_Wrd_t * vObjs; // hash objects +}; + + + +typedef struct Hsh_VecObj_t_ Hsh_VecObj_t; +struct Hsh_VecObj_t_ +{ + int nSize; + int iNext; + int pArray[0]; +}; + +typedef struct Hsh_VecMan_t_ Hsh_VecMan_t; +struct Hsh_VecMan_t_ +{ + Vec_Int_t * vTable; // hash table + Vec_Int_t * vData; // data storage + Vec_Int_t * vMap; // mapping entries into data; + Vec_Int_t vTemp; // temporary array +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline unsigned * Hsh_IntData( Hsh_IntMan_t * p, int iData ) { return (unsigned *)Vec_IntEntryP( p->vData, p->nSize * iData ); } +static inline Hsh_IntObj_t * Hsh_IntObj( Hsh_IntMan_t * p, int iObj ) { return iObj == -1 ? NULL : (Hsh_IntObj_t *)Vec_WrdEntryP( p->vObjs, iObj ); } +static inline word Hsh_IntWord( int iData, int iNext ) { Hsh_IntObj_t Obj = {iData, iNext}; return *((word *)&Obj); } + +static inline Hsh_VecObj_t * Hsh_VecObj( Hsh_VecMan_t * p, int i ) { return i == -1 ? NULL : (Hsh_VecObj_t *)Vec_IntEntryP(p->vData, Vec_IntEntry(p->vMap, i)); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Hashing data entries composed of nSize integers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Hsh_IntMan_t * Hsh_IntManStart( Vec_Int_t * vData, int nSize, int nEntries ) +{ + Hsh_IntMan_t * p; + p = ABC_CALLOC( Hsh_IntMan_t, 1 ); + p->nSize = nSize; + p->vData = vData; + p->vTable = Vec_IntStartFull( Abc_PrimeCudd(nEntries) ); + p->vObjs = Vec_WrdAlloc( nEntries ); + return p; +} +static inline void Hsh_IntManStop( Hsh_IntMan_t * p ) +{ + Vec_IntFree( p->vTable ); + Vec_WrdFree( p->vObjs ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Hsh_IntManHash( unsigned * pData, int nSize, int nTableSize ) +{ + static int s_Primes[7] = { 4177, 5147, 5647, 6343, 7103, 7873, 8147 }; + unsigned char * pDataC = (unsigned char *)pData; + int c, nChars = nSize * 4; + unsigned Key = 0; + for ( c = 0; c < nChars; c++ ) + Key += pDataC[c] * s_Primes[c % 7]; + return (int)(Key % nTableSize); +} +static inline int Hsh_IntManAdd( Hsh_IntMan_t * p, int iData ) +{ + Hsh_IntObj_t * pObj; + unsigned * pData = Hsh_IntData( p, iData ); + int i, * pPlace; + if ( Vec_WrdSize(p->vObjs) > Vec_IntSize(p->vTable) ) + { + Vec_IntFill( p->vTable, Abc_PrimeCudd(2*Vec_IntSize(p->vTable)), -1 ); + for ( i = 0; i < Vec_WrdSize(p->vObjs); i++ ) + { + pPlace = Vec_IntEntryP( p->vTable, Hsh_IntManHash(Hsh_IntData(p, i), p->nSize, Vec_IntSize(p->vTable)) ); + Hsh_IntObj(p, i)->iNext = *pPlace; *pPlace = i; + } + } + pPlace = Vec_IntEntryP( p->vTable, Hsh_IntManHash(pData, p->nSize, Vec_IntSize(p->vTable)) ); + for ( ; (pObj = Hsh_IntObj(p, *pPlace)); pPlace = &pObj->iNext ) + if ( !memcmp( pData, Hsh_IntData(p, pObj->iData), sizeof(int) * p->nSize ) ) + return (word *)pObj - Vec_WrdArray(p->vObjs); + *pPlace = Vec_WrdSize(p->vObjs); + Vec_WrdPush( p->vObjs, Hsh_IntWord(iData, -1) ); + return Vec_WrdSize(p->vObjs)-1; +} + +/**Function************************************************************* + + Synopsis [Hashes data by value.] + + Description [Array vData contains data entries, each of 'nSize' integers. + The resulting array contains the indexes of unique data entries.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Int_t * Hsh_IntManHashArray( Vec_Int_t * vData, int nSize ) +{ + Hsh_IntMan_t * p; + Vec_Int_t * vRes = Vec_IntAlloc( 100 ); + int i, nEntries = Vec_IntSize(vData) / nSize; + assert( Vec_IntSize(vData) % nSize == 0 ); + p = Hsh_IntManStart( vData, nSize, nEntries ); + for ( i = 0; i < nEntries; i++ ) + Vec_IntPush( vRes, Hsh_IntManAdd(p, i) ); + Hsh_IntManStop( p ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Test procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Hsh_IntManHashArrayTest() +{ + Vec_Int_t * vData = Vec_IntAlloc( 10 ); + Vec_Int_t * vRes; + Vec_IntPush( vData, 12 ); + Vec_IntPush( vData, 17 ); + Vec_IntPush( vData, 13 ); + Vec_IntPush( vData, 12 ); + Vec_IntPush( vData, 15 ); + Vec_IntPush( vData, 3 ); + Vec_IntPush( vData, 16 ); + Vec_IntPush( vData, 16 ); + Vec_IntPush( vData, 12 ); + Vec_IntPush( vData, 17 ); + Vec_IntPush( vData, 12 ); + Vec_IntPush( vData, 12 ); + + vRes = Hsh_IntManHashArray( vData, 2 ); + + Vec_IntPrint( vData ); + Vec_IntPrint( vRes ); + + Vec_IntFree( vData ); + Vec_IntFree( vRes ); +} + + + + + +/**Function************************************************************* + + Synopsis [Hashing integer arrays.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Hsh_VecMan_t * Hsh_VecManStart( int nEntries ) +{ + Hsh_VecMan_t * p; + p = ABC_CALLOC( Hsh_VecMan_t, 1 ); + p->vTable = Vec_IntStartFull( Abc_PrimeCudd(nEntries) ); + p->vData = Vec_IntAlloc( nEntries * 4 ); + p->vMap = Vec_IntAlloc( nEntries ); + return p; +} +static inline void Hsh_VecManStop( Hsh_VecMan_t * p ) +{ + Vec_IntFree( p->vTable ); + Vec_IntFree( p->vData ); + Vec_IntFree( p->vMap ); + ABC_FREE( p ); +} +static inline Vec_Int_t * Hsh_VecReadEntry( Hsh_VecMan_t * p, int i ) +{ + Hsh_VecObj_t * pObj = Hsh_VecObj( p, i ); + p->vTemp.nSize = p->vTemp.nCap = pObj->nSize; + p->vTemp.pArray = (int*)pObj + 2; + return &p->vTemp; +} +static inline int Hsh_VecSize( Hsh_VecMan_t * p ) +{ + return Vec_IntSize(p->vMap); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Hsh_VecManHash( Vec_Int_t * vVec, int nTableSize ) +{ + static unsigned s_Primes[7] = {4177, 5147, 5647, 6343, 7103, 7873, 8147}; + unsigned Key = 0; + int i, Entry; + Vec_IntForEachEntry( vVec, Entry, i ) + Key += (unsigned)Entry * s_Primes[i % 7]; + return (int)(Key % nTableSize); +} +static inline int Hsh_VecManAdd( Hsh_VecMan_t * p, Vec_Int_t * vVec ) +{ + Hsh_VecObj_t * pObj; + int i, Ent, * pPlace; + if ( Vec_IntSize(p->vMap) > Vec_IntSize(p->vTable) ) + { + Vec_IntFill( p->vTable, Abc_PrimeCudd(2*Vec_IntSize(p->vTable)), -1 ); + for ( i = 0; i < Vec_IntSize(p->vMap); i++ ) + { + pPlace = Vec_IntEntryP( p->vTable, Hsh_VecManHash(Hsh_VecReadEntry(p, i), Vec_IntSize(p->vTable)) ); + Hsh_VecObj(p, i)->iNext = *pPlace; *pPlace = i; + } + } + pPlace = Vec_IntEntryP( p->vTable, Hsh_VecManHash(vVec, Vec_IntSize(p->vTable)) ); + for ( ; (pObj = Hsh_VecObj(p, *pPlace)); pPlace = &pObj->iNext ) + if ( pObj->nSize == Vec_IntSize(vVec) && !memcmp( pObj->pArray, Vec_IntArray(vVec), sizeof(int) * pObj->nSize ) ) + return *pPlace; + *pPlace = Vec_IntSize(p->vMap); + assert( Vec_IntSize(p->vData) % 2 == 0 ); + Vec_IntPush( p->vMap, Vec_IntSize(p->vData) ); + Vec_IntPush( p->vData, Vec_IntSize(vVec) ); + Vec_IntPush( p->vData, -1 ); + Vec_IntForEachEntry( vVec, Ent, i ) + Vec_IntPush( p->vData, Ent ); + if ( Vec_IntSize(vVec) & 1 ) + Vec_IntPush( p->vData, -1 ); + return Vec_IntSize(p->vMap) - 1; +} + +/**Function************************************************************* + + Synopsis [Test procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Hsh_VecManHashTest() +{ + Hsh_VecMan_t * p; + Vec_Int_t * vTemp; + Vec_Int_t * vRes = Vec_IntAlloc( 1000 ); + int i; + + p = Hsh_VecManStart( 5 ); + for ( i = 0; i < 20; i++ ) + { + vTemp = Vec_IntStartNatural( i ); + Vec_IntPush( vRes, Hsh_VecManAdd( p, vTemp ) ); + Vec_IntFree( vTemp ); + } + for ( ; i > 0; i-- ) + { + vTemp = Vec_IntStartNatural( i ); + Vec_IntPush( vRes, Hsh_VecManAdd( p, vTemp ) ); + Vec_IntFree( vTemp ); + } + Vec_IntPrint( vRes ); + Vec_IntFree( vRes ); + + Hsh_VecManStop( p ); +} + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 9744a031..60352a0f 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -1193,6 +1193,24 @@ static inline int Vec_IntUniqify( Vec_Int_t * p ) p->nSize = k; return RetValue; } +static inline int Vec_IntCountDuplicates( Vec_Int_t * p ) +{ + int RetValue; + Vec_Int_t * pDup = Vec_IntDup( p ); + Vec_IntUniqify( pDup ); + RetValue = Vec_IntSize(p) - Vec_IntSize(pDup); + Vec_IntFree( pDup ); + return RetValue; +} +static inline int Vec_IntCheckUniqueSmall( Vec_Int_t * p ) +{ + int i, k; + for ( i = 0; i < p->nSize; i++ ) + for ( k = i+1; k < p->nSize; k++ ) + if ( p->pArray[i] == p->pArray[k] ) + return 0; + return 1; +} /**Function************************************************************* diff --git a/src/misc/vec/vecQue.h b/src/misc/vec/vecQue.h index aaa1c01d..1b6bc4bb 100644 --- a/src/misc/vec/vecQue.h +++ b/src/misc/vec/vecQue.h @@ -140,6 +140,10 @@ static inline int Vec_QueTop( Vec_Que_t * p ) { return Vec_QueSize(p) > 0 ? p->pHeap[1] : -1; } +static inline float Vec_QueTopCost( Vec_Que_t * p ) +{ + return Vec_QueSize(p) > 0 ? Vec_QueCost(p, p->pHeap[1]) : -ABC_INFINITY; +} /**Function************************************************************* diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h index d935be0f..f8f36d8b 100644 --- a/src/misc/vec/vecVec.h +++ b/src/misc/vec/vecVec.h @@ -253,6 +253,7 @@ static inline int Vec_VecCap( Vec_Vec_t * p ) ***********************************************************************/ static inline int Vec_VecLevelSize( Vec_Vec_t * p, int i ) { + assert( i >= 0 && i < p->nSize ); return Vec_PtrSize( (Vec_Ptr_t *)p->pArray[i] ); } @@ -617,7 +618,7 @@ static inline void Vec_VecPrintInt( Vec_Vec_t * p, int fSkipSingles ) int i, k, Entry; Vec_VecForEachEntryInt( p, Entry, i, k ) { - if ( Vec_VecLevelSize(p, i) == 1 ) + if ( fSkipSingles && Vec_VecLevelSize(p, i) == 1 ) break; if ( k == 0 ) printf( " %4d : {", i ); diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h new file mode 100644 index 00000000..49ecb3da --- /dev/null +++ b/src/misc/vec/vecWec.h @@ -0,0 +1,476 @@ +/**CFile**************************************************************** + + FileName [vecWec.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Resizable arrays.] + + Synopsis [Resizable vector of resizable vectors.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: vecWec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__misc__vec__vecWec_h +#define ABC__misc__vec__vecWec_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Vec_Wec_t_ Vec_Wec_t; +struct Vec_Wec_t_ +{ + int nCap; + int nSize; + Vec_Int_t * pArray; +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +// 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_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 ) \ + for ( i = 0; (i < LevelStop) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i++ ) +#define Vec_WecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \ + for ( i = LevelStart; (i < LevelStop) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i++ ) +#define Vec_WecForEachLevelReverse( vGlob, vVec, i ) \ + for ( i = Vec_WecSize(vGlob)-1; (i >= 0) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i-- ) +#define Vec_WecForEachLevelReverseStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \ + for ( i = LevelStart-1; (i >= LevelStop) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i-- ) +#define Vec_WecForEachLevelTwo( vGlob1, vGlob2, vVec1, vVec2, i ) \ + for ( i = 0; (i < Vec_WecSize(vGlob1)) && (((vVec1) = Vec_WecEntry(vGlob1, i)), 1) && (((vVec2) = Vec_WecEntry(vGlob2, i)), 1); i++ ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates a vector with the given capacity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Wec_t * Vec_WecAlloc( int nCap ) +{ + Vec_Wec_t * p; + p = ABC_ALLOC( Vec_Wec_t, 1 ); + if ( nCap > 0 && nCap < 8 ) + nCap = 8; + p->nSize = 0; + p->nCap = nCap; + p->pArray = p->nCap? ABC_CALLOC( Vec_Int_t, p->nCap ) : NULL; + return p; +} +static inline Vec_Wec_t * Vec_WecStart( int nSize ) +{ + Vec_Wec_t * p; + p = Vec_WecAlloc( nSize ); + p->nSize = nSize; + return p; +} + +/**Function************************************************************* + + Synopsis [Resizes the vector to the given capacity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_WecGrow( Vec_Wec_t * p, int nCapMin ) +{ + if ( p->nCap >= nCapMin ) + return; + p->pArray = ABC_REALLOC( Vec_Int_t, p->pArray, nCapMin ); + memset( p->pArray + p->nCap, 0, sizeof(Vec_Int_t) * (nCapMin - p->nCap) ); + p->nCap = nCapMin; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Int_t * Vec_WecEntry( Vec_Wec_t * p, int i ) +{ + assert( i >= 0 && i < p->nSize ); + return p->pArray + i; +} +static inline Vec_Int_t * Vec_WecEntryLast( Vec_Wec_t * p ) +{ + assert( p->nSize > 0 ); + return p->pArray + p->nSize - 1; +} +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 int Vec_WecCap( Vec_Wec_t * p ) +{ + return p->nCap; +} +static inline int Vec_WecSize( Vec_Wec_t * p ) +{ + return p->nSize; +} +static inline int Vec_WecLevelSize( Vec_Wec_t * p, int i ) +{ + assert( i >= 0 && i < p->nSize ); + return Vec_IntSize( p->pArray + i ); +} +static inline int Vec_WecSizeSize( Vec_Wec_t * p ) +{ + Vec_Int_t * vVec; + int i, Counter = 0; + Vec_WecForEachLevel( p, vVec, i ) + Counter += Vec_IntSize(vVec); + return Counter; +} +static inline int Vec_WecSizeUsed( Vec_Wec_t * p ) +{ + Vec_Int_t * vVec; + int i, Counter = 0; + Vec_WecForEachLevel( p, vVec, i ) + Counter += (int)(Vec_IntSize(vVec) > 0); + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_WecShrink( Vec_Wec_t * p, int nSizeNew ) +{ + assert( p->nSize >= nSizeNew ); + p->nSize = nSizeNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_WecClear( Vec_Wec_t * p ) +{ + Vec_Int_t * vVec; + int i; + Vec_WecForEachLevel( p, vVec, i ) + Vec_IntClear( vVec ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_WecPush( Vec_Wec_t * p, int Level, int Entry ) +{ + if ( p->nSize < Level + 1 ) + { + Vec_WecGrow( p, 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 ); + return Vec_WecEntryLast( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline double Vec_WecMemory( Vec_Wec_t * p ) +{ + int i; + double Mem; + if ( p == NULL ) return 0.0; + Mem = sizeof(Vec_Int_t) * Vec_WecCap(p); + for ( i = 0; i < p->nSize; i++ ) + Mem += sizeof(int) * Vec_IntCap( Vec_WecEntry(p, i) ); + return Mem; +} + +/**Function************************************************************* + + Synopsis [Frees the vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_WecFree( Vec_Wec_t * p ) +{ + Vec_Int_t * vVec; + int i; + Vec_WecForEachLevel( p, vVec, i ) + ABC_FREE( vVec->pArray ); + ABC_FREE( p->pArray ); + ABC_FREE( p ); +} +static inline void Vec_WecFreeP( Vec_Wec_t ** p ) +{ + if ( *p == NULL ) + return; + Vec_WecFree( *p ); + *p = NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_WecPushUnique( Vec_Wec_t * p, int Level, int Entry ) +{ + if ( p->nSize < Level + 1 ) + Vec_WecPush( p, Level, Entry ); + else + Vec_IntPushUnique( Vec_WecEntry(p, Level), Entry ); +} + +/**Function************************************************************* + + Synopsis [Frees the vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Wec_t * Vec_WecDup( Vec_Wec_t * p ) +{ + Vec_Wec_t * vNew; + Vec_Int_t * vVec; + int i, k, Entry; + vNew = Vec_WecAlloc( Vec_WecSize(p) ); + Vec_WecForEachLevel( p, vVec, i ) + Vec_IntForEachEntry( vVec, Entry, k ) + Vec_WecPush( vNew, i, Entry ); + return vNew; +} + +/**Function************************************************************* + + Synopsis [Comparison procedure for two arrays.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int Vec_WecSortCompare1( Vec_Int_t * p1, Vec_Int_t * p2 ) +{ + if ( Vec_IntSize(p1) < Vec_IntSize(p2) ) + return -1; + if ( Vec_IntSize(p1) > Vec_IntSize(p2) ) + return 1; + return 0; +} +static int Vec_WecSortCompare2( Vec_Int_t * p1, Vec_Int_t * p2 ) +{ + if ( Vec_IntSize(p1) > Vec_IntSize(p2) ) + return -1; + if ( Vec_IntSize(p1) < Vec_IntSize(p2) ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Sorting the entries by their integer value.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_WecSort( Vec_Wec_t * p, int fReverse ) +{ + if ( fReverse ) + qsort( (void *)p->pArray, p->nSize, sizeof(Vec_Int_t), + (int (*)(const void *, const void *)) Vec_WecSortCompare2 ); + else + qsort( (void *)p->pArray, p->nSize, sizeof(Vec_Int_t), + (int (*)(const void *, const void *)) Vec_WecSortCompare1 ); +} + +/**Function************************************************************* + + Synopsis [Comparison procedure for two integers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int Vec_WecSortCompare3( Vec_Int_t * p1, Vec_Int_t * p2 ) +{ + if ( Vec_IntEntry(p1,0) < Vec_IntEntry(p2,0) ) + return -1; + if ( Vec_IntEntry(p1,0) > Vec_IntEntry(p2,0) ) + return 1; + return 0; +} +static int Vec_WecSortCompare4( Vec_Int_t * p1, Vec_Int_t * p2 ) +{ + if ( Vec_IntEntry(p1,0) > Vec_IntEntry(p2,0) ) + return -1; + if ( Vec_IntEntry(p1,0) < Vec_IntEntry(p2,0) ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Sorting the entries by their integer value.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_WecSortByFirstInt( Vec_Wec_t * p, int fReverse ) +{ + if ( fReverse ) + qsort( (void *)p->pArray, p->nSize, sizeof(Vec_Int_t), + (int (*)(const void *, const void *)) Vec_WecSortCompare4 ); + else + qsort( (void *)p->pArray, p->nSize, sizeof(Vec_Int_t), + (int (*)(const void *, const void *)) Vec_WecSortCompare3 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_WecPrint( Vec_Wec_t * p, int fSkipSingles ) +{ + Vec_Int_t * vVec; + int i, k, Entry; + Vec_WecForEachLevel( p, vVec, i ) + { + if ( fSkipSingles && Vec_IntSize(vVec) == 1 ) + break; + printf( " %4d : {", i ); + Vec_IntForEachEntry( vVec, Entry, k ) + printf( " %d", Entry ); + printf( " }\n" ); + } +} + +ABC_NAMESPACE_HEADER_END + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index e05959a2..4063757c 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -1142,27 +1142,6 @@ void Ga2_ManRestart( Ga2_Man_t * p ) } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Vec_IntCheckUnique( Vec_Int_t * p ) -{ - int RetValue; - Vec_Int_t * pDup = Vec_IntDup( p ); - Vec_IntUniqify( pDup ); - RetValue = Vec_IntSize(p) - Vec_IntSize(pDup); - Vec_IntFree( pDup ); - return RetValue; -} - /**Function************************************************************* Synopsis [] diff --git a/src/proof/ssc/sscUtil.c b/src/proof/ssc/sscUtil.c index efabe545..21d78f85 100644 --- a/src/proof/ssc/sscUtil.c +++ b/src/proof/ssc/sscUtil.c @@ -27,27 +27,6 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -typedef struct Hsh_Obj_t_ Hsh_Obj_t; -struct Hsh_Obj_t_ -{ - int iThis; - int iNext; -}; - -typedef struct Hsh_Man_t_ Hsh_Man_t; -struct Hsh_Man_t_ -{ - unsigned * pData; // user's data - int * pTable; // hash table - Hsh_Obj_t * pObjs; - int nObjs; - int nSize; - int nTableSize; -}; - -static inline unsigned * Hsh_ObjData( Hsh_Man_t * p, int iThis ) { return p->pData + p->nSize * iThis; } -static inline Hsh_Obj_t * Hsh_ObjGet( Hsh_Man_t * p, int iObj ) { return iObj == -1 ? NULL : p->pObjs + iObj; } - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -63,85 +42,6 @@ static inline Hsh_Obj_t * Hsh_ObjGet( Hsh_Man_t * p, int iObj ) { return SeeAlso [] ***********************************************************************/ -Hsh_Man_t * Hsh_ManStart( unsigned * pData, int nDatas, int nSize ) -{ - Hsh_Man_t * p; - p = ABC_CALLOC( Hsh_Man_t, 1 ); - p->pData = pData; - p->nSize = nSize; - p->nTableSize = Abc_PrimeCudd( nDatas ); - p->pTable = ABC_FALLOC( int, p->nTableSize ); - p->pObjs = ABC_FALLOC( Hsh_Obj_t, p->nTableSize ); - return p; -} -void Hsh_ManStop( Hsh_Man_t * p ) -{ - ABC_FREE( p->pObjs ); - ABC_FREE( p->pTable ); - ABC_FREE( p ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Hsh_ManHash( unsigned * pData, int nSize, int nTableSize ) -{ - static unsigned s_BigPrimes[7] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457}; - unsigned char * pDataC = (unsigned char *)pData; - int c, nChars = nSize * 4, Key = 0; - for ( c = 0; c < nChars; c++ ) - Key += pDataC[c] * s_BigPrimes[c % 7]; - return Key % nTableSize; -} -int Hsh_ManAdd( Hsh_Man_t * p, int iThis ) -{ - Hsh_Obj_t * pObj; - unsigned * pThis = Hsh_ObjData( p, iThis ); - int * pPlace = p->pTable + Hsh_ManHash( pThis, p->nSize, p->nTableSize ); - for ( pObj = Hsh_ObjGet(p, *pPlace); pObj; pObj = Hsh_ObjGet(p, pObj->iNext) ) - if ( !memcmp( pThis, Hsh_ObjData(p, pObj->iThis), sizeof(unsigned) * p->nSize ) ) - return pObj - p->pObjs; - assert( p->nObjs < p->nTableSize ); - pObj = p->pObjs + p->nObjs; - pObj->iThis = iThis; - return (*pPlace = p->nObjs++); -} - -/**Function************************************************************* - - Synopsis [Hashes data by value.] - - Description [Array of 'nTotal' int entries, each of size 'nSize' ints, - is hashed and the resulting unique numbers is returned in the array.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Hsh_ManHashData( unsigned * pData, int nDatas, int nSize, int nInts ) -{ - Vec_Int_t * vRes; - Hsh_Man_t * p; - int i; - assert( nDatas * nSize == nInts ); - p = Hsh_ManStart( pData, nDatas, nSize ); - vRes = Vec_IntAlloc( 1000 ); - for ( i = 0; i < nDatas; i++ ) - Vec_IntPush( vRes, Hsh_ManAdd(p, i) ); - Hsh_ManStop( p ); - return vRes; -} - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// -- cgit v1.2.3