Changes to LUT mappers.

5 files changed, 468 insertions, 265 deletions

diff --git a/src/map/if/if.h b/src/map/if/if.h
index 47bd7390..c8b04ef1 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -517,12 +517,18 @@ extern int             If_CluCheckExt( void * p, word * pTruth, int nVars, int n
 extern int             If_CluCheckExt3( void * p, word * pTruth, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot, 
                            char * pLut0, char * pLut1, char * pLut2, word * pFunc0, word * pFunc1, word * pFunc2 );
 /*=== ifDsd.c =============================================================*/
-extern If_DsdMan_t *   If_DsdManAlloc( int nLutSize );
+extern If_DsdMan_t *   If_DsdManAlloc( int nVars, int nLutSize );
 extern void            If_DsdManDump( If_DsdMan_t * p );
 extern void            If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose );
 extern void            If_DsdManFree( If_DsdMan_t * p, int fVerbose );
+extern void            If_DsdManSave( If_DsdMan_t * p, char * pFileName );
+extern If_DsdMan_t *   If_DsdManLoad( char * pFileName );
 extern int             If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct );
+extern char *          If_DsdManFileName( If_DsdMan_t * p );
+extern int             If_DsdManVarNum( If_DsdMan_t * p );
+extern int             If_DsdManLutSize( If_DsdMan_t * p );
 extern int             If_DsdManCheckDec( If_DsdMan_t * p, int iDsd );
+extern unsigned        If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose );
 /*=== ifLib.c =============================================================*/
 extern If_LibLut_t *   If_LibLutRead( char * FileName );
 extern If_LibLut_t *   If_LibLutDup( If_LibLut_t * p );
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index 23160e62..a72362d7 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -53,7 +53,9 @@ struct If_DsdObj_t_
 
 struct If_DsdMan_t_
 {
+    char *         pStore;         // input/output file
     int            nVars;          // max var number
+    int            LutSize;        // LUT size
     int            nWords;         // word number
     int            nBins;          // table size
     unsigned *     pBins;          // hash table
@@ -113,10 +115,10 @@ static inline void          If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj )
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
- 
+
 /**Function*************************************************************
 
-  Synopsis    [Sorting DSD literals.]
+  Synopsis    []
 
   Description []
                
@@ -125,114 +127,21 @@ static inline void          If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj )
   SeeAlso     []
 
 ***********************************************************************/
-int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 )
+char * If_DsdManFileName( If_DsdMan_t * p )
 {
-    If_DsdObj_t * p0 = If_DsdVecObj(p, Abc_Lit2Var(iLit0));
-    If_DsdObj_t * p1 = If_DsdVecObj(p, Abc_Lit2Var(iLit1));
-    int i, Res;
-    if ( If_DsdObjType(p0) < If_DsdObjType(p1) )
-        return -1;
-    if ( If_DsdObjType(p0) > If_DsdObjType(p1) )
-        return 1;
-    if ( If_DsdObjType(p0) < IF_DSD_AND )
-        return 0;
-    if ( If_DsdObjFaninNum(p0) < If_DsdObjFaninNum(p1) )
-        return -1;
-    if ( If_DsdObjFaninNum(p0) > If_DsdObjFaninNum(p1) )
-        return 1;
-    for ( i = 0; i < If_DsdObjFaninNum(p0); i++ )
-    {
-        Res = If_DsdObjCompare( p, If_DsdObjFaninLit(p0, i), If_DsdObjFaninLit(p1, i) );
-        if ( Res != 0 )
-            return Res;
-    }
-    if ( Abc_LitIsCompl(iLit0) < Abc_LitIsCompl(iLit1) )
-        return -1;
-    if ( Abc_LitIsCompl(iLit0) > Abc_LitIsCompl(iLit1) )
-        return 1;
-    return 0;
+    return p->pStore;
 }
-void If_DsdObjSort( Vec_Ptr_t * p, int * pLits, int nLits, int * pPerm )
+int If_DsdManVarNum( If_DsdMan_t * p )
 {
-    int i, j, best_i;
-    for ( i = 0; i < nLits-1; i++ )
-    {
-        best_i = i;
-        for ( j = i+1; j < nLits; j++ )
-            if ( If_DsdObjCompare(p, pLits[best_i], pLits[j]) == 1 )
-                best_i = j;
-        if ( i == best_i )
-            continue;
-        ABC_SWAP( int, pLits[i], pLits[best_i] );
-        if ( pPerm )
-            ABC_SWAP( int, pPerm[i], pPerm[best_i] );
-    }
+    return p->nVars;
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Creating DSD objects.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans )
+int If_DsdManLutSize( If_DsdMan_t * p )
 {
-    int nWords = If_DsdObjWordNum( nFans + (int)(Type == DAU_DSD_PRIME) );
-    If_DsdObj_t * pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords );
-    If_DsdObjClean( pObj );
-    pObj->Type   = Type;
-    pObj->nFans  = nFans;
-    pObj->Id     = Vec_PtrSize( p->vObjs );
-    pObj->fMark  = 0;
-    pObj->Count  = 0;
-    Vec_PtrPush( p->vObjs, pObj );
-    Vec_IntPush( p->vNexts, 0 );
-    return pObj;
+    return p->LutSize;
 }
