Version abc50901

17 files changed, 1126 insertions, 245 deletions

diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index 0d911e79..97e5663f 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -47,6 +47,7 @@ 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_CommandSweep        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFastExtract  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDisjoint     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -58,11 +59,13 @@ 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_CommandMuxes        ( 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_CommandSplit        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOneOutput    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOneNode      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShortNames   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandCut         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCut          ( 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 );
@@ -119,6 +122,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     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",    "sweep",         Abc_CommandSweep,            1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "fx",            Abc_CommandFastExtract,      1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "dsd",           Abc_CommandDisjoint,         1 );
 
@@ -130,9 +134,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
     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",      "muxes",         Abc_CommandMuxes,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "sat",           Abc_CommandSat,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "ext_seq_dcs",   Abc_CommandExtSeqDcs,        0 );
-    Cmd_CommandAdd( pAbc, "Various",      "split",         Abc_CommandSplit,            1 );
+    Cmd_CommandAdd( pAbc, "Various",      "one_output",    Abc_CommandOneOutput,        1 );
+    Cmd_CommandAdd( pAbc, "Various",      "one_node",      Abc_CommandOneNode,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "short_names",   Abc_CommandShortNames,       0 );
     Cmd_CommandAdd( pAbc, "Various",      "cut",           Abc_CommandCut,              0 );
 
@@ -428,17 +434,22 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pNode;
     int c;
+    int fUseRealNames;
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fUseRealNames = 1;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "nh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'n':
+            fUseRealNames ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -472,18 +483,19 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
             return 1;
         }
-        Abc_NodePrintFactor( pOut, pNode );
+        Abc_NodePrintFactor( pOut, pNode, fUseRealNames );
         return 0;
     }
     // print the nodes
-    Abc_NtkPrintFactor( pOut, pNtk );
+    Abc_NtkPrintFactor( pOut, pNtk, fUseRealNames );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: print_factor [-h] <node>\n" );
+    fprintf( pErr, "usage: print_factor [-nh] <node>\n" );
     fprintf( pErr, "\t        prints the factored forms of nodes\n" );
-    fprintf( pErr, "\tnode  : (optional) one node to consider\n");
+    fprintf( pErr, "\t-n    : toggles real/dummy fanin names [default = %s]\n", fUseRealNames? "real": "dummy" );
     fprintf( pErr, "\t-h    : print the command usage\n");
+    fprintf( pErr, "\tnode  : (optional) one node to consider\n");
     return 1;
 }
 
@@ -1182,7 +1194,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nThresh   =  0;
+    nThresh   =  1;
     nFaninMax = 20;
     fCnf      =  0;
     fMulti    =  0;
@@ -1255,11 +1267,14 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: renode [-T num] [-F num] [-cmsh]\n" );
     fprintf( pErr, "\t          transforms an AIG into a logic network by creating larger nodes\n" );
-    fprintf( pErr, "\t-T num  : the threshold for AIG node duplication [default = %d]\n", nThresh );
     fprintf( pErr, "\t-F num  : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
-    fprintf( pErr, "\t-c      : performs renoding to derive the CNF [default = %s]\n", fCnf? "yes": "no" );
+    fprintf( pErr, "\t-T num  : the threshold for AIG node duplication [default = %d]\n", nThresh );
+    fprintf( pErr, "\t          (an AIG node is the root of a new node after renoding\n" );
+    fprintf( pErr, "\t          if doing so prevents duplication of more than %d AIG nodes,\n", nThresh );
+    fprintf( pErr, "\t          that is, if [(numFanouts(Node)-1) * size(MFFC(Node))] > %d)\n", nThresh );
     fprintf( pErr, "\t-m      : creates multi-input AND graph [default = %s]\n", fMulti? "yes": "no" );
     fprintf( pErr, "\t-s      : creates a simple AIG (no renoding) [default = %s]\n", fSimple? "yes": "no" );
+    fprintf( pErr, "\t-c      : performs renoding to derive the CNF [default = %s]\n", fCnf? "yes": "no" );
     fprintf( pErr, "\t-h      : print the command usage\n");
     return 1;
 }
@@ -1280,22 +1295,17 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
-    int fDuplicate;
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fDuplicate = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "dh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'd':
-            fDuplicate ^= 1;
-            break;
         case 'h':
             goto usage;
         default:
@@ -1313,7 +1323,6 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Cleanup cannot be performed on the AIG.\n" );
         return 1;
     }
-
     // modify the current network
     Abc_NtkCleanup( pNtk, 0 );
     return 0;
@@ -1321,7 +1330,61 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: cleanup [-h]\n" );
     fprintf( pErr, "\t        removes dangling nodes\n" );
-//    fprintf( pErr, "\t-d    : toggle duplication of logic [default = %s]\n", fDuplicate? "yes": "no" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+
+    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_NtkIsSopLogic(pNtk) && !Abc_NtkIsBddLogic(pNtk) )
+    {
+        fprintf( pErr, "Sweep cannot be performed on an AIG or a mapped network (unmap it first).\n" );
+        return 1;
+    }
+    // modify the current network
+    Abc_NtkSweep( pNtk, 0 );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: sweep [-h]\n" );
+    fprintf( pErr, "\t        removes dangling nodes; propagates constant, buffers, inverters\n" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -1426,6 +1489,14 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    if ( !Abc_NtkIsLogic(pNtk) )
+    {
+        fprintf( pErr, "Fast extract can only be applied to a logic network.\n" );
+        Abc_NtkFxuFreeInfo( p );
+        return 1;
+    }
+
+
     // the nodes to be merged are linked into the special linked list
     Abc_NtkFastExtract( pNtk, p );
     Abc_NtkFxuFreeInfo( p );
@@ -1464,7 +1535,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
     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 );
