Changes to LUT mappers.

5 files changed, 247 insertions, 163 deletions

diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c
index 0e737adc..04dfb719 100644
--- a/src/aig/gia/giaJf.c
+++ b/src/aig/gia/giaJf.c
@@ -371,16 +371,7 @@ Jf_Man_t * Jf_ManAlloc( Gia_Man_t * pGia, Jf_Par_t * pPars )
     p->pGia      = pGia;
     p->pPars     = pPars;
     if ( pPars->fCutMin && !pPars->fFuncDsd )
-    {
-        word uTruth[JF_WORD_MAX]; 
-        int Value, nWords = Abc_Truth6WordNum(pPars->nLutSize);
-        p->vTtMem = Vec_MemAlloc( nWords, 12 ); // 32 KB/page for 6-var functions
-        Vec_MemHashAlloc( p->vTtMem, 10000 );
-        memset( uTruth, 0x00, sizeof(word) * nWords );
-        Value = Vec_MemHashInsert( p->vTtMem, uTruth ); assert( Value == 0 );
-        memset( uTruth, 0xAA, sizeof(word) * nWords );
-        Value = Vec_MemHashInsert( p->vTtMem, uTruth ); assert( Value == 1 );
-    }
+        p->vTtMem = Vec_MemAllocForTT( pPars->nLutSize );
     else if ( pPars->fCutMin && pPars->fFuncDsd )
     {
         p->pDsd = Sdm_ManRead();
@@ -401,18 +392,6 @@ Jf_Man_t * Jf_ManAlloc( Gia_Man_t * pGia, Jf_Par_t * pPars )
     p->clkStart  = Abc_Clock();
     return p;
 }
-void Jf_ManDumpTruthTables( Jf_Man_t * p )
-{
-    char pFileName[1000];
-    FILE * pFile;
-    sprintf( pFileName, "tt_%s_%02d.txt", Gia_ManName(p->pGia), p->pPars->nLutSize );
-    pFile = fopen( pFileName, "wb" );
-    Vec_MemDump( pFile, p->vTtMem );
-    fclose( pFile );
-    printf( "Dumped %d %d-var truth tables into file \"%s\" (%.2f MB).\n", 
-        Vec_MemEntryNum(p->vTtMem), p->pPars->nLutSize, pFileName,
-        17.0 * Vec_MemEntryNum(p->vTtMem) / (1 << 20) );
-}
 void Jf_ManFree( Jf_Man_t * p )
 {
     if ( p->pPars->fVerbose && p->pDsd )
@@ -1748,7 +1727,7 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
         Jf_ManPropagateEla( p, 1 );                 Jf_ManPrintStats( p, "Edge " );
     }
     if ( p->pPars->fVeryVerbose && p->pPars->fCutMin && !p->pPars->fFuncDsd )
-        Jf_ManDumpTruthTables( p );
+        Vec_MemDumpTruthTables( p->vTtMem, Gia_ManName(p->pGia), p->pPars->nLutSize );
     if ( p->pPars->fPureAig )
         pNew = Jf_ManDeriveGia(p);
     else if ( p->pPars->fCutMin )
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 205ff9e3..37728fcb 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -515,6 +515,7 @@ extern int             If_CluCheckExt3( void * p, word * pTruth, int nVars, int
                            char * pLut0, char * pLut1, char * pLut2, word * pFunc0, word * pFunc1, word * pFunc2 );
 /*=== ifDsd.c =============================================================*/
 extern If_DsdMan_t *   If_DsdManAlloc( int nLutSize );
+extern void            If_DsdManDump( If_DsdMan_t * p );
 extern void            If_DsdManPrint( If_DsdMan_t * p, char * pFileName );
 extern void            If_DsdManFree( If_DsdMan_t * p );
 extern int             If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm );
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index 502c6000..923e188a 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -43,11 +43,8 @@ struct If_DsdObj_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       nSupp   :  5;   // variable
+    unsigned       Count   : 19;   // variable
     unsigned       nFans   :  5;   // fanin count
     unsigned       pFans[0];       // fanins
 };
