dauNpn2.c

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

  FileName    [dauNpn2.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Functional enumeration.]

  Synopsis    [Functional enumeration.]

  Author      [Siang-Yun Lee]
  
  Affiliation [National Taiwan University]

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

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

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

#include "dauInt.h"
#include "misc/util/utilTruth.h"
#include "misc/extra/extra.h"
#include "aig/gia/gia.h"

ABC_NAMESPACE_IMPL_START

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

typedef struct Dtt_Man_t_ Dtt_Man_t;
struct Dtt_Man_t_
{
    int            nVars;          // variable number
    int            nPerms;         // number of permutations
    int            nComps;         // number of complementations
    int *          pPerms;         // permutations
    int *          pComps;         // complementations
    word *         pPres;          // function marks
    Vec_Int_t *    vFanins;        // node fanins
    Vec_Int_t *    vTruths;        // node truth tables
    Vec_Int_t *    vConfigs;       // configurations
    Vec_Int_t *    vClasses;       // node NPN classes
    Vec_Int_t *    vTruthNpns;     // truth tables of the classes
    Vec_Wec_t *    vFunNodes;      // nodes by NPN class
    Vec_Int_t *    vTemp;          // temporary
    Vec_Int_t *    vTemp2;         // temporary
    unsigned       FunMask;        // function mask
    unsigned       CmpMask;        // function mask
    unsigned       BinMask;        // hash mask
    unsigned *     pBins;          // hash bins
    Vec_Int_t *    vUsedBins;      // used bins
    int            Counts[32];     // node counts
    int            nClasses;       // count of classes
    unsigned *     pTable;         // mapping of funcs into their classes
    int *          pNodes;         // the number of nodes in min-node network
    int *          pTimes;         // the number of different min-node networks
    char *         pVisited;       // visited classes
    Vec_Int_t *    vVisited;       // the number of visited classes
};

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////
 