+    extern int         Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -1510,14 +1581,9 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !fGlobal && !fRecursive )
-    {
-        fprintf( pErr, "Decomposition should be either global or recursive.\n" );
-        return 1;
-    }
-
     if ( fGlobal )
     {
+//        fprintf( stdout, "Performing DSD of global functions of the network.\n" );
         // get the new network
         if ( !Abc_NtkIsStrash(pNtk) )
         {
@@ -1531,18 +1597,9 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
         if ( pNtkRes == NULL )
         {
-            fprintf( pErr, "Global disjoint support decomposition has failed.\n" );
+            fprintf( pErr, "Global DSD 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 );
     }
@@ -1553,16 +1610,28 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
             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" );
+        fprintf( stdout, "Performing recursive DSD and MUX decomposition of local functions.\n" );
+        if ( !Abc_NtkDsdLocal( pNtk, fVerbose, fRecursive ) )
+            fprintf( pErr, "Recursive DSD has failed.\n" );
+    }
+    else 
+    {
+        if ( !Abc_NtkIsBddLogic( pNtk ) )
+        {
+            fprintf( pErr, "This command is only applicable to logic BDD networks.\n" );
+            return 1;
+        }
+        fprintf( stdout, "Performing simple non-recursive DSD of local functions.\n" );
+        if ( !Abc_NtkDsdLocal( pNtk, fVerbose, fRecursive ) )
+            fprintf( pErr, "Simple DSD of local functions 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-g     : toggle DSD of global and local functions [default = %s]\n", fGlobal? "global": "local" );  
+    fprintf( pErr, "\t-r     : toggle recursive DSD/MUX and simple DSD [default = %s]\n", fRecursive? "recursive DSD/MUX": "simple DSD" );  
     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" ); 
@@ -2135,6 +2204,71 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+
+    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_NtkIsBddLogic(pNtk) )
+    {
+        fprintf( pErr, "Only a BDD logic network can be converted to MUXes.\n" );
+        return 1;
+    }
+
+    // get the new network
+    pNtkRes = Abc_NtkBddToMuxes( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Converting to MUXes has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: muxes [-h]\n" );
+    fprintf( pErr, "\t        converts the current network by a network derived by\n" );
+    fprintf( pErr, "\t        replacing all nodes by DAGs isomorphic to the local BDDs\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -2279,7 +2413,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandSplit( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -2373,7 +2507,7 @@ int Abc_CommandSplit( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: split [-O num] [-ah] <name>\n" );
+    fprintf( pErr, "usage: one_output [-O num] [-ah] <name>\n" );
     fprintf( pErr, "\t         replaces the current network by the logic cone of one output\n" );
     fprintf( pErr, "\t-a     : toggle writing all CIs or structral support only [default = %s]\n", fUseAllCis? "all": "structural" );
     fprintf( pErr, "\t-h     : print the command usage\n");
@@ -2382,6 +2516,86 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    Abc_Obj_t * pNode;
+    int c;
+
+    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_NtkIsLogic(pNtk) )
+    {
+        fprintf( pErr, "Currently can only be applied to a logic network.\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;
+    }
+
+    pNtkRes = Abc_NtkSplitNode( pNtk, pNode );
+//    pNtkRes = Abc_NtkDeriveFromBdd( pNtk->pManFunc, pNode->pData, NULL, NULL );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Splitting one node has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: one_node [-h] <name>\n" );
+    fprintf( pErr, "\t         replaces the current network by the network composed of one node\n" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\tname   : the node name\n");
+    return 1;
+}
+
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index ab457cc9..c779230a 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -415,8 +415,6 @@ extern bool               Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
 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( Abc_Ntk_t * pNtk );
 /*=== abcCreate.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
@@ -427,6 +425,7 @@ extern void               Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkDup( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis );
 extern Abc_Ntk_t *        Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues );
+extern Abc_Ntk_t *        Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode );
 extern void               Abc_NtkDelete( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
@@ -491,6 +490,8 @@ extern int                Abc_NtkUnmap( Abc_Ntk_t * pNtk );
 /*=== abcMiter.c ==========================================================*/
 extern int                Abc_NtkMinimumBase( Abc_Ntk_t * pNtk );
 extern int                Abc_NodeMinimumBase( Abc_Obj_t * pNode );
+extern int                Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
+extern int                Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
 /*=== abcMiter.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 extern Abc_Ntk_t *        Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 );
@@ -515,14 +516,19 @@ extern Abc_Ntk_t *        Abc_NtkLogicToNetlistBench( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk );
+/*=== abcNtbdd.c ==========================================================*/
+extern Abc_Ntk_t *        Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi );
+extern Abc_Ntk_t *        Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
+extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly );
+extern void               Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk );
 /*=== abcPrint.c ==========================================================*/
 extern void               Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored );
 extern void               Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode );
-extern void               Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk );
-extern void               Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode );
+extern void               Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames );
+extern void               Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames );
 extern void               Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile );
 extern void               Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
 /*=== abcReconv.c ==========================================================*/
@@ -537,6 +543,7 @@ extern DdNode *           Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, Dd
 extern Vec_Ptr_t *        Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax );
 /*=== abcRefs.c ==========================================================*/
 extern int                Abc_NodeMffcSize( Abc_Obj_t * pNode );
+extern int                Abc_NodeMffcSizeStop( Abc_Obj_t * pNode );
 extern int                Abc_NodeMffcLabel( Abc_Obj_t * pNode );
 extern Vec_Ptr_t *        Abc_NodeMffcCollect( Abc_Obj_t * pNode );
 extern void               Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, int nGain );
@@ -593,6 +600,7 @@ extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
 /*=== abcSweep.c ==========================================================*/
 extern bool               Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose );
 extern int                Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
+extern int                Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose );
 /*=== abcTiming.c ==========================================================*/
 extern Abc_Time_t *       Abc_NodeReadArrival( Abc_Obj_t * pNode );
 extern Abc_Time_t *       Abc_NodeReadRequired( Abc_Obj_t * pNode );
@@ -646,7 +654,8 @@ 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_NodeGetFaninNames( Abc_Obj_t * pNode );
-extern void               Abc_NodeFreeFaninNames( Vec_Ptr_t * vNames );
+extern Vec_Ptr_t *        Abc_NodeGetFakeNames( int nNames );
+extern void               Abc_NodeFreeNames( Vec_Ptr_t * vNames );
 extern char **            Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos );
 extern void               Abc_NtkAlphaOrderSignals( Abc_Ntk_t * pNtk, int fComb );
 extern void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 25d1c86c..9b9e9ee2 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -367,7 +367,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pFanin, * pFanout;
     int i, Value = 1;
-//    int k;
+    int k;
 
     // check the network
     if ( pObj->pNtk != pNtk )
@@ -401,7 +401,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
             Value = 0;
         }
     }
-/*
+
     // make sure fanins are not duplicated
     for ( i = 0; i < pObj->vFanins.nSize; i++ )
         for ( k = i + 1; k < pObj->vFanins.nSize; k++ )
@@ -423,7 +423,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
                 printf( "Warning: Node %s has", Abc_ObjName(pObj) );
                 printf( " duplicated fanout %s.\n", Abc_ObjName(Abc_ObjFanout(pObj,k)) );
             }
-*/
+
     return Value;
 }
 
diff --git a/src/base/abc/abcCollapse.c b/src/base/abc/abcCollapse.c
index a6eda7b3..4e359506 100644
--- a/src/base/abc/abcCollapse.c
+++ b/src/base/abc/abcCollapse.c
@@ -24,7 +24,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static DdNode *    Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode );
 static Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk );
 static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc );
 
