Improvements to DSD manager.

1 files changed, 226 insertions, 136 deletions

diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index 4ea4f83d..5c7d7f4e 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -22,6 +22,7 @@
 #include "if.h"
 #include "misc/extra/extra.h"
 #include "sat/bsat/satSolver.h"
+#include "aig/gia/gia.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -64,13 +65,16 @@ struct If_DsdMan_t_
     Mem_Flex_t *   pMem;           // memory for nodes
     Vec_Ptr_t *    vObjs;          // objects
     Vec_Int_t *    vNexts;         // next pointers
+    Vec_Int_t *    vTruths;        // truth IDs of prime nodes
     Vec_Int_t *    vTemp1;         // temp
     Vec_Int_t *    vTemp2;         // temp
     word **        pTtElems;       // elementary TTs
-    Vec_Mem_t *    vTtMem;         // truth table memory and hash table
-    Vec_Ptr_t *    vTtDecs;        // truth table decompositions
+    Vec_Mem_t *    vTtMem[IF_MAX_FUNC_LUTSIZE+1];  // truth table memory and hash table
+    Vec_Ptr_t *    vTtDecs[IF_MAX_FUNC_LUTSIZE+1]; // truth table decompositions
+    int *          pSched[IF_MAX_FUNC_LUTSIZE];    // grey code schedules
+    Gia_Man_t *    pTtGia;         // GIA to represent truth tables
+    Vec_Int_t *    vCover;         // temporary memory
     void *         pSat;           // SAT solver
-    int *          pSched[16];     // grey code schedules
     int            nUniqueHits;    // statistics
     int            nUniqueMisses;  // statistics
     abctime        timeDsd;        // statistics
@@ -81,9 +85,9 @@ struct If_DsdMan_t_
 };
 
 static inline int           If_DsdObjWordNum( int nFans )                                    { return sizeof(If_DsdObj_t) / 8 + nFans / 2 + ((nFans & 1) > 0);              }
-static inline int           If_DsdObjTruthId( If_DsdObj_t * pObj )                           { return pObj->Type == IF_DSD_PRIME ? pObj->pFans[pObj->nFans] : -1;           }
-static inline word *        If_DsdObjTruth( If_DsdMan_t * p, If_DsdObj_t * pObj )            { return Vec_MemReadEntry(p->vTtMem, If_DsdObjTruthId(pObj));                  }
-static inline void          If_DsdObjSetTruth( If_DsdMan_t * p, If_DsdObj_t * pObj, int Id ) { assert( pObj->Type == IF_DSD_PRIME && pObj->nFans > 2 ); pObj->pFans[pObj->nFans] = Id;                    }
+static inline int           If_DsdObjTruthId( If_DsdMan_t * p, If_DsdObj_t * pObj )          { return (pObj->Type == IF_DSD_PRIME && pObj->nFans > 2) ? Vec_IntEntry(p->vTruths, pObj->Id) : -1;     }
+static inline word *        If_DsdObjTruth( If_DsdMan_t * p, If_DsdObj_t * pObj )            { return Vec_MemReadEntry(p->vTtMem[pObj->nFans], If_DsdObjTruthId(p, pObj));  }
+static inline void          If_DsdObjSetTruth( If_DsdMan_t * p, If_DsdObj_t * pObj, int Id ) { assert( pObj->Type == IF_DSD_PRIME && pObj->nFans > 2 ); Vec_IntWriteEntry(p->vTruths, pObj->Id, Id); }
 
 static inline void          If_DsdObjClean( If_DsdObj_t * pObj )                       { memset( pObj, 0, sizeof(If_DsdObj_t) );                                            }
 static inline int           If_DsdObjId( If_DsdObj_t * pObj )                          { return pObj->Id;                                                                   }
@@ -117,6 +121,8 @@ static inline void          If_DsdVecObjClearMark( Vec_Ptr_t * p, int iObj )
 #define If_DsdObjForEachFaninLit( vVec, pObj, iLit, i )      \
     for ( i = 0; (i < If_DsdObjFaninNum(pObj)) && ((iLit) = If_DsdObjFaninLit(pObj, i)); i++ )
 
+extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -174,7 +180,7 @@ static inline word ** If_ManDsdTtElems()
 }
 If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans )
 {
-    int nWords = If_DsdObjWordNum( nFans + (int)(Type == DAU_DSD_PRIME) );
+    int nWords = If_DsdObjWordNum( nFans );
     If_DsdObj_t * pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords );
     If_DsdObjClean( pObj );
     pObj->Type   = Type;