@@ -92,6 +89,8 @@ static inline If_DsdObj_t * If_DsdVecConst0( Vec_Ptr_t * p )
 static inline If_DsdObj_t * If_DsdVecVar( Vec_Ptr_t * p, int v )                       { return If_DsdVecObj( p, v+1 );                                                     }
 static inline int           If_DsdVecObjSuppSize( Vec_Ptr_t * p, int iObj )            { return If_DsdVecObj( p, iObj )->nSupp;                                             }
 static inline int           If_DsdVecLitSuppSize( Vec_Ptr_t * p, int iLit )            { return If_DsdVecObjSuppSize( p, Abc_Lit2Var(iLit) );                               }
+static inline int           If_DsdVecObjRef( Vec_Ptr_t * p, int iObj )                 { return If_DsdVecObj( p, iObj )->Count;                                             }
+static inline void          If_DsdVecObjIncRef( Vec_Ptr_t * p, int iObj )              { if ( If_DsdVecObjRef(p, iObj) < 0x7FFFF ) If_DsdVecObj( p, iObj )->Count++;        }
 static inline If_DsdObj_t * If_DsdObjFanin( Vec_Ptr_t * p, If_DsdObj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return If_DsdVecObj(p, Abc_Lit2Var(pObj->pFans[i])); }
 
 #define If_DsdVecForEachObj( vVec, pObj, i )                \
@@ -106,6 +105,7 @@ static inline If_DsdObj_t * If_DsdObjFanin( Vec_Ptr_t * p, If_DsdObj_t * pObj, i
 #define If_DsdObjForEachFaninLit( vVec, pObj, iLit, i )      \
     for ( i = 0; (i < If_DsdObjFaninNum(pObj)) && ((iLit) = If_DsdObjFaninLit(pObj, i)); i++ )
 
+extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -184,9 +184,8 @@ If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans )
     If_DsdObjClean( pObj );
     pObj->Type   = Type;
     pObj->nFans  = nFans;
-    pObj->nWords = nWords;
     pObj->Id     = Vec_PtrSize( p->vObjs );
-    pObj->iVar   = 31;
+    pObj->Count  = 0;
     Vec_PtrPush( p->vObjs, pObj );
     Vec_IntPush( p->vNexts, 0 );
     return pObj;