/**Function*************************************************************

  Synopsis    [Parse one formula into a truth table.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
char * Dau_ParseFormulaEndToken( char * pForm )
{
    int Counter = 0;
    char * pThis;
    for ( pThis = pForm; *pThis; pThis++ )
    {
        if ( *pThis == '~' )
            continue;
        if ( *pThis == '(' )
            Counter++;
        else if ( *pThis == ')' )
            Counter--;
        if ( Counter == 0 )
            return pThis + 1;
    }
    assert( 0 );
    return NULL;
}
word Dau_ParseFormula_rec( char * pBeg, char * pEnd )
{
    word iFans[2], Res, Oper = -1;
    char * pEndNew;
    int fCompl = 0;
    while ( pBeg[0] == '~' )
    {
        pBeg++;
        fCompl ^= 1;
    }
    if ( pBeg + 1 == pEnd )
    {
        if ( pBeg[0] >= 'a' && pBeg[0] <= 'f' )
            return fCompl ? ~s_Truths6[pBeg[0] - 'a'] : s_Truths6[pBeg[0] - 'a'];
        assert( 0 );
        return -1;
    }
    if ( pBeg[0] == '(' )
    {
        pEndNew = Dau_ParseFormulaEndToken( pBeg );
        if ( pEndNew == pEnd )
        {
            assert( pBeg[0] == '(' );
            assert( pBeg[pEnd-pBeg-1] == ')' );
            Res = Dau_ParseFormula_rec( pBeg + 1, pEnd - 1 );
            return fCompl ? ~Res : Res;
        }
    }
    // get first part
    pEndNew  = Dau_ParseFormulaEndToken( pBeg );
    iFans[0] = Dau_ParseFormula_rec( pBeg, pEndNew );
    iFans[0] = fCompl ? ~iFans[0] : iFans[0];
    Oper     = pEndNew[0];
    // get second part
    pBeg     = pEndNew + 1;
    pEndNew  = Dau_ParseFormulaEndToken( pBeg );
    iFans[1] = Dau_ParseFormula_rec( pBeg, pEndNew );
    // derive the formula
    if ( Oper == '&' )
        return iFans[0] & iFans[1];
    if ( Oper == '^' )
        return iFans[0] ^ iFans[1];
    assert( 0 );
    return -1;
}
word Dau_ParseFormula( char * p )
{
    return Dau_ParseFormula_rec( p, p + strlen(p) );
}
void Dau_ParseFormulaTest()
{
    char * p = "~((~~d&~(~~b&c))^(~(~a&~d)&~(~c^~b)))";
    word r = ABC_CONST(0x037d037d037d037d);
    word t = Dau_ParseFormula( p );
    assert( r == t );
}

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

  Synopsis    [Parse one formula into a AIG.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Dau_ParseFormulaAig_rec( Gia_Man_t * p, char * pBeg, char * pEnd )
{
    int iFans[2], Res, Oper = -1;
    char * pEndNew;
    int fCompl = 0;
    while ( pBeg[0] == '~' )
    {
        pBeg++;
        fCompl ^= 1;
    }
    if ( pBeg + 1 == pEnd )
    {
        if ( pBeg[0] >= 'a' && pBeg[0] <= 'f' )
            return Abc_Var2Lit( 1 + pBeg[0] - 'a', fCompl );
        assert( 0 );
        return -1;
    }
    if ( pBeg[0] == '(' )
    {
        pEndNew = Dau_ParseFormulaEndToken( pBeg );
        if ( pEndNew == pEnd )
        {
            assert( pBeg[0] == '(' );
            assert( pBeg[pEnd-pBeg-1] == ')' );
            Res = Dau_ParseFormulaAig_rec( p, pBeg + 1, pEnd - 1 );
            return Abc_LitNotCond( Res, fCompl );
        }
    }
    // get first part
    pEndNew  = Dau_ParseFormulaEndToken( pBeg );
    iFans[0] = Dau_ParseFormulaAig_rec( p, pBeg, pEndNew );
    iFans[0] = Abc_LitNotCond( iFans[0], fCompl );
    Oper     = pEndNew[0];
    // get second part
    pBeg     = pEndNew + 1;
    pEndNew  = Dau_ParseFormulaEndToken( pBeg );
    iFans[1] = Dau_ParseFormulaAig_rec( p, pBeg, pEndNew );
    // derive the formula
    if ( Oper == '&' )
        return Gia_ManHashAnd( p, iFans[0], iFans[1] );
    if ( Oper == '^' )
        return Gia_ManHashXor( p, iFans[0], iFans[1] );
    assert( 0 );
    return -1;
}
int Dau_ParseFormulaAig( Gia_Man_t * p, char * pStr )
{
    return Dau_ParseFormulaAig_rec( p, pStr, pStr + strlen(pStr) );
}
Gia_Man_t * Dau_ParseFormulaAigTest()
{
    int i;
    char * pStr = "~((~~d&~(~~b&c))^(~(~a&~d)&~(~c^~b)))";
    Gia_Man_t * p = Gia_ManStart( 1000 );
    p->pName = Abc_UtilStrsav( "func_enum_aig" );
    Gia_ManHashAlloc( p );
    for ( i = 0; i < 5; i++ )
        Gia_ManAppendCi( p );
    Gia_ManAppendCo( p, Dau_ParseFormulaAig(p, pStr) );
    return p;
}


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

  Synopsis    [Verify one file.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dau_VerifyFile( char * pFileName )
{
    char Buffer[1000];
    unsigned uTruth, uTruth2; 
    int nFails = 0, nLines = 0;
    FILE * pFile = fopen( pFileName, "rb" );
    while ( fgets( Buffer, 1000, pFile ) )
    {
        if ( Buffer[strlen(Buffer)-1] == '\n' )
            Buffer[strlen(Buffer)-1] = 0;
        if ( Buffer[strlen(Buffer)-1] == '\r' )
            Buffer[strlen(Buffer)-1] = 0;
        Extra_ReadHexadecimal( &uTruth2, Buffer, 5 );
        uTruth = (unsigned)Dau_ParseFormula( Buffer + 11 );
        if ( uTruth != uTruth2 )
            printf( "Verification failed in line %d:  %s\n", nLines, Buffer ), nFails++;
        nLines++;
    }
    printf( "Verification succeeded for %d functions and failed for %d functions.\n", nLines-nFails, nFails );
}
void Dau_VerifyFileTest()
{
    char * pFileName = "lib4var.txt";
    Dau_VerifyFile( pFileName );
}


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

  Synopsis    [Create AIG for one file.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Dau_ConstructAigFromFile( char * pFileName )
{
    char Buffer[1000];
    int i, nLines = 0;
    FILE * pFile = fopen( pFileName, "rb" );
    Gia_Man_t * p = Gia_ManStart( 1000 );
    p->pName = Abc_UtilStrsav( "func_enum_aig" );
    Gia_ManHashAlloc( p );
    for ( i = 0; i < 5; i++ )
        Gia_ManAppendCi( p );
    while ( fgets( Buffer, 1000, pFile ) )
    {
        if ( Buffer[strlen(Buffer)-1] == '\n' )
            Buffer[strlen(Buffer)-1] = 0;
        if ( Buffer[strlen(Buffer)-1] == '\r' )
            Buffer[strlen(Buffer)-1] = 0;
        Gia_ManAppendCo( p, Dau_ParseFormulaAig(p, Buffer + 11) );
        nLines++;
    }
    printf( "Finish constructing AIG for %d structures.\n", nLines );
    return p;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned * Dau_ReadFile2( char * pFileName, int nSizeW )
{
    abctime clk = Abc_Clock();
    unsigned * p;
    int RetValue;
    FILE * pFile = fopen( pFileName, "rb" );
    if (pFile == NULL) return NULL;
    p = (unsigned *)ABC_CALLOC(word, nSizeW);
    RetValue = pFile ? fread( p, sizeof(word), nSizeW, pFile ) : 0;
    RetValue = 0;
    if ( pFile )
    {
        printf( "Finished reading file \"%s\".\n", pFileName );
        fclose( pFile );
    }
    else
        printf( "Cannot open input file \"%s\".\n", pFileName );
    Abc_PrintTime( 1, "File reading", Abc_Clock() - clk );
    return p;
}
void Dtt_ManRenum( int nVars, unsigned * pTable, int * pnClasses )
{
    unsigned i, Limit = 1 << ((1 << nVars)-1), Count = 0;
    for ( i = 0; i < Limit; i++ )
        if ( pTable[i] == i )
            pTable[i] = Count++;
        else 
        {
            assert( pTable[i] < i );
            pTable[i] = pTable[pTable[i]];
        }
    printf( "The total number of NPN classes = %d.\n", Count );
    *pnClasses = Count;
}
unsigned * Dtt_ManLoadClasses( int nVars, int * pnClasses )
{
    extern void Dau_TruthEnum(int nVars);
    unsigned * pTable = NULL;
    int nSizeLog = (1<<nVars) -2;
    int nSizeW = 1 << nSizeLog;
    char pFileName[200];
    sprintf( pFileName, "tableW%d.data", nSizeLog );
    pTable = Dau_ReadFile2( pFileName, nSizeW );
    if (pTable == NULL)
    {
        Dau_TruthEnum(nVars);
        pTable = Dau_ReadFile2( pFileName, nSizeW );
    }
    Dtt_ManRenum( nVars, pTable, pnClasses );
    return pTable;
}
 
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dtt_ManAddVisited( Dtt_Man_t * p, unsigned Truth2, int n )
{
    unsigned Truth = Truth2 & p->CmpMask ? ~Truth2 : Truth2;
    unsigned Class = p->pTable[Truth & p->FunMask];
    assert( Class < (unsigned)p->nClasses );
    if ( p->pNodes[Class] < n )
        return;
    assert( p->pNodes[Class] == n );
    if ( p->pVisited[Class] )
        return;
    p->pVisited[Class] = 1;
    Vec_IntPush( p->vVisited, Class );
}
void Dtt_ManProcessVisited( Dtt_Man_t * p )
{
    int i, Class;
    Vec_IntForEachEntry( p->vVisited, Class, i )
    {
        assert( p->pVisited[Class] );
        p->pVisited[Class] = 0;
        p->pTimes[Class]++;
    }
    Vec_IntClear( p->vVisited );
}
 
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Dtt_Man_t * Dtt_ManAlloc( int nVars, int fMulti )
{
    Dtt_Man_t * p = ABC_CALLOC( Dtt_Man_t, 1 );
    p->nVars      = nVars;
    p->nPerms     = Extra_Factorial( nVars );
    p->nComps     = 1 << nVars;
    p->pPerms     = Extra_PermSchedule( nVars );
    p->pComps     = Extra_GreyCodeSchedule( nVars );
    p->pPres      = ABC_CALLOC( word, 1 << (p->nComps - 7) );
    p->vFanins    = Vec_IntAlloc( 2*617000 );
    p->vTruths    = Vec_IntAlloc( 617000 );
    p->vConfigs   = Vec_IntAlloc( 617000 );
    p->vClasses   = Vec_IntAlloc( 617000 );
    p->vTruthNpns = Vec_IntAlloc( 617000 );
    p->vFunNodes  = Vec_WecStart( 16 );
    p->vTemp      = Vec_IntAlloc( 4000 );
    p->vTemp2     = Vec_IntAlloc( 4000 );
    p->FunMask    = nVars == 5 ?      ~0 : (nVars == 4 ?  0xFFFF :   0xFF);
    p->CmpMask    = nVars == 5 ? 1 << 31 : (nVars == 4 ? 1 << 15 : 1 << 7);
    p->BinMask    = 0x3FFF;
    p->pBins      = ABC_FALLOC( unsigned, p->BinMask + 1 );
    p->vUsedBins  = Vec_IntAlloc( 4000 );
    if ( !fMulti ) return p;
    p->pTable     = Dtt_ManLoadClasses( p->nVars, &p->nClasses );
    p->pNodes     = ABC_CALLOC( int, p->nClasses );
    p->pTimes     = ABC_CALLOC( int, p->nClasses );
    p->pVisited   = ABC_CALLOC( char, p->nClasses );
    p->vVisited   = Vec_IntAlloc( 1000 );
    return p;
}
void Dtt_ManFree( Dtt_Man_t * p )
{
    Vec_IntFreeP( &p->vVisited );
    ABC_FREE( p->pTable );
    ABC_FREE( p->pNodes );
    ABC_FREE( p->pTimes );
    ABC_FREE( p->pVisited );
    Vec_IntFreeP( &p->vFanins );
    Vec_IntFreeP( &p->vTruths );
    Vec_IntFreeP( &p->vConfigs );
    Vec_IntFreeP( &p->vClasses );
    Vec_IntFreeP( &p->vTruthNpns );
    Vec_WecFreeP( &p->vFunNodes );
    Vec_IntFreeP( &p->vTemp );
    Vec_IntFreeP( &p->vTemp2 );
    Vec_IntFreeP( &p->vUsedBins );
    ABC_FREE( p->pPerms );
    ABC_FREE( p->pComps );
    ABC_FREE( p->pPres );
    ABC_FREE( p->pBins );
    ABC_FREE( p );
}

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

  Synopsis    [Collect representatives of the same class.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline unsigned Dtt_ManHashKey( Dtt_Man_t * p, unsigned Truth )
{
    static unsigned s_P[4] = { 1699, 5147, 7103, 8147 };
    unsigned char * pD = (unsigned char*)&Truth;
    return pD[0] * s_P[0] + pD[1] * s_P[1] + pD[2] * s_P[2] + pD[3] * s_P[3];
}
int Dtt_ManCheckHash( Dtt_Man_t * p, unsigned Truth )
{
    unsigned Hash = Dtt_ManHashKey(p, Truth);
    unsigned * pSpot = p->pBins + (Hash & p->BinMask);
    for ( ; ~*pSpot; Hash++, pSpot = p->pBins + (Hash & p->BinMask) )
        if ( *pSpot == Truth ) // equal
            return 0;
    Vec_IntPush( p->vUsedBins, pSpot - p->pBins );
    *pSpot = Truth;
    return 1;
}
Vec_Int_t * Dtt_ManCollect( Dtt_Man_t * p, unsigned Truth, Vec_Int_t * vFuns )
{
    int i, k, Entry;
    word tCur = ((word)Truth << 32) | (word)Truth;
    Vec_IntClear( vFuns );
    for ( i = 0; i < p->nPerms; i++ )
    {
        for ( k = 0; k < p->nComps; k++ )
        {
//            unsigned tTemp = (unsigned)(tCur & 1 ? ~tCur : tCur);
            unsigned tTemp = (unsigned)(tCur & p->CmpMask ? ~tCur : tCur);
            if ( Dtt_ManCheckHash( p, tTemp ) )
                Vec_IntPush( vFuns, tTemp );
            tCur = Abc_Tt6Flip( tCur, p->pComps[k] );
        }
        tCur = Abc_Tt6SwapAdjacent( tCur, p->pPerms[i] );
    }
    assert( tCur == (((word)Truth << 32) | (word)Truth) );
    // clean hash table
    Vec_IntForEachEntry( p->vUsedBins, Entry, i )
        p->pBins[Entry] = ~0;
    Vec_IntClear( p->vUsedBins );
    //printf( "%d ", Vec_IntSize(vFuns) );
    return vFuns;
}
 
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Dtt_ManGetFun( Dtt_Man_t * p, unsigned tFun, int n )
{
    unsigned Class;
    tFun = tFun & p->CmpMask ? ~tFun : tFun;
    //return Abc_TtGetBit( p->pPres, tFun & p->FunMask );
    if ( !Abc_TtGetBit( p->pPres, tFun & p->FunMask ) ) return 0;
    if ( p->pTable == NULL ) return 1;

    Class = p->pTable[tFun & p->FunMask];
    assert( Class < (unsigned)p->nClasses );
    if ( p->pNodes[Class] < n )
        return 1;
    assert( p->pNodes[Class] == n );
    if ( p->pVisited[Class] )
        return 1;
    
    return 0;
}
static inline void Dtt_ManSetFun( Dtt_Man_t * p, unsigned tFun )
{
    tFun = tFun & p->CmpMask ? ~tFun : tFun;
    //assert( !Dtt_ManGetFun(p, fFun & p->FunMask );
    Abc_TtSetBit( p->pPres, tFun & p->FunMask );
}
void Dtt_ManAddFunction( Dtt_Man_t * p, int n, int FanI, int FanJ, int Type, unsigned Truth )
{
    Vec_Int_t * vFuncs = Dtt_ManCollect( p, Truth, p->vTemp2 );
    unsigned Min = Vec_IntFindMin( vFuncs ); 
    int i, nObjs = Vec_IntSize(p->vFanins)/2;
    int nNodesI = 0xF & (Vec_IntEntry(p->vConfigs, FanI) >> 3);
    int nNodesJ = 0xF & (Vec_IntEntry(p->vConfigs, FanJ) >> 3);
    int nNodes  = nNodesI + nNodesJ + 1;
    assert( nObjs == Vec_IntSize(p->vTruths) );
    assert( nObjs == Vec_IntSize(p->vConfigs) );
    assert( nObjs == Vec_IntSize(p->vClasses) );
    Vec_WecPush( p->vFunNodes, n, nObjs );
    Vec_IntPushTwo( p->vFanins, FanI, FanJ );
    Vec_IntPush( p->vTruths, Truth );
    Vec_IntPush( p->vConfigs, (nNodes << 3) | Type );
    Vec_IntPush( p->vClasses, Vec_IntSize(p->vTruthNpns) );
    Vec_IntPush( p->vTruthNpns, Min );
    Vec_IntForEachEntry( vFuncs, Min, i )
        Dtt_ManSetFun( p, Min );
    assert( nNodes < 32 );
    p->Counts[nNodes]++;        

    if ( p->pTable == NULL )
        return;
    Truth = Truth & p->CmpMask ? ~Truth : Truth;
    Truth &= p->FunMask;
    //assert( p->pNodes[p->pTable[Truth]] == 0 );
    p->pNodes[p->pTable[Truth]] = n;
}

int Dtt_PrintStats( int nNodes, int nVars, Vec_Wec_t * vFunNodes, word nSteps, abctime clk, int fDelay, word nMultis )
{
    int nNew = Vec_IntSize(Vec_WecEntry(vFunNodes, nNodes));
    printf("%c =%2d  |  ",     fDelay ? 'D':'N', nNodes );
    printf("C =%12.0f  |  ",   (double)(iword)nSteps );
    printf("New%d =%10d   ",   nVars, nNew + (int)(nNodes==0) );
    printf("All%d =%10d  |  ", nVars, Vec_WecSizeSize(vFunNodes)+1 );
    printf("Multi =%10d  |  ", (int)nMultis );
    Abc_PrintTime( 1, "Time",  Abc_Clock() - clk );
    //Abc_Print(1, "%9.2f sec\n", 1.0*(Abc_Clock() - clk)/(CLOCKS_PER_SEC));
    fflush(stdout);
    return nNew;
}
void Dtt_PrintDistrib( Dtt_Man_t * p )
{
    int i;
    printf( "NPN classes for each node count (N):\n" );
    for ( i = 0; i < 32; i++ )
        if ( p->Counts[i] )
            printf( "N = %2d : NPN = %6d\n", i, p->Counts[i] );
}
void Dtt_PrintMulti2( Dtt_Man_t * p )
{
    int i, n;
    for ( n = 0; n <= 7; n++ )
    {
        printf( "n=%d : ", n);
        for ( i = 0; i < p->nClasses; i++ )
            if ( p->pNodes[i] == n )
                printf( "%d ", p->pTimes[i] );
        printf( "\n" );
    }
}
void Dtt_PrintMulti1( Dtt_Man_t * p )
{
    int i, n, Entry, Count, Prev;
    for ( n = 0; n < 16; n++ )
    {
        Vec_Int_t * vTimes = Vec_IntAlloc( 100 );
        Vec_Int_t * vUsed  = Vec_IntAlloc( 100 );
        for ( i = 0; i < p->nClasses; i++ )
            if ( p->pNodes[i] == n )
                Vec_IntPush( vTimes, p->pTimes[i] );
        if ( Vec_IntSize(vTimes) == 0 )
        {
            Vec_IntFree(vTimes);
            Vec_IntFree(vUsed);
            break;
        }
        Vec_IntSort( vTimes, 0 );
        Count = 1;
        Prev = Vec_IntEntry( vTimes, 0 );
        Vec_IntForEachEntryStart( vTimes, Entry, i, 1 )
            if ( Prev == Entry )
                Count++;
            else
            {
                assert( Prev < Entry );
                Vec_IntPushTwo( vUsed, Prev, Count );
                Count = 1;
                Prev = Entry;
            }
        if ( Count > 0 )
            Vec_IntPushTwo( vUsed, Prev, Count );
        printf( "n=%d : ", n);
        Vec_IntForEachEntryDouble( vUsed, Prev, Entry, i )
            printf( "%d=%d ", Prev, Entry );
        printf( "\n" );
        Vec_IntFree( vTimes );
        Vec_IntFree( vUsed );
    }
}
void Dtt_PrintMulti( Dtt_Man_t * p )
{
    int n, Counts[13][15] = {{0}};
    for ( n = 0; n < 13; n++ )
    {
        int i, Total = 0, Count = 0;
        for ( i = 0; i < p->nClasses; i++ )
            if ( p->pNodes[i] == n )
            {
                int Log = Abc_Base2Log(p->pTimes[i]);
                assert( Log < 15 );
                if ( p->pTimes[i] < 2 )
                    Counts[n][0]++;
                else
                    Counts[n][Log]++;
                Total += p->pTimes[i];
                Count++;
            }
        if ( Count == 0 )
            break;
        printf( "n=%2d : ", n );
        printf( "All = %7d  ", Count );
        printf( "Ave = %6.2f  ", 1.0*Total/Count );
        for ( i = 0; i < 15; i++ )
            if ( Counts[n][i] )
                printf( "%6d", Counts[n][i] );
            else
                printf( "%6s", "" );
        printf( "\n" );
    }
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
typedef struct Dtt_FunImpl_t_ Dtt_FunImpl_t;
struct Dtt_FunImpl_t_
{
    int Type;
    int NP1;     // 4 bits for an input (NPPP)
    int FI1;     // the id (in vLibFun) of the first fanin function
    int NP2;
    int FI2;     // the id (in vLibFun) of the second fanin function
};

void Dtt_FunImplFI2Str( int FI, int NP, Vec_Int_t* vLibFun, char* str )
{
    int i, P[5], N[5];
    for ( i = 0; i < 5; i++ )
    {
        P[i] = NP & 0x7;
        NP = NP >> 3;
        N[i] = NP & 0x1;
        NP = NP >> 1 ;
    }
    sprintf( str, "[%08x(%03d),%d%d%d%d%d,%d%d%d%d%d]", Vec_IntEntry( vLibFun, FI ), FI, P[0], P[1], P[2], P[3], P[4], N[0], N[1], N[2], N[3], N[4] ); 
}

void Dtt_FunImpl2Str( int Type, char* sFI1, char* sFI2, char* str )
{
    // 0: 1&2, 1: ~1&2, 2: 1&~2, 3: 1|2 = ~(~1&~2), 4: 1^2
    // 5: ~(1&2), 6: ~(~1&2), 7: ~(1&~2), 8: ~1&~2, 9: ~(1^2)
    switch( Type )
    {
        case 0: sprintf( str, "(%s&%s)", sFI1, sFI2 ); break;
        case 1: sprintf( str, "(~%s&%s)", sFI1, sFI2 ); break;
        case 2: sprintf( str, "(%s&~%s)", sFI1, sFI2 ); break;
        case 3: sprintf( str, "~(~%s&~%s)", sFI1, sFI2 ); break;
        case 4: sprintf( str, "(%s^%s)", sFI1, sFI2 ); break;
        case 5: sprintf( str, "~(%s&%s)", sFI1, sFI2 ); break;
        case 6: sprintf( str, "~(~%s&%s)", sFI1, sFI2 ); break;
        case 7: sprintf( str, "~(%s&~%s)", sFI1, sFI2 ); break;
        case 8: sprintf( str, "(~%s&~%s)", sFI1, sFI2 ); break;
        case 9: sprintf( str, "~(%s^%s)", sFI1, sFI2 ); break;
        /*case 0: sprintf( str, " ( %s& %s)", sFI1, sFI2 ); break;
        case 1: sprintf( str, " (~%s& %s)", sFI1, sFI2 ); break;
        case 2: sprintf( str, " ( %s&~%s)", sFI1, sFI2 ); break;
        case 3: sprintf( str, "~(~%s&~%s)", sFI1, sFI2 ); break;
        case 4: sprintf( str, " ( %s^ %s)", sFI1, sFI2 ); break;
        case 5: sprintf( str, "~( %s& %s)", sFI1, sFI2 ); break;
        case 6: sprintf( str, "~(~%s& %s)", sFI1, sFI2 ); break;
        case 7: sprintf( str, "~( %s&~%s)", sFI1, sFI2 ); break;
        case 8: sprintf( str, " (~%s&~%s)", sFI1, sFI2 ); break;
        case 9: sprintf( str, "~( %s^ %s)", sFI1, sFI2 ); break;*/
    }
}

