Version abc50807

24 files changed, 2393 insertions, 298 deletions

diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index 1179e400..b8c9a3ef 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -28,41 +28,45 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int Ntk_CommandPrintStats   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandPrintIo      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandPrintFanio   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandPrintFactor  ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Ntk_CommandCollapse     ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandStrash       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandBalance      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandRenode       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandCleanup      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandFx           ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Ntk_CommandLogic        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandMiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandFrames       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandSop          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandBdd          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandSat          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Ntk_CommandFraig        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandFraigTrust   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandFraigStore   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandFraigClean   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandFraigSweep   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Ntk_CommandMap          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandUnmap        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandAttach       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandSuperChoice  ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Ntk_CommandFpga         ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Ntk_CommandCec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintStats   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintIo      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintFanio   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintFactor  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowBdd      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandCollapse     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandStrash       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBalance      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRenode       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCleanup      ( 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_CommandRes          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandLogic        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFrames       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSop          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBdd          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSat          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExtSeqDcs    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandFraig        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigTrust   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigStore   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigClean   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigSweep   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandMap          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandUnmap        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAttach       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSuperChoice  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandFpga         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandCec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -81,41 +85,46 @@ static int Ntk_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv
 ***********************************************************************/
 void Abc_Init( Abc_Frame_t * pAbc )
 {
-    Cmd_CommandAdd( pAbc, "Printing",     "print_stats",   Ntk_CommandPrintStats,       0 ); 
-    Cmd_CommandAdd( pAbc, "Printing",     "print_io",      Ntk_CommandPrintIo,          0 );
-    Cmd_CommandAdd( pAbc, "Printing",     "print_fanio",   Ntk_CommandPrintFanio,       0 );
-    Cmd_CommandAdd( pAbc, "Printing",     "print_factor",  Ntk_CommandPrintFactor,      0 );
-
-    Cmd_CommandAdd( pAbc, "Synthesis",    "collapse",      Ntk_CommandCollapse,         1 );
-    Cmd_CommandAdd( pAbc, "Synthesis",    "strash",        Ntk_CommandStrash,           1 );
-    Cmd_CommandAdd( pAbc, "Synthesis",    "balance",       Ntk_CommandBalance,          1 );
-    Cmd_CommandAdd( pAbc, "Synthesis",    "renode",        Ntk_CommandRenode,           1 );
-    Cmd_CommandAdd( pAbc, "Synthesis",    "cleanup",       Ntk_CommandCleanup,          1 );
-    Cmd_CommandAdd( pAbc, "Synthesis",    "fx",            Ntk_CommandFx,               1 );
-
-    Cmd_CommandAdd( pAbc, "Various",      "logic",         Ntk_CommandLogic,            1 );
-    Cmd_CommandAdd( pAbc, "Various",      "miter",         Ntk_CommandMiter,            1 );
-    Cmd_CommandAdd( pAbc, "Various",      "frames",        Ntk_CommandFrames,           1 );
-    Cmd_CommandAdd( pAbc, "Various",      "sop",           Ntk_CommandSop,              0 );
-    Cmd_CommandAdd( pAbc, "Various",      "bdd",           Ntk_CommandBdd,              0 );
-    Cmd_CommandAdd( pAbc, "Various",      "sat",           Ntk_CommandSat,              0 );
-
-    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Ntk_CommandFraig,            1 );
-    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_trust",   Ntk_CommandFraigTrust,       1 );
-    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_store",   Ntk_CommandFraigStore,       0 );
-    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_restore", Ntk_CommandFraigRestore,     1 );
-    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_clean",   Ntk_CommandFraigClean,       0 );
-    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_sweep",   Ntk_CommandFraigSweep,       1 );
-
-    Cmd_CommandAdd( pAbc, "SC mapping",   "map",           Ntk_CommandMap,              1 );
-    Cmd_CommandAdd( pAbc, "SC mapping",   "unmap",         Ntk_CommandUnmap,            1 );
-    Cmd_CommandAdd( pAbc, "SC mapping",   "attach",        Ntk_CommandAttach,           1 );
-    Cmd_CommandAdd( pAbc, "SC mapping",   "sc",            Ntk_CommandSuperChoice,      1 );
-
-    Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Ntk_CommandFpga,             1 );
-
-    Cmd_CommandAdd( pAbc, "Verification", "cec",           Ntk_CommandCec,              0 );
-    Cmd_CommandAdd( pAbc, "Verification", "sec",           Ntk_CommandSec,              0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_stats",   Abc_CommandPrintStats,       0 ); 
+    Cmd_CommandAdd( pAbc, "Printing",     "print_io",      Abc_CommandPrintIo,          0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_fanio",   Abc_CommandPrintFanio,       0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_factor",  Abc_CommandPrintFactor,      0 );
+
+    Cmd_CommandAdd( pAbc, "Printing",     "show_bdd",      Abc_CommandShowBdd,          0 );
+
+    Cmd_CommandAdd( pAbc, "Synthesis",    "collapse",      Abc_CommandCollapse,         1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "strash",        Abc_CommandStrash,           1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "balance",       Abc_CommandBalance,          1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "renode",        Abc_CommandRenode,           1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "cleanup",       Abc_CommandCleanup,          1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "fx",            Abc_CommandFastExtract,      1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "dsd",           Abc_CommandDisjoint,         1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "res",           Abc_CommandRes,              1 );
+
+    Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
+    Cmd_CommandAdd( pAbc, "Various",      "miter",         Abc_CommandMiter,            1 );
+    Cmd_CommandAdd( pAbc, "Various",      "frames",        Abc_CommandFrames,           1 );
+    Cmd_CommandAdd( pAbc, "Various",      "sop",           Abc_CommandSop,              0 );
+    Cmd_CommandAdd( pAbc, "Various",      "bdd",           Abc_CommandBdd,              0 );
+    Cmd_CommandAdd( pAbc, "Various",      "sat",           Abc_CommandSat,              0 );
+    Cmd_CommandAdd( pAbc, "Various",      "ext_seq_dcs",   Abc_CommandExtSeqDcs,        0 );
+
+    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
+    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_trust",   Abc_CommandFraigTrust,       1 );
+    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_store",   Abc_CommandFraigStore,       0 );
+    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_restore", Abc_CommandFraigRestore,     1 );
+    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_clean",   Abc_CommandFraigClean,       0 );
+    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_sweep",   Abc_CommandFraigSweep,       1 );
+
+    Cmd_CommandAdd( pAbc, "SC mapping",   "map",           Abc_CommandMap,              1 );
+    Cmd_CommandAdd( pAbc, "SC mapping",   "unmap",         Abc_CommandUnmap,            1 );
+    Cmd_CommandAdd( pAbc, "SC mapping",   "attach",        Abc_CommandAttach,           1 );
+    Cmd_CommandAdd( pAbc, "SC mapping",   "sc",            Abc_CommandSuperChoice,      1 );
+
+    Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Abc_CommandFpga,             1 );
+
+    Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
+    Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
 
     Ft_FactorStartMan();
 }
@@ -148,7 +157,7 @@ void Abc_End()
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -202,7 +211,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -271,7 +280,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -322,7 +331,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -391,6 +400,81 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pNode;
+    int c;
+    extern void Abc_NodePrintBdd( Abc_Obj_t * pNode );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsLogicBdd(pNtk) )
+    {
+        fprintf( pErr, "Printing BDDs can only be done for logic BDD networks.\n" );
+        return 1;
+    }
+
+    if ( argc != util_optind + 1 )
+    {
+        fprintf( pErr, "Wrong number of auguments.\n" );
+        goto usage;
+    }
+
+    pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+    if ( pNode == NULL )
+    {
+        fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+        return 1;
+    }
+    Abc_NodePrintBdd( pNode );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: show_bdd [-h] <node>\n" );
+    fprintf( pErr, "       visualizes the BDD of a node using DOT and GSVIEW\n" );
+#ifdef WIN32
+    fprintf( pErr, "       \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
+    fprintf( pErr, "       (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
+#endif
+    fprintf( pErr, "\tnode  : the node to consider\n");
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
@@ -403,7 +487,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -443,7 +527,7 @@ int Ntk_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
         pNtkRes = Abc_NtkCollapse( pNtk, 1 );
     else
     {
-        pNtk = Abc_NtkStrash( pNtk );
+        pNtk = Abc_NtkStrash( pNtk, 0 );
         pNtkRes = Abc_NtkCollapse( pNtk, 1 );
         Abc_NtkDelete( pNtk );
     }
@@ -475,22 +559,27 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
+    int fAllNodes;
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fAllNodes = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "ah" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'a':
+            fAllNodes ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -505,7 +594,7 @@ int Ntk_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkStrash( pNtk );
+    pNtkRes = Abc_NtkStrash( pNtk, fAllNodes );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Strashing has failed.\n" );
@@ -516,8 +605,9 @@ int Ntk_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: strash [-h]\n" );
+    fprintf( pErr, "usage: strash [-ah]\n" );
     fprintf( pErr, "\t        transforms combinational logic into an AIG\n" );
+    fprintf( pErr, "\t-a    : toggles between using all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "DFS" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -533,7 +623,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -602,7 +692,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -709,7 +799,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -767,7 +857,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFx( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk;
     FILE * pOut, * pErr;
@@ -875,6 +965,129 @@ usage:
     return 1;       
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes, * pNtkNew;
+    int fGlobal, fRecursive, fVerbose, fPrint, fShort, c;
+
+    extern Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort );
+    extern int         Abc_NtkDsdRecursive( Abc_Ntk_t * pNtk, bool fVerbose );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fGlobal    = 1;
+    fRecursive = 0;
+    fVerbose   = 0;
+    fPrint     = 0;
+    fShort     = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "grvpsh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'g':
+                fGlobal ^= 1;
+                break;
+            case 'r':
+                fRecursive ^= 1;
+                break;
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'p':
+                fPrint ^= 1;
+                break;
+            case 's':
+                fShort ^= 1;
+                break;
+            case 'h':
+                goto usage;
+                break;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !fGlobal && !fRecursive )
+    {
+        fprintf( pErr, "Decomposition should be either global or recursive.\n" );
+        return 1;
+    }
+
+    if ( fGlobal )
+    {
+        // get the new network
+        if ( !Abc_NtkIsAig(pNtk) )
+        {
+            pNtkNew = Abc_NtkStrash( pNtk, 0 );
+            pNtkRes = Abc_NtkDsdGlobal( pNtkNew, fVerbose, fPrint, fShort );
+            Abc_NtkDelete( pNtkNew );
+        }
+        else
+        {
+            pNtkRes = Abc_NtkDsdGlobal( pNtk, fVerbose, fPrint, fShort );
+        }
+        if ( pNtkRes == NULL )
+        {
+            fprintf( pErr, "Global disjoint support decomposition has failed.\n" );
+            return 1;
+        }
+        if ( fRecursive )
+        {
+            if ( !Abc_NtkDsdRecursive( pNtkRes, fVerbose ) )
+            {
+                fprintf( pErr, "Recursive decomposition has failed.\n" );
+                Abc_NtkDelete( pNtkRes );
+                return 1;
+            }
+        }
+        // replace the current network
+        Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    }
+    else if ( fRecursive )
+    {
+        if ( !Abc_NtkIsLogicBdd( pNtk ) )
+        {
+            fprintf( pErr, "This command is only applicable to logic BDD networks.\n" );
+            return 1;
+        }
+        if ( !Abc_NtkDsdRecursive( pNtk, fVerbose ) )
+            fprintf( pErr, "Recursive decomposition has failed.\n" );
+    }
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: dsd [-grvpsh]\n" );
+    fprintf( pErr, "\t     decomposes the network using disjoint-support decomposition\n" );
+    fprintf( pErr, "\t-g     : collapses the network and decomposes shared BDDs [default = %s]\n", fGlobal? "yes": "no" );  
+    fprintf( pErr, "\t-r     : applied DSD and MUX-decomposition recursively [default = %s]\n", fRecursive? "yes": "no" );  
+    fprintf( pErr, "\t-v     : prints DSD statistics and runtime [default = %s]\n", fVerbose? "yes": "no" ); 
+    fprintf( pErr, "\t-p     : prints DSD structure to the standard output [default = %s]\n", fPrint? "yes": "no" ); 
+    fprintf( pErr, "\t-s     : use short PI names when printing DSD structure [default = %s]\n", fShort? "yes": "no" ); 
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
 
 /**Function*************************************************************
 
@@ -887,7 +1100,106 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandRes( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    Abc_ManRes_t * p;
+    extern int Abc_NtkAigResynthesize( Abc_Ntk_t * pNtk, Abc_ManRes_t * p );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    p = Abc_NtkManResStart();
+    p->fVerbose     =  0;
+    p->nNodeSizeMax = 10;
+    p->nConeSizeMax = 10;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "ncvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'n':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            p->nNodeSizeMax = atoi(argv[util_optind]);
+            util_optind++;
+            if ( p->nNodeSizeMax < 0 ) 
+                goto usage;
+            break;
+        case 'c':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-c\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            p->nConeSizeMax = atoi(argv[util_optind]);
+            util_optind++;
+            if ( p->nConeSizeMax < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            p->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        Abc_NtkManResStop( p );
+        return 1;
+    }
+    if ( !Abc_NtkIsAig(pNtk) )
+    {
+        fprintf( pErr, "This command can only be applied to an AIG.\n" );
+        Abc_NtkManResStop( p );
+        return 1;
+    }
+    if ( Abc_NtkCountChoiceNodes(pNtk) )
+    {
+        fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" );
+        Abc_NtkManResStop( p );
+        return 1;
+    }
+
+    // modify the current network
+    Abc_NtkAigResynthesize( pNtk, p );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: res [-n num] [-c num] [-vh]\n" );
+    fprintf( pErr, "\t         performs technology-independent resynthesis of the AIG\n" );
+    fprintf( pErr, "\t-n num : the max support of the collapsed node [default = %d]\n", p->nNodeSizeMax );  
+    fprintf( pErr, "\t-c num : the max support of the containing cone [default = %d]\n", p->nConeSizeMax );  
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", p->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -951,7 +1263,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtk1, * pNtk2, * pNtkRes;
@@ -1025,7 +1337,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkTemp, * pNtkRes;
@@ -1075,7 +1387,7 @@ int Ntk_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
     // get the new network
     if ( !Abc_NtkIsAig(pNtk) )
     {
-        pNtkTemp = Abc_NtkStrash( pNtk );
+        pNtkTemp = Abc_NtkStrash( pNtk, 0 );
         pNtkRes  = Abc_NtkFrames( pNtkTemp, nFrames, fInitial );
         Abc_NtkDelete( pNtkTemp );
     }
@@ -1111,7 +1423,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -1171,7 +1483,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -1231,7 +1543,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -1295,6 +1607,76 @@ usage:
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandExtSeqDcs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int fVerbose;
+    extern int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNet, bool fVerbose );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkLatchNum(pNtk) == 0 )
+    {
+        fprintf( stdout, "The current network has no latches.\n" );
+        return 0;
+    }
+    if ( !Abc_NtkIsAig(pNtk) )
+    {
+        fprintf( stdout, "This command works only for AIGs.\n" );
+        return 0;
+    }
+    if ( !Abc_NtkExtractSequentialDcs( pNtk, fVerbose ) )
+    {
+        fprintf( stdout, "Extracting sequential don't-cares has failed.\n" );
+        return 1;
+    }
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: ext_seq_dcs [-vh]\n" );
+    fprintf( pErr, "\t         create EXDC network using unreachable states\n" );
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 
 
@@ -1309,7 +1691,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     char Buffer[100];
     Fraig_Params_t Params;
@@ -1419,7 +1801,7 @@ int Ntk_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
     else
     {
-        pNtk = Abc_NtkStrash( pNtk );
+        pNtk = Abc_NtkStrash( pNtk, 0 );
         pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
         Abc_NtkDelete( pNtk );
     }
@@ -1464,7 +1846,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFraigTrust( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFraigTrust( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -1528,7 +1910,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFraigStore( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFraigStore( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -1589,7 +1971,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFraigRestore( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFraigRestore( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -1653,7 +2035,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFraigClean( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFraigClean( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -1702,7 +2084,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -1779,7 +2161,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -1840,7 +2222,7 @@ int Ntk_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsAig(pNtk) )
     {
-        pNtk = Abc_NtkStrash( pNtk );
+        pNtk = Abc_NtkStrash( pNtk, 0 );
         if ( pNtk == NULL )
         {
             fprintf( pErr, "Strashing before mapping has failed.\n" );
@@ -1909,7 +2291,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -1970,7 +2352,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandAttach( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAttach( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -2033,7 +2415,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -2098,7 +2480,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -2141,7 +2523,7 @@ int Ntk_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( !Abc_NtkIsAig(pNtk) )
     {
         // strash and balance the network
-        pNtk = Abc_NtkStrash( pNtk );
+        pNtk = Abc_NtkStrash( pNtk, 0 );
         if ( pNtk == NULL )
         {
             fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
@@ -2202,7 +2584,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtk1, * pNtk2;
@@ -2273,7 +2655,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtk1, * pNtk2;
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 35fa85e9..9b9bd81e 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -21,25 +21,6 @@
 #ifndef __ABC_H__
 #define __ABC_H__
 
-/*
-    In the netlist, the PI/PO arrays store PI/PO nets.
-    The names belongs to the nets and are stored in pNet->pData.
-    When a netlist is made combinational:
-    - LO/LI nets are added to PI/PO arrays,
-    - the array of latches is temporarily stored in vLatch2,
-    - the original number of PIs/POs is remembered in nPisOld/nPosOld.
-
-    In a logic network, the PI/PO arrays store PI/PO nodes.
-    The PO nodes have only one fanin edge, which can be complemented.
-    The arrays vNamesPi/vNamesPo/vNamesLatch store PI/PO/latch names.
-    The internal nodes are nameless.
-    When a logic network is made combinational:
-    - laches are added to the PI/PO arrays,
-    - the arrays of names are not changed,
-    - the array of latches is temporarily stored in vLatch2,
-    - the original number of PIs/POs is remembered in nPisOld/nPosOld.
-*/
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -103,6 +84,7 @@ typedef struct Abc_Obj_t_     Abc_Obj_t;
 typedef struct Abc_Ntk_t_     Abc_Ntk_t;
 typedef struct Abc_Aig_t_     Abc_Aig_t;
 typedef struct Abc_ManTime_t_ Abc_ManTime_t;
+typedef struct Abc_ManRes_t_  Abc_ManRes_t;
 typedef struct Abc_Time_t_    Abc_Time_t;
 
 struct Abc_Time_t_
@@ -182,6 +164,30 @@ struct Abc_Ntk_t_
     Extra_MmStep_t * pMmStep;       // memory manager for arrays
 };
 
