Version abc70406

15 files changed, 831 insertions, 249 deletions

diff --git a/abc.rc b/abc.rc
index 2499e11d..16c03c65 100644
--- a/abc.rc
+++ b/abc.rc
@@ -30,6 +30,7 @@ alias fs fraig_sweep
 alias fsto fraig_store
 alias fres fraig_restore
 alias ft fraig_trust
+alias lp lutpack
 alias pex print_exdc -d
 alias pf print_factor
 alias pfan print_fanio
@@ -165,3 +166,5 @@ alias trec12   "rec_start -K 12; r i10.blif; st; rec_add; rec_use"
 alias tst4     "r i10_if4.blif; st; ps; r x/rec4_.blif; st; rec_start; r i10_if4.blif; st -r; ps; cec"
 alias tst4n    "r i10_if4.blif; st; ps; r 5npn/all_functions.aig; st; rec_start; r i10_if4.blif; st -r; ps; cec"
 alias tst6     "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_if6.blif; st -r; ps; cec"
+
+
diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index 44f5ac8e..8413fb02 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -314,6 +314,7 @@ extern void            Hop_TableProfile( Hop_Man_t * p );
 /*=== aigUtil.c =========================================================*/
 extern void            Hop_ManIncrementTravId( Hop_Man_t * p );
 extern void            Hop_ManCleanData( Hop_Man_t * p );
+extern void            Hop_ObjCleanData_rec( Hop_Obj_t * pObj );
 extern void            Hop_ObjCollectMulti( Hop_Obj_t * pFunc, Vec_Ptr_t * vSuper );
 extern int             Hop_ObjIsMuxType( Hop_Obj_t * pObj );
 extern int             Hop_ObjRecognizeExor( Hop_Obj_t * pObj, Hop_Obj_t ** ppFan0, Hop_Obj_t ** ppFan1 );
diff --git a/src/aig/hop/hopUtil.c b/src/aig/hop/hopUtil.c
index 9b5bf686..34f689f6 100644
--- a/src/aig/hop/hopUtil.c
+++ b/src/aig/hop/hopUtil.c
@@ -48,7 +48,7 @@ void Hop_ManIncrementTravId( Hop_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Sets the DFS ordering of the nodes.]
+  Synopsis    [Cleans the data pointers for the nodes.]
 
   Description []
                
@@ -73,6 +73,29 @@ void Hop_ManCleanData( Hop_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Recursively cleans the data pointers in the cone of the node.]
+
+  Description [Applicable to small AIGs only because no caching is performed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Hop_ObjCleanData_rec( Hop_Obj_t * pObj )
+{
+    assert( !Hop_IsComplement(pObj) );
+    assert( !Hop_ObjIsPo(pObj) );
+    if ( Hop_ObjIsAnd(pObj) )
+    {
+        Hop_ObjCleanData_rec( Hop_ObjFanin0(pObj) );
+        Hop_ObjCleanData_rec( Hop_ObjFanin1(pObj) );
+    }
+    pObj->pData = NULL;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Detects multi-input gate rooted at this node.]
 
   Description []
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index bf4aeb0f..c89e6b83 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -787,6 +787,7 @@ extern Vec_Ptr_t *        Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t *
 extern int                Abc_NodeMffcSize( Abc_Obj_t * pNode );
 extern int                Abc_NodeMffcSizeSupp( Abc_Obj_t * pNode );
 extern int                Abc_NodeMffcSizeStop( Abc_Obj_t * pNode );
+extern int                Abc_NodeMffcLabelAig( Abc_Obj_t * pNode );
 extern int                Abc_NodeMffcLabel( Abc_Obj_t * pNode );
 extern void               Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
 extern int                Abc_NodeDeref_rec( Abc_Obj_t * pNode );
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 24f10475..899cba96 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -523,7 +523,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_ObjName(pNode) );
+        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) );
         return 0;
     }
     // the netlist and SOP logic network should have SOPs
diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c
index bc9c316f..d30198c1 100644
--- a/src/base/abc/abcRefs.c
+++ b/src/base/abc/abcRefs.c
@@ -94,7 +94,7 @@ int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NodeMffcLabel( Abc_Obj_t * pNode )
+int Abc_NodeMffcLabelAig( Abc_Obj_t * pNode )
 {
     int nConeSize1, nConeSize2;
     assert( Abc_NtkIsStrash(pNode->pNtk) );
@@ -279,6 +279,7 @@ void Abc_NodeMffsConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t *
         Abc_NodeMffsConeSupp_rec( pFanin, vCone, vSupp, 0 );
     // collect the internal node
     if ( vCone ) Vec_PtrPush( vCone, pNode );
+//    printf( "%d ", pNode->Id );
 }
 
 /**Function*************************************************************
@@ -300,6 +301,7 @@ void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSu
     if ( vSupp ) Vec_PtrClear( vSupp );
     Abc_NtkIncrementTravId( pNode->pNtk );
     Abc_NodeMffsConeSupp_rec( pNode, vCone, vSupp, 1 );
+//    printf( "\n" );
 }
 
 /**Function*************************************************************
@@ -389,6 +391,60 @@ Vec_Ptr_t * Abc_NodeMffsInsideCollect( Abc_Obj_t * pNode )
     return vInside;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collects the internal and boundary nodes in the derefed MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeMffcLabel_rec( Abc_Obj_t * pNode, int fTopmost )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    // add to the new support nodes
+    if ( !fTopmost && (Abc_ObjIsCi(pNode) || pNode->vFanouts.nSize > 0) )
+        return;
+    // skip visited nodes
+    if ( Abc_NodeIsTravIdCurrent(pNode) )
+        return;
+    Abc_NodeSetTravIdCurrent(pNode);
+    // recur on the children
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        Abc_NodeMffcLabel_rec( pFanin, 0 );
+    // collect the internal node
+//    printf( "%d ", pNode->Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the internal nodes of the MFFC limited by cut.]
+
+  Description []
+               
+  SideEffects [Increments the trav ID and marks visited nodes.]
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeMffcLabel( Abc_Obj_t * pNode )
+{
+    int Count1, Count2;
+    // dereference the node
+    Count1 = Abc_NodeDeref_rec( pNode );
+    // collect the nodes inside the MFFC
+    Abc_NtkIncrementTravId( pNode->pNtk );
+    Abc_NodeMffcLabel_rec( pNode, 1 );
+    // reference it back
+    Count2 = Abc_NodeRef_rec( pNode );
+    assert( Count1 == Count2 );
+    return Count1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 753a2fb7..216a737a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -63,7 +63,7 @@ static int Abc_CommandSweep          ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandFastExtract    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDisjoint       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandImfs           ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandLutjam         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandLutpack        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandRewrite        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRefactor       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -218,7 +218,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "fx",            Abc_CommandFastExtract,      1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "dsd",           Abc_CommandDisjoint,         1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "imfs",          Abc_CommandImfs,             1 );
-    Cmd_CommandAdd( pAbc, "Synthesis",    "lutjam",        Abc_CommandLutjam,           1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "lutpack",       Abc_CommandLutpack,          1 );
 
     Cmd_CommandAdd( pAbc, "Synthesis",    "rewrite",       Abc_CommandRewrite,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "refactor",      Abc_CommandRefactor,         1 );
@@ -328,6 +328,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
 //    Abc_NtkPrint256();
 //    Kit_TruthCountMintermsPrecomp();
+//    Kit_DsdPrecompute4Vars();
 } 
 
 /**Function*************************************************************
@@ -1536,7 +1537,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
     // convert it to truth table
     {
         Abc_Obj_t * pObj = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
-        Vec_Int_t * vMemory = Vec_IntAlloc( 100 );
+        Vec_Int_t * vMemory = Vec_IntAlloc( 10000 );
         unsigned * pTruth;
         if ( !Abc_ObjIsNode(pObj) )
         {
@@ -1548,7 +1549,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "Currently works only for up to 8 inputs.\n" );
             return 1;
         }
-        pTruth = Abc_ConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 1 );
+        pTruth = Abc_ConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 0 );
         if ( Hop_IsComplement(pObj->pData) )
             Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) );
         Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
@@ -2889,7 +2890,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandLutjam( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -2907,7 +2908,7 @@ int Abc_CommandLutjam( 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    =  1; // (Q) the maximum number of LUTs not in the MFFC
+    pPars->nLutsOver    =  2; // (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->fVeryVerbose =  0;
@@ -2982,7 +2983,7 @@ int Abc_CommandLutjam( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: lutjam [-N <num>] [-Q <num>] [-S <num>] [-vwh]\n" );
+    fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-vwh]\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 );
diff --git a/src/base/abci/abcDsdRes.c b/src/base/abci/abcDsdRes.c
index 68748577..a76df9ce 100644
--- a/src/base/abci/abcDsdRes.c
+++ b/src/base/abci/abcDsdRes.c
@@ -41,6 +41,7 @@ struct Lut_Cut_t_
     unsigned     fMark         : 1;     // multipurpose mark
 //    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
     int          pNodes[LUT_SIZE_MAX];  // the nodes of the cut
 };
@@ -53,25 +54,35 @@ struct Lut_Man_t_
     Abc_Ntk_t *  pNtk;                  // the network
     Abc_Obj_t *  pObj;                  // the node to resynthesize 
     // cut representation
+    int          nMffc;                 // the size of MFFC of the node
     int          nCuts;                 // the total number of cuts    
     int          nCutsMax;              // the largest possible number of cuts
     int          nEvals;                // the number of good cuts
     Lut_Cut_t    pCuts[LUT_CUTS_MAX];   // the storage for cuts
-    int          pEvals[LUT_SIZE_MAX];  // the good cuts
+    int          pEvals[LUT_CUTS_MAX];  // the good cuts
     // temporary variables
     int          pRefs[LUT_SIZE_MAX];   // fanin reference counters 
     int          pCands[LUT_SIZE_MAX];  // internal nodes pointing only to the leaves
     // truth table representation
     Vec_Ptr_t *  vTtElems;              // elementary truth tables
     Vec_Ptr_t *  vTtNodes;              // storage for temporary truth tables of the nodes 
+    // statistics
+    int          nCutsTotal; 
+    int          nGainTotal;
+    // rutime
+    int          timeCuts;
+    int          timeTruth;
+    int          timeEval;
+    int          timeOther;
+    int          timeTotal;
 };
 
-static int Abc_LutResynthesizeNode( Lut_Man_t * p );
-
 #define Abc_LutCutForEachLeaf( pNtk, pCut, pObj, i )                                        \
     for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ )
 #define Abc_LutCutForEachNode( pNtk, pCut, pObj, i )                                        \
     for ( i = 0; (i < (int)(pCut)->nNodes) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i++ )
+#define Abc_LutCutForEachNodeReverse( pNtk, pCut, pObj, i )                                 \
+    for ( i = (int)(pCut)->nNodes - 1; (i >= 0) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i-- )
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -93,14 +104,15 @@ 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->nLutsMax );
-    p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nLutsMax) );
+    p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax );
+    p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nVarsMax) );
     return p;
 }
 
@@ -124,51 +136,6 @@ void Abc_LutManStop( Lut_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs resynthesis for one network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_LutResynthesize( Abc_Ntk_t * pNtk, Lut_Par_t * pPars )
-{
-    Lut_Man_t * p;
-    Abc_Obj_t * pObj;
-    int i;
-    assert( Abc_NtkIsLogic(pNtk) );
-    // convert logic to AIGs
-    Abc_NtkToAig( pNtk );
-    // compute the levels
-    Abc_NtkLevel( pNtk );
-    // start the manager
-    p = Abc_LutManStart( pPars );
-    p->pNtk = pNtk;
-    // get the number of inputs
-    p->pPars->nLutSize = Abc_NtkGetFaninMax( pNtk );
-    p->pPars->nVarsMax = p->pPars->nLutsMax * (p->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",
-        p->pPars->nLutsMax, p->pPars->nLutSize, p->pPars->nLutsOver, p->pPars->nVarsShared, p->pPars->nVarsMax );
-    // consider all nodes
-    Abc_NtkForEachNode( pNtk, pObj, i )
-    {
-        p->pObj = pObj;
-        Abc_LutResynthesizeNode( p );
-    }
-    Abc_LutManStop( p );
-    // check the resulting network
-    if ( !Abc_NtkCheck( pNtk ) )
-    {
-        printf( "Abc_LutResynthesize: The network check has failed.\n" );
-        return 0;
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Returns 1 if the cut has structural DSD.]
 
   Description []
@@ -216,7 +183,7 @@ int Abc_LutNodeCutsCheckDsd( Lut_Man_t * p, Lut_Cut_t * pCut )
             if ( p->pRefs[(int)pFanin->pCopy] > 1 )
                 break;
         }
-        if ( k == Abc_ObjFaninNum(pFanin) )
+        if ( k == Abc_ObjFaninNum(pObj) )
         {
             RetValue = 1;
             break;
@@ -316,6 +283,36 @@ int Abc_LutNodeCutsOneFilter( Lut_Cut_t * pCuts, int nCuts, Lut_Cut_t * pCutNew
 
 /**Function*************************************************************
 
+  Synopsis    [Prints the given cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_LutNodePrintCut( Lut_Man_t * p, Lut_Cut_t * pCut )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    printf( "LEAVES:\n" );
+    Abc_LutCutForEachLeaf( p->pNtk, pCut, pObj, i )
+    {
+        Abc_ObjPrint( stdout, pObj );
+    }
+    printf( "NODES:\n" );
+    Abc_LutCutForEachNode( p->pNtk, pCut, pObj, i )
+    {
+        Abc_ObjPrint( stdout, pObj );
+        assert( Abc_ObjIsNode(pObj) );
+    }
+    printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Computes the set of all cuts.]
 
   Description []
@@ -335,8 +332,14 @@ void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node )
     if ( pCut->nNodes == LUT_SIZE_MAX )
         return;
 
-    // if the node is not in the MFFC, check the limit
+    // if the node is a PI, quit
     pObj = Abc_NtkObj( p->pNtk, Node );
+    if ( Abc_ObjIsCi(pObj) )
+        return;
+    assert( Abc_ObjIsNode(pObj) );
+    assert( Abc_ObjFaninNum(pObj) <= p->pPars->nLutSize );
+
+    // if the node is not in the MFFC, check the limit
     if ( !Abc_NodeIsTravIdCurrent(pObj) )
     {
         if ( (int)pCut->nNodesMarked == p->pPars->nLutsOver )
@@ -344,8 +347,17 @@ void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node )
         assert( (int)pCut->nNodesMarked < p->pPars->nLutsOver );
     }
 
-    // create the new set of leaves
+    // initialize the set of leaves to the nodes in the cut
+    assert( p->nCuts < LUT_CUTS_MAX );
     pCutNew = p->pCuts + p->nCuts;
+/*
+if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1] == 34 && pCut->pNodes[2] == 35 )//p->nCuts == 48 )
+{
+    int x = 0;
+    printf( "Start:\n" );
+    Abc_LutNodePrintCut( p, pCut );
+}
+*/
     pCutNew->nLeaves = 0;
     for ( i = 0; i < (int)pCut->nLeaves; i++ )
         if ( pCut->pLeaves[i] != Node )
@@ -358,7 +370,7 @@ void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node )
         for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
             if ( pCutNew->pLeaves[k] >= pFanin->Id )
                 break;
-        if ( pCutNew->pLeaves[k] == pFanin->Id )
+        if ( k < (int)pCutNew->nLeaves && pCutNew->pLeaves[k] == pFanin->Id )
             continue;
         // check if there is room
         if ( (int)pCutNew->nLeaves == p->pPars->nVarsMax )
@@ -371,22 +383,34 @@ void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node )
         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
     if ( Abc_LutNodeCutsOneFilter( p->pCuts, p->nCuts, pCutNew ) )
         return;
 
     // update the set of internal nodes
     assert( pCut->nNodes < LUT_SIZE_MAX );
-    memcpy( pCutNew->pNodes, pCutNew->pNodes, pCut->nNodes * sizeof(int) );
-    pCutNew->pNodes[ pCut->nNodes++ ] = Node;
+    memcpy( pCutNew->pNodes, pCut->pNodes, pCut->nNodes * sizeof(int) );
+    pCutNew->nNodes = pCut->nNodes;
+    pCutNew->pNodes[ pCutNew->nNodes++ ] = Node;
 
     // add the marked node
     pCutNew->nNodesMarked = pCut->nNodesMarked + !Abc_NodeIsTravIdCurrent(pObj);
-
+/*
+if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 )
+{
+    int x = 0;
+    printf( "Finish:\n" );
+    Abc_LutNodePrintCut( p, pCutNew );
+}
+*/
     // add the cut to storage
     assert( p->nCuts < LUT_CUTS_MAX );
     p->nCuts++;
 
