Version abc70407

13 files changed, 1014 insertions, 209 deletions

diff --git a/abc.rc b/abc.rc
index 16c03c65..3d033934 100644
--- a/abc.rc
+++ b/abc.rc
@@ -141,9 +141,6 @@ alias qsA      "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar
 alias chnew    "st; haig_start; resyn2; haig_use"
 alias chnewrs  "st; haig_start; resyn2rs; haig_use"
 
-alias bug      "r a/quip_opt/nut_001_opt.blif; chnew; st; cec"
-alias bug2     "r a/quip_opt/nut_001_opt.blif; chnew; if -K 6; ps; cec"
-
 alias t        "read_dsd a*(b+(c*d)+e); clp -r; print_dsd"
 alias t1       "read_dsd a*(b+(c*d)); clp -r; print_dsd"
 alias t2       "read_dsd 56BA(a,b,c,d); clp -r; print_dsd"
@@ -168,3 +165,4 @@ alias tst4n    "r i10_if4.blif; st; ps; r 5npn/all_functions.aig; st; rec_start;
 alias tst6     "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_if6.blif; st -r; ps; cec"
 
 
+alias bug      "r pj1_if3.blif; lp"
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index c89e6b83..0c7c03f8 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -234,6 +234,9 @@ struct Lut_Par_t_
     int               nLutsMax;      // (N) the maximum number of LUTs in the structure
     int               nLutsOver;     // (Q) the maximum number of LUTs not in the MFFC
     int               nVarsShared;   // (S) the maximum number of shared variables (crossbars)
+    int               nGrowthLevel;  // (L) the maximum increase in the node level after resynthesis
+    int               fSatur;        // iterate till saturation
+    int               fZeroCost;     // accept zero-cost replacements
     int               fVerbose;      // the verbosiness flag
     int               fVeryVerbose;  // additional verbose info printout
     // internal parameters
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 899cba96..e1728296 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -38,6 +38,8 @@ static bool Abc_NtkComparePis( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 static bool Abc_NtkComparePos( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 static bool Abc_NtkCompareLatches( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 
+static inline char * Abc_ObjNameNet( Abc_Obj_t * pObj ) { return (Abc_ObjIsNode(pObj) && Abc_NtkIsNetlist(pObj->pNtk)) ? Abc_ObjName(Abc_ObjFanout0(pObj)) : Abc_ObjName(pObj); }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -523,7 +525,7 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
     // the node should have a function assigned unless it is an AIG
     if ( pNode->pData == NULL )
     {
-        fprintf( stdout, "NodeCheck: An internal node \"%s\" does not have a logic function.\n", Abc_NtkIsNetlist(pNode->pNtk)? Abc_ObjName(Abc_ObjFanout0(pNode)) : Abc_ObjName(pNode) );
+        fprintf( stdout, "NodeCheck: An internal node \"%s\" does not have a logic function.\n", Abc_ObjNameNet(pNode) );
         return 0;
     }
     // the netlist and SOP logic network should have SOPs
@@ -531,7 +533,7 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
     {
         if ( !Abc_SopCheck( pNode->pData, Abc_ObjFaninNum(pNode) ) )
         {
-            fprintf( stdout, "NodeCheck: SOP check for node \"%s\" has failed.\n", Abc_ObjName(pNode) );
+            fprintf( stdout, "NodeCheck: SOP check for node \"%s\" has failed.\n", Abc_ObjNameNet(pNode) );
             return 0;
         }
     }
@@ -540,7 +542,7 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
         int nSuppSize = Cudd_SupportSize(pNtk->pManFunc, pNode->pData);
         if ( nSuppSize > Abc_ObjFaninNum(pNode) )
         {
-            fprintf( stdout, "NodeCheck: BDD of the node \"%s\" has incorrect support size.\n", Abc_ObjName(pNode) );
+            fprintf( stdout, "NodeCheck: BDD of the node \"%s\" has incorrect support size.\n", Abc_ObjNameNet(pNode) );
             return 0;
         }
     }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 216a737a..a91d6325 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -1264,9 +1264,9 @@ int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsBddLogic(pNtk) )
+    if ( !Abc_NtkIsLogic(pNtk) )
     {
-        fprintf( pErr, "Visualizing Karnaugh map works for BDD logic networks (run \"bdd\").\n" );
+        fprintf( pErr, "Visualization of Karnaugh maps works for logic networks.\n" );
         return 1;
     }
     if ( argc > globalUtilOptind + 1 )
@@ -1292,6 +1292,7 @@ int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
     }
+    Abc_NtkToBdd(pNtk);
     Abc_NodePrintKMap( pNode, fUseRealNames );
     return 0;
 
@@ -2908,12 +2909,15 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     memset( pPars, 0, sizeof(Lut_Par_t) );
     pPars->nLutsMax     =  4; // (N) the maximum number of LUTs in the structure
-    pPars->nLutsOver    =  2; // (Q) the maximum number of LUTs not in the MFFC
+    pPars->nLutsOver    =  3; // (Q) the maximum number of LUTs not in the MFFC
     pPars->nVarsShared  =  0; // (S) the maximum number of shared variables (crossbars)
-    pPars->fVerbose     =  0;
+    pPars->nGrowthLevel =  1;
+    pPars->fSatur       =  1;
+    pPars->fZeroCost    =  0; 
+    pPars->fVerbose     =  1;
     pPars->fVeryVerbose =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "NQSvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2950,6 +2954,23 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nVarsShared < 0 || pPars->nVarsShared > 4 ) 
                 goto usage;
             break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nGrowthLevel = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY ) 
+                goto usage;
+            break;
+        case 's':
+            pPars->fSatur ^= 1;
+            break;
+        case 'z':
+            pPars->fZeroCost ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -2983,11 +3004,14 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-vwh]\n" );
+    fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-L <num>] [-szvwh]\n" );
     fprintf( pErr, "\t           performs \"rewriting\" for LUT networks\n" );
     fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax );
     fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver );
     fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num) [default = %d]\n", pPars->nVarsShared );