-int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId )
+int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd )
 {
-    If_DsdObj_t * pObj, * pFanin;
-    int i, iPrev = -1;
-    // check structural canonicity
-    assert( Type != DAU_DSD_MUX || nLits == 3 );
-    assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[0]) );
-    assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[1]) || !Abc_LitIsCompl(pLits[2]) );
-    // check that leaves are in good order
-    if ( Type == DAU_DSD_AND || Type == DAU_DSD_XOR )
-    {
-        for ( i = 0; i < nLits; i++ )
-        {
-            pFanin = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[i]) );
-            assert( Type != DAU_DSD_AND || Abc_LitIsCompl(pLits[i]) || If_DsdObjType(pFanin) != DAU_DSD_AND );
-            assert( Type != DAU_DSD_XOR || If_DsdObjType(pFanin) != DAU_DSD_XOR );
-            assert( iPrev == -1 || If_DsdObjCompare(p->vObjs, iPrev, pLits[i]) <= 0 );
-            iPrev = pLits[i];
-        }
-    }
-    if ( Vec_PtrSize(p->vObjs) % p->nBins == 0 )
-        printf( "Warning: The number of objects in If_DsdObjCreate() is more than the number of bins.\n" );
-    // create new node
-    pObj = If_DsdObjAlloc( p, Type, nLits );
-    if ( Type == DAU_DSD_PRIME )
-        If_DsdObjSetTruth( p, pObj, truthId );
-    assert( pObj->nSupp == 0 );
-    for ( i = 0; i < nLits; i++ )
-    {
-        pObj->pFans[i] = pLits[i];
-        pObj->nSupp += If_DsdVecLitSuppSize(p->vObjs, pLits[i]);
-    }
-/*
-    {
-        extern void If_DsdManPrintOne( If_DsdMan_t * p, int iDsdLit, int * pPermLits );
-        If_DsdManPrintOne( p, If_DsdObj2Lit(pObj), NULL );
-    }
-*/
-    return pObj->Id;
+    return If_DsdVecObjMark( p->vObjs, Abc_Lit2Var(iDsd) );
 }
 
 /**Function*************************************************************
@@ -258,17 +167,35 @@ static inline word ** If_ManDsdTtElems()
     }
     return pTtElems;
 }
-If_DsdMan_t * If_DsdManAlloc( int nVars )
+If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans )
+{
+    int nWords = If_DsdObjWordNum( nFans + (int)(Type == DAU_DSD_PRIME) );
+    If_DsdObj_t * pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords );
+    If_DsdObjClean( pObj );
+    pObj->Type   = Type;
+    pObj->nFans  = nFans;
+    pObj->Id     = Vec_PtrSize( p->vObjs );
+    pObj->fMark  = 0;
+    pObj->Count  = 0;
+    Vec_PtrPush( p->vObjs, pObj );
+    Vec_IntPush( p->vNexts, 0 );
+    return pObj;
+}
+If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
 {
     If_DsdMan_t * p; int v;
+    char pFileName[10];
+    sprintf( pFileName, "%02d.dsd", nVars );
     p = ABC_CALLOC( If_DsdMan_t, 1 );
-    p->nVars  = nVars;
-    p->nWords = Abc_TtWordNum( nVars );
-    p->nBins  = Abc_PrimeCudd( 1000000 );
-    p->pBins  = ABC_CALLOC( unsigned, p->nBins );
-    p->pMem   = Mem_FlexStart();
-    p->vObjs  = Vec_PtrAlloc( 10000 );
-    p->vNexts = Vec_IntAlloc( 10000 );
+    p->pStore  = Abc_UtilStrsav( pFileName );
+    p->nVars   = nVars;
+    p->LutSize = LutSize;
+    p->nWords  = Abc_TtWordNum( nVars );
+    p->nBins   = Abc_PrimeCudd( 1000000 );
+    p->pBins   = ABC_CALLOC( unsigned, p->nBins );
+    p->pMem    = Mem_FlexStart();
+    p->vObjs   = Vec_PtrAlloc( 10000 );
+    p->vNexts  = Vec_IntAlloc( 10000 );
     If_DsdObjAlloc( p, IF_DSD_CONST0, 0 );
     If_DsdObjAlloc( p, IF_DSD_VAR, 0 )->nSupp = 1;
     p->vNodes   = Vec_IntAlloc( 32 );
@@ -284,8 +211,8 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
 {
     int v;
 //    If_DsdManDump( p );
-    If_DsdManPrint( p, NULL, 0 );
-    Vec_MemDumpTruthTables( p->vTtMem, "dumpdsd", p->nVars );
+    if ( fVerbose )
+        If_DsdManPrint( p, NULL, 0 );
     if ( fVerbose )
     {
         Abc_PrintTime( 1, "Time DSD   ", p->timeDsd    );
@@ -293,6 +220,8 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
         Abc_PrintTime( 1, "Time check ", p->timeCheck  );
         Abc_PrintTime( 1, "Time verify", p->timeVerify );
     }
+    if ( fVerbose )
+        Vec_MemDumpTruthTables( p->vTtMem, "dumpdsd", p->nVars );
     for ( v = 2; v < p->nVars; v++ )
         ABC_FREE( p->pSched[v] );
     Vec_VecFree( (Vec_Vec_t *)p->vTtDecs );
@@ -302,9 +231,46 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
     Vec_IntFreeP( &p->vNexts );
     Vec_PtrFreeP( &p->vObjs );
     Mem_FlexStop( p->pMem, 0 );
+    ABC_FREE( p->pStore );
     ABC_FREE( p->pBins );
     ABC_FREE( p );
 }
+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( "    " );
+        Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars );
+    }
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Printing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void If_DsdManHashProfile( If_DsdMan_t * p )
 {
     If_DsdObj_t * pObj;
@@ -367,6 +333,7 @@ void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char
     fprintf( pFile, "%6d : ", iObjId );
     fprintf( pFile, "%2d ",   If_DsdVecObjSuppSize(p->vObjs, iObjId) );
     fprintf( pFile, "%8d ",   If_DsdVecObjRef(p->vObjs, iObjId) );
+    fprintf( pFile, "%d  ",    If_DsdVecObjMark(p->vObjs, iObjId) );
     If_DsdManPrint_rec( pFile, p, Abc_Var2Lit(iObjId, 0), pPermLits, &nSupp );
     if ( fNewLine )
         fprintf( pFile, "\n" );
@@ -400,7 +367,7 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
     fprintf( pFile, "Memory used for objects    = %8.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
     fprintf( pFile, "Memory used for hash table = %8.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) );
     fprintf( pFile, "Memory used for array      = %8.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+//    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 //    If_DsdManHashProfile( p );
 //    If_DsdManDump( p );
 //    return;
@@ -416,57 +383,6 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
     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( "    " );
-        Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars );
-    }
-    fclose( pFile );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collect nodes of the tree.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
-{
-    int i, iFanin;
-    If_DsdObj_t * pObj = If_DsdVecObj( p->vObjs, Id );
-    if ( If_DsdObjType(pObj) == IF_DSD_CONST0 || If_DsdObjType(pObj) == IF_DSD_VAR )
-        return;
-    If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
-        If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes );
-    Vec_IntPush( vNodes, Id );
-}
-void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
-{
-    Vec_IntClear( vNodes );
-    If_DsdManCollect_rec( p, Id, vNodes );
-}
 
 /**Function*************************************************************
 
@@ -481,7 +397,6 @@ void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
 ***********************************************************************/
 static inline unsigned If_DsdObjHashKey( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId )
 {
-//    static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
     static int s_Primes[24] = { 1049, 1297, 1559, 1823, 2089, 2371, 2663, 2909, 
                                 3221, 3517, 3779, 4073, 4363, 4663, 4973, 5281, 
                                 5573, 5861, 6199, 6481, 6803, 7109, 7477, 7727 };
@@ -512,6 +427,43 @@ unsigned * If_DsdObjHashLookup( If_DsdMan_t * p, int Type, int * pLits, int nLit
     p->nUniqueMisses++;
     return pSpot;
 }
+int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId )
+{
+    If_DsdObj_t * pObj, * pFanin;
+    int i, iPrev = -1;
+    // check structural canonicity
+    assert( Type != DAU_DSD_MUX || nLits == 3 );
+    assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[0]) );
+    assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[1]) || !Abc_LitIsCompl(pLits[2]) );
+    // check that leaves are in good order
+    if ( Type == DAU_DSD_AND || Type == DAU_DSD_XOR )
+    {
+        for ( i = 0; i < nLits; i++ )
+        {
+            pFanin = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[i]) );
+            assert( Type != DAU_DSD_AND || Abc_LitIsCompl(pLits[i]) || If_DsdObjType(pFanin) != DAU_DSD_AND );
+            assert( Type != DAU_DSD_XOR || If_DsdObjType(pFanin) != DAU_DSD_XOR );
+            assert( iPrev == -1 || If_DsdObjCompare(p->vObjs, iPrev, pLits[i]) <= 0 );
+            iPrev = pLits[i];
+        }
+    }
+    if ( Vec_PtrSize(p->vObjs) % p->nBins == 0 )
+        printf( "Warning: The number of objects in If_DsdObjCreate() is more than the number of bins.\n" );
+    // create new node
+    pObj = If_DsdObjAlloc( p, Type, nLits );
+    if ( Type == DAU_DSD_PRIME )
+        If_DsdObjSetTruth( p, pObj, truthId );
+    assert( pObj->nSupp == 0 );
+    for ( i = 0; i < nLits; i++ )
+    {
+        pObj->pFans[i] = pLits[i];
+        pObj->nSupp += If_DsdVecLitSuppSize(p->vObjs, pLits[i]);
+    }
+    // check decomposability
+    if ( p->LutSize && !If_DsdManCheckXY(p, Abc_Var2Lit(pObj->Id, 0), p->LutSize, 0, 0) )
+        If_DsdVecObjSetMark( p->vObjs, pObj->Id );
+    return pObj->Id;
+}
 int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word * pTruth )
 {
     int truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem, pTruth) : -1;