+    assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesMarked );
 }
 
 /**Function*************************************************************
@@ -407,13 +431,13 @@ int Abc_LutNodeCuts( Lut_Man_t * p )
     int i, k, Temp, nMffc, fChanges;
 
     // mark the MFFC of the node with the current trav ID
-    nMffc = Abc_NodeMffcLabel( p->pObj );
+    nMffc = p->nMffc = Abc_NodeMffcLabel( p->pObj );
     assert( nMffc > 0 );
     if ( nMffc == 1 )
         return 0;
 
     // initialize the first cut
-    pCut = p->pCuts;
+    pCut = p->pCuts; p->nCuts = 1;
     // assign internal nodes
     pCut->nNodes = 1; 
     pCut->pNodes[0] = p->pObj->Id;
@@ -439,10 +463,10 @@ int Abc_LutNodeCuts( Lut_Man_t * p )
     // perform the cut computation
     for ( i = 0; i < p->nCuts; i++ )
     {
-        pCut = p->pCuts + p->pEvals[i];
+        pCut = p->pCuts + i;
         if ( pCut->nLeaves == 0 )
             continue;
-        // try to expand each fanin of each cut
+        // try to expand the fanins of this cut
         for ( k = 0; k < (int)pCut->nLeaves; k++ )
         {
             Abc_LutNodeCutsOne( p, pCut, pCut->pLeaves[k] );
@@ -457,10 +481,14 @@ int Abc_LutNodeCuts( Lut_Man_t * p )
     p->nEvals = 0;
     for ( i = 0; i < p->nCuts; i++ )
     {
-        pCut = p->pCuts + p->pEvals[i];
+        pCut = p->pCuts + i;
+        if ( pCut->nLeaves == 0 )
+            continue;
         pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesMarked) / p->pPars->nLutsMax;
+        if ( pCut->Weight <= 1.0 )
+            continue;
         pCut->fHasDsd = Abc_LutNodeCutsCheckDsd( p, pCut );
-        if ( pCut->nLeaves == 0 || pCut->Weight <= 1.0 || pCut->fHasDsd )
+        if ( pCut->fHasDsd )
             continue;
         p->pEvals[p->nEvals++] = i;
     }
@@ -496,9 +524,77 @@ int Abc_LutNodeCuts( Lut_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+unsigned * Abc_LutCutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * iCount )
+{
+    unsigned * pTruth, * pTruth0, * pTruth1;
+    assert( !Hop_IsComplement(pObj) );
+    if ( pObj->pData )
+    {
+        assert( ((unsigned)pObj->pData) & 0xffff0000 );
+        return pObj->pData;
+    }
+    // get the plan for a new truth table
+    pTruth = Vec_PtrEntry( vTtNodes, (*iCount)++ );
+    if ( Hop_ObjIsConst1(pObj) )
+        Extra_TruthFill( pTruth, nVars );
+    else
+    {
+        assert( Hop_ObjIsAnd(pObj) );
+        // compute the truth tables of the fanins
+        pTruth0 = Abc_LutCutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, iCount );
+        pTruth1 = Abc_LutCutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, iCount );
+        // creat the truth table of the node
+        Extra_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) );
+    }
+    pObj->pData = pTruth;
+    return pTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth able of one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 unsigned * Abc_LutCutTruth( Lut_Man_t * p, Lut_Cut_t * pCut )
 {
-    unsigned * pTruth = NULL;
+    Hop_Man_t * pManHop = p->pNtk->pManFunc;
+    Hop_Obj_t * pObjHop;
+    Abc_Obj_t * pObj, * pFanin;
+    unsigned * pTruth;
+    int i, k, iCount = 0;
+//    Abc_LutNodePrintCut( p, pCut );
+
+    // initialize the leaves
+    Abc_LutCutForEachLeaf( p->pNtk, pCut, pObj, i )
+        pObj->pCopy = Vec_PtrEntry( p->vTtElems, i );
+
+    // construct truth table in the topological order
+    Abc_LutCutForEachNodeReverse( p->pNtk, pCut, pObj, i )
+    {
+        // get the local AIG
+        pObjHop = Hop_Regular(pObj->pData);
+        // clean the data field of the nodes in the AIG subgraph
+        Hop_ObjCleanData_rec( pObjHop );
+        // set the initial truth tables at the fanins
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            assert( ((unsigned)pFanin->pCopy) & 0xffff0000 );
+            Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
+        }
+        // compute the truth table of internal nodes
+        pTruth = Abc_LutCutTruth_rec( pManHop, pObjHop, pCut->nLeaves, p->vTtNodes, &iCount );
+        if ( Hop_IsComplement(pObj->pData) )
+            Extra_TruthNot( pTruth, pTruth, pCut->nLeaves );
+        // set the truth table at the node
+        pObj->pCopy = (Abc_Obj_t *)pTruth;
+    }
+
     return pTruth;
 }
 
@@ -531,28 +627,121 @@ int Abc_LutCutUpdate( Lut_Man_t * p, Lut_Cut_t * pCut, void * pDsd )
 ***********************************************************************/
 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 );
+
     Lut_Cut_t * pCut;
     unsigned * pTruth;
-    void * pDsd;
-    int i;
+    void * pDsd = NULL;
+    int i, Result, GainBest, Gain;
+    int clk;
     // compute the cuts
+clk = clock();
     if ( !Abc_LutNodeCuts( p ) )
+    {
+p->timeCuts += clock() - clk;
         return 0;
+    }
+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;
     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 );
-        // check decomposition
-        pDsd = /***/ NULL;
+p->timeTruth += clock() - clk;
+        // evaluate the result of decomposition        
+clk = clock();
+//        Kit_DsdTest( pTruth, pCut->nLeaves );
+        Result = Kit_DsdEval( pTruth, pCut->nLeaves, 3 );
+p->timeEval += clock() - clk;
+
+        // calculate the gain
+        Gain = Result < 0 ? 0 : pCut->nNodes - pCut->nNodesMarked - Result;
+        if ( GainBest < Gain )
+            GainBest = Gain;
+
+        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" );
+        }
+//        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 );
     }
+    p->nGainTotal += GainBest;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs resynthesis for one network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_LutResynthesize( Abc_Ntk_t * pNtk, Lut_Par_t * pPars )
+{
+    Lut_Man_t * p;
+    Abc_Obj_t * pObj;
+    int i, 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 );
+    // 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 );
+
+    Abc_LutManStop( p );
+    // check the resulting network
+    if ( !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Abc_LutResynthesize: The network check has failed.\n" );
+        return 0;
+    }
     return 1;
 }
 
diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c
index a81e94ad..e77f055a 100644
--- a/src/base/abci/abcReconv.c
+++ b/src/base/abci/abcReconv.c
@@ -712,7 +712,7 @@ Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Pt
 
     // mark MFFC 
     if ( pRoot )
-        Abc_NodeMffcLabel( pRoot );
+        Abc_NodeMffcLabelAig( pRoot );
 
     // go through the levels up
     Vec_PtrClear( p->vNodesTfo );
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 834e33aa..872ffaf0 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -248,7 +248,7 @@ p->timeFact += clock() - clk;
         pFanin->vFanouts.nSize++;
     // label MFFC with current traversal ID
     Abc_NtkIncrementTravId( pNode->pNtk );
-    nNodesSaved = Abc_NodeMffcLabel( pNode );
+    nNodesSaved = Abc_NodeMffcLabelAig( pNode );
     // unmark the fanin boundary and set the fanins as leaves in the form
     Vec_PtrForEachEntry( vFanins, pFanin, i )
     {
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index 2d4f50fb..b9ffd932 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -391,7 +391,7 @@ p->timeDsd += clock() - clk;
         pLeaf->vFanouts.nSize++;
     // label MFFC with current traversal ID
     Abc_NtkIncrementTravId( pRoot->pNtk );
-    nNodesSaved = Abc_NodeMffcLabel( pRoot );
+    nNodesSaved = Abc_NodeMffcLabelAig( pRoot );
     // unmark the fanin boundary and set the fanins as leaves in the form
     Vec_PtrForEachEntry( p->vLeaves, pLeaf, i )
         pLeaf->vFanouts.nSize--;
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index 19889fc4..12c54dba 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -1203,6 +1203,12 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
                     Vec_PtrPush( pMan->vNames, pEquation );
                     // get the buffer
                     pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf(Abc_FrameReadLibGen());
+                    if ( pFunc == NULL )
+                    {
+                        sprintf( pMan->sError, "Reading assign statement for node %s has failed because the genlib library has no buffer.", Abc_ObjName(pNet) );
+                        Ver_ParsePrintErrorMessage( pMan );
+                        return 0;
+                    }
                 }
             }
             else
@@ -1391,6 +1397,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
         Ver_ParsePrintErrorMessage( pMan );
         return 0;
     }
+    Ver_ParseSkipComments( pMan );
 
     // start the node
     pNode = Abc_NtkCreateNode( pNtk );
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 06ba309d..5a98348a 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -530,6 +530,30 @@ static inline void Extra_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned *
     for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
         pOut[w] = ~(pIn0[w] & pIn1[w]);
 }
+static inline void Extra_TruthAndPhase( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars, int fCompl0, int fCompl1 )
+{
+    int w;
+    if ( fCompl0 && fCompl1 )
+    {
+        for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = ~(pIn0[w] | pIn1[w]);
+    }
+    else if ( fCompl0 && !fCompl1 )
+    {
+        for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = ~pIn0[w] & pIn1[w];
+    }
+    else if ( !fCompl0 && fCompl1 )
+    {
+        for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = pIn0[w] & ~pIn1[w];
+    }
+    else // if ( !fCompl0 && !fCompl1 )
+    {
+        for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = pIn0[w] & pIn1[w];
+    }
+}
 
 extern unsigned ** Extra_TruthElementary( int nVars );
 extern void        Extra_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int Start );
