Version abc70317

24 files changed, 1697 insertions, 147 deletions

diff --git a/abc.dsp b/abc.dsp
index ed7ae4e4..8bdabae4 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -466,6 +466,10 @@ SOURCE=.\src\base\io\ioReadBlifMv.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\io\ioReadDsd.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\io\ioReadEdif.c
 # End Source File
 # Begin Source File
@@ -1674,6 +1678,10 @@ SOURCE=.\src\opt\kit\kitBdd.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\opt\kit\kitDsd.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\kit\kitFactor.c
 # End Source File
 # Begin Source File
diff --git a/abc.rc b/abc.rc
index 33bc0c96..e7b0d9f1 100644
--- a/abc.rc
+++ b/abc.rc
@@ -124,9 +124,6 @@ alias fflitmin    "compress2rs; ren; sop; ps -f"
 #alias ttb      "wh a/quip_opt/nut_001_opt.blif 1.blif"
 #alias ttv      "wh a/quip_opt/nut_001_opt.blif 1.v"
 
-alias t        "r c.blif; st; haig_start; resyn; haig_use"
-alias tt       "r i10.blif; st; haig_start; resyn2; haig_use"
-
 alias reach    "st; ps; compress2; ps; qrel; ps; compress2; ps; qreach -v; ps"
 
 alias qs1      "qvar -I 96 -u; ps; qbf -P 96" 
@@ -139,3 +136,18 @@ alias qs7      "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar
 alias qs8      "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; ps; qbf -P 96" 
 alias qs9      "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; qvar -I 104 -u; ps; qbf -P 96" 
 alias qsA      "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; qvar -I 104 -u; qvar -I 105 -u; ps; qbf -P 96" 
+
+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"
+alias t3       "read_dsd 56BA(a,b*c,e,d); clp -r; print_dsd"
+alias t4       "read_dsd 56BA(a,b*c,e+d,f); clp -r; print_dsd"
+alias t5       "read_dsd 56BA(a,CA(b,c,d),e,f); clp -r; print_dsd"
+alias t6       "read_dsd f*CA(b,c,d)*CA(e,a,g); clp -r; print_dsd"
+
diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index 34124599..44f5ac8e 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -81,7 +81,7 @@ struct Hop_Man_t_
     // AIG nodes
     Vec_Ptr_t *      vPis;           // the array of PIs
     Vec_Ptr_t *      vPos;           // the array of POs
-    Vec_Ptr_t *      vNodes;         // the array of all nodes (optional)
+    Vec_Ptr_t *      vObjs;          // the array of all nodes (optional)
     Hop_Obj_t *      pConst1;        // the constant 1 node
     Hop_Obj_t        Ghost;          // the ghost node
     // AIG node counters
@@ -131,6 +131,8 @@ static inline Hop_Obj_t *  Hop_ManConst0( Hop_Man_t * p )         { return Hop_N
 static inline Hop_Obj_t *  Hop_ManConst1( Hop_Man_t * p )         { return p->pConst1;                              }
 static inline Hop_Obj_t *  Hop_ManGhost( Hop_Man_t * p )          { return &p->Ghost;                               }
 static inline Hop_Obj_t *  Hop_ManPi( Hop_Man_t * p, int i )      { return (Hop_Obj_t *)Vec_PtrEntry(p->vPis, i);   }
+static inline Hop_Obj_t *  Hop_ManPo( Hop_Man_t * p, int i )      { return (Hop_Obj_t *)Vec_PtrEntry(p->vPos, i);   }
+static inline Hop_Obj_t *  Hop_ManObj( Hop_Man_t * p, int i )     { return p->vObjs ? (Hop_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL;  }
 
 static inline Hop_Edge_t   Hop_EdgeCreate( int Id, int fCompl )            { return (Id << 1) | fCompl;             }
 static inline int          Hop_EdgeId( Hop_Edge_t Edge )                   { return Edge >> 1;                      }
@@ -223,10 +225,10 @@ static inline Hop_Obj_t * Hop_ManFetchMemory( Hop_Man_t * p )
     pTemp = p->pListFree;
     p->pListFree = *((Hop_Obj_t **)pTemp);
     memset( pTemp, 0, sizeof(Hop_Obj_t) ); 
-    if ( p->vNodes )
+    if ( p->vObjs )
     {
-        assert( p->nCreated == Vec_PtrSize(p->vNodes) );
-        Vec_PtrPush( p->vNodes, pTemp );
+        assert( p->nCreated == Vec_PtrSize(p->vObjs) );
+        Vec_PtrPush( p->vObjs, pTemp );
     }
     pTemp->Id = p->nCreated++;
     return pTemp;
diff --git a/src/aig/hop/hopMan.c b/src/aig/hop/hopMan.c
index 4fa52fbd..b7858564 100644
--- a/src/aig/hop/hopMan.c
+++ b/src/aig/hop/hopMan.c
@@ -94,10 +94,10 @@ void Hop_ManStop( Hop_Man_t * p )
     if ( p->time1 ) { PRT( "time1", p->time1 ); }
     if ( p->time2 ) { PRT( "time2", p->time2 ); }
 //    Hop_TableProfile( p );
-    if ( p->vChunks )   Hop_ManStopMemory( p );
-    if ( p->vPis )      Vec_PtrFree( p->vPis );
-    if ( p->vPos )      Vec_PtrFree( p->vPos );
-    if ( p->vNodes )    Vec_PtrFree( p->vNodes );
+    if ( p->vChunks )  Hop_ManStopMemory( p );
+    if ( p->vPis )     Vec_PtrFree( p->vPis );
+    if ( p->vPos )     Vec_PtrFree( p->vPos );
+    if ( p->vObjs )    Vec_PtrFree( p->vObjs );
     free( p->pTable );
     free( p );
 }
@@ -115,20 +115,20 @@ void Hop_ManStop( Hop_Man_t * p )
 ***********************************************************************/
 int Hop_ManCleanup( Hop_Man_t * p )
 {
-    Vec_Ptr_t * vNodes;
+    Vec_Ptr_t * vObjs;
     Hop_Obj_t * pNode;
     int i, nNodesOld;
     assert( p->fRefCount );
     nNodesOld = Hop_ManNodeNum(p);
     // collect roots of dangling nodes
-    vNodes = Vec_PtrAlloc( 100 );
+    vObjs = Vec_PtrAlloc( 100 );
     Hop_ManForEachNode( p, pNode, i )
         if ( Hop_ObjRefs(pNode) == 0 )
-            Vec_PtrPush( vNodes, pNode );
+            Vec_PtrPush( vObjs, pNode );
     // recursively remove dangling nodes
-    Vec_PtrForEachEntry( vNodes, pNode, i )
+    Vec_PtrForEachEntry( vObjs, pNode, i )
         Hop_ObjDelete_rec( p, pNode );
-    Vec_PtrFree( vNodes );
+    Vec_PtrFree( vObjs );
     return nNodesOld - Hop_ManNodeNum(p);
 }
 
diff --git a/src/aig/hop/hopObj.c b/src/aig/hop/hopObj.c
index c4430abd..c8e70dd3 100644
--- a/src/aig/hop/hopObj.c
+++ b/src/aig/hop/hopObj.c
@@ -73,7 +73,7 @@ Hop_Obj_t * Hop_ObjCreatePo( Hop_Man_t * p, Hop_Obj_t * pDriver )
     else
         pObj->nRefs = Hop_ObjLevel( Hop_Regular(pDriver) );
     // set the phase
-//    pObj->fPhase = Hop_ObjFaninPhase(pDriver);
+    pObj->fPhase = Hop_ObjFaninPhase(pDriver);
     // update node counters of the manager
     p->nObjs[AIG_PO]++;
     return pObj;
@@ -136,7 +136,7 @@ void Hop_ObjConnect( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFan0, Hop_Obj
     else
         pObj->nRefs = Hop_ObjLevelNew( pObj );
     // set the phase
-//    pObj->fPhase = Hop_ObjFaninPhase(pFan0) & Hop_ObjFaninPhase(pFan1);
+    pObj->fPhase = Hop_ObjFaninPhase(pFan0) & Hop_ObjFaninPhase(pFan1);
     // add the node to the structural hash table
     Hop_TableInsert( p, pObj );
 }
@@ -236,9 +236,10 @@ void Hop_ObjDelete_rec( Hop_Man_t * p, Hop_Obj_t * pObj )
 ***********************************************************************/
 Hop_Obj_t * Hop_ObjRepr( Hop_Obj_t * pObj )
 {
-    if ( Hop_Regular(pObj)->pData == NULL )
-        return Hop_Regular(pObj);
-    return Hop_ObjRepr( Hop_Regular(pObj)->pData );
+    assert( !Hop_IsComplement(pObj) );
+    if ( pObj->pData == NULL || pObj->pData == pObj )
+        return pObj;
+    return Hop_ObjRepr( pObj->pData );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 3a278927..ececd26f 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -616,7 +616,7 @@ extern int                Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
 extern void               Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkAigToBdd( Abc_Ntk_t * pNtk );
-extern unsigned *         Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth );
+extern unsigned *         Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst );
 extern int                Abc_NtkMapToSop( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect );
 extern int                Abc_NtkToBdd( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 03f41f3b..2bfad15b 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -866,7 +866,7 @@ unsigned * Abc_ConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth )
+unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst )
 {
     static unsigned uTruths[8][8] = { // elementary truth tables
         { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
@@ -899,9 +899,18 @@ unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, V
         return pTruth;
     }
     // set elementary truth tables at the leaves
+    assert( nVars <= Hop_ManPiNum(p) );
     assert( Hop_ManPiNum(p) <= 8 ); 
-    Hop_ManForEachPi( p, pObj, i )
-        pObj->pData = (void *)uTruths[i];
+    if ( fMsbFirst )
+    {
+        Hop_ManForEachPi( p, pObj, i )
+            pObj->pData = (void *)uTruths[nVars-1-i];
+    }
+    else
+    {
+        Hop_ManForEachPi( p, pObj, i )
+            pObj->pData = (void *)uTruths[i];
+    }
     // clear the marks and compute the truth table
     pTruth2 = Abc_ConvertAigToTruth_rec2( pRoot, vTruth, nWords );
     // copy the result
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index a39bd7bf..01fa8e13 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -855,7 +855,8 @@ char * Abc_SopFromTruthBin( char * pTruth )
     {
         pCube = pSopCover + i * (nVars + 3);
         for ( b = 0; b < nVars; b++ )
-            if ( Mint & (1 << b) )
+            if ( Mint & (1 << (nVars-1-b)) )
+//            if ( Mint & (1 << b) )
                 pCube[b] = '1';
             else
                 pCube[b] = '0';
@@ -921,7 +922,8 @@ char * Abc_SopFromTruthHex( char * pTruth )
     {
         pCube = pSopCover + i * (nVars + 3);
         for ( b = 0; b < nVars; b++ )
-            if ( Mint & (1 << b) )
+            if ( Mint & (1 << (nVars-1-b)) )
+//            if ( Mint & (1 << b) )
                 pCube[b] = '1';
             else
                 pCube[b] = '0';
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4aa13733..9138d897 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -47,6 +47,7 @@ static int Abc_CommandPrintKMap      ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandPrintGates     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintSharing   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintXCut      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintDsd       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandShow           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShowBdd        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -61,7 +62,7 @@ static int Abc_CommandCleanup        ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandSweep          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 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_CommandIfs            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandImfs           ( 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 );
@@ -194,6 +195,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Printing",     "print_gates",   Abc_CommandPrintGates,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_sharing", Abc_CommandPrintSharing,     0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_xcut",    Abc_CommandPrintXCut,        0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_dsd",     Abc_CommandPrintDsd,         0 );
 
     Cmd_CommandAdd( pAbc, "Printing",     "show",          Abc_CommandShow,             0 );
     Cmd_CommandAdd( pAbc, "Printing",     "show_bdd",      Abc_CommandShowBdd,          0 );
@@ -208,7 +210,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "sweep",         Abc_CommandSweep,            1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "fx",            Abc_CommandFastExtract,      1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "dsd",           Abc_CommandDisjoint,         1 );
-    Cmd_CommandAdd( pAbc, "Synthesis",    "ifs",           Abc_CommandIfs,              1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "imfs",          Abc_CommandImfs,             1 );
 
     Cmd_CommandAdd( pAbc, "Synthesis",    "rewrite",       Abc_CommandRewrite,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "refactor",      Abc_CommandRefactor,         1 );
@@ -1463,6 +1465,92 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int fUseLibrary;
+
+    extern void Kit_DsdTest( unsigned * pTruth, int nVars );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fUseLibrary = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'l':
+            fUseLibrary ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    // get the truth table of the first output
+    if ( !Abc_NtkIsLogic(pNtk) )
+    {
+        fprintf( pErr, "Currently works only for logic networks.\n" );
+        return 1;
+    }
+    Abc_NtkToAig( pNtk );
+    // convert it to truth table
+    {
+        Abc_Obj_t * pObj = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
+        Vec_Int_t * vMemory = Vec_IntAlloc( 100 );
+        unsigned * pTruth;
+        if ( !Abc_ObjIsNode(pObj) )
+        {
+            fprintf( pErr, "The fanin of the first PO node does not have a logic function.\n" );
+            return 1;
+        }
+        if ( Abc_ObjFaninNum(pObj) > 8 )
+        {
+            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 );
+        if ( Hop_IsComplement(pObj->pData) )
+            Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) );
+        Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
+        printf( "\n" );
+        Kit_DsdTest( pTruth, Abc_ObjFaninNum(pObj) );
+        Vec_IntFree( vMemory );
+    }
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: print_dsd [-h]\n" );
+    fprintf( pErr, "\t        print DSD formula for a single-output function with less than 16 variables\n" );
+//    fprintf( pErr, "\t-l    : used library gate names (if mapped) [default = %s]\n", fUseLibrary? "yes": "no" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
@@ -2649,7 +2737,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandIfs( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -2756,7 +2844,7 @@ int Abc_CommandIfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ifs [-W <NM>] [-L <num>] [-C <num>] [-S <num>] [-avwh]\n" );
+    fprintf( pErr, "usage: imfs [-W <NM>] [-L <num>] [-C <num>] [-S <num>] [-avwh]\n" );
     fprintf( pErr, "\t           performs resubstitution-based resynthesis with interpolation\n" );
     fprintf( pErr, "\t-W <NM>  : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
     fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
diff --git a/src/base/abci/abcHaig.c b/src/base/abci/abcHaig.c
index 87fada22..a0ed5906 100644
--- a/src/base/abci/abcHaig.c
+++ b/src/base/abci/abcHaig.c
@@ -57,8 +57,8 @@ int Abc_NtkHaigStart( Abc_Ntk_t * pNtk )
         assert( pObj->pEquiv == NULL );
     // start the HOP package
     p = Hop_ManStart();
-    p->vNodes = Vec_PtrAlloc( 4096 );
-    Vec_PtrPush( p->vNodes, Hop_ManConst1(p) );
+    p->vObjs = Vec_PtrAlloc( 4096 );
+    Vec_PtrPush( p->vObjs, Hop_ManConst1(p) );
     // map the constant node
     Abc_AigConst1(pNtk)->pEquiv = Hop_ManConst1(p);
     // map the CIs
@@ -149,7 +149,6 @@ void Abc_NtkHaigTranfer( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew )
 
 
 
-
 /**Function*************************************************************
 
   Synopsis    [Collects the nodes in the classes.]
@@ -163,18 +162,18 @@ void Abc_NtkHaigTranfer( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew )
 ***********************************************************************/
 Vec_Ptr_t * Abc_NtkHaigCollectMembers( Hop_Man_t * p )
 {
-    Vec_Ptr_t * vNodes;
+    Vec_Ptr_t * vObjs;
     Hop_Obj_t * pObj;
     int i;
-    vNodes = Vec_PtrAlloc( 4098 );
-    Vec_PtrForEachEntry( p->vNodes, pObj, i )
+    vObjs = Vec_PtrAlloc( 4098 );
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
     {
         if ( pObj->pData == NULL )
             continue;
         pObj->pData = Hop_ObjRepr( pObj );
-        Vec_PtrPush( vNodes, pObj );
+        Vec_PtrPush( vObjs, pObj );
     }
-    return vNodes;
+    return vObjs;
 }
 
 /**Function*************************************************************
@@ -235,10 +234,15 @@ Vec_Ptr_t * Abc_NtkHaigCreateClasses( Vec_Ptr_t * vMembers )
     {
         pRepr = pObj->pData;
         assert( pRepr->pData == pRepr );
-        pRepr->pData = NULL;
+//        pRepr->pData = NULL;
         Vec_PtrWriteEntry( vClasses, i, pRepr );
         Vec_PtrPush( vMembers, pObj );
     }
+
+    Vec_PtrForEachEntry( vMembers, pObj, i )
+        if ( pObj->pData == pObj )
+            pObj->pData = NULL;
+
 /*
     Vec_PtrForEachEntry( vMembers, pObj, i )
     {
@@ -258,6 +262,122 @@ Vec_Ptr_t * Abc_NtkHaigCreateClasses( Vec_Ptr_t * vMembers )
     return vClasses;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Counts how many data members have non-trivial fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkHaigCountFans( Hop_Man_t * p )
+{
+    Hop_Obj_t * pObj;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        if ( pObj->pData == NULL )
+            continue;
+        if ( Hop_ObjRefs(pObj) > 0 )
+            Counter++;
+    }
+    printf( "The number of class members with fanouts = %5d.\n", Counter );
+    return Counter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Hop_Obj_t * Hop_ObjReprHop( Hop_Obj_t * pObj )
+{
+    Hop_Obj_t * pRepr;
+    assert( pObj->pNext != NULL );
+    if ( pObj->pData == NULL )
+        return pObj->pNext;
+    pRepr = pObj->pData;
+    assert( pRepr->pData == pRepr );
+    return Hop_NotCond( pRepr->pNext, pObj->fPhase ^ pRepr->fPhase );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Hop_Obj_t * Hop_ObjChild0Hop( Hop_Obj_t * pObj ) { return Hop_NotCond( Hop_ObjReprHop(Hop_ObjFanin0(pObj)), Hop_ObjFaninC0(pObj) ); }
+static inline Hop_Obj_t * Hop_ObjChild1Hop( Hop_Obj_t * pObj ) { return Hop_NotCond( Hop_ObjReprHop(Hop_ObjFanin1(pObj)), Hop_ObjFaninC1(pObj) ); }
+
+/**Function*************************************************************
+
+  Synopsis    [Stops history AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Man_t * Abc_NtkHaigReconstruct( Hop_Man_t * p )
+{ 
+    Hop_Man_t * pNew;
+    Hop_Obj_t * pObj;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+        pObj->pNext = NULL;
+    // start the HOP package
+    pNew = Hop_ManStart();
+    pNew->vObjs = Vec_PtrAlloc( p->nCreated );
+    Vec_PtrPush( pNew->vObjs, Hop_ManConst1(pNew) );
+    // map the constant node
+    Hop_ManConst1(p)->pNext = Hop_ManConst1(pNew);
+    // map the CIs
+    Hop_ManForEachPi( p, pObj, i )
+        pObj->pNext = Hop_ObjCreatePi(pNew);
+    // map the internal nodes
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        if ( !Hop_ObjIsNode(pObj) )
+            continue;
+        pObj->pNext = Hop_And( pNew, Hop_ObjChild0Hop(pObj), Hop_ObjChild1Hop(pObj) );
+//        assert( !Hop_IsComplement(pObj->pNext) );
+        if ( Hop_ManConst1(pNew) == Hop_Regular(pObj->pNext) )
+            Counter++;
+        if ( pObj->pData ) // member of the class
+            Hop_Regular(pObj->pNext)->pData = Hop_Regular(((Hop_Obj_t *)pObj->pData)->pNext);
+    }
+    printf( " Counter = %d.\n", Counter );
+    // transfer the POs
+    Hop_ManForEachPo( p, pObj, i )
+        Hop_ObjCreatePo( pNew, Hop_ObjChild0Hop(pObj) );
+    // check the new manager
+    if ( !Hop_ManCheck(pNew) )
+    {
+        printf( "Abc_NtkHaigReconstruct: Check for History AIG has failed.\n" );
+        Hop_ManStop(pNew);
+        return NULL;
+    }
+    return pNew;
+}
+
 
 /**Function*************************************************************
 
@@ -277,7 +397,7 @@ int Abc_NtkHaigCheckTfi_rec( Abc_Obj_t * pNode, Abc_Obj_t * pOld )
     if ( pNode == pOld )
         return 1;
     // check the trivial cases
-    if ( Abc_ObjIsPi(pNode) )
+    if ( Abc_ObjIsCi(pNode) )
         return 0;
     assert( Abc_ObjIsNode(pNode) );
     // if this node is already visited, skip
@@ -324,36 +444,8 @@ int Abc_NtkHaigCheckTfi( Abc_Ntk_t * pNtk, Abc_Obj_t * pOld, Abc_Obj_t * pNew )
   SeeAlso     []
 
 ***********************************************************************/
-static inline Abc_Obj_t * Hop_ObjReprAbc( Hop_Obj_t * pObj )
-{
-    Hop_Obj_t * pRepr;
-    Abc_Obj_t * pObjAbcThis, * pObjAbcRepr;
-    assert( pObj->pNext != NULL );
-    if ( pObj->pData == NULL )
-        return (Abc_Obj_t *)pObj->pNext;
-    pRepr = pObj->pData;
-    assert( pRepr->pData == NULL );
-    pObjAbcThis = (Abc_Obj_t *)pObj->pNext;
-    pObjAbcRepr = (Abc_Obj_t *)pRepr->pNext;
-    assert( !Abc_ObjIsComplement(pObjAbcThis) );
-    assert( !Abc_ObjIsComplement(pObjAbcRepr) );
-    return Abc_ObjNotCond( pObjAbcRepr, pObjAbcRepr->fPhase ^ pObjAbcThis->fPhase );
-//    return (Abc_Obj_t *)pObj->pNext;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Abc_Obj_t * Hop_ObjChild0Abc( Hop_Obj_t * pObj ) { return Abc_ObjNotCond( Hop_ObjReprAbc(Hop_ObjFanin0(pObj)), Hop_ObjFaninC0(pObj) ); }
-static inline Abc_Obj_t * Hop_ObjChild1Abc( Hop_Obj_t * pObj ) { return Abc_ObjNotCond( Hop_ObjReprAbc(Hop_ObjFanin1(pObj)), Hop_ObjFaninC1(pObj) ); }
+static inline Abc_Obj_t * Hop_ObjChild0Next( Hop_Obj_t * pObj ) { return Abc_ObjNotCond( (Abc_Obj_t *)Hop_ObjFanin0(pObj)->pNext, Hop_ObjFaninC0(pObj) );  }
+static inline Abc_Obj_t * Hop_ObjChild1Next( Hop_Obj_t * pObj ) { return Abc_ObjNotCond( (Abc_Obj_t *)Hop_ObjFanin1(pObj)->pNext, Hop_ObjFaninC1(pObj) );  }
 
 /**Function*************************************************************
 
@@ -369,13 +461,10 @@ static inline Abc_Obj_t * Hop_ObjChild1Abc( Hop_Obj_t * pObj ) { return Abc_ObjN
 Abc_Ntk_t * Abc_NtkHaigRecreateAig( Abc_Ntk_t * pNtk, Hop_Man_t * p )
 {
     Abc_Ntk_t * pNtkAig;
-    Abc_Obj_t * pObjAbcThis, * pObjAbcRepr;
-    Abc_Obj_t * pObjOld, * pObjNew;
+    Abc_Obj_t * pObjOld, * pObjAbcThis, * pObjAbcRepr;
     Hop_Obj_t * pObj;
     int i;
-
-    assert( p->nCreated == Vec_PtrSize(p->vNodes) );
-    assert( Hop_ManPoNum(p) == 0 );
+    assert( p->nCreated == Vec_PtrSize(p->vObjs) );
 
     // start the new network
     pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
@@ -383,51 +472,42 @@ Abc_Ntk_t * Abc_NtkHaigRecreateAig( Abc_Ntk_t * pNtk, Hop_Man_t * p )
     // transfer new nodes to the PIs of HOP
     Hop_ManConst1(p)->pNext = (Hop_Obj_t *)Abc_AigConst1( pNtkAig );
     Hop_ManForEachPi( p, pObj, i )
-        pObj->pNext = (Hop_Obj_t *)Abc_NtkPi( pNtkAig, i );
+        pObj->pNext = (Hop_Obj_t *)Abc_NtkCi( pNtkAig, i );
 
     // construct new nodes
-    Vec_PtrForEachEntry( p->vNodes, pObj, i )
-        if ( Hop_ObjIsNode(pObj) )
-            pObj->pNext = (Hop_Obj_t *)Abc_AigAnd( pNtkAig->pManFunc, Hop_ObjChild0Abc(pObj), Hop_ObjChild1Abc(pObj) );
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        if ( !Hop_ObjIsNode(pObj) )
+            continue;
+        pObj->pNext = (Hop_Obj_t *)Abc_AigAnd( pNtkAig->pManFunc, Hop_ObjChild0Next(pObj), Hop_ObjChild1Next(pObj) );
+        assert( !Hop_IsComplement(pObj->pNext) );
+    }
 
     // set the COs
     Abc_NtkForEachCo( pNtk, pObjOld, i )
-    {
-        pObjNew = Hop_ObjReprAbc( Abc_ObjFanin0(pObjOld)->pEquiv );
-        pObjNew = Abc_ObjNotCond( pObjNew, Abc_ObjFaninC0(pObjOld) );
-        Abc_ObjAddFanin( pObjOld->pCopy, pObjNew );
-    }
+        Abc_ObjAddFanin( pObjOld->pCopy, Hop_ObjChild0Next(Hop_ManPo(p,i)) );
 
-    // create choice nodes
-    Vec_PtrForEachEntry( p->vNodes, pObj, i )
+    // construct choice nodes
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
     {
-        Abc_Obj_t * pTemp;
+        // skip the node without choices
         if ( pObj->pData == NULL )
             continue;
-
-        pObjAbcThis = (Abc_Obj_t *)pObj->pNext;
-        pObjAbcRepr = (Abc_Obj_t *)((Hop_Obj_t *)pObj->pData)->pNext;
-        assert( !Abc_ObjIsComplement(pObjAbcThis) );
-        assert( !Abc_ObjIsComplement(pObjAbcRepr) );
-
-        // skip the case when the class is constant 1
-        if ( pObjAbcRepr == Abc_AigConst1(pNtkAig) )
-            continue;
-
-        // skip the case when pObjAbcThis is part of the class already
-        for ( pTemp = pObjAbcRepr; pTemp; pTemp = pTemp->pData )
-            if ( pTemp == pObjAbcThis )
-                break;
-        if ( pTemp )
-            continue;
-
-//        assert( Abc_ObjFanoutNum(pObjAbcThis) == 0 );
-        if ( Abc_ObjFanoutNum(pObjAbcThis) > 0 )
+        // skip the representative of the class
+        if ( pObj->pData == pObj )
             continue;
-//        assert( pObjAbcThis->pData == NULL );
-        if ( pObjAbcThis->pData )
+        // do not create choices for constant 1 and PIs
+        if ( !Hop_ObjIsNode(pObj->pData) )
             continue;
-
+        // get the corresponding new nodes
+        pObjAbcThis = (Abc_Obj_t *)pObj->pNext;
+        pObjAbcRepr = (Abc_Obj_t *)((Hop_Obj_t *)pObj->pData)->pNext;
+        // the new node cannot be already in the class
+        assert( pObjAbcThis->pData == NULL );
+        // the new node cannot have fanouts
+        assert( Abc_ObjFanoutNum(pObjAbcThis) == 0 );
+        // these should be different nodes
+        assert( pObjAbcRepr != pObjAbcThis );
         // do not create choices if there is a path from pObjAbcThis to pObjAbcRepr
         if ( !Abc_NtkHaigCheckTfi( pNtkAig, pObjAbcRepr, pObjAbcThis ) )
         {
@@ -454,6 +534,110 @@ Abc_Ntk_t * Abc_NtkHaigRecreateAig( Abc_Ntk_t * pNtk, Hop_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Resets representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkHaigResetReprsOld( Hop_Man_t * pMan )
+{
+    Vec_Ptr_t * vMembers, * vClasses;
+
+    // collect members of the classes and make them point to reprs
+    vMembers = Abc_NtkHaigCollectMembers( pMan );
+    printf( "Collected %6d class members.\n", Vec_PtrSize(vMembers) );
+
+    // create classes
+    vClasses = Abc_NtkHaigCreateClasses( vMembers );
+    printf( "Collected %6d classes. (Ave = %5.2f)\n", Vec_PtrSize(vClasses), 
+        (float)(Vec_PtrSize(vMembers))/Vec_PtrSize(vClasses) );
+
+    Vec_PtrFree( vMembers );
+    Vec_PtrFree( vClasses );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resets representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkHaigResetReprs( Hop_Man_t * p )
+{
+    Hop_Obj_t * pObj, * pRepr;
+    int i, nClasses, nMembers, nFanouts, nNormals;
+    // clear self-classes
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        // fix the strange situation of double-loop
+        pRepr = pObj->pData;
+        if ( pRepr && pRepr->pData == pObj )
+            pRepr->pData = pRepr;
+        // remove self-loops
+        if ( pObj->pData == pObj )
+            pObj->pData = NULL;
+    }
+    // set representatives
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        if ( pObj->pData == NULL )
+            continue;
+        // get representative of the node
+        pRepr = Hop_ObjRepr( pObj );
+        pRepr->pData = pRepr;
+        // set the representative
+        pObj->pData = pRepr;
+    }
+    // make each class point to the smallest topological order
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        if ( pObj->pData == NULL )
+            continue;
+        pRepr = Hop_ObjRepr( pObj );
+        if ( pRepr->Id > pObj->Id )
+        {
+            pRepr->pData = pObj;
+            pObj->pData = pObj;
+        }
+        else
+            pObj->pData = pRepr;
+    }
+    // count classes, members, and fanouts - and verify
+    nMembers = nClasses = nFanouts = nNormals = 0;
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        if ( pObj->pData == NULL )
+            continue;
+        // count members
+        nMembers++;
+        // count the classes and fanouts
+        if ( pObj->pData == pObj )
+            nClasses++;
+        else if ( Hop_ObjRefs(pObj) > 0 )
+            nFanouts++;
+        else
+            nNormals++;
+        // compare representatives
+        pRepr = Hop_ObjRepr( pObj );
+        assert( pObj->pData == pRepr );
+        assert( pRepr->Id <= pObj->Id );
+    }
+//    printf( "Nodes = %7d.  Member = %7d.  Classes = %6d.  Fanouts = %6d.  Normals = %6d.\n", 
+//        Hop_ManNodeNum(p), nMembers, nClasses, nFanouts, nNormals );
+    return nFanouts;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Stops history AIG.]
 
   Description []
@@ -465,8 +649,10 @@ Abc_Ntk_t * Abc_NtkHaigRecreateAig( Abc_Ntk_t * pNtk, Hop_Man_t * p )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk )
 {
+    Hop_Man_t * pMan, * pManTemp;
     Abc_Ntk_t * pNtkAig;
-    Vec_Ptr_t * vMembers, * vClasses;
+    Abc_Obj_t * pObj;
+    int i;
 
     // check if HAIG is available
     assert( Abc_NtkIsStrash(pNtk) );
@@ -476,26 +662,39 @@ Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk )
         return NULL;
     }
     // convert HOP package into AIG with choices
-
     // print HAIG stats
-//    Hop_ManPrintStats( pNtk->pHaig ); // USES DATA!!!
+//    Hop_ManPrintStats( pMan ); // USES DATA!!!
 
-    // collect members of the classes and make them point to reprs
-    vMembers = Abc_NtkHaigCollectMembers( pNtk->pHaig );
-    printf( "Collected %6d class members.\n", Vec_PtrSize(vMembers) );
+    // add the POs
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Hop_ObjCreatePo( pNtk->pHaig, Abc_ObjChild0Equiv(pObj) );
 
-    // create classes
-    vClasses = Abc_NtkHaigCreateClasses( vMembers );
-    printf( "Collected %6d classes. (Ave = %5.2f)\n", Vec_PtrSize(vClasses), 
-        (float)(Vec_PtrSize(vMembers))/Vec_PtrSize(vClasses) );
-    Vec_PtrFree( vMembers );
-    Vec_PtrFree( vClasses );
+    // clean the old network
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->pEquiv = NULL;
+    pMan = pNtk->pHaig; 
+    pNtk->pHaig = 0;
 
+    // iteratively reconstruct the HOP manager to create choice nodes
+    while ( Abc_NtkHaigResetReprs( pMan ) )
+    {
+        pMan = Abc_NtkHaigReconstruct( pManTemp = pMan );
+        Hop_ManStop( pManTemp );
+    }
+/*
+    pMan = Abc_NtkHaigReconstruct( pManTemp = pMan );
+    Hop_ManStop( pManTemp );
+    Abc_NtkHaigResetReprs( pMan );
+
+    pMan = Abc_NtkHaigReconstruct( pManTemp = pMan );
+    Hop_ManStop( pManTemp );
+    Abc_NtkHaigResetReprs( pMan );
+*/
     // traverse in the topological order and create new AIG
-    pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pNtk->pHaig );
+    pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pMan );
+    Hop_ManStop( pMan );
 
     // free HAIG
-    Abc_NtkHaigStop( pNtk );
     return pNtkAig;
 }
 
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 00861e1b..46f7dd13 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -150,6 +150,7 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
         // set up the choice node
         if ( Abc_AigNodeIsChoice( pNode ) )
         {
+            pIfMan->nChoices++;
             for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
                 If_ObjSetChoice( (If_Obj_t *)pPrev->pCopy, (If_Obj_t *)pFanin->pCopy );
             If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pCopy );
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 17db7ed9..6423d10c 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -38,6 +38,8 @@ static DdManager * s_pDd      = NULL;
 static Vec_Int_t * s_vMemory  = NULL;
 static Vec_Int_t * s_vMemory2 = NULL;
 