@@ -83,142 +82,6 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
 
 /**Function*************************************************************
 
-  Synopsis    [Derives global BDDs for the node function.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
-{
-    int fReorder = 1;
-    ProgressBar * pProgress;
-    Vec_Ptr_t * vFuncsGlob;
-    Abc_Obj_t * pNode;
-    DdNode * bFunc;
-    DdManager * dd;
-    int i;
-
-    // start the manager
-    assert( pNtk->pManGlob == NULL );
-    dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    if ( fReorder )
-        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
-
-    // set the elementary variables
-    Abc_NtkCleanCopy( pNtk );
-    Abc_NtkForEachCi( pNtk, pNode, i )
-        pNode->pCopy = (Abc_Obj_t *)dd->vars[i]; 
-    // assign the constant node BDD
-    pNode = Abc_AigConst1( pNtk->pManFunc );
-    pNode->pCopy = (Abc_Obj_t *)dd->one;   Cudd_Ref( dd->one );
-
-    vFuncsGlob = Vec_PtrAlloc( 100 );
-    if ( fLatchOnly )
-    {
-        // construct the BDDs
-        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkLatchNum(pNtk) );
-        Abc_NtkForEachLatch( 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) );   Cudd_Ref( bFunc );
-            Vec_PtrPush( vFuncsGlob, 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) );   Cudd_Ref( bFunc );
-            Vec_PtrPush( vFuncsGlob, bFunc );
-        }
-        Extra_ProgressBarStop( pProgress );
-    }
-
-    // derefence the intermediate BDDs
-    Abc_NtkForEachNode( pNtk, pNode, i )
-        if ( pNode->pCopy ) 
-        {
-            Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
-            pNode->pCopy = NULL;
-        }
-    // reorder one more time
-    if ( fReorder )
-    {
-        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
-        Cudd_AutodynDisable( dd );
-    }
-    pNtk->pManGlob = dd;
-    pNtk->vFuncsGlob = vFuncsGlob;
-    return dd;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the global BDD of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode )
-{
-    DdNode * bFunc, * bFunc0, * bFunc1;
-    assert( !Abc_ObjIsComplement(pNode) );
-    if ( Cudd_ReadKeys(dd) > 500000 )
-        return NULL;
-    // if the result is available return
-    if ( pNode->pCopy )
-        return (DdNode *)pNode->pCopy;
-    // compute the result for both branches
-    bFunc0 = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0) ); 
-    if ( bFunc0 == NULL )
-        return NULL;
-    Cudd_Ref( bFunc0 );
-    bFunc1 = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1) ); 
-    if ( bFunc1 == NULL )
-        return NULL;
-    Cudd_Ref( bFunc1 );
-    bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
-    bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
-    // get the final result
-    bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
-    Cudd_RecursiveDeref( dd, bFunc0 );
-    Cudd_RecursiveDeref( dd, bFunc1 );
-    // set the result
-    assert( pNode->pCopy == NULL );
-    pNode->pCopy = (Abc_Obj_t *)bFunc;
-    return bFunc;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Derives the network with the given global BDD.]
 
   Description []
@@ -276,29 +139,6 @@ 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( Abc_Ntk_t * pNtk )
-{
-    DdNode * bFunc;
-    int i;
-    assert( pNtk->pManGlob );
-    assert( pNtk->vFuncsGlob );
-    Vec_PtrForEachEntry( pNtk->vFuncsGlob, bFunc, i )
-        Cudd_RecursiveDeref( pNtk->pManGlob, bFunc );
-    Vec_PtrFree( pNtk->vFuncsGlob );
-    pNtk->vFuncsGlob = NULL;
-}
-
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcCreate.c
index d6500803..16d5ec05 100644
--- a/src/base/abc/abcCreate.c
+++ b/src/base/abc/abcCreate.c
@@ -406,6 +406,44 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t *
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
+{    
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pFanin, * pNodePo;
+    int i;
+    // start the network
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew->pName = util_strsav(Abc_ObjName(pNode));
+    // add the PIs corresponding to the fanins of the node
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        pFanin->pCopy = Abc_NtkCreatePi( pNtkNew );
+        Abc_NtkLogicStoreName( pFanin->pCopy, Abc_ObjName(pFanin) );
+    }
+    // duplicate and connect the node
+    pNode->pCopy = Abc_NtkDupObj( pNtkNew, pNode );
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        Abc_ObjAddFanin( pNode->pCopy, pFanin->pCopy );
+    // create the only PO
+    pNodePo = Abc_NtkCreatePo( pNtkNew );
+    Abc_ObjAddFanin( pNodePo, pNode->pCopy );
+    Abc_NtkLogicStoreName( pNodePo, Abc_ObjName(pNode) );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkSplitNode(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the Ntk.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_NtkDelete( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
@@ -758,6 +796,8 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
     }
     else if ( Abc_ObjIsNode(pObj) )
     {
+        if ( Abc_NtkHasBdd(pNtk) )
+            Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
         pNtk->nNodes--;
     }
     else if ( Abc_ObjIsLatch(pObj) )
diff --git a/src/base/abc/abcDsd.c b/src/base/abc/abcDsd.c
index ccb52ffa..013b7ac4 100644
--- a/src/base/abc/abcDsd.c
+++ b/src/base/abc/abcDsd.c
@@ -30,7 +30,7 @@ static void            Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t *
 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 void            Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd, bool fRecursive );
 static bool            Abc_NodeIsForDsd( Abc_Obj_t * pNode );
 static int             Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int nVars );
 
@@ -192,6 +192,8 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
         pDriver = Abc_ObjFanin0( pNode );
         if ( !Abc_ObjIsNode(pDriver) )
             continue;
+        if ( !Abc_NodeIsAigAnd(pDriver) )
+            continue;
         pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i );
         pNodeNew = (Abc_Obj_t *)Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) );
         assert( !Abc_ObjIsComplement(pNodeNew) );
@@ -300,7 +302,7 @@ Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNode
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDsdRecursive( Abc_Ntk_t * pNtk, bool fVerbose )
+int Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive )
 {
     int fCheck = 1;
     Dsd_Manager_t * pManDsd;
@@ -319,7 +321,7 @@ int Abc_NtkDsdRecursive( Abc_Ntk_t * pNtk, bool fVerbose )
     // collect nodes for decomposition
     vNodes = Abc_NtkCollectNodesForDsd( pNtk );
     for ( i = 0; i < vNodes->nSize; i++ )
-        Abc_NodeDecompDsdAndMux( vNodes->pArray[i], vNodes, pManDsd );
+        Abc_NodeDecompDsdAndMux( vNodes->pArray[i], vNodes, pManDsd, fRecursive );
     Vec_PtrFree( vNodes );
 
     // stop the DSD manager
@@ -371,7 +373,7 @@ Vec_Ptr_t * Abc_NtkCollectNodesForDsd( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd )
+void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd, bool fRecursive )
 {
     DdManager * dd = pNode->pNtk->pManFunc;
     Abc_Obj_t * pRoot, * pFanin, * pNode1, * pNode2, * pNodeC;
@@ -384,7 +386,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager
     pNodeDsd = Dsd_Regular( pNodeDsd );
 
     // determine what decomposition to use   
-    if ( Dsd_NodeReadDecsNum(pNodeDsd) != Abc_ObjFaninNum(pNode) )
+    if ( !fRecursive || Dsd_NodeReadDecsNum(pNodeDsd) != Abc_ObjFaninNum(pNode) )
     { // perform DSD
 
         // set the inputs
@@ -399,7 +401,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager
         for ( i = 0; i < nNodesDsd; i++ )
         {
             pRoot = Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNode->pNtk );
-            if ( Abc_NodeIsForDsd(pRoot) )
+            if ( Abc_NodeIsForDsd(pRoot) && fRecursive )
                 Vec_PtrPush( vNodes, pRoot );
         }
         free( ppNodesDsd );
@@ -457,9 +459,24 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager
 ***********************************************************************/
 bool Abc_NodeIsForDsd( Abc_Obj_t * pNode )
 {
+    DdManager * dd = pNode->pNtk->pManFunc;
+    DdNode * bFunc, * bFunc0, * bFunc1;
     assert( Abc_ObjIsNode(pNode) );
-    if ( Cudd_DagSize(pNode->pData)-1 > Abc_ObjFaninNum(pNode) )
-        return 1;
+//    if ( Cudd_DagSize(pNode->pData)-1 > Abc_ObjFaninNum(pNode) )
+//        return 1;
+//    return 0;
+
+    for ( bFunc = Cudd_Regular(pNode->pData); !cuddIsConstant(bFunc); )
+    {
+        bFunc0 = Cudd_Regular( cuddE(bFunc) );
+        bFunc1 = cuddT(bFunc);
+        if ( bFunc0 == b1 )
+            bFunc = bFunc1;
+        else if ( bFunc1 == b1 || bFunc0 == bFunc1 )
+            bFunc = bFunc0;
+        else
+            return 1;
+    }
     return 0;
 }
 