@@ -536,6 +488,146 @@ p->timeCheck += Abc_Clock() - clk;
 
 /**Function*************************************************************
 
+  Synopsis    [Saving/loading DSD manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_DsdManSave( If_DsdMan_t * p, char * pFileName )
+{
+    If_DsdObj_t * pObj; 
+    Vec_Int_t * vSets;
+    char * pBuffer = "dsd0";
+    word * pTruth; 
+    int i, Num;
+    FILE * pFile = fopen( pFileName ? pFileName : p->pStore, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Writing DSD manager file \"%s\" has failed.\n", pFileName ? pFileName : p->pStore );
+        return;
+    }
+    fwrite( pBuffer, 4, 1, pFile );
+    Num = p->nVars;
+    fwrite( &Num, 4, 1, pFile );
+    Num = p->LutSize;
+    fwrite( &Num, 4, 1, pFile );
+    Num = Vec_PtrSize(p->vObjs);
+    fwrite( &Num, 4, 1, pFile );
+    Vec_PtrForEachEntryStart( If_DsdObj_t *, p->vObjs, pObj, i, 2 )
+    {
+        Num = If_DsdObjWordNum( pObj->nFans + (int)(pObj->Type == DAU_DSD_PRIME) );
+        fwrite( &Num, 4, 1, pFile );
+        fwrite( pObj, sizeof(word)*Num, 1, pFile );
+    }
+    assert( Vec_MemEntryNum(p->vTtMem) == Vec_PtrSize(p->vTtDecs) ); 
+    Num = Vec_MemEntryNum(p->vTtMem);
+    fwrite( &Num, 4, 1, pFile );
+    Vec_MemForEachEntry( p->vTtMem, pTruth, i )
+        fwrite( pTruth, sizeof(word)*p->nWords, 1, pFile );
+    Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs, vSets, i )
+    {
+        Num = Vec_IntSize(vSets);
+        fwrite( &Num, 4, 1, pFile );
+        fwrite( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
+    }
+    fclose( pFile );
+}
+If_DsdMan_t * If_DsdManLoad( char * pFileName )
+{
+    If_DsdMan_t * p;
+    If_DsdObj_t * pObj; 
+    Vec_Int_t * vSets;
+    char pBuffer[10];
+    unsigned * pSpot;
+    word * pTruth;
+    int i, Num;
+    FILE * pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Reading DSD manager file \"%s\" has failed.\n", pFileName );
+        return NULL;
+    }
+    fread( pBuffer, 4, 1, pFile );
+    if ( pBuffer[0] != 'd' && pBuffer[1] != 's' && pBuffer[2] != 'd' && pBuffer[3] != '0' )
+    {
+        printf( "Unrecognized format of file \"%s\".\n", pFileName );
+        return NULL;
+    }
+    fread( &Num, 4, 1, pFile );
+    p = If_DsdManAlloc( Num, 0 );
+    ABC_FREE( p->pStore );
+    p->pStore = Abc_UtilStrsav( pFileName );
+    fread( &Num, 4, 1, pFile );
+    p->LutSize = Num;
+    fread( &Num, 4, 1, pFile );
+    assert( Num >= 2 );
+    Vec_PtrFillExtra( p->vObjs, Num, NULL );
+    Vec_IntFill( p->vNexts, Num, 0 );
+    for ( i = 2; i < Vec_PtrSize(p->vObjs); i++ )
+    {
+        fread( &Num, 4, 1, pFile );
+        pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * Num );
+        fread( pObj, sizeof(word)*Num, 1, pFile );
+        Vec_PtrWriteEntry( p->vObjs, i, pObj );
+        pSpot = If_DsdObjHashLookup( p, pObj->Type, pObj->pFans, pObj->nFans, If_DsdObjTruthId(p, pObj) );
+        assert( *pSpot == 0 );
+        *pSpot = pObj->Id;
+    }
+    fread( &Num, 4, 1, pFile );
+    pTruth = ABC_ALLOC( word, p->nWords );
+    for ( i = 0; i < Num; i++ )
+    {
+        fread( pTruth, sizeof(word)*p->nWords, 1, pFile );
+        Vec_MemHashInsert( p->vTtMem, pTruth );
+    }
+    ABC_FREE( pTruth );
+    assert( Num == Vec_MemEntryNum(p->vTtMem) );
+    for ( i = 0; i < Vec_MemEntryNum(p->vTtMem); i++ )
+    {
+        fread( &Num, 4, 1, pFile );
+        vSets = Vec_IntAlloc( Num );
+        fread( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
+        vSets->nSize = Num;
+        Vec_PtrPush( p->vTtDecs, vSets );
+    }
+    assert( Vec_MemEntryNum(p->vTtMem) == Vec_PtrSize(p->vTtDecs) ); 
+    fclose( pFile );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect nodes of the tree.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
+{
+    int i, iFanin;
+    If_DsdObj_t * pObj = If_DsdVecObj( p->vObjs, Id );
+    if ( If_DsdObjType(pObj) == IF_DSD_CONST0 || If_DsdObjType(pObj) == IF_DSD_VAR )
+        return;
+    If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
+        If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes );
+    Vec_IntPush( vNodes, Id );
+}
+void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
+{
+    Vec_IntClear( vNodes );
+    If_DsdManCollect_rec( p, Id, vNodes );
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -617,6 +709,61 @@ word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLi
     assert( nSupp == If_DsdVecObjSuppSize(p->vObjs, Abc_Lit2Var(iDsd)) );
     return pRes;
 }
+ 
+/**Function*************************************************************
+
+  Synopsis    [Sorting DSD literals.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 )
+{
+    If_DsdObj_t * p0 = If_DsdVecObj(p, Abc_Lit2Var(iLit0));
+    If_DsdObj_t * p1 = If_DsdVecObj(p, Abc_Lit2Var(iLit1));
+    int i, Res;
+    if ( If_DsdObjType(p0) < If_DsdObjType(p1) )
+        return -1;
+    if ( If_DsdObjType(p0) > If_DsdObjType(p1) )
+        return 1;
+    if ( If_DsdObjType(p0) < IF_DSD_AND )
+        return 0;
+    if ( If_DsdObjFaninNum(p0) < If_DsdObjFaninNum(p1) )
+        return -1;
+    if ( If_DsdObjFaninNum(p0) > If_DsdObjFaninNum(p1) )
+        return 1;
+    for ( i = 0; i < If_DsdObjFaninNum(p0); i++ )
+    {
+        Res = If_DsdObjCompare( p, If_DsdObjFaninLit(p0, i), If_DsdObjFaninLit(p1, i) );
+        if ( Res != 0 )
+            return Res;
+    }
+    if ( Abc_LitIsCompl(iLit0) < Abc_LitIsCompl(iLit1) )
+        return -1;
+    if ( Abc_LitIsCompl(iLit0) > Abc_LitIsCompl(iLit1) )
+        return 1;
+    return 0;
+}
+void If_DsdObjSort( Vec_Ptr_t * p, int * pLits, int nLits, int * pPerm )
+{
+    int i, j, best_i;
+    for ( i = 0; i < nLits-1; i++ )
+    {
+        best_i = i;
+        for ( j = i+1; j < nLits; j++ )
+            if ( If_DsdObjCompare(p, pLits[best_i], pLits[j]) == 1 )
+                best_i = j;
+        if ( i == best_i )
+            continue;
+        ABC_SWAP( int, pLits[i], pLits[best_i] );
+        if ( pPerm )
+            ABC_SWAP( int, pPerm[i], pPerm[best_i] );
+    }
+}
 
 /**Function*************************************************************
 
@@ -697,13 +844,26 @@ int If_DsdManOperation2( If_DsdMan_t * p, int Type, int * pLits, int nLits )
   SeeAlso     []
 
 ***********************************************************************/
