From 3d6eac52abb1fd05a0c954f00dd5b8b855765f6e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 28 Feb 2014 21:06:21 -0800 Subject: Changes to LUT mappers. --- src/map/if/if.h | 8 +- src/map/if/ifDsd.c | 622 ++++++++++++++++++++++++++++++++++------------------- src/map/if/ifMan.c | 22 +- src/map/if/ifMap.c | 57 ++--- src/map/if/ifSat.c | 24 +-- 5 files changed, 468 insertions(+), 265 deletions(-) (limited to 'src/map') diff --git a/src/map/if/if.h b/src/map/if/if.h index 47bd7390..c8b04ef1 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -517,12 +517,18 @@ extern int If_CluCheckExt( void * p, word * pTruth, int nVars, int n extern int If_CluCheckExt3( void * p, word * pTruth, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot, char * pLut0, char * pLut1, char * pLut2, word * pFunc0, word * pFunc1, word * pFunc2 ); /*=== ifDsd.c =============================================================*/ -extern If_DsdMan_t * If_DsdManAlloc( int nLutSize ); +extern If_DsdMan_t * If_DsdManAlloc( int nVars, int nLutSize ); extern void If_DsdManDump( If_DsdMan_t * p ); extern void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose ); extern void If_DsdManFree( If_DsdMan_t * p, int fVerbose ); +extern void If_DsdManSave( If_DsdMan_t * p, char * pFileName ); +extern If_DsdMan_t * If_DsdManLoad( char * pFileName ); extern int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct ); +extern char * If_DsdManFileName( If_DsdMan_t * p ); +extern int If_DsdManVarNum( If_DsdMan_t * p ); +extern int If_DsdManLutSize( If_DsdMan_t * p ); extern int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd ); +extern unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose ); /*=== ifLib.c =============================================================*/ extern If_LibLut_t * If_LibLutRead( char * FileName ); extern If_LibLut_t * If_LibLutDup( If_LibLut_t * p ); diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index 23160e62..a72362d7 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -53,7 +53,9 @@ struct If_DsdObj_t_ struct If_DsdMan_t_ { + char * pStore; // input/output file int nVars; // max var number + int LutSize; // LUT size int nWords; // word number int nBins; // table size unsigned * pBins; // hash table @@ -113,10 +115,10 @@ static inline void If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// - + /**Function************************************************************* - Synopsis [Sorting DSD literals.] + Synopsis [] Description [] @@ -125,114 +127,21 @@ static inline void If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj ) SeeAlso [] ***********************************************************************/ -int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 ) +char * If_DsdManFileName( If_DsdMan_t * p ) { - If_DsdObj_t * p0 = If_DsdVecObj(p, Abc_Lit2Var(iLit0)); - If_DsdObj_t * p1 = If_DsdVecObj(p, Abc_Lit2Var(iLit1)); - int i, Res; - if ( If_DsdObjType(p0) < If_DsdObjType(p1) ) - return -1; - if ( If_DsdObjType(p0) > If_DsdObjType(p1) ) - return 1; - if ( If_DsdObjType(p0) < IF_DSD_AND ) - return 0; - if ( If_DsdObjFaninNum(p0) < If_DsdObjFaninNum(p1) ) - return -1; - if ( If_DsdObjFaninNum(p0) > If_DsdObjFaninNum(p1) ) - return 1; - for ( i = 0; i < If_DsdObjFaninNum(p0); i++ ) - { - Res = If_DsdObjCompare( p, If_DsdObjFaninLit(p0, i), If_DsdObjFaninLit(p1, i) ); - if ( Res != 0 ) - return Res; - } - if ( Abc_LitIsCompl(iLit0) < Abc_LitIsCompl(iLit1) ) - return -1; - if ( Abc_LitIsCompl(iLit0) > Abc_LitIsCompl(iLit1) ) - return 1; - return 0; + return p->pStore; } -void If_DsdObjSort( Vec_Ptr_t * p, int * pLits, int nLits, int * pPerm ) +int If_DsdManVarNum( If_DsdMan_t * p ) { - 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 ) - best_i = j; - if ( i == best_i ) - continue; - ABC_SWAP( int, pLits[i], pLits[best_i] ); - if ( pPerm ) - ABC_SWAP( int, pPerm[i], pPerm[best_i] ); - } + return p->nVars; } - -/**Function************************************************************* - - Synopsis [Creating DSD objects.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans ) +int If_DsdManLutSize( If_DsdMan_t * p ) { - int nWords = If_DsdObjWordNum( nFans + (int)(Type == DAU_DSD_PRIME) ); - If_DsdObj_t * pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords ); - If_DsdObjClean( pObj ); - pObj->Type = Type; - pObj->nFans = nFans; - pObj->Id = Vec_PtrSize( p->vObjs ); - pObj->fMark = 0; - pObj->Count = 0; - Vec_PtrPush( p->vObjs, pObj ); - Vec_IntPush( p->vNexts, 0 ); - return pObj; + return p->LutSize; } -int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId ) +int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd ) { - If_DsdObj_t * pObj, * pFanin; - int i, iPrev = -1; - // check structural canonicity - assert( Type != DAU_DSD_MUX || nLits == 3 ); - assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[0]) ); - assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[1]) || !Abc_LitIsCompl(pLits[2]) ); - // check that leaves are in good order - if ( Type == DAU_DSD_AND || Type == DAU_DSD_XOR ) - { - for ( i = 0; i < nLits; i++ ) - { - 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 ); - iPrev = pLits[i]; - } - } - if ( Vec_PtrSize(p->vObjs) % p->nBins == 0 ) - printf( "Warning: The number of objects in If_DsdObjCreate() is more than the number of bins.\n" ); - // create new node - pObj = If_DsdObjAlloc( p, Type, nLits ); - if ( Type == DAU_DSD_PRIME ) - If_DsdObjSetTruth( p, pObj, truthId ); - assert( pObj->nSupp == 0 ); - for ( i = 0; i < nLits; i++ ) - { - pObj->pFans[i] = pLits[i]; - pObj->nSupp += If_DsdVecLitSuppSize(p->vObjs, pLits[i]); - } -/* - { - extern void If_DsdManPrintOne( If_DsdMan_t * p, int iDsdLit, int * pPermLits ); - If_DsdManPrintOne( p, If_DsdObj2Lit(pObj), NULL ); - } -*/ - return pObj->Id; + return If_DsdVecObjMark( p->vObjs, Abc_Lit2Var(iDsd) ); } /**Function************************************************************* @@ -258,17 +167,35 @@ static inline word ** If_ManDsdTtElems() } return pTtElems; } -If_DsdMan_t * If_DsdManAlloc( int nVars ) +If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans ) +{ + int nWords = If_DsdObjWordNum( nFans + (int)(Type == DAU_DSD_PRIME) ); + If_DsdObj_t * pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords ); + If_DsdObjClean( pObj ); + pObj->Type = Type; + pObj->nFans = nFans; + pObj->Id = Vec_PtrSize( p->vObjs ); + pObj->fMark = 0; + pObj->Count = 0; + Vec_PtrPush( p->vObjs, pObj ); + Vec_IntPush( p->vNexts, 0 ); + return pObj; +} +If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize ) { If_DsdMan_t * p; int v; + char pFileName[10]; + sprintf( pFileName, "%02d.dsd", nVars ); p = ABC_CALLOC( If_DsdMan_t, 1 ); - p->nVars = nVars; - p->nWords = Abc_TtWordNum( nVars ); - p->nBins = Abc_PrimeCudd( 1000000 ); - p->pBins = ABC_CALLOC( unsigned, p->nBins ); - p->pMem = Mem_FlexStart(); - p->vObjs = Vec_PtrAlloc( 10000 ); - p->vNexts = Vec_IntAlloc( 10000 ); + p->pStore = Abc_UtilStrsav( pFileName ); + p->nVars = nVars; + p->LutSize = LutSize; + p->nWords = Abc_TtWordNum( nVars ); + p->nBins = Abc_PrimeCudd( 1000000 ); + p->pBins = ABC_CALLOC( unsigned, p->nBins ); + p->pMem = Mem_FlexStart(); + p->vObjs = Vec_PtrAlloc( 10000 ); + p->vNexts = Vec_IntAlloc( 10000 ); If_DsdObjAlloc( p, IF_DSD_CONST0, 0 ); If_DsdObjAlloc( p, IF_DSD_VAR, 0 )->nSupp = 1; p->vNodes = Vec_IntAlloc( 32 ); @@ -284,8 +211,8 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose ) { int v; // If_DsdManDump( p ); - If_DsdManPrint( p, NULL, 0 ); - Vec_MemDumpTruthTables( p->vTtMem, "dumpdsd", p->nVars ); + if ( fVerbose ) + If_DsdManPrint( p, NULL, 0 ); if ( fVerbose ) { Abc_PrintTime( 1, "Time DSD ", p->timeDsd ); @@ -293,6 +220,8 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose ) Abc_PrintTime( 1, "Time check ", p->timeCheck ); Abc_PrintTime( 1, "Time verify", p->timeVerify ); } + if ( fVerbose ) + Vec_MemDumpTruthTables( p->vTtMem, "dumpdsd", p->nVars ); for ( v = 2; v < p->nVars; v++ ) ABC_FREE( p->pSched[v] ); Vec_VecFree( (Vec_Vec_t *)p->vTtDecs ); @@ -302,9 +231,46 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose ) Vec_IntFreeP( &p->vNexts ); Vec_PtrFreeP( &p->vObjs ); Mem_FlexStop( p->pMem, 0 ); + ABC_FREE( p->pStore ); ABC_FREE( p->pBins ); ABC_FREE( p ); } +void If_DsdManDump( If_DsdMan_t * p ) +{ + char * pFileName = "dss_tts.txt"; + FILE * pFile; + If_DsdObj_t * pObj; + int i; + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\".\n", pFileName ); + return; + } + If_DsdVecForEachObj( p->vObjs, pObj, i ) + { + if ( If_DsdObjType(pObj) != IF_DSD_PRIME ) + continue; + fprintf( pFile, "0x" ); + Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), p->nVars ); + fprintf( pFile, "\n" ); + printf( " " ); + Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars ); + } + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [Printing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void If_DsdManHashProfile( If_DsdMan_t * p ) { If_DsdObj_t * pObj; @@ -367,6 +333,7 @@ void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char fprintf( pFile, "%6d : ", iObjId ); fprintf( pFile, "%2d ", If_DsdVecObjSuppSize(p->vObjs, iObjId) ); fprintf( pFile, "%8d ", If_DsdVecObjRef(p->vObjs, iObjId) ); + fprintf( pFile, "%d ", If_DsdVecObjMark(p->vObjs, iObjId) ); If_DsdManPrint_rec( pFile, p, Abc_Var2Lit(iObjId, 0), pPermLits, &nSupp ); if ( fNewLine ) fprintf( pFile, "\n" ); @@ -400,7 +367,7 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose ) fprintf( pFile, "Memory used for objects = %8.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) ); fprintf( pFile, "Memory used for hash table = %8.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) ); fprintf( pFile, "Memory used for array = %8.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); +// Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); // If_DsdManHashProfile( p ); // If_DsdManDump( p ); // return; @@ -416,57 +383,6 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose ) if ( pFileName ) fclose( pFile ); } -void If_DsdManDump( If_DsdMan_t * p ) -{ - char * pFileName = "dss_tts.txt"; - FILE * pFile; - If_DsdObj_t * pObj; - int i; - pFile = fopen( pFileName, "wb" ); - if ( pFile == NULL ) - { - printf( "Cannot open file \"%s\".\n", pFileName ); - return; - } - If_DsdVecForEachObj( p->vObjs, pObj, i ) - { - if ( If_DsdObjType(pObj) != IF_DSD_PRIME ) - continue; - fprintf( pFile, "0x" ); - Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), p->nVars ); - fprintf( pFile, "\n" ); - printf( " " ); - Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars ); - } - fclose( pFile ); -} - -/**Function************************************************************* - - Synopsis [Collect nodes of the tree.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes ) -{ - int i, iFanin; - If_DsdObj_t * pObj = If_DsdVecObj( p->vObjs, Id ); - if ( If_DsdObjType(pObj) == IF_DSD_CONST0 || If_DsdObjType(pObj) == IF_DSD_VAR ) - return; - If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i ) - If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes ); - Vec_IntPush( vNodes, Id ); -} -void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes ) -{ - Vec_IntClear( vNodes ); - If_DsdManCollect_rec( p, Id, vNodes ); -} /**Function************************************************************* @@ -481,7 +397,6 @@ void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes ) ***********************************************************************/ static inline unsigned If_DsdObjHashKey( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId ) { -// static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 }; static int s_Primes[24] = { 1049, 1297, 1559, 1823, 2089, 2371, 2663, 2909, 3221, 3517, 3779, 4073, 4363, 4663, 4973, 5281, 5573, 5861, 6199, 6481, 6803, 7109, 7477, 7727 }; @@ -512,6 +427,43 @@ unsigned * If_DsdObjHashLookup( If_DsdMan_t * p, int Type, int * pLits, int nLit p->nUniqueMisses++; return pSpot; } +int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId ) +{ + If_DsdObj_t * pObj, * pFanin; + int i, iPrev = -1; + // check structural canonicity + assert( Type != DAU_DSD_MUX || nLits == 3 ); + assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[0]) ); + assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[1]) || !Abc_LitIsCompl(pLits[2]) ); + // check that leaves are in good order + if ( Type == DAU_DSD_AND || Type == DAU_DSD_XOR ) + { + for ( i = 0; i < nLits; i++ ) + { + 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 ); + iPrev = pLits[i]; + } + } + if ( Vec_PtrSize(p->vObjs) % p->nBins == 0 ) + printf( "Warning: The number of objects in If_DsdObjCreate() is more than the number of bins.\n" ); + // create new node + pObj = If_DsdObjAlloc( p, Type, nLits ); + if ( Type == DAU_DSD_PRIME ) + If_DsdObjSetTruth( p, pObj, truthId ); + assert( pObj->nSupp == 0 ); + for ( i = 0; i < nLits; i++ ) + { + pObj->pFans[i] = pLits[i]; + pObj->nSupp += If_DsdVecLitSuppSize(p->vObjs, pLits[i]); + } + // check decomposability + if ( p->LutSize && !If_DsdManCheckXY(p, Abc_Var2Lit(pObj->Id, 0), p->LutSize, 0, 0) ) + If_DsdVecObjSetMark( p->vObjs, pObj->Id ); + return pObj->Id; +} int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word * pTruth ) { int truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem, pTruth) : -1; @@ -534,6 +486,146 @@ p->timeCheck += Abc_Clock() - clk; } +/**Function************************************************************* + + Synopsis [Saving/loading DSD manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_DsdManSave( If_DsdMan_t * p, char * pFileName ) +{ + If_DsdObj_t * pObj; + Vec_Int_t * vSets; + char * pBuffer = "dsd0"; + word * pTruth; + int i, Num; + FILE * pFile = fopen( pFileName ? pFileName : p->pStore, "wb" ); + if ( pFile == NULL ) + { + printf( "Writing DSD manager file \"%s\" has failed.\n", pFileName ? pFileName : p->pStore ); + return; + } + fwrite( pBuffer, 4, 1, pFile ); + Num = p->nVars; + fwrite( &Num, 4, 1, pFile ); + Num = p->LutSize; + fwrite( &Num, 4, 1, pFile ); + Num = Vec_PtrSize(p->vObjs); + 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) ); + fwrite( &Num, 4, 1, pFile ); + fwrite( pObj, sizeof(word)*Num, 1, pFile ); + } + assert( Vec_MemEntryNum(p->vTtMem) == Vec_PtrSize(p->vTtDecs) ); + Num = Vec_MemEntryNum(p->vTtMem); + fwrite( &Num, 4, 1, pFile ); + Vec_MemForEachEntry( p->vTtMem, pTruth, i ) + fwrite( pTruth, sizeof(word)*p->nWords, 1, pFile ); + Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs, vSets, i ) + { + Num = Vec_IntSize(vSets); + fwrite( &Num, 4, 1, pFile ); + fwrite( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile ); + } + fclose( pFile ); +} +If_DsdMan_t * If_DsdManLoad( char * pFileName ) +{ + If_DsdMan_t * p; + If_DsdObj_t * pObj; + Vec_Int_t * vSets; + char pBuffer[10]; + unsigned * pSpot; + word * pTruth; + int i, Num; + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Reading DSD manager file \"%s\" has failed.\n", pFileName ); + return NULL; + } + fread( pBuffer, 4, 1, pFile ); + if ( pBuffer[0] != 'd' && pBuffer[1] != 's' && pBuffer[2] != 'd' && pBuffer[3] != '0' ) + { + printf( "Unrecognized format of file \"%s\".\n", pFileName ); + return NULL; + } + fread( &Num, 4, 1, pFile ); + p = If_DsdManAlloc( Num, 0 ); + ABC_FREE( p->pStore ); + p->pStore = Abc_UtilStrsav( pFileName ); + fread( &Num, 4, 1, pFile ); + p->LutSize = Num; + fread( &Num, 4, 1, pFile ); + assert( Num >= 2 ); + Vec_PtrFillExtra( p->vObjs, Num, NULL ); + Vec_IntFill( p->vNexts, Num, 0 ); + for ( i = 2; i < Vec_PtrSize(p->vObjs); i++ ) + { + fread( &Num, 4, 1, pFile ); + pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * Num ); + fread( pObj, sizeof(word)*Num, 1, pFile ); + Vec_PtrWriteEntry( p->vObjs, i, pObj ); + pSpot = If_DsdObjHashLookup( p, pObj->Type, pObj->pFans, pObj->nFans, If_DsdObjTruthId(p, pObj) ); + assert( *pSpot == 0 ); + *pSpot = pObj->Id; + } + fread( &Num, 4, 1, pFile ); + pTruth = ABC_ALLOC( word, p->nWords ); + for ( i = 0; i < Num; i++ ) + { + fread( pTruth, sizeof(word)*p->nWords, 1, pFile ); + Vec_MemHashInsert( p->vTtMem, pTruth ); + } + ABC_FREE( pTruth ); + assert( Num == Vec_MemEntryNum(p->vTtMem) ); + for ( i = 0; i < Vec_MemEntryNum(p->vTtMem); i++ ) + { + fread( &Num, 4, 1, pFile ); + vSets = Vec_IntAlloc( Num ); + fread( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile ); + vSets->nSize = Num; + Vec_PtrPush( p->vTtDecs, vSets ); + } + assert( Vec_MemEntryNum(p->vTtMem) == Vec_PtrSize(p->vTtDecs) ); + fclose( pFile ); + return p; +} + +/**Function************************************************************* + + Synopsis [Collect nodes of the tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes ) +{ + int i, iFanin; + If_DsdObj_t * pObj = If_DsdVecObj( p->vObjs, Id ); + if ( If_DsdObjType(pObj) == IF_DSD_CONST0 || If_DsdObjType(pObj) == IF_DSD_VAR ) + return; + If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i ) + If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes ); + Vec_IntPush( vNodes, Id ); +} +void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes ) +{ + Vec_IntClear( vNodes ); + If_DsdManCollect_rec( p, Id, vNodes ); +} + /**Function************************************************************* Synopsis [] @@ -617,6 +709,61 @@ word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLi assert( nSupp == If_DsdVecObjSuppSize(p->vObjs, Abc_Lit2Var(iDsd)) ); return pRes; } + +/**Function************************************************************* + + Synopsis [Sorting DSD literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_DsdObjCompare( 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)); + int i, Res; + if ( If_DsdObjType(p0) < If_DsdObjType(p1) ) + return -1; + if ( If_DsdObjType(p0) > If_DsdObjType(p1) ) + return 1; + if ( If_DsdObjType(p0) < IF_DSD_AND ) + return 0; + if ( If_DsdObjFaninNum(p0) < If_DsdObjFaninNum(p1) ) + return -1; + if ( If_DsdObjFaninNum(p0) > If_DsdObjFaninNum(p1) ) + return 1; + for ( i = 0; i < If_DsdObjFaninNum(p0); i++ ) + { + Res = If_DsdObjCompare( p, If_DsdObjFaninLit(p0, i), If_DsdObjFaninLit(p1, i) ); + if ( Res != 0 ) + return Res; + } + if ( Abc_LitIsCompl(iLit0) < Abc_LitIsCompl(iLit1) ) + return -1; + if ( Abc_LitIsCompl(iLit0) > Abc_LitIsCompl(iLit1) ) + return 1; + return 0; +} +void If_DsdObjSort( 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 ) + best_i = j; + if ( i == best_i ) + continue; + ABC_SWAP( int, pLits[i], pLits[best_i] ); + if ( pPerm ) + ABC_SWAP( int, pPerm[i], pPerm[best_i] ); + } +} /**Function************************************************************* @@ -697,13 +844,26 @@ int If_DsdManOperation2( If_DsdMan_t * p, int Type, int * pLits, int nLits ) SeeAlso [] ***********************************************************************/ +int If_DsdManComputeFirstArray( If_DsdMan_t * p, int * pLits, int nLits, int * pFirsts ) +{ + int i, nSSize = 0; + for ( i = 0; i < nLits; i++ ) + { + pFirsts[i] = nSSize; + nSSize += If_DsdVecLitSuppSize(p->vObjs, pLits[i]); + } + return nSSize; +} +int If_DsdManComputeFirst( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pFirsts ) +{ + return If_DsdManComputeFirstArray( p, pObj->pFans, pObj->nFans, pFirsts ); +} int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm, word * pTruth ) { If_DsdObj_t * pObj, * pFanin; unsigned char pPermNew[DAU_MAX_VAR]; int nChildren = 0, pChildren[DAU_MAX_VAR], pBegEnd[DAU_MAX_VAR]; int i, k, j, Id, iFanin, fComplFan, fCompl = 0, nSSize = 0; -// abctime clk; if ( Type == IF_DSD_AND ) { for ( k = 0; k < nLits; k++ ) @@ -813,11 +973,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig int i, uCanonPhase, pFirsts[DAU_MAX_VAR]; uCanonPhase = Abc_TtCanonicize( pTruth, nLits, pCanonPerm ); fCompl = ((uCanonPhase >> nLits) & 1); - for ( i = 0; i < nLits; i++ ) - { - pFirsts[i] = nSSize; - nSSize += If_DsdVecLitSuppSize(p->vObjs, pLits[i]); - } + nSSize = If_DsdManComputeFirstArray( p, pLits, nLits, pFirsts ); for ( j = i = 0; i < nLits; i++ ) { int iLitNew = Abc_LitNotCond( pLits[(int)pCanonPerm[i]], ((uCanonPhase>>i)&1) ); @@ -873,7 +1029,6 @@ int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * p fCompl = 1; (*p)++; } -// assert( !((**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9')) ); if ( **p >= 'a' && **p <= 'z' ) // var { pPerm[(*pnSupp)++] = Abc_Var2Lit( **p - 'a', fCompl ); @@ -952,6 +1107,23 @@ int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char SeeAlso [] ***********************************************************************/ +// create signature of the support of the node +unsigned If_DsdSign_rec( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pnSupp ) +{ + unsigned uSign = 0; int i; + If_DsdObj_t * pFanin; + if ( If_DsdObjType(pObj) == IF_DSD_VAR ) + return (1 << (2*(*pnSupp)++)); + If_DsdObjForEachFanin( p->vObjs, pObj, pFanin, i ) + uSign |= If_DsdSign_rec( p, pFanin, pnSupp ); + return uSign; +} +unsigned If_DsdSign( If_DsdMan_t * p, If_DsdObj_t * pObj, int iFan, int iFirst, int fShared ) +{ + If_DsdObj_t * pFanin = If_DsdObjFanin( p->vObjs, pObj, iFan ); + unsigned uSign = If_DsdSign_rec( p, pFanin, &iFirst ); + return fShared ? (uSign << 1) | uSign : uSign; +} // collect supports of the node void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes ) { @@ -960,10 +1132,10 @@ void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes ) pSSizes[i] = If_DsdObjSuppSize(pFanin); } // checks if there is a way to package some fanins -int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose ) +unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose ) { int i[6], LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR]; - int nFans = If_DsdObjFaninNum(pObj); + int nFans = If_DsdObjFaninNum(pObj), pFirsts[DAU_MAX_VAR]; assert( pObj->nFans > 2 ); assert( If_DsdObjSuppSize(pObj) > LutSize ); If_DsdManGetSuppSizes( p, pObj, pSSizes ); @@ -976,7 +1148,10 @@ int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int SizeOut = pObj->nSupp - SizeIn; if ( SizeIn > LutSize || SizeOut > LimitOut ) continue; - return (1 << i[0]) | (1 << i[1]); + if ( !fDerive ) + return ~0; + If_DsdManComputeFirst( p, pObj, pFirsts ); + return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0); } if ( pObj->nFans == 3 ) return 0; @@ -988,7 +1163,10 @@ int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int SizeOut = pObj->nSupp - SizeIn; if ( SizeIn > LutSize || SizeOut > LimitOut ) continue; - return (1 << i[0]) | (1 << i[1]) | (1 << i[2]); + if ( !fDerive ) + return ~0; + If_DsdManComputeFirst( p, pObj, pFirsts ); + return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0) | If_DsdSign(p, pObj, i[2], pFirsts[i[2]], 0); } if ( pObj->nFans == 4 ) return 0; @@ -1001,14 +1179,17 @@ int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int SizeOut = pObj->nSupp - SizeIn; if ( SizeIn > LutSize || SizeOut > LimitOut ) continue; - return (1 << i[0]) | (1 << i[1]) | (1 << i[2]) | (1 << i[3]); + if ( !fDerive ) + return ~0; + If_DsdManComputeFirst( p, pObj, pFirsts ); + return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0) | If_DsdSign(p, pObj, i[2], pFirsts[i[2]], 0) | If_DsdSign(p, pObj, i[3], pFirsts[i[3]], 0); } return 0; } // checks if there is a way to package some fanins -int If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose ) +unsigned If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose ) { - int LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR]; + int LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR]; assert( If_DsdObjFaninNum(pObj) == 3 ); assert( If_DsdObjSuppSize(pObj) > LutSize ); If_DsdManGetSuppSizes( p, pObj, pSSizes ); @@ -1019,21 +1200,27 @@ int If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int Lu SizeOut = pSSizes[2]; if ( SizeIn <= LutSize && SizeOut <= LimitOut ) { - return 1; + if ( !fDerive ) + return ~0; + If_DsdManComputeFirst( p, pObj, pFirsts ); + return If_DsdSign(p, pObj, 0, pFirsts[0], 1) | If_DsdSign(p, pObj, 1, pFirsts[1], 0); } // second input SizeIn = pSSizes[0] + pSSizes[2]; SizeOut = pSSizes[1]; if ( SizeIn <= LutSize && SizeOut <= LimitOut ) { - return 1; + if ( !fDerive ) + return ~0; + If_DsdManComputeFirst( p, pObj, pFirsts ); + return If_DsdSign(p, pObj, 0, pFirsts[0], 1) | If_DsdSign(p, pObj, 2, pFirsts[2], 0); } return 0; } // checks if there is a way to package some fanins -int If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose ) +unsigned If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose ) { - int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR]; + int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR]; int truthId = If_DsdObjTruthId( p, pObj ); int nFans = If_DsdObjFaninNum(pObj); Vec_Int_t * vSets = (Vec_Int_t *)Vec_PtrEntry(p->vTtDecs, truthId); @@ -1066,11 +1253,29 @@ Dau_DecPrintSets( vSets, nFans ); break; } if ( v == nFans ) - return set; + { + unsigned uSign; + if ( !fDerive ) + return ~0; + uSign = 0; + If_DsdManComputeFirst( p, pObj, pFirsts ); + for ( v = 0; v < nFans; v++ ) + { + int Value = ((set >> (v << 1)) & 3); + if ( Value == 0 ) + {} + else if ( Value == 1 ) + uSign |= If_DsdSign(p, pObj, v, pFirsts[v], 0); + else if ( Value == 3 ) + uSign |= If_DsdSign(p, pObj, v, pFirsts[v], 1); + else assert( Value == 0 ); + } + return uSign; + } } return 0; } -int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose ) +unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose ) { If_DsdObj_t * pObj, * pTemp; int i, Mask; pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) ); @@ -1080,7 +1285,7 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose ) { if ( fVerbose ) printf( " Trivial\n" ); - return 1; + return ~0; } If_DsdManCollect( p, pObj->Id, p->vNodes ); If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) @@ -1090,12 +1295,12 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose ) printf( " Dec using node " ); if ( fVerbose ) If_DsdManPrintOne( stdout, p, pTemp->Id, NULL, 1 ); - return 1; + return ~0; } If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) if ( (If_DsdObjType(pTemp) == IF_DSD_AND || If_DsdObjType(pTemp) == IF_DSD_XOR) && If_DsdObjFaninNum(pTemp) > 2 && If_DsdObjSuppSize(pTemp) > LutSize ) { - if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) ) + if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) ) { if ( fVerbose ) printf( " " ); @@ -1103,13 +1308,13 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose ) Abc_TtPrintBinary( (word *)&Mask, 4 ); if ( fVerbose ) printf( " Using multi-input AND/XOR node\n" ); - return 1; + return Mask; } } If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) if ( If_DsdObjType(pTemp) == IF_DSD_MUX && If_DsdObjSuppSize(pTemp) > LutSize ) { - if ( (Mask = If_DsdManCheckMux(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) ) + if ( (Mask = If_DsdManCheckMux(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) ) { if ( fVerbose ) printf( " " ); @@ -1117,13 +1322,13 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose ) Abc_TtPrintBinary( (word *)&Mask, 4 ); if ( fVerbose ) printf( " Using multi-input MUX node\n" ); - return 1; + return Mask; } } If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) if ( If_DsdObjType(pTemp) == IF_DSD_PRIME && If_DsdObjSuppSize(pTemp) > LutSize ) { - if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) ) + if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) ) { if ( fVerbose ) printf( " " ); @@ -1131,19 +1336,14 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose ) Dau_DecPrintSet( Mask, If_DsdObjFaninNum(pTemp), 0 ); if ( fVerbose ) printf( " Using prime node\n" ); - return 1; + return Mask; } } if ( fVerbose ) printf( " UNDEC\n" ); - // If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 ); return 0; } -int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize ) -{ - return 1; -} /**Function************************************************************* @@ -1156,9 +1356,9 @@ int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize ) SeeAlso [] ***********************************************************************/ -int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd ) +unsigned If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose ) { - return If_DsdVecObjMark( p->vObjs, Abc_Lit2Var(iDsd) ); + return ~0; } /**Function************************************************************* @@ -1183,17 +1383,6 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char clk = Abc_Clock(); nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 1, pDsd ); p->timeDsd += Abc_Clock() - clk; -/* - if ( nLeaves <= 6 ) - { - word pCopy2[DAU_MAX_WORD], t; - char pDsd2[DAU_MAX_STR]; - Abc_TtCopy( pCopy2, pTruth, p->nWords, 0 ); - nSizeNonDec = Dau_DsdDecompose( pCopy2, nLeaves, 0, 1, pDsd2 ); - t = Dau_Dsd6ToTruth( pDsd2 ); - assert( t == *pTruth ); - } -*/ // if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") ) // { // int x = 0; @@ -1217,18 +1406,9 @@ p->timeVerify += Abc_Clock() - clk; printf( "%s\n", pDsd ); Dau_DsdPrintFromTruth( pTruth, nLeaves ); Dau_DsdPrintFromTruth( pRes, nLeaves ); -// Kit_DsdPrintFromTruth( (unsigned *)pTruth, nLeaves ); printf( "\n" ); -// Kit_DsdPrintFromTruth( (unsigned *)pRes, nLeaves ); printf( "\n" ); If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm, 1 ); printf( "\n" ); } - if ( pLutStruct && If_DsdVecObjRef(p->vObjs, Abc_Lit2Var(iDsd)) ) - { - int LutSize = (int)(pLutStruct[0] - '0'); - assert( pLutStruct[2] == 0 ); // XY - if ( !If_DsdManCheckXY( p, iDsd, LutSize, 0 ) ) - If_DsdVecObjSetMark( p->vObjs, Abc_Lit2Var(iDsd) ); - } If_DsdVecObjIncRef( p->vObjs, Abc_Lit2Var(iDsd) ); return iDsd; } diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index d03fc200..686af7ae 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -85,7 +85,6 @@ If_Man_t * If_ManStart( If_Par_t * pPars ) p->puTempW = p->pPars->fTruth? ABC_ALLOC( word, p->nTruth6Words ) : NULL; if ( pPars->fUseDsd ) { - p->pIfDsdMan = If_DsdManAlloc( pPars->nLutSize ); p->vTtDsds = Vec_IntAlloc( 1000 ); Vec_IntPush( p->vTtDsds, 0 ); Vec_IntPush( p->vTtDsds, 2 ); @@ -142,6 +141,15 @@ void If_ManRestart( If_Man_t * p ) ***********************************************************************/ void If_ManStop( If_Man_t * p ) { +/* + if ( p->pIfDsdMan ) + { + If_DsdMan_t * pNew; + If_DsdManSave( p->pIfDsdMan, NULL ); + pNew = If_DsdManLoad( If_DsdManFileName(p->pIfDsdMan) ); + If_DsdManFree( pNew, 1 ); + } +*/ { // extern void If_CluHashFindMedian( If_Man_t * p ); // extern void If_CluHashTableCheck( If_Man_t * p ); @@ -158,11 +166,13 @@ void If_ManStop( If_Man_t * p ) Abc_Print( 1, "Useless cuts %2d = %9d (out of %9d) (%6.2f %%)\n", i, p->nCutsUseless[i], p->nCutsCount[i], 100.0*p->nCutsUseless[i]/(p->nCutsCount[i]+1) ); Abc_Print( 1, "Useless cuts all = %9d (out of %9d) (%6.2f %%)\n", p->nCutsUselessAll, p->nCutsCountAll, 100.0*p->nCutsUselessAll/(p->nCutsCountAll+1) ); } - if ( p->pPars->fVerbose && p->nCuts5 ) - Abc_Print( 1, "Statistics about 5-cuts: Total = %d Non-decomposable = %d (%.2f %%)\n", p->nCuts5, p->nCuts5-p->nCuts5a, 100.0*(p->nCuts5-p->nCuts5a)/p->nCuts5 ); - if ( p->pPars->fUseDsd ) - If_DsdManFree( p->pIfDsdMan, p->pPars->fVerbose ); - if ( p->pPars->fUseDsd ) +// if ( p->pPars->fVerbose && p->nCuts5 ) +// Abc_Print( 1, "Statistics about 5-cuts: Total = %d Non-decomposable = %d (%.2f %%)\n", p->nCuts5, p->nCuts5-p->nCuts5a, 100.0*(p->nCuts5-p->nCuts5a)/p->nCuts5 ); +// if ( p->pPars->fUseDsd ) +// If_DsdManFree( p->pIfDsdMan, p->pPars->fVerbose ); + if ( p->pIfDsdMan ) + p->pIfDsdMan = NULL; + if ( p->pPars->fUseDsd && (p->nCountNonDec[0] || p->nCountNonDec[1]) ) printf( "NonDec0 = %d. NonDec1 = %d.\n", p->nCountNonDec[0], p->nCountNonDec[1] ); // Abc_PrintTime( 1, "Truth", p->timeTruth ); // Abc_Print( 1, "Small support = %d.\n", p->nSmallSupp ); diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index d7b7f4cc..5c23c1b6 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -217,12 +217,39 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep // abctime clk = Abc_Clock(); If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 ); // p->timeTruth += Abc_Clock() - clk; + if ( p->pPars->fUseDsd ) + { + int truthId = Abc_Lit2Var(pCut->iCutFunc); + if ( Vec_IntSize(p->vTtDsds) <= truthId || Vec_IntEntry(p->vTtDsds, truthId) == -1 ) + { + pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct ); +// printf( "%d(%d) ", pCut->iCutDsd, If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ) ); + while ( Vec_IntSize(p->vTtDsds) <= truthId ) + { + Vec_IntPush( p->vTtDsds, -1 ); + for ( v = 0; v < p->pPars->nLutSize; v++ ) + Vec_StrPush( p->vTtPerms, IF_BIG_CHAR ); + } + Vec_IntWriteEntry( p->vTtDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) ); + for ( v = 0; v < (int)pCut->nLeaves; v++ ) + Vec_StrWriteEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v, (char)pCut->pPerm[v] ); + } + else + { + pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) ); + for ( v = 0; v < (int)pCut->nLeaves; v++ ) + pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v ); + } + } // run user functions pCut->fUseless = 0; if ( p->pPars->pFuncCell ) { assert( pCut->nLimit >= 4 && pCut->nLimit <= 16 ); - pCut->fUseless = !p->pPars->pFuncCell( p, If_CutTruth(p, pCut), pCut->nLimit, pCut->nLeaves, p->pPars->pLutStruct ); + if ( p->pPars->fUseDsd ) + pCut->fUseless = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ); + else + pCut->fUseless = !p->pPars->pFuncCell( p, If_CutTruth(p, pCut), pCut->nLimit, pCut->nLeaves, p->pPars->pLutStruct ); p->nCutsUselessAll += pCut->fUseless; p->nCutsUseless[pCut->nLeaves] += pCut->fUseless; p->nCutsCountAll++; @@ -251,29 +278,9 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep p->nCuts5a++; } } +/* if ( p->pPars->fUseDsd ) { - int truthId = Abc_Lit2Var(pCut->iCutFunc); - if ( Vec_IntSize(p->vTtDsds) <= truthId || Vec_IntEntry(p->vTtDsds, truthId) == -1 ) - { - pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct ); -// printf( "%d(%d) ", pCut->iCutDsd, If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ) ); - while ( Vec_IntSize(p->vTtDsds) <= truthId ) - { - Vec_IntPush( p->vTtDsds, -1 ); - for ( v = 0; v < p->pPars->nLutSize; v++ ) - Vec_StrPush( p->vTtPerms, IF_BIG_CHAR ); - } - Vec_IntWriteEntry( p->vTtDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) ); - for ( v = 0; v < (int)pCut->nLeaves; v++ ) - Vec_StrWriteEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v, (char)pCut->pPerm[v] ); - } - else - { - pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) ); - for ( v = 0; v < (int)pCut->nLeaves; v++ ) - pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v ); - } if ( p->pPars->pLutStruct ) { int Value = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ); @@ -283,7 +290,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep p->nCountNonDec[0]++; if ( !pCut->fUseless && Value ) p->nCountNonDec[1]++; -/* + // if ( pCut->fUseless && !Value ) // printf( "Old does not work. New works.\n" ); if ( !pCut->fUseless && Value ) @@ -307,14 +314,14 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep z = If_Dec6Perform( t, 1 ); If_DecPrintConfig( z ); - s = If_DsdManCheckXY( p->pIfDsdMan, pCut->iCutDsd, 4, 1 ); + s = If_DsdManCheckXY( p->pIfDsdMan, pCut->iCutDsd, 4, 0, 1 ); printf( "Confirm %d\n", s ); s = 0; } -*/ } } } +*/ } // compute the application-specific cost and depth diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c index 5ddb8241..3fec34e0 100644 --- a/src/map/if/ifSat.c +++ b/src/map/if/ifSat.c @@ -204,46 +204,46 @@ void If_ManSatTest() uSet = (3 << 0) | (1 << 2) | (1 << 4); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); - printf( "%d", RetValue ); + printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) ); uSet = (1 << 0) | (3 << 2) | (1 << 4); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); - printf( "%d", RetValue ); + printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) ); uSet = (1 << 0) | (1 << 2) | (3 << 4); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); - printf( "%d", RetValue ); + printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) ); uSet = (3 << 0) | (1 << 2) | (1 << 6); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); - printf( "%d", RetValue ); + printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) ); uSet = (1 << 0) | (3 << 2) | (1 << 6); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); - printf( "%d", RetValue ); + printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) ); uSet = (1 << 0) | (1 << 2) | (3 << 6); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); - printf( "%d", RetValue ); + printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) ); uSet = (3 << 0) | (1 << 4) | (1 << 6); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); - printf( "%d", RetValue ); + printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) ); uSet = (1 << 0) | (3 << 4) | (1 << 6); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); - printf( "%d", RetValue ); + printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) ); uSet = (1 << 0) | (1 << 4) | (3 << 6); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); - printf( "%d", RetValue ); + printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) ); uSet = (3 << 2) | (1 << 4) | (1 << 6); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); - printf( "%d", RetValue ); + printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) ); uSet = (1 << 2) | (3 << 4) | (1 << 6); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); - printf( "%d", RetValue ); + printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) ); uSet = (1 << 2) | (1 << 4) | (3 << 6); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); - printf( "%d", RetValue ); + printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) ); printf( "\n" ); -- cgit v1.2.3