luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Improved DSD.

This commit is contained in:
Alan Mishchenko 2012-11-06 16:32:58 -08:00
parent cb5e2308b2
commit 3f7f497351
2 changed files with 365 additions and 88 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

209
src/misc/util/utilTruth.h
View File

@ -80,8 +80,30 @@ static word s_PMasks[5][3] = {
SeeAlso []
***********************************************************************/
static inline int Abc_TtWordNum( int nVars ) { return nVars <= 6 ? 1 : 1 << (nVars-6); }
static inline int Abc_TtByteNum( int nVars ) { return nVars <= 3 ? 1 : 1 << (nVars-3); }
// read/write/flip i-th bit of a bit string table:
static inline int Abc_TtGetBit( word * p, int i ) { return (int)(p[i>>6] >> (i & 63)) & 1; }
static inline void Abc_TtSetBit( word * p, int i ) { p[i>>6] |= (((word)1)<<(i & 63)); }
static inline void Abc_TtXorBit( word * p, int i ) { p[i>>6] ^= (((word)1)<<(i & 63)); }
// read/write k-th digit d of a hexadecimal number:
static inline int Abc_TtGetHex( word * p, int k ) { return (int)(p[k>>4] >> ((k<<2) & 63)) & 15; }
static inline void Abc_TtSetHex( word * p, int k, int d ) { p[k>>4] |= (((word)d)<<((k<<2) & 63)); }
static inline void Abc_TtXorHex( word * p, int k, int d ) { p[k>>4] ^= (((word)d)<<((k<<2) & 63)); }
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_TtWordNum( int nVars ) { return nVars <= 6 ? 1 : 1 << (nVars-6); }
static inline int Abc_TtByteNum( int nVars ) { return nVars <= 3 ? 1 : 1 << (nVars-3); }
static inline int Abc_TtHexDigitNum( int nVars ) { return nVars <= 2 ? 1 : 1 << (nVars-2); }
/**Function*************************************************************
@ -425,6 +447,66 @@ static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar )
}
}
/**Function*************************************************************
Synopsis [Stretch truthtable to have more input variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB )
{
int w, i, step, nWords;
if ( nVarS == nVarB )
return;
assert( nVarS < nVarB );
step = Abc_TruthWordNum(nVarS);
nWords = Abc_TruthWordNum(nVarB);
if ( step == nWords )
return;
assert( step < nWords );
for ( w = 0; w < nWords; w += step )
for ( i = 0; i < step; i++ )
pInOut[w + i] = pInOut[i];
}
static inline void Abc_TtStretch6( word * pInOut, int nVarS, int nVarB )
{
int w, i, step, nWords;
if ( nVarS == nVarB )
return;
assert( nVarS < nVarB );
step = Abc_Truth6WordNum(nVarS);
nWords = Abc_Truth6WordNum(nVarB);
if ( step == nWords )
return;
assert( step < nWords );
for ( w = 0; w < nWords; w += step )
for ( i = 0; i < step; i++ )
pInOut[w + i] = pInOut[i];
}
static inline word Abc_Tt6Stretch( word t, int nVars )
{
assert( nVars >= 0 );
if ( nVars == 0 )
nVars++, t = (t & 0x1) | ((t & 0x1) << 1);
if ( nVars == 1 )
nVars++, t = (t & 0x3) | ((t & 0x3) << 2);
if ( nVars == 2 )
nVars++, t = (t & 0xF) | ((t & 0xF) << 4);
if ( nVars == 3 )
nVars++, t = (t & 0xFF) | ((t & 0xFF) << 8);
if ( nVars == 4 )
nVars++, t = (t & 0xFFFF) | ((t & 0xFFFF) << 16);
if ( nVars == 5 )
nVars++, t = (t & 0xFFFFFFFF) | ((t & 0xFFFFFFFF) << 32);
assert( nVars == 6 );
return t;
}
/**Function*************************************************************
Synopsis []
@ -436,13 +518,40 @@ static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar )
SeeAlso []
***********************************************************************/
static inline int Abc_TtIsHexDigit( char HexChar )
{
return (HexChar >= '0' && HexChar <= '9') || (HexChar >= 'A' && HexChar <= 'F') || (HexChar >= 'a' && HexChar <= 'f');
}
static inline char Abc_TtPrintDigit( int Digit )
{
assert( Digit >= 0 && Digit < 16 );
if ( Digit < 10 )
return '0' + Digit;;
return '0' + Digit;
return 'A' + Digit-10;
}
static inline int Abc_TtReadHexDigit( char HexChar )
{
if ( HexChar >= '0' && HexChar <= '9' )
return HexChar - '0';
if ( HexChar >= 'A' && HexChar <= 'F' )
return HexChar - 'A' + 10;
if ( HexChar >= 'a' && HexChar <= 'f' )
return HexChar - 'a' + 10;
assert( 0 ); // not a hexadecimal symbol
return -1; // return value which makes no sense
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Abc_TtPrintHex( word * pTruth, int nVars )
{
word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
@ -485,6 +594,58 @@ static inline int Abc_TtWriteHexRev( char * pStr, word * pTruth, int nVars )
return pStr - pStrInit;
}
/**Function*************************************************************
Synopsis [Reads hex truth table from a string.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_TtReadHex( word * pTruth, char * pString )
{
int k, nVars, Digit, nDigits;
// skip the first 2 symbols if they are "0x"
if ( pString[0] == '0' && pString[1] == 'x' )
pString += 2;
// count the number of hex digits
nDigits = 0;
for ( k = 0; Abc_TtIsHexDigit(pString[k]); k++ )
nDigits++;
if ( nDigits == 1 )
{
if ( pString[0] == '0' || pString[0] == 'F' )
{
pTruth[0] = (pString[0] == '0') ? 0 : ~(word)0;
return 0;
}
if ( pString[0] == '5' || pString[0] == 'A' )
{
pTruth[0] = (pString[0] == '5') ? s_Truths6Neg[0] : s_Truths6[0];
return 1;
}
}
// determine the number of variables
nVars = 2 + Abc_Base2Log( nDigits );
// clean storage
for ( k = Abc_TtWordNum(nVars) - 1; k >= 0; k-- )
pTruth[k] = 0;
// read hexadecimal digits in the reverse order
// (the last symbol in the string is the least significant digit)
for ( k = 0; k < nDigits; k++ )
{
Digit = Abc_TtReadHexDigit( pString[nDigits - 1 - k] );
assert( Digit >= 0 && Digit < 16 );
Abc_TtSetHex( pTruth, k, Digit );
}
if ( nVars < 6 )
pTruth[0] = Abc_Tt6Stretch( pTruth[0], nVars );
return nVars;
}
/**Function*************************************************************
@ -890,48 +1051,6 @@ static inline void Abc_TtReverseBits( word * pTruth, int nVars )
}
/**Function*************************************************************
Synopsis [Stretch truthtable to have more input variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB )
{
int w, i, step, nWords;
if ( nVarS == nVarB )
return;
assert( nVarS < nVarB );
step = Abc_TruthWordNum(nVarS);
nWords = Abc_TruthWordNum(nVarB);
if ( step == nWords )
return;
assert( step < nWords );
for ( w = 0; w < nWords; w += step )
for ( i = 0; i < step; i++ )
pInOut[w + i] = pInOut[i];
}
static inline void Abc_TtStretch6( word * pInOut, int nVarS, int nVarB )
{
int w, i, step, nWords;
if ( nVarS == nVarB )
return;
assert( nVarS < nVarB );
step = Abc_Truth6WordNum(nVarS);
nWords = Abc_Truth6WordNum(nVarB);
if ( step == nWords )
return;
assert( step < nWords );
for ( w = 0; w < nWords; w += step )
for ( i = 0; i < step; i++ )
pInOut[w + i] = pInOut[i];
}
/*=== utilTruth.c ===========================================================*/

244
src/opt/dau/dauDsd.c
View File

@ -27,7 +27,9 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define DAU_MAX_STR 256
#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.
@ -54,15 +56,39 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
int * Dau_DsdComputeMatches( char * p )
{
static int pMatches[DAU_MAX_STR];
int pNested[DAU_MAX_VAR];
int v, nNested = 0;
for ( v = 0; p[v]; v++ )
{
pMatches[v] = 0;
if ( p[v] == '(' || p[v] == '[' || p[v] == '<' || p[v] == '{' )
pNested[nNested++] = v;
else if ( p[v] == ')' || p[v] == ']' || p[v] == '>' || p[v] == '}' )
pMatches[pNested[--nNested]] = v;
}
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;
}
char * Dau_DsdFindMatch( char * p )
{
int Counter = 0;
assert( *p == '(' || *p == '[' || *p == '<' );
assert( *p == '(' || *p == '[' || *p == '<' || *p == '{' );
while ( *p )
{
if ( *p == '(' || *p == '[' || *p == '<' )
if ( *p == '(' || *p == '[' || *p == '<' || *p == '{' )
Counter++;
else if ( *p == ')' || *p == ']' || *p == '>' )
else if ( *p == ')' || *p == ']' || *p == '>' || *p == '}' )
Counter--;
if ( Counter == 0 )
return p;
@ -70,7 +96,23 @@ char * Dau_DsdFindMatch( char * p )
}
return NULL;
}
word Dau_DsdToTruth_rec( char ** p )
word Dau_DsdTruthCompose_rec( word Func, word * pFanins, int nVars )
{
word t0, t1;
if ( Func == 0 )
return 0;
if ( Func == ~(word)0 )
return ~(word)0;
assert( nVars > 0 );
if ( --nVars == 0 )
return (Func == s_Truths6[0]) ? pFanins[0] : ~pFanins[0];
if ( !Abc_Tt6HasVar(Func, nVars) )
return Dau_DsdTruthCompose_rec( Func, pFanins, nVars );
t0 = Dau_DsdTruthCompose_rec( Abc_Tt6Cofactor0(Func, nVars), pFanins, nVars );
t1 = Dau_DsdTruthCompose_rec( Abc_Tt6Cofactor1(Func, nVars), pFanins, nVars );
return (~pFanins[nVars] & t0) | (pFanins[nVars] & t1);
}
word Dau_DsdToTruth_rec( char * pStr, char ** p, int * pMatches )
{
int fCompl = 0;
if ( **p == '!' )
@ -83,8 +125,8 @@ word Dau_DsdToTruth_rec( char ** p )
if ( **p == '(' || **p == '[' || **p == '<' )
{
word Res = 0;
char * q = Dau_DsdFindMatch( *p );
assert( q != NULL );
// char * q2 = Dau_DsdFindMatch( *p );
char * q = pStr + pMatches[ *p - pStr ];
assert( (**p == '(') == (*q == ')') );
assert( (**p == '[') == (*q == ']') );
assert( (**p == '<') == (*q == '>') );
@ -92,19 +134,19 @@ word Dau_DsdToTruth_rec( char ** p )
{
Res = ~(word)0;
for ( (*p)++; *p < q; (*p)++ )
Res &= Dau_DsdToTruth_rec( p );
Res &= Dau_DsdToTruth_rec( pStr, p, pMatches );
}
else if ( **p == '[' ) // xor
{
Res = 0;
for ( (*p)++; *p < q; (*p)++ )
Res ^= Dau_DsdToTruth_rec( p );
Res ^= Dau_DsdToTruth_rec( pStr, p, pMatches );
}
else if ( **p == '<' ) // mux
{
word Temp[3], * pTemp = Temp;
for ( (*p)++; *p < q; (*p)++ )
*pTemp++ = Dau_DsdToTruth_rec( p );
*pTemp++ = Dau_DsdToTruth_rec( pStr, p, pMatches );
assert( pTemp == Temp + 3 );
Res = (Temp[0] & Temp[1]) | (~Temp[0] & Temp[2]);
}
@ -112,18 +154,31 @@ word Dau_DsdToTruth_rec( char ** p )
assert( *p == q );
return fCompl ? ~Res : Res;
}
if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
{
word Func, Fanins[6];
char * q;
int i, nVars = Abc_TtReadHex( &Func, *p );
*p += Abc_TtHexDigitNum( nVars );
q = pStr + pMatches[ *p - pStr ];
assert( **p == '{' && *q == '}' );
for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
Fanins[i] = Dau_DsdToTruth_rec( pStr, p, pMatches );
assert( i == nVars );
return Dau_DsdTruthCompose_rec( Func, Fanins, nVars );
}
assert( 0 );
return 0;
}
word Dau_DsdToTruth( char * p )
{
word Res;
if ( *p == '0' )
if ( *p == '0' && *(p+1) == 0 )
Res = 0;
else if ( *p == '1' )
else if ( *p == '1' && *(p+1) == 0 )
Res = ~(word)0;
else
Res = Dau_DsdToTruth_rec( &p );
Res = Dau_DsdToTruth_rec( p, &p, Dau_DsdComputeMatches(p) );
assert( *++p == 0 );
return Res;
}
@ -779,7 +834,7 @@ static inline void Dau_DsdWriteVar( Dau_Dsd_t * p, int iVar, int fInv )
static inline void Dau_DsdTranslate( Dau_Dsd_t * p, int * pVars, int nVars, char * pStr )
{
for ( ; *pStr; pStr++ )
if ( *pStr >= 'a' + nVars && *pStr < 'a' + nVars )
if ( *pStr >= 'a' && *pStr < 'a' + nVars )
Dau_DsdWriteVar( p, pVars[*pStr - 'a'], 0 );
else
p->pOutput[ p->nPos++ ] = *pStr;
@ -814,6 +869,15 @@ static inline int Dau_DsdAddVarDef( Dau_Dsd_t * p, char * pStr )
sprintf( p->pVarDefs[p->nVarsUsed++], "%s", pStr );
return p->nVarsUsed - 1;
}
static inline int Dau_DsdFindVarDef( int * pVars, int nVars, int VarDef )
{
int v;
for ( v = 0; v < nVars; v++ )
if ( pVars[v] == VarDef )
break;
assert( v < nVars );
return v;
}
static inline void Dau_DsdInsertVarCache( Dau_Dsd_t * p, int v, int u, int Status )
{
assert( v != u );
@ -826,6 +890,48 @@ static inline int Dau_DsdLookupVarCache( Dau_Dsd_t * p, int v, int u )
return p->Cache[v][u];
}
/**Function*************************************************************
Synopsis [Generate random permutation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dau_DsdFindVarNum( char * pDsd )
{
int vMax = 0;
pDsd--;
while ( *++pDsd )
if ( *pDsd >= 'a' && *pDsd <= 'z' )
vMax = Abc_MaxInt( vMax, *pDsd - 'a' );
return vMax + 1;
}
void Dau_DsdGenRandPerm( int * pPerm, int nVars )
{
int v, vNew;
for ( v = 0; v < nVars; v++ )
pPerm[v] = v;
for ( v = 0; v < nVars; v++ )
{
vNew = rand() % nVars;
ABC_SWAP( int, pPerm[v], pPerm[vNew] );
}
}
void Dau_DsdPermute( char * pDsd )
{
int pPerm[16];
int nVars = Dau_DsdFindVarNum( pDsd );
Dau_DsdGenRandPerm( pPerm, nVars );
pDsd--;
while ( *++pDsd )
if ( *pDsd >= 'a' && *pDsd < 'a' + nVars )
*pDsd = 'a' + pPerm[*pDsd - 'a'];
}
/**Function*************************************************************
Synopsis []
@ -955,6 +1061,8 @@ static inline unsigned Dau_Dsd6FindSupports( Dau_Dsd_t * p, word * pTruth, int
unsigned uSupports = 0;
word tCof0 = Abc_Tt6Cofactor0( pTruth[0], v );
word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v );
//Kit_DsdPrintFromTruth( (unsigned *)&tCof0, 6 );printf( "\n" );
//Kit_DsdPrintFromTruth( (unsigned *)&tCof1, 6 );printf( "\n" );
for ( u = 0; u < nVars; u++ )
if ( u != v )
uSupports |= (Dau_Dsd6FindSupportOne( p, tCof0, tCof1, pVars, nVars, v, u ) << (2 * u));
@ -1051,7 +1159,7 @@ int Dau_Dsd6DecomposeDoubleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int
{
for ( u = v - 1; u >= 0; u-- )
{
if ( Dau_DsdLookupVarCache( p, v, u ) )
if ( Dau_DsdLookupVarCache( p, pVars[v], pVars[u] ) )
continue;
nVarsOld = nVars;
nVars = Dau_Dsd6DecomposeDoubleVarsOne( p, pTruth, pVars, nVars, v, u );
@ -1074,24 +1182,25 @@ static inline int Dau_Dsd6DecomposeTripleVarsOuter( Dau_Dsd_t * p, word * pTrut
{
extern void Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit );
Dau_Dsd_t P1, * p1 = &P1;
Dau_Dsd_t P2, * p2 = &P2;
word tCof0, tCof1;
// move this variable to the top
pVars[v] = pVars[nVars-1];
ABC_SWAP( int, pVars[v], pVars[nVars-1] );
Abc_TtSwapVars( pTruth, 6, v, nVars-1 );
// cofactor w.r.t the last variable
tCof0 = Abc_Tt6Cofactor0( pTruth[0], nVars - 1 );
tCof1 = Abc_Tt6Cofactor1( pTruth[0], nVars - 1 );
// split decomposition
Dau_DsdDecomposeInt( p1, &tCof0, nVars - 1 );
Dau_DsdDecomposeInt( p2, &tCof1, nVars - 1 );
p->nSizeNonDec = Abc_MaxInt( p1->nSizeNonDec, p2->nSizeNonDec );
// compose the result
Dau_DsdWriteString( p, "<" );
Dau_DsdWriteVar( p, pVars[nVars - 1], 0 );
// split decomposition
Dau_DsdDecomposeInt( p1, &tCof1, nVars - 1 );
Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
p->nSizeNonDec = p1->nSizeNonDec;
// split decomposition
Dau_DsdDecomposeInt( p1, &tCof0, nVars - 1 );
Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
Dau_DsdTranslate( p, pVars, nVars - 1, p2->pOutput );
Dau_DsdWriteString( p, ">" );
p->nSizeNonDec = Abc_MaxInt( p->nSizeNonDec, p1->nSizeNonDec );
return 0;
}
static inline int Dau_Dsd6DecomposeTripleVarsInner( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, unsigned uSupports )
@ -1112,20 +1221,23 @@ static inline int Dau_Dsd6DecomposeTripleVarsInner( Dau_Dsd_t * p, word * pTrut
if ( fEqual0 || fEqual1 )
{
char pBuffer[10];
int iVarMin = Abc_MinInt( v, Abc_MinInt( iVar0, iVar1 ) );
// assert( iVarMin < iVar0 && iVar0 < iVar1 );
pTruth[0] = (s_Truths6[iVarMin] & Abc_Tt6Cofactor0(tCof1, iVar1)) | (~s_Truths6[iVarMin] & Abc_Tt6Cofactor1(tCof1, iVar1));
if ( fEqual1 )
pTruth[0] = ~pTruth[0];
sprintf( pBuffer, "<%c%c%c>", 'a' + pVars[v], 'a' + pVars[iVar1], 'a' + pVars[iVar0] );
pVars[iVarMin] = Dau_DsdAddVarDef( p, pBuffer );
pVars[iVar1] = pVars[nVars-1];
Abc_TtSwapVars( pTruth, 6, iVar1, nVars-1 );
pVars[iVar0] = pVars[nVars-2];
Abc_TtSwapVars( pTruth, 6, iVar0, nVars-2 );
nVars -= 2;
return Dau_Dsd6DecomposeSingleVar( p, pTruth, pVars, nVars );
int VarId = pVars[iVar0];
pTruth[0] = (s_Truths6[v] & C11) | (~s_Truths6[v] & C10);
sprintf( pBuffer, "<%c%c%s%c>", 'a' + pVars[v], 'a' + pVars[iVar1], fEqual1 ? "!":"", 'a' + pVars[iVar0] );
pVars[v] = Dau_DsdAddVarDef( p, pBuffer );
// remove iVar1
ABC_SWAP( int, pVars[iVar1], pVars[nVars-1] );
Abc_TtSwapVars( pTruth, 6, iVar1, --nVars );
// remove iVar0
iVar0 = Dau_DsdFindVarDef( pVars, nVars, VarId );
ABC_SWAP( int, pVars[iVar0], pVars[nVars-1] );
Abc_TtSwapVars( pTruth, 6, iVar0, --nVars );
// find the new var
v = Dau_DsdFindVarDef( pVars, nVars, p->nVarsUsed-1 );
// remove single variables if possible
if ( Dau_Dsd6DecomposeSingleVarOne( p, pTruth, pVars, nVars, v ) )
nVars = Dau_Dsd6DecomposeSingleVar( p, pTruth, pVars, --nVars );
return nVars;
}
return nVars;
}
@ -1134,13 +1246,14 @@ int Dau_Dsd6DecomposeTripleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int
while ( 1 )
{
int v;
// Kit_DsdPrintFromTruth( (unsigned *)pTruth, 6 ); printf( "\n" );
for ( v = nVars - 1; v >= 0; v-- )
{
unsigned uSupports = Dau_Dsd6FindSupports( p, pTruth, pVars, nVars, v );
Dau_DsdPrintSupports( uSupports, nVars );
// Dau_DsdPrintSupports( uSupports, nVars );
if ( (uSupports & (uSupports >> 1) & 0x55555555) == 0 ) // non-overlapping supports
return Dau_Dsd6DecomposeTripleVarsOuter( p, pTruth, pVars, nVars, v );
if ( Abc_TtSuppOnlyOne( uSupports & (~uSupports >> 1) & 0x55555555) ||
if ( Abc_TtSuppOnlyOne( uSupports & (~uSupports >> 1) & 0x55555555) &&
Abc_TtSuppOnlyOne(~uSupports & ( uSupports >> 1) & 0x55555555) ) // one unique variable in each cofactor
{
nVars = Dau_Dsd6DecomposeTripleVarsInner( p, pTruth, pVars, nVars, v, uSupports );
@ -1246,6 +1359,7 @@ char * Dau_DsdDecompose( word * pTruth, int nVarsInit, int * pnSizeNonDec )
{
static Dau_Dsd_t P;
Dau_Dsd_t * p = &P;
p->nSizeNonDec = 0;
if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) )
p->pOutput[0] = '0', p->pOutput[1] = 0;
else if ( (pTruth[0] & 1) && Abc_TtIsConst1(pTruth, Abc_TtWordNum(nVarsInit)) )
@ -1254,24 +1368,68 @@ char * Dau_DsdDecompose( word * pTruth, int nVarsInit, int * pnSizeNonDec )
{
Dau_DsdDecomposeInt( p, pTruth, nVarsInit );
Dau_DsdCleanBraces( p->pOutput );
if ( pnSizeNonDec )
*pnSizeNonDec = p->nSizeNonDec;
}
if ( pnSizeNonDec )
*pnSizeNonDec = p->nSizeNonDec;
return p->pOutput;
}
void Dau_DsdTest()
{
// char * pStr = "(!(!a<bcd>)!(!fe))";
// char * pStr = "<cba>";
// char * pStr = "([acb]<!edf>)";
// 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 = "[d8001{a(!bc)ef}]";
char * pStr2;
word t = Dau_DsdToTruth( pStr );
return;
// return;
pStr2 = Dau_DsdDecompose( &t, 6, NULL );
t = 0;
}
void Dau_DsdTest22()
{
char * pFileName = "_npn/npn/dsd06.txt";
FILE * pFile = fopen( pFileName, "rb" );
word t, t1, t2;
char pBuffer[100];
char * pStr2;
int nSizeNonDec;
int i, Counter = 0;
while ( fgets( pBuffer, 100, pFile ) != NULL )
{
pStr2 = pBuffer + strlen(pBuffer)-1;
if ( *pStr2 == '\n' )
*pStr2-- = 0;
if ( *pStr2 == '\r' )
*pStr2-- = 0;
if ( pBuffer[0] == 'V' || pBuffer[0] == 0 )
continue;
Counter++;
for ( i = 0; i < 10; i++ )
{
Dau_DsdPermute( pBuffer );
t = t1 = Dau_DsdToTruth( pBuffer[0] == '*' ? pBuffer + 1 : pBuffer );
pStr2 = Dau_DsdDecompose( &t, 6, &nSizeNonDec );
assert( nSizeNonDec == 0 );
t2 = Dau_DsdToTruth( pStr2 );
if ( t1 != t2 )
{
// Kit_DsdPrintFromTruth( (unsigned *)&t, 6 );
// printf( " " );
// Kit_DsdPrintFromTruth( (unsigned *)&t2, 6 );
printf( "%s -> %s \n", pBuffer, pStr2 );
printf( "Verification failed.\n" );
}
}
}
printf( "Finished trying %d decompositions.\n", Counter );
fclose( pFile );
}
////////////////////////////////////////////////////////////////////////