+    fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
+    fprintf( pErr, "\t-s       : toggle iteration till saturation [default = %s]\n", pPars->fSatur? "yes": "no" );
+    fprintf( pErr, "\t-z       : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" );
     fprintf( pErr, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w       : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : print the command usage\n");
diff --git a/src/base/abci/abcDsdRes.c b/src/base/abci/abcDsdRes.c
index a76df9ce..50c624d7 100644
--- a/src/base/abci/abcDsdRes.c
+++ b/src/base/abci/abcDsdRes.c
@@ -19,13 +19,15 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "kit.h"
+#include "if.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
 #define LUT_SIZE_MAX     16   // the largest size of the function
-#define LUT_CUTS_MAX    128   // the largest number of cuts considered
+#define LUT_CUTS_MAX   1024   // the largest number of cuts considered
 
 typedef struct Lut_Man_t_ Lut_Man_t;
 typedef struct Lut_Cut_t_ Lut_Cut_t;
@@ -34,12 +36,12 @@ struct Lut_Cut_t_
 {
     unsigned     nLeaves       : 6;     // (L) the number of leaves
     unsigned     nNodes        : 6;     // (M) the number of nodes
-    unsigned     nNodesMarked  : 6;     // (Q) nodes outside of MFFC
-    unsigned     nNodesMax     : 6;     // the max number of nodes 
-    unsigned     nLeavesMax    : 6;     // the max number of leaves
+    unsigned     nNodesDup     : 6;     // (Q) nodes outside of MFFC
+    unsigned     nLuts         : 6;     // (N) the number of LUTs to try
+    unsigned     unused        : 6;     // unused
     unsigned     fHasDsd       : 1;     // set to 1 if the cut has structural DSD (and so cannot be used)
     unsigned     fMark         : 1;     // multipurpose mark
-//    unsigned     uSign[2];              // the signature
+    unsigned     uSign[2];              // the signature
     float        Weight;                // the weight of the cut: (M - Q)/N(V)   (the larger the better)
     int          Gain;                  // the gain achieved using this cut
     int          pLeaves[LUT_SIZE_MAX]; // the leaves of the cut
@@ -60,6 +62,12 @@ struct Lut_Man_t_
     int          nEvals;                // the number of good cuts
     Lut_Cut_t    pCuts[LUT_CUTS_MAX];   // the storage for cuts
     int          pEvals[LUT_CUTS_MAX];  // the good cuts
+    // visited nodes 
+    Vec_Vec_t *  vVisited;
+    // mapping manager
+    If_Man_t *   pIfMan;
+    Vec_Int_t *  vCover; 
+    Vec_Vec_t *  vLevels;
     // temporary variables
     int          pRefs[LUT_SIZE_MAX];   // fanin reference counters 
     int          pCands[LUT_SIZE_MAX];  // internal nodes pointing only to the leaves
@@ -67,12 +75,19 @@ struct Lut_Man_t_
     Vec_Ptr_t *  vTtElems;              // elementary truth tables
     Vec_Ptr_t *  vTtNodes;              // storage for temporary truth tables of the nodes 
     // statistics
-    int          nCutsTotal; 
-    int          nGainTotal;
+    int          nNodesTotal;           // total number of nodes
+    int          nNodesOver;            // nodes with cuts over the limit 
+    int          nCutsTotal;            // total number of cuts
+    int          nCutsUseful;           // useful cuts 
+    int          nGainTotal;            // the gain in LUTs
+    int          nChanges;              // the number of changed nodes
+    // counter of non-DSD blocks
+    int          nBlocks[17];
     // rutime
     int          timeCuts;
     int          timeTruth;
     int          timeEval;
+    int          timeMap;
     int          timeOther;
     int          timeTotal;
 };
@@ -84,6 +99,13 @@ struct Lut_Man_t_
 #define Abc_LutCutForEachNodeReverse( pNtk, pCut, pObj, i )                                 \
     for ( i = (int)(pCut)->nNodes - 1; (i >= 0) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i-- )
 
+static inline If_Obj_t *  If_Regular( If_Obj_t * p )        { return (If_Obj_t *)((unsigned long)(p) & ~01);  }
+static inline If_Obj_t *  If_Not( If_Obj_t * p )            { return (If_Obj_t *)((unsigned long)(p) ^  01);  }
+static inline If_Obj_t *  If_NotCond( If_Obj_t * p, int c ) { return (If_Obj_t *)((unsigned long)(p) ^ (c));  }
+static inline int         If_IsComplement( If_Obj_t * p )   { return (int )(((unsigned long)p) & 01);         }
+
+extern void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -102,17 +124,15 @@ struct Lut_Man_t_
 Lut_Man_t * Abc_LutManStart( Lut_Par_t * pPars )
 {
     Lut_Man_t * p;
-    int i;
     assert( pPars->nLutsMax <= 16 );
     assert( pPars->nVarsMax > 0 );
     p = ALLOC( Lut_Man_t, 1 );
     memset( p, 0, sizeof(Lut_Man_t) );
     p->pPars = pPars;
     p->nCutsMax = LUT_CUTS_MAX;
-    for ( i = 0; i < p->nCuts; i++ )
-        p->pCuts[i].nLeavesMax = p->pCuts[i].nNodesMax = LUT_SIZE_MAX;
     p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax );
     p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nVarsMax) );
+    p->vCover = Vec_IntAlloc( 1 << 12 );
     return p;
 }
 