@@ -184,7 +190,9 @@ If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans )
     pObj->Count  = 0;
     Vec_PtrPush( p->vObjs, pObj );
     Vec_IntPush( p->vNexts, 0 );
+    Vec_IntPush( p->vTruths, -1 );
     assert( Vec_IntSize(p->vNexts) == Vec_PtrSize(p->vObjs) );
+    assert( Vec_IntSize(p->vTruths) == Vec_PtrSize(p->vObjs) );
     return pObj;
 }
 If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
@@ -202,14 +210,25 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
     p->pMem    = Mem_FlexStart();
     p->vObjs   = Vec_PtrAlloc( 10000 );
     p->vNexts  = Vec_IntAlloc( 10000 );
+    p->vTruths = Vec_IntAlloc( 10000 );
     If_DsdObjAlloc( p, IF_DSD_CONST0, 0 );
     If_DsdObjAlloc( p, IF_DSD_VAR, 0 )->nSupp = 1;
     p->vTemp1   = Vec_IntAlloc( 32 );
     p->vTemp2   = Vec_IntAlloc( 32 );
     p->pTtElems = If_ManDsdTtElems();
-    p->vTtDecs  = Vec_PtrAlloc( 1000 );
-    p->vTtMem   = Vec_MemAlloc( Abc_TtWordNum(nVars), 12 );
-    Vec_MemHashAlloc( p->vTtMem, 10000 );
+    for ( v = 3; v <= nVars; v++ )
+    {
+        p->vTtMem[v] = Vec_MemAlloc( Abc_TtWordNum(v), 12 );
+        Vec_MemHashAlloc( p->vTtMem[v], 10000 );
+        p->vTtDecs[v] = Vec_PtrAlloc( 1000 );
+    }
+/*
+    p->pTtGia   = Gia_ManStart( nVars );
+    Gia_ManHashAlloc( p->pTtGia );
+    for ( v = 0; v < nVars; v++ )
+        Gia_ManAppendCi( p->pTtGia );
+    p->vCover   = Vec_IntAlloc( 0 );
+*/
     for ( v = 2; v < nVars; v++ )
         p->pSched[v] = Extra_GreyCodeSchedule( v );
     if ( LutSize )
@@ -223,17 +242,30 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
     if ( fVerbose )
         If_DsdManPrint( p, NULL, 0, 0, 0, 0, 0 );
     if ( fVerbose )
-        Vec_MemDumpTruthTables( p->vTtMem, "dumpdsd", p->nVars );
+    {
+        char FileName[10];
+        for ( v = 3; v <= p->nVars; v++ )
+        {
+            sprintf( FileName, "dumpdsd%02d", v );
+            Vec_MemDumpTruthTables( p->vTtMem[v], FileName, v );
+        }
+    }
     for ( v = 2; v < p->nVars; v++ )
         ABC_FREE( p->pSched[v] );
-    Vec_VecFree( (Vec_Vec_t *)p->vTtDecs );
-    Vec_MemHashFree( p->vTtMem );
-    Vec_MemFreeP( &p->vTtMem );
+    for ( v = 3; v <= p->nVars; v++ )
+    {
+        Vec_MemHashFree( p->vTtMem[v] );
+        Vec_MemFree( p->vTtMem[v] );
+        Vec_VecFree( (Vec_Vec_t *)(p->vTtDecs[v]) );
+    }
     Vec_IntFreeP( &p->vTemp1 );
     Vec_IntFreeP( &p->vTemp2 );
     Vec_IntFreeP( &p->vNexts );
+    Vec_IntFreeP( &p->vTruths );
     Vec_PtrFreeP( &p->vObjs );
     Mem_FlexStop( p->pMem, 0 );
+    Gia_ManStopP( &p->pTtGia );
+    Vec_IntFreeP( &p->vCover );
     If_ManSatUnbuild( p->pSat );
     ABC_FREE( p->pStore );
     ABC_FREE( p->pBins );
