/**CFile****************************************************************

  FileName    [dauTree.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [DAG-aware unmapping.]

  Synopsis    [Canonical DSD package.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: dauTree.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "dauInt.h"
#include "misc/mem/mem.h"
#include "misc/util/utilTruth.h"

ABC_NAMESPACE_IMPL_START

////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Dss_Fun_t_ Dss_Fun_t;
struct Dss_Fun_t_
{
    unsigned       iDsd  :    26;  // DSD literal
    unsigned       nFans :     6;  // fanin count
    unsigned char  pFans[0];       // fanins
};

typedef struct Dss_Ent_t_ Dss_Ent_t;
struct Dss_Ent_t_
{
    Dss_Fun_t *    pFunc;
    Dss_Ent_t *    pNext;
    unsigned       iDsd0  :   27;  // dsd entry
    unsigned       nWords :    5;  // total word count (struct + shared)
    unsigned       iDsd1  :   27;  // dsd entry
    unsigned       nShared:    5;  // shared count
    unsigned char  pShared[0];     // shared literals
};

typedef struct Dss_Obj_t_ Dss_Obj_t;
struct Dss_Obj_t_
{
    unsigned       Id;             // node ID
    unsigned       Type    :   3;  // node type
    unsigned       nSupp   :   8;  // variable
    unsigned       iVar    :   8;  // variable
    unsigned       nWords  :   6;  // variable
    unsigned       fMark0  :   1;  // user mark
    unsigned       fMark1  :   1;  // user mark
    unsigned       nFans   :   5;  // fanin count
    unsigned       pFans[0];       // fanins
};

typedef struct Dss_Ntk_t_ Dss_Ntk_t;
struct Dss_Ntk_t_
{
    int            nVars;          // the number of variables
    int            nMem;           // memory used
    int            nMemAlloc;      // memory allocated
    word *         pMem;           // memory array
    Dss_Obj_t *    pRoot;          // root node
    Vec_Ptr_t *    vObjs;          // internal nodes
};

struct Dss_Man_t_
{
    int            nVars;          // variable number
    int            nNonDecLimit;   // limit on non-dec size
    int            nBins;          // table size
    unsigned *     pBins;          // hash table
    Mem_Flex_t *   pMem;           // memory for nodes
    Vec_Ptr_t *    vObjs;          // objects
    Vec_Int_t *    vNexts;         // next pointers
    Vec_Int_t *    vLeaves;        // temp
    Vec_Int_t *    vCopies;        // temp
    word **        pTtElems;       // elementary TTs
    Dss_Ent_t **   pCache;         // decomposition cache
    int            nCache;         // size of decomposition cache
    Mem_Flex_t *   pMemEnts;       // memory for cache entries
    int            nCacheHits[2];
    int            nCacheMisses[2];
    int            nCacheEntries[2];
    abctime        timeBeg;
    abctime        timeDec;
    abctime        timeLook;
    abctime        timeEnd;
};

static inline Dss_Obj_t *  Dss_Regular( Dss_Obj_t * p )                            { return (Dss_Obj_t *)((ABC_PTRUINT_T)(p) & ~01);                                    }
static inline Dss_Obj_t *  Dss_Not( Dss_Obj_t * p )                                { return (Dss_Obj_t *)((ABC_PTRUINT_T)(p) ^  01);                                    }
static inline Dss_Obj_t *  Dss_NotCond( Dss_Obj_t * p, int c )                     { return (Dss_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c));                                    }
static inline int          Dss_IsComplement( Dss_Obj_t * p )                       { return (int)((ABC_PTRUINT_T)(p) & 01);                                             }

static inline int          Dss_EntWordNum( Dss_Ent_t * p )                         { return sizeof(Dss_Ent_t) / 8 + p->nShared / 4 + ((p->nShared & 3) > 0);            }
static inline int          Dss_FunWordNum( Dss_Fun_t * p )                         { assert(p->nFans >= 2); return (p->nFans + 4) / 8 + (((p->nFans + 4) & 7) > 0);     }
static inline int          Dss_ObjWordNum( int nFans )                             { return sizeof(Dss_Obj_t) / 8 + nFans / 2 + ((nFans & 1) > 0);                      }
static inline word *       Dss_ObjTruth( Dss_Obj_t * pObj )                        { return (word *)pObj + pObj->nWords;                                                }

static inline void         Dss_ObjClean( Dss_Obj_t * pObj )                        { memset( pObj, 0, sizeof(Dss_Obj_t) );                                              }
static inline int          Dss_ObjId( Dss_Obj_t * pObj )                           { return pObj->Id;                                                                   }
static inline int          Dss_ObjType( Dss_Obj_t * pObj )                         { return pObj->Type;                                                                 }
static inline int          Dss_ObjSuppSize( Dss_Obj_t * pObj )                     { return pObj->nSupp;                                                                }
static inline int          Dss_ObjFaninNum( Dss_Obj_t * pObj )                     { return pObj->nFans;                                                                }
static inline int          Dss_ObjFaninC( Dss_Obj_t * pObj, int i )                { assert(i < (int)pObj->nFans); return Abc_LitIsCompl(pObj->pFans[i]);               }

static inline Dss_Obj_t *  Dss_VecObj( Vec_Ptr_t * p, int Id )                     { return (Dss_Obj_t *)Vec_PtrEntry(p, Id);                                           }
static inline Dss_Obj_t *  Dss_VecConst0( Vec_Ptr_t * p )                          { return Dss_VecObj( p, 0 );                                                         }
static inline Dss_Obj_t *  Dss_VecVar( Vec_Ptr_t * p, int v )                      { return Dss_VecObj( p, v+1 );                                                       }
static inline int          Dss_VecLitSuppSize( Vec_Ptr_t * p, int iLit )           { return Dss_VecObj( p, Abc_Lit2Var(iLit) )->nSupp;                                  }

static inline int          Dss_Obj2Lit( Dss_Obj_t * pObj )                         { return Abc_Var2Lit(Dss_Regular(pObj)->Id, Dss_IsComplement(pObj));                 }
static inline Dss_Obj_t *  Dss_Lit2Obj( Vec_Ptr_t * p, int iLit )                  { return Dss_NotCond(Dss_VecObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit));        }
static inline Dss_Obj_t *  Dss_ObjFanin( Vec_Ptr_t * p, Dss_Obj_t * pObj, int i )  { assert(i < (int)pObj->nFans); return Dss_VecObj(p, Abc_Lit2Var(pObj->pFans[i]));   }
static inline Dss_Obj_t *  Dss_ObjChild( Vec_Ptr_t * p, Dss_Obj_t * pObj, int i )  { assert(i < (int)pObj->nFans); return Dss_Lit2Obj(p, pObj->pFans[i]);               }

#define Dss_VecForEachObj( vVec, pObj, i )                \
    Vec_PtrForEachEntry( Dss_Obj_t *, vVec, pObj, i )
#define Dss_VecForEachObjVec( vLits, vVec, pObj, i )      \
    for ( i = 0; (i < Vec_IntSize(vLits)) && ((pObj) = Dss_Lit2Obj(vVec, Vec_IntEntry(vLits,i))); i++ )
#define Dss_VecForEachNode( vVec, pObj, i )               \
    Vec_PtrForEachEntry( Dss_Obj_t *, vVec, pObj, i )     \
        if ( pObj->Type == DAU_DSD_CONST0 || pObj->Type == DAU_DSD_VAR ) {} else
#define Dss_ObjForEachFanin( vVec, pObj, pFanin, i )      \
    for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjFanin(vVec, pObj, i)); i++ )
#define Dss_ObjForEachChild( vVec, pObj, pFanin, i )      \
    for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjChild(vVec, pObj, i)); i++ )

static inline int Dss_WordCountOnes( unsigned uWord )
{
    uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
    uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
    uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
    uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
    return  (uWord & 0x0000FFFF) + (uWord>>16);
}

static inline int Dss_Lit2Lit( int * pMapLit, int Lit )   { return Abc_Var2Lit( Abc_Lit2Var(pMapLit[Abc_Lit2Var(Lit)]), Abc_LitIsCompl(Lit) ^ Abc_LitIsCompl(pMapLit[Abc_Lit2Var(Lit)]) );   }

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

#if 0

/**Function*************************************************************

  Synopsis    [Check decomposability for 666.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
// recursively collects 6-feasible supports
int Dss_ObjCheck666_rec( Dss_Ntk_t * p, Dss_Obj_t * pObj, Vec_Int_t * vSupps )
{
    Dss_Obj_t * pFanin;
    int i, uSupp = 0;
    assert( !Dss_IsComplement(pObj) );
    if ( pObj->Type == DAU_DSD_VAR )
    {
        assert( pObj->iVar >= 0 && pObj->iVar < 30 );
        return (1 << pObj->iVar);
    }
    if ( pObj->Type == DAU_DSD_AND || pObj->Type == DAU_DSD_XOR )
    {
        int c0, c1, c2, uSuppTemp;
        int uSuppVars[16];
        int nSuppVars = 0;
        int nFanins = Dss_ObjFaninNum(pObj);
        int uSupps[16], nSuppSizes[16];
        Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
        {
            uSupps[i] = Dss_ObjCheck666_rec( p, pFanin, vSupps );
            nSuppSizes[i] = Dss_WordCountOnes( uSupps[i] );
            uSupp |= uSupps[i];
            if ( nSuppSizes[i] == 1 )
                uSuppVars[nSuppVars++] = uSupps[i];
        }
        // iterate through the permutations
        for ( c0 = 0; c0 < nFanins; c0++ )
        if ( nSuppSizes[c0] > 1 && nSuppSizes[c0] < 6 )
        {
            uSuppTemp = uSupps[c0];
            for ( i = 0; i < nSuppVars; i++ )
                if ( nSuppSizes[c0] + i < 6 )
                    uSuppTemp |= uSuppVars[i];
                else
                    break;
            if ( Dss_WordCountOnes(uSuppTemp) <= 6 )
                Vec_IntPush( vSupps, uSuppTemp );

            for ( c1 = c0 + 1; c1 < nFanins; c1++ )
            if ( nSuppSizes[c1] > 1 && nSuppSizes[c1] < 6 )
            {
                if ( nSuppSizes[c0] + nSuppSizes[c1] <= 6 )
                    Vec_IntPush( vSupps, uSupps[c0] | uSupps[c1] );

                uSuppTemp = uSupps[c0] | uSupps[c1];
                for ( i = 0; i < nSuppVars; i++ )
                    if ( nSuppSizes[c0] + nSuppSizes[c1] + i < 6 )
                        uSuppTemp |= uSuppVars[i];
                    else
                        break;
                if ( Dss_WordCountOnes(uSuppTemp) <= 6 )
                    Vec_IntPush( vSupps, uSuppTemp );

                for ( c2 = c1 + 1; c2 < nFanins; c2++ )
                if ( nSuppSizes[c2] > 1 && nSuppSizes[c2] < 6 )
                {
                    if ( nSuppSizes[c0] + nSuppSizes[c1] + nSuppSizes[c2] <= 6 )
                        Vec_IntPush( vSupps, uSupps[c0] | uSupps[c1] | uSupps[c2] );
                    assert( nSuppSizes[c0] + nSuppSizes[c1] + nSuppSizes[c2] >= 6 );
                }
            }
        }
        if ( nSuppVars > 1 && nSuppVars <= 6 )
        {
            uSuppTemp = 0;
            for ( i = 0; i < nSuppVars; i++ )
                uSuppTemp |= uSuppVars[i];
            Vec_IntPush( vSupps, uSuppTemp );
        }
        else if ( nSuppVars > 6 && nSuppVars <= 12 )
        {
            uSuppTemp = 0;
            for ( i = 0; i < 6; i++ )
                uSuppTemp |= uSuppVars[i];
            Vec_IntPush( vSupps, uSuppTemp );

            uSuppTemp = 0;
            for ( i = 6; i < nSuppVars; i++ )
                uSuppTemp |= uSuppVars[i];
            Vec_IntPush( vSupps, uSuppTemp );
        }
    }
    else if ( pObj->Type == DAU_DSD_MUX || pObj->Type == DAU_DSD_PRIME )
    {
        Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
            uSupp |= Dss_ObjCheck666_rec( p, pFanin, vSupps );
    }
    if ( Dss_WordCountOnes( uSupp ) <= 6 )
        Vec_IntPush( vSupps, uSupp );
    return uSupp;
}
int Dss_ObjCheck666( Dss_Ntk_t * p )
{
    Vec_Int_t * vSupps;
    int i, k, SuppI, SuppK;
    int nSupp = Dss_ObjSuppSize(Dss_Regular(p->pRoot));
    if ( nSupp <= 6 )
        return 1;
    // compute supports
    vSupps = Vec_IntAlloc( 100 );
    Dss_ObjCheck666_rec( p, Dss_Regular(p->pRoot), vSupps );
    Vec_IntUniqify( vSupps );
    Vec_IntForEachEntry( vSupps, SuppI, i )
    {
        k = Dss_WordCountOnes(SuppI);
        assert( k > 0 && k <= 6 );
/*
        for ( k = 0; k < 16; k++ )
            if ( (SuppI >> k) & 1 )
                printf( "%c", 'a' + k );
            else
                printf( "-" );
        printf( "\n" );
*/
    }
    // consider support pairs
    Vec_IntForEachEntry( vSupps, SuppI, i )
    Vec_IntForEachEntryStart( vSupps, SuppK, k, i+1 )
    {
        if ( SuppI & SuppK )
            continue;
        if ( Dss_WordCountOnes(SuppI | SuppK) + 4 >= nSupp )
        {
            Vec_IntFree( vSupps );
            return 1;
        }
    }
    Vec_IntFree( vSupps );
    return 0;
}
void Dau_DsdTest_()
{
/*
    extern Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars, word * pTruth );
    extern void Dss_NtkFree( Dss_Ntk_t * p );

//    char * pDsd = "(!(amn!(bh))[cdeij]!(fklg)o)";
    char * pDsd = "<[(ab)(cd)(ef)][(gh)(ij)(kl)](mn)>";
    Dss_Ntk_t * pNtk = Dss_NtkCreate( pDsd, 16, NULL );
    int Status = Dss_ObjCheck666( pNtk );
    Dss_NtkFree( pNtk );
*/
}