+int If_DsdManComputeFirstArray( If_DsdMan_t * p, int * pLits, int nLits, int * pFirsts )
+{
+    int i, nSSize = 0;
+    for ( i = 0; i < nLits; i++ )
+    {
+        pFirsts[i] = nSSize;
+        nSSize += If_DsdVecLitSuppSize(p->vObjs, pLits[i]);
+    }
+    return nSSize;
+}
+int If_DsdManComputeFirst( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pFirsts )
+{
+    return If_DsdManComputeFirstArray( p, pObj->pFans, pObj->nFans, pFirsts );
+}
 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;
-//    abctime clk;
     if ( Type == IF_DSD_AND )
     {
         for ( k = 0; k < nLits; k++ )
@@ -813,11 +973,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig
         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]);
-        }
+        nSSize = If_DsdManComputeFirstArray( p, pLits, nLits, pFirsts );
         for ( j = i = 0; i < nLits; i++ )
         {
             int iLitNew = Abc_LitNotCond( pLits[(int)pCanonPerm[i]], ((uCanonPhase>>i)&1) );
@@ -873,7 +1029,6 @@ int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * p
         fCompl = 1;
         (*p)++;
     }
-//    assert( !((**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9')) );
     if ( **p >= 'a' && **p <= 'z' ) // var
     {
         pPerm[(*pnSupp)++] = Abc_Var2Lit( **p - 'a', fCompl );
@@ -952,6 +1107,23 @@ int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char
   SeeAlso     []
 
 ***********************************************************************/
+// create signature of the support of the node
+unsigned If_DsdSign_rec( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pnSupp )
+{
+    unsigned uSign = 0; int i;
+    If_DsdObj_t * pFanin;
+    if ( If_DsdObjType(pObj) == IF_DSD_VAR )
+        return (1 << (2*(*pnSupp)++));
+    If_DsdObjForEachFanin( p->vObjs, pObj, pFanin, i )
+        uSign |= If_DsdSign_rec( p, pFanin, pnSupp );
+    return uSign;
+}
+unsigned If_DsdSign( If_DsdMan_t * p, If_DsdObj_t * pObj, int iFan, int iFirst, int fShared )
+{
+    If_DsdObj_t * pFanin = If_DsdObjFanin( p->vObjs, pObj, iFan );
+    unsigned uSign = If_DsdSign_rec( p, pFanin, &iFirst );
+    return fShared ? (uSign << 1) | uSign : uSign;
+}
 // collect supports of the node
 void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes )
 {
@@ -960,10 +1132,10 @@ void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes )
         pSSizes[i] = If_DsdObjSuppSize(pFanin);    
 }
 // checks if there is a way to package some fanins 