+struct Abc_ManRes_t_
+{
+    // user specified parameters
+    int              nNodeSizeMax;  // the limit on the size of the supernode
+    int              nConeSizeMax;  // the limit on the size of the containing cone
+    int              fVerbose;      // the verbosity flag
+    // internal parameters
+    DdManager *      dd;            // the BDD manager
+    DdNode *         bCubeX;        // the cube of PI variables
+    Abc_Obj_t *      pNode;         // the node currently considered
+    Vec_Ptr_t *      vFaninsNode;   // fanins of the supernode
+    Vec_Ptr_t *      vInsideNode;   // inside of the supernode
+    Vec_Ptr_t *      vFaninsCone;   // fanins of the containing cone
+    Vec_Ptr_t *      vInsideCone;   // inside of the containing cone
+    Vec_Ptr_t *      vVisited;      // the visited nodes
+    Vec_Str_t *      vCube;         // temporary cube for generating covers
+    Vec_Int_t *      vForm;         // the factored form (temporary)
+    // runtime statistics
+    int              time1;
+    int              time2;
+    int              time3;
+    int              time4;
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
@@ -380,11 +386,12 @@ extern bool               Abc_NtkCheck( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 /*=== abcCollapse.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose );
+extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly );
+extern void               Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk );
 /*=== abcCreate.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type );
 extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type );
 extern void               Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-extern void               Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 extern Abc_Ntk_t *        Abc_NtkDup( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkDelete( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
@@ -407,6 +414,7 @@ extern Abc_Obj_t *        Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFani
 extern Abc_Obj_t *        Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
 extern Abc_Obj_t *        Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
 extern Abc_Obj_t *        Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
+extern Abc_Obj_t *        Abc_NodeClone( Abc_Obj_t * pNode );
 /*=== abcDfs.c ==========================================================*/
 extern Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_AigDfs( Abc_Ntk_t * pNtk );
@@ -415,6 +423,7 @@ extern bool               Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
 /*=== abcFanio.c ==========================================================*/
 extern void               Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
 extern void               Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
+extern void               Abc_ObjRemoveFanins( Abc_Obj_t * pObj );
 extern void               Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFaninNew );
 extern void               Abc_ObjTransferFanout( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
 extern void               Abc_ObjReplace( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
@@ -426,7 +435,7 @@ extern Abc_Ntk_t *        Abc_NtkFraigRestore();
 extern void               Abc_NtkFraigStoreClean();
 /*=== abcFunc.c ==========================================================*/
 extern int                Abc_NtkSopToBdd( Abc_Ntk_t * pNtk );
-extern char *             Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFunc, int nFanins, Vec_Str_t * vCube, int fMode );
+extern char *             Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode );
 extern int                Abc_NtkBddToSop( Abc_Ntk_t * pNtk );
 extern void               Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 );
 extern int                Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
@@ -475,6 +484,9 @@ extern int                Abc_NodeMffcRemove( Abc_Obj_t * pNode );
 /*=== abcRenode.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple );
 extern DdNode *           Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
+/*=== abcRes.c ==========================================================*/
+extern Abc_ManRes_t *     Abc_NtkManResStart();
+extern void               Abc_NtkManResStop( Abc_ManRes_t * p );
 /*=== abcSat.c ==========================================================*/
 extern bool               Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose );
 extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk );
@@ -497,7 +509,7 @@ extern bool               Abc_SopCheck( char * pSop, int nFanins );
 extern void               Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_Int_t * vVars );
 extern void               Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp );
 /*=== abcStrash.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes );
 extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
 extern Abc_Ntk_t *        Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate );
 /*=== abcSweep.c ==========================================================*/
@@ -512,7 +524,7 @@ extern void               Abc_NtkTimeSetDefaultArrival( Abc_Ntk_t * pNtk, float
 extern void               Abc_NtkTimeSetDefaultRequired( Abc_Ntk_t * pNtk, float Rise, float Fall );
 extern void               Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall );
 extern void               Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall );
-extern void               Abc_NtkTimeFinalize( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkTimeInitialize( Abc_Ntk_t * pNtk );
 extern void               Abc_ManTimeStop( Abc_ManTime_t * p );
 extern void               Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew );
 extern void               Abc_NtkSetNodeLevelsArrival( Abc_Ntk_t * pNtk );
@@ -549,6 +561,9 @@ extern void               Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t *
 extern int                Abc_NodeCompareLevelsIncrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
 extern int                Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
 extern Vec_Ptr_t *        Abc_AigCollectAll( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t *        Abc_NodeGetFaninNames( Abc_Obj_t * pNode );
+extern void               Abc_NodeFreeFaninNames( Vec_Ptr_t * vNames );
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 67cfe9df..6a733185 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -108,11 +108,11 @@ bool Abc_NtkCheck( Abc_Ntk_t * pNtk )
     // check the EXDC network if present
     if ( pNtk->pExdc )
     {
-        if ( pNtk->Type != pNtk->pExdc->Type )
-        {
-            fprintf( stdout, "NetworkCheck: Network and its EXDC have different types.\n" );
-            return 0;
-        }
+//        if ( pNtk->Type != pNtk->pExdc->Type )
+//        {
+//            fprintf( stdout, "NetworkCheck: Network and its EXDC have different types.\n" );
+//            return 0;
+//        }
         return Abc_NtkCheck( pNtk->pExdc );
     }
     return 1;
diff --git a/src/base/abc/abcCollapse.c b/src/base/abc/abcCollapse.c
index 372b1553..3ee086c0 100644
--- a/src/base/abc/abcCollapse.c
+++ b/src/base/abc/abcCollapse.c
@@ -24,7 +24,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk );
 static DdNode *    Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode );
 static Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk );
 static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc );
@@ -52,33 +51,16 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
 
     assert( Abc_NtkIsAig(pNtk) );
 
-    // perform FPGA mapping
-    dd = Abc_NtkGlobalBdds( pNtk );    
+    // compute the global BDDs
+    dd = Abc_NtkGlobalBdds( pNtk, 0 );    
     if ( dd == NULL )
         return NULL;
     if ( fVerbose )
         printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
-/*
-    {
-        Abc_Obj_t * pNode;
-        int i;
-        Abc_NtkForEachPo( pNtk, pNode, i )
-        {
-            Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext );
-            pNode->pNext = NULL;
-        }
-        Abc_NtkForEachLatch( pNtk, pNode, i )
-        {
-            Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext );
-            pNode->pNext = NULL;
-        }
-    }
-    Extra_StopManager( dd );
-    return NULL;
-*/
 
-    // transform the result of mapping into a BDD network
+    // create the new network
     pNtkNew = Abc_NtkFromGlobalBdds( dd, pNtk );
+    Abc_NtkFreeGlobalBdds( dd, pNtk );
     if ( pNtkNew == NULL )
     {
         Cudd_Quit( dd );
@@ -110,8 +92,9 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk )
+DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
 {
+    int fReorder = 1;
     ProgressBar * pProgress;
     Abc_Obj_t * pNode;
     DdNode * bFunc;
@@ -120,7 +103,8 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk )
 
     // start the manager
     dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+    if ( fReorder )
+        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
 
     // set the elementary variables
     Abc_NtkCleanCopy( pNtk );