@@ -129,6 +149,17 @@ Lut_Man_t * Abc_LutManStart( Lut_Par_t * pPars )
 ***********************************************************************/
 void Abc_LutManStop( Lut_Man_t * p )
 {
+    if ( p->pIfMan )
+    {
+        void * pPars = p->pIfMan->pPars;
+        If_ManStop( p->pIfMan );
+        free( pPars );
+    }
+    if ( p->vLevels )
+        Vec_VecFree( p->vLevels );
+    if ( p->vVisited )
+        Vec_VecFree( p->vVisited );
+    Vec_IntFree( p->vCover );
     Vec_PtrFree( p->vTtElems );
     Vec_PtrFree( p->vTtNodes );
     free( p );
@@ -136,6 +167,81 @@ void Abc_LutManStop( Lut_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if at least one entry has changed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_LutNodeHasChanged( Lut_Man_t * p, int iNode )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pTemp;
+    int i;
+    vNodes = Vec_VecEntry( p->vVisited, iNode );
+    if ( Vec_PtrSize(vNodes) == 0 )
+        return 1;
+    Vec_PtrForEachEntry( vNodes, pTemp, i )
+    {
+        // check if the node has changed
+        pTemp = Abc_NtkObj( p->pNtk, (int)pTemp );
+        if ( pTemp == NULL )
+            return 1;
+        // check if the number of fanouts has changed
+//        if ( Abc_ObjFanoutNum(pTemp) != (int)Vec_PtrEntry(vNodes, i+1) )
+//            return 1;
+        i++;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if at least one entry has changed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_LutNodeRecordImpact( Lut_Man_t * p )
+{
+    Lut_Cut_t * pCut;
+    Vec_Ptr_t * vNodes = Vec_VecEntry( p->vVisited, p->pObj->Id );
+    Abc_Obj_t * pNode;
+    int i, k;
+    // collect the nodes that impact the given node
+    Vec_PtrClear( vNodes );
+    for ( i = 0; i < p->nCuts; i++ )
+    {
+        pCut = p->pCuts + i;
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+        {
+            pNode = Abc_NtkObj( p->pNtk, pCut->pLeaves[k] );
+            if ( pNode->fMarkC )
+                continue;
+            pNode->fMarkC = 1;
+            Vec_PtrPush( vNodes, (void *)pNode->Id );
+            Vec_PtrPush( vNodes, (void *)Abc_ObjFanoutNum(pNode) );
+        }
+    }
+    // clear the marks
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        pNode = Abc_NtkObj( p->pNtk, (int)pNode );
+        pNode->fMarkC = 0;
+        i++;
+    }
+//printf( "%d ", Vec_PtrSize(vNodes) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if the cut has structural DSD.]
 
   Description []
@@ -236,7 +342,7 @@ int Abc_LutNodeCutsOneFilter( Lut_Cut_t * pCuts, int nCuts, Lut_Cut_t * pCutNew
 {
     Lut_Cut_t * pCut;
     int i, k;
-//    assert( pCutNew->uHash );
+    assert( pCutNew->uSign[0] || pCutNew->uSign[1] );
     // try to find the cut
     for ( i = 0; i < nCuts; i++ )
     {
@@ -245,7 +351,7 @@ int Abc_LutNodeCutsOneFilter( Lut_Cut_t * pCuts, int nCuts, Lut_Cut_t * pCutNew
             continue;
         if ( pCut->nLeaves == pCutNew->nLeaves )
         {
-//            if ( pCut->uHash[0] == pCutNew->uHash[0] && pCut->uHash[1] == pCutNew->uHash[1] )
+            if ( pCut->uSign[0] == pCutNew->uSign[0] && pCut->uSign[1] == pCutNew->uSign[1] )
             {
                 for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
                     if ( pCut->pLeaves[k] != pCutNew->pLeaves[k] )
@@ -258,10 +364,10 @@ int Abc_LutNodeCutsOneFilter( Lut_Cut_t * pCuts, int nCuts, Lut_Cut_t * pCutNew
         if ( pCut->nLeaves < pCutNew->nLeaves )
         {
             // skip the non-contained cuts
-//            if ( (pCut->uHash[0] & pCutNew->uHash[0]) != pCut->uHash[0] )
-//                continue;
-//            if ( (pCut->uHash[1] & pCutNew->uHash[1]) != pCut->uHash[1] )
-//                continue;
+            if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCut->uSign[0] )
+                continue;
+            if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCut->uSign[1] )
+                continue;
             // check containment seriously
             if ( Abc_LutNodeCutsOneDominance( pCut, pCutNew ) )
                 return 1;
@@ -270,10 +376,10 @@ int Abc_LutNodeCutsOneFilter( Lut_Cut_t * pCuts, int nCuts, Lut_Cut_t * pCutNew
         // check potential containment of other cut
 
         // skip the non-contained cuts
-//        if ( (pCut->uHash[0] & pCutNew->uHash[0]) != pCutNew->uHash[0] )
-//            continue;
-//        if ( (pCut->uHash[1] & pCutNew->uHash[1]) != pCutNew->uHash[1] )
-//            continue;
+        if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCutNew->uSign[0] )
+            continue;
+        if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCutNew->uSign[1] )
+            continue;
         // check containment seriously
         if ( Abc_LutNodeCutsOneDominance( pCutNew, pCut ) )
             pCut->nLeaves = 0; // removed
@@ -310,6 +416,29 @@ void Abc_LutNodePrintCut( Lut_Man_t * p, Lut_Cut_t * pCut )
     printf( "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Set the cut signature.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_LutNodeCutSignature( Lut_Cut_t * pCut )
+{
+    unsigned i;
+    pCut->uSign[0] = pCut->uSign[1] = 0;
+    for ( i = 0; i < pCut->nLeaves; i++ )
+    {
+        pCut->uSign[(pCut->pLeaves[i] & 32) > 0] |= (1 << (pCut->pLeaves[i] & 31));
+        if ( i != pCut->nLeaves - 1 )
+            assert( pCut->pLeaves[i] < pCut->pLeaves[i+1] );
+    }
+}
+
 
 /**Function*************************************************************
 
@@ -326,7 +455,7 @@ void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node )
 {
     Lut_Cut_t * pCutNew;
     Abc_Obj_t * pObj, * pFanin;
-    int i, k, j;
+    int i, k, j, nLeavesNew;
 
     // check if the cut can stand adding one more internal node
     if ( pCut->nNodes == LUT_SIZE_MAX )
@@ -342,9 +471,19 @@ void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node )
     // if the node is not in the MFFC, check the limit
     if ( !Abc_NodeIsTravIdCurrent(pObj) )
     {
-        if ( (int)pCut->nNodesMarked == p->pPars->nLutsOver )
+        if ( (int)pCut->nNodesDup == p->pPars->nLutsOver )
+            return;
+        assert( (int)pCut->nNodesDup < p->pPars->nLutsOver );
+    }
+
+    // check the possibility of adding this node using the signature
+    nLeavesNew = pCut->nLeaves - 1;
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+    {
+        if ( (pCut->uSign[(pFanin->Id & 32) > 0] & (1 << (pFanin->Id & 31))) )
+            continue;
+        if ( ++nLeavesNew > p->pPars->nVarsMax )
             return;
-        assert( (int)pCut->nNodesMarked < p->pPars->nLutsOver );
     }
 
     // initialize the set of leaves to the nodes in the cut
@@ -382,11 +521,9 @@ if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1]
         pCutNew->nLeaves++;
         assert( pCutNew->nLeaves <= LUT_SIZE_MAX );
     }
-
-    for ( k = 0; k < (int)pCutNew->nLeaves - 1; k++ )
-        assert( pCutNew->pLeaves[k] < pCutNew->pLeaves[k+1] );
-
+    
     // skip the contained cuts
+    Abc_LutNodeCutSignature( pCutNew );
     if ( Abc_LutNodeCutsOneFilter( p->pCuts, p->nCuts, pCutNew ) )
         return;
 
@@ -397,7 +534,7 @@ if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1]
     pCutNew->pNodes[ pCutNew->nNodes++ ] = Node;
 
     // add the marked node
-    pCutNew->nNodesMarked = pCut->nNodesMarked + !Abc_NodeIsTravIdCurrent(pObj);
+    pCutNew->nNodesDup = pCut->nNodesDup + !Abc_NodeIsTravIdCurrent(pObj);
 /*
 if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 )
 {
@@ -410,7 +547,7 @@ if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 )
     assert( p->nCuts < LUT_CUTS_MAX );
     p->nCuts++;
 
-    assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesMarked );
+    assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup );
 }
 
 /**Function*************************************************************
@@ -426,7 +563,6 @@ if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 )
 ***********************************************************************/
 int Abc_LutNodeCuts( Lut_Man_t * p )
 {
-    Abc_Obj_t * pFanin;
     Lut_Cut_t * pCut, * pCut2;
     int i, k, Temp, nMffc, fChanges;
 
@@ -438,27 +574,12 @@ int Abc_LutNodeCuts( Lut_Man_t * p )
 
     // initialize the first cut
     pCut = p->pCuts; p->nCuts = 1;
-    // assign internal nodes
-    pCut->nNodes = 1; 
-    pCut->pNodes[0] = p->pObj->Id;
-    pCut->nNodesMarked = 0;
-    // assign the leaves
-    pCut->nLeaves = Abc_ObjFaninNum( p->pObj );
-    Abc_ObjForEachFanin( p->pObj, pFanin, i )
-        pCut->pLeaves[i] = pFanin->Id;
-    // sort the leaves
-    do {
-        fChanges = 0;
-        for ( i = 0; i < (int)pCut->nLeaves - 1; i++ )
-        {
-            if ( pCut->pLeaves[i] <= pCut->pLeaves[i+1] )
-                continue;
-            Temp = pCut->pLeaves[i];
-            pCut->pLeaves[i] = pCut->pLeaves[i+1];
-            pCut->pLeaves[i+1] = Temp;
-            fChanges = 1;
-        }
-    } while ( fChanges );
+    pCut->nNodes = 0; 
+    pCut->nNodesDup = 0;
+    pCut->nLeaves = 1;
+    pCut->pLeaves[0] = p->pObj->Id;
+    // assign the signature
+    Abc_LutNodeCutSignature( pCut );
 
     // perform the cut computation
     for ( i = 0; i < p->nCuts; i++ )
@@ -469,22 +590,33 @@ int Abc_LutNodeCuts( Lut_Man_t * p )
         // try to expand the fanins of this cut
         for ( k = 0; k < (int)pCut->nLeaves; k++ )
         {
+            // create a new cut
             Abc_LutNodeCutsOne( p, pCut, pCut->pLeaves[k] );
+            // quit if the number of cuts has exceeded the limit
             if ( p->nCuts == LUT_CUTS_MAX )
                 break;
         }
         if ( p->nCuts == LUT_CUTS_MAX )
             break;
     }
+    if ( p->nCuts == LUT_CUTS_MAX ) 
+        p->nNodesOver++;
 
-    // compress the cuts by removing empty ones, decomposable ones, and those with negative Weight
+    // record the impact of this node
+    if ( p->pPars->fSatur )
+        Abc_LutNodeRecordImpact( p );
+
+    // compress the cuts by removing empty ones, those with negative Weight, and decomposable ones
     p->nEvals = 0;
     for ( i = 0; i < p->nCuts; i++ )
     {
         pCut = p->pCuts + i;
-        if ( pCut->nLeaves == 0 )
+        if ( pCut->nLeaves < 2 )
             continue;
-        pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesMarked) / p->pPars->nLutsMax;
+        // compute the number of LUTs neede to implement this cut
+        // V = N * (K-1) + 1  ~~~~~  N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0]
+        pCut->nLuts = (pCut->nLeaves-1)/(p->pPars->nLutSize-1) + ( (pCut->nLeaves-1)%(p->pPars->nLutSize-1) > 0 ); 
+        pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
         if ( pCut->Weight <= 1.0 )
             continue;
         pCut->fHasDsd = Abc_LutNodeCutsCheckDsd( p, pCut );
@@ -598,9 +730,210 @@ unsigned * Abc_LutCutTruth( Lut_Man_t * p, Lut_Cut_t * pCut )
     return pTruth;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the mapping manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_LutIfManStart( Lut_Man_t * p )
+{
+    If_Par_t * pPars;
+    assert( p->pIfMan == NULL );
+    // set defaults
+    pPars = ALLOC( If_Par_t, 1 );
+    memset( pPars, 0, sizeof(If_Par_t) );
+    // user-controlable paramters
+    pPars->nLutSize    =  p->pPars->nLutSize;
+    pPars->nCutsMax    =  8;
+    pPars->nFlowIters  =  0; // 1
+    pPars->nAreaIters  =  0; // 1 
+    pPars->DelayTarget = -1;
+    pPars->fPreprocess =  0;
+    pPars->fArea       =  1;
+    pPars->fFancy      =  0;
+    pPars->fExpRed     =  0; //
+    pPars->fLatchPaths =  0;
+    pPars->fSeqMap     =  0;
+    pPars->fVerbose    =  0;
+    // internal parameters
+    pPars->fTruth      =  0;
+    pPars->fUsePerm    =  0; 
+    pPars->nLatches    =  0;
+    pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
+    pPars->pTimesArr   =  NULL; 
+    pPars->pTimesArr   =  NULL;   
+    pPars->fUseBdds    =  0;
+    pPars->fUseSops    =  0;
+    pPars->fUseCnfs    =  0;
+    pPars->fUseMv      =  0;
+    // start the mapping manager and set its parameters
+    p->pIfMan = If_ManStart( pPars );
+    If_ManSetupSetAll( p->pIfMan, 1000 );
+    p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the decomposition graph into the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * Abc_LutIfManMapPrimeInternal( If_Man_t * pIfMan, Kit_Graph_t * pGraph )
+{
+    Kit_Node_t * pNode;
+    If_Obj_t * pAnd0, * pAnd1;
+    int i;
+    // check for constant function
+    if ( Kit_GraphIsConst(pGraph) )
+        return If_ManConst1(pIfMan);
+    // check for a literal
+    if ( Kit_GraphIsVar(pGraph) )
+        return Kit_GraphVar(pGraph)->pFunc;
+    // build the AIG nodes corresponding to the AND gates of the graph
+    Kit_GraphForEachNode( pGraph, pNode, i )
+    {
+        pAnd0 = Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc; 
+        pAnd1 = Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc; 
+        pNode->pFunc = If_ManCreateAnd( pIfMan, 
+            If_Regular(pAnd0), If_IsComplement(pAnd0) ^ pNode->eEdge0.fCompl, 
+            If_Regular(pAnd1), If_IsComplement(pAnd1) ^ pNode->eEdge1.fCompl );
+    }
+    return pNode->pFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * Abc_LutIfManMapPrime( If_Man_t * pIfMan, If_Obj_t ** ppLeaves, Kit_Graph_t * pGraph )
+{
+    Kit_Node_t * pNode;
+    If_Obj_t * pRes;
+    int i;
+    // collect the fanins
+    Kit_GraphForEachLeaf( pGraph, pNode, i )
+        pNode->pFunc = ppLeaves[i];
+    // perform strashing
+    pRes = Abc_LutIfManMapPrimeInternal( pIfMan, pGraph );
+    return If_NotCond( pRes, Kit_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the choice node for the given number.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * Abc_LutIfManChoiceOne( If_Man_t * pIfMan, If_Obj_t ** pNodes, int iNode, int nLeaves, int fXor )
+{
+    If_Obj_t * pPrev, * pAnd, * pOne, * pMany;
+    int v;
+    pPrev = NULL;
+    for ( v = 0; v < nLeaves; v++ )
+    {
+        if ( (iNode & (1 << v)) == 0 )
+            continue;
+        pOne  = pNodes[1 << v];
+        pMany = pNodes[iNode & ~(1 << v)];
+        if ( fXor )
+            pAnd = If_ManCreateXnor( pIfMan, If_Regular(pOne), pMany ); 
+        else
+            pAnd = If_ManCreateAnd( pIfMan, If_Regular(pOne), If_IsComplement(pOne), If_Regular(pMany), If_IsComplement(pMany) ); 
+        pAnd->pEquiv = pPrev;
+        pPrev = pAnd;
+    }
+    return pPrev;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the choice node for the given number.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * Abc_LutIfManChoice( If_Man_t * pIfMan, If_Obj_t ** pLeaves, int nLeaves, int fXor )
+{
+    If_Obj_t ** pNodes, * pRes;
+    int v, m, nMints;
+    // allocate room for nodes
+    assert( nLeaves >= 2 );
+    nMints = (1 << nLeaves);
+    pNodes = ALLOC( If_Obj_t *, nMints );
+    // set elementary ones
+    pNodes[0] = NULL;
+    for ( v = 0; v < nLeaves; v++ )
+        pNodes[1<<v] = pLeaves[v];
+    // set triples and so on
+    for ( v = 2; v <= nLeaves; v++ )
+        for ( m = 0; m < nMints; m++ )
+            if ( Kit_WordCountOnes(m) == v )
+            {
+                pNodes[m] = Abc_LutIfManChoiceOne( pIfMan, pNodes, m, nLeaves, fXor );
+                if ( v > 2 )
+                    If_ManCreateChoice( pIfMan, pNodes[m] );
+            }
+    pRes = pNodes[nMints-1];
+    free( pNodes );
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the choice node for the given number.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * Abc_LutIfManPart_rec( If_Man_t * pIfMan, If_Obj_t ** pLeaves, int nLeaves, int fXor )
+{
+    If_Obj_t * pObjNew1, * pObjNew2;
+    if ( nLeaves <= 5 )
+        return Abc_LutIfManChoice( pIfMan, pLeaves, nLeaves, fXor );
+    pObjNew1 = Abc_LutIfManPart_rec( pIfMan, pLeaves,               nLeaves / 2,             fXor );
+    pObjNew2 = Abc_LutIfManPart_rec( pIfMan, pLeaves + nLeaves / 2, nLeaves - (nLeaves / 2), fXor );
+    if ( fXor )
+        return If_ManCreateXnor( pIfMan, pObjNew1, pObjNew2 ); 
+    else
+        return If_ManCreateAnd( pIfMan, pObjNew1, 0, pObjNew2, 0 ); 
+}
+
 /**Function*************************************************************
 
-  Synopsis    [Implements the given DSD network.]
+  Synopsis    [Prepares the mapping manager.]
 
   Description []
                
@@ -609,11 +942,237 @@ unsigned * Abc_LutCutTruth( Lut_Man_t * p, Lut_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_LutCutUpdate( Lut_Man_t * p, Lut_Cut_t * pCut, void * pDsd )
+If_Obj_t * Abc_LutIfManMap_New_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit )
 {
+    Kit_Graph_t * pGraph;
+    Kit_DsdObj_t * pObj;
+    If_Obj_t * pObjNew, * pFansNew[16];
+    unsigned i, iLitFanin, fCompl;
+
+    // remember the complement
+    fCompl = Kit_DsdLitIsCompl(iLit); 
+    iLit = Kit_DsdLitRegular(iLit); 
+    assert( !Kit_DsdLitIsCompl(iLit) );
+
+    // consider the case of simple gate
+    pObj = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iLit) );
+    if ( pObj == NULL )
+    {
+        pObjNew = If_ManCi( p->pIfMan, Kit_DsdLit2Var(iLit) );
+        return If_NotCond( pObjNew, fCompl );
+    }
+
+    // solve for the inputs
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
+        pFansNew[i] = Abc_LutIfManMap_New_rec( p, pNtk, iLitFanin );
+
+    // generate choices for multi-input gate
+    if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
+    {
+        assert( pObj->nFans >= 2 );
+        if ( pObj->Type == KIT_DSD_XOR )
+        {
+            fCompl ^= ((pObj->nFans-1) & 1); // flip if the number of operations is odd
+            for ( i = 0; i < pObj->nFans; i++ )
+            {
+                fCompl ^= If_IsComplement(pFansNew[i]);
+                pFansNew[i] = If_Regular(pFansNew[i]);
+            }
+        }
+        pObjNew = Abc_LutIfManPart_rec( p->pIfMan, pFansNew, pObj->nFans, pObj->Type == KIT_DSD_XOR );
+        return If_NotCond( pObjNew, fCompl );
+    }
+    assert( pObj->Type == KIT_DSD_PRIME );
+
+    // derive the factored form
+    pGraph = Kit_TruthToGraph( Kit_DsdObjTruth(pObj), pObj->nFans, p->vCover );
+    // convert factored form into the AIG
+    pObjNew = Abc_LutIfManMapPrime( p->pIfMan, pFansNew, pGraph ); 
+    Kit_GraphFree( pGraph );
+    return If_NotCond( pObjNew, fCompl );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the mapping manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit )
+{
+    Kit_Graph_t * pGraph;
+    Kit_DsdObj_t * pObj;
+    If_Obj_t * pObjNew, * pFansNew[16];
+    unsigned i, iLitFanin, fCompl;
+
+    // remember the complement
+    fCompl = Kit_DsdLitIsCompl(iLit); 
+    iLit = Kit_DsdLitRegular(iLit); 
+    assert( !Kit_DsdLitIsCompl(iLit) );
+
+    // consider the case of simple gate
+    pObj = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iLit) );
+    if ( pObj == NULL )
+    {
+        pObjNew = If_ManCi( p->pIfMan, Kit_DsdLit2Var(iLit) );
+        return If_NotCond( pObjNew, fCompl );
+    }
+    if ( pObj->Type == KIT_DSD_AND )
+    {
+        assert( pObj->nFans == 2 );
+        pFansNew[0] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0] );
+        pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1] );
+        if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
+            return NULL;
+        pObjNew = If_ManCreateAnd( p->pIfMan, If_Regular(pFansNew[0]), If_IsComplement(pFansNew[0]), If_Regular(pFansNew[1]), If_IsComplement(pFansNew[1]) ); 
+        return If_NotCond( pObjNew, fCompl );
+    }
+    if ( pObj->Type == KIT_DSD_XOR )
+    {
+        assert( pObj->nFans == 2 );
+        pFansNew[0] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0] );
+        pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1] );
+        if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
+            return NULL;
+        fCompl ^= 1 ^ If_IsComplement(pFansNew[0]) ^ If_IsComplement(pFansNew[1]);
+        pObjNew = If_ManCreateXnor( p->pIfMan, If_Regular(pFansNew[0]), If_Regular(pFansNew[1]) );
+        return If_NotCond( pObjNew, fCompl );
+    }
+    assert( pObj->Type == KIT_DSD_PRIME );
+    p->nBlocks[pObj->nFans]++;
+
+    // solve for the inputs
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
+    {
+        pFansNew[i] = Abc_LutIfManMap_rec( p, pNtk, iLitFanin );
+        if ( pFansNew[i] == NULL )
+            return NULL;
+    }
+
+    // derive the factored form
+    pGraph = Kit_TruthToGraph( Kit_DsdObjTruth(pObj), pObj->nFans, p->vCover );
+    if ( pGraph == NULL )
+        return NULL;
+    // convert factored form into the AIG
+    pObjNew = Abc_LutIfManMapPrime( p->pIfMan, pFansNew, pGraph ); 
+    Kit_GraphFree( pGraph );
+    return If_NotCond( pObjNew, fCompl );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the mapping manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_LutCutUpdate( Lut_Man_t * p, Lut_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
+{
+    extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
+    Kit_DsdObj_t * pRoot;
+    If_Obj_t * pDriver;
+    Abc_Obj_t * pLeaf, * pObjNew;
+    int nGain, i;
+
+    // check special cases
+    pRoot = Kit_DsdNtkRoot( pNtk );
+    if ( pRoot->Type == KIT_DSD_CONST1 )
+    {
+        pObjNew = Abc_NtkCreateNodeConst1( p->pNtk );
+        pObjNew = Abc_ObjNotCond( pObjNew, Kit_DsdLitIsCompl(pNtk->Root) );
+
+        // perform replacement
+        pObjNew->Level = p->pObj->Level;
+        Abc_ObjReplace( p->pObj, pObjNew );
+        Res_UpdateNetworkLevel( pObjNew, p->vLevels );
+        p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
+        return 1;
+    }
+    if ( pRoot->Type == KIT_DSD_VAR )
+    {
+        pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] );
+        pObjNew = Abc_ObjNotCond( pObjNew, Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) );
+
+        // perform replacement
+        pObjNew->Level = p->pObj->Level;
+        Abc_ObjReplace( p->pObj, pObjNew );
+        Res_UpdateNetworkLevel( pObjNew, p->vLevels );
+        p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
+        return 1;
+    }
+    assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME );
+
+    // start the mapping manager
+    if ( p->pIfMan == NULL )
+        Abc_LutIfManStart( p );
+
+    // prepare the mapping manager
+    If_ManRestart( p->pIfMan );
+    // create the PI variables
+    for ( i = 0; i < p->pPars->nVarsMax; i++ )
+        If_ManCreateCi( p->pIfMan );
+    // set the arrival times
+    Abc_LutCutForEachLeaf( p->pNtk, pCut, pLeaf, i )
+        p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level;
+    // prepare the PI cuts
+    If_ManSetupCiCutSets( p->pIfMan );
+    // create the internal nodes
+//    pDriver = Abc_LutIfManMap_New_rec( p, pNtk, pNtk->Root );
+    pDriver = Abc_LutIfManMap_rec( p, pNtk, pNtk->Root );
+    if ( pDriver == NULL )
+        return 0;
+    // create the PO node
+    If_ManCreateCo( p->pIfMan, If_Regular(pDriver), 0 );
+
+    // perform mapping
+    p->pIfMan->pPars->fAreaOnly = 1;
+    If_ManPerformMappingComb( p->pIfMan );
+
+    // compute the gain in area
+    nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo;
+    if ( p->pPars->fVeryVerbose )
+        printf( "       Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d.\n", 
+            pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level );
+
+    // quit if there is no gain
+    if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) )
+        return 0;
+    // quit if depth increases too much
+    if ( (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level > p->pPars->nGrowthLevel )
+        return 0;
+
+    // perform replacement
+    p->nGainTotal += nGain;
+    p->nChanges++;
+
+    // prepare the mapping manager
+    If_ManCleanNodeCopy( p->pIfMan );
+    If_ManCleanCutData( p->pIfMan );
+    // set the PIs of the cut
+    Abc_LutCutForEachLeaf( p->pNtk, pCut, pLeaf, i )
+        If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf );
+    // get the area of mapping
+    pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover );
+    pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
+
+    // perform replacement
+    pObjNew->Level = p->pObj->Level;
+    Abc_ObjReplace( p->pObj, pObjNew );
+    Res_UpdateNetworkLevel( pObjNew, p->vLevels );
     return 1;
 }
 
+
+
 /**Function*************************************************************
 
   Synopsis    [Performs resynthesis for one node.]
@@ -630,11 +1189,13 @@ int Abc_LutResynthesizeNode( Lut_Man_t * p )
     extern void Kit_DsdTest( unsigned * pTruth, int nVars );
     extern int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize );
 
+    Kit_DsdNtk_t * pDsdNtk;
     Lut_Cut_t * pCut;
     unsigned * pTruth;
     void * pDsd = NULL;
-    int i, Result, GainBest, Gain;
-    int clk;
+//    int Result, Gain;
+    int i, RetValue, clk;
+
     // compute the cuts
 clk = clock();
     if ( !Abc_LutNodeCuts( p ) )
@@ -647,48 +1208,67 @@ p->timeCuts += clock() - clk;
     if ( p->pPars->fVeryVerbose )
     printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
     // try the good cuts
-    p->nCutsTotal += p->nEvals;
-    GainBest = 0;
+    p->nCutsTotal  += p->nCuts;
+    p->nCutsUseful += p->nEvals;
     for ( i = 0; i < p->nEvals; i++ )
     {
         // get the cut
         pCut = p->pCuts + p->pEvals[i];
+
         // compute the truth table
 clk = clock();
         pTruth = Abc_LutCutTruth( p, pCut );
 p->timeTruth += clock() - clk;
+
+/*
         // evaluate the result of decomposition        
+        Result = Kit_DsdEval( pTruth, pCut->nLeaves, 3 );
+        // calculate expected gain
+        Gain = (Result < 0) ? -1 : pCut->nNodes - pCut->nNodesDup - Result;
+        if ( !(Gain < 0 || (Gain == 0 && p->pPars->fZeroCost)) )
+            continue;
+*/
+
 clk = clock();
 //        Kit_DsdTest( pTruth, pCut->nLeaves );
-        Result = Kit_DsdEval( pTruth, pCut->nLeaves, 3 );
+        pDsdNtk = Kit_DsdDeriveNtk( pTruth, pCut->nLeaves, p->pPars->nLutSize );
 p->timeEval += clock() - clk;
 
-        // calculate the gain
-        Gain = Result < 0 ? 0 : pCut->nNodes - pCut->nNodesMarked - Result;
-        if ( GainBest < Gain )
-            GainBest = Gain;
-
+        if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 ) // skip 16-input non-DSD because ISOP will not work
+        {
+            Kit_DsdNtkFree( pDsdNtk );
+            continue;
+        }
+/*
+        // skip large non-DSD blocks
+        if ( Kit_DsdNonDsdSizeMax(pDsdNtk) > 7 )
+        {
+            Kit_DsdNtkFree( pDsdNtk );
+            continue;
+        }
+*/
         if ( p->pPars->fVeryVerbose )
         {
-            printf( "    Cut %2d : Lvs = %2d. Supp = %2d. Vol = %2d. Q = %d. Weight = %4.2f. New = %2d. Gain = %2d.\n", 
-                i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesMarked, pCut->Weight, Result, Gain );
-//            for ( k = 0; k < pCut->nNodes; k++ )
-//                printf( "%d(%d) ", pCut->pNodes[k], Abc_NodeIsTravIdCurrent( Abc_NtkObj(p->pNtk, pCut->pNodes[k]) ) );
-//            printf( "\n" );
+//            Extra_PrintHexadecimal( stdout, pTruth, pCut->nLeaves ); printf( "\n" );
+//            printf( "    Cut %2d : L = %2d. S = %2d. Vol = %2d. Q = %d. N = %d. W = %4.2f. New = %2d. Gain = %2d.\n", 
+//                i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight, Result, Gain );
+            printf( "  C%02d: L= %2d/%2d  V= %2d/%d  N= %d  W= %4.2f  ", 
+                i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
+            Kit_DsdPrint( stdout, pDsdNtk );
         }
-//        pTruth = NULL;
-//Extra_PrintHexadecimal( stdout, pTruth, pCut->nLeaves ); printf( "\n" );
 
-        // if it is not DSD decomposable, return
-        if ( pDsd == NULL )
-            continue;
         // update the network
-        Abc_LutCutUpdate( p, pCut, pDsd );
+clk = clock();
+        RetValue = Abc_LutCutUpdate( p, pCut, pDsdNtk );
+        Kit_DsdNtkFree( pDsdNtk );
+p->timeMap += clock() - clk;
+        if ( RetValue )
+            break;
     }
-    p->nGainTotal += GainBest;
     return 1;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Performs resynthesis for one network.]
@@ -702,38 +1282,93 @@ p->timeEval += clock() - clk;
 ***********************************************************************/
 int Abc_LutResynthesize( Abc_Ntk_t * pNtk, Lut_Par_t * pPars )
 {
+    ProgressBar * pProgress;
     Lut_Man_t * p;
     Abc_Obj_t * pObj;
-    int i, clk = clock();
+    double Delta;
+    int i, Iter, nNodes, nNodesPrev, clk = clock();
     assert( Abc_NtkIsLogic(pNtk) );
-    // convert logic to AIGs
-    Abc_NtkToAig( pNtk );
-    // compute the levels
-    Abc_NtkLevel( pNtk );
+
     // get the number of inputs
     pPars->nLutSize = Abc_NtkGetFaninMax( pNtk );
     pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1; // V = N * (K-1) + 1
-    printf( "Resynthesis for %d %d-LUTs with %d non-MFFC LUTs, %d crossbars, and %d-input cuts.\n",
-        pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax );
+    if ( pPars->fVerbose )
+    {
+        printf( "Resynthesis for %d %d-LUTs with %d non-MFFC LUTs, %d crossbars, and %d-input cuts.\n",
+            pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax );
+    }
+    if ( pPars->nVarsMax > 16 )
+    {
+        printf( "Currently cannot handle resynthesis with more than %d inputs (reduce \"-N <num>\").\n", 16 );
+        return 1;
+    }
+ 
+    // convert logic to AIGs
+    Abc_NtkToAig( pNtk );
+
     // start the manager
     p = Abc_LutManStart( pPars );
     p->pNtk = pNtk;
-    // consider all nodes
-    Abc_NtkForEachNode( pNtk, pObj, i )
-    {
-        p->pObj = pObj;
-        Abc_LutResynthesizeNode( p );
-    }
-    printf( "Total nodes = %5d. Total cuts = %5d. Total gain = %5d. (%5.2f %%)\n", 
-        Abc_NtkNodeNum(pNtk), p->nCutsTotal, p->nGainTotal, 100.0 * p->nGainTotal / Abc_NtkNodeNum(pNtk) );
-
-    p->timeTotal = clock() - clk;
-    p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval;
-    PRTP( "Cuts  ", p->timeCuts,  p->timeTotal );
-    PRTP( "Truth ", p->timeTruth, p->timeTotal );
-    PRTP( "Eval  ", p->timeEval,  p->timeTotal );
-    PRTP( "Other ", p->timeOther, p->timeTotal );
-    PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
+    p->nNodesTotal = Abc_NtkNodeNum(pNtk);
+    p->vLevels = Vec_VecStart( 3 * Abc_NtkLevel(pNtk) ); // computes levels of all nodes
+    if ( p->pPars->fSatur )
+        p->vVisited = Vec_VecStart( 0 );
+
+    // iterate over the network
+    nNodesPrev = p->nNodesTotal;
+    for ( Iter = 1; ; Iter++ )
+    {
+        // expand storage for changed nodes
+        if ( p->pPars->fSatur )
+            Vec_VecExpand( p->vVisited, Abc_NtkObjNumMax(pNtk) + 1 );
+
+        // consider all nodes
+        nNodes = Abc_NtkObjNumMax(pNtk);
+        if ( !pPars->fVeryVerbose )
+            pProgress = Extra_ProgressBarStart( stdout, nNodes );
+        Abc_NtkForEachNode( pNtk, pObj, i )
+        {
+            if ( i >= nNodes )
+                break;
+            if ( !pPars->fVeryVerbose )
+                Extra_ProgressBarUpdate( pProgress, i, NULL );
+            // skip the nodes that did not change
+            if ( p->pPars->fSatur && !Abc_LutNodeHasChanged(p, pObj->Id) )
+                continue;
+            // resynthesize
+            p->pObj = pObj;
+            Abc_LutResynthesizeNode( p );
+        }
+        if ( !pPars->fVeryVerbose )
+            Extra_ProgressBarStop( pProgress );
+
+        // check the increase
+        Delta = 100.00 * (nNodesPrev - Abc_NtkNodeNum(pNtk)) / p->nNodesTotal;
+        if ( Delta < 0.05 )
+            break;
+        nNodesPrev = Abc_NtkNodeNum(pNtk);
+        if ( !p->pPars->fSatur )
+            break;
+    }
+
+    if ( pPars->fVerbose )
+    {
+        printf( "N = %5d (%3d)  Cut = %5d (%4d)  Change = %5d  Gain = %5d  (%5.2f %%) Iter = %2d\n", 
+            p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal, Iter );
+        printf( "Non_DSD blocks: " );
+        for ( i = 3; i <= pPars->nVarsMax; i++ )
+            if ( p->nBlocks[i] )
+                printf( "%d=%d  ", i, p->nBlocks[i] );
+        printf( "\n" );
+        p->timeTotal = clock() - clk;
+        p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap;
+        PRTP( "Cuts  ", p->timeCuts,  p->timeTotal );
+        PRTP( "Truth ", p->timeTruth, p->timeTotal );
+        PRTP( "Eval  ", p->timeEval,  p->timeTotal );
+        PRTP( "Map   ", p->timeMap,   p->timeTotal );
+        PRTP( "Other ", p->timeOther, p->timeTotal );
+        PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
+    }
 
     Abc_LutManStop( p );
     // check the resulting network
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 46f7dd13..b8c4a6c0 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -28,7 +28,7 @@
 
 static If_Man_t *  Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
 static Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk );
-static Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
+extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
 static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj );
 static Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk );
 
@@ -262,6 +262,11 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
         If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i )
             Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) );
     }
+    // set the level of the new node
+    {
+        extern int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj );
+        pNodeNew->Level = Res_UpdateNetworkLevelNew( pNodeNew );
+    }
     // derive the function of this node
     if ( pIfMan->pPars->fTruth )
     {
diff --git a/src/map/if/if.h b/src/map/if/if.h
index a440d7ea..cdf9e1c7 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -331,17 +331,19 @@ extern void            If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t *
 extern void            If_ManSortCuts( If_Man_t * p, int Mode );
 /*=== ifMan.c =============================================================*/
 extern If_Man_t *      If_ManStart( If_Par_t * pPars );
+extern void            If_ManRestart( If_Man_t * p );
 extern void            If_ManStop( If_Man_t * p );
 extern If_Obj_t *      If_ManCreateCi( If_Man_t * p );
 extern If_Obj_t *      If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 );
 extern If_Obj_t *      If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 );
+extern If_Obj_t *      If_ManCreateXnor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 );
 extern void            If_ManCreateChoice( If_Man_t * p, If_Obj_t * pRepr );
 extern void            If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId );
 extern void            If_ManSetupCiCutSets( If_Man_t * p );
 extern If_Set_t *      If_ManSetupNodeCutSet( If_Man_t * p, If_Obj_t * pObj );
 extern void            If_ManDerefNodeCutSet( If_Man_t * p, If_Obj_t * pObj );
 extern void            If_ManDerefChoiceCutSet( If_Man_t * p, If_Obj_t * pObj );
-extern void            If_ManSetupSetAll( If_Man_t * p );
+extern void            If_ManSetupSetAll( If_Man_t * p, int nCrossCut );
 /*=== ifMap.c =============================================================*/
 extern void            If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess );
 extern void            If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess );
diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c
index c36642bc..59ad5a1c 100644
--- a/src/map/if/ifCore.c
+++ b/src/map/if/ifCore.c
@@ -48,7 +48,7 @@ int If_ManPerformMapping( If_Man_t * p )
     // create the CI cutsets
     If_ManSetupCiCutSets( p );
     // allocate memory for other cutsets
-    If_ManSetupSetAll( p );
+    If_ManSetupSetAll( p, If_ManCrossCut(p) );
 
     // try sequential mapping
     if ( p->pPars->fSeqMap )
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 77f4930a..00a5b228 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -79,6 +79,7 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
     p->pConst1 = If_ManSetupObj( p );
     p->pConst1->Type = IF_CONST1;
     p->pConst1->fPhase = 1;
+    p->nObjs[IF_CONST1]++;
     return p;
 }
 