-int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose )
+unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
 {
     int i[6], LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
-    int nFans = If_DsdObjFaninNum(pObj);
+    int nFans = If_DsdObjFaninNum(pObj), pFirsts[DAU_MAX_VAR];
     assert( pObj->nFans > 2 );
     assert( If_DsdObjSuppSize(pObj) > LutSize );
     If_DsdManGetSuppSizes( p, pObj, pSSizes );
@@ -976,7 +1148,10 @@ int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int
         SizeOut = pObj->nSupp - SizeIn;
         if ( SizeIn > LutSize || SizeOut > LimitOut )
             continue;
-        return (1 << i[0]) | (1 << i[1]);
+        if ( !fDerive )
+            return ~0;
+        If_DsdManComputeFirst( p, pObj, pFirsts );
+        return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0);
     }
     if ( pObj->nFans == 3 )
         return 0;
@@ -988,7 +1163,10 @@ int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int
         SizeOut = pObj->nSupp - SizeIn;
         if ( SizeIn > LutSize || SizeOut > LimitOut )
             continue;
-        return (1 << i[0]) | (1 << i[1]) | (1 << i[2]);
+        if ( !fDerive )
+            return ~0;
+        If_DsdManComputeFirst( p, pObj, pFirsts );
+        return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0) | If_DsdSign(p, pObj, i[2], pFirsts[i[2]], 0);
     }
     if ( pObj->nFans == 4 )
         return 0;
@@ -1001,14 +1179,17 @@ int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int
         SizeOut = pObj->nSupp - SizeIn;
         if ( SizeIn > LutSize || SizeOut > LimitOut )
             continue;