int Dtt_ComposeNP( int NP1, int NP2 )
{
    // NP[i] = NP1[NP2[i]]
    int NP = 0, i;
    for ( i = 0; i < 5; i++ )
    {
        NP |= ( ( NP1 >> ((NP2&0x7)<<2) ) & 0x7 ) << (i<<2); // P'[i] = P1[P2[i]]
        NP |= ( ( NP1 >> ((NP2&0x7)<<2) ^ NP2 ) & 0x8 ) << (i<<2); // N'[i] = N1[P2[i]] ^ N2[i]
        NP2 = NP2 >> 4;
    }
    return NP; 
}

void Dtt_MakePI( int NP, char* str )
{
    // apply P'[i], find the i s.t. P'[i]==0, correspond to N'[i]
    int i;
    for ( i = 0; i < 5; i++ )
    {
        if ( ( NP & 0x7 ) == 0 )
        {
            if ( NP & 0x8 ) 
                sprintf( str, "~%c", 'a'+i );
            else
                sprintf( str, "%c", 'a'+i );
            return;
        }
        NP = NP >> 4;
    }
    assert(0);
}

void Dtt_MakeFormula( unsigned tFun, Dtt_FunImpl_t* pFun, Vec_Vec_t* vLibImpl, int NP, char* sF, int fPrint, FILE* pFile );
void Dtt_MakeFormulaFI2( unsigned tFun, Dtt_FunImpl_t* pFun, Vec_Vec_t* vLibImpl, int NP, char* sFI1, char* sF, int fPrint, FILE* pFile )
{
    int j;
    Dtt_FunImpl_t* pImpl2;
    char sFI2[100] = {0}; //sprintf( sFI2, "" );

    if ( pFun->FI2 == 0 ) // PI
    {
        Dtt_MakePI( Dtt_ComposeNP( pFun->NP2, NP ), sFI2 );
        Dtt_FunImpl2Str( pFun->Type, sFI1, sFI2, sF );
        if (fPrint)
            fprintf(pFile, "%08x = %s\n", tFun, sF);
    }
    else
    {
        Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pImpl2, j, pFun->FI2 )
        {
            Dtt_MakeFormula( tFun, pImpl2, vLibImpl, Dtt_ComposeNP( pFun->NP2, NP ), sFI2, 0, pFile );
            Dtt_FunImpl2Str( pFun->Type, sFI1, sFI2, sF );
            if (fPrint)
                fprintf(pFile, "%08x = %s\n", tFun, sF);
        }
    }   
}