diff --git a/src/opt/kit/kitDsd.c b/src/opt/kit/kitDsd.c
index dfe143be..3540fa03 100644
--- a/src/opt/kit/kitDsd.c
+++ b/src/opt/kit/kitDsd.c
@@ -24,9 +24,9 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Dsd_Man_t_ Dsd_Man_t;
-typedef struct Dsd_Ntk_t_ Dsd_Ntk_t;
-typedef struct Dsd_Obj_t_ Dsd_Obj_t;
+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 { 
@@ -39,7 +39,7 @@ typedef enum {
 } Kit_Dsd_t;
 
 // DSD manager
-struct Dsd_Man_t_
+struct Kit_DsdMan_t_
 {
     int            nVars;           // the maximum number of variables
     int            nWords;          // the number of words in TTs
@@ -48,18 +48,18 @@ struct Dsd_Man_t_
 };
 
 // DSD network
-struct Dsd_Ntk_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?)
-    Dsd_Obj_t *    pNodes[0];       // the nodes
+    Kit_DsdObj_t * pNodes[0];       // the nodes
 };
 
 // DSD node
-struct Dsd_Obj_t_
+struct Kit_DsdObj_t_
 { 
     unsigned       Id         : 6;  // the number of this node
     unsigned       Type       : 3;  // none, const, var, AND, XOR, MUX, PRIME
@@ -70,27 +70,27 @@ struct Dsd_Obj_t_
     unsigned char  pFans[0];        // the fanin literals
 };
 
-static inline int          Dsd_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
-static inline int          Dsd_Lit2Var( int Lit )             { return Lit >> 1;           }
-static inline int          Dsd_LitIsCompl( int Lit )          { return Lit & 1;            }
-static inline int          Dsd_LitNot( int Lit )              { return Lit ^ 1;            }
-static inline int          Dsd_LitNotCond( int Lit, int c )   { return Lit ^ (int)(c > 0); }
-static inline int          Dsd_LitRegular( int Lit )          { return Lit & 0xfe;         }
+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     Dsd_ObjOffset( int nFans )         { return (nFans >> 2) + ((nFans & 3) > 0); }
-static inline unsigned *   Dsd_ObjTruth( Dsd_Obj_t * pObj )   { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
-static inline Dsd_Obj_t *  Dsd_NtkObj( Dsd_Ntk_t * pNtk, int Id )  { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
-static inline Dsd_Obj_t *  Dsd_NtkRoot( Dsd_Ntk_t * pNtk )    { return Dsd_NtkObj( pNtk, Dsd_Lit2Var(pNtk->Root) ); }
+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 Dsd_NtkForEachObj( pNtk, pObj, i )                                      \
+#define Kit_DsdNtkForEachObj( pNtk, pObj, i )                                      \
     for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
-#define Dsd_ObjForEachFanin( pNtk, pObj, iLit, i )                              \
+#define Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )                              \
     for ( i = 0; (i < (pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
 
-extern unsigned *  Kit_DsdTruthCompute( Dsd_Man_t * p, Dsd_Ntk_t * pNtk );
-extern void        Kit_DsdPrint( FILE * pFile, Dsd_Ntk_t * pNtk );
-extern Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars );
-extern void        Kit_DsdNtkFree( Dsd_Ntk_t * pNtk );
+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                         ///
@@ -107,11 +107,11 @@ extern void        Kit_DsdNtkFree( Dsd_Ntk_t * pNtk );
   SeeAlso     []
 
 ***********************************************************************/
-Dsd_Man_t * Dsd_ManAlloc( int nVars )
+Kit_DsdMan_t * Kit_DsdManAlloc( int nVars )
 {
-    Dsd_Man_t * p;
-    p = ALLOC( Dsd_Man_t, 1 );
-    memset( p, 0, sizeof(Dsd_Man_t) );
+    Kit_DsdMan_t * p;
+    p = ALLOC( Kit_DsdMan_t, 1 );
+    memset( p, 0, sizeof(Kit_DsdMan_t) );
     p->nVars = nVars;
     p->nWords = Kit_TruthWordNum( p->nVars );
     p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
@@ -130,7 +130,7 @@ Dsd_Man_t * Dsd_ManAlloc( int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-void Dsd_ManFree( Dsd_Man_t * p )
+void Kit_DsdManFree( Kit_DsdMan_t * p )
 {
     Vec_PtrFree( p->vTtElems );
     Vec_PtrFree( p->vTtNodes );
@@ -148,16 +148,16 @@ void Dsd_ManFree( Dsd_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Dsd_Obj_t * Dsd_ObjAlloc( Dsd_Ntk_t * pNtk, Kit_Dsd_t Type, int nFans )
+Kit_DsdObj_t * Kit_DsdObjAlloc( Kit_DsdNtk_t * pNtk, Kit_Dsd_t Type, int nFans )
 {
-    Dsd_Obj_t * pObj;
-    int nSize = sizeof(Dsd_Obj_t) + sizeof(unsigned) * (Dsd_ObjOffset(nFans) + (Type == KIT_DSD_PRIME) * Kit_TruthWordNum(nFans));
-    pObj = (Dsd_Obj_t *)ALLOC( char, nSize );
+    Kit_DsdObj_t * pObj;
+    int nSize = sizeof(Kit_DsdObj_t) + sizeof(unsigned) * (Kit_DsdObjOffset(nFans) + (Type == KIT_DSD_PRIME) * Kit_TruthWordNum(nFans));
+    pObj = (Kit_DsdObj_t *)ALLOC( char, nSize );
     memset( pObj, 0, nSize );
     pObj->Id = pNtk->nVars + pNtk->nNodes;
     pObj->Type = Type;
     pObj->nFans = nFans;
-    pObj->Offset = Dsd_ObjOffset( nFans );
+    pObj->Offset = Kit_DsdObjOffset( nFans );
     // add the object
     assert( pNtk->nNodes < pNtk->nNodesAlloc );
     pNtk->pNodes[pNtk->nNodes++] = pObj;
@@ -175,7 +175,7 @@ Dsd_Obj_t * Dsd_ObjAlloc( Dsd_Ntk_t * pNtk, Kit_Dsd_t Type, int nFans )
   SeeAlso     []
 
 ***********************************************************************/
-void Dsd_ObjFree( Dsd_Ntk_t * p, Dsd_Obj_t * pObj )
+void Kit_DsdObjFree( Kit_DsdNtk_t * p, Kit_DsdObj_t * pObj )
 {
     free( pObj );
 }
@@ -191,12 +191,12 @@ void Dsd_ObjFree( Dsd_Ntk_t * p, Dsd_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-Dsd_Ntk_t * Kit_DsdNtkAlloc( int nVars )
+Kit_DsdNtk_t * Kit_DsdNtkAlloc( int nVars )
 {
-    Dsd_Ntk_t * pNtk;
-    int nSize = sizeof(Dsd_Ntk_t) + sizeof(void *) * nVars;
+    Kit_DsdNtk_t * pNtk;
+    int nSize = sizeof(Kit_DsdNtk_t) + sizeof(void *) * nVars;
     // allocate the network
-    pNtk = (Dsd_Ntk_t *)ALLOC( char, nSize );
+    pNtk = (Kit_DsdNtk_t *)ALLOC( char, nSize );
     memset( pNtk, 0, nSize );
     pNtk->nVars = nVars;
     pNtk->nNodesAlloc = nVars;
@@ -215,11 +215,11 @@ Dsd_Ntk_t * Kit_DsdNtkAlloc( int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdNtkFree( Dsd_Ntk_t * pNtk )
+void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk )
 {
-    Dsd_Obj_t * pObj;
+    Kit_DsdObj_t * pObj;
     unsigned i;
-    Dsd_NtkForEachObj( pNtk, pObj, i )
+    Kit_DsdNtkForEachObj( pNtk, pObj, i )
         free( pObj );
     free( pNtk->pMem );
     free( pNtk );
@@ -261,13 +261,13 @@ void Kit_DsdPrintHex( FILE * pFile, unsigned * pTruth, int nFans )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdPrint_rec( FILE * pFile, Dsd_Ntk_t * pNtk, int Id )
+void Kit_DsdPrint_rec( FILE * pFile, Kit_DsdNtk_t * pNtk, int Id )
 {
-    Dsd_Obj_t * pObj;
+    Kit_DsdObj_t * pObj;
     unsigned iLit, i;
     char Symbol;
 
-    pObj = Dsd_NtkObj( pNtk, Id );
+    pObj = Kit_DsdNtkObj( pNtk, Id );
     if ( pObj == NULL )
     {
         assert( Id < pNtk->nVars );
@@ -293,14 +293,14 @@ void Kit_DsdPrint_rec( FILE * pFile, Dsd_Ntk_t * pNtk, int Id )
         Symbol = ',';
 
     if ( pObj->Type == KIT_DSD_PRIME )
-        Kit_DsdPrintHex( stdout, Dsd_ObjTruth(pObj), pObj->nFans );
+        Kit_DsdPrintHex( stdout, Kit_DsdObjTruth(pObj), pObj->nFans );
 
     fprintf( pFile, "(" );
-    Dsd_ObjForEachFanin( pNtk, pObj, iLit, i )
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
     {
-        if ( Dsd_LitIsCompl(iLit) ) 
+        if ( Kit_DsdLitIsCompl(iLit) ) 
             fprintf( pFile, "!" );
-        Kit_DsdPrint_rec( pFile, pNtk, Dsd_Lit2Var(iLit) );
+        Kit_DsdPrint_rec( pFile, pNtk, Kit_DsdLit2Var(iLit) );
         if ( i < pObj->nFans - 1 )
             fprintf( pFile, "%c", Symbol );
     }
@@ -318,12 +318,12 @@ void Kit_DsdPrint_rec( FILE * pFile, Dsd_Ntk_t * pNtk, int Id )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdPrint( FILE * pFile, Dsd_Ntk_t * pNtk )
+void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk )
 {
     fprintf( pFile, "F = " );
-    if ( Dsd_LitIsCompl(pNtk->Root) )
+    if ( Kit_DsdLitIsCompl(pNtk->Root) )
         fprintf( pFile, "!" );
-    Kit_DsdPrint_rec( pFile, pNtk, Dsd_Lit2Var(pNtk->Root) );
+    Kit_DsdPrint_rec( pFile, pNtk, Kit_DsdLit2Var(pNtk->Root) );
     fprintf( pFile, "\n" );
 }
 
@@ -338,14 +338,14 @@ void Kit_DsdPrint( FILE * pFile, Dsd_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id )
+unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id )
 {
-    Dsd_Obj_t * pObj;
+    Kit_DsdObj_t * pObj;
     unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16];
     unsigned i, m, iLit, nMints, fCompl;
 
     // get the node with this ID
-    pObj = Dsd_NtkObj( pNtk, Id );
+    pObj = Kit_DsdNtkObj( pNtk, Id );
     pTruthRes = Vec_PtrEntry( p->vTtNodes, Id );
 
     // special case: literal of an internal node
@@ -368,8 +368,8 @@ unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id
     {
         assert( pObj->nFans == 1 );
         iLit = pObj->pFans[0];
-        pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Dsd_Lit2Var(iLit) );
-        if ( Dsd_LitIsCompl(iLit) )
+        pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) );
+        if ( Kit_DsdLitIsCompl(iLit) )
             Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars );
         else
             Kit_TruthCopy( pTruthRes, pTruthFans[0], pNtk->nVars );
@@ -377,26 +377,26 @@ unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id
     }
 
     // collect the truth tables of the fanins
-    Dsd_ObjForEachFanin( pNtk, pObj, iLit, i )
-        pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Dsd_Lit2Var(iLit) );
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+        pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) );
     // create the truth table
 
     // simple gates
     if ( pObj->Type == KIT_DSD_AND )
     {
         Kit_TruthFill( pTruthRes, pNtk->nVars );
-        Dsd_ObjForEachFanin( pNtk, pObj, iLit, i )
-            Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Dsd_LitIsCompl(iLit) );
+        Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+            Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) );
         return pTruthRes;
     }
     if ( pObj->Type == KIT_DSD_XOR )
     {
         Kit_TruthClear( pTruthRes, pNtk->nVars );
         fCompl = 0;
-        Dsd_ObjForEachFanin( pNtk, pObj, iLit, i )
+        Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
         {
             Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
-            fCompl ^= Dsd_LitIsCompl(iLit);
+            fCompl ^= Kit_DsdLitIsCompl(iLit);
         }
         if ( fCompl )
             Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
@@ -405,7 +405,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id
     assert( pObj->Type == KIT_DSD_PRIME );
 
     // get the truth table of the prime node
-    pTruthPrime = Dsd_ObjTruth( pObj );
+    pTruthPrime = Kit_DsdObjTruth( pObj );
     // get storage for the temporary minterm
     pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes);
 
@@ -417,8 +417,8 @@ unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id
         if ( !Kit_TruthHasBit(pTruthPrime, m) )
             continue;
         Kit_TruthFill( pTruthMint, pNtk->nVars );
-        Dsd_ObjForEachFanin( pNtk, pObj, iLit, i )
-            Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, Dsd_LitIsCompl(iLit) );
+        Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+            Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) );
         Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
     }
     return pTruthRes;
