Skip to content

A
abc
Commit ee789ba9 by Alan Mishchenko
Options

Improved DSD.

parent e0f27f5a
Showing with 256 additions and 58 deletions
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;
......
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
......
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 )
{
......
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 ///
////////////////////////////////////////////////////////////////////////
......@@ -80,6 +82,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.]
Description [Mapping modes: delay (0), area flow (1), area (2).]
......@@ -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
......
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))
////////////////////////////////////////////////////////////////////////
......
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
......
src/opt/dau/dauMerge.c
......@@ -43,23 +43,40 @@ ABC_NAMESPACE_IMPL_START
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.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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 );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment