/**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 "dauInt.h"
#include "misc/util/utilTruth.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_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;
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;
}
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 int Dau_DsdMergeStoreStartDef( Dau_Sto_t * pS, char 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, int New, char * pBeg, char * pEnd )
{
while ( pBeg < pEnd )
*pS->pPosStore[New]++ = *pBeg++;
}
static inline void Dau_DsdMergeStoreAddToDefChar( Dau_Sto_t * pS, int New, char c )
{
*pS->pPosStore[New]++ = c;
}
static inline void Dau_DsdMergeStoreStopDef( Dau_Sto_t * pS, int New, char c )
{
if (c) *pS->pPosStore[New]++ = c;
*pS->pPosStore[New]++ = 0;
}
static inline char Dau_DsdMergeStoreCreateDef( Dau_Sto_t * pS, char * pBeg, char * pEnd )
{
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->pStore[i][0] )
printf( "%c = %s\n", 'a' + i, pS->pStore[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 ( Dau_DsdIsConst(pDsd) ) // 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, Dau_Sto_t * pS, 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 = pS->pStore[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 <= 'z' ) // 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 <= 'z' ) // var
{
if ( fWrite )
Dau_DsdMergeStoreAddToOutputChar( pS, **p );
return;
}
if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
{
int New, StatusFan, Status = pStatus[*p - pStr];
char * 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 )
{
int New = Dau_DsdMergeStoreCreateDef( pS, pBeg, *p+1 );
Dau_DsdMergeStoreAddToOutputChar( pS, (char)('a' + New) );
}
}
Dau_DsdMergeStoreAddToOutputChar( pS, **p );
assert( *p == q );
return;
}
if ( Status == 2 )
{
// add more than one defs
Dau_DsdMergeStoreAddToOutputChar( pS, **p );
New = 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, New, '!' );
(*p)++;
pBeg++;
}
Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, StatusFan != 3 );
if ( StatusFan == 3 )
Dau_DsdMergeStoreAddToDef( pS, New, pBeg, *p+1 );
}
Dau_DsdMergeStoreStopDef( pS, New, *q );
Dau_DsdMergeStoreAddToOutputChar( pS, (char)('a' + 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 )
{
/*
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 );
}
/**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 <= 'z' ) // 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 != ' ' )
{
if ( *p == '!' && *(q-1) == '!' && p != q )
{
q--;
continue;
}
*q++ = *p;
}
*q = 0;
}
abctime s_TimeComp[4] = {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, int nVars )
{
int fVerbose = 0;
int fCheck = 0;
static int Counter = 0;
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 * pTruth, * pt = NULL, * pt0 = NULL, * pt1 = NULL;
word pParts[3][DAU_MAX_WORD];
int Status;
abctime clk = Abc_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 ( Dau_DsdIsConst(pDsd0) || Dau_DsdIsConst(pDsd1) )
{
if ( Dau_DsdIsConst0(pDsd0) )
strcpy( pRes, pDsd0 );
else if ( Dau_DsdIsConst1(pDsd0) )
strcpy( pRes, pDsd1 );
else if ( Dau_DsdIsConst0(pDsd1) )
strcpy( pRes, pDsd1 );
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 );
if ( fCheck )
{
pt0 = Dau_DsdToTruth( pDsd0, nVars );
Abc_TtCopy( pParts[0], pt0, Abc_TtWordNum(nVars), 0 );
}
if ( fCheck )
{
pt1 = Dau_DsdToTruth( pDsd1, nVars );
Abc_TtCopy( pParts[1], pt1, Abc_TtWordNum(nVars), 0 );
Abc_TtAnd( pParts[2], pParts[0], pParts[1], Abc_TtWordNum(nVars), 0 );
}
// 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[0] += Abc_Clock() - clk;
return pRes;
}
s_TimeComp[3] += Abc_Clock() - clk;
// 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 );
if ( fVerbose )
printf( "Individual status:\n" );
if ( fVerbose )
Dau_DsdMergePrintWithStatus( pDsd0, pStatus0 );
if ( fVerbose )
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 );
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
// assert( nVarsTotal <= 6 );
sprintf( pS->pOutput, "(%s%s)", pDsd0, pDsd1 );
pTruth = Dau_DsdToTruth( pS->pOutput, nVarsTotal );
Status = Dau_DsdDecompose( pTruth, nVarsTotal, 0, 1, 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, 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 );
if ( fCheck )
{
pt = Dau_DsdToTruth( pRes, nVars );
if ( !Abc_TtEqual( pParts[2], pt, Abc_TtWordNum(nVars) ) )
printf( "Dau_DsdMerge(): Verification failed!\n" );
}
if ( Status == 0 )
s_TimeComp[1] += Abc_Clock() - clk;
else
s_TimeComp[2] += Abc_Clock() - clk;
return pRes;
}
void Dau_DsdTest66()
{
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 * 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 );
// Dau_DsdMergeMatches( pStr, pMatches );
// Dau_DsdMergeStatus( pStr, pMatches, 2, pStatus );
// Dau_DsdMergePrintWithStatus( pStr, pStatus );
pRes = Dau_DsdMerge( pStr1, Perm0, pStr2, Perm0, 0, 0, 6 );
t = 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END