abctime if_dec_time;

void Dau_DsdCheckStructOne( word * pTruth, int nVars, int nLeaves )
{
    extern Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars, word * pTruth );
    extern void Dss_NtkFree( Dss_Ntk_t * p );

    static abctime timeTt  = 0;
    static abctime timeDsd = 0;
    abctime clkTt, clkDsd;

    char pDsd[1000];
    word Truth[1024];
    Dss_Ntk_t * pNtk;
    int Status, nNonDec;

    if ( pTruth == NULL )
    {
        Abc_PrintTime( 1, "TT  runtime", timeTt );
        Abc_PrintTime( 1, "DSD runtime", timeDsd );
        Abc_PrintTime( 1, "Total      ", if_dec_time );

        if_dec_time = 0;
        timeTt = 0;
        timeDsd = 0;
        return;
    }

    Abc_TtCopy( Truth, pTruth, Abc_TtWordNum(nVars), 0 );
    nNonDec = Dau_DsdDecompose( Truth, nVars, 0, 0, pDsd );
    if ( nNonDec > 0 )
        return;

    pNtk = Dss_NtkCreate( pDsd, 16, NULL );

    // measure DSD runtime
    clkDsd = Abc_Clock();
    Status = Dss_ObjCheck666( pNtk );
    timeDsd += Abc_Clock() - clkDsd;

    Dss_NtkFree( pNtk );

    // measure TT runtime
    clkTt = Abc_Clock();
    {
        #define CLU_VAR_MAX  16

        // decomposition
        typedef struct If_Grp_t_ If_Grp_t;
        struct If_Grp_t_
        {
            char       nVars;
            char       nMyu;
            char       pVars[CLU_VAR_MAX];
        };


        int nLutLeaf  = 6;
        int nLutLeaf2 = 6;
        int nLutRoot  = 6;

        If_Grp_t G;
        If_Grp_t G2, R;
        word Func0, Func1, Func2;

        {
            extern If_Grp_t If_CluCheck3( void * p, word * pTruth0, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot, 
                          If_Grp_t * pR, If_Grp_t * pG2, word * pFunc0, word * pFunc1, word * pFunc2 );
            G = If_CluCheck3( NULL, pTruth, nLeaves, nLutLeaf, nLutLeaf2, nLutRoot, &R, &G2, &Func0, &Func1, &Func2 );
        }

    }
    timeTt += Abc_Clock() - clkTt;
}