+static int nDsdCounter = 0;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -62,6 +64,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Performing renoding with choices.\n" );
 
+    nDsdCounter = 0;
+
     // set defaults
     memset( pPars, 0, sizeof(If_Par_t) );
     // user-controlable paramters
@@ -136,6 +140,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
         s_vMemory2 = NULL;
     }
 
+    printf( "Decomposed %d functions.\n", nDsdCounter );
+
     return pNtkNew;
 }
 
@@ -154,6 +160,14 @@ int Abc_NtkRenodeEvalAig( If_Cut_t * pCut )
 {
     Kit_Graph_t * pGraph;
     int i, nNodes;
+
+extern void Kit_DsdTest( unsigned * pTruth, int nVars );
+if ( If_CutLeaveNum(pCut) == 8 )
+{
+    nDsdCounter++;
+    Kit_DsdTest( If_CutTruth(pCut), If_CutLeaveNum(pCut) );
+}
+
     pGraph = Kit_TruthToGraph( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory );
     if ( pGraph == NULL )
     {
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index b7a7d4b9..1054e071 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -256,13 +256,25 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
     nOutputs = 0;
     Abc_NtkForEachPo( pMiter, pObj, i )
     {
-        // get the cone of this output
-        pMiterPart = Abc_NtkCreateCone( pMiter, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 0 );
-        if ( Abc_ObjFaninC0(pObj) )
-            Abc_ObjXorFaninC( Abc_NtkPo(pMiterPart,0), 0 );
-        // solve the cone
-    //    RetValue = Abc_NtkMiterProve( &pMiterPart, pParams );
-        RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
+        if ( Abc_ObjFanin0(pObj) == Abc_AigConst1(pMiter) )
+        {
+            if ( Abc_ObjFaninC0(pObj) ) // complemented -> const 0
+                RetValue = 1;
+            else
+                RetValue = 0;
+            pMiterPart = NULL;
+        }
+        else
+        {
+            // get the cone of this output
+            pMiterPart = Abc_NtkCreateCone( pMiter, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 0 );
+            if ( Abc_ObjFaninC0(pObj) )
+                Abc_ObjXorFaninC( Abc_NtkPo(pMiterPart,0), 0 );
+            // solve the cone
+        //    RetValue = Abc_NtkMiterProve( &pMiterPart, pParams );
+            RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
+        }
+
         if ( RetValue == -1 )
         {
             printf( "Networks are undecided (resource limits is reached).\r" );
@@ -286,7 +298,8 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
         }
 //        if ( pMiter->pModel )
 //            Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
-        Abc_NtkDelete( pMiterPart );
+        if ( pMiterPart )
+            Abc_NtkDelete( pMiterPart );
     }
 
     Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
diff --git a/src/base/io/io.c b/src/base/io/io.c
index cc907eb2..a7801f71 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -31,6 +31,7 @@ static int IoCommandReadBaf     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadBlif    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadBlifMv  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadBench   ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadDsd     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEdif    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEqn     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadPla     ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -82,6 +83,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "read_blif",     IoCommandReadBlif,     1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv",  IoCommandReadBlif,     1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_bench",    IoCommandReadBench,    1 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_dsd",      IoCommandReadDsd,      1 );
 //    Cmd_CommandAdd( pAbc, "I/O", "read_edif",     IoCommandReadEdif,     1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_eqn",      IoCommandReadEqn,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_pla",      IoCommandReadPla,      1 );
@@ -483,6 +485,67 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandReadDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk;
+    char * pString;
+    int fCheck;
+    int c;
+    extern Abc_Ntk_t * Io_ReadDsd( char * pFormula );
+
+    fCheck = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'c':
+                fCheck ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+        goto usage;
+    // get the input file name
+    pString = argv[globalUtilOptind];
+    // read the file using the corresponding file reader
+    pNtk = Io_ReadDsd( pString );
+    if ( pNtk == NULL )
+        return 1;
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_dsd [-h] <formula>\n" );
+    fprintf( pAbc->Err, "\t          parses a formula representing DSD of a function\n" );
+    fprintf( pAbc->Err, "\t-h      : prints the command summary\n" );
+    fprintf( pAbc->Err, "\tformula : the formula representing disjoint-support decomposition (DSD)\n" );
+    fprintf( pAbc->Err, "\t          Example of a formula: !(a*(b+CA(c,!d,e*f))*79B3(g,h,i,k))\n" );
+    fprintf( pAbc->Err, "\t          where \'!\' is an INV, \'*\' is an AND, \'+\' is an XOR, \n" );
+    fprintf( pAbc->Err, "\t          CA and 79B3 are hexadecimal representations of truth tables\n" );
+    fprintf( pAbc->Err, "\t          (in this case CA=11001010 is truth table of MUX(Ctrl,Data1,Data0))\n" );
+    fprintf( pAbc->Err, "\t          The lower chars (a,b,c,etc) are reserved for elementary variables.\n" );
+    fprintf( pAbc->Err, "\t          The upper chars (A,B,C,etc) are reserved for hexadecimal digits.\n" );
+    fprintf( pAbc->Err, "\t          No spaces are allowed in the formula.\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk;
diff --git a/src/base/io/ioReadDsd.c b/src/base/io/ioReadDsd.c
new file mode 100644
index 00000000..1ab726e5
--- /dev/null
+++ b/src/base/io/ioReadDsd.c
@@ -0,0 +1,308 @@
+/**CFile****************************************************************
+
+  FileName    [ioReadDsd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedure to read network from file.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioReadDsd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the end of the part.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Io_ReadDsdFindEnd( char * pCur )
+{
+    char * pEnd;
+    int nParts = 0;
+    assert( *pCur == '(' );
+    for ( pEnd = pCur; *pEnd; pEnd++ )
+    {
+        if ( *pEnd == '(' )
+            nParts++;
+        else if ( *pEnd == ')' )
+            nParts--;
+        if ( nParts == 0 )
+            return pEnd;
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Splits the formula into parts.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_ReadDsdStrSplit( char * pCur, char * pParts[], int * pTypeXor )
+{
+    int fAnd = 0, fXor = 0, fPri = 0, nParts = 0;
+    assert( *pCur );
+    // process the parts
+    while ( 1 )
+    {
+        // save the current part
+        pParts[nParts++] = pCur;
+        // skip the complement
+        if ( *pCur == '!' )
+            pCur++;
+        // skip var
+        if ( *pCur >= 'a' && *pCur <= 'z' )
+            pCur++;
+        else
+        {
+            // skip hex truth table
+            while ( (*pCur >= '0' && *pCur <= '9') || (*pCur >= 'A' && *pCur <= 'F') )
+                pCur++;
+            // process parantheses
+            if ( *pCur != '(' )
+            {
+                printf( "Cannot find the opening paranthesis.\n" );
+                break;
+            }
+            // find the corresponding closing paranthesis
+            pCur = Io_ReadDsdFindEnd( pCur );
+            if ( pCur == NULL )
+            {
+                printf( "Cannot find the closing paranthesis.\n" );
+                break;
+            }
+            pCur++;
+        }
+        // check the end
+        if ( *pCur == 0 )
+            break;
+        // check symbol
+        if ( *pCur != '*' && *pCur != '+' && *pCur != ',' )
+        {
+            printf( "Wrong separating symbol.\n" );
+            break;
+        }
+        // remember the symbol
+        fAnd |= (*pCur == '*');
+        fXor |= (*pCur == '+');
+        fPri |= (*pCur == ',');
+        *pCur++ = 0;
+    }
+    // check separating symbols
+    if ( fAnd + fXor + fPri > 1 )
+    {
+        printf( "Different types of separating symbol ennPartsed.\n" );
+        return 0;
+    }
+    *pTypeXor = fXor;
+    return nParts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively parses the formula.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Io_ReadDsd_rec( Abc_Ntk_t * pNtk, char * pCur, char * pSop )
+{
+    Abc_Obj_t * pObj, * pFanin;
+    char * pEnd, * pParts[32];
+    int i, nParts, TypeExor;
+
+    // consider complemented formula
+    if ( *pCur == '!' )
+    {
+        pObj = Io_ReadDsd_rec( pNtk, pCur + 1, NULL );
+        return Abc_NtkCreateNodeInv( pNtk, pObj );
+    }
+    if ( *pCur == '(' )
+    {
+        assert( pCur[strlen(pCur)-1] == ')' );
+        pCur[strlen(pCur)-1] = 0;
+        nParts = Io_ReadDsdStrSplit( pCur+1, pParts, &TypeExor );
+        if ( nParts == 0 )
+        {
+            Abc_NtkDelete( pNtk );
+            return NULL;
+        }
+        pObj = Abc_NtkCreateNode( pNtk );
+        if ( pSop )
+        {
+//            for ( i = nParts - 1; i >= 0; i-- )
+            for ( i = 0; i < nParts; i++ )
+            {
+                pFanin = Io_ReadDsd_rec( pNtk, pParts[i], NULL );
+                if ( pFanin == NULL )
+                    return NULL;
+                Abc_ObjAddFanin( pObj, pFanin );
+            }
+        }
+        else
+        {
+            for ( i = 0; i < nParts; i++ )
+            {
+                pFanin = Io_ReadDsd_rec( pNtk, pParts[i], NULL );
+                if ( pFanin == NULL )
+                    return NULL;
+                Abc_ObjAddFanin( pObj, pFanin );
+            }
+        }
+        if ( pSop )
+            pObj->pData = Abc_SopRegister( pNtk->pManFunc, pSop );
+        else if ( TypeExor )
+            pObj->pData = Abc_SopCreateXorSpecial( pNtk->pManFunc, nParts );
+        else
+            pObj->pData = Abc_SopCreateAnd( pNtk->pManFunc, nParts, NULL );
+        return pObj;
+    }
+    if ( *pCur >= 'a' && *pCur <= 'z' )
+    {
+        assert( *(pCur+1) == 0 );
+        return Abc_NtkPi( pNtk, *pCur - 'a' );
+    }
+
+    // skip hex truth table
+    pEnd = pCur;
+    while ( (*pEnd >= '0' && *pEnd <= '9') || (*pEnd >= 'A' && *pEnd <= 'F') )
+        pEnd++;
+    if ( *pEnd != '(' )
+    {
+        printf( "Cannot find the end of hexidecimal truth table.\n" );
+        return NULL;
+    }
+
+    // parse the truth table
+    *pEnd = 0;
+    pSop = Abc_SopFromTruthHex( pCur );
+    *pEnd = '(';
+    pObj = Io_ReadDsd_rec( pNtk, pEnd, pSop );
+    free( pSop );
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the DSD network of the formula.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadDsd( char * pForm )
+{
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObj, * pTop;
+    Vec_Ptr_t * vNames;
+    char * pCur, * pFormCopy;
+    int i, nInputs;
+
+    // count the number of elementary variables
+    nInputs = 0;
+    for ( pCur = pForm; *pCur; pCur++ )
+        if ( *pCur >= 'a' && *pCur <= 'z' )
+            nInputs = ABC_MAX( nInputs, *pCur - 'a' );
+    nInputs++;
+
+    // create the network
+    pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
+    pNtk->pName = Extra_UtilStrsav( "dsd" );
+
+    // create PIs
+    vNames = Abc_NodeGetFakeNames( nInputs );
+    for ( i = 0; i < nInputs; i++ )
+        Abc_ObjAssignName( Abc_NtkCreatePi(pNtk), Vec_PtrEntry(vNames, i), NULL );
+    Abc_NodeFreeNames( vNames );
+
+    // transform the formula by inserting parantheses
+    // this transforms strings like PRIME(a,b,cd) into (PRIME((a),(b),(cd)))
+    pCur = pFormCopy = ALLOC( char, 3 * strlen(pForm) + 10 );
+    *pCur++ = '(';
+    for ( ; *pForm; pForm++ )
+        if ( *pForm == '(' )
+        {
+            *pCur++ = '(';
+            *pCur++ = '(';
+        }
+        else if ( *pForm == ')' )
+        {
+            *pCur++ = ')';
+            *pCur++ = ')';
+        }
+        else if ( *pForm == ',' )
+        {
+            *pCur++ = ')';
+            *pCur++ = ',';
+            *pCur++ = '(';
+        }
+        else
+            *pCur++ = *pForm;
+    *pCur++ = ')';
+    *pCur = 0;
+
+    // parse the formula
+    pObj = Io_ReadDsd_rec( pNtk, pFormCopy, NULL );
+    free( pFormCopy );
+    if ( pObj == NULL )
+        return NULL;
+
+    // create output
+    pTop = Abc_NtkCreatePo(pNtk);
+    Abc_ObjAssignName( pTop, "F", NULL );
+    Abc_ObjAddFanin( pTop, pObj );
+
+    // create the only PO
+    if ( !Abc_NtkCheck( pNtk ) )
+    {
+        fprintf( stdout, "Io_ReadDsd(): Network check has failed.\n" );
+        Abc_NtkDelete( pNtk );
+        return NULL;
+    }
+    return pNtk;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+
diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c
index e63489f4..b8b3b83b 100644
--- a/src/base/io/ioWriteBench.c
+++ b/src/base/io/ioWriteBench.c
@@ -258,7 +258,7 @@ int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth
     nFanins = Abc_ObjFaninNum(pNode);
     assert( nFanins <= 8 );
     // compute the truth table
-    pTruth = Abc_ConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth );
+    pTruth = Abc_ConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth, 0 );
     if ( Hop_IsComplement(pNode->pData) )
         Extra_TruthNot( pTruth, pTruth, nFanins );
     // consider simple cases
diff --git a/src/base/io/io_.c b/src/base/io/io_.c
index 7721545a..62dd60e5 100644
--- a/src/base/io/io_.c
+++ b/src/base/io/io_.c
@@ -28,6 +28,18 @@
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/module.make b/src/base/io/module.make
index 4b6f762c..bb35a7fc 100644
--- a/src/base/io/module.make
+++ b/src/base/io/module.make
@@ -5,6 +5,7 @@ SRC +=  src/base/io/io.c \
     src/base/io/ioReadBlif.c \
     src/base/io/ioReadBlifAig.c \
     src/base/io/ioReadBlifMv.c \
+    src/base/io/ioReadDsd.c \
     src/base/io/ioReadEdif.c \
     src/base/io/ioReadEqn.c \
     src/base/io/ioReadPla.c \
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 7e22707f..759a9801 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -139,6 +139,7 @@ struct If_Man_t_
     unsigned *         puTemp[4];     // used for the truth table computation
     int                SortMode;      // one of the three sorting modes
     int                fNextRound;    // set to 1 after the first round
+    int                nChoices;      // the number of choice nodes
     // sequential mapping
     Vec_Ptr_t *        vLatchOrder;   // topological ordering of latches
     Vec_Int_t *        vLags;         // sequentail lags of all nodes
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 20b2657f..77f4930a 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -480,7 +480,8 @@ void If_ManSetupSetAll( If_Man_t * p )
 
     if ( p->pPars->fVerbose )
     {
-        printf( "Total memory = %7.2f Mb. Peak cut memory = %7.2f Mb.  \n", 
+        printf( "Node = %7d.  Ch = %5d.  Total mem = %7.2f Mb. Peak cut mem = %7.2f Mb.\n", 
+            If_ManAndNum(p), p->nChoices,
             1.0 * (p->nObjBytes + 2*sizeof(void *)) * If_ManObjNum(p) / (1<<20), 
             1.0 * p->nSetBytes * nCrossCut / (1<<20) );
     }
diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h
index ed2745e3..5d37a9e9 100644
--- a/src/opt/kit/kit.h
+++ b/src/opt/kit/kit.h
@@ -153,13 +153,22 @@ static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t
 
 static inline int          Kit_Float2Int( float Val )     { return *((int *)&Val);               }
 static inline float        Kit_Int2Float( int Num )       { return *((float *)&Num);             }
-static inline int          Kit_BitWordNum( int nBits )    { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0);  }
-static inline int          Kit_TruthWordNum( int nVars )  { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
+static inline int          Kit_BitWordNum( int nBits )    { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); }
+static inline int          Kit_TruthWordNum( int nVars )  { return nVars <= 5 ? 1 : (1 << (nVars - 5));                             }
+static inline unsigned     Kit_BitMask( int nBits )       { assert( nBits <= 32 ); return ~((~(unsigned)0) << nBits);               }
 
 static inline void         Kit_TruthSetBit( unsigned * p, int Bit )   { p[Bit>>5] |= (1<<(Bit & 31));               }
 static inline void         Kit_TruthXorBit( unsigned * p, int Bit )   { p[Bit>>5] ^= (1<<(Bit & 31));               }
 static inline int          Kit_TruthHasBit( unsigned * p, int Bit )   { return (p[Bit>>5] & (1<<(Bit & 31))) > 0;   }
 
+static inline int Kit_WordFindFirstBit( unsigned uWord )
+{
+    int i;
+    for ( i = 0; i < 32; i++ )
+        if ( uWord & (1 << i) )
+            return i;
+    return -1;
+}
 static inline int Kit_WordCountOnes( unsigned uWord )
 {
     uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
@@ -183,6 +192,14 @@ static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars
             return 0;
     return 1;
 }
+static inline int Kit_TruthIsOpposite( unsigned * pIn0, unsigned * pIn1, int nVars )
+{
+    int w;
+    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+        if ( pIn0[w] != ~pIn1[w] )
+            return 0;
+    return 1;
+}
 static inline int Kit_TruthIsConst0( unsigned * pIn, int nVars )
 {
     int w;
@@ -332,9 +349,11 @@ extern void            Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nV
 extern void            Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
 extern int             Kit_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar );
 extern int             Kit_TruthSupportSize( unsigned * pTruth, int nVars );
-extern int             Kit_TruthSupport( unsigned * pTruth, int nVars );
+extern unsigned        Kit_TruthSupport( unsigned * pTruth, int nVars );
 extern void            Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar );
 extern void            Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
+extern void            Kit_TruthCofactor0New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
+extern void            Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
 extern void            Kit_TruthExist( unsigned * pTruth, int nVars, int iVar );
 extern void            Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
 extern void            Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
diff --git a/src/opt/kit/kitDsd.c b/src/opt/kit/kitDsd.c
new file mode 100644
index 00000000..0068a29a
--- /dev/null
+++ b/src/opt/kit/kitDsd.c
@@ -0,0 +1,689 @@
+/**CFile****************************************************************
+
+  FileName    [kitDsd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Computation kit.]
+
+  Synopsis    [Performs disjoint-support decomposition based on truth tables.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Dec 6, 2006.]
+
+  Revision    [$Id: kitDsd.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Dsd_Ntk_t_ Dsd_Ntk_t;
+typedef struct Dsd_Obj_t_ Dsd_Obj_t;
+
+// network 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_MUX,        // 5: multiplexer
+    KIT_DSD_PRIME       // 6: arbitrary function of 3+ variables
+} Kit_Dsd_t;
+
+struct Dsd_Obj_t_
+{ 
+    unsigned       uSupp;              // the support of this node
+    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      : 16;   // offset to the truth table
+    unsigned       nFans       :  6;   // the number of fanins of this node
+    unsigned char  pFans[0];           // the fanin literals
+};
+
+struct Dsd_Ntk_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
+};
+
+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_NtkRoot( Dsd_Ntk_t * pNtk )   { return pNtk->pNodes[(pNtk->Root >> 1) - pNtk->nVars]; }
+
+#define Dsd_NtkForEachObj( pNtk, pObj, i )                                       \
+    for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
+#define Dsd_ObjForEachFanin( pNtk, pObj, pFanin, iVar, i )                       \
+    for ( i = 0; (i < (pObj)->nFans) && (((pFanin) = ((pObj)->pFans[i] < 2*pNtk->nVars)? NULL: (pNtk)->pNodes[((pObj)->pFans[i]>>1) - pNtk->nVars]), 1) && ((iVar) = (pObj)->pFans[i], 1); i++ )
+
+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 );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the DSD node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dsd_Obj_t * Dsd_ObjAlloc( Dsd_Ntk_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 );
+    memset( pObj, 0, nSize );
+    pObj->Type = Type;
+    pObj->Id = pNtk->nVars + pNtk->nNodes;
+    pObj->nFans = nFans;
+    pObj->Offset = Dsd_ObjOffset( nFans );
+    // add the object
+    assert( pNtk->nNodes < pNtk->nNodesAlloc );
+    pNtk->pNodes[pNtk->nNodes++] = pObj;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the DSD node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dsd_ObjFree( Dsd_Ntk_t * p, Dsd_Obj_t * pObj )
+{
+    free( pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the DSD network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dsd_Ntk_t * Kit_DsdNtkAlloc( unsigned * pTruth, int nVars )
+{
+    Dsd_Ntk_t * pNtk;
+    int nSize = sizeof(Dsd_Ntk_t) + sizeof(void *) * nVars;
+    // allocate the network
+    pNtk = (Dsd_Ntk_t *)ALLOC( char, nSize );
+    memset( pNtk, 0, nSize );
+    pNtk->nVars = nVars;
+    pNtk->nNodesAlloc = nVars;
+    pNtk->pMem = ALLOC( unsigned, 6 * Kit_TruthWordNum(nVars) );
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocate the DSD network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdNtkFree( Dsd_Ntk_t * pNtk )
+{
+    Dsd_Obj_t * pObj;
+    unsigned i;
+    Dsd_NtkForEachObj( pNtk, pObj, i )
+        free( pObj );
+    free( pNtk->pMem );
+    free( pNtk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the hex unsigned into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdPrintHex( FILE * pFile, unsigned * pTruth, int nFans )
+{
+    int nDigits, Digit, k;
+    nDigits = (1 << nFans) / 4;
+    for ( k = nDigits - 1; k >= 0; k-- )
+    {
+        Digit = ((pTruth[k/8] >> ((k%8) * 4)) & 15);
+        if ( Digit < 10 )
+            fprintf( pFile, "%d", Digit );
+        else
+            fprintf( pFile, "%c", 'A' + Digit-10 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively print the DSD formula.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdPrint_rec( FILE * pFile, Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj )
+{
+    Dsd_Obj_t * pFanin;
+    unsigned iVar, i;
+    char Symbol;
+
+    if ( pObj->Type == KIT_DSD_CONST1 )
+    {
+        assert( pObj->nFans == 0 );
+        fprintf( pFile, "Const1" );
+        return;
+    }
+
+    if ( pObj->Type == KIT_DSD_VAR )
+        assert( pObj->nFans == 1 );
+
+    if ( pObj->Type == KIT_DSD_AND )
+        Symbol = '*';
+    else if ( pObj->Type == KIT_DSD_XOR )
+        Symbol = '+';
+    else 
+        Symbol = ',';
+
+    if ( pObj->Type == KIT_DSD_MUX )
+        fprintf( pFile, "CA" );
+    else if ( pObj->Type == KIT_DSD_PRIME )
+        Kit_DsdPrintHex( stdout, Dsd_ObjTruth(pObj), pObj->nFans );
+
+    fprintf( pFile, "(" );
+    Dsd_ObjForEachFanin( pNtk, pObj, pFanin, iVar, i )
+    {
+        if ( iVar & 1 ) 
+            fprintf( pFile, "!" );
+        if ( pFanin )
+            Kit_DsdPrint_rec( pFile, pNtk, pFanin );
+        else
+            fprintf( pFile, "%c", 'a' + (pNtk->nVars - 1 - (iVar >> 1)) );
+        if ( i < pObj->nFans - 1 )
+            fprintf( pFile, "%c", Symbol );
+    }
+    fprintf( pFile, ")" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Print the DSD formula.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdPrint( FILE * pFile, Dsd_Ntk_t * pNtk )
+{
+    fprintf( pFile, "F = " );
+    if ( pNtk->Root & 1 )
+        fprintf( pFile, "!" );
+    Kit_DsdPrint_rec( pFile, pNtk, Dsd_NtkRoot(pNtk) );
+    fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if there is a component with more than 3 inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdFindLargeBox( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj )
+{
+    Dsd_Obj_t * pFanin;
+    unsigned iVar, i, RetValue;
+    if ( pObj->nFans > 3 )
+        return 1;
+    RetValue = 0;
+    Dsd_ObjForEachFanin( pNtk, pObj, pFanin, iVar, i )
+        if ( pFanin )
+            RetValue |= Kit_DsdFindLargeBox( pNtk, pFanin );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * pPar )
+{
+    Dsd_Obj_t * pRes, * pRes0, * pRes1;
+    int nWords = Kit_TruthWordNum(pObj->nFans);
+    unsigned * pTruth = Dsd_ObjTruth(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 nFans0, nFans1, iVar0, iVar1, nPairs;
+    int fEquals[2][2], fOppos, fPairs[4][4];
+    unsigned j, k, nFansNew, uSupp0, uSupp1;
+    int i;
+
+    assert( pObj->nFans > 0 );
+    assert( pObj->Type == KIT_DSD_PRIME );
+    assert( pObj->uSupp == (uSupp0 = (unsigned)Kit_TruthSupport(pTruth, pObj->nFans)) );
+
+    // compress the truth table
+    if ( pObj->uSupp != Kit_BitMask(pObj->nFans) )
+    {
+        nFansNew = Kit_WordCountOnes(pObj->uSupp);
+        Kit_TruthShrink( pNtk->pMem, pTruth, nFansNew, pObj->nFans, pObj->uSupp );
+        Kit_TruthCopy( pTruth, pNtk->pMem, pObj->nFans );
+        for ( j = k = 0; j < pObj->nFans; j++ )
+            if ( pObj->uSupp & (1 << j) )
+                pObj->pFans[k++] = pObj->pFans[j];
+        assert( k == nFansNew );
+        pObj->nFans = k;
+        pObj->uSupp = Kit_BitMask(pObj->nFans);
+    }
+
+    // consider the single variable case
+    if ( pObj->nFans == 1 )
+    {
+        pObj->Type = KIT_DSD_NONE;
+        if ( pTruth[0] == 0x55555555 )
+            pObj->pFans[0] ^= 1;
+        else
+            assert( pTruth[0] == 0xAAAAAAAA );
+        // update the parent pointer
+//        assert( !((*pPar) & 1) );
+        *pPar = pObj->pFans[0] ^ ((*pPar) & 1);
+        return;
+    }
+
+    // decompose the output
+    if ( !pObj->fMark )
+    for ( i = pObj->nFans - 1; i >= 0; i-- )
+    {
+        // get the two-variable cofactors
+        Kit_TruthCofactor0New( pCofs2[0], pTruth, pObj->nFans, i );
+        Kit_TruthCofactor1New( pCofs2[1], pTruth, pObj->nFans, i );
+//        assert( !Kit_TruthVarInSupport( pCofs2[0], pObj->nFans, i) );
+//        assert( !Kit_TruthVarInSupport( pCofs2[1], pObj->nFans, i) );
+        // get the constant cofs
+        fEquals[0][0] = Kit_TruthIsConst0( pCofs2[0], pObj->nFans );
+        fEquals[0][1] = Kit_TruthIsConst0( pCofs2[1], pObj->nFans );
+        fEquals[1][0] = Kit_TruthIsConst1( pCofs2[0], pObj->nFans );
+        fEquals[1][1] = Kit_TruthIsConst1( pCofs2[1], pObj->nFans );
+        fOppos        = Kit_TruthIsOpposite( pCofs2[0], pCofs2[1], pObj->nFans );
+        assert( !Kit_TruthIsEqual(pCofs2[0], pCofs2[1], pObj->nFans) );
+        if ( fEquals[0][0] + fEquals[0][1] + fEquals[1][0] + fEquals[1][1] + fOppos == 0 )
+        {
+            // check the MUX decomposition
+            uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
+            uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
+            assert( pObj->uSupp == (uSupp0 | uSupp1 | (1<<i)) );
+            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 );
+            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 ); 
+            pRes0->uSupp = uSupp0;
+            pRes1->uSupp = uSupp1;
+            // update the current one
+            pObj->Type = KIT_DSD_MUX;
+            pObj->nFans = 3;
+            pObj->pFans[0] = pObj->pFans[i];
+            pObj->pFans[1] = 2*pRes1->Id;
+            pObj->pFans[2] = 2*pRes0->Id;
+            // call recursively
+            Kit_DsdDecompose_rec( pNtk, pRes0, pObj->pFans + 2 );
+            Kit_DsdDecompose_rec( pNtk, pRes1, pObj->pFans + 1 );
+            return;
+        }
+//Extra_PrintBinary( stdout, pTruth, 1 << pObj->nFans ); printf( "\n" );
+
+        // create the new node
+        pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_AND, 2 );
+        pRes->nFans = 2;
+        pRes->pFans[0] = pObj->pFans[i];  pObj->pFans[i] = 127;  pObj->uSupp &= ~(1 << i);
+        pRes->pFans[1] = 2*pObj->Id;
+        // update the parent pointer
+        *pPar = 2 * pRes->Id;
+        // consider different decompositions
+        if ( fEquals[0][0] )
+        {
+            Kit_TruthCopy( pTruth, pCofs2[1], pObj->nFans );
+        }
+        else if ( fEquals[0][1] )
+        {
+            pRes->pFans[0] ^= 1;
+            Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
+        }
+        else if ( fEquals[1][0] )
+        {
+            *pPar ^= 1;
+            pRes->pFans[1] ^= 1;
+            Kit_TruthCopy( pTruth, pCofs2[1], pObj->nFans );
+        }
+        else if ( fEquals[1][1] )
+        {
+            *pPar ^= 1;
+            pRes->pFans[0] ^= 1;  
+            pRes->pFans[1] ^= 1;
+            Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
+        }
+        else if ( fOppos )
+        {
+            pRes->Type = KIT_DSD_XOR;
+            Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
+        }
+        else
+            assert( 0 );
+        // decompose the remainder
+        assert( Dsd_ObjTruth(pObj) == pTruth );
+        Kit_DsdDecompose_rec( pNtk, pObj, pRes->pFans + 1 );
+        return;
+    }
+    pObj->fMark = 1;
+
+    // decompose the input
+    for ( i = pObj->nFans - 1; i >= 0; i-- )
+    {
+        assert( Kit_TruthVarInSupport( pTruth, pObj->nFans, i ) );
+        // get the single variale cofactors
+        Kit_TruthCofactor0New( pCofs2[0], pTruth, pObj->nFans, i );
+        Kit_TruthCofactor1New( pCofs2[1], pTruth, pObj->nFans, i );
+        // check the existence of MUX decomposition
+        uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
+        uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
+        // if one of the cofs is a constant, it is time to check it again
+        if ( uSupp0 == 0 || uSupp1 == 0 )
+        {
+            pObj->fMark = 0;
+            Kit_DsdDecompose_rec( pNtk, pObj, pPar );
+            return;
+        }
+        assert( uSupp0 && uSupp1 );
+        // get the number of unique variables
+        nFans0 = Kit_WordCountOnes( uSupp0 & ~uSupp1 );
+        nFans1 = Kit_WordCountOnes( uSupp1 & ~uSupp0 );
+        if ( nFans0 == 1 && nFans1 == 1 )
+        {
+            // get the cofactors w.r.t. the unique variables
+            iVar0 = Kit_WordFindFirstBit( uSupp0 & ~uSupp1 );
+            iVar1 = Kit_WordFindFirstBit( uSupp1 & ~uSupp0 );
+            // get four cofactors                                        
+            Kit_TruthCofactor0New( pCofs4[0][0], pCofs2[0], pObj->nFans, iVar0 );
+            Kit_TruthCofactor1New( pCofs4[0][1], pCofs2[0], pObj->nFans, iVar0 );
+            Kit_TruthCofactor0New( pCofs4[1][0], pCofs2[1], pObj->nFans, iVar1 );
+            Kit_TruthCofactor1New( pCofs4[1][1], pCofs2[1], pObj->nFans, iVar1 );
+            // check existence conditions
+            fEquals[0][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][0], pObj->nFans );
+            fEquals[0][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][1], pObj->nFans );
+            fEquals[1][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][1], pObj->nFans );
+            fEquals[1][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][0], pObj->nFans );
+            if ( (fEquals[0][0] && fEquals[0][1]) || (fEquals[1][0] && fEquals[1][1]) )
+            {
+                // construct the MUX
+                pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_MUX, 3 );
+                pRes->nFans = 3;
+                pRes->pFans[0] = pObj->pFans[i];     pObj->pFans[i] = 2 * pRes->Id; // remains in support
+                pRes->pFans[1] = pObj->pFans[iVar1]; pObj->pFans[iVar1] = 127;  pObj->uSupp &= ~(1 << iVar1);
+                pRes->pFans[2] = pObj->pFans[iVar0]; pObj->pFans[iVar0] = 127;  pObj->uSupp &= ~(1 << iVar0);
+                // 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 );
+                // decompose the remainder
+                Kit_DsdDecompose_rec( pNtk, pObj, pPar );
+                return;
+            }
+        }
+
+        // try other inputs
+        for ( k = i+1; k < pObj->nFans; k++ )
+        {
+            // get four cofactors                                                ik
+            Kit_TruthCofactor0New( pCofs4[0][0], pCofs2[0], pObj->nFans, k ); // 00 
+            Kit_TruthCofactor1New( pCofs4[0][1], pCofs2[0], pObj->nFans, k ); // 01 
+            Kit_TruthCofactor0New( pCofs4[1][0], pCofs2[1], pObj->nFans, k ); // 10 
+            Kit_TruthCofactor1New( pCofs4[1][1], pCofs2[1], pObj->nFans, k ); // 11 
+            // compare equal pairs
+            fPairs[0][1] = fPairs[1][0] = Kit_TruthIsEqual(pCofs4[0][0], pCofs4[0][1], pObj->nFans);
+            fPairs[0][2] = fPairs[2][0] = Kit_TruthIsEqual(pCofs4[0][0], pCofs4[1][0], pObj->nFans);
+            fPairs[0][3] = fPairs[3][0] = Kit_TruthIsEqual(pCofs4[0][0], pCofs4[1][1], pObj->nFans);
+            fPairs[1][2] = fPairs[2][1] = Kit_TruthIsEqual(pCofs4[0][1], pCofs4[1][0], pObj->nFans);
+            fPairs[1][3] = fPairs[3][1] = Kit_TruthIsEqual(pCofs4[0][1], pCofs4[1][1], pObj->nFans);
+            fPairs[2][3] = fPairs[3][2] = Kit_TruthIsEqual(pCofs4[1][0], pCofs4[1][1], pObj->nFans);
+            nPairs = fPairs[0][1] + fPairs[0][2] + fPairs[0][3] + fPairs[1][2] + fPairs[1][3] + fPairs[2][3];
+            if ( nPairs != 3 && nPairs != 2 )
+                continue;
+
+            // decomposition exists
+            pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_AND, 2 );
+            pRes->nFans = 2;
+            pRes->pFans[0] = pObj->pFans[k]; pObj->pFans[k] = 2 * pRes->Id;  // remains the support
+            pRes->pFans[1] = pObj->pFans[i]; pObj->pFans[i] = 127;       pObj->uSupp &= ~(1 << i);
+            if ( !fPairs[0][1] && !fPairs[0][2] && !fPairs[0][3] ) // 00
+            {
+                pRes->pFans[0] ^= 1;  
+                pRes->pFans[1] ^= 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] ^= 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] ^= 1;  
+                Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[1][0], pObj->nFans, k );
+            }
+            else if ( !fPairs[3][0] && !fPairs[3][1] && !fPairs[3][2] ) // 11
+            {
+//                unsigned uSupp0 = Kit_TruthSupport(pCofs4[0][0], pObj->nFans);
+//                unsigned uSupp1 = Kit_TruthSupport(pCofs4[1][1], pObj->nFans);
+//                unsigned uSupp;
+//                Extra_PrintBinary( stdout, &uSupp0, pObj->nFans ); printf( "\n" );
+//                Extra_PrintBinary( stdout, &uSupp1, pObj->nFans ); printf( "\n" );
+                Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[1][1], pObj->nFans, k );
+//                uSupp = Kit_TruthSupport(pTruth, pObj->nFans);
+//                Extra_PrintBinary( stdout, &uSupp, pObj->nFans ); printf( "\n" ); printf( "\n" );
+            }
+            else
+            {
+                assert( fPairs[0][3] && fPairs[1][2] );
+                pRes->Type = KIT_DSD_XOR;;
+                Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
+            }
+            // decompose the remainder
+            Kit_DsdDecompose_rec( pNtk, pObj, pPar );
+            return;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
+{
+    Dsd_Ntk_t * pNtk;
+    Dsd_Obj_t * pObj;
+    int i, nVarsReal;
+    assert( nVars <= 16 );
+    pNtk = Kit_DsdNtkAlloc( pTruth, nVars );
+    pNtk->Root = 2*pNtk->nVars;
+    // create the first node
+    pObj = Dsd_ObjAlloc( pNtk, KIT_DSD_PRIME, nVars );
+    pNtk->pNodes[0] = pObj;
+    for ( i = 0; i < nVars; i++ )
+       pObj->pFans[i] = 2*i;
+    Kit_TruthCopy( Dsd_ObjTruth(pObj), pTruth, nVars );
+    pObj->uSupp = Kit_TruthSupport( pTruth, nVars );
+    // consider special cases
+    nVarsReal = Kit_WordCountOnes( pObj->uSupp );
+    if ( nVarsReal == 0 )
+    {
+        pObj->Type = KIT_DSD_CONST1;
+        pObj->nFans = 0;
+        pNtk->Root ^= (pTruth[0] == 0);
+        return pNtk;
+    }
+    if ( nVarsReal == 1 )
+    {
+        pObj->Type = KIT_DSD_VAR;
+        pObj->nFans = 1;
+        pObj->pFans[0] = 2 * Kit_WordFindFirstBit( pObj->uSupp );
+        pObj->pFans[0] ^= (pTruth[0] & 1);
+        return pNtk;
+    }
+    Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], &pNtk->Root );
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdTestCofs( Dsd_Ntk_t * pNtk, unsigned * pTruthInit )
+{
+    Dsd_Ntk_t * pNtk0, * pNtk1;
+    Dsd_Obj_t * pRoot;
+    unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) };
+    unsigned i, * pTruth;
+    int fVerbose = 1;
+
+//    pTruth = pTruthInit;
+
+    pRoot = Dsd_NtkRoot(pNtk);
+    pTruth = Dsd_ObjTruth(pRoot);
+    assert( pRoot->nFans == pNtk->nVars );
+
+    if ( fVerbose )
+    {
+        printf( "Function: " );
+//        Extra_PrintBinary( stdout, pTruth, (1 << pNtk->nVars) ); 
+        Extra_PrintHexadecimal( stdout, pTruth, pNtk->nVars ); 
+        printf( "\n" );
+    }
+    for ( i = 0; i < pNtk->nVars; i++ )
+    {
+        Kit_TruthCofactor0New( pCofs2[0], pTruth, pNtk->nVars, i );
+        pNtk0 = Kit_DsdDecompose( pCofs2[0], pNtk->nVars );
+        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 );
+        if ( fVerbose )
+        {
+            printf( "Cof%d1: ", i );
+            Kit_DsdPrint( stdout, pNtk1 );
+        }
+        Kit_DsdNtkFree( pNtk0 );
+    }
+    if ( fVerbose )
+        printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdTest( unsigned * pTruth, int nVars )
+{
+    Dsd_Ntk_t * pNtk;
+    pNtk = Kit_DsdDecompose( pTruth, nVars );
+
+//    if ( Kit_DsdFindLargeBox(pNtk, Dsd_NtkRoot(pNtk)) )
+//        Kit_DsdPrint( stdout, pNtk );
+
+    if ( Dsd_NtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 8 )
+        Kit_DsdTestCofs( pNtk, pTruth );
+
+    Kit_DsdNtkFree( pNtk );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/kit/kitTruth.c b/src/opt/kit/kitTruth.c
index 429875bc..5ac85524 100644
--- a/src/opt/kit/kitTruth.c
+++ b/src/opt/kit/kitTruth.c
@@ -311,7 +311,7 @@ int Kit_TruthSupportSize( unsigned * pTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-int Kit_TruthSupport( unsigned * pTruth, int nVars )
+unsigned Kit_TruthSupport( unsigned * pTruth, int nVars )
 {
     int i, Support = 0;
     for ( i = 0; i < nVars; i++ )
@@ -324,6 +324,57 @@ int Kit_TruthSupport( unsigned * pTruth, int nVars )
 
 /**Function*************************************************************
 
+  Synopsis    [Computes negative cofactor of the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
+{
+    int nWords = Kit_TruthWordNum( nVars );
+    int i, k, Step;
+
+    assert( iVar < nVars );
+    switch ( iVar )
+    {
+    case 0:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
+        return;
+    case 1:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
+        return;
+    case 2:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
+        return;
+    case 3:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
+        return;
+    case 4:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
+        return;
+    default:
+        Step = (1 << (iVar - 5));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+                pTruth[Step+i] = pTruth[i];
+            pTruth += 2*Step;
+        }
+        return;
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes positive cofactor of the function.]
 
   Description []
@@ -375,7 +426,7 @@ void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar )
 
 /**Function*************************************************************
 
-  Synopsis    [Computes negative cofactor of the function.]
+  Synopsis    [Computes positive cofactor of the function.]
 
   Description []
                
@@ -384,7 +435,7 @@ void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
+void Kit_TruthCofactor0New( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
 {
     int nWords = Kit_TruthWordNum( nVars );
     int i, k, Step;
@@ -394,31 +445,84 @@ void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
     {
     case 0:
         for ( i = 0; i < nWords; i++ )
-            pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
+            pOut[i] = (pIn[i] & 0x55555555) | ((pIn[i] & 0x55555555) << 1);
         return;
     case 1:
         for ( i = 0; i < nWords; i++ )
-            pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
+            pOut[i] = (pIn[i] & 0x33333333) | ((pIn[i] & 0x33333333) << 2);
         return;
     case 2:
         for ( i = 0; i < nWords; i++ )
-            pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
+            pOut[i] = (pIn[i] & 0x0F0F0F0F) | ((pIn[i] & 0x0F0F0F0F) << 4);
         return;
     case 3:
         for ( i = 0; i < nWords; i++ )
-            pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
+            pOut[i] = (pIn[i] & 0x00FF00FF) | ((pIn[i] & 0x00FF00FF) << 8);
         return;
     case 4:
         for ( i = 0; i < nWords; i++ )
-            pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
+            pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i] & 0x0000FFFF) << 16);
         return;
     default:
         Step = (1 << (iVar - 5));
         for ( k = 0; k < nWords; k += 2*Step )
         {
             for ( i = 0; i < Step; i++ )
-                pTruth[Step+i] = pTruth[i];
-            pTruth += 2*Step;
+                pOut[i] = pOut[Step+i] = pIn[i];
+            pIn += 2*Step;
+            pOut += 2*Step;
+        }
+        return;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes positive cofactor of the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
+{
+    int nWords = Kit_TruthWordNum( nVars );
+    int i, k, Step;
+
+    assert( iVar < nVars );
+    switch ( iVar )
+    {
+    case 0:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (pIn[i] & 0xAAAAAAAA) | ((pIn[i] & 0xAAAAAAAA) >> 1);
+        return;
+    case 1:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (pIn[i] & 0xCCCCCCCC) | ((pIn[i] & 0xCCCCCCCC) >> 2);
+        return;
+    case 2:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (pIn[i] & 0xF0F0F0F0) | ((pIn[i] & 0xF0F0F0F0) >> 4);
+        return;
+    case 3:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (pIn[i] & 0xFF00FF00) | ((pIn[i] & 0xFF00FF00) >> 8);
+        return;
+    case 4:
+        for ( i = 0; i < nWords; i++ )
+            pOut[i] = (pIn[i] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
+        return;
+    default:
+        Step = (1 << (iVar - 5));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+                pOut[i] = pOut[Step+i] = pIn[Step+i];
+            pIn += 2*Step;
+            pOut += 2*Step;
         }
         return;
     }
@@ -733,6 +837,8 @@ void Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVar
                 pOut[Step+i] = pCof1[Step+i];
             }
             pOut += 2*Step;
+            pCof0 += 2*Step;
+            pCof1 += 2*Step;
         }
         return;
     }
diff --git a/src/opt/kit/module.make b/src/opt/kit/module.make
index 36beda7a..d1363ee2 100644
--- a/src/opt/kit/module.make
+++ b/src/opt/kit/module.make
@@ -1,4 +1,5 @@
 SRC +=  src/opt/kit/kitBdd.c \
+    src/opt/kit/kitDsd.c \
     src/opt/kit/kitFactor.c \
     src/opt/kit/kitGraph.c \
     src/opt/kit/kitHop.c \