@@ -275,6 +274,9 @@ If_DsdMan_t * If_DsdManAlloc( int nVars )
 void If_DsdManFree( If_DsdMan_t * p )
 {
     int fVerbose = 0;
+//    If_DsdManDump( p );
+    If_DsdManPrint( p, NULL );
+    Vec_MemDumpTruthTables( p->vTtMem, NULL, p->nVars );
     if ( fVerbose )
     {
         Abc_PrintTime( 1, "Time begin ", p->timeBeg );
@@ -292,7 +294,23 @@ void If_DsdManFree( If_DsdMan_t * p )
     ABC_FREE( p->pBins );
     ABC_FREE( p );
 }
-void If_DsdManPrint_rec( FILE * pFile, If_DsdMan_t * p, int iDsdLit, int * pPermLits, int * pnSupp )
+int If_DsdManCheckNonDec_rec( If_DsdMan_t * p, int Id )
+{
+    If_DsdObj_t * pObj;
+    int i, iFanin;
+    pObj = If_DsdVecObj( p->vObjs, Id );
+    if ( If_DsdObjType(pObj) == IF_DSD_CONST0 )
+        return 0;
+    if ( If_DsdObjType(pObj) == IF_DSD_VAR )
+        return 0;
+    if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
+        return 1;
+    If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
+        if ( If_DsdManCheckNonDec_rec( p, Abc_Lit2Var(iFanin) ) )
+            return 1;
+    return 0;
+}
+void If_DsdManPrint_rec( FILE * pFile, If_DsdMan_t * p, int iDsdLit, unsigned char * pPermLits, int * pnSupp )
 {
     char OpenType[7]  = {0, 0, 0, '(', '[', '<', '{'};
     char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'};
@@ -304,7 +322,7 @@ void If_DsdManPrint_rec( FILE * pFile, If_DsdMan_t * p, int iDsdLit, int * pPerm
         { fprintf( pFile, "0" ); return; }
     if ( If_DsdObjType(pObj) == IF_DSD_VAR )
     {
-        int iPermLit = pPermLits ? pPermLits[(*pnSupp)++] : Abc_Var2Lit((*pnSupp)++, 0);
+        int iPermLit = pPermLits ? (int)pPermLits[(*pnSupp)++] : Abc_Var2Lit((*pnSupp)++, 0);
         fprintf( pFile, "%s%c", Abc_LitIsCompl(iPermLit)? "!":"", 'a' + Abc_Lit2Var(iPermLit) );
         return;
     }
@@ -312,62 +330,19 @@ void If_DsdManPrint_rec( FILE * pFile, If_DsdMan_t * p, int iDsdLit, int * pPerm
         Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), If_DsdObjFaninNum(pObj) );
     fprintf( pFile, "%c", OpenType[If_DsdObjType(pObj)] );
     If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
-    {
-        fprintf( pFile, "%s", Abc_LitIsCompl(iFanin) ? "!":"" );
-        If_DsdManPrint_rec( pFile, p, Abc_Lit2Var(iFanin), pPermLits, pnSupp );
-    }
+        If_DsdManPrint_rec( pFile, p, iFanin, pPermLits, pnSupp );
     fprintf( pFile, "%c", CloseType[If_DsdObjType(pObj)] );
 }
-void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, int * pPermLits )
+void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char * pPermLits )
 {
     int nSupp = 0;
     fprintf( pFile, "%6d : ", iObjId );
     fprintf( pFile, "%2d ",   If_DsdVecObjSuppSize(p->vObjs, iObjId) );
+    fprintf( pFile, "%8d ",   If_DsdVecObjRef(p->vObjs, iObjId) );
     If_DsdManPrint_rec( pFile, p, Abc_Var2Lit(iObjId, 0), pPermLits, &nSupp );
     fprintf( pFile, "\n" );
     assert( nSupp == If_DsdVecObjSuppSize(p->vObjs, iObjId) );
 }
-int If_DsdManCheckNonDec_rec( If_DsdMan_t * p, int iObj )
-{
-    If_DsdObj_t * pObj;
-    int i, iFanin;
-    assert( !Abc_LitIsCompl(iObj) );
-    pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iObj) );
-    if ( If_DsdObjType(pObj) == IF_DSD_CONST0 )
-        return 0;
-    if ( If_DsdObjType(pObj) == IF_DSD_VAR )
-        return 0;
-    if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
-        return 1;
-    If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
-        if ( If_DsdManCheckNonDec_rec( p, iFanin ) )
-            return 1;
-    return 0;
-}
-void If_DsdManDump( If_DsdMan_t * p )
-{
-    char * pFileName = "dss_tts.txt";
-    FILE * pFile;
-    If_DsdObj_t * pObj;
-    int i;
-    pFile = fopen( pFileName, "wb" );
-    if ( pFile == NULL )
-    {
-        printf( "Cannot open file \"%s\".\n", pFileName );
-        return;
-    }
-    If_DsdVecForEachObj( p->vObjs, pObj, i )
-    {
-        if ( If_DsdObjType(pObj) != IF_DSD_PRIME )
-            continue;
-        fprintf( pFile, "0x" );
-        Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), p->nVars );
-        fprintf( pFile, "\n" );
-//        printf( "    " );
-//        If_DsdPrintFromTruth( stdout, If_DsdObjTruth(p, pObj), p->nVars );
-    }
-    fclose( pFile );
-}
 void If_DsdManPrint( If_DsdMan_t * p, char * pFileName )
 {
     If_DsdObj_t * pObj;
@@ -383,7 +358,7 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName )
     If_DsdVecForEachObj( p->vObjs, pObj, i )
     {
         CountNonDsd += (If_DsdObjType(pObj) == IF_DSD_PRIME);
-        CountNonDsdStr += If_DsdManCheckNonDec_rec( p, Abc_Var2Lit(pObj->Id, 0) );
+        CountNonDsdStr += If_DsdManCheckNonDec_rec( p, pObj->Id );
     }
     fprintf( pFile, "Total number of objects    = %8d\n", Vec_PtrSize(p->vObjs) );
     fprintf( pFile, "Non-DSD objects (max =%2d) = %8d\n", Vec_MemEntryNum(p->vTtMem), CountNonDsd );