@@ -242,31 +274,35 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
 void If_DsdManDumpDsd( If_DsdMan_t * p, int Support )
 {
     char * pFileName = "tts_nondsd.txt";
-    If_DsdObj_t * pObj; int i;
+    If_DsdObj_t * pObj; 
     Vec_Int_t * vMap;
     FILE * pFile = fopen( pFileName, "wb" );
+    int v, i;
     if ( pFile == NULL )
     {
         printf( "Cannot open file \"%s\".\n", pFileName );
         return;
     }
-    vMap = Vec_IntStart( Vec_MemEntryNum(p->vTtMem) );
-    If_DsdVecForEachObj( p->vObjs, pObj, i )
+    for ( v = 3; v <= p->nVars; v++ )
     {
-        if ( Support && Support != If_DsdObjSuppSize(pObj) )
-            continue;
-        if ( If_DsdObjType(pObj) != IF_DSD_PRIME )
-            continue;
-        if ( Vec_IntEntry(vMap, If_DsdObjTruthId(pObj)) )
-            continue;
-        Vec_IntWriteEntry(vMap, If_DsdObjTruthId(pObj), 1);
-        fprintf( pFile, "0x" );
-        Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), Support ? Abc_MaxInt(Support, 6) : p->nVars );
-        fprintf( pFile, "\n" );
-//        printf( "    " );
-//        Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars );
+        vMap = Vec_IntStart( Vec_MemEntryNum(p->vTtMem[v]) );
+        If_DsdVecForEachObj( p->vObjs, pObj, i )
+        {
+            if ( Support && Support != If_DsdObjSuppSize(pObj) )
+                continue;
+            if ( If_DsdObjType(pObj) != IF_DSD_PRIME )
+                continue;
+            if ( Vec_IntEntry(vMap, If_DsdObjTruthId(p, pObj)) )
+                continue;
+            Vec_IntWriteEntry(vMap, If_DsdObjTruthId(p, pObj), 1);
+            fprintf( pFile, "0x" );
+            Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), Support ? Abc_MaxInt(Support, 6) : v );
+            fprintf( pFile, "\n" );
+            //printf( "    " );
+            //Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars );
+        }
+        Vec_IntFree( vMap );
     }
-    Vec_IntFree( vMap );
     fclose( pFile );
 }
 void If_DsdManDumpAll( If_DsdMan_t * p, int Support )
@@ -378,38 +414,41 @@ void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char
 void If_DsdManPrintDecs( FILE * pFile, If_DsdMan_t * p )
 {
     Vec_Int_t * vDecs;
-    int i, k, nSuppSize, nDecMax = 0;
+    int i, k, v, nSuppSize, nDecMax = 0;
     int pDecMax[IF_MAX_FUNC_LUTSIZE] = {0};
     int pCountsAll[IF_MAX_FUNC_LUTSIZE] = {0};
     int pCountsSSizes[IF_MAX_FUNC_LUTSIZE] = {0};
     int pCounts[IF_MAX_FUNC_LUTSIZE][DSD_ARRAY_LIMIT+2] = {{0}};
     word * pTruth;
-    assert( Vec_MemEntryNum(p->vTtMem) == Vec_PtrSize(p->vTtDecs) );
-    // find max number of decompositions
-    Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs, vDecs, i )
-    {
-        pTruth = Vec_MemReadEntry( p->vTtMem, i );
-        nSuppSize = Abc_TtSupportSize( pTruth, p->nVars );
-        pDecMax[nSuppSize] = Abc_MaxInt( pDecMax[nSuppSize], Vec_IntSize(vDecs) );
-        nDecMax = Abc_MaxInt( nDecMax, Vec_IntSize(vDecs) );
-    }
-    // fill up
-    Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs, vDecs, i )
-    {
-        pTruth = Vec_MemReadEntry( p->vTtMem, i );
-        nSuppSize = Abc_TtSupportSize( pTruth, p->nVars );
-        pCountsAll[nSuppSize]++;
-        pCountsSSizes[nSuppSize] += Vec_IntSize(vDecs);
-        pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs))]++;
-//        pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs)?1+(Vec_IntSize(vDecs)/10):0)]++;
-/*
-        if ( nSuppSize == 6 && Vec_IntSize(vDecs) == pDecMax[6] )
+    for ( v = 3; v <= p->nVars; v++ )
+    {
+        assert( Vec_MemEntryNum(p->vTtMem[v]) == Vec_PtrSize(p->vTtDecs[v]) );
+        // find max number of decompositions
+        Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs[v], vDecs, i )
         {
-            fprintf( pFile, "0x" );
-            Abc_TtPrintHex( pTruth, nSuppSize );
-            Dau_DecPrintSets( vDecs, nSuppSize );
+            pTruth = Vec_MemReadEntry( p->vTtMem[v], i );
+            nSuppSize = Abc_TtSupportSize( pTruth, p->nVars );
+            pDecMax[nSuppSize] = Abc_MaxInt( pDecMax[nSuppSize], Vec_IntSize(vDecs) );
+            nDecMax = Abc_MaxInt( nDecMax, Vec_IntSize(vDecs) );
+        }
+        // fill up
+        Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs[v], vDecs, i )
+        {
+            pTruth = Vec_MemReadEntry( p->vTtMem[v], i );
+            nSuppSize = Abc_TtSupportSize( pTruth, p->nVars );
+            pCountsAll[nSuppSize]++;
+            pCountsSSizes[nSuppSize] += Vec_IntSize(vDecs);
+            pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs))]++;
+    //        pCounts[nSuppSize][Abc_MinInt(DSD_ARRAY_LIMIT+1,Vec_IntSize(vDecs)?1+(Vec_IntSize(vDecs)/10):0)]++;
+    /*
+            if ( nSuppSize == 6 && Vec_IntSize(vDecs) == pDecMax[6] )
+            {
+                fprintf( pFile, "0x" );
+                Abc_TtPrintHex( pTruth, nSuppSize );
+                Dau_DecPrintSets( vDecs, nSuppSize );
+            }
+    */
         }