void Dtt_MakeFormula( unsigned tFun, Dtt_FunImpl_t* pFun, Vec_Vec_t* vLibImpl, int NP, char* sF, int fPrint, FILE* pFile )
{
    int j;
    Dtt_FunImpl_t* pImpl1;
    char sFI1[100], sCopy[100] = {0}; //sprintf( sFI1, "" );

    if ( pFun->FI1 == 0 ) // PI
    {
        Dtt_MakePI( Dtt_ComposeNP( pFun->NP1, NP ), sFI1 );
        sprintf( sCopy, "%s", sF );
        Dtt_MakeFormulaFI2( tFun, pFun, vLibImpl, NP, sFI1, sF, fPrint, pFile );
    }
    else
    {
        Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pImpl1, j, pFun->FI1 )
        {
            Dtt_MakeFormula( tFun, pImpl1, vLibImpl, Dtt_ComposeNP( pFun->NP1, NP ), sFI1, 0, pFile );
            sprintf( sCopy, "%s", sF );
            Dtt_MakeFormulaFI2( tFun, pFun, vLibImpl, NP, sFI1, sF, fPrint, pFile );
        }
    }
}

void Dtt_ProcessType( int* Type, int nFanin )
{
    // 0: 1&2, 1: ~1&2, 2: 1&~2, 3: 1|2 = ~(~1&~2), 4: 1^2
    // 5: ~(1&2), 6: ~(~1&2), 7: ~(1&~2), 8: ~1&~2, 9: ~(1^2)
    if ( nFanin == 3 ) // for output negation
        *Type += (*Type<5)? 5: -5;
    else if ( *Type == 0 || *Type == 5 )
        *Type += nFanin;
    else if ( *Type == nFanin ) // 1,1 ; 2,2
        *Type = 0;
    else if ( *Type + nFanin == 3 ) // 1,2 ; 2,1
        *Type = 8;
    else if ( *Type == 3 )
        *Type = (nFanin==1)? 7: 6;
    else if ( *Type == 4 )
        *Type = 9;
    else if ( *Type == nFanin+5 ) // 6,1 ; 7,2
        *Type = 5;
    else if ( *Type + nFanin == 8 ) // 6,2 ; 7,1
        *Type = 3;
    else if ( *Type == 8 )
        *Type = (nFanin==1)? 2: 1;
    else if ( *Type == 9 )
        *Type = 4;
    else
        assert( 0 );
}