@@ -130,31 +114,60 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk )
     pNode = Abc_AigConst1( pNtk->pManFunc );
     pNode->pCopy = (Abc_Obj_t *)dd->one;   Cudd_Ref( dd->one );
 
-    // construct the BDDs
-    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
-    Abc_NtkForEachCo( pNtk, pNode, i )
+    if ( fLatchOnly )
     {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
-        bFunc = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) );
-        if ( bFunc == NULL )
+        // construct the BDDs
+        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkLatchNum(pNtk) );
+        Abc_NtkForEachLatch( pNtk, pNode, i )
         {
-            printf( "Constructing global BDDs timed out.\n" );
-            Extra_ProgressBarStop( pProgress );
-            Cudd_Quit( dd );
-            return NULL;
+            Extra_ProgressBarUpdate( pProgress, i, NULL );
+            bFunc = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) );
+            if ( bFunc == NULL )
+            {
+                printf( "Constructing global BDDs timed out.\n" );
+                Extra_ProgressBarStop( pProgress );
+                Cudd_Quit( dd );
+                return NULL;
+            }
+            bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );
+            pNode->pNext = (Abc_Obj_t *)bFunc;   Cudd_Ref( bFunc );
         }
-        bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );
-        pNode->pNext = (Abc_Obj_t *)bFunc;   Cudd_Ref( bFunc );
+        Extra_ProgressBarStop( pProgress );
+    }
+    else
+    {
+        // construct the BDDs
+        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+        Abc_NtkForEachCo( pNtk, pNode, i )
+        {
+            Extra_ProgressBarUpdate( pProgress, i, NULL );
+            bFunc = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) );
+            if ( bFunc == NULL )
+            {
+                printf( "Constructing global BDDs timed out.\n" );
+                Extra_ProgressBarStop( pProgress );
+                Cudd_Quit( dd );
+                return NULL;
+            }
+            bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );
+            pNode->pNext = (Abc_Obj_t *)bFunc;   Cudd_Ref( bFunc );
+        }
+        Extra_ProgressBarStop( pProgress );
     }
-    Extra_ProgressBarStop( pProgress );
 
     // derefence the intermediate BDDs
     Abc_NtkForEachNode( pNtk, pNode, i )
         if ( pNode->pCopy ) 
+        {
             Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
-    Abc_NtkCleanCopy( pNtk );
+            pNode->pCopy = NULL;
+        }
     // reorder one more time
-    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 0 );
+    if ( fReorder )
+    {
+        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
+        Cudd_AutodynDisable( dd );
+    }
     return dd;
 }
 
@@ -227,9 +240,6 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)pNode->pNext );
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
-        // deref the BDD of the PO
-        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext );
-        pNode->pNext = NULL;
     }
     Extra_ProgressBarStop( pProgress );
     // transfer the names
@@ -263,6 +273,30 @@ Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode
     return pNodeNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Dereferences global functions of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        if ( pNode->pNext == NULL )
+            continue;
+        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext );
+        pNode->pNext = NULL;
+    }
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcCreate.c
index e4cfb7e3..5049a72e 100644
--- a/src/base/abc/abcCreate.c
+++ b/src/base/abc/abcCreate.c
@@ -157,34 +157,6 @@ void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
 
 /**Function*************************************************************
 
-  Synopsis    [Finalizes the network using the existing network as a model.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
-{
-    Abc_Obj_t * pObj, * pDriver, * pDriverNew;
-    int i;
-    assert( !Abc_NtkIsNetlist(pNtk) );
-    // set the COs of the strashed network
-    Abc_NtkForEachCo( pNtk, pObj, i )
-    {
-        pDriver    = Abc_ObjFanin0(pObj);
-        pDriverNew = pDriver->pCopy;
-        Abc_ObjAddFanin( pObj->pCopy, pDriverNew );
-    }
-    // transfer the names
-    Abc_NtkDupNameArrays( pNtk, pNtkNew );
-    Abc_ManTimeDup( pNtk, pNtkNew );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Duplicate the Ntk.]
 
   Description []
@@ -635,7 +607,58 @@ void Abc_NtkRemovePoNode( Abc_Obj_t * pNode )
 ***********************************************************************/
 Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName )
 {
-    return NULL;
+    Abc_Obj_t * pNode, * pDriver;
+    int i, Num;
+    // check if the node is among CIs
+    Abc_NtkForEachCi( pNtk, pNode, i )
+    {
+        if ( strcmp( Abc_NtkNameCi(pNtk,i), pName ) == 0 )
+        {
+            if ( i < Abc_NtkPiNum(pNtk) )
+                printf( "Node \"%s\" is a primary input.\n", pName );
+            else
+                printf( "Node \"%s\" is a latch output.\n", pName );
+            return NULL;
+        }
+    }
+    // search the node among COs
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        if ( strcmp( Abc_NtkNameCo(pNtk,i), pName ) == 0 )
+        {
+            pDriver = Abc_ObjFanin0(pNode);
+            if ( !Abc_ObjIsNode(pDriver) )
+            {
+                printf( "Node \"%s\" does not have logic associated with it.\n", pName );
+                return NULL;
+            }
+            return pDriver;
+        }
+    }
+    // find the internal node
+    if ( pName[0] != '[' || pName[strlen(pName)-1] != ']' )
+    {
+        printf( "Node \"%s\" has non-standard name (expected name is \"[integer]\").\n", pName );
+        return NULL;
+    }
+    Num = atoi( pName + 1 );
+    if ( Num < 0 || Num > Abc_NtkObjNum(pNtk) )
+    {
+        printf( "The node \"%s\" with ID %d is not in the current network.\n", pName, Num );
+        return NULL;
+    }
+    pNode = Abc_NtkObj( pNtk, Num );
+    if ( pNode == NULL )
+    {
+        printf( "The node \"%s\" with ID %d has been removed from the current network.\n", pName, Num );
+        return NULL;
+    }
+    if ( !Abc_ObjIsNode(pNode) )
+    {
+        printf( "Object with ID %d is not a node.\n", Num );
+        return NULL;
+    }
+    return pNode;
 }
 
 /**Function*************************************************************
@@ -997,6 +1020,27 @@ Abc_Obj_t * Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t *
     return pNode;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Clones the given node but does not assign the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeClone( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pClone, * pFanin;
+    int i;
+    assert( Abc_ObjIsNode(pNode) );
+    pClone = Abc_NtkCreateNode( pNode->pNtk );   
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        Abc_ObjAddFanin( pClone, pFanin );
+    return pClone;
+}
 
 
 
diff --git a/src/base/abc/abcDsd.c b/src/base/abc/abcDsd.c
index 47b288d3..c9adab38 100644
--- a/src/base/abc/abcDsd.c
+++ b/src/base/abc/abcDsd.c
@@ -19,18 +19,443 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "dsd.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
  
+static Abc_Ntk_t *     Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort );
+static Dsd_Manager_t * Abc_NtkDsdPerform( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose );
+static void            Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+static Abc_Obj_t *     Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew );
+
+static Vec_Ptr_t *     Abc_NtkCollectNodesForDsd( Abc_Ntk_t * pNtk );
+static void            Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd );
+static bool            Abc_NodeIsForDsd( Abc_Obj_t * pNode );
+static int             Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int nVars );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Decomposes the network using disjoint-support decomposition.]
+  Synopsis    [Derives the DSD network.]
+
+  Description [Takes the strashed network (pNtk), derives global BDDs for
+  the combinational outputs of this network, and decomposes these BDDs using
+  disjoint support decomposition. Finally, constructs and return a new 
+  network, which is topologically equivalent to the decomposition tree.
+  Allocates and frees a new BDD manager and a new DSD manager.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
+{
+    int fCheck = 1;
+    Abc_Ntk_t * pNtkNew;
+    DdManager * dd;
+
+    assert( Abc_NtkIsAig(pNtk) );
+
+    // perform FPGA mapping
+    dd = Abc_NtkGlobalBdds( pNtk, 0 );    
+    if ( dd == NULL )
+        return NULL;
+    if ( fVerbose )
+        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+
+    // transform the result of mapping into a BDD network
+    pNtkNew = Abc_NtkDsdInternal( dd, pNtk, fVerbose, fPrint, fShort );
+    if ( pNtkNew == NULL )
+    {
+        Cudd_Quit( dd );
+        return NULL;
+    }
+    Extra_StopManager( dd );
+
+    // make sure that everything is okay
+    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkDsdGlobal: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
+{
+    Dsd_Manager_t * pManDsd;
+    Abc_Ntk_t * pNtkNew;
+
+    // perform the decomposition
+    pManDsd = Abc_NtkDsdPerform( dd, pNtk, fVerbose );
+    Abc_NtkFreeGlobalBdds( dd, pNtk );
+    if ( pManDsd == NULL )
+        return NULL;
+
+    // start the new network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_BDD );
+    // make sure the new manager has enough inputs
+    Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 );
+    // put the results into the new network (save new CO drivers in old CO drivers)
+    Abc_NtkDsdConstruct( pManDsd, pNtk, pNtkNew );
+    // finalize the new network
+    Abc_NtkFinalize( pNtk, pNtkNew );
+
+    if ( fPrint )
+    Dsd_TreePrint( stdout, pManDsd, (char **)pNtk->vNamesPi->pArray, (char **)pNtk->vNamesPo->pArray, fShort, -1 );
+
+    // stop the DSD manager
+    Dsd_ManagerStop( pManDsd );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DSD by creating the manager and decomposing the functions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dsd_Manager_t * Abc_NtkDsdPerform( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose )
+{
+    Dsd_Manager_t * pManDsd;
+    DdNode ** pbFuncsGlo;
+    Abc_Obj_t * pNode;
+    int i;
+
+    // collect global functions into the array
+    pbFuncsGlo = ALLOC( DdNode *, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        pbFuncsGlo[i] = Cudd_NotCond( pNode->pNext, Abc_ObjFaninC0(pNode) );
+//printf( "Output %3d : Support size = %3d. Nodes = %5d.\n", i, Cudd_SupportSize(dd, pbFuncsGlo[i]), Cudd_DagSize(pbFuncsGlo[i]) );
+    }
+
+    // start the DSD manager and decompose global functions
+    pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose );
+    Dsd_Decompose( pManDsd, pbFuncsGlo, Abc_NtkCoNum(pNtk) );
+    FREE( pbFuncsGlo );
+    return pManDsd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
+{
+    Dsd_Node_t ** ppNodesDsd;
+    Dsd_Node_t * pNodeDsd;
+    Abc_Obj_t * pNode, * pNodeNew, * pDriver, * pConst1;
+    int i, nNodesDsd;
+
+    // save the CI nodes in the DSD nodes
+    Abc_NtkForEachCi( pNtk, pNode, i )
+    {
+        pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
+        Dsd_NodeSetMark( pNodeDsd, (int)pNode->pCopy );
+    }
+    // set the constant node
+    pConst1 = Abc_AigConst1(pNtk->pManFunc);
+    if ( Abc_ObjFanoutNum(pConst1) > 0 )
+        pConst1->pCopy = Abc_NodeCreateConst1(pNtkNew);
+
+    // collect DSD nodes in DFS order (leaves and const1 are not collected)
+    ppNodesDsd = Dsd_TreeCollectNodesDfs( pManDsd, &nNodesDsd );
+    for ( i = 0; i < nNodesDsd; i++ )
+        Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNtkNew );
+    free( ppNodesDsd );
+
+    // set the pointers to the CO drivers
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        pDriver = Abc_ObjFanin0( pNode );
+        if ( !Abc_ObjIsNode(pDriver) )
+            continue;
+        pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i );
+        pNodeNew = (Abc_Obj_t *)Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) );
+        assert( !Abc_ObjIsComplement(pNodeNew) );
+        pDriver->pCopy = Abc_ObjNotCond( pNodeNew, Dsd_IsComplement(pNodeDsd) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DSD using the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew )
+{
+    DdManager * ddDsd = Dsd_ManagerReadDd( pManDsd );
+    DdManager * ddNew = pNtkNew->pManFunc;
+    Dsd_Node_t * pFaninDsd;
+    Abc_Obj_t * pNodeNew, * pFanin;
+    DdNode * bLocal, * bTemp, * bVar;
+    Dsd_Type_t Type;
+    int i, nDecs;
+
+    // create the new node
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    // add the fanins
+    Type  = Dsd_NodeReadType( pNodeDsd );
+    nDecs = Dsd_NodeReadDecsNum( pNodeDsd );
+    assert( nDecs > 1 );
+    for ( i = 0; i < nDecs; i++ )
+    {
+        pFaninDsd  = Dsd_NodeReadDec( pNodeDsd, i );
+        pFanin     = (Abc_Obj_t *)Dsd_NodeReadMark(Dsd_Regular(pFaninDsd));
+        Abc_ObjAddFanin( pNodeNew, pFanin );
+        assert( Type == DSD_NODE_OR || !Dsd_IsComplement(pFaninDsd) );
+    }
+
+    // create the local function depending on the type of the node
+    ddNew = pNtkNew->pManFunc;
+    switch ( Type )
+    {
+        case DSD_NODE_CONST1:
+        {
+            bLocal = ddNew->one; Cudd_Ref( bLocal );
+            break;
+        }
+        case DSD_NODE_OR:
+        {
+            bLocal = Cudd_Not(ddNew->one); Cudd_Ref( bLocal );
+            for ( i = 0; i < nDecs; i++ )
+            {
+                pFaninDsd  = Dsd_NodeReadDec( pNodeDsd, i );
+                bVar   = Cudd_NotCond( ddNew->vars[i], Dsd_IsComplement(pFaninDsd) );
+                bLocal = Cudd_bddOr( ddNew, bTemp = bLocal, bVar );               Cudd_Ref( bLocal );
+                Cudd_RecursiveDeref( ddNew, bTemp );
+            }
+            break;
+        }
+        case DSD_NODE_EXOR:
+        {
+            bLocal = Cudd_Not(ddNew->one); Cudd_Ref( bLocal );
+            for ( i = 0; i < nDecs; i++ )
+            {
+                bLocal = Cudd_bddXor( ddNew, bTemp = bLocal, ddNew->vars[i] );    Cudd_Ref( bLocal );
+                Cudd_RecursiveDeref( ddNew, bTemp );
+            }
+            break;
+        }
+        case DSD_NODE_PRIME:
+        {
+            bLocal = Dsd_TreeGetPrimeFunction( ddDsd, pNodeDsd );                Cudd_Ref( bLocal );
+            bLocal = Extra_TransferLevelByLevel( ddDsd, ddNew, bTemp = bLocal ); Cudd_Ref( bLocal );
+            Cudd_RecursiveDeref( ddDsd, bTemp );
+            // bLocal is now in the new BDD manager
+            break;
+        }
+        default:
+        {
+            assert( 0 );
+            break;
+        }
+    }
+    pNodeNew->pData = bLocal;
+    Dsd_NodeSetMark( pNodeDsd, (int)pNodeNew );
+    return pNodeNew;
+}
+
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively decomposes internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDsdRecursive( Abc_Ntk_t * pNtk, bool fVerbose )
+{
+    int fCheck = 1;
+    Dsd_Manager_t * pManDsd;
+    DdManager * dd = pNtk->pManFunc;
+    Vec_Ptr_t * vNodes;
+    int i;
+
+    assert( Abc_NtkIsLogicBdd(pNtk) );
+
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtk );
+
+    // start the DSD manager
+    pManDsd = Dsd_ManagerStart( dd, dd->size, 0 );
+
+    // collect nodes for decomposition
+    vNodes = Abc_NtkCollectNodesForDsd( pNtk );
+    for ( i = 0; i < vNodes->nSize; i++ )
+        Abc_NodeDecompDsdAndMux( vNodes->pArray[i], vNodes, pManDsd );
+    Vec_PtrFree( vNodes );
+
+    // stop the DSD manager
+    Dsd_ManagerStop( pManDsd );
+
+    // make sure everything is okay
+    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Abc_NtkDsdRecursive: The network check has failed.\n" );
+        return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the nodes that may need decomposition.]
+
+  Description [The nodes that do not need decomposition are those
+  whose BDD has more internal nodes than the support size.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkCollectNodesForDsd( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pNode;
+    int i;
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_NodeIsForDsd(pNode) )
+            Vec_PtrPush( vNodes, pNode );
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd )
+{
+    DdManager * dd = pNode->pNtk->pManFunc;
+    Abc_Obj_t * pRoot, * pFanin, * pNode1, * pNode2, * pNodeC;
+    Dsd_Node_t ** ppNodesDsd, * pNodeDsd, * pFaninDsd;
+    int i, nNodesDsd, iVar, fCompl;
+
+    // try disjoint support decomposition
+    pNodeDsd = Dsd_DecomposeOne( pManDsd, pNode->pData );
+    fCompl   = Dsd_IsComplement( pNodeDsd );
+    pNodeDsd = Dsd_Regular( pNodeDsd );
+
+    // determine what decomposition to use   
+    if ( Dsd_NodeReadDecsNum(pNodeDsd) != Abc_ObjFaninNum(pNode) )
+    { // perform DSD
+
+        // set the inputs
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+        {
+            pFaninDsd = Dsd_ManagerReadInput( pManDsd, i );
+            Dsd_NodeSetMark( pFaninDsd, (int)pFanin );
+        }
+
+        // construct the intermediate nodes
+        ppNodesDsd = Dsd_TreeCollectNodesDfsOne( pManDsd, pNodeDsd, &nNodesDsd );
+        for ( i = 0; i < nNodesDsd; i++ )
+        {
+            pRoot = Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNode->pNtk );
+            if ( Abc_NodeIsForDsd(pRoot) )
+                Vec_PtrPush( vNodes, pRoot );
+        }
+        free( ppNodesDsd );
+
+        // remove the current fanins
+        Abc_ObjRemoveFanins( pNode );
+        // add fanin to the root
+        Abc_ObjAddFanin( pNode, pRoot );
+        // update the function to be that of buffer
+        Cudd_RecursiveDeref( dd, pNode->pData );
+        pNode->pData = Cudd_NotCond( dd->vars[0], fCompl ); Cudd_Ref( pNode->pData );
+    }
+    else // perform MUX-decomposition
+    {
+        // get the cofactoring variable
+        iVar = Abc_NodeFindMuxVar( dd, pNode->pData, Abc_ObjFaninNum(pNode) );
+        pNodeC = Abc_ObjFanin( pNode, iVar );
+
+        // get the negative cofactor
+        pNode1 = Abc_NodeClone( pNode );
+        pNode1->pData = Cudd_Cofactor( dd, pNode->pData, Cudd_Not(dd->vars[iVar]) );  Cudd_Ref( pNode1->pData );
+        Abc_NodeMinimumBase( pNode1 );
+        if ( Abc_NodeIsForDsd(pNode1) )
+            Vec_PtrPush( vNodes, pNode1 );
+
+        // get the positive cofactor
+        pNode2 = Abc_NodeClone( pNode );
+        pNode2->pData = Cudd_Cofactor( dd, pNode->pData, dd->vars[iVar] );            Cudd_Ref( pNode2->pData );
+        Abc_NodeMinimumBase( pNode2 );
+        if ( Abc_NodeIsForDsd(pNode2) )
+            Vec_PtrPush( vNodes, pNode2 );
+
+        // remove the current fanins
+        Abc_ObjRemoveFanins( pNode );
+        // add new fanins
+        Abc_ObjAddFanin( pNode, pNodeC );
+        Abc_ObjAddFanin( pNode, pNode2 );
+        Abc_ObjAddFanin( pNode, pNode1 );
+        // update the function to be that of MUX
+        Cudd_RecursiveDeref( dd, pNode->pData );
+        pNode->pData = Cudd_bddIte( dd, dd->vars[0], dd->vars[1], dd->vars[2] );    Cudd_Ref( pNode->pData );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of one node.]
 
   Description []
                
@@ -39,7 +464,64 @@
   SeeAlso     []
 
 ***********************************************************************/