@@ -435,7 +435,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Kit_DsdTruthCompute( Dsd_Man_t * p, Dsd_Ntk_t * pNtk )
+unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk )
 {
     unsigned * pTruthRes;
     int i;
@@ -444,13 +444,81 @@ unsigned * Kit_DsdTruthCompute( Dsd_Man_t * p, Dsd_Ntk_t * pNtk )
     for ( i = 0; i < (int)pNtk->nVars; i++ )
         Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars );
     // compute truth table for each node
-    pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Dsd_Lit2Var(pNtk->Root) );
+    pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root) );
     // complement the truth table if needed
-    if ( Dsd_LitIsCompl(pNtk->Root) )
+    if ( Kit_DsdLitIsCompl(pNtk->Root) )
         Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
     return pTruthRes;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of blocks of the given number of inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdCountLuts_rec( Kit_DsdNtk_t * pNtk, int nLutSize, int Id, int * pCounter )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned iLit, i, Res0, Res1;
+    pObj = Kit_DsdNtkObj( pNtk, Id );
+    if ( pObj == NULL )
+        return 0;
+    if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
+    {
+        assert( pObj->nFans == 2 );
+        Res0 = Kit_DsdCountLuts_rec( pNtk, nLutSize, Kit_DsdLit2Var(pObj->pFans[0]), pCounter );
+        Res1 = Kit_DsdCountLuts_rec( pNtk, nLutSize, Kit_DsdLit2Var(pObj->pFans[1]), pCounter );
+        if ( Res0 == 0 && Res1 > 0 )
+            return Res1 - 1;
+        if ( Res0 > 0 && Res1 == 0 )
+            return Res0 - 1;
+        (*pCounter)++;
+        return nLutSize - 2;
+    }
+    assert( pObj->Type == KIT_DSD_PRIME );
+    if ( (int)pObj->nFans > nLutSize )
+    {
+        *pCounter = 1000;
+        return 0;
+    }
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+        Kit_DsdCountLuts_rec( pNtk, nLutSize, Kit_DsdLit2Var(iLit), pCounter );
+    (*pCounter)++;
+    return nLutSize - pObj->nFans;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of blocks of the given number of inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdCountLuts( Kit_DsdNtk_t * pNtk, int nLutSize )
+{
+    int Counter = 0;
+    if ( Kit_DsdNtkRoot(pNtk)->Type == KIT_DSD_CONST1 )
+        return 0;
+    if ( Kit_DsdNtkRoot(pNtk)->Type == KIT_DSD_VAR )
+        return 0;
+    Kit_DsdCountLuts_rec( pNtk, nLutSize, Kit_DsdLit2Var(pNtk->Root), &Counter );
+    if ( Counter >= 1000 )
+        return -1;
+    return Counter;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Expands the node.]
@@ -462,19 +530,19 @@ unsigned * Kit_DsdTruthCompute( Dsd_Man_t * p, Dsd_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdExpandCollectAnd_rec( Dsd_Ntk_t * p, int iLit, int * piLitsNew, int * nLitsNew )
+void Kit_DsdExpandCollectAnd_rec( Kit_DsdNtk_t * p, int iLit, int * piLitsNew, int * nLitsNew )
 {
-    Dsd_Obj_t * pObj;
+    Kit_DsdObj_t * pObj;
     unsigned i, iLitFanin;
     // check the end of the supergate
-    pObj = Dsd_NtkObj( p, Dsd_Lit2Var(iLit) );
-    if ( Dsd_LitIsCompl(iLit) || Dsd_Lit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_AND )
+    pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
+    if ( Kit_DsdLitIsCompl(iLit) || Kit_DsdLit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_AND )
     {
         piLitsNew[(*nLitsNew)++] = iLit;
         return;
     }
     // iterate through the fanins
-    Dsd_ObjForEachFanin( p, pObj, iLitFanin, i )
+    Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
         Kit_DsdExpandCollectAnd_rec( p, iLitFanin, piLitsNew, nLitsNew );
 }
 
@@ -489,24 +557,24 @@ void Kit_DsdExpandCollectAnd_rec( Dsd_Ntk_t * p, int iLit, int * piLitsNew, int
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdExpandCollectXor_rec( Dsd_Ntk_t * p, int iLit, int * piLitsNew, int * nLitsNew )
+void Kit_DsdExpandCollectXor_rec( Kit_DsdNtk_t * p, int iLit, int * piLitsNew, int * nLitsNew )
 {
-    Dsd_Obj_t * pObj;
+    Kit_DsdObj_t * pObj;
     unsigned i, iLitFanin;
     // check the end of the supergate
-    pObj = Dsd_NtkObj( p, Dsd_Lit2Var(iLit) );
-    if ( Dsd_Lit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_XOR )
+    pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
+    if ( Kit_DsdLit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_XOR )
     {
         piLitsNew[(*nLitsNew)++] = iLit;
         return;
     }
     // iterate through the fanins
-    pObj = Dsd_NtkObj( p, Dsd_Lit2Var(iLit) );
-    Dsd_ObjForEachFanin( p, pObj, iLitFanin, i )
+    pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
+    Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
         Kit_DsdExpandCollectXor_rec( p, iLitFanin, piLitsNew, nLitsNew );
     // if the literal was complemented, pass the complemented attribute somewhere
-    if ( Dsd_LitIsCompl(iLit) )
-        piLitsNew[0] = Dsd_LitNot( piLitsNew[0] );
+    if ( Kit_DsdLitIsCompl(iLit) )
+        piLitsNew[0] = Kit_DsdLitNot( piLitsNew[0] );
 }
 
 /**Function*************************************************************
@@ -520,61 +588,63 @@ void Kit_DsdExpandCollectXor_rec( Dsd_Ntk_t * p, int iLit, int * piLitsNew, int
   SeeAlso     []
 
 ***********************************************************************/
-int Kit_DsdExpandNode_rec( Dsd_Ntk_t * pNew, Dsd_Ntk_t * p, int iLit )
+int Kit_DsdExpandNode_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit )
 {
     unsigned * pTruth, * pTruthNew;
     unsigned i, fCompl, iLitFanin, piLitsNew[16], nLitsNew = 0;
-    Dsd_Obj_t * pObj, * pObjNew;
+    Kit_DsdObj_t * pObj, * pObjNew;
 
     // remember the complement
-    fCompl = Dsd_LitIsCompl(iLit); 
-    iLit = Dsd_LitRegular(iLit); 
-    assert( !Dsd_LitIsCompl(iLit) );
+    fCompl = Kit_DsdLitIsCompl(iLit); 
+    iLit = Kit_DsdLitRegular(iLit); 
+    assert( !Kit_DsdLitIsCompl(iLit) );
 
     // consider the case of simple gate
-    pObj = Dsd_NtkObj( p, Dsd_Lit2Var(iLit) );
+    pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
+    if ( pObj == NULL )
+        return Kit_DsdLitNotCond( iLit, fCompl );
     if ( pObj->Type == KIT_DSD_AND )
     {
         Kit_DsdExpandCollectAnd_rec( p, iLit, piLitsNew, &nLitsNew );
-        pObjNew = Dsd_ObjAlloc( pNew, KIT_DSD_AND, nLitsNew );
+        pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, nLitsNew );
         for ( i = 0; i < pObjNew->nFans; i++ )
             pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, piLitsNew[i] );
-        return Dsd_Var2Lit( pObjNew->Id, fCompl );
+        return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
     }
     if ( pObj->Type == KIT_DSD_XOR )
     {
         Kit_DsdExpandCollectXor_rec( p, iLit, piLitsNew, &nLitsNew );
-        pObjNew = Dsd_ObjAlloc( pNew, KIT_DSD_XOR, nLitsNew );
+        pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, nLitsNew );
         for ( i = 0; i < pObjNew->nFans; i++ )
         {
-            pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, Dsd_LitRegular(piLitsNew[i]) );
-            fCompl ^= Dsd_LitIsCompl(piLitsNew[i]);
+            pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, Kit_DsdLitRegular(piLitsNew[i]) );
+            fCompl ^= Kit_DsdLitIsCompl(piLitsNew[i]);
         }
