From ee789ba902b6f2c443717bdcb82506ecb6aed3b8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 10 Nov 2012 19:37:53 -0800 Subject: Improved DSD. --- src/base/abci/abc.c | 8 +- src/map/if/if.h | 7 +- src/map/if/ifMan.c | 19 +++++ src/map/if/ifMap.c | 57 ++++++++++++- src/opt/dau/dau.h | 4 +- src/opt/dau/dauDsd.c | 8 ++ src/opt/dau/dauMerge.c | 211 +++++++++++++++++++++++++++++++++++++------------ 7 files changed, 256 insertions(+), 58 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3941fe5d..4395607d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -14541,7 +14541,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) fLutMux = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGDEWSqaflepmrsdbugyojikcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGDEWSqaflepmrsdbugyojikcnvh" ) ) != EOF ) { switch ( c ) { @@ -14706,6 +14706,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'c': pPars->fEnableRealPos ^= 1; break; + case 'n': + pPars->fUseDsd ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -14958,7 +14961,7 @@ usage: sprintf(LutSize, "library" ); else sprintf(LutSize, "%d", pPars->nLutSize ); - Abc_Print( -2, "usage: if [-KCFAG num] [-DEW float] [-S str] [-qarlepmsdbugyojikcvh]\n" ); + Abc_Print( -2, "usage: if [-KCFAG num] [-DEW float] [-S str] [-qarlepmsdbugyojikcnvh]\n" ); Abc_Print( -2, "\t performs FPGA technology mapping of the network\n" ); Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize ); Abc_Print( -2, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax ); @@ -14988,6 +14991,7 @@ usage: Abc_Print( -2, "\t-i : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck08? "yes": "no" ); Abc_Print( -2, "\t-k : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck10? "yes": "no" ); Abc_Print( -2, "\t-c : toggles enabling additional feature [default = %s]\n", pPars->fEnableRealPos? "yes": "no" ); + Abc_Print( -2, "\t-n : toggles computing DSDs of the cut functions [default = %s]\n", pPars->fUseDsd? "yes": "no" ); Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : prints the command usage\n"); return 1; diff --git a/src/map/if/if.h b/src/map/if/if.h index 04ff59e4..6a2fdd5d 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -34,7 +34,7 @@ #include "misc/vec/vec.h" #include "misc/mem/mem.h" #include "misc/tim/tim.h" - +#include "misc/util/utilNam.h" ABC_NAMESPACE_HEADER_START @@ -116,6 +116,7 @@ struct If_Par_t_ int fEnableCheck08;// enable additional checking int fEnableCheck10;// enable additional checking int fEnableRealPos;// enable additional feature + int fUseDsd; // compute DSD of the cut functions int fVerbose; // the verbosity flag char * pLutStruct; // LUT structure float WireDelay; // wire delay @@ -215,6 +216,9 @@ struct If_Man_t_ int nCutsCount[32]; int nCutsCountAll; int nCutsUselessAll; + Abc_Nam_t * pNamDsd; + int iNamVar; + // timing manager Tim_Man_t * pManTim; Vec_Int_t * vCoAttrs; // CO attributes 0=optimize; 1=keep; 2=relax @@ -235,6 +239,7 @@ struct If_Cut_t_ float Edge; // the edge flow float Power; // the power flow float Delay; // delay of the cut + int iDsd; // DSD ID of the cut unsigned uSign; // cut signature unsigned Cost : 13; // the user's cost of the cut (related to IF_COST_MAX) unsigned fCompl : 1; // the complemented attribute diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index 0ebdec1b..db63a831 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -32,6 +32,8 @@ static If_Obj_t * If_ManSetupObj( If_Man_t * p ); static void If_ManCutSetRecycle( If_Man_t * p, If_Set_t * pSet ) { pSet->pNext = p->pFreeList; p->pFreeList = pSet; } static If_Set_t * If_ManCutSetFetch( If_Man_t * p ) { If_Set_t * pTemp = p->pFreeList; p->pFreeList = p->pFreeList->pNext; return pTemp; } +extern clock_t s_TimeComp[3]; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -79,6 +81,11 @@ If_Man_t * If_ManStart( If_Par_t * pPars ) p->puTemp[2] = p->puTemp[1] + p->nTruthWords; p->puTemp[3] = p->puTemp[2] + p->nTruthWords; p->pCutTemp = (If_Cut_t *)ABC_ALLOC( char, p->nCutBytes ); + if ( pPars->fUseDsd ) + { + p->pNamDsd = Abc_NamStart( 1000, 20 ); + p->iNamVar = Abc_NamStrFindOrAdd( p->pNamDsd, "a", NULL ); + } // create the constant node p->pConst1 = If_ManSetupObj( p ); @@ -143,6 +150,17 @@ 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->pNamDsd ) + { + if ( p->pPars->fVerbose ) + Abc_Print( 1, "Number of unique entries in the DSD table = %d. Memory = %.1f MB.\n", + Abc_NamObjNumMax(p->pNamDsd), 1.0*Abc_NamMemAlloc(p->pNamDsd)/(1<<20) ); + Abc_PrintTime( 1, "Time0", s_TimeComp[0] ); + Abc_PrintTime( 1, "Time1", s_TimeComp[1] ); + Abc_PrintTime( 1, "Time2", s_TimeComp[2] ); +// Abc_NamPrint( p->pNamDsd ); + Abc_NamStop( p->pNamDsd ); + } // Abc_PrintTime( 1, "Truth", p->timeTruth ); // Abc_Print( 1, "Small support = %d.\n", p->nSmallSupp ); Vec_IntFreeP( &p->vCoAttrs ); @@ -408,6 +426,7 @@ void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId ) pCut->nLeaves = 1; pCut->pLeaves[0] = p->pPars->fLiftLeaves? (ObjId << 8) : ObjId; pCut->uSign = If_ObjCutSign( pCut->pLeaves[0] ); + pCut->iDsd = p->iNamVar; // set up elementary truth table of the unit cut if ( p->pPars->fTruth ) { diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index d4d0d1dd..cb3c6832 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -27,6 +27,8 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1 ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -78,6 +80,50 @@ float If_CutDelaySpecial( If_Man_t * p, If_Cut_t * pCut, int fCarry ) } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int * If_CutPerm0( If_Cut_t * pCut, If_Cut_t * pCut0 ) +{ + static int pPerm[IF_MAX_LUTSIZE]; + int i, k; + for ( i = k = 0; i < (int)pCut->nLeaves; i++ ) + { + if ( k == (int)pCut0->nLeaves ) + break; + if ( pCut->pLeaves[i] < pCut0->pLeaves[k] ) + continue; + assert( pCut->pLeaves[i] == pCut0->pLeaves[k] ); + pPerm[k++] = i; + } + return pPerm; +} +static inline int * If_CutPerm1( If_Cut_t * pCut, If_Cut_t * pCut1 ) +{ + static int pPerm[IF_MAX_LUTSIZE]; + int i, k; + for ( i = k = 0; i < (int)pCut->nLeaves; i++ ) + { + if ( k == (int)pCut1->nLeaves ) + break; + if ( pCut->pLeaves[i] < pCut1->pLeaves[k] ) + continue; + assert( pCut->pLeaves[i] == pCut1->pLeaves[k] ); + pPerm[k++] = i; + } + return pPerm; +} + + + /**Function************************************************************* Synopsis [Finds the best cut for the given node.] @@ -227,7 +273,16 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep p->nCutsCountAll++; p->nCutsCount[pCut->nLeaves]++; } - + } + if ( p->pPars->fUseDsd ) + { + char * pName = Dau_DsdMerge( + Abc_NamStr(p->pNamDsd, pCut0->iDsd), + If_CutPerm0(pCut, pCut0), + Abc_NamStr(p->pNamDsd, pCut1->iDsd), + If_CutPerm1(pCut, pCut1), + pObj->fCompl0, pObj->fCompl1 ); + pCut->iDsd = Abc_NamStrFindOrAdd( p->pNamDsd, pName, NULL ); } // compute the application-specific cost and depth diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h index f9d4f2b2..277da3d3 100644 --- a/src/opt/dau/dau.h +++ b/src/opt/dau/dau.h @@ -39,8 +39,8 @@ ABC_NAMESPACE_HEADER_START -#define DAU_MAX_VAR 16 // should be 6 or more -#define DAU_MAX_STR 256 +#define DAU_MAX_VAR 8 // should be 6 or more +#define DAU_MAX_STR 64 #define DAU_MAX_WORD (1<<(DAU_MAX_VAR-6)) //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c index 80782429..fbba16db 100644 --- a/src/opt/dau/dauDsd.c +++ b/src/opt/dau/dauDsd.c @@ -184,6 +184,14 @@ void Dau_DsdNormalize_rec( char * pStr, char ** p, int * pMatches ) static char pBuffer[DAU_MAX_STR]; if ( **p == '!' ) (*p)++; + while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') ) + (*p)++; + if ( **p == '<' ) + { + char * q = pStr + pMatches[*p - pStr]; + if ( *(q+1) == '{' ) + *p = q+1; + } if ( **p >= 'a' && **p <= 'f' ) // var return; if ( **p == '(' || **p == '[' ) // and/or/xor diff --git a/src/opt/dau/dauMerge.c b/src/opt/dau/dauMerge.c index cbb8e145..8ab39568 100644 --- a/src/opt/dau/dauMerge.c +++ b/src/opt/dau/dauMerge.c @@ -32,6 +32,22 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Substitution storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Dau_DsdIsConst( char * p ) { return (p[0] == '0' || p[0] == '1') && p[1] == 0; } +static inline int Dau_DsdIsConst0( char * p ) { return p[0] == '0' && p[1] == 0; } +static inline int Dau_DsdIsConst1( char * p ) { return p[0] == '1' && p[1] == 0; } + + /**Function************************************************************* Synopsis [Substitution storage.] @@ -46,20 +62,21 @@ ABC_NAMESPACE_IMPL_START typedef struct Dau_Sto_t_ Dau_Sto_t; struct Dau_Sto_t_ { - int iVarUsed; // counter of used variables - char pOutput[DAU_MAX_STR]; // storage for reduced function - char * pPosOutput; // place in the output - char pStore[DAU_MAX_STR]; // storage for definitions - char * pPosStore; // place in the store - char * pVarDefs[DAU_MAX_VAR];// variable definition (inside pStore) + int iVarUsed; // counter of used variables + char pOutput[DAU_MAX_STR]; // storage for reduced function + char * pPosOutput; // place in the output + char pStore[DAU_MAX_VAR][DAU_MAX_STR]; // storage for definitions + char * pPosStore[DAU_MAX_VAR]; // place in the store }; static inline void Dau_DsdMergeStoreClean( Dau_Sto_t * pS, int nShared ) { + int i; pS->iVarUsed = nShared; - pS->pPosStore = pS->pStore; - memset( pS->pVarDefs, 0, sizeof(char *) * DAU_MAX_VAR ); + for ( i = 0; i < DAU_MAX_VAR; i++ ) + pS->pStore[i][0] = 0; } + static inline void Dau_DsdMergeStoreCleanOutput( Dau_Sto_t * pS ) { pS->pPosOutput = pS->pOutput; @@ -74,39 +91,40 @@ static inline void Dau_DsdMergeStoreAddToOutputChar( Dau_Sto_t * pS, char c ) *pS->pPosOutput++ = c; } -static inline void Dau_DsdMergeStoreStartDef( Dau_Sto_t * pS, char c ) +static inline int Dau_DsdMergeStoreStartDef( Dau_Sto_t * pS, char c ) { - pS->pVarDefs[pS->iVarUsed] = pS->pPosStore; - if (c) *pS->pPosStore++ = c; + pS->pPosStore[pS->iVarUsed] = pS->pStore[pS->iVarUsed]; + if (c) *pS->pPosStore[pS->iVarUsed]++ = c; + return pS->iVarUsed++; } -static inline void Dau_DsdMergeStoreAddToDef( Dau_Sto_t * pS, char * pBeg, char * pEnd ) +static inline void Dau_DsdMergeStoreAddToDef( Dau_Sto_t * pS, int New, char * pBeg, char * pEnd ) { while ( pBeg < pEnd ) - *pS->pPosStore++ = *pBeg++; + *pS->pPosStore[New]++ = *pBeg++; } -static inline void Dau_DsdMergeStoreAddToDefChar( Dau_Sto_t * pS, char c ) +static inline void Dau_DsdMergeStoreAddToDefChar( Dau_Sto_t * pS, int New, char c ) { - *pS->pPosStore++ = c; + *pS->pPosStore[New]++ = c; } -static inline char Dau_DsdMergeStoreStopDef( Dau_Sto_t * pS, char c ) +static inline void Dau_DsdMergeStoreStopDef( Dau_Sto_t * pS, int New, char c ) { - if (c) *pS->pPosStore++ = c; - *pS->pPosStore++ = 0; - return 'a' + pS->iVarUsed++; + if (c) *pS->pPosStore[New]++ = c; + *pS->pPosStore[New]++ = 0; } static inline char Dau_DsdMergeStoreCreateDef( Dau_Sto_t * pS, char * pBeg, char * pEnd ) { - Dau_DsdMergeStoreStartDef( pS, 0 ); - Dau_DsdMergeStoreAddToDef( pS, pBeg, pEnd ); - return Dau_DsdMergeStoreStopDef( pS, 0 ); + int New = Dau_DsdMergeStoreStartDef( pS, 0 ); + Dau_DsdMergeStoreAddToDef( pS, New, pBeg, pEnd ); + Dau_DsdMergeStoreStopDef( pS, New, 0 ); + return New; } static inline void Dau_DsdMergeStorePrintDefs( Dau_Sto_t * pS ) { int i; for ( i = 0; i < DAU_MAX_VAR; i++ ) - if ( pS->pVarDefs[i] != NULL ) - printf( "%c = %s\n", 'a' + i, pS->pVarDefs[i] ); + if ( pS->pStore[i][0] ) + printf( "%c = %s\n", 'a' + i, pS->pStore[i] ); } /**Function************************************************************* @@ -124,7 +142,7 @@ static inline void Dau_DsdMergeCopy( char * pDsd, int fCompl, char * pRes ) { if ( fCompl && pDsd[0] == '!' ) fCompl = 0, pDsd++; - if ( pDsd[1] == 0 ) // constant + if ( Dau_DsdIsConst(pDsd) ) // constant pRes[0] = (fCompl ? (char)((int)pDsd[0] ^ 1) : pDsd[0]), pRes[1] = 0; else sprintf( pRes, "%s%s", fCompl ? "!" : "", pDsd ); @@ -226,7 +244,7 @@ static inline int Dau_DsdMergeCreateMaps( int * pVarPres, int nShared, int * pOl } return Counter2; } -static inline void Dau_DsdMergeInlineDefinitions( char * pDsd, int * pMatches, char ** pVarDefs, char * pRes, int nShared ) +static inline void Dau_DsdMergeInlineDefinitions( char * pDsd, int * pMatches, Dau_Sto_t * pS, char * pRes, int nShared ) { int i; char * pDef; @@ -251,7 +269,7 @@ static inline void Dau_DsdMergeInlineDefinitions( char * pDsd, int * pMatches, c } // inline definition assert( pDsd[i]-'a' < DAU_MAX_STR ); - for ( pDef = pVarDefs[pDsd[i]-'a']; *pDef; pDef++ ) + for ( pDef = pS->pStore[pDsd[i]-'a']; *pDef; pDef++ ) *pRes++ = *pDef; } *pRes++ = 0; @@ -372,15 +390,15 @@ static inline int Dau_DsdMergeGetStatus( char * pBeg, char * pStr, int * pMatche } void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * pMatches, int * pStatus, int fWrite ) { - assert( **p != '!' ); -/* +// assert( **p != '!' ); + if ( **p == '!' ) { if ( fWrite ) Dau_DsdMergeStoreAddToOutputChar( pS, **p ); (*p)++; } -*/ + while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') ) { if ( fWrite ) @@ -407,8 +425,8 @@ void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * p } if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor { - int StatusFan, Status = pStatus[*p - pStr]; - char New, * pBeg, * q = pStr + pMatches[ *p - pStr ]; + int New, StatusFan, Status = pStatus[*p - pStr]; + char * pBeg, * q = pStr + pMatches[ *p - pStr ]; assert( *q == **p + 1 + (**p != '(') ); if ( !fWrite ) { @@ -448,8 +466,8 @@ void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * p Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, StatusFan != 3 ); if ( StatusFan == 3 ) { - char New = Dau_DsdMergeStoreCreateDef( pS, pBeg, *p+1 ); - Dau_DsdMergeStoreAddToOutputChar( pS, New ); + int New = Dau_DsdMergeStoreCreateDef( pS, pBeg, *p+1 ); + Dau_DsdMergeStoreAddToOutputChar( pS, (char)('a' + New) ); } } Dau_DsdMergeStoreAddToOutputChar( pS, **p ); @@ -460,7 +478,7 @@ void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * p { // add more than one defs Dau_DsdMergeStoreAddToOutputChar( pS, **p ); - Dau_DsdMergeStoreStartDef( pS, **p ); + New = Dau_DsdMergeStoreStartDef( pS, **p ); for ( (*p)++; *p < q; (*p)++ ) { pBeg = *p; @@ -470,16 +488,16 @@ void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * p if ( StatusFan != 3 ) Dau_DsdMergeStoreAddToOutputChar( pS, '!' ); else - Dau_DsdMergeStoreAddToDefChar( pS, '!' ); + Dau_DsdMergeStoreAddToDefChar( pS, New, '!' ); (*p)++; pBeg++; } Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, StatusFan != 3 ); if ( StatusFan == 3 ) - Dau_DsdMergeStoreAddToDef( pS, pBeg, *p+1 ); + Dau_DsdMergeStoreAddToDef( pS, New, pBeg, *p+1 ); } - New = Dau_DsdMergeStoreStopDef( pS, *q ); - Dau_DsdMergeStoreAddToOutputChar( pS, New ); + Dau_DsdMergeStoreStopDef( pS, New, *q ); + Dau_DsdMergeStoreAddToOutputChar( pS, (char)('a' + New) ); Dau_DsdMergeStoreAddToOutputChar( pS, **p ); return; } @@ -490,11 +508,15 @@ void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * p } static inline void Dau_DsdMergeSubstitute( Dau_Sto_t * pS, char * pDsd, int * pMatches, int * pStatus ) { +/* + int fCompl = 0; if ( pDsd[0] == '!' ) { Dau_DsdMergeStoreAddToOutputChar( pS, '!' ); pDsd++; + fCompl = 1; } +*/ Dau_DsdMergeSubstitute_rec( pS, pDsd, &pDsd, pMatches, pStatus, 1 ); Dau_DsdMergeStoreAddToOutputChar( pS, 0 ); } @@ -552,11 +574,20 @@ void Dau_DsdRemoveBraces( char * pDsd, int * pMatches ) Dau_DsdRemoveBraces_rec( pDsd, &pDsd, pMatches ); for ( q = p; *p; p++ ) if ( *p != ' ' ) + { + if ( *p == '!' && *(q-1) == '!' && p != q ) + { + q--; + continue; + } *q++ = *p; + } *q = 0; } +clock_t s_TimeComp[3] = {0}; + /**Function************************************************************* Synopsis [Performs merging of two DSD formulas.] @@ -570,6 +601,9 @@ void Dau_DsdRemoveBraces( char * pDsd, int * pMatches ) ***********************************************************************/ char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1 ) { + int fVerbose = 0; + int fCheck = 1; + static int Counter = 0; static char pRes[DAU_MAX_STR]; char pDsd0[DAU_MAX_STR]; char pDsd1[DAU_MAX_STR]; @@ -583,40 +617,73 @@ char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, i int pMatches[DAU_MAX_STR]; int nVarsShared, nVarsTotal; Dau_Sto_t S, * pS = &S; - word Truth, t, t0, t1; + word Truth, t = 0, t0 = 0, t1 = 0; int Status; + clock_t clk = clock(); + Counter++; // create local copies Dau_DsdMergeCopy( pDsd0i, fCompl0, pDsd0 ); Dau_DsdMergeCopy( pDsd1i, fCompl1, pDsd1 ); +if ( fVerbose ) +printf( "\nAfter copying:\n" ); +if ( fVerbose ) +printf( "%s\n", pDsd0 ); +if ( fVerbose ) +printf( "%s\n", pDsd1 ); // handle constants - if ( pDsd0[1] == 0 || pDsd1[1] == 0 ) + if ( Dau_DsdIsConst(pDsd0) || Dau_DsdIsConst(pDsd1) ) { - if ( pDsd0[0] == '0' ) + if ( Dau_DsdIsConst0(pDsd0) ) strcpy( pRes, pDsd0 ); - else if ( pDsd0[0] == '1' ) + else if ( Dau_DsdIsConst1(pDsd0) ) strcpy( pRes, pDsd1 ); - else if ( pDsd1[0] == '0' ) + else if ( Dau_DsdIsConst0(pDsd1) ) strcpy( pRes, pDsd1 ); - else if ( pDsd1[0] == '1' ) + else if ( Dau_DsdIsConst1(pDsd1) ) strcpy( pRes, pDsd0 ); else assert( 0 ); return pRes; } + // compute matches Dau_DsdMergeMatches( pDsd0, pMatches0 ); Dau_DsdMergeMatches( pDsd1, pMatches1 ); // implement permutation Dau_DsdMergeReplace( pDsd0, pMatches0, pPerm0 ); Dau_DsdMergeReplace( pDsd1, pMatches1, pPerm1 ); +if ( fVerbose ) +printf( "After replacement:\n" ); +if ( fVerbose ) printf( "%s\n", pDsd0 ); +if ( fVerbose ) printf( "%s\n", pDsd1 ); - t0 = Dau_Dsd6ToTruth( pDsd0 ); - t1 = Dau_Dsd6ToTruth( pDsd1 ); + +//s_TimeComp[2] += clock() - clk; + + if ( fCheck ) + t0 = Dau_Dsd6ToTruth( pDsd0 ); + if ( fCheck ) + t1 = Dau_Dsd6ToTruth( pDsd1 ); + // find shared varaiables nVarsShared = Dau_DsdMergeFindShared(pDsd0, pDsd1, pMatches0, pMatches1, pVarPres); if ( nVarsShared == 0 ) { sprintf( pRes, "(%s%s)", pDsd0, pDsd1 ); +if ( fVerbose ) +printf( "Disjoint:\n" ); +if ( fVerbose ) +printf( "%s\n", pRes ); + + Dau_DsdMergeMatches( pRes, pMatches ); + Dau_DsdRemoveBraces( pRes, pMatches ); + Dau_DsdNormalize( pRes ); +if ( fVerbose ) +printf( "Normalized:\n" ); +if ( fVerbose ) +printf( "%s\n", pRes ); + + s_TimeComp[2] += clock() - clk; return pRes; } // create variable mapping @@ -627,7 +694,11 @@ printf( "%s\n", pDsd1 ); // find uniqueness status Dau_DsdMergeStatus( pDsd0, pMatches0, nVarsShared, pStatus0 ); Dau_DsdMergeStatus( pDsd1, pMatches1, nVarsShared, pStatus1 ); +if ( fVerbose ) +printf( "Individual status:\n" ); +if ( fVerbose ) Dau_DsdMergePrintWithStatus( pDsd0, pStatus0 ); +if ( fVerbose ) Dau_DsdMergePrintWithStatus( pDsd1, pStatus1 ); // prepare storage Dau_DsdMergeStoreClean( pS, nVarsShared ); @@ -635,13 +706,18 @@ Dau_DsdMergePrintWithStatus( pDsd1, pStatus1 ); Dau_DsdMergeStoreCleanOutput( pS ); Dau_DsdMergeSubstitute( pS, pDsd0, pMatches0, pStatus0 ); strcpy( pDsd0, pS->pOutput ); +if ( fVerbose ) +printf( "Substitutions:\n" ); +if ( fVerbose ) printf( "%s\n", pDsd0 ); // perform substitutions Dau_DsdMergeStoreCleanOutput( pS ); Dau_DsdMergeSubstitute( pS, pDsd1, pMatches1, pStatus1 ); strcpy( pDsd1, pS->pOutput ); +if ( fVerbose ) printf( "%s\n", pDsd1 ); +if ( fVerbose ) Dau_DsdMergeStorePrintDefs( pS ); // create new function @@ -649,24 +725,50 @@ Dau_DsdMergeStorePrintDefs( pS ); sprintf( pS->pOutput, "(%s%s)", pDsd0, pDsd1 ); Truth = Dau_Dsd6ToTruth( pS->pOutput ); Status = Dau_DsdDecompose( &Truth, nVarsTotal, 0, pS->pOutput ); +//printf( "%d ", Status ); if ( Status == -1 ) // did not find 1-step DSD return NULL; if ( Status > 6 ) // non-DSD part is too large return NULL; + if ( Dau_DsdIsConst(pS->pOutput) ) + { + strcpy( pRes, pS->pOutput ); + return pRes; + } +if ( fVerbose ) +printf( "Decomposition:\n" ); +if ( fVerbose ) printf( "%s\n", pS->pOutput ); // substitute definitions Dau_DsdMergeMatches( pS->pOutput, pMatches ); - Dau_DsdMergeInlineDefinitions( pS->pOutput, pMatches, pS->pVarDefs, pRes, nVarsShared ); + Dau_DsdMergeInlineDefinitions( pS->pOutput, pMatches, pS, pRes, nVarsShared ); +if ( fVerbose ) +printf( "Inlining:\n" ); +if ( fVerbose ) printf( "%s\n", pRes ); // perform variable replacement Dau_DsdMergeMatches( pRes, pMatches ); Dau_DsdMergeReplace( pRes, pMatches, pNew2Old ); Dau_DsdRemoveBraces( pRes, pMatches ); +if ( fVerbose ) +printf( "Replaced:\n" ); +if ( fVerbose ) printf( "%s\n", pRes ); Dau_DsdNormalize( pRes ); +if ( fVerbose ) +printf( "Normalized:\n" ); +if ( fVerbose ) printf( "%s\n", pRes ); - t = Dau_Dsd6ToTruth( pRes ); - assert( t == (t0 & t1) ); + + if ( fCheck ) + t = Dau_Dsd6ToTruth( pRes ); + if ( t != (t0 & t1) ) + printf( "Dau_DsdMerge(): Verification failed!\n" ); + + if ( Status == 0 ) + s_TimeComp[0] += clock() - clk; + else + s_TimeComp[1] += clock() - clk; return pRes; } @@ -696,11 +798,16 @@ void Dau_DsdTest() // char * pStr2 = "(df)"; // char * pStr1 = "(abf)"; // char * pStr2 = "(a[(bc)(fde)])"; - char * pStr1 = "8001{abc[ef]}"; - char * pStr2 = "(abe)"; +// char * pStr1 = "8001{abc[ef]}"; +// char * pStr2 = "(abe)"; + + char * pStr1 = "(!(ab)de)"; + char * pStr2 = "(!(ac)f)"; + char * pRes; word t = Dau_Dsd6ToTruth( pStr ); return; + // pStr2 = Dau_DsdDecompose( &t, 6, 0, NULL ); // Dau_DsdNormalize( pStr2 ); -- cgit v1.2.3