+bool Abc_NodeIsForDsd( Abc_Obj_t * pNode )
+{
+    assert( Abc_ObjIsNode(pNode) );
+    if ( Cudd_DagSize(pNode->pData)-1 > Abc_ObjFaninNum(pNode) )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determines a cofactoring variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int nVars )
+{
+    DdNode * bVar, * bCof0, * bCof1;
+    int SuppSumMin = 1000000;
+    int i, nSSD, nSSQ, iVar;
+
+//    printf( "\n\nCofactors:\n\n" );
+    iVar = -1;
+    for ( i = 0; i < nVars; i++ )
+    {
+        bVar = dd->vars[i];
+
+        bCof0 = Cudd_Cofactor( dd, bFunc, Cudd_Not(bVar) );  Cudd_Ref( bCof0 );
+        bCof1 = Cudd_Cofactor( dd, bFunc,          bVar  );  Cudd_Ref( bCof1 );
+
+//        nodD = Cudd_DagSize(bCof0);
+//        nodQ = Cudd_DagSize(bCof1);
+//        printf( "+%02d: D=%2d. Q=%2d.  ", i, nodD, nodQ );
+//        printf( "S=%2d. D=%2d.  ", nodD + nodQ, abs(nodD-nodQ) );
+
+        nSSD = Cudd_SupportSize( dd, bCof0 );
+        nSSQ = Cudd_SupportSize( dd, bCof1 );
+
+//        printf( "SD=%2d. SQ=%2d.  ", nSSD, nSSQ );
+//        printf( "S=%2d. D=%2d.  ", nSSD + nSSQ, abs(nSSD - nSSQ) );
+//        printf( "Cost=%3d. ", Cost(nodD,nodQ,nSSD,nSSQ) );
+//        printf( "\n" );
+
+        Cudd_RecursiveDeref( dd, bCof0 );
+        Cudd_RecursiveDeref( dd, bCof1 );
 
+        if ( SuppSumMin > nSSD + nSSQ )
+        {
+             SuppSumMin = nSSD + nSSQ;
+             iVar = i;
+        }
+    }
+    return iVar;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index 51fc73ce..866c6e5d 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -85,6 +85,32 @@ void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
     }
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Destroys fanout/fanin relationship between the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjRemoveFanins( Abc_Obj_t * pObj )
+{
+    Vec_Fan_t * vFaninsOld;
+    Abc_Obj_t * pFanin;
+    int k;
+    // remove old fanins
+    vFaninsOld = &pObj->vFanins;
+    for ( k = vFaninsOld->nSize - 1; k >= 0; k-- )
+    {
+        pFanin = Abc_NtkObj( pObj->pNtk, vFaninsOld->pArray[k].iFan );
+        Abc_ObjDeleteFanin( pObj, pFanin );
+    }
+}
+
 /**Function*************************************************************
 
   Synopsis    [Replaces a fanin of the node.]
diff --git a/src/base/abc/abcFraig.c b/src/base/abc/abcFraig.c
index 85dba6f3..75c5c290 100644
--- a/src/base/abc/abcFraig.c
+++ b/src/base/abc/abcFraig.c
@@ -435,7 +435,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
     if ( pStore == NULL )
     {
         // start the stored network
-        pStore = Abc_NtkStrash( pNtk );
+        pStore = Abc_NtkStrash( pNtk, 0 );
         if ( pStore == NULL )
         {
             printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 59f0dc34..a040758e 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -166,7 +166,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk )
         assert( pNode->pData );
         bFunc = pNode->pData;
 //Extra_bddPrint( dd, bFunc ); printf( "\n" ); printf( "\n" );
-        pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, Abc_ObjFaninNum(pNode), vCube, -1 );
+        pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, -1 );
         if ( pNode->pData == NULL )
             return 0;
         Cudd_RecursiveDeref( dd, bFunc );
@@ -193,18 +193,20 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFunc, int nFanins, Vec_Str_t * vCube, int fMode )
+char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode )
 {
+    int fVerify = 1;
     char * pSop;
     DdNode * bFuncNew, * bCover, * zCover, * zCover0, * zCover1;
     int nCubes, nCubes0, nCubes1, fPhase;
 
-    if ( Cudd_IsConstant(bFunc) )
+    assert( bFuncOn == bFuncOnDc || Cudd_bddLeq( dd, bFuncOn, bFuncOnDc ) );
+    if ( Cudd_IsConstant(bFuncOn) || Cudd_IsConstant(bFuncOnDc) )
     {
         Vec_StrFill( vCube, nFanins, '-' );
         Vec_StrPush( vCube, '\0' );
         pSop = Extra_MmFlexEntryFetch( pMan, nFanins + 4 );
-        if ( bFunc == Cudd_ReadLogicZero(dd) )
+        if ( bFuncOn == Cudd_ReadLogicZero(dd) )
             sprintf( pSop, "%s 0\n", vCube->pArray );
         else
             sprintf( pSop, "%s 1\n", vCube->pArray );
@@ -216,14 +218,14 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
     { // try both phases
 
         // get the ZDD of the negative polarity
-        bCover = Cudd_zddIsop( dd, Cudd_Not(bFunc), Cudd_Not(bFunc), &zCover0 );
+        bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover0 );
         Cudd_Ref( zCover0 );
         Cudd_Ref( bCover );
         Cudd_RecursiveDeref( dd, bCover );
         nCubes0 = Abc_CountZddCubes( dd, zCover0 );
 
         // get the ZDD of the positive polarity
-        bCover = Cudd_zddIsop( dd, bFunc, bFunc, &zCover1 );
+        bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover1 );
         Cudd_Ref( zCover1 );
         Cudd_Ref( bCover );
         Cudd_RecursiveDeref( dd, bCover );
@@ -248,7 +250,7 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
     else if ( fMode == 0 )
     {
         // get the ZDD of the positive polarity
-        bCover = Cudd_zddIsop( dd, Cudd_Not(bFunc), Cudd_Not(bFunc), &zCover );
+        bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover );
         Cudd_Ref( zCover );
         Cudd_Ref( bCover );
         Cudd_RecursiveDeref( dd, bCover );
@@ -258,7 +260,7 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
     else if ( fMode == 1 )
     {
         // get the ZDD of the positive polarity
-        bCover = Cudd_zddIsop( dd, bFunc, bFunc, &zCover );
+        bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover );
         Cudd_Ref( zCover );
         Cudd_Ref( bCover );
         Cudd_RecursiveDeref( dd, bCover );
@@ -271,7 +273,10 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
     }
 
     // allocate memory for the cover
-    pSop = Extra_MmFlexEntryFetch( pMan, (nFanins + 3) * nCubes + 1 );
+    if ( pMan )
+        pSop = Extra_MmFlexEntryFetch( pMan, (nFanins + 3) * nCubes + 1 );
+    else 
+        pSop = ALLOC( char, (nFanins + 3) * nCubes + 1 );
     pSop[(nFanins + 3) * nCubes] = 0;
     // create the SOP
     Vec_StrFill( vCube, nFanins, '-' );
@@ -280,12 +285,21 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
     Cudd_RecursiveDerefZdd( dd, zCover );
 
     // verify
-    bFuncNew = Abc_ConvertSopToBdd( dd, pSop, nFanins );  Cudd_Ref( bFuncNew );
-//Extra_bddPrint( dd, bFunc );
-//Extra_bddPrint( dd, bFuncNew );
-    if ( bFuncNew != bFunc )
-        printf( "Verification failed.\n" );
-    Cudd_RecursiveDeref( dd, bFuncNew );
+    if ( fVerify )
+    {
+        bFuncNew = Abc_ConvertSopToBdd( dd, pSop, nFanins );  Cudd_Ref( bFuncNew );
+        if ( bFuncOn == bFuncOnDc )
+        {
+            if ( bFuncNew != bFuncOn )
+                printf( "Verification failed.\n" );
+        }
+        else
+        {
+            if ( !Cudd_bddLeq(dd, bFuncOn, bFuncNew) || !Cudd_bddLeq(dd, bFuncNew, bFuncOnDc) )
+                printf( "Verification failed.\n" );
+        }
+        Cudd_RecursiveDeref( dd, bFuncNew );
+    }
     return pSop;
 }
 
@@ -359,8 +373,8 @@ int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFani
 void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 )
 {
     assert( Abc_NtkIsLogicBdd(pNode->pNtk) ); 
-    *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 0 );
-    *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 1 );
+    *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 0 );
+    *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 1 );
 }
 
 
diff --git a/src/base/abc/abcFxu.c b/src/base/abc/abcFxu.c
index 99f37dfc..bbfef208 100644
--- a/src/base/abc/abcFxu.c
+++ b/src/base/abc/abcFxu.c
@@ -52,6 +52,8 @@ static void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p );
 ***********************************************************************/
 bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
 {
+    int fCheck = 1;
+
     assert( Abc_NtkIsLogicBdd(pNtk) || Abc_NtkIsLogicSop(pNtk) );
     // convert nodes to SOPs
     if ( Abc_NtkIsLogicBdd(pNtk) )
@@ -70,20 +72,19 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
     // sweep removes useless nodes
     Abc_NtkCleanup( pNtk, 0 );
     // collect information about the covers
-    // make sure all covers are SCC free
-    // allocate literal array for each cover
     Abc_NtkFxuCollectInfo( pNtk, p );
     // call the fast extract procedure
-    // returns the number of divisor extracted
     if ( Fxu_FastExtract(p) > 0 )
     {
         // update the network
         Abc_NtkFxuReconstruct( pNtk, p );
         // make sure everything is okay
-        if ( !Abc_NtkCheck( pNtk ) )
+        if ( fCheck && !Abc_NtkCheck( pNtk ) )
             printf( "Abc_NtkFastExtract: The network check has failed.\n" );
         return 1;
     }
+    else
+        printf( "Warning: The network has not been changed by \"fx\".\n" );
     return 0;
 }
 