-        return (1 << i[0]) | (1 << i[1]) | (1 << i[2]) | (1 << i[3]);
+        if ( !fDerive )
+            return ~0;
+        If_DsdManComputeFirst( p, pObj, pFirsts );
+        return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0) | If_DsdSign(p, pObj, i[2], pFirsts[i[2]], 0) | If_DsdSign(p, pObj, i[3], pFirsts[i[3]], 0);
     }
     return 0;
 }
 // checks if there is a way to package some fanins 
-int If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose )
+unsigned If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
 {
-    int LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
+    int LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR];
     assert( If_DsdObjFaninNum(pObj) == 3 );
     assert( If_DsdObjSuppSize(pObj) > LutSize );
     If_DsdManGetSuppSizes( p, pObj, pSSizes );
@@ -1019,21 +1200,27 @@ int If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int Lu
     SizeOut = pSSizes[2];
     if ( SizeIn <= LutSize && SizeOut <= LimitOut )
     {
-        return 1;
+        if ( !fDerive )
+            return ~0;
+        If_DsdManComputeFirst( p, pObj, pFirsts );
+        return If_DsdSign(p, pObj, 0, pFirsts[0], 1) | If_DsdSign(p, pObj, 1, pFirsts[1], 0);
     }
     // second input
     SizeIn = pSSizes[0] + pSSizes[2];
     SizeOut = pSSizes[1];
     if ( SizeIn <= LutSize && SizeOut <= LimitOut )
     {
-        return 1;
+        if ( !fDerive )
+            return ~0;
+        If_DsdManComputeFirst( p, pObj, pFirsts );
+        return If_DsdSign(p, pObj, 0, pFirsts[0], 1) | If_DsdSign(p, pObj, 2, pFirsts[2], 0);
     }
     return 0;
 }
 // checks if there is a way to package some fanins 
-int If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose )
+unsigned If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
 {
-    int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
+    int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR];
     int truthId = If_DsdObjTruthId( p, pObj );
     int nFans = If_DsdObjFaninNum(pObj);
     Vec_Int_t * vSets = (Vec_Int_t *)Vec_PtrEntry(p->vTtDecs, truthId);
@@ -1066,11 +1253,29 @@ Dau_DecPrintSets( vSets, nFans );
                 break;
         }
         if ( v == nFans )
-            return set;
+        {
+            unsigned uSign;
+            if ( !fDerive )
+                return ~0;
+            uSign = 0;
+            If_DsdManComputeFirst( p, pObj, pFirsts );
+            for ( v = 0; v < nFans; v++ )
+            {
+                int Value = ((set >> (v << 1)) & 3);
+                if ( Value == 0 )
+                {}
+                else if ( Value == 1 )
+                    uSign |= If_DsdSign(p, pObj, v, pFirsts[v], 0);
+                else if ( Value == 3 )
+                    uSign |= If_DsdSign(p, pObj, v, pFirsts[v], 1);
+                else assert( Value == 0 );
+            }
+            return uSign;
+        }
     }
     return 0;
 }
-int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose )
+unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose )
 {
     If_DsdObj_t * pObj, * pTemp; int i, Mask;
     pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) );
@@ -1080,7 +1285,7 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose )
     {
         if ( fVerbose )
         printf( "    Trivial\n" );
-        return 1;
+        return ~0;
     }
     If_DsdManCollect( p, pObj->Id, p->vNodes );
     If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
@@ -1090,12 +1295,12 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose )
             printf( "    Dec using node " );
             if ( fVerbose )
             If_DsdManPrintOne( stdout, p, pTemp->Id, NULL, 1 );
-            return 1;
+            return ~0;
         }
     If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
         if ( (If_DsdObjType(pTemp) == IF_DSD_AND || If_DsdObjType(pTemp) == IF_DSD_XOR) && If_DsdObjFaninNum(pTemp) > 2 && If_DsdObjSuppSize(pTemp) > LutSize )
         {
-            if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) )
+            if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
             {
                 if ( fVerbose )
                 printf( "    " );
@@ -1103,13 +1308,13 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose )
                 Abc_TtPrintBinary( (word *)&Mask, 4 ); 
                 if ( fVerbose )
                 printf( "    Using multi-input AND/XOR node\n" );
-                return 1;
+                return Mask;
             }
         }
     If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
         if ( If_DsdObjType(pTemp) == IF_DSD_MUX && If_DsdObjSuppSize(pTemp) > LutSize )
         {
-            if ( (Mask = If_DsdManCheckMux(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) )
+            if ( (Mask = If_DsdManCheckMux(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
             {
                 if ( fVerbose )
                 printf( "    " );
@@ -1117,13 +1322,13 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose )
                 Abc_TtPrintBinary( (word *)&Mask, 4 ); 
                 if ( fVerbose )
                 printf( "    Using multi-input MUX node\n" );
-                return 1;
+                return Mask;
             }
         }
     If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
         if ( If_DsdObjType(pTemp) == IF_DSD_PRIME && If_DsdObjSuppSize(pTemp) > LutSize )
         {
-            if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) )
+            if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
             {
                 if ( fVerbose )
                 printf( "    " );
@@ -1131,19 +1336,14 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose )
                 Dau_DecPrintSet( Mask, If_DsdObjFaninNum(pTemp), 0 );
                 if ( fVerbose )
                 printf( "    Using prime node\n" );
-                return 1;
+                return Mask;
             }
         }
     if ( fVerbose )
     printf( "    UNDEC\n" );
-
 //    If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
     return 0;
 }