#endif

 
/**Function*************************************************************

  Synopsis    [Elementary truth tables.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline word ** Dss_ManTtElems()
{
    static word TtElems[DAU_MAX_VAR+1][DAU_MAX_WORD], * pTtElems[DAU_MAX_VAR+1] = {NULL};
    if ( pTtElems[0] == NULL )
    {
        int v;
        for ( v = 0; v <= DAU_MAX_VAR; v++ )
            pTtElems[v] = TtElems[v];
        Abc_TtElemInit( pTtElems, DAU_MAX_VAR );
    }
    return pTtElems;
}

/**Function*************************************************************

  Synopsis    [Creating DSD network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Dss_Obj_t * Dss_ObjAllocNtk( Dss_Ntk_t * p, int Type, int nFans, int nTruthVars )
{
    Dss_Obj_t * pObj;
    pObj = (Dss_Obj_t *)(p->pMem + p->nMem);
    Dss_ObjClean( pObj );
    pObj->nFans  = nFans;
    pObj->nWords = Dss_ObjWordNum( nFans );
    pObj->Type   = Type;
    pObj->Id     = Vec_PtrSize( p->vObjs );
    pObj->iVar   = 31;
    Vec_PtrPush( p->vObjs, pObj );
    p->nMem += pObj->nWords + (nTruthVars ? Abc_TtWordNum(nTruthVars) : 0);
    assert( p->nMem < p->nMemAlloc );
    return pObj;
}
Dss_Obj_t * Dss_ObjCreateNtk( Dss_Ntk_t * p, int Type, Vec_Int_t * vFaninLits )
{
    Dss_Obj_t * pObj;
    int i, Entry;
    pObj = Dss_ObjAllocNtk( p, Type, Vec_IntSize(vFaninLits), Type == DAU_DSD_PRIME ? Vec_IntSize(vFaninLits) : 0 );
    Vec_IntForEachEntry( vFaninLits, Entry, i )
    {
        pObj->pFans[i] = Entry;
        pObj->nSupp += Dss_VecLitSuppSize(p->vObjs, Entry);
    }
    assert( i == (int)pObj->nFans );
    return pObj;
}
Dss_Ntk_t * Dss_NtkAlloc( int nVars )
{
    Dss_Ntk_t * p;
    Dss_Obj_t * pObj;
    int i;
    p = ABC_CALLOC( Dss_Ntk_t, 1 );
    p->nVars     = nVars;
    p->nMemAlloc = DAU_MAX_STR;
    p->pMem      = ABC_ALLOC( word, p->nMemAlloc );
    p->vObjs     = Vec_PtrAlloc( 100 );
    Dss_ObjAllocNtk( p, DAU_DSD_CONST0, 0, 0 );
    for ( i = 0; i < nVars; i++ )
    {
        pObj = Dss_ObjAllocNtk( p, DAU_DSD_VAR, 0, 0 );
        pObj->iVar = i;
        pObj->nSupp = 1;
    }
    return p;
}
void Dss_NtkFree( Dss_Ntk_t * p )
{
    Vec_PtrFree( p->vObjs );
    ABC_FREE( p->pMem );
    ABC_FREE( p );
}
void Dss_NtkPrint_rec( Dss_Ntk_t * p, Dss_Obj_t * pObj )
{
    char OpenType[7]  = {0, 0, 0, '(', '[', '<', '{'};
    char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'};
    Dss_Obj_t * pFanin;
    int i;
    assert( !Dss_IsComplement(pObj) );
    if ( pObj->Type == DAU_DSD_VAR )
        { printf( "%c", 'a' + pObj->iVar ); return; }
    if ( pObj->Type == DAU_DSD_PRIME )
        Abc_TtPrintHexRev( stdout, Dss_ObjTruth(pObj), pObj->nFans );
    printf( "%c", OpenType[pObj->Type] );
    Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
    {
        printf( "%s", Dss_ObjFaninC(pObj, i) ? "!":"" );
        Dss_NtkPrint_rec( p, pFanin );
    }
    printf( "%c", CloseType[pObj->Type] );
}
void Dss_NtkPrint( Dss_Ntk_t * p )
{
    if ( Dss_Regular(p->pRoot)->Type == DAU_DSD_CONST0 )
        printf( "%d", Dss_IsComplement(p->pRoot) );
    else
    {
        printf( "%s", Dss_IsComplement(p->pRoot) ? "!":"" );        
        if ( Dss_Regular(p->pRoot)->Type == DAU_DSD_VAR )
            printf( "%c", 'a' + Dss_Regular(p->pRoot)->iVar );
        else
            Dss_NtkPrint_rec( p, Dss_Regular(p->pRoot) );
    }
    printf( "\n" );
}

/**Function*************************************************************

  Synopsis    [Creating DSD network from SOP.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
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 );
}
int Dss_NtkCreate_rec( char * pStr, char ** p, int * pMatches, Dss_Ntk_t * pNtk, word * pTruth )
{
    int fCompl = 0;
    if ( **p == '!' )
    {
        fCompl = 1;
        (*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 Abc_Var2Lit( Dss_ObjId(Dss_VecVar(pNtk->vObjs, **p - 'a')), fCompl );
    if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
    {
        Dss_Obj_t * pObj;
        Vec_Int_t * vFaninLits = Vec_IntAlloc( 10 );
        char * q = pStr + pMatches[ *p - pStr ];
        int Type = 0;
        if ( **p == '(' )
            Type = DAU_DSD_AND;
        else if ( **p == '[' )
            Type = DAU_DSD_XOR;
        else if ( **p == '<' )
            Type = DAU_DSD_MUX;
        else if ( **p == '{' )
            Type = DAU_DSD_PRIME;
        else assert( 0 );
        assert( *q == **p + 1 + (**p != '(') );
        for ( (*p)++; *p < q; (*p)++ )
            Vec_IntPush( vFaninLits, Dss_NtkCreate_rec(pStr, p, pMatches, pNtk, pTruth) );
        assert( *p == q );
        if ( Type == DAU_DSD_PRIME )
        {
            Vec_Int_t * vFaninLitsNew;
            word pTemp[DAU_MAX_WORD];
            char pCanonPerm[DAU_MAX_VAR];
            int i, uCanonPhase, nFanins = Vec_IntSize(vFaninLits);
            Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nFanins), 0 );
            uCanonPhase = Abc_TtCanonicize( pTemp, nFanins, pCanonPerm );
            fCompl = (uCanonPhase >> nFanins) & 1;
            vFaninLitsNew = Vec_IntAlloc( nFanins );
            for ( i = 0; i < nFanins; i++ )
                Vec_IntPush( vFaninLitsNew, Abc_LitNotCond(Vec_IntEntry(vFaninLits, pCanonPerm[i]), (uCanonPhase>>i)&1) );
            pObj = Dss_ObjCreateNtk( pNtk, DAU_DSD_PRIME, vFaninLitsNew );
            Abc_TtCopy( Dss_ObjTruth(pObj), pTemp, Abc_TtWordNum(nFanins), 0 );
            Vec_IntFree( vFaninLitsNew );
        }
        else
            pObj = Dss_ObjCreateNtk( pNtk, Type, vFaninLits );
        Vec_IntFree( vFaninLits );
        return Abc_LitNotCond( Dss_Obj2Lit(pObj), fCompl );
    }
    assert( 0 );
    return -1;
}
Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars, word * pTruth )
{
    int fCompl = 0;
    Dss_Ntk_t * pNtk = Dss_NtkAlloc( nVars );
    if ( *pDsd == '!' )
         pDsd++, fCompl = 1;
    if ( Dau_DsdIsConst(pDsd) )
        pNtk->pRoot = Dss_VecConst0(pNtk->vObjs);
    else if ( Dau_DsdIsVar(pDsd) )
        pNtk->pRoot = Dss_VecVar(pNtk->vObjs, Dau_DsdReadVar(pDsd));
    else
    {
        int iLit, pMatches[DAU_MAX_STR];
        Dau_DsdMergeMatches( pDsd, pMatches );
        iLit = Dss_NtkCreate_rec( pDsd, &pDsd, pMatches, pNtk, pTruth );
        pNtk->pRoot = Dss_Lit2Obj( pNtk->vObjs, iLit );
    }
    if ( fCompl )
        pNtk->pRoot = Dss_Not(pNtk->pRoot);
    return pNtk;
}
 
/**Function*************************************************************

  Synopsis    [Comparing two DSD nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Dss_ObjCompare( Vec_Ptr_t * p, Dss_Obj_t * p0i, Dss_Obj_t * p1i )
{
    Dss_Obj_t * p0 = Dss_Regular(p0i);
    Dss_Obj_t * p1 = Dss_Regular(p1i);
    Dss_Obj_t * pChild0, * pChild1;
    int i, Res;
    if ( Dss_ObjType(p0) < Dss_ObjType(p1) )
        return -1;
    if ( Dss_ObjType(p0) > Dss_ObjType(p1) )
        return 1;
    if ( Dss_ObjType(p0) < DAU_DSD_AND )
        return 0;
    if ( Dss_ObjFaninNum(p0) < Dss_ObjFaninNum(p1) )
        return -1;
    if ( Dss_ObjFaninNum(p0) > Dss_ObjFaninNum(p1) )
        return 1;
    for ( i = 0; i < Dss_ObjFaninNum(p0); i++ )
    {
        pChild0 = Dss_ObjChild( p, p0, i );
        pChild1 = Dss_ObjChild( p, p1, i );
        Res = Dss_ObjCompare( p, pChild0, pChild1 );
        if ( Res != 0 )
            return Res;
    }
    if ( Dss_IsComplement(p0i) < Dss_IsComplement(p1i) )
        return -1;
    if ( Dss_IsComplement(p0i) > Dss_IsComplement(p1i) )
        return 1;
    return 0;
}
void Dss_ObjSort( Vec_Ptr_t * p, Dss_Obj_t ** pNodes, int nNodes, int * pPerm )
{
    int i, j, best_i;
    for ( i = 0; i < nNodes-1; i++ )
    {
        best_i = i;
        for ( j = i+1; j < nNodes; j++ )
            if ( Dss_ObjCompare(p, pNodes[best_i], pNodes[j]) == 1 )
                best_i = j;
        if ( i == best_i )
            continue;
        ABC_SWAP( Dss_Obj_t *, pNodes[i], pNodes[best_i] );
        if ( pPerm )
            ABC_SWAP( int, pPerm[i], pPerm[best_i] );
    }
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dss_NtkCheck( Dss_Ntk_t * p )
{
    Dss_Obj_t * pObj, * pFanin;
    int i, k;
    Dss_VecForEachNode( p->vObjs, pObj, i )
    {
        Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, k )
        {
            if ( pObj->Type == DAU_DSD_AND && pFanin->Type == DAU_DSD_AND )
                assert( Dss_ObjFaninC(pObj, k) );
            else if ( pObj->Type == DAU_DSD_XOR )
                assert( pFanin->Type != DAU_DSD_XOR );
            else if ( pObj->Type == DAU_DSD_MUX )
                assert( !Dss_ObjFaninC(pObj, 0) );
        }
    }
}
int Dss_NtkCollectPerm_rec( Dss_Ntk_t * p, Dss_Obj_t * pObj, int * pPermDsd, int * pnPerms )
{
    Dss_Obj_t * pChild;
    int k, fCompl = Dss_IsComplement(pObj);
    pObj = Dss_Regular( pObj );
    if ( pObj->Type == DAU_DSD_VAR )
    {
        pPermDsd[*pnPerms] = Abc_Var2Lit(pObj->iVar, fCompl);
        pObj->iVar = (*pnPerms)++;
        return fCompl;
    }
    Dss_ObjForEachChild( p->vObjs, pObj, pChild, k )
        if ( Dss_NtkCollectPerm_rec( p, pChild, pPermDsd, pnPerms ) )
            pObj->pFans[k] = (unsigned char)Abc_LitRegular((int)pObj->pFans[k]);
    return 0;
}
void Dss_NtkTransform( Dss_Ntk_t * p, int * pPermDsd )
{
    Dss_Obj_t * pChildren[DAU_MAX_VAR];
    Dss_Obj_t * pObj, * pChild;
    int i, k, nPerms;
    if ( Dss_Regular(p->pRoot)->Type == DAU_DSD_CONST0 )
        return;
    Dss_VecForEachNode( p->vObjs, pObj, i )
    {
        if ( pObj->Type == DAU_DSD_MUX || pObj->Type == DAU_DSD_PRIME )
            continue;
        Dss_ObjForEachChild( p->vObjs, pObj, pChild, k )
            pChildren[k] = pChild;
        Dss_ObjSort( p->vObjs, pChildren, Dss_ObjFaninNum(pObj), NULL );
        for ( k = 0; k < Dss_ObjFaninNum(pObj); k++ )
            pObj->pFans[k] = Dss_Obj2Lit( pChildren[k] );
    }
    nPerms = 0;
    if ( Dss_NtkCollectPerm_rec( p, p->pRoot, pPermDsd, &nPerms ) )
        p->pRoot = Dss_Regular(p->pRoot);
    assert( nPerms == (int)Dss_Regular(p->pRoot)->nSupp );
}


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Dss_Obj_t * Dss_ObjAlloc( Dss_Man_t * p, int Type, int nFans, int nTruthVars )
{
    int nWords = Dss_ObjWordNum(nFans) + (nTruthVars ? Abc_TtWordNum(nTruthVars) : 0);
    Dss_Obj_t * pObj = (Dss_Obj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords );
    Dss_ObjClean( pObj );
    pObj->Type   = Type;
    pObj->nFans  = nFans;
    pObj->nWords = Dss_ObjWordNum(nFans);
    pObj->Id     = Vec_PtrSize( p->vObjs );
    pObj->iVar   = 31;
    Vec_PtrPush( p->vObjs, pObj );
    Vec_IntPush( p->vNexts, 0 );
    return pObj;
}
Dss_Obj_t * Dss_ObjCreate( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
{
    Dss_Obj_t * pObj, * pFanin, * pPrev = NULL;
    int i, Entry;
    // check structural canonicity
    assert( Type != DAU_DSD_MUX || Vec_IntSize(vFaninLits) == 3 );
    assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(Vec_IntEntry(vFaninLits, 0)) );
    assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(Vec_IntEntry(vFaninLits, 1)) || !Abc_LitIsCompl(Vec_IntEntry(vFaninLits, 2)) );
    // check that leaves are in good order
    if ( Type == DAU_DSD_AND || Type == DAU_DSD_XOR )
    Dss_VecForEachObjVec( vFaninLits, p->vObjs, pFanin, i )
    {
        assert( Type != DAU_DSD_AND || Abc_LitIsCompl(Vec_IntEntry(vFaninLits, i)) || Dss_ObjType(pFanin) != DAU_DSD_AND );
        assert( Type != DAU_DSD_XOR || Dss_ObjType(pFanin) != DAU_DSD_XOR );
        assert( pPrev == NULL || Dss_ObjCompare(p->vObjs, pPrev, pFanin) <= 0 );
        pPrev = pFanin;
    }
    // create new node
    pObj = Dss_ObjAlloc( p, Type, Vec_IntSize(vFaninLits), Type == DAU_DSD_PRIME ? Vec_IntSize(vFaninLits) : 0 );
    if ( Type == DAU_DSD_PRIME )
        Abc_TtCopy( Dss_ObjTruth(pObj), pTruth, Abc_TtWordNum(Vec_IntSize(vFaninLits)), 0 );
    assert( pObj->nSupp == 0 );
    Vec_IntForEachEntry( vFaninLits, Entry, i )
    {
        pObj->pFans[i] = Entry;
        pObj->nSupp += Dss_VecLitSuppSize(p->vObjs, Entry);
    }
/*
    {
        extern void Dss_ManPrintOne( Dss_Man_t * p, int iDsdLit, int * pPermLits );
        Dss_ManPrintOne( p, Dss_Obj2Lit(pObj), NULL );
    }
*/
    return pObj;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dss_ManHashProfile( Dss_Man_t * p )
{
    Dss_Obj_t * pObj;
    unsigned * pSpot;
    int i, Counter;
    for ( i = 0; i < p->nBins; i++ )
    {
        Counter = 0;
        for ( pSpot = p->pBins + i; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(p->vNexts, pObj->Id), Counter++ )
             pObj = Dss_VecObj( p->vObjs, *pSpot );
        if ( Counter )
            printf( "%d ", Counter );
    }
    printf( "\n" );
}
static inline unsigned Dss_ObjHashKey( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
{
    static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
    int i, Entry;
    unsigned uHash = Type * 7873 + Vec_IntSize(vFaninLits) * 8147;
    Vec_IntForEachEntry( vFaninLits, Entry, i )
        uHash += Entry * s_Primes[i & 0x7];
    assert( (Type == DAU_DSD_PRIME) == (pTruth != NULL) );
    if ( pTruth )
    {
        unsigned char * pTruthC = (unsigned char *)pTruth;
        int nBytes = Abc_TtByteNum(Vec_IntSize(vFaninLits));
        for ( i = 0; i < nBytes; i++ )
            uHash += pTruthC[i] * s_Primes[i & 0x7];
    }
    return uHash % p->nBins;
}
unsigned * Dss_ObjHashLookup( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
{
    Dss_Obj_t * pObj;
    unsigned * pSpot = p->pBins + Dss_ObjHashKey(p, Type, vFaninLits, pTruth);
    for ( ; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(p->vNexts, pObj->Id) )
    {
        pObj = Dss_VecObj( p->vObjs, *pSpot );
        if ( (int)pObj->Type == Type && 
             (int)pObj->nFans == Vec_IntSize(vFaninLits) && 
             !memcmp(pObj->pFans, Vec_IntArray(vFaninLits), sizeof(int)*pObj->nFans) &&
             (pTruth == NULL || !memcmp(Dss_ObjTruth(pObj), pTruth, Abc_TtByteNum(pObj->nFans))) ) // equal
            return pSpot;
    }
    return pSpot;
}
Dss_Obj_t * Dss_ObjFindOrAdd( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
{
    Dss_Obj_t * pObj;
    unsigned * pSpot = Dss_ObjHashLookup( p, Type, vFaninLits, pTruth );
    if ( *pSpot )
        return Dss_VecObj( p->vObjs, *pSpot );
    *pSpot = Vec_PtrSize( p->vObjs );
    pObj = Dss_ObjCreate( p, Type, vFaninLits, pTruth );
    return pObj;
}

/**Function*************************************************************

  Synopsis    [Cache for decomposition calls.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dss_ManCacheAlloc( Dss_Man_t * p )
{
    assert( p->nCache == 0 );
    p->nCache = Abc_PrimeCudd( 100000 );
    p->pCache = ABC_CALLOC( Dss_Ent_t *, p->nCache );
}
void Dss_ManCacheFree( Dss_Man_t * p )
{
    if ( p->pCache == NULL )
        return;
    assert( p->nCache != 0 );
    p->nCache = 0;
    ABC_FREE( p->pCache );
}
static inline unsigned Dss_ManCacheHashKey( Dss_Man_t * p, Dss_Ent_t * pEnt )
{ 
    static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
    int i;
    unsigned uHash = pEnt->nShared * 7103 + pEnt->iDsd0 * 7873 + pEnt->iDsd1 * 8147;
    for ( i = 0; i < 2*(int)pEnt->nShared; i++ )
        uHash += pEnt->pShared[i] * s_Primes[i & 0x7];
    return uHash % p->nCache;
}
void Dss_ManCacheProfile( Dss_Man_t * p )
{
    Dss_Ent_t ** pSpot;
    int i, Counter;
    for ( i = 0; i < p->nCache; i++ )
    {
        Counter = 0;
        for ( pSpot = p->pCache + i; *pSpot; pSpot = &(*pSpot)->pNext, Counter++ )
            ;
        if ( Counter )
            printf( "%d ", Counter );
    }
    printf( "\n" );
}
Dss_Ent_t ** Dss_ManCacheLookup( Dss_Man_t * p, Dss_Ent_t * pEnt )
{
    Dss_Ent_t ** pSpot = p->pCache + Dss_ManCacheHashKey( p, pEnt );
    for ( ; *pSpot; pSpot = &(*pSpot)->pNext )
    {
        if ( (*pSpot)->iDsd0   == pEnt->iDsd0 && 
             (*pSpot)->iDsd1   == pEnt->iDsd1 && 
             (*pSpot)->nShared == pEnt->nShared && 
             !memcmp((*pSpot)->pShared, pEnt->pShared, sizeof(char)*2*pEnt->nShared)  ) // equal
        {
            p->nCacheHits[pEnt->nShared!=0]++;
            return pSpot;
        }
    }
    p->nCacheMisses[pEnt->nShared!=0]++;
    return pSpot;
}
Dss_Ent_t * Dss_ManCacheCreate( Dss_Man_t * p, Dss_Ent_t * pEnt0, Dss_Fun_t * pFun0 )
{
    Dss_Ent_t * pEnt = (Dss_Ent_t *)Mem_FlexEntryFetch( p->pMemEnts, sizeof(word) * pEnt0->nWords );
    Dss_Fun_t * pFun = (Dss_Fun_t *)Mem_FlexEntryFetch( p->pMemEnts, sizeof(word) * Dss_FunWordNum(pFun0) );
    memcpy( pEnt, pEnt0, sizeof(word) * pEnt0->nWords );
    memcpy( pFun, pFun0, sizeof(word) * Dss_FunWordNum(pFun0) );
    pEnt->pFunc = pFun;
    pEnt->pNext = NULL;
    p->nCacheEntries[pEnt->nShared!=0]++;
    return pEnt;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Dss_Man_t * Dss_ManAlloc( int nVars, int nNonDecLimit )
{
    Dss_Man_t * p;
    p = ABC_CALLOC( Dss_Man_t, 1 );
    p->nVars  = nVars;
    p->nNonDecLimit = nNonDecLimit;
    p->nBins  = Abc_PrimeCudd( 1000000 );
    p->pBins  = ABC_CALLOC( unsigned, p->nBins );
    p->pMem   = Mem_FlexStart();
    p->vObjs  = Vec_PtrAlloc( 10000 );
    p->vNexts = Vec_IntAlloc( 10000 );
    Dss_ObjAlloc( p, DAU_DSD_CONST0, 0, 0 );
    Dss_ObjAlloc( p, DAU_DSD_VAR, 0, 0 )->nSupp = 1;
    p->vLeaves = Vec_IntAlloc( 32 );
    p->vCopies = Vec_IntAlloc( 32 );
    p->pTtElems = Dss_ManTtElems();
    p->pMemEnts = Mem_FlexStart();
//    Dss_ManCacheAlloc( p );
    return p;
}
void Dss_ManFree( Dss_Man_t * p )
{
    Abc_PrintTime( 1, "Time begin ", p->timeBeg );
    Abc_PrintTime( 1, "Time decomp", p->timeDec );
    Abc_PrintTime( 1, "Time lookup", p->timeLook );
    Abc_PrintTime( 1, "Time end   ", p->timeEnd );

//    Dss_ManCacheProfile( p );
    Dss_ManCacheFree( p );
    Mem_FlexStop( p->pMemEnts, 0 );
    Vec_IntFreeP( &p->vCopies );
    Vec_IntFreeP( &p->vLeaves );
    Vec_IntFreeP( &p->vNexts );
    Vec_PtrFreeP( &p->vObjs );
    Mem_FlexStop( p->pMem, 0 );
    ABC_FREE( p->pBins );
    ABC_FREE( p );
}
void Dss_ManPrint_rec( FILE * pFile, Dss_Man_t * p, Dss_Obj_t * pObj, int * pPermLits, int * pnSupp )
{
    char OpenType[7]  = {0, 0, 0, '(', '[', '<', '{'};
    char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'};
    Dss_Obj_t * pFanin;
    int i;
    assert( !Dss_IsComplement(pObj) );
    if ( pObj->Type == DAU_DSD_CONST0 )
        { fprintf( pFile, "0" ); return; }
    if ( pObj->Type == DAU_DSD_VAR )
    {
        int iPermLit = pPermLits ? pPermLits[(*pnSupp)++] : Abc_Var2Lit((*pnSupp)++, 0);
        fprintf( pFile, "%s%c", Abc_LitIsCompl(iPermLit)? "!":"", 'a' + Abc_Lit2Var(iPermLit) );
        return;
    }
    if ( pObj->Type == DAU_DSD_PRIME )
        Abc_TtPrintHexRev( pFile, Dss_ObjTruth(pObj), pObj->nFans );
    fprintf( pFile, "%c", OpenType[pObj->Type] );
    Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
    {
        fprintf( pFile, "%s", Dss_ObjFaninC(pObj, i) ? "!":"" );
        Dss_ManPrint_rec( pFile, p, pFanin, pPermLits, pnSupp );
    }
    fprintf( pFile, "%c", CloseType[pObj->Type] );
}
void Dss_ManPrintOne( FILE * pFile, Dss_Man_t * p, int iDsdLit, int * pPermLits )
{
    int nSupp = 0;
    fprintf( pFile, "%6d : ", Abc_Lit2Var(iDsdLit) );
    fprintf( pFile, "%2d ",   Dss_VecLitSuppSize(p->vObjs, iDsdLit) );
    fprintf( pFile, "%s",     Abc_LitIsCompl(iDsdLit) ? "!" : ""  );
    Dss_ManPrint_rec( pFile, p, Dss_VecObj(p->vObjs, Abc_Lit2Var(iDsdLit)), pPermLits, &nSupp );
    fprintf( pFile, "\n" );
    assert( nSupp == (int)Dss_VecObj(p->vObjs, Abc_Lit2Var(iDsdLit))->nSupp );
}
int Dss_ManCheckNonDec_rec( Dss_Man_t * p, Dss_Obj_t * pObj )
{
    Dss_Obj_t * pFanin;
    int i;
    assert( !Dss_IsComplement(pObj) );
    if ( pObj->Type == DAU_DSD_CONST0 )
        return 0;
    if ( pObj->Type == DAU_DSD_VAR )
        return 0;
    if ( pObj->Type == DAU_DSD_PRIME )
        return 1;
    Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
        if ( Dss_ManCheckNonDec_rec( p, pFanin ) )
            return 1;
    return 0;
}
void Dss_ManDump( Dss_Man_t * p )
{
    char * pFileName = "dss_tts.txt";
    FILE * pFile;
    word Temp[DAU_MAX_WORD];
    Dss_Obj_t * pObj;
    int i;
    pFile = fopen( pFileName, "wb" );
    if ( pFile == NULL )
    {
        printf( "Cannot open file \"%s\".\n", pFileName );
        return;
    }
    Dss_VecForEachObj( p->vObjs, pObj, i )
    {
        if ( pObj->Type != DAU_DSD_PRIME )
            continue;
        Abc_TtCopy( Temp, Dss_ObjTruth(pObj), Abc_TtWordNum(pObj->nFans), 0 );
        Abc_TtStretch6( Temp, pObj->nFans, p->nVars );
        fprintf( pFile, "0x" );
        Abc_TtPrintHexRev( pFile, Temp, p->nVars );
        fprintf( pFile, "\n" );

//        printf( "%6d : ", i );
//        Abc_TtPrintHexRev( stdout, Temp, p->nVars );
//        printf( "    " );
//        Dau_DsdPrintFromTruth( stdout, Temp, p->nVars );
    }
    fclose( pFile );
}
void Dss_ManPrint( char * pFileName, Dss_Man_t * p )
{
    Dss_Obj_t * pObj;
    int CountNonDsd = 0, CountNonDsdStr = 0;
    int i, clk = Abc_Clock();
    FILE * pFile;
    pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
    if ( pFileName && pFile == NULL )
    {
        printf( "cannot open output file\n" );
        return;
    }
    Dss_VecForEachObj( p->vObjs, pObj, i )
    {
        CountNonDsd += (pObj->Type == DAU_DSD_PRIME);
        CountNonDsdStr += Dss_ManCheckNonDec_rec( p, pObj );
    }
    fprintf( pFile, "Total number of objects    = %8d\n", Vec_PtrSize(p->vObjs) );
    fprintf( pFile, "Non-DSD objects (max =%2d)  = %8d\n", p->nNonDecLimit, CountNonDsd );
    fprintf( pFile, "Non-DSD structures         = %8d\n", CountNonDsdStr );
    fprintf( pFile, "Memory used for objects    = %6.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
    fprintf( pFile, "Memory used for array      = %6.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) );
    fprintf( pFile, "Memory used for hash table = %6.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) );
    fprintf( pFile, "Memory used for cache      = %6.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMemEnts)/(1<<20) );
    fprintf( pFile, "Cache hits    = %8d %8d\n", p->nCacheHits[0],    p->nCacheHits[1] );
    fprintf( pFile, "Cache misses  = %8d %8d\n", p->nCacheMisses[0],  p->nCacheMisses[1] );
    fprintf( pFile, "Cache entries = %8d %8d\n", p->nCacheEntries[0], p->nCacheEntries[1] );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
//    Dss_ManHashProfile( p );
//    Dss_ManDump( p );
//    return;
    Dss_VecForEachObj( p->vObjs, pObj, i )
    {
        if ( i == 50 )
            break;
        Dss_ManPrintOne( pFile, p, Dss_Obj2Lit(pObj), NULL );
    }
    fprintf( pFile, "\n" );
    if ( pFileName )
        fclose( pFile );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dss_ManComputeTruth_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int nVars, word * pRes, int * pPermLits, int * pnSupp )
{
    Dss_Obj_t * pChild;
    int nWords = Abc_TtWordNum(nVars);
    int i, fCompl = Dss_IsComplement(pObj);
    pObj = Dss_Regular(pObj);
    if ( pObj->Type == DAU_DSD_VAR )
    {
        int iPermLit = pPermLits[(*pnSupp)++];
        assert( (*pnSupp) <= nVars );
        Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], nWords, fCompl ^ Abc_LitIsCompl(iPermLit) );
        return;
    }
    if ( pObj->Type == DAU_DSD_AND || pObj->Type == DAU_DSD_XOR )
    {
        word pTtTemp[DAU_MAX_WORD];
        if ( pObj->Type == DAU_DSD_AND )
            Abc_TtConst1( pRes, nWords );
        else
            Abc_TtConst0( pRes, nWords );
        Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
        {
            Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp, pPermLits, pnSupp );
            if ( pObj->Type == DAU_DSD_AND )
                Abc_TtAnd( pRes, pRes, pTtTemp, nWords, 0 );
            else
                Abc_TtXor( pRes, pRes, pTtTemp, nWords, 0 );
        }
        if ( fCompl ) Abc_TtNot( pRes, nWords );
        return;
    }
    if ( pObj->Type == DAU_DSD_MUX ) // mux
    {
        word pTtTemp[3][DAU_MAX_WORD];
        Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
            Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp[i], pPermLits, pnSupp );
        assert( i == 3 );
        Abc_TtMux( pRes, pTtTemp[0], pTtTemp[1], pTtTemp[2], nWords );
        if ( fCompl ) Abc_TtNot( pRes, nWords );
        return;
    }
    if ( pObj->Type == DAU_DSD_PRIME ) // function
    {
        word pFanins[DAU_MAX_VAR][DAU_MAX_WORD];
        Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
            Dss_ManComputeTruth_rec( p, pChild, nVars, pFanins[i], pPermLits, pnSupp );
        Dau_DsdTruthCompose_rec( Dss_ObjTruth(pObj), pFanins, pRes, pObj->nFans, nWords );
        if ( fCompl ) Abc_TtNot( pRes, nWords );
        return;
    }
    assert( 0 );

}
word * Dss_ManComputeTruth( Dss_Man_t * p, int iDsd, int nVars, int * pPermLits )
{
    Dss_Obj_t * pObj = Dss_Lit2Obj(p->vObjs, iDsd);
    word * pRes = p->pTtElems[DAU_MAX_VAR];
    int nWords = Abc_TtWordNum( nVars );
    int nSupp = 0;
    assert( nVars <= DAU_MAX_VAR );
    if ( iDsd == 0 )
        Abc_TtConst0( pRes, nWords );
    else if ( iDsd == 1 )
        Abc_TtConst1( pRes, nWords );
    else if ( Dss_Regular(pObj)->Type == DAU_DSD_VAR )
    {
        int iPermLit = pPermLits[nSupp++];
        Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], nWords, Abc_LitIsCompl(iDsd) ^ Abc_LitIsCompl(iPermLit) );
    }
    else
        Dss_ManComputeTruth_rec( p, pObj, nVars, pRes, pPermLits, &nSupp );
    assert( nSupp == (int)Dss_Regular(pObj)->nSupp );
    return pRes;
}


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
// returns literal of non-shifted tree in p, corresponding to pObj in pNtk, which may be compl
int Dss_NtkRebuild_rec( Dss_Man_t * p, Dss_Ntk_t * pNtk, Dss_Obj_t * pObj )
{
    Dss_Obj_t * pChildren[DAU_MAX_VAR];
    Dss_Obj_t * pChild, * pObjNew;
    int i, k, fCompl = Dss_IsComplement(pObj);
    pObj = Dss_Regular(pObj);
    if ( pObj->Type == DAU_DSD_VAR )
        return Abc_Var2Lit( 1, fCompl );
    Dss_ObjForEachChild( pNtk->vObjs, pObj, pChild, k )
    {
        pChildren[k] = Dss_Lit2Obj( p->vObjs, Dss_NtkRebuild_rec( p, pNtk, pChild ) );
        if ( pObj->Type == DAU_DSD_XOR && Dss_IsComplement(pChildren[k]) )
            pChildren[k] = Dss_Not(pChildren[k]), fCompl ^= 1;
    }
    // normalize MUX
    if ( pObj->Type == DAU_DSD_MUX )
    {
        if ( Dss_IsComplement(pChildren[0]) )
        {
            pChildren[0] = Dss_Not(pChildren[0]);
            ABC_SWAP( Dss_Obj_t *, pChildren[1], pChildren[2] );
        }
        if ( Dss_IsComplement(pChildren[1]) )
        {
            pChildren[1] = Dss_Not(pChildren[1]);
            pChildren[2] = Dss_Not(pChildren[2]);
            fCompl ^= 1;
        }
    }
    // shift subgraphs
    Vec_IntClear( p->vLeaves );
    for ( i = 0; i < k; i++ )
        Vec_IntPush( p->vLeaves, Dss_Obj2Lit(pChildren[i]) );
    // create new graph
    pObjNew = Dss_ObjFindOrAdd( p, pObj->Type, p->vLeaves, pObj->Type == DAU_DSD_PRIME ? Dss_ObjTruth(pObj) : NULL );
    return Abc_Var2Lit( pObjNew->Id, fCompl );
}
int Dss_NtkRebuild( Dss_Man_t * p, Dss_Ntk_t * pNtk )
{
    assert( p->nVars == pNtk->nVars );
    if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_CONST0 )
        return Dss_IsComplement(pNtk->pRoot);
    if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_VAR )
        return Abc_Var2Lit( Dss_Regular(pNtk->pRoot)->iVar + 1, Dss_IsComplement(pNtk->pRoot) );
    return Dss_NtkRebuild_rec( p, pNtk, pNtk->pRoot );
}

/**Function*************************************************************

  Synopsis    [Performs DSD operation on the two literals.]

  Description [Returns the perm of the resulting literals. The perm size 
  is equal to the number of support variables. The perm variables are 0-based
  numbers of pLits[0] followed by nLits[0]-based numbers of pLits[1].]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm, word * pTruth )
{
    Dss_Obj_t * pChildren[DAU_MAX_VAR];
    Dss_Obj_t * pObj, * pChild;
    int i, k, nChildren = 0, fCompl = 0, fComplFan;

    assert( Type == DAU_DSD_AND || pPerm == NULL );
    if ( Type == DAU_DSD_AND && pPerm != NULL )
    {
        int pBegEnd[DAU_MAX_VAR];
        int j, nSSize = 0;
        for ( k = 0; k < nLits; k++ )
        {
            pObj = Dss_Lit2Obj(p->vObjs, pLits[k]);
            if ( Dss_IsComplement(pObj) || pObj->Type != DAU_DSD_AND )
            {
                fComplFan = (Dss_Regular(pObj)->Type == DAU_DSD_VAR && Dss_IsComplement(pObj));
                if ( fComplFan )
                    pObj = Dss_Regular(pObj);
                pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + Dss_Regular(pObj)->nSupp);
                nSSize += Dss_Regular(pObj)->nSupp;
                pChildren[nChildren++] = pObj;
            }
            else
                Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
                {
                    fComplFan = (Dss_Regular(pChild)->Type == DAU_DSD_VAR && Dss_IsComplement(pChild));
                    if ( fComplFan )
                        pChild = Dss_Regular(pChild);
                    pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + Dss_Regular(pChild)->nSupp);
                    nSSize += Dss_Regular(pChild)->nSupp;
                    pChildren[nChildren++] = pChild;
                }
        }
        Dss_ObjSort( p->vObjs, pChildren, nChildren, pBegEnd );
        // create permutation
        for ( j = i = 0; i < nChildren; i++ )
            for ( k = (pBegEnd[i] >> 16); k < (pBegEnd[i] & 0xFF); k++ )
                pPerm[j++] = (unsigned char)Abc_Var2Lit( k, (pBegEnd[i] >> 8) & 1 );
        assert( j == nSSize );
    }
    else if ( Type == DAU_DSD_AND )
    {
        for ( k = 0; k < nLits; k++ )
        {
            pObj = Dss_Lit2Obj(p->vObjs, pLits[k]);
            if ( Dss_IsComplement(pObj) || pObj->Type != DAU_DSD_AND )
                pChildren[nChildren++] = pObj;
            else
                Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
                    pChildren[nChildren++] = pChild;
        }
        Dss_ObjSort( p->vObjs, pChildren, nChildren, NULL );
    }
    else if ( Type == DAU_DSD_XOR )
    {
        for ( k = 0; k < nLits; k++ )
        {
            fCompl ^= Abc_LitIsCompl(pLits[k]);
            pObj = Dss_Lit2Obj(p->vObjs, Abc_LitRegular(pLits[k]));
            if ( pObj->Type != DAU_DSD_XOR )
                pChildren[nChildren++] = pObj;
            else
                Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
                {
                    assert( !Dss_IsComplement(pChild) );
                    pChildren[nChildren++] = pChild;
                }
        }
        Dss_ObjSort( p->vObjs, pChildren, nChildren, NULL );
    }
    else if ( Type == DAU_DSD_MUX )
    {
        if ( Abc_LitIsCompl(pLits[0]) )
        {
            pLits[0] = Abc_LitNot(pLits[0]);
            ABC_SWAP( int, pLits[1], pLits[2] );
        }
        if ( Abc_LitIsCompl(pLits[1]) )
        {
            pLits[1] = Abc_LitNot(pLits[1]);
            pLits[2] = Abc_LitNot(pLits[2]);
            fCompl ^= 1;
        }
        for ( k = 0; k < nLits; k++ )
            pChildren[nChildren++] = Dss_Lit2Obj(p->vObjs, pLits[k]);
    }
    else if ( Type == DAU_DSD_PRIME )
    {
        for ( k = 0; k < nLits; k++ )
            pChildren[nChildren++] = Dss_Lit2Obj(p->vObjs, pLits[k]);
    }
    else assert( 0 );

    // shift subgraphs
    Vec_IntClear( p->vLeaves );
    for ( i = 0; i < nChildren; i++ )
        Vec_IntPush( p->vLeaves, Dss_Obj2Lit(pChildren[i]) );
    // create new graph
    pObj = Dss_ObjFindOrAdd( p, Type, p->vLeaves, pTruth );
    return Abc_Var2Lit( pObj->Id, fCompl );
}
Dss_Fun_t * Dss_ManOperationFun( Dss_Man_t * p, int * iDsd, int nFansTot )
{
    static char Buffer[100];
    Dss_Fun_t * pFun = (Dss_Fun_t *)Buffer;
    pFun->iDsd = Dss_ManOperation( p, DAU_DSD_AND, iDsd, 2, pFun->pFans, NULL );
//printf( "%d %d -> %d  ", iDsd[0], iDsd[1], pFun->iDsd );
    pFun->nFans = nFansTot;
    assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
    return pFun;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dss_EntPrint( Dss_Ent_t * p, Dss_Fun_t * pFun )
{
    int i;
    printf( "%d %d ", p->iDsd0, p->iDsd1 );
    for ( i = 0; i < (int)p->nShared; i++ )
        printf( "%d=%d ", p->pShared[2*i], p->pShared[2*i+1] );
    printf( "-> %d   ", pFun->iDsd );
}

/**Function*************************************************************

  Synopsis    [Performs AND on two DSD functions with support overlap.]

  Description [Returns the perm of the resulting literals. The perm size 
  is equal to the number of support variables. The perm variables are 0-based
  numbers of pLits[0] followed by nLits[0]-based numbers of pLits[1].]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Dss_Fun_t * Dss_ManBooleanAnd( Dss_Man_t * p, Dss_Ent_t * pEnt, int Counter )
{
    static char Buffer[100];
    Dss_Fun_t * pFun = (Dss_Fun_t *)Buffer;
    Dss_Ntk_t * pNtk;
    word * pTruthOne, pTruth[DAU_MAX_WORD];
    char pDsd[DAU_MAX_STR];
    int pMapDsd2Truth[DAU_MAX_VAR];
    int pPermLits[DAU_MAX_VAR];
    int pPermDsd[DAU_MAX_VAR];
    int i, nNonDec, nSuppSize = 0;
    int nFans[2];
    nFans[0] = Dss_VecLitSuppSize( p->vObjs, pEnt->iDsd0 );
    nFans[1] = Dss_VecLitSuppSize( p->vObjs, pEnt->iDsd1 );
    // create first truth table
    for ( i = 0; i < nFans[0]; i++ )
    {
        pMapDsd2Truth[nSuppSize] = i;
        pPermLits[i] = Abc_Var2Lit( nSuppSize++, 0 );
    }
    pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd0, p->nVars, pPermLits );
    Abc_TtCopy( pTruth, pTruthOne, Abc_TtWordNum(p->nVars), 0 );
if ( Counter )
{
//Kit_DsdPrintFromTruth( pTruthOne, p->nVars );  printf( "\n" );
}
    // create second truth table
    for ( i = 0; i < nFans[1]; i++ )
        pPermLits[i] = -1;
    for ( i = 0; i < (int)pEnt->nShared; i++ )
        pPermLits[pEnt->pShared[2*i+0]] = pEnt->pShared[2*i+1];
    for ( i = 0; i < nFans[1]; i++ )
        if ( pPermLits[i] == -1 )
        {
            pMapDsd2Truth[nSuppSize] = nFans[0] + i;
            pPermLits[i] = Abc_Var2Lit( nSuppSize++, 0 );
        }
    pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd1, p->nVars, pPermLits );
if ( Counter )
{
//Kit_DsdPrintFromTruth( pTruthOne, p->nVars );  printf( "\n" );
}
    Abc_TtAnd( pTruth, pTruth, pTruthOne, Abc_TtWordNum(p->nVars), 0 );
    // perform decomposition
    nNonDec = Dau_DsdDecompose( pTruth, nSuppSize, 0, 0, pDsd );
    if ( p->nNonDecLimit && nNonDec > p->nNonDecLimit )
        return NULL;
    // derive network and convert it into the manager
    pNtk = Dss_NtkCreate( pDsd, p->nVars, nNonDec ? pTruth : NULL );
//Dss_NtkPrint( pNtk );    
    Dss_NtkCheck( pNtk );
    Dss_NtkTransform( pNtk, pPermDsd );
//Dss_NtkPrint( pNtk );    
    pFun->iDsd = Dss_NtkRebuild( p, pNtk );
    Dss_NtkFree( pNtk );
    // pPermDsd maps vars of iDsdRes into literals of pTruth
    // translate this map into the one that maps vars of iDsdRes into literals of cut
    pFun->nFans = Dss_VecLitSuppSize( p->vObjs, pFun->iDsd );
    for ( i = 0; i < (int)pFun->nFans; i++ )
        pFun->pFans[i] = (unsigned char)Abc_Lit2LitV( pMapDsd2Truth, pPermDsd[i] );

//    Dss_EntPrint( pEnt, pFun );
    return pFun;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
// returns mapping of variables of dsd1 into literals of dsd0
Dss_Ent_t * Dss_ManSharedMap( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask )
{
    static char Buffer[100];
    Dss_Ent_t * pEnt = (Dss_Ent_t *)Buffer;
    pEnt->iDsd0 = iDsd[0];
    pEnt->iDsd1 = iDsd[1];
    pEnt->nShared = 0;
    if ( uSharedMask )
    {
        int i, g, pMapGtoL[DAU_MAX_VAR] = {-1};
        for ( i = 0; i < nFans[0]; i++ )
            pMapGtoL[ Abc_Lit2Var(pFans[0][i]) ] = Abc_Var2Lit( i, Abc_LitIsCompl(pFans[0][i]) );
        for ( i = 0; i < nFans[1]; i++ )
        {
            g = Abc_Lit2Var( pFans[1][i] );
            if ( (uSharedMask >> g) & 1 )
            {
                assert( pMapGtoL[g] >= 0 );
                pEnt->pShared[2*pEnt->nShared+0] = (unsigned char)i;
                pEnt->pShared[2*pEnt->nShared+1] = (unsigned char)Abc_LitNotCond( pMapGtoL[g], Abc_LitIsCompl(pFans[1][i]) );
                pEnt->nShared++;
            }
        }
    }
    pEnt->nWords = Dss_EntWordNum( pEnt );
    return pEnt;
}

// merge two DSD functions
int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask, int nKLutSize, unsigned char * pPermRes, word * pTruth )
{
    int fVerbose = 0;
    int fCheck = 0;
    static int Counter = 0;
//    word pTtTemp[DAU_MAX_WORD];
    word * pTruthOne;
    int pPermResInt[DAU_MAX_VAR];
    Dss_Ent_t * pEnt, ** ppSpot;
    Dss_Fun_t * pFun;
    int i;
    abctime clk;
    Counter++;
    if ( DAU_MAX_VAR < nKLutSize )
    {
        printf( "Paramater DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, nKLutSize );
        return -1;
    }
    assert( iDsd[0] <= iDsd[1] );

if ( fVerbose )
{
Dss_ManPrintOne( stdout, p, iDsd[0], pFans[0] );
Dss_ManPrintOne( stdout, p, iDsd[1], pFans[1] );
} 

    // constant argument
    if ( iDsd[0] == 0 ) return 0;
    if ( iDsd[0] == 1 ) return iDsd[1];
    if ( iDsd[1] == 0 ) return 0;
    if ( iDsd[1] == 1 ) return iDsd[0];

    // no overlap
clk = Abc_Clock();
    assert( nFans[0] == Dss_VecLitSuppSize(p->vObjs, iDsd[0]) );
    assert( nFans[1] == Dss_VecLitSuppSize(p->vObjs, iDsd[1]) );
    assert( nFans[0] + nFans[1] <= nKLutSize + Dss_WordCountOnes(uSharedMask) );
    // create map of shared variables
    pEnt = Dss_ManSharedMap( p, iDsd, nFans, pFans, uSharedMask );
p->timeBeg += Abc_Clock() - clk;
    // check cache
    if ( p->pCache == NULL )
    {
clk = Abc_Clock();
        if ( uSharedMask == 0 )
            pFun = Dss_ManOperationFun( p, iDsd, nFans[0] + nFans[1] );
        else
            pFun = Dss_ManBooleanAnd( p, pEnt, 0 );
        if ( pFun == NULL )
            return -1;
        assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
        assert( (int)pFun->nFans <= nKLutSize );
p->timeDec += Abc_Clock() - clk;
    }
    else
    {
clk = Abc_Clock();
        ppSpot = Dss_ManCacheLookup( p, pEnt );
p->timeLook += Abc_Clock() - clk;
clk = Abc_Clock();
        if ( *ppSpot == NULL )
        {
            if ( uSharedMask == 0 )
                pFun = Dss_ManOperationFun( p, iDsd, nFans[0] + nFans[1] );
            else
                pFun = Dss_ManBooleanAnd( p, pEnt, 0 );
            if ( pFun == NULL )
                return -1;
            assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
            assert( (int)pFun->nFans <= nKLutSize );
            // create cache entry
            *ppSpot = Dss_ManCacheCreate( p, pEnt, pFun );
        }
        pFun = (*ppSpot)->pFunc;
p->timeDec += Abc_Clock() - clk;
    }

clk = Abc_Clock();
    for ( i = 0; i < (int)pFun->nFans; i++ )
        if ( pFun->pFans[i] < 2 * nFans[0] ) // first dec
            pPermRes[i] = (unsigned char)Dss_Lit2Lit( pFans[0], pFun->pFans[i] );
        else
            pPermRes[i] = (unsigned char)Dss_Lit2Lit( pFans[1], pFun->pFans[i] - 2 * nFans[0] );
    // perform support minimization
    if ( uSharedMask && pFun->nFans > 1 )
    {
        int pVarPres[DAU_MAX_VAR];
        int nSupp = 0;
        for ( i = 0; i < p->nVars; i++ )
            pVarPres[i] = -1;
        for ( i = 0; i < (int)pFun->nFans; i++ )
            pVarPres[ Abc_Lit2Var(pPermRes[i]) ] = i;
        for ( i = 0; i < p->nVars; i++ )
            if ( pVarPres[i] >= 0 )
                pPermRes[pVarPres[i]] = Abc_Var2Lit( nSupp++, Abc_LitIsCompl(pPermRes[pVarPres[i]]) );
        assert( nSupp == (int)pFun->nFans );
    }

    for ( i = 0; i < (int)pFun->nFans; i++ )
        pPermResInt[i] = pPermRes[i];
p->timeEnd += Abc_Clock() - clk;

if ( fVerbose )
{
Dss_ManPrintOne( stdout, p, pFun->iDsd, pPermResInt );
printf( "\n" );
}

if ( Counter == 43418 )
{
//    int s = 0;
//    Dss_ManPrint( NULL, p );
}


    if ( fCheck )
    {
        pTruthOne = Dss_ManComputeTruth( p, pFun->iDsd, p->nVars, pPermResInt );
        if ( !Abc_TtEqual( pTruthOne, pTruth, Abc_TtWordNum(p->nVars) ) )
        {
            int s;
    //        Kit_DsdPrintFromTruth( pTruthOne, p->nVars );  printf( "\n" );
    //        Kit_DsdPrintFromTruth( pTruth, p->nVars );     printf( "\n" );
            printf( "Verification failed.\n" );
            s = 0;
        }
    }
    return pFun->iDsd;
}


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Dss_Ent_t * Dss_ManSharedMapDerive( Dss_Man_t * p, int iDsd0, int iDsd1, Vec_Str_t * vShared )
{
    static char Buffer[100];
    Dss_Ent_t * pEnt = (Dss_Ent_t *)Buffer;
    pEnt->iDsd0 = iDsd0;
    pEnt->iDsd1 = iDsd1;
    pEnt->nShared = Vec_StrSize(vShared)/2;
    memcpy( pEnt->pShared, (unsigned char *)Vec_StrArray(vShared), sizeof(char) * Vec_StrSize(vShared) );
    pEnt->nWords = Dss_EntWordNum( pEnt );
    return pEnt;
}

int Mpm_FuncCompute( Dss_Man_t * p, int iDsd0, int iDsd1, Vec_Str_t * vShared, int * pPerm, int * pnLeaves )
{
    int fVerbose = 0;
//    int fCheck = 0;
    Dss_Ent_t * pEnt, ** ppSpot;
    Dss_Fun_t * pFun;
    int iDsd[2] = { iDsd0, iDsd1 };
    int i;
    abctime clk;

    assert( iDsd0 <= iDsd1 );
    if ( DAU_MAX_VAR < *pnLeaves )
    {
        printf( "Paramater DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, *pnLeaves );
        return -1;
    }
    if ( fVerbose )
    {
        Dss_ManPrintOne( stdout, p, iDsd0, NULL );
        Dss_ManPrintOne( stdout, p, iDsd1, NULL );
    } 

clk = Abc_Clock();
    pEnt = Dss_ManSharedMapDerive( p, iDsd0, iDsd1, vShared );
    ppSpot = Dss_ManCacheLookup( p, pEnt );
p->timeLook += Abc_Clock() - clk;

clk = Abc_Clock();
    if ( *ppSpot == NULL )
    {
        if ( Vec_StrSize(vShared) == 0 )
            pFun = Dss_ManOperationFun( p, iDsd, *pnLeaves );
        else
            pFun = Dss_ManBooleanAnd( p, pEnt, 0 );
        if ( pFun == NULL )
            return -1;
        assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
        assert( (int)pFun->nFans <= *pnLeaves );
        // create cache entry
        *ppSpot = Dss_ManCacheCreate( p, pEnt, pFun );
    }
    pFun = (*ppSpot)->pFunc;
p->timeDec += Abc_Clock() - clk;

    *pnLeaves = (int)pFun->nFans;
    for ( i = 0; i < (int)pFun->nFans; i++ )
        pPerm[i] = (int)pFun->pFans[i];

    if ( fVerbose )
    {
        Dss_ManPrintOne( stdout, p, pFun->iDsd, NULL );
        printf( "\n" );
    }

/*
    if ( fCheck )
    {
        pTruthOne = Dss_ManComputeTruth( p, pFun->iDsd, p->nVars, pPermResInt );
        if ( !Abc_TtEqual( pTruthOne, pTruth, Abc_TtWordNum(p->nVars) ) )
        {
            int s;
    //        Kit_DsdPrintFromTruth( pTruthOne, p->nVars );  printf( "\n" );
    //        Kit_DsdPrintFromTruth( pTruth, p->nVars );     printf( "\n" );
            printf( "Verification failed.\n" );
            s = 0;
        }
    }
*/
    return pFun->iDsd;
}


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Dss_ObjCheckTransparent( Dss_Man_t * p, Dss_Obj_t * pObj )
{
    Dss_Obj_t * pFanin;
    int i;
    if ( pObj->Type == DAU_DSD_VAR )
        return 1;
    if ( pObj->Type == DAU_DSD_AND )
        return 0;
    if ( pObj->Type == DAU_DSD_XOR )
    {
        Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
            if ( Dss_ObjCheckTransparent( p, pFanin ) )
                return 1;
        return 0;
    }
    if ( pObj->Type == DAU_DSD_MUX )
    {
        pFanin = Dss_ObjFanin( p->vObjs, pObj, 1 );
        if ( !Dss_ObjCheckTransparent(p, pFanin) )
            return 0;
        pFanin = Dss_ObjFanin( p->vObjs, pObj, 2 );
        if ( !Dss_ObjCheckTransparent(p, pFanin) )
            return 0;
        return 1;
    }
    assert( pObj->Type == DAU_DSD_PRIME );
    return 0;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dau_DsdTest__()
{
    int nVars = 8;
//    char * pDsd = "[(ab)(cd)]";
    char * pDsd = "(!(a!(bh))[cde]!(fg))";
    Dss_Ntk_t * pNtk = Dss_NtkCreate( pDsd, nVars, NULL );
//    Dss_NtkPrint( pNtk );
//    Dss_NtkCheck( pNtk );
//    Dss_NtkTransform( pNtk );
//    Dss_NtkPrint( pNtk );
    Dss_NtkFree( pNtk );
    nVars = 0;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dau_DsdTest()
{
    int nVars = 8;
    Vec_Vec_t * vFuncs;
    Vec_Int_t * vOne, * vTwo, * vRes;//, * vThree;
    Dss_Man_t * p;
    int pEntries[3];
    int iLit, e0, e1;//, e2;
    int i, k, s;//, j;

    return;

    vFuncs = Vec_VecStart( nVars+1 );
    assert( nVars < DAU_MAX_VAR );
    p = Dss_ManAlloc( nVars, 0 );

    // init
    Vec_VecPushInt( vFuncs, 1, Dss_Obj2Lit(Dss_VecVar(p->vObjs,0)) );

    // enumerate
    for ( s = 2; s <= nVars; s++ )
    {
        vRes = Vec_VecEntryInt( vFuncs, s );
        for ( i = 1; i < s; i++ )
        for ( k = i; k < s; k++ )
        if ( i + k == s )
        {
            vOne = Vec_VecEntryInt( vFuncs, i );
            vTwo = Vec_VecEntryInt( vFuncs, k );
            Vec_IntForEachEntry( vOne, pEntries[0], e0 )
            Vec_IntForEachEntry( vTwo, pEntries[1], e1 )
            {
                int fAddInv0 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[0])) );
                int fAddInv1 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[1])) );

                iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
                assert( !Abc_LitIsCompl(iLit) );
                Vec_IntPush( vRes, iLit );

                if ( fAddInv0 )
                {
                    pEntries[0] = Abc_LitNot( pEntries[0] );
                    iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
                    pEntries[0] = Abc_LitNot( pEntries[0] );
                    assert( !Abc_LitIsCompl(iLit) );
                    Vec_IntPush( vRes, iLit );
                }

                if ( fAddInv1 )
                {
                    pEntries[1] = Abc_LitNot( pEntries[1] );
                    iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
                    pEntries[1] = Abc_LitNot( pEntries[1] );
                    assert( !Abc_LitIsCompl(iLit) );
                    Vec_IntPush( vRes, iLit );
                }

                if ( fAddInv0 && fAddInv1 )
                {
                    pEntries[0] = Abc_LitNot( pEntries[0] );
                    pEntries[1] = Abc_LitNot( pEntries[1] );
                    iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
                    pEntries[0] = Abc_LitNot( pEntries[0] );
                    pEntries[1] = Abc_LitNot( pEntries[1] );
                    assert( !Abc_LitIsCompl(iLit) );
                    Vec_IntPush( vRes, iLit );
                }

                iLit = Dss_ManOperation( p, DAU_DSD_XOR, pEntries, 2, NULL, NULL );
                assert( !Abc_LitIsCompl(iLit) );
                Vec_IntPush( vRes, Abc_LitRegular(iLit) );
            }
        }