@@ -399,14 +374,39 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName )
 //    return;
     If_DsdVecForEachObj( p->vObjs, pObj, i )
     {
-        if ( i == 50 )
-            break;
+//        if ( i == 50 )
+//            break;
         If_DsdManPrintOne( pFile, p, pObj->Id, NULL );
     }
     fprintf( pFile, "\n" );
     if ( pFileName )
         fclose( pFile );
 }
+void If_DsdManDump( If_DsdMan_t * p )
+{
+    char * pFileName = "dss_tts.txt";
+    FILE * pFile;
+    If_DsdObj_t * pObj;
+    int i;
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\".\n", pFileName );
+        return;
+    }
+    If_DsdVecForEachObj( p->vObjs, pObj, i )
+    {
+        if ( If_DsdObjType(pObj) != IF_DSD_PRIME )
+            continue;
+        fprintf( pFile, "0x" );
+        Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), p->nVars );
+        fprintf( pFile, "\n" );
+        printf( "    " );
+        Kit_DsdPrintFromTruth( (unsigned *)If_DsdObjTruth(p, pObj), p->nVars );
+        printf( "\n" );
+    }
+    fclose( pFile );
+}
 
 /**Function*************************************************************
 
@@ -568,17 +568,82 @@ word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLi
   SeeAlso     []
 
 ***********************************************************************/
-int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm, word * pTruth )
+int If_DsdManOperation2( If_DsdMan_t * p, int Type, int * pLits, int nLits )
 {
-    If_DsdObj_t * pObj, * pFanin;
+    If_DsdObj_t * pObj;
     int nChildren = 0, pChildren[DAU_MAX_VAR];
-    int i, k, Id, iFanin, fComplFan, fCompl = 0;
+    int i, k, Id, iFanin, fCompl = 0;
+    if ( Type == IF_DSD_AND )
+    {
+        for ( k = 0; k < nLits; k++ )
+        {
+            pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[k]) );
+            if ( Abc_LitIsCompl(pLits[k]) || If_DsdObjType(pObj) != IF_DSD_AND )
+                pChildren[nChildren++] = pLits[k];
+            else
+                If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
+                    pChildren[nChildren++] = iFanin;
+        }
+        If_DsdObjSort( p->vObjs, pChildren, nChildren, NULL );
+    }
+    else if ( Type == IF_DSD_XOR )
+    {
+        for ( k = 0; k < nLits; k++ )
+        {
+            fCompl ^= Abc_LitIsCompl(pLits[k]);
+            pObj = If_DsdVecObj( p->vObjs, Abc_LitRegular(pLits[k]) );
+            if ( If_DsdObjType(pObj) != IF_DSD_XOR )
+                pChildren[nChildren++] = pLits[k];
+            else
+                If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
+                {
+                    assert( !Abc_LitIsCompl(iFanin) );
+                    pChildren[nChildren++] = iFanin;
+                }
+        }
+        If_DsdObjSort( p->vObjs, pChildren, nChildren, NULL );
+    }
+    else if ( Type == IF_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++] = pLits[k];
+    }
+    else assert( 0 );
+    // create new graph
+    Id = If_DsdObjFindOrAdd( p, Type, pChildren, nChildren, NULL );
+    return Abc_Var2Lit( Id, fCompl );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DSD operation.]
+
+  Description []
+               
+  SideEffects []
 