@@ -93,6 +94,34 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
+void If_ManRestart( If_Man_t * p )
+{
+    FREE( p->pMemCi );
+    Vec_PtrClear( p->vCis );
+    Vec_PtrClear( p->vCos );
+    Vec_PtrClear( p->vObjs );
+    Vec_PtrClear( p->vMapped );
+    Vec_PtrClear( p->vTemp );
+    Mem_FixedRestart( p->pMemObj );
+    // create the constant node
+    p->pConst1 = If_ManSetupObj( p );
+    p->pConst1->Type = IF_CONST1;
+    p->pConst1->fPhase = 1;
+    // reset the counter of other nodes
+    p->nObjs[IF_CI] = p->nObjs[IF_CO] = p->nObjs[IF_AND] = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void If_ManStop( If_Man_t * p )
 {
     Vec_PtrFree( p->vCis );
@@ -103,7 +132,6 @@ void If_ManStop( If_Man_t * p )
     if ( p->vLatchOrder ) Vec_PtrFree( p->vLatchOrder );
     if ( p->vLags ) Vec_IntFree( p->vLags );
     Mem_FixedStop( p->pMemObj, 0 );
-//    Mem_FixedStop( p->pMemSet, 0 );
     FREE( p->pMemCi );
     FREE( p->pMemAnd );
     FREE( p->puTemp[0] );
@@ -190,6 +218,25 @@ If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_
 
 /**Function*************************************************************
 
+  Synopsis    [Create the new node assuming it does not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * If_ManCreateXnor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 )
+{
+    If_Obj_t * pRes1, * pRes2;
+    pRes1 = If_ManCreateAnd( p, pFan0, 0, pFan1, 1 );
+    pRes2 = If_ManCreateAnd( p, pFan0, 1, pFan1, 0 );
+    return If_ManCreateAnd( p, pRes1, 1, pRes2, 1 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates the choice node.]
 
   Description [Should be called after the equivalence class nodes are linked.]
@@ -460,11 +507,10 @@ void If_ManDerefChoiceCutSet( If_Man_t * p, If_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void If_ManSetupSetAll( If_Man_t * p )
+void If_ManSetupSetAll( If_Man_t * p, int nCrossCut )
 {
     If_Set_t * pCutSet;
-    int i, nCrossCut, nCutSets;
-    nCrossCut = If_ManCrossCut( p );
+    int i, nCutSets;
     nCutSets = 128 + nCrossCut;
     p->pFreeList = p->pMemAnd = pCutSet = (If_Set_t *)malloc( nCutSets * p->nSetBytes );
     for ( i = 0; i < nCutSets; i++ )
diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h
index c08ea81a..9e7d2bf1 100644
--- a/src/opt/kit/kit.h
+++ b/src/opt/kit/kit.h
@@ -87,6 +87,69 @@ struct Kit_Graph_t_
     Kit_Edge_t        eRoot;           // the pointer to the topmost node
 };
 
+
+// DSD node types
+typedef enum { 
+    KIT_DSD_NONE  = 0,  // 0: unknown
+    KIT_DSD_CONST1,     // 1: constant 1
+    KIT_DSD_VAR,        // 2: elementary variable
+    KIT_DSD_AND,        // 3: multi-input AND
+    KIT_DSD_XOR,        // 4: multi-input XOR
+    KIT_DSD_PRIME       // 5: arbitrary function of 3+ variables
+} Kit_Dsd_t;
+
+// DSD node
+typedef struct Kit_DsdObj_t_ Kit_DsdObj_t;
+struct Kit_DsdObj_t_
+{ 
+    unsigned       Id         : 6;  // the number of this node
+    unsigned       Type       : 3;  // none, const, var, AND, XOR, MUX, PRIME
+    unsigned       fMark      : 1;  // finished checking output
+    unsigned       Offset     : 8;  // offset to the truth table
+    unsigned       nRefs      : 8;  // offset to the truth table
+    unsigned       nFans      : 6;  // the number of fanins of this node
+    unsigned char  pFans[0];        // the fanin literals
+};
+
+// DSD network
+typedef struct Kit_DsdNtk_t_ Kit_DsdNtk_t;
+struct Kit_DsdNtk_t_
+{
+    unsigned char  nVars;           // at most 16 (perhaps 18?)
+    unsigned char  nNodesAlloc;     // the number of allocated nodes (at most nVars)
+    unsigned char  nNodes;          // the number of nodes
+    unsigned char  Root;            // the root of the tree
+    unsigned *     pMem;            // memory for the truth tables (memory manager?)
+    Kit_DsdObj_t * pNodes[0];       // the nodes
+};
+
+// DSD manager
+typedef struct Kit_DsdMan_t_ Kit_DsdMan_t;
+struct Kit_DsdMan_t_
+{
+    int            nVars;           // the maximum number of variables
+    int            nWords;          // the number of words in TTs
+    Vec_Ptr_t *    vTtElems;        // elementary truth tables
+    Vec_Ptr_t *    vTtNodes;        // the node truth tables
+};
+
+static inline int             Kit_DsdVar2Lit( int Var, int fCompl )  { return Var + Var + fCompl; }
+static inline int             Kit_DsdLit2Var( int Lit )              { return Lit >> 1;           }
+static inline int             Kit_DsdLitIsCompl( int Lit )           { return Lit & 1;            }
+static inline int             Kit_DsdLitNot( int Lit )               { return Lit ^ 1;            }
+static inline int             Kit_DsdLitNotCond( int Lit, int c )    { return Lit ^ (int)(c > 0); }
+static inline int             Kit_DsdLitRegular( int Lit )           { return Lit & 0xfe;         }
+ 
+static inline unsigned        Kit_DsdObjOffset( int nFans )          { return (nFans >> 2) + ((nFans & 3) > 0);                    }
+static inline unsigned *      Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
+static inline Kit_DsdObj_t *  Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id )  { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
+static inline Kit_DsdObj_t *  Kit_DsdNtkRoot( Kit_DsdNtk_t * pNtk )  { return Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(pNtk->Root) );   }
+
+#define Kit_DsdNtkForEachObj( pNtk, pObj, i )                                      \
+    for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
+#define Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )                              \
+    for ( i = 0; (i < (pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -358,6 +421,13 @@ static inline void Kit_TruthAndPhase( unsigned * pOut, unsigned * pIn0, unsigned
 extern DdNode *        Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars );
 extern DdNode *        Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph );
 extern DdNode *        Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop );
+/*=== kitDsd.c ==========================================================*/
+extern Kit_DsdNtk_t *  Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize );
+extern unsigned *      Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk );
+extern void            Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
+extern Kit_DsdNtk_t *  Kit_DsdDecompose( unsigned * pTruth, int nVars );
+extern void            Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
+extern int             Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
 /*=== kitFactor.c ==========================================================*/
 extern Kit_Graph_t *   Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_t * vMemory );
 /*=== kitGraph.c ==========================================================*/