-        return Dsd_Var2Lit( pObjNew->Id, fCompl );
+        return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
     }
     assert( pObj->Type == KIT_DSD_PRIME );
 
     // create new PRIME node
-    pObjNew = Dsd_ObjAlloc( pNew, KIT_DSD_PRIME, pObj->nFans );
+    pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_PRIME, pObj->nFans );
     // copy the truth table
-    pTruth = Dsd_ObjTruth( pObj );
-    pTruthNew = Dsd_ObjTruth( pObjNew );
+    pTruth = Kit_DsdObjTruth( pObj );
+    pTruthNew = Kit_DsdObjTruth( pObjNew );
     Kit_TruthCopy( pTruthNew, pTruth, pObj->nFans );
     // create fanins
-    Dsd_ObjForEachFanin( pNtk, pObj, iLitFanin, i )
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
     {
         pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, iLitFanin );
         // complement the corresponding inputs of the truth table
-        if ( Dsd_LitIsCompl(pObjNew->pFans[i]) )
+        if ( Kit_DsdLitIsCompl(pObjNew->pFans[i]) )
         {
-            pObjNew->pFans[i] = Dsd_LitRegular(pObjNew->pFans[i]);
+            pObjNew->pFans[i] = Kit_DsdLitRegular(pObjNew->pFans[i]);
             Kit_TruthChangePhase( pTruthNew, pObjNew->nFans, i );
         }
     }
     // if the incoming phase is complemented, absorb it into the prime node
     if ( fCompl )
         Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
-    return Dsd_Var2Lit( pObjNew->Id, 0 );
+    return Kit_DsdVar2Lit( pObjNew->Id, 0 );
 }
 
 /**Function*************************************************************
@@ -588,25 +658,25 @@ int Kit_DsdExpandNode_rec( Dsd_Ntk_t * pNew, Dsd_Ntk_t * p, int iLit )
   SeeAlso     []
 
 ***********************************************************************/
-Dsd_Ntk_t * Kit_DsdExpand( Dsd_Ntk_t * p )
+Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p )
 {
-    Dsd_Ntk_t * pNew;
-    Dsd_Obj_t * pObjNew;
+    Kit_DsdNtk_t * pNew;
+    Kit_DsdObj_t * pObjNew;
     assert( p->nVars <= 16 );
     // create a new network
     pNew = Kit_DsdNtkAlloc( p->nVars );
     // consider simple special cases
-    if ( Dsd_NtkRoot(p)->Type == KIT_DSD_CONST1 )
+    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
     {
-        pObjNew = Dsd_ObjAlloc( pNew, KIT_DSD_CONST1, 0 );
-        pNew->Root = Dsd_Var2Lit( pObjNew->Id, Dsd_LitIsCompl(p->Root) );
+        pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
+        pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) );
         return pNew;
     }
-    if ( Dsd_NtkRoot(p)->Type == KIT_DSD_VAR )
+    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
     {
-        pObjNew = Dsd_ObjAlloc( pNew, KIT_DSD_VAR, 1 );
-        pObjNew->pFans[0] = Dsd_NtkRoot(p)->pFans[0];
-        pNew->Root = Dsd_Var2Lit( pObjNew->Id, Dsd_LitIsCompl(p->Root) );
+        pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
+        pObjNew->pFans[0] = Kit_DsdNtkRoot(p)->pFans[0];
+        pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) );
         return pNew;
     }
     // convert the root node