-int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize ) 
-{
-    return 1;
-}
 
 /**Function*************************************************************
 
@@ -1156,9 +1356,9 @@ int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize )
   SeeAlso     []
 
 ***********************************************************************/
-int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd )
+unsigned If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose ) 
 {
-    return If_DsdVecObjMark( p->vObjs, Abc_Lit2Var(iDsd) );
+    return ~0;
 }
 
 /**Function*************************************************************
@@ -1183,17 +1383,6 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char
 clk = Abc_Clock();
     nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 1, pDsd );
 p->timeDsd += Abc_Clock() - clk;
-/*
-    if ( nLeaves <= 6 )
-    {
-        word pCopy2[DAU_MAX_WORD], t;
-        char pDsd2[DAU_MAX_STR];
-        Abc_TtCopy( pCopy2, pTruth, p->nWords, 0 );
-        nSizeNonDec = Dau_DsdDecompose( pCopy2, nLeaves, 0, 1, pDsd2 );
-        t = Dau_Dsd6ToTruth( pDsd2 );
-        assert( t == *pTruth );
-    }
-*/
 //    if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") )
 //    {
 //        int x = 0;
@@ -1217,18 +1406,9 @@ p->timeVerify += Abc_Clock() - clk;
         printf( "%s\n", pDsd );
         Dau_DsdPrintFromTruth( pTruth, nLeaves );
         Dau_DsdPrintFromTruth( pRes, nLeaves );
-//        Kit_DsdPrintFromTruth( (unsigned *)pTruth, nLeaves ); printf( "\n" );
-//        Kit_DsdPrintFromTruth( (unsigned *)pRes, nLeaves ); printf( "\n" );
         If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm, 1 );
         printf( "\n" );
     }
-    if ( pLutStruct && If_DsdVecObjRef(p->vObjs, Abc_Lit2Var(iDsd)) )
-    {
-        int LutSize = (int)(pLutStruct[0] - '0');
-        assert( pLutStruct[2] == 0 ); // XY
-        if ( !If_DsdManCheckXY( p, iDsd, LutSize, 0 ) )
-            If_DsdVecObjSetMark( p->vObjs, Abc_Lit2Var(iDsd) );
-    }
     If_DsdVecObjIncRef( p->vObjs, Abc_Lit2Var(iDsd) );
     return iDsd;
 }
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index d03fc200..686af7ae 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -85,7 +85,6 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
     p->puTempW   = p->pPars->fTruth? ABC_ALLOC( word, p->nTruth6Words ) : NULL;
     if ( pPars->fUseDsd )
     {
-        p->pIfDsdMan = If_DsdManAlloc( pPars->nLutSize );
         p->vTtDsds = Vec_IntAlloc( 1000 );
         Vec_IntPush( p->vTtDsds, 0 );
         Vec_IntPush( p->vTtDsds, 2 );
@@ -142,6 +141,15 @@ void If_ManRestart( If_Man_t * p )
 ***********************************************************************/
 void If_ManStop( If_Man_t * p )
 {
+/*
+    if ( p->pIfDsdMan )
+    {
+        If_DsdMan_t * pNew;
+        If_DsdManSave( p->pIfDsdMan, NULL );
+        pNew = If_DsdManLoad( If_DsdManFileName(p->pIfDsdMan) );
+        If_DsdManFree( pNew, 1 );
+    }
+*/
     {
 //        extern void If_CluHashFindMedian( If_Man_t * p );
 //        extern void If_CluHashTableCheck( If_Man_t * p );
@@ -158,11 +166,13 @@ void If_ManStop( If_Man_t * p )
                 Abc_Print( 1, "Useless cuts %2d  = %9d  (out of %9d)  (%6.2f %%)\n", i, p->nCutsUseless[i], p->nCutsCount[i], 100.0*p->nCutsUseless[i]/(p->nCutsCount[i]+1) );
         Abc_Print( 1, "Useless cuts all = %9d  (out of %9d)  (%6.2f %%)\n", p->nCutsUselessAll, p->nCutsCountAll, 100.0*p->nCutsUselessAll/(p->nCutsCountAll+1) );
     }
-    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_DsdManFree( p->pIfDsdMan, p->pPars->fVerbose );
-    if ( p->pPars->fUseDsd )
+//    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_DsdManFree( p->pIfDsdMan, p->pPars->fVerbose );
+    if ( p->pIfDsdMan )
+        p->pIfDsdMan = NULL;
+    if ( p->pPars->fUseDsd && (p->nCountNonDec[0] || p->nCountNonDec[1]) )
         printf( "NonDec0 = %d.  NonDec1 = %d.\n", p->nCountNonDec[0], p->nCountNonDec[1] );
 //    Abc_PrintTime( 1, "Truth", p->timeTruth );
 //    Abc_Print( 1, "Small support = %d.\n", p->nSmallSupp );
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index d7b7f4cc..5c23c1b6 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -217,12 +217,39 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
 //            abctime clk = Abc_Clock();
             If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
 //            p->timeTruth += Abc_Clock() - clk;
+            if ( p->pPars->fUseDsd )
+            {
+                int truthId = Abc_Lit2Var(pCut->iCutFunc);
+                if ( Vec_IntSize(p->vTtDsds) <= truthId || Vec_IntEntry(p->vTtDsds, truthId) == -1 )
+                {
+                    pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct );
+//                    printf( "%d(%d) ", pCut->iCutDsd, If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ) );
+                    while ( Vec_IntSize(p->vTtDsds) <= truthId )
+                    {
+                        Vec_IntPush( p->vTtDsds, -1 );
+                        for ( v = 0; v < p->pPars->nLutSize; v++ )
+                            Vec_StrPush( p->vTtPerms, IF_BIG_CHAR );
+                    }
+                    Vec_IntWriteEntry( p->vTtDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) );
+                    for ( v = 0; v < (int)pCut->nLeaves; v++ )
+                        Vec_StrWriteEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v, (char)pCut->pPerm[v] );
+                }
+                else
+                {
+                    pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) );
+                    for ( v = 0; v < (int)pCut->nLeaves; v++ )
+                        pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v );
+                }
+            }
             // run user functions
             pCut->fUseless = 0;
             if ( p->pPars->pFuncCell )
             {
                 assert( pCut->nLimit >= 4 && pCut->nLimit <= 16 );
-                pCut->fUseless = !p->pPars->pFuncCell( p, If_CutTruth(p, pCut), pCut->nLimit, pCut->nLeaves, p->pPars->pLutStruct );
+                if ( p->pPars->fUseDsd )
+                    pCut->fUseless = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd );
+                else
+                    pCut->fUseless = !p->pPars->pFuncCell( p, If_CutTruth(p, pCut), pCut->nLimit, pCut->nLeaves, p->pPars->pLutStruct );
                 p->nCutsUselessAll += pCut->fUseless;
                 p->nCutsUseless[pCut->nLeaves] += pCut->fUseless;
                 p->nCutsCountAll++;