int Dtt_Check( unsigned tFun, unsigned tGoal, unsigned tCur, int* pType )
{
    if (!tGoal) //for Fanin2 and output
        return ( tCur == tFun || ~tCur == tFun );
    //for Fanin1: check if tFun(Type)tCur==tGoal
    switch (*pType)
    {
    // 0: 1&2, 1: ~1&2, 2: 1&~2, 3: 1|2 = ~(~1&~2), 4: 1^2
    // 5: ~(1&2), 6: ~(~1&2), 7: ~(1&~2), 8: ~1&~2, 9: ~(1^2)
        case 0: case 5: if ( (~tCur & tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; }
                else return ( (tCur & tFun) == tGoal );
        case 1: case 6: if ( (tCur & tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; }
                else return ( (~tCur & tFun) == tGoal );
        case 2: case 7: if ( (~tCur & ~tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; }
                else return ( (tCur & ~tFun) == tGoal );
        case 3: case 8: if ( (~tCur | tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; }
                else return ( (tCur | tFun) == tGoal );
        case 4: case 9: if ( (~tCur ^ tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; }
                else return ( (tCur ^ tFun) == tGoal );
        default: assert(0);
    }
    return -1;
}

void Dtt_FindNP( Dtt_Man_t * p, unsigned tFun, unsigned tGoal, unsigned tNpn, int * NP, int* pType, int NPout )
{
    int i, k, j;
    int P[5] = { 0, 1, 2, 3, 4 };
    int N[5] = { 0, 0, 0, 0, 0 };
    int temp;
    
    word tCur = ((word)tNpn << 32) | (word)tNpn;
    for ( i = 0; i < p->nPerms; i++ )
    {
        for ( k = 0; k < p->nComps; k++ )
        {
            if ( Dtt_Check( tFun, tGoal, (unsigned)tCur, pType ))
            {
                if ( !tGoal && ( tFun == (unsigned)~tCur ) ) // !tGoal: not FI1
                {
                    if (!NPout) Dtt_ProcessType( pType, 3 );
                    else Dtt_ProcessType( pType, 2 );
                }
                *NP = 0;
                if (!NPout)
                {
                    for ( j = 0; j < 5; j++ )
                        *NP |= ( ( ( N[j] & 0x1 ) << 3 ) | ( P[j] & 0x7 ) ) << (j<<2) ;
                }
                else
                {
                    for ( j = 0; j < 5; j++ )
                    {
                        *NP |= P[NPout&0x7] << (j<<2); // P'[j] = P[Pout[j]]
                        *NP |= ( N[NPout&0x7] ^ ( (NPout>>3) & 0x1 )) << (j<<2) << 3; // N'[i] = N1[P2[i]] ^ N2[i]
                        NPout = NPout >> 4;
                    }
                }
                
                return;
            }
            tCur = Abc_Tt6Flip( tCur, p->pComps[k] );
            N[p->pComps[k]] ^= 0x1;
        }
        tCur = Abc_Tt6SwapAdjacent( tCur, p->pPerms[i] );
        temp = P[p->pPerms[i]]; P[p->pPerms[i]] = P[p->pPerms[i]+1]; P[p->pPerms[i]+1] = temp;
    }
    assert(0);
}

void Dtt_DumpLibrary( Dtt_Man_t * p, char* FileName )
{
    FILE * pFile;
    char str[100], sFI1[50], sFI2[50];
    int i, j, Entry, fRepeat;
    Dtt_FunImpl_t * pFun, * pFun2;
    Vec_Int_t * vLibFun = Vec_IntDup( p->vTruthNpns );  // none-duplicating vector of NPN representitives
    Vec_Vec_t * vLibImpl;
    Vec_IntUniqify( vLibFun );
    vLibImpl = Vec_VecStart( Vec_IntSize( vLibFun ) );
    Vec_IntForEachEntry( p->vTruths, Entry, i )
    {
        int NP, Fanin2, Fanin1Npn, Fanin2Npn;
        if (i<2) continue; // skip const 0
        pFun = ABC_CALLOC( Dtt_FunImpl_t, 1 );
        pFun->Type = (int)( 0x7 & Vec_IntEntry(p->vConfigs, i) );
        //word Fanin1 = Vec_IntEntry( p->vTruths, Vec_IntEntry( p->vFanins, i*2 ) );
        Fanin2 = Vec_IntEntry( p->vTruths, Vec_IntEntry( p->vFanins, i*2+1 ) );
        Fanin1Npn = Vec_IntEntry( p->vTruthNpns, Vec_IntEntry( p->vFanins, i*2 ) );
        Fanin2Npn = Vec_IntEntry( p->vTruthNpns, Vec_IntEntry( p->vFanins, i*2+1 ) );
        pFun->FI1 = Vec_IntFind( vLibFun, Fanin1Npn );
        pFun->FI2 = Vec_IntFind( vLibFun, Fanin2Npn );
        
        fRepeat = 0;
        Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pFun2, j, Vec_IntFind( vLibFun, Vec_IntEntry( p->vTruthNpns, i ) ) )
        {
            if ( ( pFun2->FI1 == pFun->FI1 && pFun2->FI2 == pFun->FI2 ) || ( pFun2->FI2 == pFun->FI1 && pFun2->FI1 == pFun->FI2 ) )
            {
                fRepeat = 1;
                break;
            }
        }
        if (fRepeat) 
        {
            ABC_FREE( pFun );
            continue;
        }

        Dtt_FindNP( p, Vec_IntEntry( p->vTruthNpns, i ), 0, Entry, &NP, &(pFun->Type), 0 ); //out: tGoal=0, NPout=0
        Dtt_FindNP( p, Fanin2, Entry, Fanin1Npn, &(pFun->NP1), &(pFun->Type), NP ); //FI1
        Dtt_FindNP( p, Fanin2, 0, Fanin2Npn, &(pFun->NP2), &(pFun->Type), NP ); //FI2: tGoal=0
        
        Vec_VecPush( vLibImpl, Vec_IntFind( vLibFun, Vec_IntEntry( p->vTruthNpns, i ) ), pFun );
    }

    // print to file
    pFile = fopen( FileName, "wb" );

    if (0)
    Vec_IntForEachEntry( vLibFun, Entry, i )
    {
        if (!Entry) continue; // skip const 0
        fprintf( pFile, "%08x: ", (unsigned)Entry );
        Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pFun, j, i )
        {
            Dtt_FunImplFI2Str( pFun->FI1, pFun->NP1, vLibFun, sFI1 ); 
            Dtt_FunImplFI2Str( pFun->FI2, pFun->NP2, vLibFun, sFI2 );
            Dtt_FunImpl2Str( pFun->Type, sFI1, sFI2, str );
            fprintf( pFile, "%s, ", str );
        }
        fprintf( pFile, "\n" );
    }

    // formula format
    Vec_IntForEachEntry( vLibFun, Entry, i )
    {
        if ( i<2 ) continue; // skip const 0 and buffer
        Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pFun, j, i )
        {
            str[0] = 0; //sprintf( str, "" );
            Dtt_MakeFormula( (unsigned)Entry, pFun, vLibImpl, (4<<16)+(3<<12)+(2<<8)+(1<<4), str, 1, pFile );
        }
    }

    fclose( pFile );
    printf( "Dumped file \"%s\". \n", FileName );
    fflush( stdout );
}

void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fMulti, int fVerbose, char* pFileName )
{
    abctime clk = Abc_Clock(); word nSteps = 0, nMultis = 0;
    Dtt_Man_t * p = Dtt_ManAlloc( nVars, fMulti ); int n, i, j;

    // constant zero class
    Vec_IntPushTwo( p->vFanins, 0, 0 );
    Vec_IntPush( p->vTruths, 0 );
    Vec_IntPush( p->vConfigs, 0 );
    Vec_IntPush( p->vClasses, Vec_IntSize(p->vTruthNpns) );
    Vec_IntPush( p->vTruthNpns, 0 );
    Dtt_ManSetFun( p, 0 );
    // buffer class
    Vec_WecPush( p->vFunNodes, 0, Vec_IntSize(p->vFanins)/2 );
    Vec_IntPushTwo( p->vFanins, 0, 0 );
    Vec_IntPush( p->vTruths, (unsigned)s_Truths6[0] );
    Vec_IntPush( p->vConfigs, 0 );
    Vec_IntPush( p->vClasses, Vec_IntSize(p->vTruthNpns) );
    Vec_IntPush( p->vTruthNpns, (unsigned)s_Truths6[0] );
    for ( i = 0; i < nVars; i++ )
        Dtt_ManSetFun( p, (unsigned)s_Truths6[i] );
    p->Counts[0] = 2;
    // enumerate
    Dtt_PrintStats(0, nVars, p->vFunNodes, nSteps, clk, fDelay, 0);
    for ( n = 1; n <= nNodeMax; n++ )
    {
        for ( i = 0, j = n - 1; i < n; i++, j = j - 1 + fDelay ) if ( i <= j )
        {
            Vec_Int_t * vFaninI = Vec_WecEntry( p->vFunNodes, i );
            Vec_Int_t * vFaninJ = Vec_WecEntry( p->vFunNodes, j );
            int k, i0, j0, EntryI, EntryJ;
            Vec_IntForEachEntry( vFaninI, EntryI, i0 )
            {
                unsigned TruthI = Vec_IntEntry(p->vTruths, EntryI);
                Vec_Int_t * vFuns = Dtt_ManCollect( p, TruthI, p->vTemp );
                int Start = i == j ? i0 : 0;
                Vec_IntForEachEntryStart( vFaninJ, EntryJ, j0, Start )
                {
                    unsigned Truth, TruthJ = Vec_IntEntry(p->vTruths, EntryJ);
                    Vec_IntForEachEntry( vFuns, Truth, k )
                    {
                        if ( !Dtt_ManGetFun(p,  TruthJ &  Truth, n) )
                            Dtt_ManAddFunction( p, n, EntryI, EntryJ, 0,  TruthJ &  Truth );
                        if ( !Dtt_ManGetFun(p,  TruthJ & ~Truth, n) )
                            Dtt_ManAddFunction( p, n, EntryI, EntryJ, 1,  TruthJ & ~Truth );
                        if ( !Dtt_ManGetFun(p, ~TruthJ &  Truth, n) )
                            Dtt_ManAddFunction( p, n, EntryI, EntryJ, 2, ~TruthJ &  Truth );
                        if ( !Dtt_ManGetFun(p,  TruthJ |  Truth, n) )
                            Dtt_ManAddFunction( p, n, EntryI, EntryJ, 3,  TruthJ |  Truth );
                        if ( !Dtt_ManGetFun(p,  TruthJ ^  Truth, n) )
                            Dtt_ManAddFunction( p, n, EntryI, EntryJ, 4,  TruthJ ^  Truth );
                        nSteps += 5;

                        if ( p->pTable ) Dtt_ManAddVisited( p,  TruthJ &  Truth, n );
                        if ( p->pTable ) Dtt_ManAddVisited( p,  TruthJ & ~Truth, n );
                        if ( p->pTable ) Dtt_ManAddVisited( p, ~TruthJ &  Truth, n );
                        if ( p->pTable ) Dtt_ManAddVisited( p,  TruthJ |  Truth, n );
                        if ( p->pTable ) Dtt_ManAddVisited( p,  TruthJ ^  Truth, n );
                    }
                    nMultis++;
                    if ( p->pTable ) Dtt_ManProcessVisited( p );
                }
            }
        }
        if ( Dtt_PrintStats(n, nVars, p->vFunNodes, nSteps, clk, fDelay, nMultis) == 0 )
            break;
    }
    if ( fDelay )
        Dtt_PrintDistrib( p );
    //if ( p->pTable ) 
        //Dtt_PrintMulti( p );
    if ( !fDelay && pFileName!=NULL )
        Dtt_DumpLibrary( p, pFileName );
    Dtt_ManFree( p );
}

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

ABC_NAMESPACE_IMPL_END