-    assert( Type == IF_DSD_AND || pPerm == NULL );
-    if ( Type == IF_DSD_AND && pPerm != NULL )
+  SeeAlso     []
+
+***********************************************************************/
+int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm, word * pTruth )
+{
+    If_DsdObj_t * pObj, * pFanin;
+    unsigned char pPermNew[DAU_MAX_VAR];
+    int nChildren = 0, pChildren[DAU_MAX_VAR], pBegEnd[DAU_MAX_VAR];
+    int i, k, j, Id, iFanin, fComplFan, fCompl = 0, nSSize = 0;
+    if ( Type == IF_DSD_AND )
     {
-        int pBegEnd[DAU_MAX_VAR];
-        int j, nSSize = 0;
         for ( k = 0; k < nLits; k++ )
         {
             pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[k]) );
@@ -596,8 +661,8 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig
                     pFanin = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iFanin) );
                     fComplFan = If_DsdObjIsVar(pFanin) && Abc_LitIsCompl(iFanin);
                     pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + pFanin->nSupp);
-                    nSSize += pFanin->nSupp;
                     pChildren[nChildren++] = Abc_LitNotCond( iFanin, fComplFan );
+                    nSSize += pFanin->nSupp;
                 }
             }
         }
@@ -605,59 +670,104 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig
         // 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 );
+                pPermNew[j++] = (unsigned char)Abc_LitNotCond( pPerm[k], (pBegEnd[i] >> 8) & 1 );
         assert( j == nSSize );
-    }
-    else if ( Type == IF_DSD_AND )
-    {
-        for ( k = 0; k < nLits; k++ )
-        {
-            pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[k]) );
-            if ( Abc_LitIsCompl(pLits[k]) || If_DsdObjType(pObj) != IF_DSD_AND )
-                pChildren[nChildren++] = pLits[k];
-            else
-                If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
-                    pChildren[nChildren++] = iFanin;
-        }
-        If_DsdObjSort( p->vObjs, pChildren, nChildren, NULL );
+        for ( j = 0; j < nSSize; j++ )
+            pPerm[j] = pPermNew[j];
     }
     else if ( Type == IF_DSD_XOR )
     {
+        fComplFan = 0;
         for ( k = 0; k < nLits; k++ )
         {
             fCompl ^= Abc_LitIsCompl(pLits[k]);
-            pObj = If_DsdVecObj( p->vObjs, Abc_LitRegular(pLits[k]) );
+            pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[k]) );
             if ( If_DsdObjType(pObj) != IF_DSD_XOR )
-                pChildren[nChildren++] = pLits[k];
+            {
+                pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + pObj->nSupp);
+                pChildren[nChildren++] = Abc_LitRegular(pLits[k]);
+                nSSize += pObj->nSupp;
+            }
             else
+            {
                 If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
                 {
                     assert( !Abc_LitIsCompl(iFanin) );
-                    pChildren[nChildren++] = iFanin;
+                    pFanin = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iFanin) );
+                    pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + pFanin->nSupp);
+                    pChildren[nChildren++] = Abc_LitRegular(iFanin);
+                    nSSize += pFanin->nSupp;
                 }
+            }
         }
-        If_DsdObjSort( p->vObjs, pChildren, nChildren, NULL );
+        If_DsdObjSort( p->vObjs, pChildren, nChildren, pBegEnd );
+        // create permutation
+        for ( j = i = 0; i < nChildren; i++ )
+            for ( k = (pBegEnd[i] >> 16); k < (pBegEnd[i] & 0xFF); k++ )
+                pPermNew[j++] = (unsigned char)Abc_LitNotCond( pPerm[k], (pBegEnd[i] >> 8) & 1 );
+        assert( j == nSSize );
+        for ( j = 0; j < nSSize; j++ )
+            pPerm[j] = pPermNew[j];
     }
     else if ( Type == IF_DSD_MUX )
     {
-        if ( Abc_LitIsCompl(pLits[0]) )
+        for ( k = 0; k < nLits; k++ )
         {
-            pLits[0] = Abc_LitNot(pLits[0]);
-            ABC_SWAP( int, pLits[1], pLits[2] );
+            pFanin = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[k]) );
+            fComplFan = If_DsdObjIsVar(pFanin) && Abc_LitIsCompl(pLits[k]);
+            pChildren[nChildren++] = Abc_LitNotCond( pLits[k], fComplFan );
+            pPerm[k] = (unsigned char)Abc_LitNotCond( (int)pPerm[k], fComplFan );
+            nSSize += pFanin->nSupp;
         }