/*
        for ( i = 1; i < s; i++ )
        for ( k = 1; k < s; k++ )
        for ( j = 1; j < s; j++ )
        if ( i + k + j == s )
        {
            vOne   = Vec_VecEntryInt( vFuncs, i );
            vTwo   = Vec_VecEntryInt( vFuncs, k );
            vThree = Vec_VecEntryInt( vFuncs, j );
            Vec_IntForEachEntry( vOne,   pEntries[0], e0 )
            Vec_IntForEachEntry( vTwo,   pEntries[1], e1 )
            Vec_IntForEachEntry( vThree, pEntries[2], e2 )
            {
                int fAddInv0 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[0])) );
                int fAddInv1 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[1])) );
                int fAddInv2 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[2])) );

                if ( !fAddInv0 && k > j )
                    continue;

                iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL );
                assert( !Abc_LitIsCompl(iLit) );
                Vec_IntPush( vRes, iLit );

                if ( fAddInv1 )
                {
                    pEntries[1] = Abc_LitNot( pEntries[1] );
                    iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL );
                    pEntries[1] = Abc_LitNot( pEntries[1] );
                    assert( !Abc_LitIsCompl(iLit) );
                    Vec_IntPush( vRes, iLit );
                }

                if ( fAddInv2 )
                {
                    pEntries[2] = Abc_LitNot( pEntries[2] );
                    iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL );
                    pEntries[2] = Abc_LitNot( pEntries[2] );
                    assert( !Abc_LitIsCompl(iLit) );
                    Vec_IntPush( vRes, iLit );
                }
            }
        }
*/
        Vec_IntUniqify( vRes );
    }
    Dss_ManPrint( "_npn/npn/dsdcanon.txt", p );

    Dss_ManFree( p );
    Vec_VecFree( vFuncs );
}


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dau_DsdTest444()
{
    Dss_Man_t * p = Dss_ManAlloc( 6, 0 );
    int iLit1[3] = { 2, 4 };
    int iLit2[3] = { 2, 4, 6 };
    int iRes[5];
    int nFans[2] = { 4, 3 };
    int pPermLits1[4] = { 0, 2, 5, 6 };
    int pPermLits2[5] = { 2, 9, 10 };
    int * pPermLits[2] = { pPermLits1, pPermLits2 };
    unsigned char pPermRes[6];
    int pPermResInt[6];
    unsigned uMaskShared = 2;
    int i;

    iRes[0] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iLit1, 2, NULL, NULL );
    iRes[1] = iRes[0]; 
    iRes[2] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iRes, 2, NULL, NULL );
    iRes[3] = Dss_ManOperation( p, DAU_DSD_AND, iLit2, 3, NULL, NULL );

    Dss_ManPrintOne( stdout, p, iRes[0], NULL );
    Dss_ManPrintOne( stdout, p, iRes[2], NULL );
    Dss_ManPrintOne( stdout, p, iRes[3], NULL );

    Dss_ManPrintOne( stdout, p, iRes[2], pPermLits1 );
    Dss_ManPrintOne( stdout, p, iRes[3], pPermLits2 );

    iRes[4] = Dss_ManMerge( p, iRes+2, nFans, pPermLits, uMaskShared, 6, pPermRes, NULL );

    for ( i = 0; i < 6; i++ )
        pPermResInt[i] = pPermRes[i];

    Dss_ManPrintOne( stdout, p, iRes[4], NULL );
    Dss_ManPrintOne( stdout, p, iRes[4], pPermResInt );

    Dss_ManFree( p );
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END