-*/
     }
     // print header
     fprintf( pFile, " N :  " );
@@ -499,39 +538,64 @@ void If_DsdManPrintOccurs( FILE * pFile, If_DsdMan_t * p )
 
 void If_DsdManPrintDistrib( If_DsdMan_t * p )
 {
-    If_DsdObj_t * pObj;
-    int CountAll[IF_MAX_FUNC_LUTSIZE] = {0};
-    int CountNon[IF_MAX_FUNC_LUTSIZE] = {0};
-    int i, nVars, CountNonTotal = 0;
-    If_DsdVecForEachObj( p->vObjs, pObj, i )
+    If_DsdObj_t * pObj; int i;
+    int CountObj[IF_MAX_FUNC_LUTSIZE+2] = {0};
+    int CountObjNon[IF_MAX_FUNC_LUTSIZE+2] = {0};
+    int CountObjNpn[IF_MAX_FUNC_LUTSIZE+2] = {0};
+    int CountStr[IF_MAX_FUNC_LUTSIZE+2] = {0};
+    int CountStrNon[IF_MAX_FUNC_LUTSIZE+2] = {0};
+    int CountMarked[IF_MAX_FUNC_LUTSIZE+2] = {0};
+    for ( i = 3; i <= p->nVars; i++ )
     {
-        nVars = If_DsdObjSuppSize(pObj);
-        CountAll[nVars]++;
-        if ( !If_DsdVecObjMark(p->vObjs, i) )
-            continue;
-        CountNon[nVars]++;
-        CountNonTotal++;
+        CountObjNpn[i] = Vec_MemEntryNum(p->vTtMem[i]);
+        CountObjNpn[p->nVars+1] += Vec_MemEntryNum(p->vTtMem[i]);
     }
-    for ( i = 0; i <= p->nVars; i++ )
+    If_DsdVecForEachObj( p->vObjs, pObj, i )
+    {
+        CountObj[If_DsdObjFaninNum(pObj)]++,        CountObj[p->nVars+1]++;
+        if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
+            CountObjNon[If_DsdObjFaninNum(pObj)]++, CountObjNon[p->nVars+1]++;
+        CountStr[If_DsdObjSuppSize(pObj)]++,        CountStr[p->nVars+1]++;
+        if ( If_DsdManCheckNonDec_rec(p, i) )
+            CountStrNon[If_DsdObjSuppSize(pObj)]++, CountStrNon[p->nVars+1]++;
+        if ( If_DsdVecObjMark(p->vObjs, i) )
+            CountMarked[If_DsdObjSuppSize(pObj)]++, CountMarked[p->nVars+1]++;
+    }
+    printf( "***** DSD MANAGER STATISTICS *****\n" );
+    printf( "Support     " );
+    printf( "Obj   " );
+    printf( "ObjNDSD            " );
+    printf( "NPNNDSD                  " );
+    printf( "Str   " );
+    printf( "StrNDSD             " );
+    printf( "Marked  " );
+    printf( "\n" );
+    for ( i = 0; i <= p->nVars + 1; i++ )
     {
-        printf( "%3d :  ", i );
-        printf( "All = %8d  ", CountAll[i] );
-        printf( "Non = %8d  ", CountNon[i] );
-        printf( "(%6.2f %%)",  100.0 * CountNon[i] / CountAll[i] );
+        if ( i == p->nVars + 1 )
+            printf( "All : " );
+        else
+            printf( "%3d : ", i );
+        printf( "%9d ", CountObj[i] );
+        printf( "%9d ", CountObjNon[i] );
+        printf( "%6.2f %% ", 100.0 * CountObjNon[i] / Abc_MaxInt(1, CountObj[i]) );
+        printf( "%9d ", CountObjNpn[i] );
+        printf( "%6.2f %% ", 100.0 * CountObjNpn[i] / Abc_MaxInt(1, CountObj[i]) );
+        printf( "  " );
+        printf( "%9d ", CountStr[i] );
+        printf( "%9d ", CountStrNon[i] );
+        printf( "%6.2f %% ", 100.0 * CountStrNon[i] / Abc_MaxInt(1, CountStr[i]) );
+        printf( "%9d ", CountMarked[i] );
+        printf( "%6.2f %%",  100.0 * CountMarked[i] / Abc_MaxInt(1, CountStr[i]) );
         printf( "\n" );
     }
-    printf( "All :  " );
-    printf( "All = %8d  ", Vec_PtrSize(p->vObjs) );
-    printf( "Non = %8d  ", CountNonTotal );
-    printf( "(%6.2f %%)",  100.0 * CountNonTotal / Vec_PtrSize(p->vObjs) );
-    printf( "\n" );
 }
 void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, int fOccurs, int fTtDump, int fVerbose )
 {
     If_DsdObj_t * pObj;
     Vec_Int_t * vStructs, * vCounts;
-    int CountUsed = 0, CountNonDsdStr = 0, CountMarked = 0, CountPrime = 0;
-    int i, * pPerm, DsdMax = 0;
+    int CountUsed = 0, CountNonDsd = 0, CountNonDsdStr = 0, CountMarked = 0, CountPrime = 0;
+    int i, v, * pPerm, DsdMax = 0, MemSizeTTs = 0, MemSizeDecs = 0;
     FILE * pFile;
     pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
     if ( pFileName && pFile == NULL )
@@ -548,22 +612,24 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support,
         CountUsed += ( If_DsdVecObjRef(p->vObjs, pObj->Id) > 0 );
         CountMarked += If_DsdVecObjMark( p->vObjs, i );
     }