@@ -199,7 +200,6 @@ void Abc_NtkFxuFreeInfo( Fxu_Data_t * p )
 ***********************************************************************/
 void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
 {
-    Vec_Fan_t * vFaninsOld;
     Vec_Int_t * vFanins;
     Abc_Obj_t * pNode, * pFanin;
     int i, k;
@@ -221,12 +221,7 @@ void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
             continue;
         // remove old fanins
         pNode = Abc_NtkObj( pNtk, i );
-        vFaninsOld = &pNode->vFanins;
-        for ( k = vFaninsOld->nSize - 1; k >= 0; k-- )
-        {
-            pFanin = Abc_NtkObj( pNtk, vFaninsOld->pArray[k].iFan );
-            Abc_ObjDeleteFanin( pNode, pFanin );
-        }
+        Abc_ObjRemoveFanins( pNode );
         // add new fanins
         vFanins = p->vFaninsNew->pArray[i];
         for ( k = 0; k < vFanins->nSize; k++ )
diff --git a/src/base/abc/abcMap.c b/src/base/abc/abcMap.c
index 7289b47b..e5f4e104 100644
--- a/src/base/abc/abcMap.c
+++ b/src/base/abc/abcMap.c
@@ -353,7 +353,7 @@ Abc_Obj_t * Abc_NodeFromMapSuper_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap
         }
         else
         {  
-            assert( 0 );
+//            assert( 0 );
             /* It might happen that a super gate with 5 inputs is constructed that
              * actually depends only on the first four variables; i.e the fifth is a
              * don't care -- in that case we connect constant node for the fifth
diff --git a/src/base/abc/abcMiter.c b/src/base/abc/abcMiter.c
index f1037dd2..f72fab0f 100644
--- a/src/base/abc/abcMiter.c
+++ b/src/base/abc/abcMiter.c
@@ -51,8 +51,8 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
     Abc_Ntk_t * pTemp = NULL;
     int fRemove1, fRemove2;
     // make sure the circuits are strashed 
-    fRemove1 = (!Abc_NtkIsAig(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1));
-    fRemove2 = (!Abc_NtkIsAig(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2));
+    fRemove1 = (!Abc_NtkIsAig(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0));
+    fRemove2 = (!Abc_NtkIsAig(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0));
     if ( pNtk1 && pNtk2 )
     {
         // check that the networks have the same PIs/POs/latches
diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c
index 49b6db72..c3e3107c 100644
--- a/src/base/abc/abcPrint.c
+++ b/src/base/abc/abcPrint.c
@@ -52,7 +52,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk )
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
     }
     else if ( Abc_NtkIsAig(pNtk) )
+    {
         fprintf( pFile, "  and = %5d", Abc_NtkNodeNum(pNtk) );
+        fprintf( pFile, "  choice = %5d", Abc_NtkCountChoiceNodes(pNtk) );
+    }
     else 
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
 
@@ -86,19 +89,19 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk )
 ***********************************************************************/
 void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk )
 {
-    Abc_Obj_t * pNet, * pLatch;
+    Abc_Obj_t * pObj, * pLatch;
     int i;
 
     if ( Abc_NtkIsNetlist(pNtk) )
     {
         fprintf( pFile, "Primary inputs (%d): ", Abc_NtkPiNum(pNtk) );    
-        Abc_NtkForEachPi( pNtk, pNet, i )
-            fprintf( pFile, " %s", Abc_ObjName(pNet) );
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            fprintf( pFile, " %s", Abc_ObjName(pObj) );
         fprintf( pFile, "\n" );   
     
         fprintf( pFile, "Primary outputs (%d):", Abc_NtkPoNum(pNtk) );    
-        Abc_NtkForEachPo( pNtk, pNet, i )
-            fprintf( pFile, " %s", Abc_ObjName(pNet) );
+        Abc_NtkForEachPo( pNtk, pObj, i )
+            fprintf( pFile, " %s", Abc_ObjName(pObj) );
         fprintf( pFile, "\n" );    
   
         fprintf( pFile, "Latches (%d):  ", Abc_NtkLatchNum(pNtk) );  
@@ -109,12 +112,12 @@ void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk )
     else
     {
         fprintf( pFile, "Primary inputs (%d): ", Abc_NtkPiNum(pNtk) );    
-        Abc_NtkForEachPi( pNtk, pNet, i )
+        Abc_NtkForEachPi( pNtk, pObj, i )
             fprintf( pFile, " %s", pNtk->vNamesPi->pArray[i] );
         fprintf( pFile, "\n" );   
     
         fprintf( pFile, "Primary outputs (%d):", Abc_NtkPoNum(pNtk) );    
-        Abc_NtkForEachPo( pNtk, pNet, i )
+        Abc_NtkForEachPo( pNtk, pObj, i )
             fprintf( pFile, " %s", pNtk->vNamesPo->pArray[i] );
         fprintf( pFile, "\n" );    
   
@@ -280,7 +283,6 @@ void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode )
     Vec_IntFree( vFactor );
 }
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcRes.c b/src/base/abc/abcRes.c
new file mode 100644
index 00000000..658c8229
--- /dev/null
+++ b/src/base/abc/abcRes.c
@@ -0,0 +1,537 @@
+/**CFile****************************************************************
+
+  FileName    [abcRes.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Technology-independent resynthesis of the AIG.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcRes.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "ft.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+static void        Abc_NodeResyn( Abc_ManRes_t * p );
+
+static void        Abc_NodeFindCut( Abc_ManRes_t * p );
+static int         Abc_NodeFindCut_int( Vec_Ptr_t * vInside, Vec_Ptr_t * vFanins, int nSizeLimit );
+static int         Abc_NodeGetFaninCost( Abc_Obj_t * pNode );
+static void        Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited );
+static void        Abc_NodeConeMark( Vec_Ptr_t * vVisited );
+static void        Abc_NodeConeUnmark( Vec_Ptr_t * vVisited );
+
+static Vec_Int_t * Abc_NodeRefactor( Abc_ManRes_t * p );
+static DdNode *    Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited );
+
+static int         Abc_NodeDecide( Abc_ManRes_t * p );
+static void        Abc_NodeUpdate( Abc_ManRes_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs incremental resynthesis of the AIG.]
+
+  Description [Starting from each node, computes a reconvergence-driven cut, 
+  derives BDD of the cut function, constructs ISOP, factors the cover, 
+  and replaces the current implementation of the MFFC of the cut by the 
+  new factored form if the number of AIG nodes is reduced. Returns the
+  number of AIG nodes saved.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkAigResynthesize( Abc_Ntk_t * pNtk, Abc_ManRes_t * p )
+{
+    int fCheck = 1;
+    ProgressBar * pProgress;
+    Abc_Obj_t * pNode;
+    int i, Counter, Approx;
+
+    assert( Abc_NtkIsAig(pNtk) );
+
+    // start the BDD manager
+    p->dd = Cudd_Init( p->nNodeSizeMax + p->nConeSizeMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_zddVarsFromBddVars( p->dd, 2 );
+    p->bCubeX = Extra_bddComputeRangeCube( p->dd, p->nNodeSizeMax, p->dd->size );   Cudd_Ref( p->bCubeX );
+
+    // remember the number of nodes
+    Counter = Abc_NtkNodeNum( pNtk );
+    // resynthesize each node
+    pProgress = Extra_ProgressBarStart( stdout, 100 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Approx = (int)(100.0 * i / pNtk->vObjs->nSize );
+        Extra_ProgressBarUpdate( pProgress, Approx, NULL );
+        p->pNode = pNode;
+        Abc_NodeResyn( p );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Abc_NtkManResStop( p );
+
+    // check
+    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Abc_NtkAigResynthesize: The network check has failed.\n" );
+        return -1;
+    }
+    return Abc_NtkNodeNum(pNtk) - Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs resynthesis of one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeResyn( Abc_ManRes_t * p )
+{
+    int RetValue;
+    int clk;
+
+    assert( Abc_ObjIsNode(p->pNode) );
+
+clk = clock();
+    // detect the cut
+    Abc_NodeFindCut( p );
+p->time1 += clock() - clk;
+
+    // refactor the cut
+clk = clock();
+    p->vForm = Abc_NodeRefactor( p );
+p->time2 += clock() - clk;
+
+    // accept or reject the factored form
+clk = clock();
+    RetValue = Abc_NodeDecide( p );
+p->time3 += clock() - clk;
+
+    // modify the network
+clk = clock();
+    if ( RetValue )
+        Abc_NodeUpdate( p );
+p->time4 += clock() - clk;
+
+    // cleanup
+    Vec_IntFree( p->vForm );
+    p->vForm = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds a reconvergence-driven cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeFindCut( Abc_ManRes_t * p )
+{
+    Abc_Obj_t * pNode = p->pNode;
+    int i;
+
+    // mark TFI using fMarkA
+    Vec_PtrClear( p->vVisited );
+    Abc_NodeConeMarkCollect_rec( pNode, p->vVisited );
+
+    // start the reconvergence-driven node
+    Vec_PtrClear( p->vInsideNode );
+    Vec_PtrClear( p->vFaninsNode );
+    Vec_PtrPush( p->vFaninsNode, pNode );
+    pNode->fMarkB = 1;
+
+    // compute reconvergence-driven node
+    while ( Abc_NodeFindCut_int( p->vInsideNode, p->vFaninsNode, p->nNodeSizeMax ) );
+
+    // compute reconvergence-driven cone
+    Vec_PtrClear( p->vInsideCone );
+    Vec_PtrClear( p->vFaninsCone );
+    if ( p->nConeSizeMax > p->nNodeSizeMax )
+    {
+        // copy the node into the cone
+        Vec_PtrForEachEntry( p->vInsideNode, pNode, i )
+            Vec_PtrPush( p->vInsideCone, pNode );
+        Vec_PtrForEachEntry( p->vFaninsNode, pNode, i )
+            Vec_PtrPush( p->vFaninsCone, pNode );
+        // compute reconvergence-driven cone
+        while ( Abc_NodeFindCut_int( p->vInsideCone, p->vFaninsCone, p->nConeSizeMax ) );
+        // unmark the nodes of the sets
+        Vec_PtrForEachEntry( p->vInsideCone, pNode, i )
+            pNode->fMarkB = 0;
+        Vec_PtrForEachEntry( p->vFaninsCone, pNode, i )
+            pNode->fMarkB = 0;
+    }
+    else
+    {
+        // unmark the nodes of the sets
+        Vec_PtrForEachEntry( p->vInsideNode, pNode, i )
+            pNode->fMarkB = 0;
+        Vec_PtrForEachEntry( p->vFaninsNode, pNode, i )
+            pNode->fMarkB = 0;
+    }
+
+    // unmark TFI using fMarkA
+    Abc_NodeConeUnmark( p->vVisited );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds a reconvergence-driven cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeFindCut_int( Vec_Ptr_t * vInside, Vec_Ptr_t * vFanins, int nSizeLimit )
+{
+    Abc_Obj_t * pNode, * pFaninBest, * pNext;
+    int CostBest, CostCur, i;
+    // find the best fanin
+    CostBest   = 100;
+    pFaninBest = NULL;
+    Vec_PtrForEachEntry( vFanins, pNode, i )
+    {
+        CostCur = Abc_NodeGetFaninCost( pNode );
+        if ( CostBest > CostCur )
+        {
+            CostBest   = CostCur;
+            pFaninBest = pNode;
+        }
+    }
+    if ( pFaninBest == NULL )
+        return 0;
+    assert( CostBest < 3 );
+    if ( vFanins->nSize - 1 + CostBest > nSizeLimit )
+        return 0;
+    assert( Abc_ObjIsNode(pFaninBest) );
+    // remove the node from the array
+    Vec_PtrRemove( vFanins, pFaninBest );
+    // add the node to the set
+    Vec_PtrPush( vInside, pFaninBest );
+    // add the left child to the fanins
+    pNext = Abc_ObjFanin0(pFaninBest);
+    if ( !pNext->fMarkB )
+    {
+        pNext->fMarkB = 1;
+        Vec_PtrPush( vFanins, pNext );
+    }
+    // add the right child to the fanins
+    pNext = Abc_ObjFanin1(pFaninBest);
+    if ( !pNext->fMarkB )
+    {
+        pNext->fMarkB = 1;
+        Vec_PtrPush( vFanins, pNext );
+    }
+    assert( vFanins->nSize <= nSizeLimit );
+    // keep doing this
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluate the fanin cost.]
+
+  Description [Returns the number of fanins that will be brought in.
+  Returns large number if the node cannot be added.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeGetFaninCost( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    assert( pNode->fMarkA == 1 );  // this node is in the TFI
+    assert( pNode->fMarkB == 1 );  // this node is in the constructed cone
+    // check the PI node
+    if ( !Abc_ObjIsNode(pNode) )
+        return 999;
+    // check the fanouts
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+        if ( pFanout->fMarkA && pFanout->fMarkB == 0 ) // in the cone but not in the set
+            return 999;
+    // the fanouts are in the TFI and inside the constructed cone
+    // return the number of fanins that will be on the boundary if this node is added
+    return (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
+{
+    if ( pNode->fMarkA == 1 )
+        return;
+    // visit transitive fanin 
+    if ( Abc_ObjIsNode(pNode) )
+    {
+        Abc_NodeConeMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited );
+        Abc_NodeConeMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited );
+    }
+    assert( pNode->fMarkA == 0 );
+    pNode->fMarkA = 1;
+    Vec_PtrPush( vVisited, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeConeMark( Vec_Ptr_t * vVisited )
+{
+    int i;
+    for ( i = 0; i < vVisited->nSize; i++ )
+        ((Abc_Obj_t *)vVisited->pArray)->fMarkA = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeConeUnmark( Vec_Ptr_t * vVisited )
+{
+    int i;
+    for ( i = 0; i < vVisited->nSize; i++ )
+        ((Abc_Obj_t *)vVisited->pArray)->fMarkA = 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the factored form of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NodeRefactor( Abc_ManRes_t * p )
+{
+    Vec_Int_t * vForm;
+    DdManager * dd = p->dd;
+    DdNode * bFuncNode, * bFuncCone, * bCare, * bFuncOn, * bFuncOnDc;
+    char * pSop;
+    int nFanins;
+
+    assert( p->vFaninsNode->nSize < p->nNodeSizeMax );
+    assert( p->vFaninsCone->nSize < p->nConeSizeMax );
+
+    // get the function of the node
+    bFuncNode = Abc_NodeConeBdd( dd, p->dd->vars, p->pNode, p->vFaninsNode, p->vVisited );  
+    Cudd_Ref( bFuncNode );
+    nFanins = p->vFaninsNode->nSize;
+    if ( p->nConeSizeMax > p->nNodeSizeMax )
+    {
+        // get the function of the cone
+        bFuncCone = Abc_NodeConeBdd( dd, p->dd->vars + p->nNodeSizeMax, p->pNode, p->vFaninsCone, p->vVisited );  
+        Cudd_Ref( bFuncCone );
+        // get the care set
+        bCare = Cudd_bddXorExistAbstract( p->dd, Cudd_Not(bFuncNode), bFuncCone, p->bCubeX );   Cudd_Ref( bCare );
+        Cudd_RecursiveDeref( dd, bFuncCone );
+        // compute the on-set and off-set of the function of the node
+        bFuncOn   = Cudd_bddAnd( dd, bFuncNode, bCare );                Cudd_Ref( bFuncOn );
+        bFuncOnDc = Cudd_bddAnd( dd, Cudd_Not(bFuncNode), bCare );      Cudd_Ref( bFuncOnDc );
+        bFuncOnDc = Cudd_Not( bFuncOnDc );
+        Cudd_RecursiveDeref( dd, bCare );
+        // get the cover
+        pSop = Abc_ConvertBddToSop( NULL, dd, bFuncOn, bFuncOnDc, nFanins, p->vCube, -1 );
+        Cudd_RecursiveDeref( dd, bFuncOn );
+        Cudd_RecursiveDeref( dd, bFuncOnDc );
+    }
+    else
+    {
+        // get the cover
+        pSop = Abc_ConvertBddToSop( NULL, dd, bFuncNode, bFuncNode, nFanins, p->vCube, -1 );
+    }
+    Cudd_RecursiveDeref( dd, bFuncNode );
+    // derive the factored form
+    vForm = Ft_Factor( pSop );
+    free( pSop );
+    return vForm;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns BDD representing the logic function of the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited )
+{
+    DdNode * bFunc0, * bFunc1, * bFunc;
+    int i;
+    // mark the fanins of the cone
+    Abc_NodeConeMark( vFanins );
+    // collect the nodes in the DFS order
+    Vec_PtrClear( vVisited );
+    Abc_NodeConeMarkCollect_rec( pNode, vVisited );
+    // unmark both sets
+    Abc_NodeConeUnmark( vFanins );
+    Abc_NodeConeUnmark( vVisited );
+    // set the elementary BDDs
+    Vec_PtrForEachEntry( vFanins, pNode, i )
+        pNode->pCopy = (Abc_Obj_t *)pbVars[i];
+    // compute the BDDs for the collected nodes
+    Vec_PtrForEachEntry( vVisited, pNode, i )
+    {
+        bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
+        bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) );
+        bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );    Cudd_Ref( bFunc );
+        pNode->pCopy = (Abc_Obj_t *)bFunc;
+    }
+    Cudd_Ref( bFunc );
+    // dereference the intermediate ones
+    Vec_PtrForEachEntry( vVisited, pNode, i )
+        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Decides whether to accept the given factored form.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int  Abc_NodeDecide( Abc_ManRes_t * p )
+{
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces MFFC of the node by the new factored.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeUpdate( Abc_ManRes_t * p )
+{
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_ManRes_t * Abc_NtkManResStart()
+{
+    Abc_ManRes_t * p;
+    p = ALLOC( Abc_ManRes_t, 1 );
+    p->vFaninsNode = Vec_PtrAlloc( 100 );
+    p->vInsideNode = Vec_PtrAlloc( 100 );
+    p->vFaninsCone = Vec_PtrAlloc( 100 );
+    p->vInsideCone = Vec_PtrAlloc( 100 );
+    p->vVisited    = Vec_PtrAlloc( 100 );
+    p->vCube       = Vec_StrAlloc( 100 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkManResStop( Abc_ManRes_t * p )
+{
+    if ( p->bCubeX ) Cudd_RecursiveDeref( p->dd, p->bCubeX );
+    if ( p->dd )     Extra_StopManager( p->dd );
+    Vec_PtrFree( p->vFaninsNode );
+    Vec_PtrFree( p->vInsideNode );
+    Vec_PtrFree( p->vFaninsCone );
+    Vec_PtrFree( p->vInsideCone );
+    Vec_PtrFree( p->vVisited    );
+    Vec_StrFree( p->vCube       );
+    free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
new file mode 100644
index 00000000..2ddd2a79
--- /dev/null
+++ b/src/base/abc/abcShow.c
@@ -0,0 +1,167 @@
+/**CFile****************************************************************
+
+  FileName    [abcShow.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Visualization procedures using DOT software and GSView.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcShow.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#ifdef WIN32
+#include "process.h" 
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the factored form of one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodePrintBdd( Abc_Obj_t * pNode )
+{
+    FILE * pFile;
+    Vec_Ptr_t * vNamesIn;
+    char * FileNameIn;
+    char * FileNameOut;
+    char * FileGeneric;
+    char * pCur, * pNameOut;
+    char FileNameDot[200];
+    char FileNamePs[200];
+    char CommandDot[1000];
+#ifndef WIN32
+    char CommandPs[1000];
+#endif
+    char * pProgDotName;
+    char * pProgGsViewName;
+    int RetValue;
+
+    assert( Abc_NtkIsLogicBdd(pNode->pNtk) );
+
+#ifdef WIN32
+    pProgDotName = "dot.exe";
+    pProgGsViewName = NULL;
+#else
+    pProgDotName = "dot";
+    pProgGsViewName = "gv";
+#endif
+
+    FileNameIn  = NULL;
+    FileNameOut = NULL;
+
+    // get the generic file name
+    pNode->pCopy = NULL;
+    FileGeneric = Abc_ObjName(pNode);
+    // get rid of not-alpha-numeric characters
+    for ( pCur = FileGeneric; *pCur; pCur++ )
+        if ( !((*pCur >= '0' && *pCur <= '9') || (*pCur >= 'a' && *pCur <= 'z') || (*pCur >= 'A' && *pCur <= 'Z')) )
+            *pCur = '_';
+    // create the file names
+    sprintf( FileNameDot, "%s.dot", FileGeneric ); 
+    sprintf( FileNamePs,  "%s.ps",  FileGeneric ); 
+
+    // write the DOT file
+    if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+        return;
+    }
+    // set the node names 
+    Abc_NtkLogicTransferNames( pNode->pNtk );
+    vNamesIn = Abc_NodeGetFaninNames( pNode );
+    pNameOut = Abc_ObjName(pNode);
+    Cudd_DumpDot( pNode->pNtk->pManFunc, 1, (DdNode **)&pNode->pData, (char **)vNamesIn->pArray, &pNameOut, pFile );
+    Abc_NodeFreeFaninNames( vNamesIn );
+    Abc_NtkCleanCopy( pNode->pNtk );
+    fclose( pFile );
+
+    // check that the input file is okay
+    if ( (pFile = fopen( FileNameDot, "r" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+        return;
+    }
+    fclose( pFile );
+
+    // generate the DOT file
+    sprintf( CommandDot,  "%s -Tps -o %s %s", pProgDotName, FileNamePs, FileNameDot ); 
+    RetValue = system( CommandDot );
+#ifdef WIN32
+        _unlink( FileNameDot );
+#else
+        unlink( FileNameDot );
+#endif
+    if ( RetValue == -1 )
+    {
+        fprintf( stdout, "Cannot find \"%s\".\n", pProgDotName );
+        return;
+    }
+
+    // check that the input file is okay
+    if ( (pFile = fopen( FileNamePs, "r" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open intermediate file \"%s\".\n", FileNamePs );
+        return;
+    }
+    fclose( pFile ); 
+
+#ifdef WIN32
+    if ( _spawnl( _P_NOWAIT, "gsview32.exe", "gsview32.exe", FileNamePs, NULL ) == -1 )
+        if ( _spawnl( _P_NOWAIT, "C:\\Program Files\\Ghostgum\\gsview\\gsview32.exe", 
+            "C:\\Program Files\\Ghostgum\\gsview\\gsview32.exe", FileNamePs, NULL ) == -1 )
+        {
+            fprintf( stdout, "Cannot find \"%s\".\n", "gsview32.exe" );
+            return;
+        }
+#else
+    sprintf( CommandPs,  "%s %s &", pProgGsViewName, FileNamePs ); 
+    if ( system( CommandPs ) == -1 )
+    {
+        fprintf( stdout, "Cannot execute \"%s\".\n", FileNamePs );
+        return;
+    }
+#endif
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c
index fcfeefda..bf494767 100644
--- a/src/base/abc/abcStrash.c
+++ b/src/base/abc/abcStrash.c
@@ -27,7 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 // static functions
-static void        Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig );
+static void        Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fAllNodes );
 static Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
 static Abc_Obj_t * Abc_NodeStrashSop( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop );
 static Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop );
@@ -53,7 +53,7 @@ extern char *      Mio_GateReadSop( void * pGate );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes )
 {
     int fCheck = 1;
     Abc_Ntk_t * pNtkAig;
@@ -68,14 +68,14 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
     // perform strashing
     pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_AIG );
-    Abc_NtkStrashPerform( pNtk, pNtkAig );
+    Abc_NtkStrashPerform( pNtk, pNtkAig, fAllNodes );
     Abc_NtkFinalize( pNtk, pNtkAig );
     // print warning about self-feed latches
     if ( Abc_NtkCountSelfFeedLatches(pNtkAig) )
         printf( "The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) );
     // duplicate EXDC 
     if ( pNtk->pExdc )
-        pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc );
+        pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0 );
     // make sure everything is okay
     if ( fCheck && !Abc_NtkCheck( pNtkAig ) )
     {
@@ -97,7 +97,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
+void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, bool fAllNodes )
 {
     ProgressBar * pProgress;
     Abc_Aig_t * pMan = pNtkNew->pManFunc;
@@ -106,8 +106,10 @@ void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
     int i;
 
     // perform strashing
-    vNodes = Abc_NtkDfs( pNtk );
-//    vNodes = Abc_AigCollectAll( pNtk );
+    if ( fAllNodes )
+        vNodes = Abc_AigCollectAll( pNtk );
+    else
+        vNodes = Abc_NtkDfs( pNtk );
     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
     for ( i = 0; i < vNodes->nSize; i++ )
     {
@@ -255,7 +257,7 @@ Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, char * pS
     assert( vForm->nSize > nVars );
     assert( nVars == Abc_ObjFaninNum(pRoot) );
 
-    // check for constant Andtion
+    // check for constant function
     pFtNode = Ft_NodeRead( vForm, 0 );
     if ( pFtNode->fConst )
     {
@@ -268,7 +270,7 @@ Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, char * pS
     Abc_ObjForEachFanin( pRoot, pFanin, i )
         Vec_PtrPush( vAnds, pFanin->pCopy );
 
-    // compute the Andtions of other nodes
+    // compute the function of other nodes
     for ( i = nVars; i < vForm->nSize; i++ )
     {
         pFtNode = Ft_NodeRead( vForm, i );
@@ -322,7 +324,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     Abc_NtkForEachCi( pNtk2, pObj, i )
         pObj->pCopy = Abc_NtkCi(pNtk1, i); 
     // add pNtk2 to pNtk1 while strashing
-    Abc_NtkStrashPerform( pNtk2, pNtk1 );
+    Abc_NtkStrashPerform( pNtk2, pNtk1, 1 );
     // make sure that everything is okay
     if ( fCheck && !Abc_NtkCheck( pNtk1 ) )
     {
diff --git a/src/base/abc/abcSweep.c b/src/base/abc/abcSweep.c
index 6890fc57..495bf1eb 100644
--- a/src/base/abc/abcSweep.c
+++ b/src/base/abc/abcSweep.c
@@ -61,7 +61,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
     assert( !Abc_NtkIsAig(pNtk) );
 
     // derive the AIG
-    pNtkAig = Abc_NtkStrash( pNtk );
+    pNtkAig = Abc_NtkStrash( pNtk, 0 );
     // perform fraiging of the AIG
     Fraig_ParamsSetDefault( &Params );
     pMan = Abc_NtkToFraig( pNtkAig, &Params, 0 );    
diff --git a/src/base/abc/abcTiming.c b/src/base/abc/abcTiming.c
index f017d93c..861a1b14 100644
--- a/src/base/abc/abcTiming.c
+++ b/src/base/abc/abcTiming.c
@@ -228,7 +228,7 @@ void Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkTimeFinalize( Abc_Ntk_t * pNtk )
+void Abc_NtkTimeInitialize( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
     Abc_Time_t ** ppTimes, * pTime;
@@ -283,11 +283,12 @@ void Abc_NtkTimePrepare( Abc_Ntk_t * pNtk )
     if ( pNtk->pManTime == NULL )
     {
         pNtk->pManTime = Abc_ManTimeStart();
-        Abc_NtkTimeFinalize( pNtk );
+        Abc_NtkTimeInitialize( pNtk );
         return;
     }
-    // if timing manager is given, clean arrivals except for PIs
-    // and required except for POs
+    // if timing manager is given, expand it if necessary
+    Abc_ManTimeExpand( pNtk->pManTime, Abc_NtkObjNum(pNtk), 0 );
+    // clean arrivals except for PIs
     ppTimes = (Abc_Time_t **)pNtk->pManTime->vArrs->pArray;
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
@@ -299,6 +300,7 @@ void Abc_NtkTimePrepare( Abc_Ntk_t * pNtk )
         pTime = ppTimes[pObj->Id];
         pTime->Fall = pTime->Rise = pTime->Worst = -ABC_INFINITY;
     }
+    // clean required except for POs
 }
 
 
@@ -392,7 +394,7 @@ void Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Expends the storage for timing information.]
 
   Description []
                
diff --git a/src/base/abc/abcUnreach.c b/src/base/abc/abcUnreach.c
new file mode 100644
index 00000000..5d5a759b
--- /dev/null
+++ b/src/base/abc/abcUnreach.c
@@ -0,0 +1,328 @@
+/**CFile****************************************************************
+
+  FileName    [abcUnreach.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Computes unreachable states for small benchmarks.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcUnreach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static DdNode *    Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose );
+static DdNode *    Abc_NtkInitStateAndVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose );
+static DdNode *    Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bRelation, DdNode * bInitial, bool fVerbose );
+static Abc_Ntk_t * Abc_NtkConstructExdc     ( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUnreach );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts sequential DCs of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
+{
+    int fCheck   = 1;
+    int fReorder = 1;
+    DdManager * dd;
+    DdNode * bRelation, * bInitial, * bUnreach;
+
+    // remove EXDC network if present
+    if ( pNtk->pExdc )
+    {
+        Abc_NtkDelete( pNtk->pExdc );
+        pNtk->pExdc = NULL; 
+    }
+
+    // compute the global BDDs of the latches
+    dd = Abc_NtkGlobalBdds( pNtk, 1 );    
+    if ( dd == NULL )
+        return 0;
+    if ( fVerbose )
+        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+
+    // create the transition relation (dereferenced global BDDs)
+    bRelation = Abc_NtkTransitionRelation( dd, pNtk, fVerbose );              Cudd_Ref( bRelation );
+    // create the initial state and the variable map
+    bInitial  = Abc_NtkInitStateAndVarMap( dd, pNtk, fVerbose );              Cudd_Ref( bInitial );
+    // compute the unreachable states
+    bUnreach  = Abc_NtkComputeUnreachable( dd, pNtk, bRelation, bInitial, fVerbose );   Cudd_Ref( bUnreach );
+    Cudd_RecursiveDeref( dd, bRelation );
+    Cudd_RecursiveDeref( dd, bInitial );
+
+    // reorder and disable reordering
+    if ( fReorder )
+    {
+        if ( fVerbose )
+            fprintf( stdout, "BDD nodes in the unreachable states before reordering %d.\n", Cudd_DagSize(bUnreach) );
+        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
+        Cudd_AutodynDisable( dd );
+        if ( fVerbose )
+            fprintf( stdout, "BDD nodes in the unreachable states after reordering %d.\n", Cudd_DagSize(bUnreach) );
+    }
+
+    // allocate ZDD variables
+    Cudd_zddVarsFromBddVars( dd, 2 );
+    // create the EXDC network representing the unreachable states
+    pNtk->pExdc = Abc_NtkConstructExdc( dd, pNtk, bUnreach );
+    Cudd_RecursiveDeref( dd, bUnreach );
+    Extra_StopManager( dd );
+
+    // make sure that everything is okay
+    if ( fCheck && !Abc_NtkCheck( pNtk->pExdc ) )
+    {
+        printf( "Abc_NtkExtractSequentialDcs: The network check has failed.\n" );
+        Abc_NtkDelete( pNtk->pExdc );
+        return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the transition relation of the network.]
+
+  Description [Assumes that the global BDDs are computed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose )
+{
+    DdNode * bRel, * bTemp, * bProd, * bVar, * bInputs;
+    Abc_Obj_t * pNode;
+    int fReorder = 1;
+    int i;
+
+    // extand the BDD manager to represent NS variables
+    assert( dd->size == Abc_NtkCiNum(pNtk) );
+    Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + Abc_NtkLatchNum(pNtk) - 1 );
+
+    // enable reordering
+    if ( fReorder )
+        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+    else
+        Cudd_AutodynDisable( dd );
+
+    // compute the transition relation
+    bRel = b1;   Cudd_Ref( bRel );
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+    {
+        bVar  = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
+        bProd = Cudd_bddXnor( dd, bVar, (DdNode *)pNode->pNext );   Cudd_Ref( bProd );
+        bRel  = Cudd_bddAnd( dd, bTemp = bRel, bProd );             Cudd_Ref( bRel );
+        Cudd_RecursiveDeref( dd, bTemp ); 
+        Cudd_RecursiveDeref( dd, bProd ); 
+    }
+    // free the global BDDs
+    Abc_NtkFreeGlobalBdds( dd, pNtk );
+
+    // quantify the PI variables
+    bInputs = Extra_bddComputeRangeCube( dd, 0, Abc_NtkPiNum(pNtk) );    Cudd_Ref( bInputs );
+    bRel    = Cudd_bddExistAbstract( dd, bTemp = bRel, bInputs );    Cudd_Ref( bRel );
+    Cudd_RecursiveDeref( dd, bTemp ); 
+    Cudd_RecursiveDeref( dd, bInputs ); 
+
+    // reorder and disable reordering
+    if ( fReorder )
+    {
+        if ( fVerbose )
+            fprintf( stdout, "BDD nodes in the transition relation before reordering %d.\n", Cudd_DagSize(bRel) );
+        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
+        Cudd_AutodynDisable( dd );
+        if ( fVerbose )
+            fprintf( stdout, "BDD nodes in the transition relation after reordering %d.\n", Cudd_DagSize(bRel) );
+    }
+    Cudd_Deref( bRel );
+    return bRel;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the initial state and sets up the variable map.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkInitStateAndVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose )
+{
+    DdNode ** pbVarsX, ** pbVarsY;
+    DdNode * bTemp, * bProd, * bVar;
+    Abc_Obj_t * pLatch;
+    int i;
+
+    // set the variable mapping for Cudd_bddVarMap()
+    pbVarsX = ALLOC( DdNode *, dd->size );
+    pbVarsY = ALLOC( DdNode *, dd->size );
+    bProd = b1;         Cudd_Ref( bProd );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        pbVarsX[i] = dd->vars[ Abc_NtkPiNum(pNtk) + i ];
+        pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
+        // get the initial value of the latch
+        bVar  = Cudd_NotCond( pbVarsX[i], (((int)pLatch->pData) != 1) );
+        bProd = Cudd_bddAnd( dd, bTemp = bProd, bVar );      Cudd_Ref( bProd );
+        Cudd_RecursiveDeref( dd, bTemp ); 
+    }
+    Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Abc_NtkLatchNum(pNtk) );
+    FREE( pbVarsX );
+    FREE( pbVarsY );
+
+    Cudd_Deref( bProd );
+    return bProd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the set of unreachable states.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bTrans, DdNode * bInitial, bool fVerbose )
+{
+    DdNode * bRelation, * bReached, * bCubeCs;
+    DdNode * bCurrent, * bNext, * bTemp;
+    int nIters;
+
+    // perform reachability analisys
+    bCurrent  = bInitial;   Cudd_Ref( bCurrent );
+    bReached  = bInitial;   Cudd_Ref( bReached );
+    bRelation = bTrans;     Cudd_Ref( bRelation );
+    bCubeCs   = Extra_bddComputeRangeCube( dd, Abc_NtkPiNum(pNtk), Abc_NtkCiNum(pNtk) );    Cudd_Ref( bCubeCs );
+    for ( nIters = 1; ; nIters++ )
+    {
+        // compute the next states
+        bNext = Cudd_bddAndAbstract( dd, bRelation, bCurrent, bCubeCs );  Cudd_Ref( bNext );
+        Cudd_RecursiveDeref( dd, bCurrent );
+        // remap these states into the current state vars
+        bNext = Cudd_bddVarMap( dd, bTemp = bNext );                      Cudd_Ref( bNext );
+        Cudd_RecursiveDeref( dd, bTemp );
+        // check if there are any new states
+        if ( Cudd_bddLeq( dd, bNext, bReached ) )
+            break;
+        // get the new states
+        bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) );          Cudd_Ref( bCurrent );
+        // minimize the new states with the reached states
+//        bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
+//        Cudd_RecursiveDeref( dd, bTemp );
+        // add to the reached states
+        bReached = Cudd_bddOr( dd, bTemp = bReached, bNext );             Cudd_Ref( bReached );
+        Cudd_RecursiveDeref( dd, bTemp );
+        Cudd_RecursiveDeref( dd, bNext );
+        // minimize the transition relation
+//        bRelation = Cudd_bddConstrain( dd, bTemp = bRelation, Cudd_Not(bReached) ); Cudd_Ref( bRelation );
+//        Cudd_RecursiveDeref( dd, bTemp );
+    }
+    Cudd_RecursiveDeref( dd, bRelation );
+    Cudd_RecursiveDeref( dd, bCubeCs );
+    Cudd_RecursiveDeref( dd, bNext );
+    // report the stats
+    if ( fVerbose )
+    {
+    fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
+    fprintf( stdout, "The number of minterms in the reachable state set = %d.\n", 
+                        (int)Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) ) ); 
+    }
+//PRB( dd, bReached );
+    Cudd_Deref( bReached );
+    return Cudd_Not( bReached );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the EXDC network.]
+
+  Description [The set of unreachable states depends on CS variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUnreach )
+{
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pNode, * pNodeNew;
+    int * pPermute;
+    int i;
+
+    // start the new network
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC_BDD );
+    // create PIs corresponding to LOs
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        pNode->pCopy = Abc_NtkCreateTermPi(pNtkNew);
+
+    // create a new node
+    pNodeNew = Abc_NtkCreateNode(pNtkNew);
+    // add the fanins corresponding to latch outputs
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        Abc_ObjAddFanin( pNodeNew, pNode->pCopy );
+
+    // create the logic function
+    pPermute = ALLOC( int, dd->size );
+    for ( i = 0; i < dd->size; i++ )
+        pPermute[i] = -1;
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        pPermute[Abc_NtkPiNum(pNtk) + i] = i;
+    // remap the functions
+    pNodeNew->pData = Extra_TransferPermute( dd, pNtkNew->pManFunc, bUnreach, pPermute );   Cudd_Ref( pNodeNew->pData );
+    free( pPermute );
+    Abc_NodeMinimumBase( pNodeNew );
+
+    // make the new node drive all the COs
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_ObjAddFanin( Abc_NtkCreateTermPo(pNtkNew), pNodeNew );
+
+    // copy the CI/CO names
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        Abc_NtkLogicStoreName( pNtkNew->vPis->pArray[i], Abc_NtkNameLatch(pNtk, i) );
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        Abc_NtkLogicStoreName( pNtkNew->vPos->pArray[i], Abc_NtkNamePo(pNtk, i) );
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        Abc_NtkLogicStoreName( pNtkNew->vPos->pArray[Abc_NtkPoNum(pNtk) + i], Abc_NtkNameLatchInput(pNtk, i) );
+
+    // transform the network to the SOP representation
+    Abc_NtkBddToSop( pNtkNew );
+    return pNtkNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index e971ca18..001a7231 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -777,6 +777,47 @@ Vec_Ptr_t * Abc_AigCollectAll( Abc_Ntk_t * pNtk )
     return vNodes;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Gets fanin node names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pFanin;
+    int i;
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        Vec_PtrPush( vNodes, util_strsav(Abc_ObjName(pFanin)) );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gets fanin node names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeFreeFaninNames( Vec_Ptr_t * vNames )
+{
+    int i;
+    for ( i = 0; i < vNames->nSize; i++ )
+        free( vNames->pArray[i] );
+    Vec_PtrFree( vNames );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/module.make b/src/base/abc/module.make
index 1eb88224..f698d167 100644
--- a/src/base/abc/module.make
+++ b/src/base/abc/module.make
@@ -10,6 +10,7 @@ SRC +=    src/base/abc/abc.c \
     src/base/abc/abcFpga.c \
     src/base/abc/abcFraig.c \
     src/base/abc/abcFunc.c \
+        src/base/abc/abcFxu.c \
     src/base/abc/abcLatch.c \
     src/base/abc/abcMap.c \
     src/base/abc/abcMinBase.c \
@@ -19,10 +20,13 @@ SRC +=    src/base/abc/abc.c \
     src/base/abc/abcPrint.c \
     src/base/abc/abcRefs.c \
     src/base/abc/abcRenode.c \
+    src/base/abc/abcRes.c \
     src/base/abc/abcSat.c \
+    src/base/abc/abcShow.c \
     src/base/abc/abcSop.c \
     src/base/abc/abcStrash.c \
     src/base/abc/abcSweep.c \
     src/base/abc/abcTiming.c \
+    src/base/abc/abcUnreach.c \
     src/base/abc/abcUtil.c \
     src/base/abc/abcVerify.c 
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 6d9c2347..10346729 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -88,7 +88,7 @@ Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck )
         Io_ReadBlifFree( p );
         return NULL;
     }
-    Abc_NtkTimeFinalize( pNtk );
+    Abc_NtkTimeInitialize( pNtk );
 
     // read the EXDC network
     if ( p->fParsingExdc )
diff --git a/src/base/main/main.h b/src/base/main/main.h
index c5d6a0c8..da47f154 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -84,6 +84,7 @@ extern void            Abc_FrameRestart( Abc_Frame_t * p );
 extern void            Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
 extern void            Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p );
 extern void            Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
+extern void            Abc_FrameUnmapAllNetworks( Abc_Frame_t * p );
 extern void            Abc_FrameDeleteAllNetworks( Abc_Frame_t * p );
 
 extern void               Abc_FrameSetGlobalFrame( Abc_Frame_t * p );
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 0b0cbbbd..38574883 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -205,19 +205,19 @@ bool Abc_FrameSetMode( Abc_Frame_t * p, bool fNameMode )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNetNew )
+void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtkNew )
 {
-    Abc_Ntk_t * pNet, * pNet2, * pNet3;
+    Abc_Ntk_t * pNtk, * pNtk2, * pNtk3;
     int nNetsPresent;
     int nNetsToSave;
     char * pValue;
 
     // link it to the previous network
-    Abc_NtkSetBackup( pNetNew, p->pNtkCur );
+    Abc_NtkSetBackup( pNtkNew, p->pNtkCur );
     // set the step of this network
-    Abc_NtkSetStep( pNetNew, ++p->nSteps );
+    Abc_NtkSetStep( pNtkNew, ++p->nSteps );
     // set this network to be the current network
-    p->pNtkCur = pNetNew;
+    p->pNtkCur = pNtkNew;
 
     // remove any extra network that may happen to be in the stack
     pValue = Cmd_FlagReadByName( p, "savesteps" );
@@ -229,20 +229,20 @@ void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNetNew )
     
     // count the network, remember the last one, and the one before the last one
     nNetsPresent = 0;
-    pNet2 = pNet3 = NULL;
-    for ( pNet = p->pNtkCur; pNet; pNet = Abc_NtkBackup(pNet2) )
+    pNtk2 = pNtk3 = NULL;
+    for ( pNtk = p->pNtkCur; pNtk; pNtk = Abc_NtkBackup(pNtk2) )
     {
         nNetsPresent++;
-        pNet3 = pNet2;
-        pNet2 = pNet;
+        pNtk3 = pNtk2;
+        pNtk2 = pNtk;
     }
 
     // remove the earliest backup network if it is more steps away than we store
     if ( nNetsPresent - 1 > nNetsToSave )
     { // delete the last network
-        Abc_NtkDelete( pNet2 );
+        Abc_NtkDelete( pNtk2 );
         // clean the pointer of the network before the last one
-        Abc_NtkSetBackup( pNet3, NULL );
+        Abc_NtkSetBackup( pNtk3, NULL );
     }
 }
 
@@ -259,31 +259,31 @@ void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNetNew )
 ***********************************************************************/
 void Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p )
 {
-    Abc_Ntk_t * pNtkCur, * pNetBack, * pNetBack2;
+    Abc_Ntk_t * pNtkCur, * pNtkBack, * pNtkBack2;
     int iStepCur, iStepBack;
 
     pNtkCur  = p->pNtkCur;
-    pNetBack = Abc_NtkBackup( pNtkCur );
+    pNtkBack = Abc_NtkBackup( pNtkCur );
     iStepCur = Abc_NtkStep  ( pNtkCur );
 
     // if there is no backup nothing to reset
-    if ( pNetBack == NULL )
+    if ( pNtkBack == NULL )
         return;
 
     // remember the backup of the backup
-    pNetBack2 = Abc_NtkBackup( pNetBack );
-    iStepBack = Abc_NtkStep  ( pNetBack );
+    pNtkBack2 = Abc_NtkBackup( pNtkBack );
+    iStepBack = Abc_NtkStep  ( pNtkBack );
 
     // set pNtkCur to be the next after the backup's backup
-    Abc_NtkSetBackup( pNtkCur, pNetBack2 );
+    Abc_NtkSetBackup( pNtkCur, pNtkBack2 );
     Abc_NtkSetStep  ( pNtkCur, iStepBack );
 
     // set pNtkCur to be the next after the backup
-    Abc_NtkSetBackup( pNetBack, pNtkCur );
-    Abc_NtkSetStep  ( pNetBack, iStepCur );
+    Abc_NtkSetBackup( pNtkBack, pNtkCur );
+    Abc_NtkSetStep  ( pNtkBack, iStepCur );
 
     // set the current network
-    p->pNtkCur = pNetBack;
+    p->pNtkCur = pNtkBack;
 }
 
 
