Updated functional enumation code.

src/base/abci/abc.c

@@ -45683,7 +45683,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-//    Gia_Man_t * pTemp = NULL;
+    Gia_Man_t * pTemp = NULL;
     int c, fVerbose = 0;
     int nFrames = 5;
     int fSwitch = 0;
@@ -45713,7 +45713,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern void Gia_ParTest( Gia_Man_t * p, int nWords, int nProcs );
 //    extern void Gia_ManTisTest( Gia_Man_t * pInit );
 //    extern void Gia_StoComputeCuts( Gia_Man_t * p );
-    extern void Abc_BddGiaTest( Gia_Man_t * pGia, int fVerbose );
+//    extern void Abc_BddGiaTest( Gia_Man_t * pGia, int fVerbose );
+    extern Gia_Man_t * Dau_ConstructAigFromFile( char * pFileName );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "WPFsvh" ) ) != EOF )
@@ -45765,11 +45766,11 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-    if ( pAbc->pGia == NULL )
+//    if ( pAbc->pGia == NULL )
-    {
+//    {
-        Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" );
+//        Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" );
-        return 1;
+//        return 1;
-    }
+//    }
 /*
     if ( pAbc->pCex == NULL )
     {
@@ -45831,6 +45832,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    pTemp = Slv_ManToAig( pAbc->pGia );
 //    Abc_FrameUpdateGia( pAbc, pTemp );
 //    Extra_TestGia2( pAbc->pGia );
+    pTemp = Dau_ConstructAigFromFile( "lib4var2.txt" );
+    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 usage:
     Abc_Print( -2, "usage: &test [-FW num] [-svh]\n" );

src/opt/dau/dauNpn2.c

@@ -1,26 +1,27 @@
 /**CFile****************************************************************
 
-  FileName    [dau.c]
+  FileName    [dauNpn2.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [DAG-aware unmapping.]
+  PackageName [Functional enumeration.]
 
-  Synopsis    []
+  Synopsis    [Functional enumeration.]
 
-  Author      [Alan Mishchenko]
+  Author      [Siang-Yun Lee]
   
-  Affiliation [UC Berkeley]
+  Affiliation [National Taiwan University]
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: dau.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  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
 
@@ -63,6 +64,239 @@ struct Dtt_Man_t_
 ///                     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    []
@@ -282,10 +516,23 @@ Vec_Int_t * Dtt_ManCollect( Dtt_Man_t * p, unsigned Truth, Vec_Int_t * vFuns )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Dtt_ManGetFun( Dtt_Man_t * p, unsigned tFun )
+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 );
+    //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 )
 {
@@ -313,13 +560,13 @@ void Dtt_ManAddFunction( Dtt_Man_t * p, int n, int FanI, int FanJ, int Type, uns
     Vec_IntForEachEntry( vFuncs, Min, i )
         Dtt_ManSetFun( p, Min );
     assert( nNodes < 32 );
-    p->Counts[nNodes]++;
+    p->Counts[nNodes]++;        
 
     if ( p->pTable == NULL )
         return;
     Truth = Truth & p->CmpMask ? ~Truth : Truth;
     Truth &= p->FunMask;
-    assert( p->pNodes[p->pTable[Truth]] == 0 );
+    //assert( p->pNodes[p->pTable[Truth]] == 0 );
     p->pNodes[p->pTable[Truth]] = n;
 }
 
@@ -397,7 +644,7 @@ void Dtt_PrintMulti1( Dtt_Man_t * p )
 }
 void Dtt_PrintMulti( Dtt_Man_t * p )
 {
-    int n, Counts[13][11] = {{0}};
+    int n, Counts[13][15] = {{0}};
     for ( n = 0; n < 13; n++ )
     {
         int i, Total = 0, Count = 0;
@@ -405,7 +652,7 @@ void Dtt_PrintMulti( Dtt_Man_t * p )
             if ( p->pNodes[i] == n )
             {
                 int Log = Abc_Base2Log(p->pTimes[i]);
-                assert( Log < 11 );
+                assert( Log < 15 );
                 if ( p->pTimes[i] < 2 )
                     Counts[n][0]++;
                 else
@@ -418,7 +665,7 @@ void Dtt_PrintMulti( Dtt_Man_t * p )
         printf( "n=%2d : ", n );
         printf( "All = %7d  ", Count );
         printf( "Ave = %6.2f  ", 1.0*Total/Count );
-        for ( i = 0; i < 11; i++ )
+        for ( i = 0; i < 15; i++ )
             if ( Counts[n][i] )
                 printf( "%6d", Counts[n][i] );
             else
@@ -426,10 +673,334 @@ void Dtt_PrintMulti( Dtt_Man_t * p )
         printf( "\n" );
     }
 }
-void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fMulti, int fVerbose )
+
+/**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]; 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]; 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 )
+{
+    FILE * pFile;
+    char FileName[100], 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
+    sprintf( FileName, "lib%dvar.txt", p->nVars );
+    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 )
+        {
+            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, int fDump )
 {
     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 );
@@ -466,15 +1037,15 @@ void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fMulti, int fVerb
                     unsigned Truth, TruthJ = Vec_IntEntry(p->vTruths, EntryJ);
                     Vec_IntForEachEntry( vFuns, Truth, k )
                     {
-                        if ( !Dtt_ManGetFun(p,  TruthJ &  Truth) )
+                        if ( !Dtt_ManGetFun(p,  TruthJ &  Truth, n) )
                             Dtt_ManAddFunction( p, n, EntryI, EntryJ, 0,  TruthJ &  Truth );
-                        if ( !Dtt_ManGetFun(p,  TruthJ & ~Truth) )
+                        if ( !Dtt_ManGetFun(p,  TruthJ & ~Truth, n) )
                             Dtt_ManAddFunction( p, n, EntryI, EntryJ, 1,  TruthJ & ~Truth );
-                        if ( !Dtt_ManGetFun(p, ~TruthJ &  Truth) )
+                        if ( !Dtt_ManGetFun(p, ~TruthJ &  Truth, n) )
                             Dtt_ManAddFunction( p, n, EntryI, EntryJ, 2, ~TruthJ &  Truth );
-                        if ( !Dtt_ManGetFun(p,  TruthJ |  Truth) )
+                        if ( !Dtt_ManGetFun(p,  TruthJ |  Truth, n) )
                             Dtt_ManAddFunction( p, n, EntryI, EntryJ, 3,  TruthJ |  Truth );
-                        if ( !Dtt_ManGetFun(p,  TruthJ ^  Truth) )
+                        if ( !Dtt_ManGetFun(p,  TruthJ ^  Truth, n) )
                             Dtt_ManAddFunction( p, n, EntryI, EntryJ, 4,  TruthJ ^  Truth );
                         nSteps += 5;
 
@@ -494,8 +1065,10 @@ void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fMulti, int fVerb
     }
     if ( fDelay )
         Dtt_PrintDistrib( p );
-    if ( p->pTable ) 
+    //if ( p->pTable ) 
-        Dtt_PrintMulti( p );
+        //Dtt_PrintMulti( p );
+    if ( !fDelay && fDump )
+        Dtt_DumpLibrary( p );
     Dtt_ManFree( p );
 }