-        if ( Abc_LitIsCompl(pLits[1]) )
+        if ( Abc_LitIsCompl(pChildren[0]) )
         {
-            pLits[1] = Abc_LitNot(pLits[1]);
-            pLits[2] = Abc_LitNot(pLits[2]);
+            If_DsdObj_t * pFans[3];
+            pChildren[0] = Abc_LitNot(pChildren[0]);
+            ABC_SWAP( int, pChildren[1], pChildren[2] );
+            pFans[0] = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pChildren[0]) );
+            pFans[1] = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pChildren[1]) );
+            pFans[2] = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pChildren[2]) );
+            nSSize = pFans[0]->nSupp + pFans[1]->nSupp + pFans[2]->nSupp;
+            for ( j = k = 0; k < If_DsdObjSuppSize(pFans[0]); k++ )
+                pPermNew[j++] = pPerm[k];
+            for ( k = 0; k < If_DsdObjSuppSize(pFans[2]); k++ )
+                pPermNew[j++] = pPerm[pFans[0]->nSupp + pFans[1]->nSupp + k];
+            for ( k = 0; k < If_DsdObjSuppSize(pFans[1]); k++ )
+                pPermNew[j++] = pPerm[pFans[0]->nSupp + k];
+            assert( j == nSSize );
+            for ( j = 0; j < nSSize; j++ )
+                pPerm[j] = pPermNew[j];
+        }
+        if ( Abc_LitIsCompl(pChildren[1]) )
+        {
+            pChildren[1] = Abc_LitNot(pChildren[1]);
+            pChildren[2] = Abc_LitNot(pChildren[2]);
             fCompl ^= 1;
         }
-        for ( k = 0; k < nLits; k++ )
-            pChildren[nChildren++] = pLits[k];
     }
     else if ( Type == IF_DSD_PRIME )
     {
-        for ( k = 0; k < nLits; k++ )
-            pChildren[nChildren++] = pLits[k];
+        char pCanonPerm[DAU_MAX_VAR];
+        int i, uCanonPhase, pFirsts[DAU_MAX_VAR];
+        uCanonPhase = Abc_TtCanonicize( pTruth, nLits, pCanonPerm );
+        fCompl = ((uCanonPhase >> nLits) & 1);
+        for ( i = 0; i < nLits; i++ )
+        {
+            pFirsts[i] = nSSize;
+            nSSize += If_DsdVecLitSuppSize(p->vObjs, pLits[i]);
+        }
+        for ( j = i = 0; i < nLits; i++ )
+        {
+            int iLitNew = Abc_LitNotCond( pLits[(int)pCanonPerm[i]], ((uCanonPhase>>i)&1) );
+            pFanin = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iLitNew) );
+            fComplFan = If_DsdObjIsVar(pFanin) && Abc_LitIsCompl(iLitNew);
+            pChildren[nChildren++] = Abc_LitNotCond( iLitNew, fComplFan );
+            for ( k = 0; k < (int)pFanin->nSupp; k++ )            
+                pPermNew[j++] = (unsigned char)Abc_LitNotCond( (int)pPerm[pFirsts[(int)pCanonPerm[i]] + k], fComplFan );
+        }
+        assert( j == nSSize );
+        for ( j = 0; j < nSSize; j++ )
+            pPerm[j] = pPermNew[j];
     }
     else assert( 0 );
     // create new graph
@@ -665,7 +775,6 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig
     return Abc_Var2Lit( Id, fCompl );
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Creating DSD network from SOP.]
@@ -692,31 +801,25 @@ static inline void If_DsdMergeMatches( char * pDsd, int * pMatches )
     }
     assert( nNested == 0 );
 }