@@ -299,26 +299,45 @@ void Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet )
+void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtk )
 {
-    if ( pNet == NULL )
+    if ( pNtk == NULL )
         return;
 
     // transfer the parameters to the new network
     if ( p->pNtkCur )
     {
-        Abc_NtkSetBackup( pNet, Abc_NtkBackup(p->pNtkCur) );
-        Abc_NtkSetStep( pNet, Abc_NtkStep(p->pNtkCur) );
+        Abc_NtkSetBackup( pNtk, Abc_NtkBackup(p->pNtkCur) );
+        Abc_NtkSetStep( pNtk, Abc_NtkStep(p->pNtkCur) );
         // delete the current network
         Abc_NtkDelete( p->pNtkCur );
     }
     else
     {
-        Abc_NtkSetBackup( pNet, NULL );
-        Abc_NtkSetStep( pNet, ++p->nSteps );
+        Abc_NtkSetBackup( pNtk, NULL );
+        Abc_NtkSetStep( pNtk, ++p->nSteps );
     }
     // set the new current network
-    p->pNtkCur = pNet;
+    p->pNtkCur = pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes library binding of all currently stored networks.]
+
+  Description [This procedure is called when the library is freed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FrameUnmapAllNetworks( Abc_Frame_t * p )
+{
+    Abc_Ntk_t * pNtk;
+    for ( pNtk = p->pNtkCur; pNtk; pNtk = Abc_NtkBackup(pNtk) )
+        if ( Abc_NtkIsLogicMap(pNtk) )
+            Abc_NtkUnmap( pNtk );
 }
 
 /**Function*************************************************************
@@ -334,14 +353,14 @@ void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet )
 ***********************************************************************/
 void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p )
 {
-    Abc_Ntk_t * pNet, * pNet2;
+    Abc_Ntk_t * pNtk, * pNtk2;
     // delete all the currently saved networks
-    for ( pNet  = p->pNtkCur, 
-          pNet2 = pNet? Abc_NtkBackup(pNet): NULL; 
-          pNet; 
-          pNet  = pNet2, 
-          pNet2 = pNet? Abc_NtkBackup(pNet): NULL )
-        Abc_NtkDelete( pNet );
+    for ( pNtk  = p->pNtkCur, 
+          pNtk2 = pNtk? Abc_NtkBackup(pNtk): NULL; 
+          pNtk; 
+          pNtk  = pNtk2, 
+          pNtk2 = pNtk? Abc_NtkBackup(pNtk): NULL )
+        Abc_NtkDelete( pNtk );
     // set the current network empty
     p->pNtkCur = NULL;
     fprintf( p->Out, "All networks have been deleted.\n" );