diff --git a/src/opt/kit/kitDsd.c b/src/opt/kit/kitDsd.c
index 3540fa03..62ee653b 100644
--- a/src/opt/kit/kitDsd.c
+++ b/src/opt/kit/kitDsd.c
@@ -24,74 +24,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Kit_DsdMan_t_ Kit_DsdMan_t;
-typedef struct Kit_DsdNtk_t_ Kit_DsdNtk_t;
-typedef struct Kit_DsdObj_t_ Kit_DsdObj_t;
-
-// DSD node types
-typedef enum { 
-    KIT_DSD_NONE  = 0,  // 0: unknown
-    KIT_DSD_CONST1,     // 1: constant 1
-    KIT_DSD_VAR,        // 2: elementary variable
-    KIT_DSD_AND,        // 3: multi-input AND
-    KIT_DSD_XOR,        // 4: multi-input XOR
-    KIT_DSD_PRIME       // 5: arbitrary function of 3+ variables
-} Kit_Dsd_t;
-
-// DSD manager
-struct Kit_DsdMan_t_
-{
-    int            nVars;           // the maximum number of variables
-    int            nWords;          // the number of words in TTs
-    Vec_Ptr_t *    vTtElems;        // elementary truth tables
-    Vec_Ptr_t *    vTtNodes;        // the node truth tables
-};
-
-// DSD network
-struct Kit_DsdNtk_t_
-{
-    unsigned char  nVars;           // at most 16 (perhaps 18?)
-    unsigned char  nNodesAlloc;     // the number of allocated nodes (at most nVars)
-    unsigned char  nNodes;          // the number of nodes
-    unsigned char  Root;            // the root of the tree
-    unsigned *     pMem;            // memory for the truth tables (memory manager?)
-    Kit_DsdObj_t * pNodes[0];       // the nodes
-};
-
-// DSD node
-struct Kit_DsdObj_t_
-{ 
-    unsigned       Id         : 6;  // the number of this node
-    unsigned       Type       : 3;  // none, const, var, AND, XOR, MUX, PRIME
-    unsigned       fMark      : 1;  // finished checking output
-    unsigned       Offset     : 8;  // offset to the truth table
-    unsigned       nRefs      : 8;  // offset to the truth table
-    unsigned       nFans      : 6;  // the number of fanins of this node
-    unsigned char  pFans[0];        // the fanin literals
-};
-
-static inline int             Kit_DsdVar2Lit( int Var, int fCompl )  { return Var + Var + fCompl; }
-static inline int             Kit_DsdLit2Var( int Lit )              { return Lit >> 1;           }
-static inline int             Kit_DsdLitIsCompl( int Lit )           { return Lit & 1;            }
-static inline int             Kit_DsdLitNot( int Lit )               { return Lit ^ 1;            }
-static inline int             Kit_DsdLitNotCond( int Lit, int c )    { return Lit ^ (int)(c > 0); }
-static inline int             Kit_DsdLitRegular( int Lit )           { return Lit & 0xfe;         }
- 
-static inline unsigned        Kit_DsdObjOffset( int nFans )          { return (nFans >> 2) + ((nFans & 3) > 0);                    }
-static inline unsigned *      Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
-static inline Kit_DsdObj_t *  Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id )  { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
-static inline Kit_DsdObj_t *  Kit_DsdNtkRoot( Kit_DsdNtk_t * pNtk )  { return Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(pNtk->Root) );   }
-
-#define Kit_DsdNtkForEachObj( pNtk, pObj, i )                                      \
-    for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
-#define Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )                              \
-    for ( i = 0; (i < (pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
-
-extern unsigned *     Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk );
-extern void           Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
-extern Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars );
-extern void           Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -483,7 +415,7 @@ int Kit_DsdCountLuts_rec( Kit_DsdNtk_t * pNtk, int nLutSize, int Id, int * pCoun
         return nLutSize - 2;
     }
     assert( pObj->Type == KIT_DSD_PRIME );
-    if ( (int)pObj->nFans > nLutSize )
+    if ( (int)pObj->nFans > nLutSize ) //+ 1 )
     {
         *pCounter = 1000;
         return 0;
@@ -491,6 +423,8 @@ int Kit_DsdCountLuts_rec( Kit_DsdNtk_t * pNtk, int nLutSize, int Id, int * pCoun
     Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
         Kit_DsdCountLuts_rec( pNtk, nLutSize, Kit_DsdLit2Var(iLit), pCounter );
     (*pCounter)++;
+//    if ( (int)pObj->nFans == nLutSize + 1 )
+//        (*pCounter)++;
     return nLutSize - pObj->nFans;
 }
 
@@ -518,6 +452,31 @@ int Kit_DsdCountLuts( Kit_DsdNtk_t * pNtk, int nLutSize )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of blocks of the given number of inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned i, nSizeMax = 0;
+    Kit_DsdNtkForEachObj( pNtk, pObj, i )
+    {
+        if ( pObj->Type != KIT_DSD_PRIME )
+            continue;
+        if ( nSizeMax < pObj->nFans )
+            nSizeMax = pObj->nFans;
+    }
+    return nSizeMax;
+}
+
 
 /**Function*************************************************************
 
@@ -1208,6 +1167,50 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
   SeeAlso     []
 
 ***********************************************************************/
+Kit_DsdNtk_t * Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize )
+{
+//    Kit_DsdMan_t * p;
+    Kit_DsdNtk_t * pNtk;//, * pTemp;
+//    unsigned * pTruthC;
+//    int Result;
+
+    // decompose the function
+    pNtk = Kit_DsdDecompose( pTruth, nVars );
+
+//    pNtk = Kit_DsdExpand( pTemp = pNtk );
+//    Kit_DsdNtkFree( pTemp );
+
+//    Result = Kit_DsdCountLuts( pNtk, nLutSize );
+
+//    printf( "\n" );
+//    Kit_DsdPrint( stdout, pNtk );
+//    printf( "Eval = %d.\n", Result );
+
+/*
+    // recompute the truth table
+    p = Kit_DsdManAlloc( nVars );
+    pTruthC = Kit_DsdTruthCompute( p, pNtk );
+    if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
+        printf( "Verification failed.\n" );
+    Kit_DsdManFree( p );
+*/
+
+//    Kit_DsdNtkFree( pNtk );
+//    return Result;
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Kit_DsdTest( unsigned * pTruth, int nVars )
 {
     Kit_DsdMan_t * p;
diff --git a/src/opt/kit/kitTruth.c b/src/opt/kit/kitTruth.c
index 62d4cf14..64a6a052 100644
--- a/src/opt/kit/kitTruth.c
+++ b/src/opt/kit/kitTruth.c
@@ -1216,7 +1216,7 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
 //    short pStore2[32];
     unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
     int nWords = Kit_TruthWordNum( nVars );
-    int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
+    int i, Temp, fChange, Counter;//, nOnes;//, k, j, w, Limit;
     unsigned uCanonPhase;
 
     // canonicize output
diff --git a/src/opt/res/resUpdate.c b/src/opt/res/resUpdate.c
index 01400ead..fb858658 100644
--- a/src/opt/res/resUpdate.c
+++ b/src/opt/res/resUpdate.c
@@ -25,14 +25,32 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the level of the node using its fanin levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i, Level = 0;
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Level = ABC_MAX( Level, (int)pFanin->Level );
+    return Level + 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Incrementally updates level of the nodes.]
 
   Description []
@@ -42,18 +60,10 @@ static int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj );
   SeeAlso     []
 
 ***********************************************************************/