@@ -251,29 +278,9 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                         p->nCuts5a++;
                 }
             }
+/*
             if ( p->pPars->fUseDsd )
             {
-                int truthId = Abc_Lit2Var(pCut->iCutFunc);
-                if ( Vec_IntSize(p->vTtDsds) <= truthId || Vec_IntEntry(p->vTtDsds, truthId) == -1 )
-                {
-                    pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct );
-//                    printf( "%d(%d) ", pCut->iCutDsd, If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ) );
-                    while ( Vec_IntSize(p->vTtDsds) <= truthId )
-                    {
-                        Vec_IntPush( p->vTtDsds, -1 );
-                        for ( v = 0; v < p->pPars->nLutSize; v++ )
-                            Vec_StrPush( p->vTtPerms, IF_BIG_CHAR );
-                    }
-                    Vec_IntWriteEntry( p->vTtDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) );
-                    for ( v = 0; v < (int)pCut->nLeaves; v++ )
-                        Vec_StrWriteEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v, (char)pCut->pPerm[v] );
-                }
-                else
-                {
-                    pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) );
-                    for ( v = 0; v < (int)pCut->nLeaves; v++ )
-                        pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v );
-                }
                 if ( p->pPars->pLutStruct )
                 {
                     int Value = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd );
@@ -283,7 +290,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                             p->nCountNonDec[0]++;
                         if ( !pCut->fUseless && Value )
                             p->nCountNonDec[1]++; 
-/*
+
 //                        if ( pCut->fUseless && !Value )
 //                            printf( "Old does not work.  New works.\n" );
                         if ( !pCut->fUseless && Value )
@@ -307,14 +314,14 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                             z = If_Dec6Perform( t, 1 );
                             If_DecPrintConfig( z );
 
-                            s = If_DsdManCheckXY( p->pIfDsdMan, pCut->iCutDsd, 4, 1 );
+                            s = If_DsdManCheckXY( p->pIfDsdMan, pCut->iCutDsd, 4, 0, 1 );
                             printf( "Confirm %d\n", s );
                             s = 0;
                         }
-*/
                     }
                 }
             }
+*/
         }
         
         // compute the application-specific cost and depth
diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c
index 5ddb8241..3fec34e0 100644
--- a/src/map/if/ifSat.c
+++ b/src/map/if/ifSat.c
@@ -204,46 +204,46 @@ void If_ManSatTest()
     
     uSet = (3 << 0) | (1 << 2) | (1 << 4);
     RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
-    printf( "%d", RetValue );
+    printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
     uSet = (1 << 0) | (3 << 2) | (1 << 4);
     RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
-    printf( "%d", RetValue );
+    printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
     uSet = (1 << 0) | (1 << 2) | (3 << 4);
     RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
-    printf( "%d", RetValue );
+    printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
 
     
     uSet = (3 << 0) | (1 << 2) | (1 << 6);
     RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
-    printf( "%d", RetValue );
+    printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
     uSet = (1 << 0) | (3 << 2) | (1 << 6);
     RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
-    printf( "%d", RetValue );
+    printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
     uSet = (1 << 0) | (1 << 2) | (3 << 6);
     RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
-    printf( "%d", RetValue );
+    printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
 
     
     uSet = (3 << 0) | (1 << 4) | (1 << 6);
     RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
-    printf( "%d", RetValue );
+    printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
     uSet = (1 << 0) | (3 << 4) | (1 << 6);
     RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
-    printf( "%d", RetValue );
+    printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
     uSet = (1 << 0) | (1 << 4) | (3 << 6);
     RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
-    printf( "%d", RetValue );
+    printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
 
     
     uSet = (3 << 2) | (1 << 4) | (1 << 6);
     RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
-    printf( "%d", RetValue );
+    printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
     uSet = (1 << 2) | (3 << 4) | (1 << 6);
     RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
-    printf( "%d", RetValue );
+    printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
     uSet = (1 << 2) | (1 << 4) | (3 << 6);
     RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
-    printf( "%d", RetValue );
+    printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
 
     printf( "\n" );