@@ -514,6 +531,7 @@ int Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int nVars )
     return iVar;
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcMinBase.c b/src/base/abc/abcMinBase.c
index 2a018e35..e143ba7b 100644
--- a/src/base/abc/abcMinBase.c
+++ b/src/base/abc/abcMinBase.c
@@ -93,6 +93,71 @@ int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
 
 /**Function*************************************************************
 
+  Synopsis    [Makes nodes of the network fanin-dup-free.]
+
+  Description [Returns the number of pairs of duplicated fanins.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i, Counter, fChanged;
+    assert( Abc_NtkIsBddLogic(pNtk) );
+    Counter = 0;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        while ( fChanged = Abc_NodeRemoveDupFanins(pNode) )
+            Counter += fChanged;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes one pair of duplicated fanins if present.]
+
+  Description [Returns 1 if the node is changed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin1, * pFanin2;
+    int i, k;
+    assert( Abc_NtkIsBddLogic(pNode->pNtk) );
+    assert( Abc_ObjIsNode(pNode) );
+    // make sure fanins are not duplicated
+    Abc_ObjForEachFanin( pNode, pFanin2, i )
+    {
+        Abc_ObjForEachFanin( pNode, pFanin1, k )
+        {
+            if ( k >= i )
+                break;
+            if ( pFanin1 == pFanin2 )
+            {
+                DdManager * dd = pNode->pNtk->pManFunc;
+                DdNode * bVar1 = Cudd_bddIthVar( dd, i );
+                DdNode * bVar2 = Cudd_bddIthVar( dd, k );
+                DdNode * bTrans, * bTemp;
+                bTrans = Cudd_bddXnor( dd, bVar1, bVar2 ); Cudd_Ref( bTrans );
+                pNode->pData = Cudd_bddAndAbstract( dd, bTemp = pNode->pData, bTrans, bVar2 ); Cudd_Ref( pNode->pData );
+                Cudd_RecursiveDeref( dd, bTemp );
+                Cudd_RecursiveDeref( dd, bTrans );
+                Abc_NodeMinimumBase( pNode );
+                return 1;
+            }
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes support of the node.]
 
   Description []
diff --git a/src/base/abc/abcNtbdd.c b/src/base/abc/abcNtbdd.c
new file mode 100644
index 00000000..61c1a110
--- /dev/null
+++ b/src/base/abc/abcNtbdd.c
@@ -0,0 +1,402 @@
+/**CFile****************************************************************
+
+  FileName    [abcNtbdd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Procedures to translate between the BDD and the network.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcNtbdd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void        Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+static Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pConst1 );
+static Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node );
+static DdNode *    Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs the network isomorphic to the given BDD.]
+
+  Description [Assumes that the BDD depends on the variables whose indexes
+  correspond to the names in the array (pNamesPi). Otherwise, returns NULL.
+  The resulting network comes with one node, whose functionality is
+  equal to the given BDD. To decompose this BDD into the network of
+  multiplexers use Abc_NtkBddToMuxes(). To decompose this BDD into
+  an And-Inverter Graph, use Abc_NtkStrash().]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi )
+{
+    Abc_Ntk_t * pNtk; 
+    Vec_Ptr_t * vNamesPiFake = NULL;
+    Abc_Obj_t * pNode, * pNodePi, * pNodePo;
+    DdNode * bSupp, * bTemp;
+    char * pName;
+    int i;
+
+    // supply fake names if real names are not given
+    if ( pNamePo == NULL )
+        pNamePo = "F";
+    if ( vNamesPi == NULL )
+    {
+        vNamesPiFake = Abc_NodeGetFakeNames( dd->size );
+        vNamesPi = vNamesPiFake;
+    }
+
+    // make sure BDD depends on the variables whose index 
+    // does not exceed the size of the array with PI names
+    bSupp = Cudd_Support( dd, bFunc );   Cudd_Ref( bSupp );
+    for ( bTemp = bSupp; bTemp != Cudd_ReadOne(dd); bTemp = cuddT(bTemp) )
+        if ( (int)Cudd_NodeReadIndex(bTemp) >= Vec_PtrSize(vNamesPi) )
+            break;
+    Cudd_RecursiveDeref( dd, bSupp );
+    if ( bTemp != Cudd_ReadOne(dd) )
+        return NULL;
+
+    // start the network
+    pNtk = Abc_NtkAlloc( ABC_TYPE_LOGIC, ABC_FUNC_BDD );
+    pNtk->pName = util_strsav(pNamePo);
+    // make sure the new manager has enough inputs
+    Cudd_bddIthVar( pNtk->pManFunc, Vec_PtrSize(vNamesPi) );
+    // add the PIs corresponding to the names
+    Vec_PtrForEachEntry( vNamesPi, pName, i )
+        Abc_NtkLogicStoreName( Abc_NtkCreatePi(pNtk), pName );
+    // create the node
+    pNode = Abc_NtkCreateNode( pNtk );
+    pNode->pData = Cudd_bddTransfer( dd, pNtk->pManFunc, bFunc ); Cudd_Ref(pNode->pData);
+    Abc_NtkForEachPi( pNtk, pNodePi, i )
+        Abc_ObjAddFanin( pNode, pNodePi );
+    // create the only PO
+    pNodePo = Abc_NtkCreatePo( pNtk );
+    Abc_ObjAddFanin( pNodePo, pNode );
+    Abc_NtkLogicStoreName( pNodePo, pNamePo );
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtk );
+    if ( vNamesPiFake )
+        Abc_NodeFreeNames( vNamesPiFake );
+    if ( !Abc_NtkCheck( pNtk ) )
+        fprintf( stdout, "Abc_NtkDeriveFromBdd(): Network check has failed.\n" );
+    return pNtk;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the network isomorphic to the union of local BDDs of the nodes.]
+
+  Description [The nodes of the local BDDs are converted into the network nodes 
+  with logic functions equal to the MUX.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk )
+{
+    int fCheck = 1;
+    Abc_Ntk_t * pNtkNew;
+    assert( Abc_NtkIsBddLogic(pNtk) );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP );
+    Abc_NtkBddToMuxesPerform( pNtk, pNtkNew );
+    Abc_NtkFinalize( pNtk, pNtkNew );
+    // make sure everything is okay
+    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkBddToMuxes: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network to MUXes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
+{
+    ProgressBar * pProgress;
+    DdManager * dd = pNtk->pManFunc;
+    Abc_Obj_t * pNode, * pNodeNew, * pConst1;
+    Vec_Ptr_t * vNodes;
+    int i;
+    // create the constant one node
+    pConst1 = Abc_NodeCreateConst1( pNtkNew );
+    // perform conversion in the topological order
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+    pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        // convert one node
+        assert( Abc_ObjIsNode(pNode) );
+        pNodeNew = Abc_NodeBddToMuxes( pNode, pNtkNew, pConst1 );
+        // mark the old node with the new one
+        assert( pNode->pCopy == NULL );
+        pNode->pCopy = pNodeNew;
+    }
+    Vec_PtrFree( vNodes );
+    Extra_ProgressBarStop( pProgress );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the node to MUXes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pConst1 )
+{
+    DdManager * dd = pNodeOld->pNtk->pManFunc;
+    DdNode * bFunc = pNodeOld->pData;
+    Abc_Obj_t * pFaninOld, * pNodeNew;
+    st_table * tBdd2Node;
+    int i;
+    // create the table mapping BDD nodes into the ABC nodes
+    tBdd2Node = st_init_table( st_ptrcmp, st_ptrhash );
+    // add the constant and the elementary vars
+    st_insert( tBdd2Node, (char *)b1, (char *)pConst1 );
+    Abc_ObjForEachFanin( pNodeOld, pFaninOld, i )
+        st_insert( tBdd2Node, (char *)Cudd_bddIthVar(dd, i), (char *)pFaninOld->pCopy );
+    // create the new nodes recursively
+    pNodeNew = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(bFunc), pNtkNew, tBdd2Node );
+    st_free_table( tBdd2Node );
+    if ( Cudd_IsComplement(bFunc) )
+        pNodeNew = Abc_NodeCreateInv( pNtkNew, pNodeNew );
+    return pNodeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the node to MUXes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node )
+{
+    Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC;
+    assert( !Cudd_IsComplement(bFunc) );
+    if ( st_lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) )
+        return pNodeNew;
+    // solve for the children nodes
+    pNodeNew0 = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(cuddE(bFunc)), pNtkNew, tBdd2Node );
+    if ( Cudd_IsComplement(cuddE(bFunc)) )
+        pNodeNew0 = Abc_NodeCreateInv( pNtkNew, pNodeNew0 );
+    pNodeNew1 = Abc_NodeBddToMuxes_rec( dd, cuddT(bFunc), pNtkNew, tBdd2Node );
+    if ( !st_lookup( tBdd2Node, (char *)Cudd_bddIthVar(dd, bFunc->index), (char **)&pNodeNewC ) )
+        assert( 0 );
+    // create the MUX node
+    pNodeNew = Abc_NodeCreateMux( pNtkNew, pNodeNewC, pNodeNew1, pNodeNew0 );
+    st_insert( tBdd2Node, (char *)bFunc, (char *)pNodeNew );
+    return pNodeNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives global BDDs for the COs of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
+{
+    int fReorder = 1;
+    ProgressBar * pProgress;
+    Vec_Ptr_t * vFuncsGlob;
+    Abc_Obj_t * pNode;
+    DdNode * bFunc;
+    DdManager * dd;
+    int i;
+
+    // start the manager
+    assert( pNtk->pManGlob == NULL );
+    dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    if ( fReorder )
+        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+
+    // set the elementary variables
+    Abc_NtkCleanCopy( pNtk );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->pCopy = (Abc_Obj_t *)dd->vars[i]; 
+    // assign the constant node BDD
+    pNode = Abc_AigConst1( pNtk->pManFunc );
+    pNode->pCopy = (Abc_Obj_t *)dd->one;   Cudd_Ref( dd->one );
+
+    // collect the global functions of the COs
+    vFuncsGlob = Vec_PtrAlloc( 100 );
+    if ( fLatchOnly )
+    {
+        // construct the BDDs
+        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkLatchNum(pNtk) );
+        Abc_NtkForEachLatch( pNtk, pNode, i )
+        {
+            Extra_ProgressBarUpdate( pProgress, i, NULL );
+            bFunc = Abc_NodeGlobalBdds_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) );   Cudd_Ref( bFunc );
+            Vec_PtrPush( vFuncsGlob, 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_NodeGlobalBdds_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) );   Cudd_Ref( bFunc );
+            Vec_PtrPush( vFuncsGlob, bFunc );
+        }
+        Extra_ProgressBarStop( pProgress );
+    }
+
+    // derefence the intermediate BDDs
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->pCopy ) 
+        {
+            Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
+            pNode->pCopy = NULL;
+        }
+    // reorder one more time
+    if ( fReorder )
+    {
+        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
+        Cudd_AutodynDisable( dd );
+    }
+    pNtk->pManGlob = dd;
+    pNtk->vFuncsGlob = vFuncsGlob;
+    return dd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the global BDD for one AIG node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode )
+{
+    DdNode * bFunc, * bFunc0, * bFunc1;
+    assert( !Abc_ObjIsComplement(pNode) );
+    if ( Cudd_ReadKeys(dd) > 500000 )
+        return NULL;
+    // if the result is available return
+    if ( pNode->pCopy )
+        return (DdNode *)pNode->pCopy;
+    // compute the result for both branches
+    bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0) ); 
+    if ( bFunc0 == NULL )
+        return NULL;
+    Cudd_Ref( bFunc0 );
+    bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1) ); 
+    if ( bFunc1 == NULL )
+        return NULL;
+    Cudd_Ref( bFunc1 );
+    bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
+    bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
+    // get the final result
+    bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( dd, bFunc0 );
+    Cudd_RecursiveDeref( dd, bFunc1 );
+    // set the result
+    assert( pNode->pCopy == NULL );
+    pNode->pCopy = (Abc_Obj_t *)bFunc;
+    return bFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dereferences global BDDs of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk )
+{
+    DdNode * bFunc;
+    int i;
+    assert( pNtk->pManGlob );
+    assert( pNtk->vFuncsGlob );
+    Vec_PtrForEachEntry( pNtk->vFuncsGlob, bFunc, i )
+        Cudd_RecursiveDeref( pNtk->pManGlob, bFunc );
+    Vec_PtrFree( pNtk->vFuncsGlob );
+    pNtk->vFuncsGlob = NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c
index c7599f11..4f8b4aeb 100644
--- a/src/base/abc/abcPrint.c
+++ b/src/base/abc/abcPrint.c
@@ -310,13 +310,13 @@ void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk )
+void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames )
 {
     Abc_Obj_t * pNode;
     int i;
     assert( Abc_NtkIsSopLogic(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
-        Abc_NodePrintFactor( pFile, pNode );
+        Abc_NodePrintFactor( pFile, pNode, fUseRealNames );
 }
 
 /**Function*************************************************************
@@ -330,9 +330,10 @@ void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode )
+void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames )
 {
     Vec_Int_t * vFactor;
+    Vec_Ptr_t * vNamesIn;
     if ( Abc_ObjIsCo(pNode) )
         pNode = Abc_ObjFanin0(pNode);
     if ( Abc_ObjIsPi(pNode) )
@@ -347,7 +348,14 @@ void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode )
     }
     assert( Abc_ObjIsNode(pNode) );
     vFactor = Ft_Factor( pNode->pData );
-    Ft_FactorPrint( stdout, vFactor, NULL, Abc_ObjName(pNode) );
+    if ( fUseRealNames )
+    {
+        vNamesIn = Abc_NodeGetFaninNames(pNode);
+        Ft_FactorPrint( stdout, vFactor, (char **)vNamesIn->pArray, Abc_ObjName(pNode) );
+        Abc_NodeFreeNames( vNamesIn );
+    }
+    else
+        Ft_FactorPrint( stdout, vFactor, (char **)NULL, Abc_ObjName(pNode) );
     Vec_IntFree( vFactor );
 }
 
diff --git a/src/base/abc/abcRefactor.c b/src/base/abc/abcRefactor.c
index 9a413bb1..1524489d 100644
--- a/src/base/abc/abcRefactor.c
+++ b/src/base/abc/abcRefactor.c
@@ -95,6 +95,8 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
     int clk, clkStart = clock();
 
     assert( Abc_NtkIsStrash(pNtk) );
+    // cleanup the AIG
+    Abc_AigCleanup(pNtk->pManFunc);
     // start the managers
     pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, 1000 );
     pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose );
diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c
index dfcc3ae5..5cfa23ba 100644
--- a/src/base/abc/abcRefs.c
+++ b/src/base/abc/abcRefs.c
@@ -6,7 +6,7 @@
 
   PackageName [Network and node package.]
 
-  Synopsis    [Reference counting of the nodes.]
+  Synopsis    [Procedures using reference counting of the AIG nodes.]
 
   Author      [Alan Mishchenko]
   
@@ -25,6 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t * vNodes );
+static int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -32,7 +33,7 @@ static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Ve
 
 /**Function*************************************************************
 
-  Synopsis    [Procedure returns the size of the MFFC of the node.]
+  Synopsis    [Returns the MFFC size.]
 
   Description []
                
@@ -57,6 +58,31 @@ int Abc_NodeMffcSize( Abc_Obj_t * pNode )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the MFFC size while stopping at the complemented edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode )
+{
+    int nConeSize1, nConeSize2;
+    assert( !Abc_ObjIsComplement( pNode ) );
+    assert( Abc_ObjIsNode( pNode ) );
+    if ( Abc_ObjFaninNum(pNode) == 0 )
+        return 0;
+    nConeSize1 = Abc_NodeRefDerefStop( pNode, 0 ); // dereference
+    nConeSize2 = Abc_NodeRefDerefStop( pNode, 1 ); // reference
+    assert( nConeSize1 == nConeSize2 );
+    assert( nConeSize1 > 0 );
+    return nConeSize1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Labels MFFC with the current traversal ID.]
 
   Description []
@@ -132,8 +158,8 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t
     if ( Abc_ObjIsCi(pNode) )
         return 0;
     // process the internal node
-    pNode0 = Abc_ObjFanin( pNode, 0 );
-    pNode1 = Abc_ObjFanin( pNode, 1 );
+    pNode0 = Abc_ObjFanin0(pNode);
+    pNode1 = Abc_ObjFanin1(pNode);
     Counter = 1;
     if ( fReference )
     {
@@ -156,6 +182,47 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t
 
 /**Function*************************************************************
 
+  Synopsis    [References/references the node and returns MFFC size.]
+
+  Description [Stops at the complemented edges.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference )
+{
+    Abc_Obj_t * pNode0, * pNode1;
+    int Counter;
+    // skip the CI
+    if ( Abc_ObjIsCi(pNode) )
+        return 0;
+    // process the internal node
+    pNode0 = Abc_ObjFanin0(pNode);
+    pNode1 = Abc_ObjFanin1(pNode);
+    Counter = 1;
+    if ( fReference )
+    {
+        if ( pNode0->vFanouts.nSize++ == 0 && !Abc_ObjFaninC0(pNode) )
+            Counter += Abc_NodeRefDerefStop( pNode0, fReference );
+        if ( pNode1->vFanouts.nSize++ == 0 && !Abc_ObjFaninC1(pNode) )
+            Counter += Abc_NodeRefDerefStop( pNode1, fReference );
+    }
+    else
+    {
+        assert( pNode0->vFanouts.nSize > 0 );
+        assert( pNode1->vFanouts.nSize > 0 );
+        if ( --pNode0->vFanouts.nSize == 0 && !Abc_ObjFaninC0(pNode) )
+            Counter += Abc_NodeRefDerefStop( pNode0, fReference );
+        if ( --pNode1->vFanouts.nSize == 0 && !Abc_ObjFaninC1(pNode) )
+            Counter += Abc_NodeRefDerefStop( pNode1, fReference );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Replaces MFFC of the node by the new factored form.]
 
   Description []
diff --git a/src/base/abc/abcRenode.c b/src/base/abc/abcRenode.c
index c45f9763..b17e2394 100644
--- a/src/base/abc/abcRenode.c
+++ b/src/base/abc/abcRenode.c
@@ -31,7 +31,7 @@ static DdNode *    Abc_NtkRenodeDeriveBdd_rec( DdManager * dd, Abc_Obj_t * pNode
 
 static void        Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax );
 static void        Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk );
-static void        Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk );
+static void        Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh );
 static void        Abc_NtkRenodeSetBoundsSimple( Abc_Ntk_t * pNtk );
 static void        Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone );
 
@@ -67,7 +67,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn
     if ( fCnf )
         Abc_NtkRenodeSetBoundsCnf( pNtk );
     else if ( fMulti )
-        Abc_NtkRenodeSetBoundsMulti( pNtk );
+        Abc_NtkRenodeSetBoundsMulti( pNtk, nThresh );
     else if ( fSimple )
         Abc_NtkRenodeSetBoundsSimple( pNtk );
     else
@@ -393,9 +393,7 @@ void Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax )
     }
 
     // mark the PO drivers
-    Abc_NtkForEachPo( pNtk, pNode, i )
-        Abc_ObjFanin0(pNode)->fMarkA = 1;
-    Abc_NtkForEachLatch( pNtk, pNode, i )
+    Abc_NtkForEachCo( pNtk, pNode, i )
         Abc_ObjFanin0(pNode)->fMarkA = 1;
 
     // make sure the fanin limit is met
@@ -474,9 +472,7 @@ void Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk )
     }
 
     // mark the PO drivers
-    Abc_NtkForEachPo( pNtk, pNode, i )
-        Abc_ObjFanin0(pNode)->fMarkA = 1;
-    Abc_NtkForEachLatch( pNtk, pNode, i )
+    Abc_NtkForEachCo( pNtk, pNode, i )
         Abc_ObjFanin0(pNode)->fMarkA = 1;
 
     // count the number of MUXes
@@ -505,10 +501,10 @@ void Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk )
+void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh )
 {
     Abc_Obj_t * pNode;
-    int i;
+    int i, nFanouts, nConeSize;
 
     // make sure the mark is not set
     Abc_NtkForEachObj( pNtk, pNode, i )
@@ -521,7 +517,12 @@ void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk )
         if ( Abc_NodeIsConst(pNode) )
             continue;
         // mark the nodes with multiple fanouts
-        if ( Abc_ObjFanoutNum(pNode) > 1 )
+//        if ( Abc_ObjFanoutNum(pNode) > 1 )
+//            pNode->fMarkA = 1;
+        // mark the nodes with multiple fanouts
+        nFanouts = Abc_ObjFanoutNum(pNode);
+        nConeSize = Abc_NodeMffcSizeStop(pNode);
+        if ( (nFanouts - 1) * nConeSize > nThresh )
             pNode->fMarkA = 1;
         // mark the children if they are pointed by the complemented edges
         if ( Abc_ObjFaninC0(pNode) )
@@ -531,9 +532,7 @@ void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk )
     }
 
     // mark the PO drivers
-    Abc_NtkForEachPo( pNtk, pNode, i )
-        Abc_ObjFanin0(pNode)->fMarkA = 1;
-    Abc_NtkForEachLatch( pNtk, pNode, i )
+    Abc_NtkForEachCo( pNtk, pNode, i )
         Abc_ObjFanin0(pNode)->fMarkA = 1;
 }
 
diff --git a/src/base/abc/abcRewrite.c b/src/base/abc/abcRewrite.c
index 62e506bb..f28aaa42 100644
--- a/src/base/abc/abcRewrite.c
+++ b/src/base/abc/abcRewrite.c
@@ -56,6 +56,8 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose )
     int clk, clkStart = clock();
 
     assert( Abc_NtkIsStrash(pNtk) );
+    // cleanup the AIG
+    Abc_AigCleanup(pNtk->pManFunc);
     // start the rewriting manager
     pManRwr = Rwr_ManStart( 0 );
     if ( pManRwr == NULL )
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index 38840de0..a3e522cb 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -68,7 +68,7 @@ void Abc_NodeShowBdd( Abc_Obj_t * pNode )
     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_NodeFreeNames( vNamesIn );
     Abc_NtkCleanCopy( pNode->pNtk );
     fclose( pFile );
 
diff --git a/src/base/abc/abcSweep.c b/src/base/abc/abcSweep.c
index 61d65ce3..ca9bd34e 100644
--- a/src/base/abc/abcSweep.c
+++ b/src/base/abc/abcSweep.c
@@ -25,13 +25,17 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern Fraig_Man_t *  Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
+
 static stmm_table *   Abc_NtkFraigEquiv( Fraig_Man_t * p, Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose );
 static void           Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv, bool fVerbose );
 static void           Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fVerbose, int fUseInv );
 static void           Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fVerbose, int fUseInv );
 static int            Abc_NodeDroppingCost( Abc_Obj_t * pNode );
 
-extern Fraig_Man_t *  Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
+static void           Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose );
+static void           Abc_NodeConstantInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin, bool fConst0 );
+static void           Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -427,6 +431,175 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
     return Counter;
 }
 
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Tranditional sweep of the network.]
+
+  Description [Propagates constant and single-input node, removes dangling nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    int fCheck = 1;
+    Abc_Obj_t * pNode;
+    int i, fConvert, nSwept, nSweptNew;
+    assert( Abc_NtkIsSopLogic(pNtk) || Abc_NtkIsBddLogic(pNtk) ); 
+    // convert to the BDD representation
+    fConvert = 0;
+    if ( Abc_NtkIsSopLogic(pNtk) )
+        Abc_NtkSopToBdd(pNtk), fConvert = 1;
+    // perform cleanup to get rid of dangling nodes
+    nSwept = Abc_NtkCleanup( pNtk, 0 );
+    // make the network minimum base
+    Abc_NtkRemoveDupFanins(pNtk);
+    Abc_NtkMinimumBase(pNtk);
+    do
+    {
+        // sweep constants and single-input nodes
+        Abc_NtkForEachNode( pNtk, pNode, i )
+            if ( Abc_ObjFaninNum(pNode) < 2 )
+                Abc_NodeSweep( pNode, fVerbose );
+        // make the network minimum base
+        Abc_NtkRemoveDupFanins(pNtk);
+        Abc_NtkMinimumBase(pNtk);
+        // perform final clean up (in case new danglies are created)
+        nSweptNew = Abc_NtkCleanup( pNtk, 0 );
+        nSwept += nSweptNew;
+    }
+    while ( nSweptNew );
+    // conver back to BDD
+    if ( fConvert )
+        Abc_NtkBddToSop(pNtk);
+    // report
+    if ( fVerbose )
+        printf( "Sweep removed %d nodes.\n", nSwept );
+    // check
+    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Abc_NtkSweep: The network check has failed.\n" );
+        return -1;
+    }
+    return nSwept;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Tranditional sweep of the network.]
+
+  Description [Propagates constant and single-input node, removes dangling nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose )
+{
+    Vec_Ptr_t * vFanout = pNode->pNtk->vPtrTemp;
+    Abc_Obj_t * pFanout, * pDriver;
+    int i;
+    assert( Abc_ObjFaninNum(pNode) < 2 );
+    assert( Abc_ObjFanoutNum(pNode) > 0 );
+    // iterate through the fanouts
+    Abc_NodeCollectFanouts( pNode, vFanout );
+    Vec_PtrForEachEntry( vFanout, pFanout, i )
+    {
+        if ( Abc_ObjIsCo(pFanout) )
+        {
+            if ( Abc_ObjFaninNum(pNode) == 1 )
+            {
+                pDriver = Abc_ObjFanin0(pNode);
+                if ( Abc_ObjIsCi(pDriver) || Abc_ObjFanoutNum(pDriver) > 1 || Abc_ObjFanoutNum(pNode) > 1 )
+                    continue;
+                // the driver is a node and its only fanout is this node
+                if ( Abc_NodeIsInv(pNode) )
+                    pDriver->pData = Cudd_Not(pDriver->pData);
+                // replace the fanin of the fanout
+                Abc_ObjPatchFanin( pFanout, pNode, pDriver );
+            }
+            continue;
+        }
+        // the fanout is a regular node
+        if ( Abc_ObjFaninNum(pNode) == 0 )
+            Abc_NodeConstantInput( pFanout, pNode, Abc_NodeIsConst0(pNode) );
+        else 
+        {
+            assert( Abc_ObjFaninNum(pNode) == 1 );
+            pDriver = Abc_ObjFanin0(pNode);
+            if ( Abc_NodeIsInv(pNode) )
+                Abc_NodeComplementInput( pFanout, pNode );
+            Abc_ObjPatchFanin( pFanout, pNode, pDriver );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces the local function by its cofactor.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeConstantInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin, bool fConst0 )
+{
+    DdManager * dd = pNode->pNtk->pManFunc;
+    DdNode * bVar, * bTemp;
+    int iFanin;
+    assert( Abc_NtkIsBddLogic(pNode->pNtk) ); 
+    if ( (iFanin = Vec_FanFindEntry( &pNode->vFanins, pFanin->Id )) == -1 )
+    {
+        printf( "Node %s should be among", Abc_ObjName(pFanin) );
+        printf( " the fanins of node %s...\n", Abc_ObjName(pNode) );
+        return;
+    }
+    bVar = Cudd_NotCond( Cudd_bddIthVar(dd, iFanin), fConst0 );
+    pNode->pData = Cudd_Cofactor( dd, bTemp = pNode->pData, bVar );   Cudd_Ref( pNode->pData );
+    Cudd_RecursiveDeref( dd, bTemp );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Changes the polarity of one fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin )
+{
+    DdManager * dd = pNode->pNtk->pManFunc;
+    DdNode * bVar, * bCof0, * bCof1;
+    int iFanin;
+    assert( Abc_NtkIsBddLogic(pNode->pNtk) ); 
+    if ( (iFanin = Vec_FanFindEntry( &pNode->vFanins, pFanin->Id )) == -1 )
+    {
+        printf( "Node %s should be among", Abc_ObjName(pFanin) );
+        printf( " the fanins of node %s...\n", Abc_ObjName(pNode) );
+        return;
+    }
+    bVar = Cudd_bddIthVar( dd, iFanin );
+    bCof0 = Cudd_Cofactor( dd, pNode->pData, Cudd_Not(bVar) );   Cudd_Ref( bCof0 );
+    bCof1 = Cudd_Cofactor( dd, pNode->pData, bVar );             Cudd_Ref( bCof1 );
+    Cudd_RecursiveDeref( dd, pNode->pData );
+    pNode->pData = Cudd_bddIte( dd, bVar, bCof0, bCof1 );        Cudd_Ref( pNode->pData );
+    Cudd_RecursiveDeref( dd, bCof0 );
+    Cudd_RecursiveDeref( dd, bCof1 );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 9a2acc32..2c460301 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [abcUtils.c]
+  FileName    [abcUtil.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: abcUtils.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: abcUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -410,6 +410,9 @@ int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate )
         Abc_ObjPatchFanin( pNode, pDriver, pDriverNew );
         assert( Abc_ObjFanoutNum(pDriverNew) == 1 );
         nDupGates++;
+        // remove the old driver if it dangles
+        if ( Abc_ObjFanoutNum(pDriver) == 0 )
+            Abc_NtkDeleteObj( pDriver );
     }
     assert( Abc_NtkLogicHasSimpleCos(pNtk) );
     return nDupGates;
@@ -887,9 +890,47 @@ Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeFreeFaninNames( Vec_Ptr_t * vNames )
+Vec_Ptr_t * Abc_NodeGetFakeNames( int nNames )
 {
+    Vec_Ptr_t * vNames;
+    char Buffer[5];
     int i;
+
+    vNames = Vec_PtrAlloc( nNames );
+    for ( i = 0; i < nNames; i++ )
+    {
+        if ( nNames < 26 )
+        {
+            Buffer[0] = 'a' + i;
+            Buffer[1] = 0;
+        }
+        else
+        {
+            Buffer[0] = 'a' + i%26;
+            Buffer[1] = '0' + i/26;
+            Buffer[2] = 0;
+        }
+        Vec_PtrPush( vNames, util_strsav(Buffer) );
+    }
+    return vNames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gets fanin node names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeFreeNames( Vec_Ptr_t * vNames )
+{
+    int i;
+    if ( vNames == NULL )
+        return;
     for ( i = 0; i < vNames->nSize; i++ )
         free( vNames->pArray[i] );
     Vec_PtrFree( vNames );
diff --git a/src/base/abc/module.make b/src/base/abc/module.make
index d3d4091b..695e056b 100644
--- a/src/base/abc/module.make
+++ b/src/base/abc/module.make
@@ -19,6 +19,7 @@ SRC +=    src/base/abc/abc.c \
     src/base/abc/abcMiter.c \
     src/base/abc/abcNames.c \
     src/base/abc/abcNetlist.c \
+    src/base/abc/abcNtbdd.c \
     src/base/abc/abcPrint.c \
     src/base/abc/abcReconv.c \
     src/base/abc/abcRefactor.c \