-void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels )
+void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
 {
-    Abc_Obj_t * pObjNew, * pFanin, * pFanout, * pTemp;
+    Abc_Obj_t * pFanout, * pTemp;
     int Lev, k, m;
-    // create the new node
-    pObjNew = Abc_NtkCreateNode( pObj->pNtk );
-    pObjNew->pData = pFunc;
-    Vec_PtrForEachEntry( vFanins, pFanin, k )
-        Abc_ObjAddFanin( pObjNew, pFanin );
-    // replace the old node by the new node
-    pObjNew->Level = pObj->Level;
-    Abc_ObjReplace( pObj, pObjNew );
     // check if level has changed
     if ( (int)pObjNew->Level == Res_UpdateNetworkLevelNew(pObjNew) )
         return;
@@ -81,7 +91,7 @@ void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the level of the node using its fanin levels.]
+  Synopsis    [Incrementally updates level of the nodes.]
 
   Description []
                
@@ -90,13 +100,20 @@ void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc
   SeeAlso     []
 
 ***********************************************************************/
-int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj )
+void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels )
 {
-    Abc_Obj_t * pFanin;
-    int i, Level = 0;
-    Abc_ObjForEachFanin( pObj, pFanin, i )
-        Level = ABC_MAX( Level, (int)pFanin->Level );
-    return Level + 1;
+    Abc_Obj_t * pObjNew, * pFanin;
+    int k;
+    // create the new node
+    pObjNew = Abc_NtkCreateNode( pObj->pNtk );
+    pObjNew->pData = pFunc;
+    Vec_PtrForEachEntry( vFanins, pFanin, k )
+        Abc_ObjAddFanin( pObjNew, pFanin );
+    // replace the old node by the new node
+    pObjNew->Level = pObj->Level;
+    Abc_ObjReplace( pObj, pObjNew );
+    // update the level of the node
+    Res_UpdateNetworkLevel( pObjNew, vLevels );
 }
 
 ////////////////////////////////////////////////////////////////////////