-    fprintf( pFile, "Total number of objects    = %8d\n", Vec_PtrSize(p->vObjs) );
-    fprintf( pFile, "Externally used objects    = %8d\n", CountUsed );
-    fprintf( pFile, "Non-DSD objects (max =%2d)  = %8d\n", DsdMax, Vec_MemEntryNum(p->vTtMem) );
-    fprintf( pFile, "Non-DSD structures         = %8d\n", CountNonDsdStr );
-    fprintf( pFile, "Prime objects              = %8d\n", CountPrime );
-    fprintf( pFile, "Marked objects             = %8d\n", CountMarked );
-    fprintf( pFile, "Unique table hits          = %8d\n", p->nUniqueHits );
+    for ( v = 3; v <= p->nVars; v++ )
+    {
+        CountNonDsd += Vec_MemEntryNum(p->vTtMem[v]);
+        MemSizeTTs += Vec_MemEntrySize(p->vTtMem[v]) * Vec_MemEntryNum(p->vTtMem[v]);
+        MemSizeDecs += (int)Vec_VecMemoryInt((Vec_Vec_t *)(p->vTtDecs[v]));
+    }
+    If_DsdManPrintDistrib( p );
+    if ( p->pTtGia )
+    fprintf( pFile, "Non-DSD AIG nodes          = %8d\n", Gia_ManAndNum(p->pTtGia) );
     fprintf( pFile, "Unique table misses        = %8d\n", p->nUniqueMisses );
