Skip to content

A
abc
Commit e0f27f5a by Alan Mishchenko
Options

Improved DSD.

parent fdcbb2cf
Showing with 1035 additions and 144 deletions
abclib.dsp
...@@ -1997,6 +1997,10 @@ SOURCE=.\src\opt\dau\dauEnum.c ...@@ -1997,6 +1997,10 @@ SOURCE=.\src\opt\dau\dauEnum.c
SOURCE=.\src\opt\dau\dauInt.h SOURCE=.\src\opt\dau\dauInt.h
# End Source File # End Source File
# Begin Source File
SOURCE=.\src\opt\dau\dauMerge.c
# End Source File
# End Group # End Group
# End Group # End Group
# Begin Group "map" # Begin Group "map"
......
src/base/abci/abcDec.c
...@@ -541,7 +541,7 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose ) ...@@ -541,7 +541,7 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
} }
else if ( DecType == 4 ) else if ( DecType == 4 )
{ {
extern void Dau_DsdTestOne( word t, int i ); // extern void Dau_DsdTestOne( word t, int i );
if ( p->nVars != 6 ) if ( p->nVars != 6 )
{ {
printf( "Currently only works for 6 variables.\n" ); printf( "Currently only works for 6 variables.\n" );
...@@ -554,7 +554,7 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose ) ...@@ -554,7 +554,7 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
{ {
if ( fVerbose ) if ( fVerbose )
printf( "%7d : ", i ); printf( "%7d : ", i );
Dau_DsdTestOne( *p->pFuncs[i], i ); // Dau_DsdTestOne( *p->pFuncs[i], i );
} }
} }
else assert( 0 ); else assert( 0 );
......
src/opt/dau/dau.h
...@@ -37,9 +37,11 @@ ...@@ -37,9 +37,11 @@
/// PARAMETERS /// /// PARAMETERS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START ABC_NAMESPACE_HEADER_START
#define DAU_MAX_VAR 16 // should be 6 or more
#define DAU_MAX_STR 256
#define DAU_MAX_WORD (1<<(DAU_MAX_VAR-6))
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// BASIC TYPES /// /// BASIC TYPES ///
...@@ -56,9 +58,14 @@ ABC_NAMESPACE_HEADER_START ...@@ -56,9 +58,14 @@ ABC_NAMESPACE_HEADER_START
/*=== dauCanon.c ==========================================================*/ /*=== dauCanon.c ==========================================================*/
extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm ); extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm );
/*=== dauDsd.c ==========================================================*/ /*=== dauDsd.c ==========================================================*/
extern char * Dau_DsdDecompose( word * pTruth, int nVarsInit, int * pnSizeNonDec ); extern int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, char * pRes );
extern word * Dau_DsdToTruth( char * p, int nVars ); extern word * Dau_DsdToTruth( char * p, int nVars );
extern word Dau_Dsd6ToTruth( char * p );
extern void Dau_DsdNormalize( char * p );
/*=== dauMerge.c ==========================================================*/
extern void Dau_DsdRemoveBraces( char * pDsd, int * pMatches );
extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1 );
ABC_NAMESPACE_HEADER_END ABC_NAMESPACE_HEADER_END
......
src/opt/dau/dauDsd.c
...@@ -28,10 +28,6 @@ ABC_NAMESPACE_IMPL_START ...@@ -28,10 +28,6 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
#define DAU_MAX_VAR 16 // should be 6 or more
#define DAU_MAX_STR 256
#define DAU_MAX_WORD (1<<(DAU_MAX_VAR-6))
/* /*
This code performs truth-table-based decomposition for 6-variable functions. This code performs truth-table-based decomposition for 6-variable functions.
Representation of operations: Representation of operations:
...@@ -73,70 +69,8 @@ int * Dau_DsdComputeMatches( char * p ) ...@@ -73,70 +69,8 @@ int * Dau_DsdComputeMatches( char * p )
assert( nNested < DAU_MAX_VAR ); assert( nNested < DAU_MAX_VAR );
} }
assert( nNested == 0 ); assert( nNested == 0 );
/*
// verify
for ( v = 0; p[v]; v++ )
if ( p[v] == '(' || p[v] == '[' || p[v] == '<' || p[v] == '{' )
assert( pMatches[v] > 0 );
else
assert( pMatches[v] == 0 );
*/
return pMatches; return pMatches;
} }
char * Dau_DsdFindMatch( char * p )
{
int Counter = 0;
assert( *p == '(' || *p == '[' || *p == '<' || *p == '{' );
while ( *p )
{
if ( *p == '(' || *p == '[' || *p == '<' || *p == '{' )
Counter++;
else if ( *p == ')' || *p == ']' || *p == '>' || *p == '}' )
Counter--;
if ( Counter == 0 )
return p;
p++;
}
return NULL;
}
static inline void Dau_DsdCleanBraces( char * p )
{
char * q, Last = -1;
int i;
for ( i = 0; p[i]; i++ )
{
if ( p[i] == '(' || p[i] == '[' || p[i] == '<' )
{
if ( p[i] != '<' && p[i] == Last && i > 0 && p[i-1] != '!' )
{
q = Dau_DsdFindMatch( p + i );
assert( (p[i] == '(') == (*q == ')') );
assert( (p[i] == '[') == (*q == ']') );
p[i] = *q = 'x';
}
else
Last = p[i];
}
else if ( p[i] == ')' || p[i] == ']' || p[i] == '>' )
Last = -1;
}
/*
if ( p[0] == '(' )
{
assert( p[i-1] == ')' );
p[0] = p[i-1] = 'x';
}
else if ( p[0] == '[' )
{
assert( p[i-1] == ']' );
p[0] = p[i-1] = 'x';
}
*/
for ( q = p; *p; p++ )
if ( *p != 'x' )
*q++ = *p;
*q = 0;
}
/**Function************************************************************* /**Function*************************************************************
...@@ -180,6 +114,130 @@ void Dau_DsdPermute( char * pDsd ) ...@@ -180,6 +114,130 @@ void Dau_DsdPermute( char * pDsd )
*pDsd = 'a' + pPerm[*pDsd - 'a']; *pDsd = 'a' + pPerm[*pDsd - 'a'];
} }
/**Function*************************************************************
Synopsis [Normalize the ordering of components.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Dau_DsdNormalizeCopy( char * pDest, char * pSour, int * pMarks, int i )
{
int s;
for ( s = pMarks[i]; s < pMarks[i+1]; s++ )
*pDest++ = pSour[s];
return pDest;
}
int Dau_DsdNormalizeCompare( char * pStr, int * pMarks, int i, int j )
{
char * pStr1 = pStr + pMarks[i];
char * pStr2 = pStr + pMarks[j];
char * pLimit1 = pStr + pMarks[i+1];
char * pLimit2 = pStr + pMarks[j+1];
for ( ; pStr1 < pLimit1 && pStr2 < pLimit2; pStr1++, pStr2++ )
{
if ( !(*pStr1 >= 'a' && *pStr1 <= 'z') )
{
pStr2--;
continue;
}
if ( !(*pStr2 >= 'a' && *pStr2 <= 'z') )
{
pStr1--;
continue;
}
if ( *pStr1 < *pStr2 )
return -1;
if ( *pStr1 > *pStr2 )
return 1;
}
assert( pStr1 < pLimit1 || pStr2 < pLimit2 );
if ( pStr1 == pLimit1 )
return -1;
if ( pStr2 == pLimit2 )
return 1;
assert( 0 );
return 0;
}
int * Dau_DsdNormalizePerm( char * pStr, int * pMarks, int nMarks )
{
static int pPerm[DAU_MAX_VAR];
int i, k;
for ( i = 0; i < nMarks; i++ )
pPerm[i] = i;
for ( i = 0; i < nMarks; i++ )
{
int iBest = i;
for ( k = i + 1; k < nMarks; k++ )
if ( Dau_DsdNormalizeCompare( pStr, pMarks, pPerm[iBest], pPerm[k] ) == 1 )
iBest = k;
ABC_SWAP( int, pPerm[i], pPerm[iBest] );
}
return pPerm;
}
void Dau_DsdNormalize_rec( char * pStr, char ** p, int * pMatches )
{
static char pBuffer[DAU_MAX_STR];
if ( **p == '!' )
(*p)++;
if ( **p >= 'a' && **p <= 'f' ) // var
return;
if ( **p == '(' || **p == '[' ) // and/or/xor
{
char * pStore, * pOld = *p + 1;
char * q = pStr + pMatches[ *p - pStr ];
int i, * pPerm, nMarks = 0, pMarks[DAU_MAX_VAR+1];
assert( *q == **p + 1 + (**p != '(') );
for ( (*p)++; *p < q; (*p)++ )
{
pMarks[nMarks++] = *p - pStr;
Dau_DsdNormalize_rec( pStr, p, pMatches );
}
pMarks[nMarks] = *p - pStr;
assert( *p == q );
// add to buffer in good order
pPerm = Dau_DsdNormalizePerm( pStr, pMarks, nMarks );
// copy to the buffer
pStore = pBuffer;
for ( i = 0; i < nMarks; i++ )
pStore = Dau_DsdNormalizeCopy( pStore, pStr, pMarks, pPerm[i] );
assert( pStore - pBuffer == *p - pOld );
memcpy( pOld, pBuffer, pStore - pBuffer );
return;
}
if ( **p == '<' || **p == '{' ) // mux
{
char * q = pStr + pMatches[ *p - pStr ];
assert( *q == **p + 1 + (**p != '(') );
if ( (**p == '<') && (*(q+1) == '{') )
{
*p = q+1;
Dau_DsdNormalize_rec( pStr, p, pMatches );
return;
}
for ( (*p)++; *p < q; (*p)++ )
Dau_DsdNormalize_rec( pStr, p, pMatches );
assert( *p == q );
return;
}
if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
{
(*p)++;
return;
}
assert( 0 );
}
void Dau_DsdNormalize( char * pDsd )
{
if ( pDsd[1] != 0 )
Dau_DsdNormalize_rec( pDsd, &pDsd, Dau_DsdComputeMatches(pDsd) );
}
/**Function************************************************************* /**Function*************************************************************
...@@ -211,7 +269,7 @@ word Dau_Dsd6TruthCompose_rec( word Func, word * pFanins, int nVars ) ...@@ -211,7 +269,7 @@ word Dau_Dsd6TruthCompose_rec( word Func, word * pFanins, int nVars )
t1 = Dau_Dsd6TruthCompose_rec( Abc_Tt6Cofactor1(Func, nVars), pFanins, nVars ); t1 = Dau_Dsd6TruthCompose_rec( Abc_Tt6Cofactor1(Func, nVars), pFanins, nVars );
return (~pFanins[nVars] & t0) | (pFanins[nVars] & t1); return (~pFanins[nVars] & t0) | (pFanins[nVars] & t1);
} }
word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches ) word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches, word * pTruths )
{ {
int fCompl = 0; int fCompl = 0;
if ( **p == '!' ) if ( **p == '!' )
...@@ -219,7 +277,7 @@ word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches ) ...@@ -219,7 +277,7 @@ word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches )
if ( **p >= 'a' && **p <= 'f' ) // var if ( **p >= 'a' && **p <= 'f' ) // var
{ {
assert( **p - 'a' >= 0 && **p - 'a' < 6 ); assert( **p - 'a' >= 0 && **p - 'a' < 6 );
return fCompl ? ~s_Truths6[**p - 'a'] : s_Truths6[**p - 'a']; return fCompl ? ~pTruths[**p - 'a'] : pTruths[**p - 'a'];
} }
if ( **p == '(' ) // and/or if ( **p == '(' ) // and/or
{ {
...@@ -227,7 +285,7 @@ word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches ) ...@@ -227,7 +285,7 @@ word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches )
word Res = ~(word)0; word Res = ~(word)0;
assert( **p == '(' && *q == ')' ); assert( **p == '(' && *q == ')' );
for ( (*p)++; *p < q; (*p)++ ) for ( (*p)++; *p < q; (*p)++ )
Res &= Dau_Dsd6ToTruth_rec( pStr, p, pMatches ); Res &= Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths );
assert( *p == q ); assert( *p == q );
return fCompl ? ~Res : Res; return fCompl ? ~Res : Res;
} }
...@@ -237,19 +295,51 @@ word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches ) ...@@ -237,19 +295,51 @@ word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches )
word Res = 0; word Res = 0;
assert( **p == '[' && *q == ']' ); assert( **p == '[' && *q == ']' );
for ( (*p)++; *p < q; (*p)++ ) for ( (*p)++; *p < q; (*p)++ )
Res ^= Dau_Dsd6ToTruth_rec( pStr, p, pMatches ); Res ^= Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths );
assert( *p == q ); assert( *p == q );
return fCompl ? ~Res : Res; return fCompl ? ~Res : Res;
} }
if ( **p == '<' ) // mux if ( **p == '<' ) // mux
{ {
char * q = pStr + pMatches[ *p - pStr ]; int nVars = 0;
word Temp[3], * pTemp = Temp, Res; word Temp[3], * pTemp = Temp, Res;
word Fanins[6], * pTruths2;
char * pOld = *p;
char * q = pStr + pMatches[ *p - pStr ];
// read fanins
if ( *(q+1) == '{' )
{
char * q2;
*p = q+1;
q2 = pStr + pMatches[ *p - pStr ];
assert( **p == '{' && *q2 == '}' );
for ( nVars = 0, (*p)++; *p < q2; (*p)++, nVars++ )
Fanins[nVars] = Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths );
assert( *p == q2 );
pTruths2 = Fanins;
}
else
pTruths2 = pTruths;
// read MUX
*p = pOld;
q = pStr + pMatches[ *p - pStr ];
assert( **p == '<' && *q == '>' ); assert( **p == '<' && *q == '>' );
// verify internal variables
if ( nVars )
for ( ; pOld < q; pOld++ )
if ( *pOld >= 'a' && *pOld <= 'z' )
assert( *pOld - 'a' < nVars );
// derive MAX components
for ( (*p)++; *p < q; (*p)++ ) for ( (*p)++; *p < q; (*p)++ )
*pTemp++ = Dau_Dsd6ToTruth_rec( pStr, p, pMatches ); *pTemp++ = Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths2 );
assert( pTemp == Temp + 3 ); assert( pTemp == Temp + 3 );
assert( *p == q ); assert( *p == q );
if ( *(q+1) == '{' ) // and/or
{
char * q = pStr + pMatches[ ++(*p) - pStr ];
assert( **p == '{' && *q == '}' );
*p = q;
}
Res = (Temp[0] & Temp[1]) | (~Temp[0] & Temp[2]); Res = (Temp[0] & Temp[1]) | (~Temp[0] & Temp[2]);
return fCompl ? ~Res : Res; return fCompl ? ~Res : Res;
} }
...@@ -262,7 +352,7 @@ word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches ) ...@@ -262,7 +352,7 @@ word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches )
q = pStr + pMatches[ *p - pStr ]; q = pStr + pMatches[ *p - pStr ];
assert( **p == '{' && *q == '}' ); assert( **p == '{' && *q == '}' );
for ( i = 0, (*p)++; *p < q; (*p)++, i++ ) for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
Fanins[i] = Dau_Dsd6ToTruth_rec( pStr, p, pMatches ); Fanins[i] = Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths );
assert( i == nVars ); assert( i == nVars );
assert( *p == q ); assert( *p == q );
Res = Dau_Dsd6TruthCompose_rec( Func, Fanins, nVars ); Res = Dau_Dsd6TruthCompose_rec( Func, Fanins, nVars );
...@@ -279,7 +369,7 @@ word Dau_Dsd6ToTruth( char * p ) ...@@ -279,7 +369,7 @@ word Dau_Dsd6ToTruth( char * p )
else if ( *p == '1' && *(p+1) == 0 ) else if ( *p == '1' && *(p+1) == 0 )
Res = ~(word)0; Res = ~(word)0;
else else
Res = Dau_Dsd6ToTruth_rec( p, &p, Dau_DsdComputeMatches(p) ); Res = Dau_Dsd6ToTruth_rec( p, &p, Dau_DsdComputeMatches(p), s_Truths6 );
assert( *++p == 0 ); assert( *++p == 0 );
return Res; return Res;
} }
...@@ -495,7 +585,7 @@ void Dau_DsdTest2() ...@@ -495,7 +585,7 @@ void Dau_DsdTest2()
***********************************************************************/ ***********************************************************************/
static inline int Dau_DsdPerformReplace( char * pBuffer, int PosStart, int Pos, int Symb, char * pNext ) static inline int Dau_DsdPerformReplace( char * pBuffer, int PosStart, int Pos, int Symb, char * pNext )
{ {
static char pTemp[DAU_MAX_STR+20]; static char pTemp[DAU_MAX_STR];
char * pCur = pTemp; char * pCur = pTemp;
int i, k, RetValue; int i, k, RetValue;
for ( i = PosStart; i < Pos; i++ ) for ( i = PosStart; i < Pos; i++ )
...@@ -666,7 +756,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars ...@@ -666,7 +756,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
} }
char * Dau_DsdPerform( word t ) char * Dau_DsdPerform( word t )
{ {
static char pBuffer[DAU_MAX_STR+20]; static char pBuffer[DAU_MAX_STR];
int pVarsNew[6] = {0, 1, 2, 3, 4, 5}; int pVarsNew[6] = {0, 1, 2, 3, 4, 5};
int Pos = 0; int Pos = 0;
if ( t == 0 ) if ( t == 0 )
...@@ -678,7 +768,7 @@ char * Dau_DsdPerform( word t ) ...@@ -678,7 +768,7 @@ char * Dau_DsdPerform( word t )
pBuffer[Pos++] = 0; pBuffer[Pos++] = 0;
// printf( "%d ", strlen(pBuffer) ); // printf( "%d ", strlen(pBuffer) );
// printf( "%s ->", pBuffer ); // printf( "%s ->", pBuffer );
Dau_DsdCleanBraces( pBuffer ); Dau_DsdRemoveBraces( pBuffer, Dau_DsdComputeMatches(pBuffer) );
// printf( " %s\n", pBuffer ); // printf( " %s\n", pBuffer );
return pBuffer; return pBuffer;
} }
...@@ -713,34 +803,55 @@ void Dau_DsdTest3() ...@@ -713,34 +803,55 @@ void Dau_DsdTest3()
if ( t != t2 ) if ( t != t2 )
printf( "Verification failed.\n" ); printf( "Verification failed.\n" );
} }
void Dau_DsdTestOne( word t, int i )
{
int nSizeNonDec;
word t2;
// char * p = Dau_DsdPerform( t );
char * p = Dau_DsdDecompose( &t, 6, &nSizeNonDec );
return;
t2 = Dau_Dsd6ToTruth( p );
if ( t != t2 )
{
printf( "Verification failed. " );
printf( "%8d : ", i );
printf( "%30s ", p );
// Kit_DsdPrintFromTruth( (unsigned *)&t, 6 );
// printf( " " );
// Kit_DsdPrintFromTruth( (unsigned *)&t2, 6 );
printf( "\n" );
}
}
/*
extern void Dau_DsdTestOne( word t, int i );
assert( p->nVars == 6 );
Dau_DsdTestOne( *p->pFuncs[i], i );
*/
/**Function*************************************************************
Synopsis [Find the best cofactoring variable.]
Description [Return -2 if non-DSD; -1 if full DSD; otherwise,
returns cofactoring variables i (i >= 0).]
SideEffects []
SeeAlso []
***********************************************************************/
int Dau_DsdCheck1Step( word * pTruth, int nVarsInit )
{
word pCofTemp[DAU_MAX_WORD];
int nWords = Abc_TtWordNum(nVarsInit);
int nSizeNonDec, nSizeNonDec0, nSizeNonDec1;
int v, vBest = -2, nSumCofsBest = ABC_INFINITY, nSumCofs;
nSizeNonDec = Dau_DsdDecompose( pTruth, nVarsInit, 0, NULL );
if ( nSizeNonDec == 0 )
return -1;
assert( nSizeNonDec > 0 );
for ( v = 0; v < nVarsInit; v++ )
{
// try first cofactor
Abc_TtCopy( pCofTemp, pTruth, nWords, 0 );
Abc_TtCofactor0( pCofTemp, nWords, v );
nSumCofs = Abc_TtSupportSize( pCofTemp, nVarsInit );
nSizeNonDec0 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, NULL );
// try second cofactor
Abc_TtCopy( pCofTemp, pTruth, nWords, 0 );
Abc_TtCofactor1( pCofTemp, nWords, v );
nSumCofs += Abc_TtSupportSize( pCofTemp, nVarsInit );
nSizeNonDec1 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, NULL );
// compare cofactors
if ( nSizeNonDec0 || nSizeNonDec1 )
continue;
if ( nSumCofsBest > nSumCofs )
{
vBest = v;
nSumCofsBest = nSumCofs;
}
}
return vBest;
}
/**Function************************************************************* /**Function*************************************************************
...@@ -762,6 +873,7 @@ struct Dau_Dsd_t_ ...@@ -762,6 +873,7 @@ struct Dau_Dsd_t_
int nSizeNonDec; // size of the largest non-decomposable block int nSizeNonDec; // size of the largest non-decomposable block
int nConsts; // the number of constant decompositions int nConsts; // the number of constant decompositions
int uConstMask; // constant decomposition mask int uConstMask; // constant decomposition mask
int fSplitPrime; // represent prime function as 1-step DSD
char pVarDefs[32][8]; // variable definitions char pVarDefs[32][8]; // variable definitions
char Cache[32][32]; // variable cache char Cache[32][32]; // variable cache
char pOutput[DAU_MAX_STR]; // output stream char pOutput[DAU_MAX_STR]; // output stream
...@@ -821,16 +933,49 @@ static inline void Dau_DsdTranslate( Dau_Dsd_t * p, int * pVars, int nVars, char ...@@ -821,16 +933,49 @@ static inline void Dau_DsdTranslate( Dau_Dsd_t * p, int * pVars, int nVars, char
else else
p->pOutput[ p->nPos++ ] = *pStr; p->pOutput[ p->nPos++ ] = *pStr;
} }
static inline void Dau_DsdWritePrime( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) static inline int Dau_DsdWritePrime( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
{ {
int v; int v, RetValue = 2;
assert( nVars > 2 ); assert( nVars > 2 );
if ( p->fSplitPrime )
{
word pCofTemp[DAU_MAX_WORD];
int nWords = Abc_TtWordNum(nVars);
int vBest = Dau_DsdCheck1Step( pTruth, nVars );
assert( vBest != -1 );
if ( vBest == -2 ) // non-dec
p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, pTruth, nVars );
else
{
char pRes[DAU_MAX_STR];
int nNonDecSize;
// compose the result
Dau_DsdWriteString( p, "<" );
Dau_DsdWriteVar( p, pVars[vBest], 0 );
// split decomposition
Abc_TtCopy( pCofTemp, pTruth, nWords, 0 );
Abc_TtCofactor1( pCofTemp, nWords, vBest );
nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, pRes );
assert( nNonDecSize == 0 );
Dau_DsdWriteString( p, pRes );
// split decomposition
Abc_TtCopy( pCofTemp, pTruth, nWords, 0 );
Abc_TtCofactor0( pCofTemp, nWords, vBest );
nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, pRes );
assert( nNonDecSize == 0 );
Dau_DsdWriteString( p, pRes );
Dau_DsdWriteString( p, ">" );
RetValue = 1;
}
}
else
p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, pTruth, nVars ); p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, pTruth, nVars );
Dau_DsdWriteString( p, "{" ); Dau_DsdWriteString( p, "{" );
for ( v = 0; v < nVars; v++ ) for ( v = 0; v < nVars; v++ )
Dau_DsdWriteVar( p, pVars[v], 0 ); Dau_DsdWriteVar( p, pVars[v], 0 );
Dau_DsdWriteString( p, "}" ); Dau_DsdWriteString( p, "}" );
p->nSizeNonDec = nVars; p->nSizeNonDec = nVars;
return RetValue;
} }
static inline void Dau_DsdFinalize( Dau_Dsd_t * p ) static inline void Dau_DsdFinalize( Dau_Dsd_t * p )
{ {
...@@ -1012,6 +1157,8 @@ static inline int Dau_Dsd6DecomposeDoubleVarsOne( Dau_Dsd_t * p, word * pTruth, ...@@ -1012,6 +1157,8 @@ static inline int Dau_Dsd6DecomposeDoubleVarsOne( Dau_Dsd_t * p, word * pTruth,
word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v ); word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v );
int Status = Dau_Dsd6FindSupportOne( p, tCof0, tCof1, pVars, nVars, v, u ); int Status = Dau_Dsd6FindSupportOne( p, tCof0, tCof1, pVars, nVars, v, u );
assert( v > u ); assert( v > u );
//printf( "Checking %s and %s.\n", p->pVarDefs[pVars[v]], p->pVarDefs[pVars[u]] );
// Kit_DsdPrintFromTruth( (unsigned *)pTruth, 6 );printf( "\n" ); // Kit_DsdPrintFromTruth( (unsigned *)pTruth, 6 );printf( "\n" );
if ( Status == 3 ) if ( Status == 3 )
{ {
...@@ -1101,9 +1248,10 @@ int Dau_Dsd6DecomposeDoubleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int ...@@ -1101,9 +1248,10 @@ int Dau_Dsd6DecomposeDoubleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int
// look for MUX-decomposable variable on top or at the bottom // look for MUX-decomposable variable on top or at the bottom
static inline int Dau_Dsd6DecomposeTripleVarsOuter( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v ) static inline int Dau_Dsd6DecomposeTripleVarsOuter( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
{ {
extern void Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit ); extern int Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit );
Dau_Dsd_t P1, * p1 = &P1; Dau_Dsd_t P1, * p1 = &P1;
word tCof0, tCof1; word tCof0, tCof1;
p1->fSplitPrime = 0;
// move this variable to the top // move this variable to the top
ABC_SWAP( int, pVars[v], pVars[nVars-1] ); ABC_SWAP( int, pVars[v], pVars[nVars-1] );
Abc_TtSwapVars( pTruth, 6, v, nVars-1 ); Abc_TtSwapVars( pTruth, 6, v, nVars-1 );
...@@ -1204,22 +1352,22 @@ int Dau_Dsd6DecomposeTripleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int ...@@ -1204,22 +1352,22 @@ int Dau_Dsd6DecomposeTripleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int
assert( 0 ); assert( 0 );
return -1; return -1;
} }
void Dau_Dsd6DecomposeInternal( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) int Dau_Dsd6DecomposeInternal( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
{ {
// decompose single variales on the output side // decompose single variales on the output side
nVars = Dau_Dsd6DecomposeSingleVar( p, pTruth, pVars, nVars ); nVars = Dau_Dsd6DecomposeSingleVar( p, pTruth, pVars, nVars );
if ( nVars == 0 ) if ( nVars == 0 )
return; return 0;
// decompose double variables on the input side // decompose double variables on the input side
nVars = Dau_Dsd6DecomposeDoubleVars( p, pTruth, pVars, nVars ); nVars = Dau_Dsd6DecomposeDoubleVars( p, pTruth, pVars, nVars );
if ( nVars == 0 ) if ( nVars == 0 )
return; return 0;
// decompose MUX on the output/input side // decompose MUX on the output/input side
nVars = Dau_Dsd6DecomposeTripleVars( p, pTruth, pVars, nVars ); nVars = Dau_Dsd6DecomposeTripleVars( p, pTruth, pVars, nVars );
if ( nVars == 0 ) if ( nVars == 0 )
return; return 0;
// write non-decomposable function // write non-decomposable function
Dau_DsdWritePrime( p, pTruth, pVars, nVars ); return Dau_DsdWritePrime( p, pTruth, pVars, nVars );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -1245,22 +1393,22 @@ int Dau_DsdDecomposeTripleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int ...@@ -1245,22 +1393,22 @@ int Dau_DsdDecomposeTripleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int
{ {
return 0; return 0;
} }
void Dau_DsdDecomposeInternal( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) int Dau_DsdDecomposeInternal( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
{ {
// decompose single variales on the output side // decompose single variales on the output side
nVars = Dau_DsdDecomposeSingleVar( p, pTruth, pVars, nVars ); nVars = Dau_DsdDecomposeSingleVar( p, pTruth, pVars, nVars );
if ( nVars == 0 ) if ( nVars == 0 )
return; return 0;
// decompose double variables on the input side // decompose double variables on the input side
nVars = Dau_DsdDecomposeDoubleVars( p, pTruth, pVars, nVars ); nVars = Dau_DsdDecomposeDoubleVars( p, pTruth, pVars, nVars );
if ( nVars == 0 ) if ( nVars == 0 )
return; return 0;
// decompose MUX on the output/input side // decompose MUX on the output/input side
nVars = Dau_DsdDecomposeTripleVars( p, pTruth, pVars, nVars ); nVars = Dau_DsdDecomposeTripleVars( p, pTruth, pVars, nVars );
if ( nVars == 0 ) if ( nVars == 0 )
return; return 0;
// write non-decomposable function // write non-decomposable function
Dau_DsdWritePrime( p, pTruth, pVars, nVars ); return Dau_DsdWritePrime( p, pTruth, pVars, nVars );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -1288,50 +1436,59 @@ int Dau_DsdMinBase( word * pTruth, int nVars, int * pVarsNew ) ...@@ -1288,50 +1436,59 @@ int Dau_DsdMinBase( word * pTruth, int nVars, int * pVarsNew )
} }
return nVars; return nVars;
} }
void Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit ) int Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit )
{ {
int nVars, pVars[16]; int Status = 0, nVars, pVars[16];
Dau_DsdInitialize( p, nVarsInit ); Dau_DsdInitialize( p, nVarsInit );
nVars = Dau_DsdMinBase( pTruth, nVarsInit, pVars ); nVars = Dau_DsdMinBase( pTruth, nVarsInit, pVars );
assert( nVars > 0 && nVars <= 6 ); assert( nVars > 0 && nVars <= 6 );
if ( nVars == 1 ) if ( nVars == 1 )
Dau_DsdWriteVar( p, pVars[0], (int)(pTruth[0] & 1) ); Dau_DsdWriteVar( p, pVars[0], (int)(pTruth[0] & 1) );
else if ( nVars <= 6 ) else if ( nVars <= 6 )
Dau_Dsd6DecomposeInternal( p, pTruth, pVars, nVars ); Status = Dau_Dsd6DecomposeInternal( p, pTruth, pVars, nVars );
else else
Dau_DsdDecomposeInternal( p, pTruth, pVars, nVars ); Status = Dau_DsdDecomposeInternal( p, pTruth, pVars, nVars );
Dau_DsdFinalize( p ); Dau_DsdFinalize( p );
return Status;
} }
char * Dau_DsdDecompose( word * pTruth, int nVarsInit, int * pnSizeNonDec ) int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, char * pRes )
{ {
static Dau_Dsd_t P; Dau_Dsd_t P, * p = &P;
Dau_Dsd_t * p = &P; p->fSplitPrime = fSplitPrime;
p->nSizeNonDec = 0; p->nSizeNonDec = 0;
if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) ) if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) )
p->pOutput[0] = '0', p->pOutput[1] = 0; pRes[0] = '0', pRes[1] = 0;
else if ( (pTruth[0] & 1) && Abc_TtIsConst1(pTruth, Abc_TtWordNum(nVarsInit)) ) else if ( (pTruth[0] & 1) && Abc_TtIsConst1(pTruth, Abc_TtWordNum(nVarsInit)) )
p->pOutput[0] = '1', p->pOutput[1] = 0; pRes[0] = '1', pRes[1] = 0;
else else
{ {
Dau_DsdDecomposeInt( p, pTruth, nVarsInit ); int Status = Dau_DsdDecomposeInt( p, pTruth, nVarsInit );
Dau_DsdCleanBraces( p->pOutput ); Dau_DsdRemoveBraces( p->pOutput, Dau_DsdComputeMatches(p->pOutput) );
if ( pRes )
strcpy( pRes, p->pOutput );
assert( fSplitPrime || Status != 1 );
if ( fSplitPrime && Status == 2 )
return -1;
} }
if ( pnSizeNonDec ) return p->nSizeNonDec;
*pnSizeNonDec = p->nSizeNonDec;
return p->pOutput;
} }
void Dau_DsdTest()
void Dau_DsdTest44()
{ {
char pRes[DAU_MAX_STR];
// char * pStr = "(!(!a<bcd>)!(!fe))"; // char * pStr = "(!(!a<bcd>)!(!fe))";
// char * pStr = "([acb]<!edf>)"; // char * pStr = "([acb]<!edf>)";
// char * pStr = "!(f!(b!c!(d[ea])))"; // char * pStr = "!(f!(b!c!(d[ea])))";
// char * pStr = "[!(a[be])!(c!df)]"; // char * pStr = "[!(a[be])!(c!df)]";
// char * pStr = "<(a<bcd>)ef>"; // char * pStr = "<(e<bca>)fd>";
char * pStr = "[d8001{a(!bc)ef}]"; // char * pStr = "[d8001{abef}c]";
char * pStr2; char * pStr = "[dc<a(cbd)(!c!b!d)>{abef}]";
// char * pStr3;
word t = Dau_Dsd6ToTruth( pStr ); word t = Dau_Dsd6ToTruth( pStr );
return; // return;
pStr2 = Dau_DsdDecompose( &t, 6, NULL ); int nNonDec = Dau_DsdDecompose( &t, 6, 1, pRes );
// Dau_DsdNormalize( pStr2 );
// Dau_DsdExtract( pStr, 2, 0 );
t = 0; t = 0;
} }
...@@ -1341,13 +1498,13 @@ void Dau_DsdTest33() ...@@ -1341,13 +1498,13 @@ void Dau_DsdTest33()
FILE * pFile = fopen( pFileName, "rb" ); FILE * pFile = fopen( pFileName, "rb" );
word t, t1, t2; word t, t1, t2;
char pBuffer[100]; char pBuffer[100];
char * pStr2; char pRes[DAU_MAX_STR];
int nSizeNonDec; int nSizeNonDec;
int i, Counter = 0; int i, Counter = 0;
clock_t clk = clock(); clock_t clk = clock();
while ( fgets( pBuffer, 100, pFile ) != NULL ) while ( fgets( pBuffer, 100, pFile ) != NULL )
{ {
pStr2 = pBuffer + strlen(pBuffer)-1; char * pStr2 = pBuffer + strlen(pBuffer)-1;
if ( *pStr2 == '\n' ) if ( *pStr2 == '\n' )
*pStr2-- = 0; *pStr2-- = 0;
if ( *pStr2 == '\r' ) if ( *pStr2 == '\r' )
...@@ -1359,12 +1516,12 @@ void Dau_DsdTest33() ...@@ -1359,12 +1516,12 @@ void Dau_DsdTest33()
for ( i = 0; i < 1000; i++ ) for ( i = 0; i < 1000; i++ )
{ {
Dau_DsdPermute( pBuffer ); Dau_DsdPermute( pBuffer );
t = t1 = Dau_Dsd6ToTruth( pBuffer[0] == '*' ? pBuffer + 1 : pBuffer ); t = t1 = Dau_Dsd6ToTruth( pBuffer[0] == '*' ? pBuffer + 1 : pBuffer );
pStr2 = Dau_DsdDecompose( &t, 6, &nSizeNonDec ); nSizeNonDec = Dau_DsdDecompose( &t, 6, 0, pRes );
Dau_DsdNormalize( pRes );
// pStr2 = Dau_DsdPerform( t ); nSizeNonDec = 0; // pStr2 = Dau_DsdPerform( t ); nSizeNonDec = 0;
assert( nSizeNonDec == 0 ); assert( nSizeNonDec == 0 );
t2 = Dau_Dsd6ToTruth( pStr2 ); t2 = Dau_Dsd6ToTruth( pRes );
if ( t1 != t2 ) if ( t1 != t2 )
{ {
// Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ); // Kit_DsdPrintFromTruth( (unsigned *)&t, 6 );
......
src/opt/dau/dauMerge.c 0 → 100644
/**CFile****************************************************************
FileName [dauMerge.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware unmapping.]
Synopsis [Enumeration of decompositions.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: dauMerge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "dau.h"
#include "dauInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**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)
};
static inline void Dau_DsdMergeStoreClean( Dau_Sto_t * pS, int nShared )
{
pS->iVarUsed = nShared;
pS->pPosStore = pS->pStore;
memset( pS->pVarDefs, 0, sizeof(char *) * DAU_MAX_VAR );
}
static inline void Dau_DsdMergeStoreCleanOutput( Dau_Sto_t * pS )
{
pS->pPosOutput = pS->pOutput;
}
static inline void Dau_DsdMergeStoreAddToOutput( Dau_Sto_t * pS, char * pBeg, char * pEnd )
{
while ( pBeg < pEnd )
*pS->pPosOutput++ = *pBeg++;
}
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 )
{
pS->pVarDefs[pS->iVarUsed] = pS->pPosStore;
if (c) *pS->pPosStore++ = c;
}
static inline void Dau_DsdMergeStoreAddToDef( Dau_Sto_t * pS, char * pBeg, char * pEnd )
{
while ( pBeg < pEnd )
*pS->pPosStore++ = *pBeg++;
}
static inline void Dau_DsdMergeStoreAddToDefChar( Dau_Sto_t * pS, char c )
{
*pS->pPosStore++ = c;
}
static inline char Dau_DsdMergeStoreStopDef( Dau_Sto_t * pS, char c )
{
if (c) *pS->pPosStore++ = c;
*pS->pPosStore++ = 0;
return 'a' + pS->iVarUsed++;
}
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 );
}
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] );
}
/**Function*************************************************************
Synopsis [Creates local copy.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Dau_DsdMergeCopy( char * pDsd, int fCompl, char * pRes )
{
if ( fCompl && pDsd[0] == '!' )
fCompl = 0, pDsd++;
if ( pDsd[1] == 0 ) // constant
pRes[0] = (fCompl ? (char)((int)pDsd[0] ^ 1) : pDsd[0]), pRes[1] = 0;
else
sprintf( pRes, "%s%s", fCompl ? "!" : "", pDsd );
}
/**Function*************************************************************
Synopsis [Replaces variables according to the mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Dau_DsdMergeReplace( char * pDsd, int * pMatches, int * pMap )
{
int i;
for ( i = 0; pDsd[i]; i++ )
{
// skip non-DSD block
if ( pDsd[i] == '<' && pDsd[pMatches[i]+1] == '{' )
i = pMatches[i] + 1;
if ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
while ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
i++;
// detect variables
if ( pDsd[i] >= 'a' && pDsd[i] <= 'z' )
pDsd[i] = 'a' + pMap[ pDsd[i] - 'a' ];
}
}
static inline void Dau_DsdMergeMatches( char * pDsd, int * pMatches )
{
int pNested[DAU_MAX_VAR];
int i, nNested = 0;
for ( i = 0; pDsd[i]; i++ )
{
pMatches[i] = 0;
if ( pDsd[i] == '(' || pDsd[i] == '[' || pDsd[i] == '<' || pDsd[i] == '{' )
pNested[nNested++] = i;
else if ( pDsd[i] == ')' || pDsd[i] == ']' || pDsd[i] == '>' || pDsd[i] == '}' )
pMatches[pNested[--nNested]] = i;
assert( nNested < DAU_MAX_VAR );
}
assert( nNested == 0 );
}
static inline void Dau_DsdMergeVarPres( char * pDsd, int * pMatches, int * pPres, int Mask )
{
int i;
for ( i = 0; pDsd[i]; i++ )
{
// skip non-DSD block
if ( pDsd[i] == '<' && pDsd[pMatches[i]+1] == '{' )
i = pMatches[i] + 1;
if ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
while ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
i++;
// skip non-variables
if ( !(pDsd[i] >= 'a' && pDsd[i] <= 'z') )
continue;
// record the mask
assert( pDsd[i]-'a' < DAU_MAX_VAR );
pPres[pDsd[i]-'a'] |= Mask;
}
}
static inline int Dau_DsdMergeCountShared( int * pPres, int Mask )
{
int i, Counter = 0;
for ( i = 0; i < DAU_MAX_VAR; i++ )
Counter += (pPres[i] == Mask);
return Counter;
}
static inline int Dau_DsdMergeFindShared( char * pDsd0, char * pDsd1, int * pMatches0, int * pMatches1, int * pVarPres )
{
memset( pVarPres, 0, sizeof(int)*DAU_MAX_VAR );
Dau_DsdMergeVarPres( pDsd0, pMatches0, pVarPres, 1 );
Dau_DsdMergeVarPres( pDsd1, pMatches1, pVarPres, 2 );
return Dau_DsdMergeCountShared( pVarPres, 3 );
}
static inline int Dau_DsdMergeCreateMaps( int * pVarPres, int nShared, int * pOld2New, int * pNew2Old )
{
int i, Counter = 0, Counter2 = nShared;
for ( i = 0; i < DAU_MAX_VAR; i++ )
{
if ( pVarPres[i] == 0 )
continue;
if ( pVarPres[i] == 3 )
{
pOld2New[i] = Counter;
pNew2Old[Counter] = i;
Counter++;
continue;
}
assert( pVarPres[i] == 1 || pVarPres[i] == 2 );
pOld2New[i] = Counter2;
pNew2Old[Counter2] = i;
Counter2++;
}
return Counter2;
}
static inline void Dau_DsdMergeInlineDefinitions( char * pDsd, int * pMatches, char ** pVarDefs, char * pRes, int nShared )
{
int i;
char * pDef;
char * pBegin = pRes;
for ( i = 0; pDsd[i]; i++ )
{
// skip non-DSD block
if ( pDsd[i] == '<' && pDsd[pMatches[i]+1] == '{' )
{
assert( pDsd[pMatches[i]] == '>' );
for ( ; i <= pMatches[i]; i++ )
*pRes++ = pDsd[i];
}
if ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
while ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') )
*pRes++ = pDsd[i++];
// detect variables
if ( !(pDsd[i] >= 'a' && pDsd[i] <= 'z') || (pDsd[i] - 'a' < nShared) )
{
*pRes++ = pDsd[i];
continue;
}
// inline definition
assert( pDsd[i]-'a' < DAU_MAX_STR );
for ( pDef = pVarDefs[pDsd[i]-'a']; *pDef; pDef++ )
*pRes++ = *pDef;
}
*pRes++ = 0;
assert( pRes - pBegin < DAU_MAX_STR );
}
/**Function*************************************************************
Synopsis [Computes independence status for each opening paranthesis.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Dau_DsdMergePrintWithStatus( char * p, int * pStatus )
{
int i;
printf( "%s\n", p );
for ( i = 0; p[i]; i++ )
if ( !(p[i] == '(' || p[i] == '[' || p[i] == '<' || p[i] == '{' || (p[i] >= 'a' && p[i] <= 'z')) )
printf( " " );
else if ( pStatus[i] >= 0 )
printf( "%d", pStatus[i] );
else
printf( "-" );
printf( "\n" );
}
int Dau_DsdMergeStatus_rec( char * pStr, char ** p, int * pMatches, int nShared, int * pStatus )
{
// none pure
// 1 one pure
// 2 two or more pure
// 3 all pure
if ( **p == '!' )
{
pStatus[*p - pStr] = -1;
(*p)++;
}
while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
{
pStatus[*p - pStr] = -1;
(*p)++;
}
if ( **p == '<' )
{
char * q = pStr + pMatches[ *p - pStr ];
if ( *(q+1) == '{' )
{
char * pTemp = *p;
*p = q+1;
for ( ; pTemp < q+1; pTemp++ )
pStatus[pTemp - pStr] = -1;
}
}
if ( **p >= 'a' && **p <= 'f' ) // var
return pStatus[*p - pStr] = (**p - 'a' < nShared) ? 0 : 3;
if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
{
int Status, nPure = 0, nTotal = 0;
char * pOld = *p;
char * q = pStr + pMatches[ *p - pStr ];
assert( *q == **p + 1 + (**p != '(') );
for ( (*p)++; *p < q; (*p)++ )
{
Status = Dau_DsdMergeStatus_rec( pStr, p, pMatches, nShared, pStatus );
nPure += (Status == 3);
nTotal++;
}
assert( *p == q );
assert( nTotal > 1 );
if ( nPure == 0 )
Status = 0;
else if ( nPure == 1 )
Status = 1;
else if ( nPure < nTotal )
Status = 2;
else if ( nPure == nTotal )
Status = 3;
else assert( 0 );
return (pStatus[pOld - pStr] = Status);
}
assert( 0 );
return 0;
}
static inline int Dau_DsdMergeStatus( char * pDsd, int * pMatches, int nShared, int * pStatus )
{
return Dau_DsdMergeStatus_rec( pDsd, &pDsd, pMatches, nShared, pStatus );
}
/**Function*************************************************************
Synopsis [Extracts the formula.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dau_DsdMergeGetStatus( char * pBeg, char * pStr, int * pMatches, int * pStatus )
{
if ( *pBeg == '!' )
pBeg++;
while ( (*pBeg >= 'A' && *pBeg <= 'F') || (*pBeg >= '0' && *pBeg <= '9') )
pBeg++;
if ( *pBeg == '<' )
{
char * q = pStr + pMatches[pBeg - pStr];
if ( *(q+1) == '{' )
pBeg = q+1;
}
return pStatus[pBeg - pStr];
}
void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * pMatches, int * pStatus, int fWrite )
{
assert( **p != '!' );
/*
if ( **p == '!' )
{
if ( fWrite )
Dau_DsdMergeStoreAddToOutputChar( pS, **p );
(*p)++;
}
*/
while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
{
if ( fWrite )
Dau_DsdMergeStoreAddToOutputChar( pS, **p );
(*p)++;
}
if ( **p == '<' )
{
char * q = pStr + pMatches[ *p - pStr ];
if ( *(q+1) == '{' )
{
char * pTemp = *p;
*p = q+1;
if ( fWrite )
for ( ; pTemp < q+1; pTemp++ )
Dau_DsdMergeStoreAddToOutputChar( pS, *pTemp );
}
}
if ( **p >= 'a' && **p <= 'f' ) // var
{
if ( fWrite )
Dau_DsdMergeStoreAddToOutputChar( pS, **p );
return;
}
if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
{
int StatusFan, Status = pStatus[*p - pStr];
char New, * pBeg, * q = pStr + pMatches[ *p - pStr ];
assert( *q == **p + 1 + (**p != '(') );
if ( !fWrite )
{
assert( Status == 3 );
*p = q;
return;
}
assert( Status != 3 );
if ( Status == 0 ) // none pure
{
Dau_DsdMergeStoreAddToOutputChar( pS, **p );
for ( (*p)++; *p < q; (*p)++ )
{
if ( **p == '!' )
{
Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
(*p)++;
}
Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, 1 );
}
Dau_DsdMergeStoreAddToOutputChar( pS, **p );
assert( *p == q );
return;
}
if ( Status == 1 || **p == '<' || **p == '{' ) // 1 pure
{
Dau_DsdMergeStoreAddToOutputChar( pS, **p );
for ( (*p)++; *p < q; (*p)++ )
{
if ( **p == '!' )
{
Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
(*p)++;
}
pBeg = *p;
StatusFan = Dau_DsdMergeGetStatus( pBeg, pStr, pMatches, pStatus );
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 );
}
}
Dau_DsdMergeStoreAddToOutputChar( pS, **p );
assert( *p == q );
return;
}
if ( Status == 2 )
{
// add more than one defs
Dau_DsdMergeStoreAddToOutputChar( pS, **p );
Dau_DsdMergeStoreStartDef( pS, **p );
for ( (*p)++; *p < q; (*p)++ )
{
pBeg = *p;
StatusFan = Dau_DsdMergeGetStatus( pBeg, pStr, pMatches, pStatus );
if ( **p == '!' )
{
if ( StatusFan != 3 )
Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
else
Dau_DsdMergeStoreAddToDefChar( pS, '!' );
(*p)++;
pBeg++;
}
Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, StatusFan != 3 );
if ( StatusFan == 3 )
Dau_DsdMergeStoreAddToDef( pS, pBeg, *p+1 );
}
New = Dau_DsdMergeStoreStopDef( pS, *q );
Dau_DsdMergeStoreAddToOutputChar( pS, New );
Dau_DsdMergeStoreAddToOutputChar( pS, **p );
return;
}
assert( 0 );
return;
}
assert( 0 );
}
static inline void Dau_DsdMergeSubstitute( Dau_Sto_t * pS, char * pDsd, int * pMatches, int * pStatus )
{
if ( pDsd[0] == '!' )
{
Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
pDsd++;
}
Dau_DsdMergeSubstitute_rec( pS, pDsd, &pDsd, pMatches, pStatus, 1 );
Dau_DsdMergeStoreAddToOutputChar( pS, 0 );
}
/**Function*************************************************************
Synopsis [Removes braces.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dau_DsdRemoveBraces_rec( char * pStr, char ** p, int * pMatches )
{
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 == '[' || **p == '<' || **p == '{' )
{
char * q = pStr + pMatches[ *p - pStr ];
assert( *q == **p + 1 + (**p != '(') );
for ( (*p)++; *p < q; (*p)++ )
{
int fCompl = (**p == '!');
char * pBeg = fCompl ? *p + 1 : *p;
Dau_DsdRemoveBraces_rec( pStr, p, pMatches );
if ( (!fCompl && *pBeg == '(' && *q == ')') || (*pBeg == '[' && *q == ']') )
{
assert( **p == ')' || **p == ']' );
*pBeg = **p = ' ';
}
}
assert( *p == q );
return;
}
assert( 0 );
}
void Dau_DsdRemoveBraces( char * pDsd, int * pMatches )
{
char * q, * p = pDsd;
if ( pDsd[1] == 0 )
return;
Dau_DsdRemoveBraces_rec( pDsd, &pDsd, pMatches );
for ( q = p; *p; p++ )
if ( *p != ' ' )
*q++ = *p;
*q = 0;
}
/**Function*************************************************************
Synopsis [Performs merging of two DSD formulas.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1 )
{
static char pRes[DAU_MAX_STR];
char pDsd0[DAU_MAX_STR];
char pDsd1[DAU_MAX_STR];
int pMatches0[DAU_MAX_STR];
int pMatches1[DAU_MAX_STR];
int pVarPres[DAU_MAX_VAR];
int pOld2New[DAU_MAX_VAR];
int pNew2Old[DAU_MAX_VAR];
int pStatus0[DAU_MAX_STR];
int pStatus1[DAU_MAX_STR];
int pMatches[DAU_MAX_STR];
int nVarsShared, nVarsTotal;
Dau_Sto_t S, * pS = &S;
word Truth, t, t0, t1;
int Status;
// create local copies
Dau_DsdMergeCopy( pDsd0i, fCompl0, pDsd0 );
Dau_DsdMergeCopy( pDsd1i, fCompl1, pDsd1 );
// handle constants
if ( pDsd0[1] == 0 || pDsd1[1] == 0 )
{
if ( pDsd0[0] == '0' )
strcpy( pRes, pDsd0 );
else if ( pDsd0[0] == '1' )
strcpy( pRes, pDsd1 );
else if ( pDsd1[0] == '0' )
strcpy( pRes, pDsd1 );
else if ( pDsd1[0] == '1' )
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 );
printf( "%s\n", pDsd0 );
printf( "%s\n", pDsd1 );
t0 = Dau_Dsd6ToTruth( pDsd0 );
t1 = Dau_Dsd6ToTruth( pDsd1 );
// find shared varaiables
nVarsShared = Dau_DsdMergeFindShared(pDsd0, pDsd1, pMatches0, pMatches1, pVarPres);
if ( nVarsShared == 0 )
{
sprintf( pRes, "(%s%s)", pDsd0, pDsd1 );
return pRes;
}
// create variable mapping
nVarsTotal = Dau_DsdMergeCreateMaps( pVarPres, nVarsShared, pOld2New, pNew2Old );
// perform variable replacement
Dau_DsdMergeReplace( pDsd0, pMatches0, pOld2New );
Dau_DsdMergeReplace( pDsd1, pMatches1, pOld2New );
// find uniqueness status
Dau_DsdMergeStatus( pDsd0, pMatches0, nVarsShared, pStatus0 );
Dau_DsdMergeStatus( pDsd1, pMatches1, nVarsShared, pStatus1 );
Dau_DsdMergePrintWithStatus( pDsd0, pStatus0 );
Dau_DsdMergePrintWithStatus( pDsd1, pStatus1 );
// prepare storage
Dau_DsdMergeStoreClean( pS, nVarsShared );
// perform substitutions
Dau_DsdMergeStoreCleanOutput( pS );
Dau_DsdMergeSubstitute( pS, pDsd0, pMatches0, pStatus0 );
strcpy( pDsd0, pS->pOutput );
printf( "%s\n", pDsd0 );
// perform substitutions
Dau_DsdMergeStoreCleanOutput( pS );
Dau_DsdMergeSubstitute( pS, pDsd1, pMatches1, pStatus1 );
strcpy( pDsd1, pS->pOutput );
printf( "%s\n", pDsd1 );
Dau_DsdMergeStorePrintDefs( pS );
// create new function
assert( nVarsTotal <= 6 );
sprintf( pS->pOutput, "(%s%s)", pDsd0, pDsd1 );
Truth = Dau_Dsd6ToTruth( pS->pOutput );
Status = Dau_DsdDecompose( &Truth, nVarsTotal, 0, pS->pOutput );
if ( Status == -1 ) // did not find 1-step DSD
return NULL;
if ( Status > 6 ) // non-DSD part is too large
return NULL;
printf( "%s\n", pS->pOutput );
// substitute definitions
Dau_DsdMergeMatches( pS->pOutput, pMatches );
Dau_DsdMergeInlineDefinitions( pS->pOutput, pMatches, pS->pVarDefs, pRes, nVarsShared );
printf( "%s\n", pRes );
// perform variable replacement
Dau_DsdMergeMatches( pRes, pMatches );
Dau_DsdMergeReplace( pRes, pMatches, pNew2Old );
Dau_DsdRemoveBraces( pRes, pMatches );
printf( "%s\n", pRes );
Dau_DsdNormalize( pRes );
printf( "%s\n", pRes );
t = Dau_Dsd6ToTruth( pRes );
assert( t == (t0 & t1) );
return pRes;
}
void Dau_DsdTest()
{
int Perm0[DAU_MAX_VAR] = { 0, 1, 2, 3, 4, 5 };
// int pMatches[DAU_MAX_STR];
// int pStatus[DAU_MAX_STR];
// char * pStr = "(!(!a<bcd>)!(!fe))";
// char * pStr = "([acb]<!edf>)";
// char * pStr = "!(f!(b!c!(d[ea])))";
char * pStr = "[!(a[be])!(c!df)]";
// char * pStr = "<(e<bca>)fd>";
// char * pStr = "[d8001{abef}c]";
// char * pStr1 = "(abc)";
// char * pStr2 = "[adf]";
// char * pStr1 = "(!abce)";
// char * pStr2 = "[adf!b]";
// char * pStr1 = "(!abc)";
// char * pStr2 = "[ab]";
// char * pStr1 = "[d81{abe}c]";
// char * pStr1 = "[d<a(bc)(!b!c)>{abe}c]";
// char * pStr1 = "[d81{abe}c]";
// char * pStr1 = "[d(a[be])c]";
// char * pStr2 = "(df)";
// char * pStr1 = "(abf)";
// char * pStr2 = "(a[(bc)(fde)])";
char * pStr1 = "8001{abc[ef]}";
char * pStr2 = "(abe)";
char * pRes;
word t = Dau_Dsd6ToTruth( pStr );
return;
// pStr2 = Dau_DsdDecompose( &t, 6, 0, NULL );
// Dau_DsdNormalize( pStr2 );
// Dau_DsdMergeMatches( pStr, pMatches );
// Dau_DsdMergeStatus( pStr, pMatches, 2, pStatus );
// Dau_DsdMergePrintWithStatus( pStr, pStatus );
pRes = Dau_DsdMerge( pStr1, Perm0, pStr2, Perm0, 0, 0 );
t = 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/opt/dau/module.make
...@@ -2,4 +2,5 @@ SRC += src/opt/dau/dau.c \ ...@@ -2,4 +2,5 @@ SRC += src/opt/dau/dau.c \
src/opt/dau/dauCanon.c \ src/opt/dau/dauCanon.c \
src/opt/dau/dauCore.c \ src/opt/dau/dauCore.c \
src/opt/dau/dauDsd.c \ src/opt/dau/dauDsd.c \
src/opt/dau/dauEnum.c src/opt/dau/dauEnum.c \
src/opt/dau/dauMerge.c
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