-int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * pMan, word * pTruth, unsigned char * pPerm )
+int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * pMan, word * pTruth, unsigned char * pPerm, int * pnSupp )
 {
+    unsigned char * pPermStart = pPerm + *pnSupp;
     int iRes = -1, fCompl = 0;
     if ( **p == '!' )
     {
         fCompl = 1;
         (*p)++;
     }
-    while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
-        (*p)++;
-/*
-    if ( **p == '<' )
+    assert( !((**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9')) );
+    if ( **p >= 'a' && **p <= 'z' ) // var
     {
-        char * q = pStr + pMatches[ *p - pStr ];
-        if ( *(q+1) == '{' )
-            *p = q+1;
+        pPerm[(*pnSupp)++] = Abc_Var2Lit( **p - 'a', fCompl );
+        return 2;
     }
-*/
-    if ( **p >= 'a' && **p <= 'z' ) // var
-        return Abc_Var2Lit( If_DsdObjId(If_DsdVecVar(pMan->vObjs, **p - 'a')), fCompl );
     if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
     {
-        int pLits[DAU_MAX_VAR], nLits = 0;
+        int Type, nLits = 0, pLits[DAU_MAX_VAR];
         char * q = pStr + pMatches[ *p - pStr ];
-        int Type;
         if ( **p == '(' )
             Type = DAU_DSD_AND;
         else if ( **p == '[' )
@@ -728,28 +831,15 @@ int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * p
         else assert( 0 );
         assert( *q == **p + 1 + (**p != '(') );
         for ( (*p)++; *p < q; (*p)++ )
-            pLits[nLits++] = If_DsdManAddDsd_rec( pStr, p, pMatches, pMan, pTruth, pPerm );
+            pLits[nLits++] = If_DsdManAddDsd_rec( pStr, p, pMatches, pMan, pTruth, pPerm, pnSupp );
         assert( *p == q );
-        if ( Type == DAU_DSD_PRIME )
-        {
-            word pTemp[DAU_MAX_WORD];
-            char pCanonPerm[DAU_MAX_VAR];
-            int i, uCanonPhase, pLitsNew[DAU_MAX_VAR];
-            Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nLits), 0 );
-            uCanonPhase = Abc_TtCanonicize( pTemp, nLits, pCanonPerm );
-            fCompl = (uCanonPhase >> nLits) & 1;
-            for ( i = 0; i < nLits; i++ )
-                pLitsNew[i] = Abc_LitNotCond( pLits[pCanonPerm[i]], (uCanonPhase>>i)&1 );
-            iRes = If_DsdManOperation( pMan, Type, pLitsNew, nLits, pPerm, pTemp );
-        }
-        else
-            iRes = If_DsdManOperation( pMan, Type, pLits, nLits, pPerm, pTruth );
+        iRes = If_DsdManOperation( pMan, Type, pLits, nLits, pPermStart, pTruth );
         return Abc_LitNotCond( iRes, fCompl );
     }
     assert( 0 );
     return -1;
 }
-int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char * pPerm )
+int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char * pPerm, int * pnSupp )
 {
     int iRes = -1, fCompl = 0;
     if ( *pDsd == '!' )
@@ -757,12 +847,15 @@ int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char
     if ( Dau_DsdIsConst(pDsd) )
         iRes = 0;
     else if ( Dau_DsdIsVar(pDsd) )
-        iRes = Dau_DsdReadVar(pDsd);
+    {
+        pPerm[(*pnSupp)++] = Dau_DsdReadVar(pDsd);
+        iRes = 2;
+    }
     else
     {
         int pMatches[DAU_MAX_STR];
         If_DsdMergeMatches( pDsd, pMatches );
-        iRes = If_DsdManAddDsd_rec( pDsd, &pDsd, pMatches, p, pTruth, pPerm );
+        iRes = If_DsdManAddDsd_rec( pDsd, &pDsd, pMatches, p, pTruth, pPerm, pnSupp );
     }
     return Abc_LitNotCond( iRes, fCompl );
 }
@@ -782,20 +875,33 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char
 {
     word pCopy[DAU_MAX_WORD], * pRes;
     char pDsd[DAU_MAX_STR];
-    int i, iDsdFunc, nSizeNonDec;
+    int iDsd, nSizeNonDec, nSupp = 0;
     assert( nLeaves <= DAU_MAX_VAR );
     Abc_TtCopy( pCopy, pTruth, p->nWords, 0 );
     nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 0, pDsd );
