diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-10 17:27:38 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-10 17:27:38 -0800 |
commit | da9d1761c9be7a18041439a135b93dfb847f8124 (patch) | |
tree | 686289f022c04a0a3ee34757942f4726c095a211 | |
parent | ad67f4ef259db50a0eaa9debdbd80c40c0fac2d3 (diff) | |
download | abc-da9d1761c9be7a18041439a135b93dfb847f8124.tar.gz abc-da9d1761c9be7a18041439a135b93dfb847f8124.tar.bz2 abc-da9d1761c9be7a18041439a135b93dfb847f8124.zip |
Improvements to DSD manager.
-rw-r--r-- | src/opt/dau/dauTree.c | 180 |
1 files changed, 46 insertions, 134 deletions
diff --git a/src/opt/dau/dauTree.c b/src/opt/dau/dauTree.c index 342c1785..9f8aba8b 100644 --- a/src/opt/dau/dauTree.c +++ b/src/opt/dau/dauTree.c @@ -52,13 +52,11 @@ typedef struct Dss_Obj_t_ Dss_Obj_t; struct Dss_Obj_t_ { unsigned Id; // node ID - unsigned Next; // next node - unsigned Mirror : 30; // node ID unsigned fMark0 : 1; // user mark unsigned fMark1 : 1; // user mark unsigned iVar : 8; // variable unsigned nSupp : 8; // variable - unsigned nWords : 8; // variable + unsigned nWords : 6; // variable unsigned Type : 3; // node type unsigned nFans : 5; // fanin count unsigned pFans[0]; // fanins @@ -83,6 +81,7 @@ struct Dss_Man_t_ unsigned * pBins; // hash table Mem_Flex_t * pMem; // memory for nodes Vec_Ptr_t * vObjs; // objects + Vec_Int_t * vNexts; // next pointers Vec_Int_t * vLeaves; // temp Vec_Int_t * vCopies; // temp word ** pTtElems; // elementary TTs @@ -113,7 +112,8 @@ static inline Dss_Obj_t * Dss_ObjChildNtk( Dss_Ntk_t * p, Dss_Obj_t * pObj,int static inline Dss_Obj_t * Dss_ManObj( Dss_Man_t * p, int Id ) { return (Dss_Obj_t *)Vec_PtrEntry(p->vObjs, Id); } static inline Dss_Obj_t * Dss_ManConst0( Dss_Man_t * p ) { return Dss_ManObj( p, 0 ); } -static inline Dss_Obj_t * Dss_ManVar( Dss_Man_t * p, int v ) { assert( v >= 0 && v < p->nVars ); return Dss_ManObj( p, v+1 ); } +//static inline Dss_Obj_t * Dss_ManVar( Dss_Man_t * p, int v ) { assert( v >= 0 && v < p->nVars ); return Dss_ManObj( p, v+1 ); } +static inline Dss_Obj_t * Dss_ManVar( Dss_Man_t * p ) { return Dss_ManObj( p, 1 ); } static inline int Dss_ManLitSuppSize( Dss_Man_t * p, int iLit ) { return Dss_ManObj( p, Abc_Lit2Var(iLit) )->nSupp; } static inline int Dss_Obj2Lit( Dss_Obj_t * pObj ) { return Abc_Var2Lit(Dss_Regular(pObj)->Id, Dss_IsComplement(pObj)); } @@ -439,7 +439,6 @@ Dss_Obj_t * Dss_ObjAllocNtk( Dss_Ntk_t * p, int Type, int nFans, int nTruthVars pObj->Type = Type; pObj->Id = Vec_PtrSize( p->vObjs ); pObj->iVar = 31; - pObj->Mirror = ~0; Vec_PtrPush( p->vObjs, pObj ); p->nMem += pObj->nWords + (nTruthVars ? Abc_TtWordNum(nTruthVars) : 0); assert( p->nMem < p->nMemAlloc ); @@ -685,7 +684,7 @@ void Dss_ObjSortNtk( Dss_Ntk_t * p, Dss_Obj_t ** pNodes, int nNodes ) /**Function************************************************************* - Synopsis [Creating DSD network from SOP.] + Synopsis [] Description [] @@ -834,8 +833,8 @@ Dss_Obj_t * Dss_ObjAlloc( Dss_Man_t * p, int Type, int nFans, int nTruthVars ) pObj->nWords = Dss_ObjWordNum(nFans); pObj->Id = Vec_PtrSize( p->vObjs ); pObj->iVar = 31; - pObj->Mirror = ~0; Vec_PtrPush( p->vObjs, pObj ); + Vec_IntPush( p->vNexts, 0 ); return pObj; } Dss_Obj_t * Dss_ObjCreate( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth ) @@ -893,7 +892,7 @@ void Dss_ManHashProfile( Dss_Man_t * p ) for ( i = 0; i < p->nBins; i++ ) { Counter = 0; - for ( pSpot = p->pBins + i; *pSpot; pSpot = &pObj->Next, Counter++ ) + for ( pSpot = p->pBins + i; *pSpot; pSpot = Vec_IntEntryP(p->vNexts, pObj->Id), Counter++ ) pObj = Dss_ManObj( p, *pSpot ); if ( Counter ) printf( "%d ", Counter ); @@ -921,7 +920,7 @@ unsigned * Dss_ObjHashLookup( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, w { Dss_Obj_t * pObj; unsigned * pSpot = p->pBins + Dss_ObjHashKey(p, Type, vFaninLits, pTruth); - for ( ; *pSpot; pSpot = &pObj->Next ) + for ( ; *pSpot; pSpot = Vec_IntEntryP(p->vNexts, pObj->Id) ) { pObj = Dss_ManObj( p, *pSpot ); if ( (int)pObj->Type == Type && @@ -938,8 +937,8 @@ Dss_Obj_t * Dss_ObjFindOrAdd( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, w unsigned * pSpot = Dss_ObjHashLookup( p, Type, vFaninLits, pTruth ); if ( *pSpot ) return Dss_ManObj( p, *pSpot ); + *pSpot = Vec_PtrSize( p->vObjs ); pObj = Dss_ObjCreate( p, Type, vFaninLits, pTruth ); - *pSpot = pObj->Id; return pObj; } @@ -957,23 +956,16 @@ Dss_Obj_t * Dss_ObjFindOrAdd( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, w Dss_Man_t * Dss_ManAlloc( int nVars, int nNonDecLimit ) { Dss_Man_t * p; - Dss_Obj_t * pObj; - int i; p = ABC_CALLOC( Dss_Man_t, 1 ); - p->nVars = nVars; + p->nVars = nVars; p->nNonDecLimit = nNonDecLimit; - p->nBins = Abc_PrimeCudd( 100000 ); - p->pBins = ABC_CALLOC( unsigned, p->nBins ); - p->pMem = Mem_FlexStart(); - p->vObjs = Vec_PtrAlloc( 10000 ); + p->nBins = Abc_PrimeCudd( 100000 ); + p->pBins = ABC_CALLOC( unsigned, p->nBins ); + p->pMem = Mem_FlexStart(); + p->vObjs = Vec_PtrAlloc( 10000 ); + p->vNexts = Vec_IntAlloc( 10000 ); Dss_ObjAlloc( p, DAU_DSD_CONST0, 0, 0 ); - for ( i = 0; i < nVars; i++ ) - { - pObj = Dss_ObjAlloc( p, DAU_DSD_VAR, 0, 0 ); - pObj->iVar = i; - pObj->nSupp = 1; - pObj->Mirror = 1; - } + Dss_ObjAlloc( p, DAU_DSD_VAR, 0, 0 )->nSupp = 1; p->vLeaves = Vec_IntAlloc( 32 ); p->vCopies = Vec_IntAlloc( 32 ); p->pTtElems = Dss_ManTtElems(); @@ -984,12 +976,13 @@ void Dss_ManFree( Dss_Man_t * p ) { Vec_IntFreeP( &p->vCopies ); Vec_IntFreeP( &p->vLeaves ); + Vec_IntFreeP( &p->vNexts ); Vec_PtrFreeP( &p->vObjs ); Mem_FlexStop( p->pMem, 0 ); ABC_FREE( p->pBins ); ABC_FREE( p ); } -void Dss_ManPrint_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int * pPermLits ) +void Dss_ManPrint_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int * pPermLits, int * pnSupp ) { char OpenType[7] = {0, 0, 0, '(', '[', '<', '{'}; char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'}; @@ -1000,7 +993,7 @@ void Dss_ManPrint_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int * pPermLits ) { printf( "0" ); return; } if ( pObj->Type == DAU_DSD_VAR ) { - int iPermLit = pPermLits ? pPermLits[pObj->iVar] : Abc_Var2Lit(pObj->iVar, 0); + int iPermLit = pPermLits ? pPermLits[(*pnSupp)++] : Abc_Var2Lit((*pnSupp)++, 0); printf( "%s%c", Abc_LitIsCompl(iPermLit)? "!":"", 'a' + Abc_Lit2Var(iPermLit) ); return; } @@ -1010,18 +1003,21 @@ void Dss_ManPrint_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int * pPermLits ) Dss_ObjForEachFanin( p, pObj, pFanin, i ) { printf( "%s", Dss_ObjFaninC(pObj, i) ? "!":"" ); - Dss_ManPrint_rec( p, pFanin, pPermLits ); + Dss_ManPrint_rec( p, pFanin, pPermLits, pnSupp ); } printf( "%c", CloseType[pObj->Type] ); } void Dss_ManPrintOne( Dss_Man_t * p, int iDsdLit, int * pPermLits ) { + int nSupp = 0; printf( "%6d : ", Abc_Lit2Var(iDsdLit) ); printf( "%2d ", Dss_ManLitSuppSize(p, iDsdLit) ); printf( "%s", Abc_LitIsCompl(iDsdLit) ? "!" : "" ); - Dss_ManPrint_rec( p, Dss_ManObj(p, Abc_Lit2Var(iDsdLit)), pPermLits ); + Dss_ManPrint_rec( p, Dss_ManObj(p, Abc_Lit2Var(iDsdLit)), pPermLits, &nSupp ); printf( "\n" ); + assert( nSupp == (int)Dss_ManObj(p, Abc_Lit2Var(iDsdLit))->nSupp ); } +/* int Dss_ManPrintIndex_rec( Dss_Man_t * p, Dss_Obj_t * pObj ) { Dss_Obj_t * pFanin; @@ -1035,6 +1031,7 @@ int Dss_ManPrintIndex_rec( Dss_Man_t * p, Dss_Obj_t * pObj ) nVarsMax = Abc_MaxInt( nVarsMax, Dss_ManPrintIndex_rec(p, pFanin) ); return nVarsMax; } +*/ int Dss_ManCheckNonDec_rec( Dss_Man_t * p, Dss_Obj_t * pObj ) { Dss_Obj_t * pFanin; @@ -1084,16 +1081,14 @@ void Dss_ManDump( Dss_Man_t * p ) void Dss_ManPrint( Dss_Man_t * p ) { Dss_Obj_t * pObj; - int i, c, CountStr = 0, CountNonDsd = 0, CountNonDsdStr = 0; - int clk = clock(); + int CountNonDsd = 0, CountNonDsdStr = 0; + int i, clk = clock(); Dss_ManForEachObj( p, pObj, i ) { - CountStr += ((int)pObj->nSupp == Dss_ManPrintIndex_rec(p, pObj)); CountNonDsd += (pObj->Type == DAU_DSD_PRIME); CountNonDsdStr += Dss_ManCheckNonDec_rec( p, pObj ); } printf( "Total number of objects = %8d\n", Vec_PtrSize(p->vObjs) ); - printf( "Total number of structures = %8d\n", CountStr ); printf( "Non-DSD objects (max =%2d) = %8d\n", p->nNonDecLimit, CountNonDsd ); printf( "Non-DSD structures = %8d\n", CountNonDsdStr ); printf( "Memory used for objects = %6.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) ); @@ -1103,13 +1098,8 @@ void Dss_ManPrint( Dss_Man_t * p ) // Dss_ManHashProfile( p ); // Dss_ManDump( p ); // return; - c = 0; Dss_ManForEachObj( p, pObj, i ) - if ( (int)pObj->nSupp == Dss_ManPrintIndex_rec(p, pObj) ) - { - printf( "%6d : ", c++ ); - Dss_ManPrintOne( p, Dss_Obj2Lit(pObj), NULL ); - } + Dss_ManPrintOne( p, Dss_Obj2Lit(pObj), NULL ); printf( "\n" ); } @@ -1124,7 +1114,7 @@ void Dss_ManPrint( Dss_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Dss_ManComputeTruth_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int nVars, word * pRes, int * pPermLits ) +void Dss_ManComputeTruth_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int nVars, word * pRes, int * pPermLits, int * pnSupp ) { Dss_Obj_t * pChild; int nWords = Abc_TtWordNum(nVars); @@ -1132,8 +1122,8 @@ void Dss_ManComputeTruth_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int nVars, word * pObj = Dss_Regular(pObj); if ( pObj->Type == DAU_DSD_VAR ) { - int iPermLit = pPermLits[(int)pObj->iVar]; - assert( (int)pObj->iVar < nVars ); + int iPermLit = pPermLits[(*pnSupp)++]; + assert( (*pnSupp) <= nVars ); Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], nWords, fCompl ^ Abc_LitIsCompl(iPermLit) ); return; } @@ -1146,7 +1136,7 @@ void Dss_ManComputeTruth_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int nVars, word * Abc_TtConst0( pRes, nWords ); Dss_ObjForEachChild( p, pObj, pChild, i ) { - Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp, pPermLits ); + Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp, pPermLits, pnSupp ); if ( pObj->Type == DAU_DSD_AND ) Abc_TtAnd( pRes, pRes, pTtTemp, nWords, 0 ); else @@ -1159,7 +1149,7 @@ void Dss_ManComputeTruth_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int nVars, word * { word pTtTemp[3][DAU_MAX_WORD]; Dss_ObjForEachChild( p, pObj, pChild, i ) - Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp[i], pPermLits ); + Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp[i], pPermLits, pnSupp ); assert( i == 3 ); Abc_TtMux( pRes, pTtTemp[0], pTtTemp[1], pTtTemp[2], nWords ); if ( fCompl ) Abc_TtNot( pRes, nWords ); @@ -1169,7 +1159,7 @@ void Dss_ManComputeTruth_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int nVars, word * { word pFanins[DAU_MAX_VAR][DAU_MAX_WORD]; Dss_ObjForEachChild( p, pObj, pChild, i ) - Dss_ManComputeTruth_rec( p, pChild, nVars, pFanins[i], pPermLits ); + Dss_ManComputeTruth_rec( p, pChild, nVars, pFanins[i], pPermLits, pnSupp ); Dau_DsdTruthCompose_rec( Dss_ObjTruth(pObj), pFanins, pRes, pObj->nFans, nWords ); if ( fCompl ) Abc_TtNot( pRes, nWords ); return; @@ -1182,6 +1172,7 @@ word * Dss_ManComputeTruth( Dss_Man_t * p, int iDsd, int nVars, int * pPermLits Dss_Obj_t * pObj = Dss_Lit2Obj(p, iDsd); word * pRes = p->pTtElems[DAU_MAX_VAR]; int nWords = Abc_TtWordNum( nVars ); + int nSupp = 0; assert( nVars <= DAU_MAX_VAR ); if ( iDsd == 0 ) Abc_TtConst0( pRes, nWords ); @@ -1189,11 +1180,12 @@ word * Dss_ManComputeTruth( Dss_Man_t * p, int iDsd, int nVars, int * pPermLits Abc_TtConst1( pRes, nWords ); else if ( Dss_Regular(pObj)->Type == DAU_DSD_VAR ) { - int iPermLit = pPermLits[Dss_Regular(pObj)->iVar]; + int iPermLit = pPermLits[nSupp++]; Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], nWords, Abc_LitIsCompl(iDsd) ^ Abc_LitIsCompl(iPermLit) ); } else - Dss_ManComputeTruth_rec( p, pObj, nVars, pRes, pPermLits ); + Dss_ManComputeTruth_rec( p, pObj, nVars, pRes, pPermLits, &nSupp ); + assert( nSupp == (int)Dss_Regular(pObj)->nSupp ); return pRes; } @@ -1209,94 +1201,12 @@ word * Dss_ManComputeTruth( Dss_Man_t * p, int iDsd, int nVars, int * pPermLits SeeAlso [] ***********************************************************************/ -Dss_Obj_t * Dss_ManShiftTree_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int Shift ) -{ - Vec_Int_t * vFaninLits; - Dss_Obj_t * pMirror, * pFanin, * pObjNew; - int i, nSupp = Shift; - assert( !Dss_IsComplement(pObj) ); - assert( pObj->Mirror == pObj->Id ); - if ( Shift == 0 ) - return pObj; - if ( pObj->Type == DAU_DSD_VAR ) - { - assert( (int)pObj->iVar + Shift < p->nVars ); - return Dss_ManVar( p, pObj->iVar + Shift ); - } - // collect fanins - vFaninLits = Vec_IntAlloc( 10 ); - Dss_ObjForEachFanin( p, pObj, pFanin, i ) - { - pMirror = Dss_ManObj( p, pFanin->Mirror ); - pFanin = Dss_ManShiftTree_rec( p, pMirror, nSupp ); - Vec_IntPush( vFaninLits, Abc_Var2Lit(pFanin->Id, Dss_ObjFaninC(pObj, i)) ); - assert( pFanin->nSupp > 0 ); - nSupp += pFanin->nSupp; - } - // create new graph - pObjNew = Dss_ObjFindOrAdd( p, pObj->Type, vFaninLits, pObj->Type == DAU_DSD_PRIME ? Dss_ObjTruth(pObj) : NULL ); - pObjNew->Mirror = pObj->Id; - Vec_IntFree( vFaninLits ); - return pObjNew; -} -void Dss_ManShiftTree( Dss_Man_t * p, Dss_Obj_t ** pChildren, int nChildren, Vec_Int_t * vLeaves ) -{ - int i, nSupp = 0; - Vec_IntClear( vLeaves ); - for ( i = 0; i < nChildren; i++ ) - { - Dss_Obj_t * pMirror = Dss_ManObj( p, Dss_Regular(pChildren[i])->Mirror ); - Dss_Obj_t * pFanin = Dss_ManShiftTree_rec( p, pMirror, nSupp ); - assert( !Dss_IsComplement(pFanin) ); - Vec_IntPush( vLeaves, Abc_Var2Lit(pFanin->Id, Dss_IsComplement(pChildren[i])) ); - assert( pFanin->nSupp > 0 ); - nSupp += pFanin->nSupp; - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -/* -int Dss_NtkRebuild( Dss_Man_t * p, Dss_Ntk_t * pNtk ) -{ - Dss_Obj_t * pObj, * pFanin, * pObjNew; - int i, k; - assert( p->nVars == pNtk->nVars ); - if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_CONST0 ) - return Dss_IsComplement(pNtk->pRoot); - if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_VAR ) - return Abc_Var2Lit( Dss_Regular(pNtk->pRoot)->iVar, Dss_IsComplement(pNtk->pRoot) ); - Vec_IntFill( p->vCopies, Vec_PtrSize(pNtk->vObjs), -1 ); - Dss_NtkForEachNode( pNtk, pObj, i ) - { - Vec_IntClear( p->vLeaves ); - Dss_ObjForEachFaninNtk( pNtk, pObj, pFanin, k ) - if ( pFanin->Type == DAU_DSD_VAR ) - Vec_IntPush( p->vLeaves, Abc_Var2Lit(pFanin->iVar+1, 0) ); - else - Vec_IntPush( p->vLeaves, Abc_Lit2Lit(Vec_IntArray(p->vCopies), pObj->pFans[k]) ); - pObjNew = Dss_ObjCreate( p, pObj->Type, p->vLeaves ); - Vec_IntWriteEntry( p->vCopies, Dss_ObjId(pObj), Dss_ObjId(pObjNew) ); - } - return Abc_Lit2Lit( Vec_IntArray(p->vCopies), Dss_Obj2Lit(pNtk->pRoot) ); -} -*/ - // returns literal of non-shifted tree in p, corresponding to pObj in pNtk, which may be compl int Dss_NtkRebuild_rec( Dss_Man_t * p, Dss_Ntk_t * pNtk, Dss_Obj_t * pObj ) { Dss_Obj_t * pChildren[DAU_MAX_VAR]; Dss_Obj_t * pChild, * pObjNew; - int k, fCompl = Dss_IsComplement(pObj); + int i, k, fCompl = Dss_IsComplement(pObj); pObj = Dss_Regular(pObj); if ( pObj->Type == DAU_DSD_VAR ) return Abc_Var2Lit( 1, fCompl ); @@ -1322,10 +1232,11 @@ int Dss_NtkRebuild_rec( Dss_Man_t * p, Dss_Ntk_t * pNtk, Dss_Obj_t * pObj ) } } // shift subgraphs - Dss_ManShiftTree( p, pChildren, k, p->vLeaves ); + Vec_IntClear( p->vLeaves ); + for ( i = 0; i < k; i++ ) + Vec_IntPush( p->vLeaves, Dss_Obj2Lit(pChildren[i]) ); // create new graph pObjNew = Dss_ObjFindOrAdd( p, pObj->Type, p->vLeaves, pObj->Type == DAU_DSD_PRIME ? Dss_ObjTruth(pObj) : NULL ); - pObjNew->Mirror = pObjNew->Id; return Abc_Var2Lit( pObjNew->Id, fCompl ); } int Dss_NtkRebuild( Dss_Man_t * p, Dss_Ntk_t * pNtk ) @@ -1446,10 +1357,11 @@ int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned else assert( 0 ); // shift subgraphs - Dss_ManShiftTree( p, pChildren, nChildren, p->vLeaves ); + Vec_IntClear( p->vLeaves ); + for ( i = 0; i < nChildren; i++ ) + Vec_IntPush( p->vLeaves, Dss_Obj2Lit(pChildren[i]) ); // create new graph pObj = Dss_ObjFindOrAdd( p, Type, p->vLeaves, pTruth ); - pObj->Mirror = pObj->Id; return Abc_Var2Lit( pObj->Id, fCompl ); } Dss_Fun_t * Dss_ManOperationFun( Dss_Man_t * p, int * iDsd, int * nFans ) @@ -1774,7 +1686,7 @@ void Dau_DsdTest_() p = Dss_ManAlloc( nVars, 0 ); // init - Vec_VecPushInt( vFuncs, 1, Dss_Obj2Lit(Dss_ManVar(p, 0)) ); + Vec_VecPushInt( vFuncs, 1, Dss_Obj2Lit(Dss_ManVar(p)) ); // enumerate for ( s = 2; s <= nVars; s++ ) |