/**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