From 883e21fe8a663844b6b12c2b202093fb0760f16c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 2 Apr 2014 18:07:50 -0700 Subject: Improvements to DSD manager. --- src/map/if/ifDsd.c | 362 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 226 insertions(+), 136 deletions(-) (limited to 'src/map') diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index 4ea4f83d..5c7d7f4e 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -22,6 +22,7 @@ #include "if.h" #include "misc/extra/extra.h" #include "sat/bsat/satSolver.h" +#include "aig/gia/gia.h" ABC_NAMESPACE_IMPL_START @@ -64,13 +65,16 @@ struct If_DsdMan_t_ Mem_Flex_t * pMem; // memory for nodes Vec_Ptr_t * vObjs; // objects Vec_Int_t * vNexts; // next pointers + Vec_Int_t * vTruths; // truth IDs of prime nodes Vec_Int_t * vTemp1; // temp Vec_Int_t * vTemp2; // temp word ** pTtElems; // elementary TTs - Vec_Mem_t * vTtMem; // truth table memory and hash table - Vec_Ptr_t * vTtDecs; // truth table decompositions + Vec_Mem_t * vTtMem[IF_MAX_FUNC_LUTSIZE+1]; // truth table memory and hash table + Vec_Ptr_t * vTtDecs[IF_MAX_FUNC_LUTSIZE+1]; // truth table decompositions + int * pSched[IF_MAX_FUNC_LUTSIZE]; // grey code schedules + Gia_Man_t * pTtGia; // GIA to represent truth tables + Vec_Int_t * vCover; // temporary memory void * pSat; // SAT solver - int * pSched[16]; // grey code schedules int nUniqueHits; // statistics int nUniqueMisses; // statistics abctime timeDsd; // statistics @@ -81,9 +85,9 @@ struct If_DsdMan_t_ }; static inline int If_DsdObjWordNum( int nFans ) { return sizeof(If_DsdObj_t) / 8 + nFans / 2 + ((nFans & 1) > 0); } -static inline int If_DsdObjTruthId( If_DsdObj_t * pObj ) { return pObj->Type == IF_DSD_PRIME ? pObj->pFans[pObj->nFans] : -1; } -static inline word * If_DsdObjTruth( If_DsdMan_t * p, If_DsdObj_t * pObj ) { return Vec_MemReadEntry(p->vTtMem, If_DsdObjTruthId(pObj)); } -static inline void If_DsdObjSetTruth( If_DsdMan_t * p, If_DsdObj_t * pObj, int Id ) { assert( pObj->Type == IF_DSD_PRIME && pObj->nFans > 2 ); pObj->pFans[pObj->nFans] = Id; } +static inline int If_DsdObjTruthId( If_DsdMan_t * p, If_DsdObj_t * pObj ) { return (pObj->Type == IF_DSD_PRIME && pObj->nFans > 2) ? Vec_IntEntry(p->vTruths, pObj->Id) : -1; } +static inline word * If_DsdObjTruth( If_DsdMan_t * p, If_DsdObj_t * pObj ) { return Vec_MemReadEntry(p->vTtMem[pObj->nFans], If_DsdObjTruthId(p, pObj)); } +static inline void If_DsdObjSetTruth( If_DsdMan_t * p, If_DsdObj_t * pObj, int Id ) { assert( pObj->Type == IF_DSD_PRIME && pObj->nFans > 2 ); Vec_IntWriteEntry(p->vTruths, pObj->Id, Id); } static inline void If_DsdObjClean( If_DsdObj_t * pObj ) { memset( pObj, 0, sizeof(If_DsdObj_t) ); } static inline int If_DsdObjId( If_DsdObj_t * pObj ) { return pObj->Id; } @@ -117,6 +121,8 @@ static inline void If_DsdVecObjClearMark( Vec_Ptr_t * p, int iObj ) #define If_DsdObjForEachFaninLit( vVec, pObj, iLit, i ) \ for ( i = 0; (i < If_DsdObjFaninNum(pObj)) && ((iLit) = If_DsdObjFaninLit(pObj, i)); i++ ) +extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -174,7 +180,7 @@ static inline word ** If_ManDsdTtElems() } If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans ) { - int nWords = If_DsdObjWordNum( nFans + (int)(Type == DAU_DSD_PRIME) ); + int nWords = If_DsdObjWordNum( nFans ); If_DsdObj_t * pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords ); If_DsdObjClean( pObj ); pObj->Type = Type; @@ -184,7 +190,9 @@ If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans ) pObj->Count = 0; Vec_PtrPush( p->vObjs, pObj ); Vec_IntPush( p->vNexts, 0 ); + Vec_IntPush( p->vTruths, -1 ); assert( Vec_IntSize(p->vNexts) == Vec_PtrSize(p->vObjs) ); + assert( Vec_IntSize(p->vTruths) == Vec_PtrSize(p->vObjs) ); return pObj; } If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize ) @@ -202,14 +210,25 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize ) p->pMem = Mem_FlexStart(); p->vObjs = Vec_PtrAlloc( 10000 ); p->vNexts = Vec_IntAlloc( 10000 ); + p->vTruths = Vec_IntAlloc( 10000 ); If_DsdObjAlloc( p, IF_DSD_CONST0, 0 ); If_DsdObjAlloc( p, IF_DSD_VAR, 0 )->nSupp = 1; p->vTemp1 = Vec_IntAlloc( 32 ); p->vTemp2 = Vec_IntAlloc( 32 ); p->pTtElems = If_ManDsdTtElems(); - p->vTtDecs = Vec_PtrAlloc( 1000 ); - p->vTtMem = Vec_MemAlloc( Abc_TtWordNum(nVars), 12 ); - Vec_MemHashAlloc( p->vTtMem, 10000 ); + for ( v = 3; v <= nVars; v++ ) + { + p->vTtMem[v] = Vec_MemAlloc( Abc_TtWordNum(v), 12 ); + Vec_MemHashAlloc( p->vTtMem[v], 10000 ); + p->vTtDecs[v] = Vec_PtrAlloc( 1000 ); + } +/* + p->pTtGia = Gia_ManStart( nVars ); + Gia_ManHashAlloc( p->pTtGia ); + for ( v = 0; v < nVars; v++ ) + Gia_ManAppendCi( p->pTtGia ); + p->vCover = Vec_IntAlloc( 0 ); +*/ for ( v = 2; v < nVars; v++ ) p->pSched[v] = Extra_GreyCodeSchedule( v ); if ( LutSize ) @@ -223,17 +242,30 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose ) if ( fVerbose ) If_DsdManPrint( p, NULL, 0, 0, 0, 0, 0 ); if ( fVerbose ) - Vec_MemDumpTruthTables( p->vTtMem, "dumpdsd", p->nVars ); + { + char FileName[10]; + for ( v = 3; v <= p->nVars; v++ ) + { + sprintf( FileName, "dumpdsd%02d", v ); + Vec_MemDumpTruthTables( p->vTtMem[v], FileName, v ); + } + } for ( v = 2; v < p->nVars; v++ ) ABC_FREE( p->pSched[v] ); - Vec_VecFree( (Vec_Vec_t *)p->vTtDecs ); - Vec_MemHashFree( p->vTtMem ); - Vec_MemFreeP( &p->vTtMem ); + for ( v = 3; v <= p->nVars; v++ ) + { + Vec_MemHashFree( p->vTtMem[v] ); + Vec_MemFree( p->vTtMem[v] ); + Vec_VecFree( (Vec_Vec_t *)(p->vTtDecs[v]) ); + } Vec_IntFreeP( &p->vTemp1 ); Vec_IntFreeP( &p->vTemp2 ); Vec_IntFreeP( &p->vNexts ); + Vec_IntFreeP( &p->vTruths ); Vec_PtrFreeP( &p->vObjs ); Mem_FlexStop( p->pMem, 0 ); + Gia_ManStopP( &p->pTtGia ); + Vec_IntFreeP( &p->vCover ); If_ManSatUnbuild( p->pSat ); ABC_FREE( p->pStore ); ABC_FREE( p->pBins ); @@ -242,31 +274,35 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose ) void If_DsdManDumpDsd( If_DsdMan_t * p, int Support ) { char * pFileName = "tts_nondsd.txt"; - If_DsdObj_t * pObj; int i; + If_DsdObj_t * pObj; Vec_Int_t * vMap; FILE * pFile = fopen( pFileName, "wb" ); + int v, i; if ( pFile == NULL ) { printf( "Cannot open file \"%s\".\n", pFileName ); return; } - vMap = Vec_IntStart( Vec_MemEntryNum(p->vTtMem) ); - If_DsdVecForEachObj( p->vObjs, pObj, i ) + for ( v = 3; v <= p->nVars; v++ ) { - if ( Support && Support != If_DsdObjSuppSize(pObj) ) - continue; - if ( If_DsdObjType(pObj) != IF_DSD_PRIME ) - continue; - if ( Vec_IntEntry(vMap, If_DsdObjTruthId(pObj)) ) - continue; - Vec_IntWriteEntry(vMap, If_DsdObjTruthId(pObj), 1); - fprintf( pFile, "0x" ); - Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), Support ? Abc_MaxInt(Support, 6) : p->nVars ); - fprintf( pFile, "\n" ); -// printf( " " ); -// Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars ); + vMap = Vec_IntStart( Vec_MemEntryNum(p->vTtMem[v]) ); + If_DsdVecForEachObj( p->vObjs, pObj, i ) + { + if ( Support && Support != If_DsdObjSuppSize(pObj) ) + continue; + if ( If_DsdObjType(pObj) != IF_DSD_PRIME ) + continue; + if ( Vec_IntEntry(vMap, If_DsdObjTruthId(p, pObj)) ) + continue; + Vec_IntWriteEntry(vMap, If_DsdObjTruthId(p, pObj), 1); + fprintf( pFile, "0x" ); + Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), Support ? Abc_MaxInt(Support, 6) : v ); + fprintf( pFile, "\n" ); + //printf( " " ); + //Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars ); + } + Vec_IntFree( vMap ); } - Vec_IntFree( vMap ); fclose( pFile ); } void If_DsdManDumpAll( If_DsdMan_t * p, int Support ) @@ -378,38 +414,41 @@ void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char void If_DsdManPrintDecs( FILE * pFile, If_DsdMan_t * p ) { Vec_Int_t * vDecs; - int i, k, nSuppSize, nDecMax = 0; + int i, k, v, nSuppSize, nDecMax = 0; int pDecMax[IF_MAX_FUNC_LUTSIZE] = {0}; int pCountsAll[IF_MAX_FUNC_LUTSIZE] = {0}; int pCountsSSizes[IF_MAX_FUNC_LUTSIZE] = {0}; int pCounts[IF_MAX_FUNC_LUTSIZE][DSD_ARRAY_LIMIT+2] = {{0}}; word * pTruth; - assert( Vec_MemEntryNum(p->vTtMem) == Vec_PtrSize(p->vTtDecs) ); - // find max number of decompositions - Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs, vDecs, i ) - { - pTruth = Vec_MemReadEntry( p->vTtMem, i ); - nSuppSize = Abc_TtSupportSize( pTruth, p->nVars ); - pDecMax[nSuppSize] = Abc_MaxInt( pDecMax[nSuppSize], Vec_IntSize(vDecs) ); - nDecMax = Abc_MaxInt( nDecMax, Vec_IntSize(vDecs) ); - } - // fill up - Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs, vDecs, i ) - { - pTruth = Vec_MemReadEntry( p->vTtMem, i ); - nSuppSize = Abc_TtSupportSize( pTruth, p->nVars ); - pCountsAll[nSuppSize]++; - pCountsSSizes[nSuppSize] += Vec_IntSize(vDecs); - pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs))]++; -// pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs)?1+(Vec_IntSize(vDecs)/10):0)]++; -/* - if ( nSuppSize == 6 && Vec_IntSize(vDecs) == pDecMax[6] ) + for ( v = 3; v <= p->nVars; v++ ) + { + assert( Vec_MemEntryNum(p->vTtMem[v]) == Vec_PtrSize(p->vTtDecs[v]) ); + // find max number of decompositions + Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs[v], vDecs, i ) { - fprintf( pFile, "0x" ); - Abc_TtPrintHex( pTruth, nSuppSize ); - Dau_DecPrintSets( vDecs, nSuppSize ); + pTruth = Vec_MemReadEntry( p->vTtMem[v], i ); + nSuppSize = Abc_TtSupportSize( pTruth, p->nVars ); + pDecMax[nSuppSize] = Abc_MaxInt( pDecMax[nSuppSize], Vec_IntSize(vDecs) ); + nDecMax = Abc_MaxInt( nDecMax, Vec_IntSize(vDecs) ); + } + // fill up + Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs[v], vDecs, i ) + { + pTruth = Vec_MemReadEntry( p->vTtMem[v], i ); + nSuppSize = Abc_TtSupportSize( pTruth, p->nVars ); + pCountsAll[nSuppSize]++; + pCountsSSizes[nSuppSize] += Vec_IntSize(vDecs); + pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs))]++; + // pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs)?1+(Vec_IntSize(vDecs)/10):0)]++; + /* + if ( nSuppSize == 6 && Vec_IntSize(vDecs) == pDecMax[6] ) + { + fprintf( pFile, "0x" ); + Abc_TtPrintHex( pTruth, nSuppSize ); + Dau_DecPrintSets( vDecs, nSuppSize ); + } + */ } -*/ } // print header fprintf( pFile, " N : " ); @@ -499,39 +538,64 @@ void If_DsdManPrintOccurs( FILE * pFile, If_DsdMan_t * p ) void If_DsdManPrintDistrib( If_DsdMan_t * p ) { - If_DsdObj_t * pObj; - int CountAll[IF_MAX_FUNC_LUTSIZE] = {0}; - int CountNon[IF_MAX_FUNC_LUTSIZE] = {0}; - int i, nVars, CountNonTotal = 0; - If_DsdVecForEachObj( p->vObjs, pObj, i ) + If_DsdObj_t * pObj; int i; + int CountObj[IF_MAX_FUNC_LUTSIZE+2] = {0}; + int CountObjNon[IF_MAX_FUNC_LUTSIZE+2] = {0}; + int CountObjNpn[IF_MAX_FUNC_LUTSIZE+2] = {0}; + int CountStr[IF_MAX_FUNC_LUTSIZE+2] = {0}; + int CountStrNon[IF_MAX_FUNC_LUTSIZE+2] = {0}; + int CountMarked[IF_MAX_FUNC_LUTSIZE+2] = {0}; + for ( i = 3; i <= p->nVars; i++ ) { - nVars = If_DsdObjSuppSize(pObj); - CountAll[nVars]++; - if ( !If_DsdVecObjMark(p->vObjs, i) ) - continue; - CountNon[nVars]++; - CountNonTotal++; + CountObjNpn[i] = Vec_MemEntryNum(p->vTtMem[i]); + CountObjNpn[p->nVars+1] += Vec_MemEntryNum(p->vTtMem[i]); } - for ( i = 0; i <= p->nVars; i++ ) + If_DsdVecForEachObj( p->vObjs, pObj, i ) + { + CountObj[If_DsdObjFaninNum(pObj)]++, CountObj[p->nVars+1]++; + if ( If_DsdObjType(pObj) == IF_DSD_PRIME ) + CountObjNon[If_DsdObjFaninNum(pObj)]++, CountObjNon[p->nVars+1]++; + CountStr[If_DsdObjSuppSize(pObj)]++, CountStr[p->nVars+1]++; + if ( If_DsdManCheckNonDec_rec(p, i) ) + CountStrNon[If_DsdObjSuppSize(pObj)]++, CountStrNon[p->nVars+1]++; + if ( If_DsdVecObjMark(p->vObjs, i) ) + CountMarked[If_DsdObjSuppSize(pObj)]++, CountMarked[p->nVars+1]++; + } + printf( "***** DSD MANAGER STATISTICS *****\n" ); + printf( "Support " ); + printf( "Obj " ); + printf( "ObjNDSD " ); + printf( "NPNNDSD " ); + printf( "Str " ); + printf( "StrNDSD " ); + printf( "Marked " ); + printf( "\n" ); + for ( i = 0; i <= p->nVars + 1; i++ ) { - printf( "%3d : ", i ); - printf( "All = %8d ", CountAll[i] ); - printf( "Non = %8d ", CountNon[i] ); - printf( "(%6.2f %%)", 100.0 * CountNon[i] / CountAll[i] ); + if ( i == p->nVars + 1 ) + printf( "All : " ); + else + printf( "%3d : ", i ); + printf( "%9d ", CountObj[i] ); + printf( "%9d ", CountObjNon[i] ); + printf( "%6.2f %% ", 100.0 * CountObjNon[i] / Abc_MaxInt(1, CountObj[i]) ); + printf( "%9d ", CountObjNpn[i] ); + printf( "%6.2f %% ", 100.0 * CountObjNpn[i] / Abc_MaxInt(1, CountObj[i]) ); + printf( " " ); + printf( "%9d ", CountStr[i] ); + printf( "%9d ", CountStrNon[i] ); + printf( "%6.2f %% ", 100.0 * CountStrNon[i] / Abc_MaxInt(1, CountStr[i]) ); + printf( "%9d ", CountMarked[i] ); + printf( "%6.2f %%", 100.0 * CountMarked[i] / Abc_MaxInt(1, CountStr[i]) ); printf( "\n" ); } - printf( "All : " ); - printf( "All = %8d ", Vec_PtrSize(p->vObjs) ); - printf( "Non = %8d ", CountNonTotal ); - printf( "(%6.2f %%)", 100.0 * CountNonTotal / Vec_PtrSize(p->vObjs) ); - printf( "\n" ); } void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, int fOccurs, int fTtDump, int fVerbose ) { If_DsdObj_t * pObj; Vec_Int_t * vStructs, * vCounts; - int CountUsed = 0, CountNonDsdStr = 0, CountMarked = 0, CountPrime = 0; - int i, * pPerm, DsdMax = 0; + int CountUsed = 0, CountNonDsd = 0, CountNonDsdStr = 0, CountMarked = 0, CountPrime = 0; + int i, v, * pPerm, DsdMax = 0, MemSizeTTs = 0, MemSizeDecs = 0; FILE * pFile; pFile = pFileName ? fopen( pFileName, "wb" ) : stdout; if ( pFileName && pFile == NULL ) @@ -548,22 +612,24 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, CountUsed += ( If_DsdVecObjRef(p->vObjs, pObj->Id) > 0 ); CountMarked += If_DsdVecObjMark( p->vObjs, i ); } - fprintf( pFile, "Total number of objects = %8d\n", Vec_PtrSize(p->vObjs) ); - fprintf( pFile, "Externally used objects = %8d\n", CountUsed ); - fprintf( pFile, "Non-DSD objects (max =%2d) = %8d\n", DsdMax, Vec_MemEntryNum(p->vTtMem) ); - fprintf( pFile, "Non-DSD structures = %8d\n", CountNonDsdStr ); - fprintf( pFile, "Prime objects = %8d\n", CountPrime ); - fprintf( pFile, "Marked objects = %8d\n", CountMarked ); - fprintf( pFile, "Unique table hits = %8d\n", p->nUniqueHits ); + for ( v = 3; v <= p->nVars; v++ ) + { + CountNonDsd += Vec_MemEntryNum(p->vTtMem[v]); + MemSizeTTs += Vec_MemEntrySize(p->vTtMem[v]) * Vec_MemEntryNum(p->vTtMem[v]); + MemSizeDecs += (int)Vec_VecMemoryInt((Vec_Vec_t *)(p->vTtDecs[v])); + } + If_DsdManPrintDistrib( p ); + if ( p->pTtGia ) + fprintf( pFile, "Non-DSD AIG nodes = %8d\n", Gia_ManAndNum(p->pTtGia) ); fprintf( pFile, "Unique table misses = %8d\n", p->nUniqueMisses ); + fprintf( pFile, "Unique table hits = %8d\n", p->nUniqueHits ); fprintf( pFile, "Memory used for objects = %8.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) ); - fprintf( pFile, "Memory used for functions = %8.2f MB.\n", 8.0*(Vec_MemEntrySize(p->vTtMem)+1)*Vec_MemEntryNum(p->vTtMem)/(1<<20) ); + fprintf( pFile, "Memory used for functions = %8.2f MB.\n", 8.0*(MemSizeTTs+sizeof(int)*Vec_IntCap(p->vTruths))/(1<<20) ); fprintf( pFile, "Memory used for hash table = %8.2f MB.\n", 1.0*sizeof(int)*(p->nBins+Vec_IntCap(p->vNexts))/(1<<20) ); - fprintf( pFile, "Memory used for bound sets = %8.2f MB.\n", (float)Vec_VecMemoryInt((Vec_Vec_t *)p->vTtDecs)/(1<<20) ); + fprintf( pFile, "Memory used for bound sets = %8.2f MB.\n", 1.0*MemSizeDecs/(1<<20) ); fprintf( pFile, "Memory used for array = %8.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) ); - If_DsdManPrintDistrib( p ); - if ( fOccurs ) - If_DsdManPrintOccurs( stdout, p ); + if ( p->pTtGia ) + fprintf( pFile, "Memory used for AIG = %8.2f MB.\n", 8.0*Gia_ManAndNum(p->pTtGia)/(1<<20) ); if ( p->timeDsd ) { Abc_PrintTime( 1, "Time DSD ", p->timeDsd ); @@ -572,6 +638,8 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, Abc_PrintTime( 1, "Time check2", p->timeCheck2 ); Abc_PrintTime( 1, "Time verify", p->timeVerify ); } + if ( fOccurs ) + If_DsdManPrintOccurs( stdout, p ); // If_DsdManHashProfile( p ); if ( fTtDump ) If_DsdManDumpDsd( p, Support ); @@ -618,7 +686,7 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, SeeAlso [] ***********************************************************************/ -int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 ) +int If_DsdObjCompare( If_DsdMan_t * pMan, Vec_Ptr_t * p, int iLit0, int iLit1 ) { If_DsdObj_t * p0 = If_DsdVecObj(p, Abc_Lit2Var(iLit0)); If_DsdObj_t * p1 = If_DsdVecObj(p, Abc_Lit2Var(iLit1)); @@ -635,14 +703,14 @@ int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 ) return 1; if ( If_DsdObjType(p0) == IF_DSD_PRIME ) { - if ( If_DsdObjTruthId(p0) < If_DsdObjTruthId(p1) ) + if ( If_DsdObjTruthId(pMan, p0) < If_DsdObjTruthId(pMan, p1) ) return -1; - if ( If_DsdObjTruthId(p0) > If_DsdObjTruthId(p1) ) + if ( If_DsdObjTruthId(pMan, p0) > If_DsdObjTruthId(pMan, p1) ) return 1; } for ( i = 0; i < If_DsdObjFaninNum(p0); i++ ) { - Res = If_DsdObjCompare( p, If_DsdObjFaninLit(p0, i), If_DsdObjFaninLit(p1, i) ); + Res = If_DsdObjCompare( pMan, p, If_DsdObjFaninLit(p0, i), If_DsdObjFaninLit(p1, i) ); if ( Res != 0 ) return Res; } @@ -653,14 +721,14 @@ int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 ) assert( iLit0 == iLit1 ); return 0; } -void If_DsdObjSort( Vec_Ptr_t * p, int * pLits, int nLits, int * pPerm ) +void If_DsdObjSort( If_DsdMan_t * pMan, Vec_Ptr_t * p, int * pLits, int nLits, int * pPerm ) { int i, j, best_i; for ( i = 0; i < nLits-1; i++ ) { best_i = i; for ( j = i+1; j < nLits; j++ ) - if ( If_DsdObjCompare(p, pLits[best_i], pLits[j]) == 1 ) + if ( If_DsdObjCompare(pMan, p, pLits[best_i], pLits[j]) == 1 ) best_i = j; if ( i == best_i ) continue; @@ -704,7 +772,7 @@ unsigned * If_DsdObjHashLookup( If_DsdMan_t * p, int Type, int * pLits, int nLit if ( If_DsdObjType(pObj) == Type && If_DsdObjFaninNum(pObj) == nLits && !memcmp(pObj->pFans, pLits, sizeof(int)*If_DsdObjFaninNum(pObj)) && - truthId == If_DsdObjTruthId(pObj) ) + truthId == If_DsdObjTruthId(p, pObj) ) { p->nUniqueHits++; return pSpot; @@ -724,7 +792,7 @@ static void If_DsdObjHashResize( If_DsdMan_t * p ) Vec_IntFill( p->vNexts, Vec_PtrSize(p->vObjs), 0 ); If_DsdVecForEachNode( p->vObjs, pObj, i ) { - pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(pObj) ); + pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(p, pObj) ); assert( *pSpot == 0 ); *pSpot = pObj->Id; } @@ -748,7 +816,7 @@ int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int trut pFanin = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[i]) ); assert( Type != DAU_DSD_AND || Abc_LitIsCompl(pLits[i]) || If_DsdObjType(pFanin) != DAU_DSD_AND ); assert( Type != DAU_DSD_XOR || If_DsdObjType(pFanin) != DAU_DSD_XOR ); - assert( iPrev == -1 || If_DsdObjCompare(p->vObjs, iPrev, pLits[i]) <= 0 ); + assert( iPrev == -1 || If_DsdObjCompare(p, p->vObjs, iPrev, pLits[i]) <= 0 ); iPrev = pLits[i]; } } @@ -775,20 +843,26 @@ int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int trut } int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word * pTruth ) { - int objId, truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem, pTruth) : -1; + int objId, truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem[nLits], pTruth) : -1; unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId ); abctime clk; if ( *pSpot ) return (int)*pSpot; clk = Abc_Clock(); - if ( p->LutSize && truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs) ) + if ( p->LutSize && truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs[nLits]) ) { Vec_Int_t * vSets = Dau_DecFindSets_int( pTruth, nLits, p->pSched ); -// printf( "%d ", Vec_IntSize(vSets) ); - assert( truthId == Vec_MemEntryNum(p->vTtMem)-1 ); - Vec_PtrPush( p->vTtDecs, vSets ); + assert( truthId == Vec_MemEntryNum(p->vTtMem[nLits])-1 ); + Vec_PtrPush( p->vTtDecs[nLits], vSets ); // Dau_DecPrintSets( vSets, nLits ); } + if ( p->pTtGia && truthId >= 0 && truthId == Vec_MemEntryNum(p->vTtMem[nLits])-1 ) + { + int nObjOld = Gia_ManAndNum(p->pTtGia); + int Lit = Kit_TruthToGia( p->pTtGia, (unsigned *)pTruth, nLits, p->vCover, NULL, 1 ); +// printf( "%d ", Gia_ManAndNum(p->pTtGia)-nObjOld ); + Gia_ManAppendCo( p->pTtGia, Lit ); + } p->timeCheck += Abc_Clock() - clk; *pSpot = Vec_PtrSize( p->vObjs ); objId = If_DsdObjCreate( p, Type, pLits, nLits, truthId ); @@ -815,7 +889,7 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName ) Vec_Int_t * vSets; char * pBuffer = "dsd0"; word * pTruth; - int i, Num; + int i, v, Num; FILE * pFile = fopen( pFileName ? pFileName : p->pStore, "wb" ); if ( pFile == NULL ) { @@ -831,21 +905,27 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName ) fwrite( &Num, 4, 1, pFile ); Vec_PtrForEachEntryStart( If_DsdObj_t *, p->vObjs, pObj, i, 2 ) { - Num = If_DsdObjWordNum( pObj->nFans + (int)(pObj->Type == DAU_DSD_PRIME) ); + Num = If_DsdObjWordNum( pObj->nFans ); fwrite( &Num, 4, 1, pFile ); fwrite( pObj, sizeof(word)*Num, 1, pFile ); + if ( pObj->Type == IF_DSD_PRIME ) + fwrite( Vec_IntEntryP(p->vTruths, i), 4, 1, pFile ); } - Num = Vec_MemEntryNum(p->vTtMem); - fwrite( &Num, 4, 1, pFile ); - Vec_MemForEachEntry( p->vTtMem, pTruth, i ) - fwrite( pTruth, sizeof(word)*p->nWords, 1, pFile ); - Num = Vec_PtrSize(p->vTtDecs); - fwrite( &Num, 4, 1, pFile ); - Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs, vSets, i ) + for ( v = 3; v <= p->nVars; v++ ) { - Num = Vec_IntSize(vSets); + int nBytes = sizeof(word)*Vec_MemEntrySize(p->vTtMem[v]); + Num = Vec_MemEntryNum(p->vTtMem[v]); + fwrite( &Num, 4, 1, pFile ); + Vec_MemForEachEntry( p->vTtMem[v], pTruth, i ) + fwrite( pTruth, nBytes, 1, pFile ); + Num = Vec_PtrSize(p->vTtDecs[v]); fwrite( &Num, 4, 1, pFile ); - fwrite( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile ); + Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs[v], vSets, i ) + { + Num = Vec_IntSize(vSets); + fwrite( &Num, 4, 1, pFile ); + fwrite( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile ); + } } fclose( pFile ); } @@ -857,7 +937,7 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName ) char pBuffer[10]; unsigned * pSpot; word * pTruth; - int i, Num, Num2, RetValue; + int i, v, Num, Num2, RetValue; FILE * pFile = fopen( pFileName, "rb" ); if ( pFile == NULL ) { @@ -881,6 +961,7 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName ) assert( Num >= 2 ); Vec_PtrFillExtra( p->vObjs, Num, NULL ); Vec_IntFill( p->vNexts, Num, 0 ); + Vec_IntFill( p->vTruths, Num, -1 ); p->nBins = Abc_PrimeCudd( 2*Num ); p->pBins = ABC_REALLOC( unsigned, p->pBins, p->nBins ); memset( p->pBins, 0, sizeof(unsigned) * p->nBins ); @@ -890,31 +971,40 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName ) pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * Num ); RetValue = fread( pObj, sizeof(word)*Num, 1, pFile ); Vec_PtrWriteEntry( p->vObjs, i, pObj ); - pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(pObj) ); + if ( pObj->Type == IF_DSD_PRIME ) + { + RetValue = fread( &Num, 4, 1, pFile ); + Vec_IntWriteEntry( p->vTruths, i, Num ); + } + pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(p, pObj) ); assert( *pSpot == 0 ); *pSpot = pObj->Id; } assert( p->nUniqueMisses == Vec_PtrSize(p->vObjs) - 2 ); p->nUniqueMisses = 0; - RetValue = fread( &Num, 4, 1, pFile ); pTruth = ABC_ALLOC( word, p->nWords ); - for ( i = 0; i < Num; i++ ) - { - RetValue = fread( pTruth, sizeof(word)*p->nWords, 1, pFile ); - Vec_MemHashInsert( p->vTtMem, pTruth ); - } - ABC_FREE( pTruth ); - assert( Num == Vec_MemEntryNum(p->vTtMem) ); - RetValue = fread( &Num2, 4, 1, pFile ); - for ( i = 0; i < Num2; i++ ) + for ( v = 3; v <= p->nVars; v++ ) { + int nBytes = sizeof(word)*Vec_MemEntrySize(p->vTtMem[v]); RetValue = fread( &Num, 4, 1, pFile ); - vSets = Vec_IntAlloc( Num ); - RetValue = fread( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile ); - vSets->nSize = Num; - Vec_PtrPush( p->vTtDecs, vSets ); + for ( i = 0; i < Num; i++ ) + { + RetValue = fread( pTruth, nBytes, 1, pFile ); + Vec_MemHashInsert( p->vTtMem[v], pTruth ); + } + assert( Num == Vec_MemEntryNum(p->vTtMem[v]) ); + RetValue = fread( &Num2, 4, 1, pFile ); + for ( i = 0; i < Num2; i++ ) + { + RetValue = fread( &Num, 4, 1, pFile ); + vSets = Vec_IntAlloc( Num ); + RetValue = fread( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile ); + vSets->nSize = Num; + Vec_PtrPush( p->vTtDecs[v], vSets ); + } + assert( Num2 == Vec_PtrSize(p->vTtDecs[v]) ); } - assert( Num2 == Vec_PtrSize(p->vTtDecs) ); + ABC_FREE( pTruth ); fclose( pFile ); return p; } @@ -1203,7 +1293,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig } pPermStart += If_DsdObjSuppSize(pObj); } - If_DsdObjSort( p->vObjs, pChildren, nChildren, pBegEnd ); + If_DsdObjSort( p, p->vObjs, pChildren, nChildren, pBegEnd ); // create permutation for ( j = i = 0; i < nChildren; i++ ) for ( k = (pBegEnd[i] >> 16); k < (pBegEnd[i] & 0xFF); k++ ) @@ -1222,7 +1312,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig pLits[k] = Abc_LitNotCond( pLits[k], If_DsdManPushInv(p, pLits[k], pPermStart) ); pPermStart += pFanin->nSupp; } - RetValue = If_DsdObjCompare( p->vObjs, pLits[1], pLits[2] ); + RetValue = If_DsdObjCompare( p, p->vObjs, pLits[1], pLits[2] ); if ( RetValue == 1 || (RetValue == 0 && Abc_LitIsCompl(pLits[0])) ) { int nSupp0 = If_DsdVecLitSuppSize( p->vObjs, pLits[0] ); @@ -1513,9 +1603,9 @@ unsigned If_DsdManCheckMux( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int unsigned If_DsdManCheckPrime( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose ) { int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR]; - int truthId = If_DsdObjTruthId(pObj); + int truthId = If_DsdObjTruthId(p, pObj); int nFans = If_DsdObjFaninNum(pObj); - Vec_Int_t * vSets = (Vec_Int_t *)Vec_PtrEntry(p->vTtDecs, truthId); + Vec_Int_t * vSets = (Vec_Int_t *)Vec_PtrEntry(p->vTtDecs[pObj->nFans], truthId); if ( fVerbose ) printf( "\n" ); if ( fVerbose ) -- cgit v1.2.3