+    fprintf( pFile, "Unique table hits          = %8d\n", p->nUniqueHits );
     fprintf( pFile, "Memory used for objects    = %8.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
-    fprintf( pFile, "Memory used for functions  = %8.2f MB.\n", 8.0*(Vec_MemEntrySize(p->vTtMem)+1)*Vec_MemEntryNum(p->vTtMem)/(1<<20) );
+    fprintf( pFile, "Memory used for functions  = %8.2f MB.\n", 8.0*(MemSizeTTs+sizeof(int)*Vec_IntCap(p->vTruths))/(1<<20) );
     fprintf( pFile, "Memory used for hash table = %8.2f MB.\n", 1.0*sizeof(int)*(p->nBins+Vec_IntCap(p->vNexts))/(1<<20) );
-    fprintf( pFile, "Memory used for bound sets = %8.2f MB.\n", (float)Vec_VecMemoryInt((Vec_Vec_t *)p->vTtDecs)/(1<<20) );
+    fprintf( pFile, "Memory used for bound sets = %8.2f MB.\n", 1.0*MemSizeDecs/(1<<20) );
     fprintf( pFile, "Memory used for array      = %8.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) );
-    If_DsdManPrintDistrib( p );
-    if ( fOccurs )
-        If_DsdManPrintOccurs( stdout, p );
+    if ( p->pTtGia )
+    fprintf( pFile, "Memory used for AIG        = %8.2f MB.\n", 8.0*Gia_ManAndNum(p->pTtGia)/(1<<20) );
     if ( p->timeDsd )
     {
         Abc_PrintTime( 1, "Time DSD   ", p->timeDsd    );
@@ -572,6 +638,8 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support,
         Abc_PrintTime( 1, "Time check2", p->timeCheck2 );
         Abc_PrintTime( 1, "Time verify", p->timeVerify );
     }
+    if ( fOccurs )
+        If_DsdManPrintOccurs( stdout, p );
 //    If_DsdManHashProfile( p );
     if ( fTtDump )
         If_DsdManDumpDsd( p, Support );
@@ -618,7 +686,7 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support,
   SeeAlso     []
 
 ***********************************************************************/
-int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 )
+int If_DsdObjCompare( If_DsdMan_t * pMan, 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));
@@ -635,14 +703,14 @@ int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 )
         return 1;
     if ( If_DsdObjType(p0) == IF_DSD_PRIME )
     {
-        if ( If_DsdObjTruthId(p0) < If_DsdObjTruthId(p1) )
+        if ( If_DsdObjTruthId(pMan, p0) < If_DsdObjTruthId(pMan, p1) )
             return -1;
-        if ( If_DsdObjTruthId(p0) > If_DsdObjTruthId(p1) )
+        if ( If_DsdObjTruthId(pMan, p0) > If_DsdObjTruthId(pMan, p1) )
             return 1;
     }
     for ( i = 0; i < If_DsdObjFaninNum(p0); i++ )
     {
-        Res = If_DsdObjCompare( p, If_DsdObjFaninLit(p0, i), If_DsdObjFaninLit(p1, i) );
+        Res = If_DsdObjCompare( pMan, p, If_DsdObjFaninLit(p0, i), If_DsdObjFaninLit(p1, i) );
         if ( Res != 0 )
             return Res;
     }
@@ -653,14 +721,14 @@ int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 )
     assert( iLit0 == iLit1 );
     return 0;
 }
-void If_DsdObjSort( Vec_Ptr_t * p, int * pLits, int nLits, int * pPerm )
+void If_DsdObjSort( If_DsdMan_t * pMan, 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 )
+            if ( If_DsdObjCompare(pMan, p, pLits[best_i], pLits[j]) == 1 )
                 best_i = j;
         if ( i == best_i )
             continue;
@@ -704,7 +772,7 @@ unsigned * If_DsdObjHashLookup( If_DsdMan_t * p, int Type, int * pLits, int nLit
         if ( If_DsdObjType(pObj) == Type && 
              If_DsdObjFaninNum(pObj) == nLits && 
              !memcmp(pObj->pFans, pLits, sizeof(int)*If_DsdObjFaninNum(pObj)) &&
-             truthId == If_DsdObjTruthId(pObj) )
+             truthId == If_DsdObjTruthId(p, pObj) )
         {
             p->nUniqueHits++;
             return pSpot;
@@ -724,7 +792,7 @@ static void If_DsdObjHashResize( If_DsdMan_t * p )
     Vec_IntFill( p->vNexts, Vec_PtrSize(p->vObjs), 0 );
     If_DsdVecForEachNode( p->vObjs, pObj, i )
     {
-        pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(pObj) );
+        pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(p, pObj) );
         assert( *pSpot == 0 );
         *pSpot = pObj->Id;
     }
@@ -748,7 +816,7 @@ int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int trut
             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 );
+            assert( iPrev == -1 || If_DsdObjCompare(p, p->vObjs, iPrev, pLits[i]) <= 0 );
             iPrev = pLits[i];
         }
     }
@@ -775,20 +843,26 @@ int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int trut
 }
 int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word * pTruth )
 {
-    int objId, truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem, pTruth) : -1;
+    int objId, truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem[nLits], pTruth) : -1;
     unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId );
 abctime clk;
     if ( *pSpot )
         return (int)*pSpot;
 clk = Abc_Clock();