+    if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") )
+    {
+//        int x = 0;
+    }
     if ( nSizeNonDec > 0 )
         Abc_TtStretch6( pCopy, nSizeNonDec, p->nVars );
-    for ( i = 0; i < p->nVars; i++ )
-        pPerm[i] = (char)i;
-    iDsdFunc = If_DsdManAddDsd( p, pDsd, pCopy, pPerm );
+    memset( pPerm, 0xFF, nLeaves );
+    iDsd = If_DsdManAddDsd( p, pDsd, pCopy, pPerm, &nSupp );
+    assert( nSupp == nLeaves );
     // verify the result
-    pRes = If_DsdManComputeTruth( p, iDsdFunc, pPerm );
+    pRes = If_DsdManComputeTruth( p, iDsd, pPerm );
     if ( !Abc_TtEqual(pRes, pTruth, p->nWords) )
+    {
+//        If_DsdManPrint( p, NULL );
+        printf( "\n" );
         printf( "Verification failed!\n" );
-    return iDsdFunc;
+        Kit_DsdPrintFromTruth( (unsigned *)pTruth, nLeaves ); printf( "\n" );
+        Kit_DsdPrintFromTruth( (unsigned *)pRes, nLeaves ); printf( "\n" );
+        If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm );
+        printf( "\n" );
+    }
+    If_DsdVecObjIncRef( p->vObjs, Abc_Lit2Var(iDsd) );
+    return iDsd;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index cd8d2688..529b8cb9 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -153,10 +153,7 @@ void If_ManStop( If_Man_t * p )
     if ( p->pPars->fVerbose && p->nCuts5 )
         Abc_Print( 1, "Statistics about 5-cuts: Total = %d  Non-decomposable = %d (%.2f %%)\n", p->nCuts5, p->nCuts5-p->nCuts5a, 100.0*(p->nCuts5-p->nCuts5a)/p->nCuts5 );
     if ( p->pPars->fUseDsd )
-    {
-        If_DsdManPrint( p->pIfDsdMan, NULL );
         If_DsdManFree( p->pIfDsdMan );
-    }
 //    Abc_PrintTime( 1, "Truth", p->timeTruth );
 //    Abc_Print( 1, "Small support = %d.\n", p->nSmallSupp );
     Vec_IntFreeP( &p->vCoAttrs );
diff --git a/src/misc/vec/vecMem.h b/src/misc/vec/vecMem.h
index 3f1b4517..206b42d2 100644
--- a/src/misc/vec/vecMem.h
+++ b/src/misc/vec/vecMem.h
@@ -281,7 +281,7 @@ static inline void Vec_MemDump( FILE * pFile, Vec_Mem_t * pVec )
     word * pEntry;
     int i, w, d;
     if ( pFile == stdout )
-        printf( "Memory vector has %d entries: ", Vec_MemEntryNum(pVec) );
+        printf( "Memory vector has %d entries: \n", Vec_MemEntryNum(pVec) );
     Vec_MemForEachEntry( pVec, pEntry, i )
     {
         for ( w = pVec->nEntrySize - 1; w >= 0; w-- )
@@ -392,12 +392,13 @@ static inline void Vec_MemDumpTruthTables( Vec_Mem_t * p, char * pName, int nLut
 {
     FILE * pFile;
     char pFileName[1000];
-    sprintf( pFileName, "tt_%s_%02d.txt", pName, nLutSize );
-    pFile = fopen( pFileName, "wb" );
+    sprintf( pFileName, "tt_%s_%02d.txt", pName ? pName : NULL, nLutSize );
+    pFile = pName ? fopen( pFileName, "wb" ) : stdout;
     Vec_MemDump( pFile, p );
-    fclose( pFile );
+    if ( pFile != stdout )
+        fclose( pFile );
     printf( "Dumped %d %d-var truth tables into file \"%s\" (%.2f MB).\n", 
-        Vec_MemEntryNum(p), nLutSize, pFileName,
+        Vec_MemEntryNum(p), nLutSize, pName ? pFileName : "stdout",
         8.0 * Vec_MemEntryNum(p) * Vec_MemEntrySize(p) / (1 << 20) );
 }