@@ -625,21 +695,86 @@ Dsd_Ntk_t * Kit_DsdExpand( Dsd_Ntk_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Kit_DsdFindLargeBox( Dsd_Ntk_t * pNtk, int Id )
+int Kit_DsdFindLargeBox_rec( Kit_DsdNtk_t * pNtk, int Id, int Size )
 {
-    Dsd_Obj_t * pObj;
+    Kit_DsdObj_t * pObj;
     unsigned iLit, i, RetValue;
-    pObj = Dsd_NtkObj( pNtk, Id );
-    if ( pObj->nFans > 3 )
+    pObj = Kit_DsdNtkObj( pNtk, Id );
+    if ( pObj == NULL )
+        return 0;
+    if ( pObj->Type == KIT_DSD_PRIME && (int)pObj->nFans > Size )
         return 1;
     RetValue = 0;
-    Dsd_ObjForEachFanin( pNtk, pObj, iLit, i )
-        RetValue |= Kit_DsdFindLargeBox( pNtk, Dsd_Lit2Var(iLit) );
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+        RetValue |= Kit_DsdFindLargeBox_rec( pNtk, Kit_DsdLit2Var(iLit), Size );
     return RetValue;
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if there is a component with more than 3 inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdFindLargeBox( Kit_DsdNtk_t * pNtk, int Size )
+{
+    return Kit_DsdFindLargeBox_rec( pNtk, Kit_DsdLit2Var(pNtk->Root), Size );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the non-DSD 4-var func is implementable with two 3-LUTs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdRootNodeHasCommonVars( Kit_DsdObj_t * pObj0, Kit_DsdObj_t * pObj1 )
+{
+    unsigned i, k;
+    for ( i = 0; i < pObj0->nFans; i++ )
+    {
+        if ( Kit_DsdLit2Var(pObj0->pFans[i]) >= 4 )
+            continue;
+        for ( k = 0; k < pObj1->nFans; k++ )
+            if ( Kit_DsdLit2Var(pObj0->pFans[i]) == Kit_DsdLit2Var(pObj1->pFans[k]) )
+                return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the non-DSD 4-var func is implementable with two 3-LUTs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdCheckVar4Dec2( Kit_DsdNtk_t * pNtk0, Kit_DsdNtk_t * pNtk1 )
+{
+    assert( pNtk0->nVars == 4 );
+    assert( pNtk1->nVars == 4 );
+    if ( Kit_DsdFindLargeBox(pNtk0, 2) )
+        return 0;
+    if ( Kit_DsdFindLargeBox(pNtk1, 2) )
+        return 0;
+    return Kit_DsdRootNodeHasCommonVars( Kit_DsdNtkRoot(pNtk0), Kit_DsdNtkRoot(pNtk1) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs decomposition of the node.]
 
   Description []
@@ -649,11 +784,11 @@ int Kit_DsdFindLargeBox( Dsd_Ntk_t * pNtk, int Id )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, unsigned char * pPar )
+void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned char * pPar )
 {
-    Dsd_Obj_t * pRes, * pRes0, * pRes1;
+    Kit_DsdObj_t * pRes, * pRes0, * pRes1;
     int nWords = Kit_TruthWordNum(pObj->nFans);
-    unsigned * pTruth = Dsd_ObjTruth(pObj);
+    unsigned * pTruth = Kit_DsdObjTruth(pObj);
     unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + nWords };
     unsigned * pCofs4[2][2] = { {pNtk->pMem + 2 * nWords, pNtk->pMem + 3 * nWords}, {pNtk->pMem + 4 * nWords, pNtk->pMem + 5 * nWords} };
     int i, iLit0, iLit1, nFans0, nFans1, nPairs;
@@ -682,12 +817,11 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
     {
         pObj->Type = KIT_DSD_NONE;
         if ( pTruth[0] == 0x55555555 )
-            pObj->pFans[0] = Dsd_LitNot(pObj->pFans[0]);
+            pObj->pFans[0] = Kit_DsdLitNot(pObj->pFans[0]);
         else
             assert( pTruth[0] == 0xAAAAAAAA );
         // update the parent pointer
-//        assert( !Dsd_LitIsCompl(*pPar) );
-        *pPar = Dsd_LitNotCond( pObj->pFans[0], Dsd_LitIsCompl(*pPar) );
+        *pPar = Kit_DsdLitNotCond( pObj->pFans[0], Kit_DsdLitIsCompl(*pPar) );
         return;
     }
 
@@ -716,22 +850,22 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
             if ( uSupp0 & uSupp1 )
                 continue;
             // perform MUX decomposition
-            pRes0 = Dsd_ObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
-            pRes1 = Dsd_ObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
+            pRes0 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
+            pRes1 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
             for ( k = 0; k < pObj->nFans; k++ )
             {
                 pRes0->pFans[k] = (uSupp0 & (1 << k))? pObj->pFans[k] : 127;
                 pRes1->pFans[k] = (uSupp1 & (1 << k))? pObj->pFans[k] : 127;
             }
-            Kit_TruthCopy( Dsd_ObjTruth(pRes0), pCofs2[0], pObj->nFans );        
-            Kit_TruthCopy( Dsd_ObjTruth(pRes1), pCofs2[1], pObj->nFans ); 
+            Kit_TruthCopy( Kit_DsdObjTruth(pRes0), pCofs2[0], pObj->nFans );        
+            Kit_TruthCopy( Kit_DsdObjTruth(pRes1), pCofs2[1], pObj->nFans ); 
             // update the current one
             assert( pObj->Type == KIT_DSD_PRIME );
             pTruth[0] = 0xCACACACA;
             pObj->nFans = 3;
+            pObj->pFans[2] = pObj->pFans[i];
             pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++;
             pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++;
-            pObj->pFans[2] = pObj->pFans[i];
             // call recursively
             Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0 );
             Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1 );
@@ -740,13 +874,13 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
 //Extra_PrintBinary( stdout, pTruth, 1 << pObj->nFans ); printf( "\n" );
 
         // create the new node
-        pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_AND, 2 );
+        pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_AND, 2 );
         pRes->nRefs++;
         pRes->nFans = 2;
         pRes->pFans[0] = pObj->pFans[i];  pObj->pFans[i] = 127;  uSupp &= ~(1 << i);
         pRes->pFans[1] = 2*pObj->Id;
         // update the parent pointer
-        *pPar = 2 * pRes->Id;
+        *pPar = Kit_DsdLitNotCond( 2 * pRes->Id, Kit_DsdLitIsCompl(*pPar) );
         // consider different decompositions
         if ( fEquals[0][0] )
         {
@@ -754,20 +888,20 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
         }
         else if ( fEquals[0][1] )
         {
-            pRes->pFans[0] = Dsd_LitNot(pRes->pFans[0]);
+            pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);
             Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
         }
         else if ( fEquals[1][0] )
         {
-            *pPar = Dsd_LitNot(*pPar);
-            pRes->pFans[1] = Dsd_LitNot(pRes->pFans[1]);
+            *pPar = Kit_DsdLitNot(*pPar);
+            pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]);
             Kit_TruthCopy( pTruth, pCofs2[1], pObj->nFans );
         }
         else if ( fEquals[1][1] )
         {
-            *pPar = Dsd_LitNot(*pPar);
-            pRes->pFans[0] = Dsd_LitNot(pRes->pFans[0]);  
-            pRes->pFans[1] = Dsd_LitNot(pRes->pFans[1]);
+            *pPar = Kit_DsdLitNot(*pPar);
+            pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);  
+            pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]);
             Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
         }
         else if ( fOppos )
@@ -778,7 +912,7 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
         else
             assert( 0 );
         // decompose the remainder
-        assert( Dsd_ObjTruth(pObj) == pTruth );
+        assert( Kit_DsdObjTruth(pObj) == pTruth );
         Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pRes->pFans + 1 );
         return;
     }
@@ -824,18 +958,21 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
             if ( (fEquals[0][0] && fEquals[0][1]) || (fEquals[1][0] && fEquals[1][1]) )
             {
                 // construct the MUX
-                pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_PRIME, 3 );
-                Dsd_ObjTruth(pRes)[0] = 0xCACACACA;
+                pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, 3 );
+                Kit_DsdObjTruth(pRes)[0] = 0xCACACACA;
                 pRes->nRefs++;
                 pRes->nFans = 3;
                 pRes->pFans[0] = pObj->pFans[iLit0]; pObj->pFans[iLit0] = 127;  uSupp &= ~(1 << iLit0);
                 pRes->pFans[1] = pObj->pFans[iLit1]; pObj->pFans[iLit1] = 127;  uSupp &= ~(1 << iLit1);
                 pRes->pFans[2] = pObj->pFans[i];     pObj->pFans[i] = 2 * pRes->Id; // remains in support
                 // update the node
-                if ( fEquals[0][0] && fEquals[0][1] )
-                    Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i );
-                else
-                    Kit_TruthMux( pTruth, pCofs4[0][1], pCofs4[0][0], pObj->nFans, i );
+//                if ( fEquals[0][0] && fEquals[0][1] )
+//                    Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i );
+//                else
+//                    Kit_TruthMux( pTruth, pCofs4[0][1], pCofs4[0][0], pObj->nFans, i );
+                Kit_TruthMux( pTruth, pCofs4[1][0], pCofs4[1][1], pObj->nFans, i );
+                if ( fEquals[1][0] && fEquals[1][1] )
+                    pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);
                 // decompose the remainder
                 Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar );
                 return;
@@ -862,25 +999,25 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
                 continue;
 
             // decomposition exists
-            pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_AND, 2 );
+            pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_AND, 2 );
             pRes->nRefs++;
             pRes->nFans = 2;
             pRes->pFans[0] = pObj->pFans[k]; pObj->pFans[k] = 2 * pRes->Id;  // remains in support
             pRes->pFans[1] = pObj->pFans[i]; pObj->pFans[i] = 127;       uSupp &= ~(1 << i);
             if ( !fPairs[0][1] && !fPairs[0][2] && !fPairs[0][3] ) // 00
             {
-                pRes->pFans[0] = Dsd_LitNot(pRes->pFans[0]);  
-                pRes->pFans[1] = Dsd_LitNot(pRes->pFans[1]);
+                pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);  
+                pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]);
                 Kit_TruthMux( pTruth, pCofs4[1][1], pCofs4[0][0], pObj->nFans, k );
             }
             else if ( !fPairs[1][0] && !fPairs[1][2] && !fPairs[1][3] ) // 01
             {
-                pRes->pFans[0] = Dsd_LitNot(pRes->pFans[0]);  
+                pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]);  
                 Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
             }
             else if ( !fPairs[2][0] && !fPairs[2][1] && !fPairs[2][3] ) // 10
             {
-                pRes->pFans[1] = Dsd_LitNot(pRes->pFans[1]);  
+                pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);  
                 Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[1][0], pObj->nFans, k );
             }
             else if ( !fPairs[3][0] && !fPairs[3][1] && !fPairs[3][2] ) // 11
@@ -918,21 +1055,21 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
   SeeAlso     []
 
 ***********************************************************************/
-Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
+Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
 {
-    Dsd_Ntk_t * pNtk;
-    Dsd_Obj_t * pObj;
+    Kit_DsdNtk_t * pNtk;
+    Kit_DsdObj_t * pObj;
     unsigned uSupp;
     int i, nVarsReal;
     assert( nVars <= 16 );
     pNtk = Kit_DsdNtkAlloc( nVars );
-    pNtk->Root = Dsd_Var2Lit( pNtk->nVars, 0 );
+    pNtk->Root = Kit_DsdVar2Lit( pNtk->nVars, 0 );
     // create the first node
-    pObj = Dsd_ObjAlloc( pNtk, KIT_DSD_PRIME, nVars );
+    pObj = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, nVars );
     assert( pNtk->pNodes[0] == pObj );
     for ( i = 0; i < nVars; i++ )
-       pObj->pFans[i] = Dsd_Var2Lit( i, 0 );
-    Kit_TruthCopy( Dsd_ObjTruth(pObj), pTruth, nVars );
+       pObj->pFans[i] = Kit_DsdVar2Lit( i, 0 );
+    Kit_TruthCopy( Kit_DsdObjTruth(pObj), pTruth, nVars );
     uSupp = Kit_TruthSupport( pTruth, nVars );
     // consider special cases
     nVarsReal = Kit_WordCountOnes( uSupp );
@@ -941,14 +1078,14 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
         pObj->Type = KIT_DSD_CONST1;
         pObj->nFans = 0;
         if ( pTruth[0] == 0 )
-             pNtk->Root = Dsd_LitNot(pNtk->Root);
+             pNtk->Root = Kit_DsdLitNot(pNtk->Root);
         return pNtk;
     }
     if ( nVarsReal == 1 )
     {
         pObj->Type = KIT_DSD_VAR;
         pObj->nFans = 1;
-        pObj->pFans[0] = Dsd_Var2Lit( Kit_WordFindFirstBit(uSupp), (pTruth[0] & 1) );
+        pObj->pFans[0] = Kit_DsdVar2Lit( Kit_WordFindFirstBit(uSupp), (pTruth[0] & 1) );
         return pNtk;
     }
     Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], uSupp, &pNtk->Root );
@@ -966,17 +1103,18 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdTestCofs( Dsd_Ntk_t * pNtk, unsigned * pTruthInit )
+int Kit_DsdTestCofs( Kit_DsdNtk_t * pNtk, unsigned * pTruthInit )
 {
-    Dsd_Ntk_t * pNtk0, * pNtk1;
-//    Dsd_Obj_t * pRoot;
+    Kit_DsdNtk_t * pNtk0, * pNtk1, * pTemp;
+//    Kit_DsdObj_t * pRoot;
     unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) };
     unsigned i, * pTruth;
-    int fVerbose = 1;
+    int fVerbose = 0;
+    int RetValue = 0;
 
     pTruth = pTruthInit;
-//    pRoot = Dsd_NtkRoot(pNtk);
-//    pTruth = Dsd_ObjTruth(pRoot);
+//    pRoot = Kit_DsdNtkRoot(pNtk);
+//    pTruth = Kit_DsdObjTruth(pRoot);
 //    assert( pRoot->nFans == pNtk->nVars );
 
     if ( fVerbose )
@@ -991,24 +1129,72 @@ void Kit_DsdTestCofs( Dsd_Ntk_t * pNtk, unsigned * pTruthInit )
     {
         Kit_TruthCofactor0New( pCofs2[0], pTruth, pNtk->nVars, i );
         pNtk0 = Kit_DsdDecompose( pCofs2[0], pNtk->nVars );
+        pNtk0 = Kit_DsdExpand( pTemp = pNtk0 );
+        Kit_DsdNtkFree( pTemp );
+
         if ( fVerbose )
         {
             printf( "Cof%d0: ", i );
             Kit_DsdPrint( stdout, pNtk0 );
         }
-        Kit_DsdNtkFree( pNtk0 );
 
         Kit_TruthCofactor1New( pCofs2[1], pTruth, pNtk->nVars, i );
         pNtk1 = Kit_DsdDecompose( pCofs2[1], pNtk->nVars );
+        pNtk1 = Kit_DsdExpand( pTemp = pNtk1 );
+        Kit_DsdNtkFree( pTemp );
+
         if ( fVerbose )
         {
             printf( "Cof%d1: ", i );
             Kit_DsdPrint( stdout, pNtk1 );
         }
+
+        if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) )
+            RetValue = 1;
+
         Kit_DsdNtkFree( pNtk0 );
+        Kit_DsdNtkFree( pNtk1 );
     }
     if ( fVerbose )
         printf( "\n" );
+
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
+{
+    Kit_DsdMan_t * p;
+    Kit_DsdNtk_t * pNtk;
+    unsigned * pTruthC;
+    int Result;
+
+    // decompose the function
+    pNtk = Kit_DsdDecompose( pTruth, nVars );
+    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;
 }
 
 /**Function*************************************************************
@@ -1024,19 +1210,110 @@ void Kit_DsdTestCofs( Dsd_Ntk_t * pNtk, unsigned * pTruthInit )
 ***********************************************************************/
 void Kit_DsdTest( unsigned * pTruth, int nVars )
 {
-    Dsd_Ntk_t * pNtk;
+    Kit_DsdMan_t * p;
+    unsigned * pTruthC;
+    Kit_DsdNtk_t * pNtk, * pTemp;
     pNtk = Kit_DsdDecompose( pTruth, nVars );
 
-//    if ( Kit_DsdFindLargeBox(pNtk, Dsd_Lit2Var(pNtk->Root)) )
+//    if ( Kit_DsdFindLargeBox(pNtk, Kit_DsdLit2Var(pNtk->Root)) )
 //        Kit_DsdPrint( stdout, pNtk );
 
-//    if ( Dsd_NtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 6 )
+//    if ( Kit_DsdNtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 6 )
+
+    printf( "\n" );
+    Kit_DsdPrint( stdout, pNtk );
+
+    pNtk = Kit_DsdExpand( pTemp = pNtk );
+    Kit_DsdNtkFree( pTemp );
+
+    Kit_DsdPrint( stdout, pNtk );
+
+//    if ( Kit_DsdFindLargeBox(pNtk, Kit_DsdLit2Var(pNtk->Root)) )
+//        Kit_DsdTestCofs( pNtk, pTruth );
+
+    // recompute the truth table
+    p = Kit_DsdManAlloc( nVars );
+    pTruthC = Kit_DsdTruthCompute( p, pNtk );
+//    Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" );
+//    Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" );
+    if ( Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
+    {
+//        printf( "Verification is okay.\n" );
+    }
+    else
+        printf( "Verification failed.\n" );
+    Kit_DsdManFree( p );
 
-    Kit_DsdTestCofs( pNtk, pTruth );
 
     Kit_DsdNtkFree( pNtk );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdPrecompute4Vars()
+{
+    Kit_DsdMan_t * p;
+    Kit_DsdNtk_t * pNtk, * pTemp;
+    FILE * pFile;
+    unsigned uTruth;
+    unsigned * pTruthC;
+    char Buffer[256];
+    int i, RetValue;
+    int Counter1 = 0, Counter2 = 0;
+
+    pFile = fopen( "5npn/npn4.txt", "r" );
+    for ( i = 0; fgets( Buffer, 100, pFile ); i++ )
+    {
+        Buffer[6] = 0;
+        Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 );
+        uTruth = ((uTruth & 0xffff) << 16) | (uTruth & 0xffff);
+        pNtk = Kit_DsdDecompose( &uTruth, 4 );
+
+        pNtk = Kit_DsdExpand( pTemp = pNtk );
+        Kit_DsdNtkFree( pTemp );
+
+
+        if ( Kit_DsdFindLargeBox(pNtk, 3) )
+        {
+//            RetValue = 0;
+            RetValue = Kit_DsdTestCofs( pNtk, &uTruth );
+            printf( "\n" );
+            printf( "%3d : Non-DSD function  %s  %s\n", i, Buffer + 2, RetValue? "implementable" : "" );
+            Kit_DsdPrint( stdout, pNtk );
+
+            Counter1++;
+            Counter2 += RetValue;
+        }
+
+/*
+        printf( "%3d : Function  %s   ", i, Buffer + 2 );
+        if ( !Kit_DsdFindLargeBox(pNtk, 3) )
+            Kit_DsdPrint( stdout, pNtk );
+        else
+            printf( "\n" );
+*/
+
+        p = Kit_DsdManAlloc( 4 );
+        pTruthC = Kit_DsdTruthCompute( p, pNtk );
+        if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) )
+            printf( "Verification failed.\n" );
+        Kit_DsdManFree( p );
+
+        Kit_DsdNtkFree( pNtk );
+    }
+    fclose( pFile );
+    printf( "non-DSD = %d   implementable = %d\n", Counter1, Counter2 );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index b53fe7df..e5b27138 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -129,7 +129,7 @@ clk2 = clock();
 
         // label MFFC with current ID
         Abc_NtkIncrementTravId( pNode->pNtk );
-        nNodesSaved = Abc_NodeMffcLabel( pNode );
+        nNodesSaved = Abc_NodeMffcLabelAig( pNode );
         // unmark the fanin boundary
         Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
             Abc_ObjRegular(pFanin)->vFanouts.nSize--;