-    if ( p->LutSize && truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs) )
+    if ( p->LutSize && truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs[nLits]) )
     {
         Vec_Int_t * vSets = Dau_DecFindSets_int( pTruth, nLits, p->pSched );
-//        printf( "%d ", Vec_IntSize(vSets) );
-        assert( truthId == Vec_MemEntryNum(p->vTtMem)-1 );
-        Vec_PtrPush( p->vTtDecs, vSets );
+        assert( truthId == Vec_MemEntryNum(p->vTtMem[nLits])-1 );
+        Vec_PtrPush( p->vTtDecs[nLits], vSets );
 //        Dau_DecPrintSets( vSets, nLits );
     }
+    if ( p->pTtGia && truthId >= 0 && truthId == Vec_MemEntryNum(p->vTtMem[nLits])-1 )
+    {
+        int nObjOld = Gia_ManAndNum(p->pTtGia);
+        int Lit = Kit_TruthToGia( p->pTtGia, (unsigned *)pTruth, nLits, p->vCover, NULL, 1 );
+//        printf( "%d ", Gia_ManAndNum(p->pTtGia)-nObjOld );
+        Gia_ManAppendCo( p->pTtGia, Lit );
+    }
 p->timeCheck += Abc_Clock() - clk;
     *pSpot = Vec_PtrSize( p->vObjs );
     objId = If_DsdObjCreate( p, Type, pLits, nLits, truthId );
@@ -815,7 +889,7 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName )
     Vec_Int_t * vSets;
     char * pBuffer = "dsd0";
     word * pTruth; 
-    int i, Num;
+    int i, v, Num;
     FILE * pFile = fopen( pFileName ? pFileName : p->pStore, "wb" );
     if ( pFile == NULL )
     {
@@ -831,21 +905,27 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName )
     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) );
+        Num = If_DsdObjWordNum( pObj->nFans );
         fwrite( &Num, 4, 1, pFile );
         fwrite( pObj, sizeof(word)*Num, 1, pFile );
+        if ( pObj->Type == IF_DSD_PRIME )
+            fwrite( Vec_IntEntryP(p->vTruths, i), 4, 1, pFile );
     }
-    Num = Vec_MemEntryNum(p->vTtMem);
-    fwrite( &Num, 4, 1, pFile );
-    Vec_MemForEachEntry( p->vTtMem, pTruth, i )
-        fwrite( pTruth, sizeof(word)*p->nWords, 1, pFile );
-    Num = Vec_PtrSize(p->vTtDecs);
-    fwrite( &Num, 4, 1, pFile );
-    Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs, vSets, i )
+    for ( v = 3; v <= p->nVars; v++ )
     {
-        Num = Vec_IntSize(vSets);
+        int nBytes = sizeof(word)*Vec_MemEntrySize(p->vTtMem[v]);
+        Num = Vec_MemEntryNum(p->vTtMem[v]);
+        fwrite( &Num, 4, 1, pFile );
+        Vec_MemForEachEntry( p->vTtMem[v], pTruth, i )
+            fwrite( pTruth, nBytes, 1, pFile );
+        Num = Vec_PtrSize(p->vTtDecs[v]);
         fwrite( &Num, 4, 1, pFile );
-        fwrite( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
+        Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs[v], vSets, i )
+        {
+            Num = Vec_IntSize(vSets);
+            fwrite( &Num, 4, 1, pFile );
+            fwrite( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
+        }
     }
     fclose( pFile );
 }
@@ -857,7 +937,7 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
     char pBuffer[10];
     unsigned * pSpot;
     word * pTruth;
-    int i, Num, Num2, RetValue;
+    int i, v, Num, Num2, RetValue;
     FILE * pFile = fopen( pFileName, "rb" );
     if ( pFile == NULL )
     {
@@ -881,6 +961,7 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
     assert( Num >= 2 );
     Vec_PtrFillExtra( p->vObjs, Num, NULL );
     Vec_IntFill( p->vNexts, Num, 0 );
+    Vec_IntFill( p->vTruths, Num, -1 );
     p->nBins = Abc_PrimeCudd( 2*Num );
     p->pBins = ABC_REALLOC( unsigned, p->pBins, p->nBins );
     memset( p->pBins, 0, sizeof(unsigned) * p->nBins );
@@ -890,31 +971,40 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
         pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * Num );
         RetValue = fread( pObj, sizeof(word)*Num, 1, pFile );
         Vec_PtrWriteEntry( p->vObjs, i, pObj );
-        pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(pObj) );
+        if ( pObj->Type == IF_DSD_PRIME )
+        {
+            RetValue = fread( &Num, 4, 1, pFile );
+            Vec_IntWriteEntry( p->vTruths, i, Num );
+        }
+        pSpot = If_DsdObjHashLookup( p, pObj->Type, (int *)pObj->pFans, pObj->nFans, If_DsdObjTruthId(p, pObj) );
         assert( *pSpot == 0 );
         *pSpot = pObj->Id;
     }
     assert( p->nUniqueMisses == Vec_PtrSize(p->vObjs) - 2 );
     p->nUniqueMisses = 0;
-    RetValue = fread( &Num, 4, 1, pFile );
     pTruth = ABC_ALLOC( word, p->nWords );
-    for ( i = 0; i < Num; i++ )
-    {
-        RetValue = fread( pTruth, sizeof(word)*p->nWords, 1, pFile );
-        Vec_MemHashInsert( p->vTtMem, pTruth );
-    }
-    ABC_FREE( pTruth );
-    assert( Num == Vec_MemEntryNum(p->vTtMem) );
-    RetValue = fread( &Num2, 4, 1, pFile );
-    for ( i = 0; i < Num2; i++ )
+    for ( v = 3; v <= p->nVars; v++ )
     {
+        int nBytes = sizeof(word)*Vec_MemEntrySize(p->vTtMem[v]);
         RetValue = fread( &Num, 4, 1, pFile );
-        vSets = Vec_IntAlloc( Num );
-        RetValue = fread( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
-        vSets->nSize = Num;
-        Vec_PtrPush( p->vTtDecs, vSets );
+        for ( i = 0; i < Num; i++ )
+        {
+            RetValue = fread( pTruth, nBytes, 1, pFile );
+            Vec_MemHashInsert( p->vTtMem[v], pTruth );
+        }
+        assert( Num == Vec_MemEntryNum(p->vTtMem[v]) );
+        RetValue = fread( &Num2, 4, 1, pFile );
+        for ( i = 0; i < Num2; i++ )
+        {
+            RetValue = fread( &Num, 4, 1, pFile );
+            vSets = Vec_IntAlloc( Num );
+            RetValue = fread( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
+            vSets->nSize = Num;
+            Vec_PtrPush( p->vTtDecs[v], vSets );
+        }
+        assert( Num2 == Vec_PtrSize(p->vTtDecs[v]) ); 
     }
-    assert( Num2 == Vec_PtrSize(p->vTtDecs) ); 
+    ABC_FREE( pTruth );
     fclose( pFile );
     return p;
 }
@@ -1203,7 +1293,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig
             }
             pPermStart += If_DsdObjSuppSize(pObj);
         }
-        If_DsdObjSort( p->vObjs, pChildren, nChildren, pBegEnd );
+        If_DsdObjSort( p, p->vObjs, pChildren, nChildren, pBegEnd );
         // create permutation
         for ( j = i = 0; i < nChildren; i++ )
             for ( k = (pBegEnd[i] >> 16); k < (pBegEnd[i] & 0xFF); k++ )
@@ -1222,7 +1312,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig
             pLits[k] = Abc_LitNotCond( pLits[k], If_DsdManPushInv(p, pLits[k], pPermStart) );
             pPermStart += pFanin->nSupp;
         }
-        RetValue = If_DsdObjCompare( p->vObjs, pLits[1], pLits[2] );
+        RetValue = If_DsdObjCompare( p, p->vObjs, pLits[1], pLits[2] );
         if ( RetValue == 1 || (RetValue == 0 && Abc_LitIsCompl(pLits[0])) )
         {
             int nSupp0 = If_DsdVecLitSuppSize( p->vObjs, pLits[0] );
@@ -1513,9 +1603,9 @@ unsigned If_DsdManCheckMux( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int
 unsigned If_DsdManCheckPrime( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
 {
     int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR];
-    int truthId = If_DsdObjTruthId(pObj);
+    int truthId = If_DsdObjTruthId(p, pObj);
     int nFans = If_DsdObjFaninNum(pObj);
-    Vec_Int_t * vSets = (Vec_Int_t *)Vec_PtrEntry(p->vTtDecs, truthId);
+    Vec_Int_t * vSets = (Vec_Int_t *)Vec_PtrEntry(p->vTtDecs[pObj->nFans], truthId);
 if ( fVerbose )
 printf( "\n" );
 if ( fVerbose )