Version abc60211

26 files changed, 903 insertions, 124 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index cbdf87c7..7ace4880 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -425,7 +425,7 @@ extern void               Abc_AigSetNodePhases( Abc_Ntk_t * pNtk );
 /*=== abcAttach.c ==========================================================*/
 extern int                Abc_NtkAttach( Abc_Ntk_t * pNtk );
 /*=== abcBalance.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate );
+extern Abc_Ntk_t *        Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective );
 /*=== abcCheck.c ==========================================================*/
 extern bool               Abc_NtkCheck( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkCheckRead( Abc_Ntk_t * pNtk );
@@ -587,6 +587,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_NodeMffcSizeSupp( Abc_Obj_t * pNode );
 extern int                Abc_NodeMffcSizeStop( Abc_Obj_t * pNode );
 extern int                Abc_NodeMffcLabel( Abc_Obj_t * pNode );
 extern int                Abc_NodeMffcLabelFast( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
@@ -673,6 +674,7 @@ extern int                Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkCleanCopy( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkCleanNext( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkCleanMarkA( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode );
 extern bool               Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate );
diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c
index 04647d0b..5d0c68d1 100644
--- a/src/base/abc/abcRefs.c
+++ b/src/base/abc/abcRefs.c
@@ -25,6 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t * vNodes );
+static int Abc_NodeMffcCountSupp( Vec_Ptr_t * vNodes );
 static int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference );
 static int Abc_NodeDeref( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
 
@@ -46,6 +47,7 @@ static int Abc_NodeDeref( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
 int Abc_NodeMffcSize( Abc_Obj_t * pNode )
 {
     int nConeSize1, nConeSize2;
+    assert( Abc_NtkIsStrash(pNode->pNtk) );
     assert( !Abc_ObjIsComplement( pNode ) );
     assert( Abc_ObjIsNode( pNode ) );
     if ( Abc_ObjFaninNum(pNode) == 0 )
@@ -59,6 +61,36 @@ int Abc_NodeMffcSize( Abc_Obj_t * pNode )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the MFFC size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeMffcSizeSupp( Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vNodes;
+    int nSuppSize, nConeSize1, nConeSize2;
+    assert( Abc_NtkIsStrash(pNode->pNtk) );
+    assert( !Abc_ObjIsComplement( pNode ) );
+    assert( Abc_ObjIsNode( pNode ) );
+    if ( Abc_ObjFaninNum(pNode) == 0 )
+        return 0;
+    vNodes = Vec_PtrAlloc( 10 );
+    nConeSize1 = Abc_NodeRefDeref( pNode, 0, 0, vNodes ); // dereference
+    nSuppSize = Abc_NodeMffcCountSupp(vNodes);
+    nConeSize2 = Abc_NodeRefDeref( pNode, 1, 0, NULL ); // reference
+    assert( nConeSize1 == nConeSize2 );
+    assert( nConeSize1 > 0 );
+    Vec_PtrFree(vNodes);
+    return nSuppSize;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the MFFC size while stopping at the complemented edges.]
 
   Description []
@@ -71,6 +103,7 @@ int Abc_NodeMffcSize( Abc_Obj_t * pNode )
 int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode )
 {
     int nConeSize1, nConeSize2;
+    assert( Abc_NtkIsStrash(pNode->pNtk) );
     assert( !Abc_ObjIsComplement( pNode ) );
     assert( Abc_ObjIsNode( pNode ) );
     if ( Abc_ObjFaninNum(pNode) == 0 )
@@ -219,6 +252,61 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t
 
 /**Function*************************************************************
 
+  Synopsis    [References/references the node and returns MFFC supp size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeMffcCountSupp( Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pNode, * pNode0, * pNode1;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        if ( Abc_ObjIsCi(pNode) )
+        {
+            if ( pNode->fMarkB == 0 )
+            {
+                pNode->fMarkB = 1;
+                Counter++;
+            }
+            continue;
+        }
+        pNode0 = Abc_ObjFanin0(pNode);
+        if ( pNode0->vFanouts.nSize > 0 && pNode0->fMarkB == 0 )
+        {
+            pNode0->fMarkB = 1;
+            Counter++;
+        }
+        pNode1 = Abc_ObjFanin1(pNode);
+        if ( pNode1->vFanouts.nSize > 0 && pNode1->fMarkB == 0 )
+        {
+            pNode1->fMarkB = 1;
+            Counter++;
+        }
+    }
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        if ( Abc_ObjIsCi(pNode) )
+        {
+            pNode->fMarkB = 0;
+            continue;
+        }
+        pNode0 = Abc_ObjFanin0(pNode);
+        pNode0->fMarkB = 0;
+        pNode1 = Abc_ObjFanin1(pNode);
+        pNode1->fMarkB = 0;
+    }
+    return Counter;
+
+}
+
+/**Function*************************************************************
+
   Synopsis    [References/references the node and returns MFFC size.]
 
   Description []
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index 4152dd0a..1e59b17b 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -308,7 +308,7 @@ char * Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars )
 char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars )
 {
     assert( nVars == 2 );
-    return Abc_SopRegister(pMan, "11 1\n11 1\n");
+    return Abc_SopRegister(pMan, "11 1\n00 1\n");
 }
 
 /**Function*************************************************************
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 9d95fade..1e52e4a6 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -335,6 +335,25 @@ void Abc_NtkCleanNext( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Cleans the copy field of all objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCleanMarkA( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i = 0;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->fMarkA = 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks if the internal node has a unique CO.]
 
   Description [Checks if the internal node can borrow a name from a CO
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5f5c4b49..119f8cdf 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -40,6 +40,8 @@ static int Abc_CommandPrintFactor  ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandPrintLevel   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintSymms   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintUnate   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintAuto    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintKMap    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintGates   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintSharing ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -137,6 +139,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Printing",     "print_level",   Abc_CommandPrintLevel,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_supp",    Abc_CommandPrintSupport,     0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_symm",    Abc_CommandPrintSymms,       0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_unate",   Abc_CommandPrintUnate,       0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_auto",    Abc_CommandPrintAuto,        0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_kmap",    Abc_CommandPrintKMap,        0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_gates",   Abc_CommandPrintGates,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_sharing", Abc_CommandPrintSharing,     0 );
@@ -247,7 +251,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fFactor;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -310,7 +314,7 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     extern double Abc_NtkSpacePercentage( Abc_Obj_t * pNode );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -398,7 +402,7 @@ int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Obj_t * pNode;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -467,7 +471,7 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -517,7 +521,7 @@ int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -570,7 +574,7 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fUseRealNames;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -653,7 +657,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fListNodes;
     int fProfile;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -742,7 +746,7 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
     extern void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -817,7 +821,7 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerbose;
     extern void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -884,6 +888,160 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandPrintUnate( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int fUseBdds;
+    int fUseNaive;
+    int fVerbose;
+    extern void Abc_NtkPrintUnate( Abc_Ntk_t * pNtk, int fUseBdds, int fUseNaive, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fUseBdds  = 1;
+    fUseNaive = 0;
+    fVerbose  = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "bnvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'b':
+            fUseBdds ^= 1;
+            break;
+        case 'n':
+            fUseNaive ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" );
+        return 1;
+    }
+    Abc_NtkPrintUnate( pNtk, fUseBdds, fUseNaive, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: print_unate [-bnvh]\n" );
+    fprintf( pErr, "\t         computes unate variables of the PO functions\n" );
+    fprintf( pErr, "\t-b     : toggle BDD-based or SAT-based computations [default = %s].\n", fUseBdds? "BDD": "SAT" );  
+    fprintf( pErr, "\t-n     : toggle naive BDD-based computation [default = %s].\n", fUseNaive? "yes": "no" );  
+    fprintf( pErr, "\t-v     : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandPrintAuto( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int Output;
+    int fNaive;
+    int fVerbose;
+    extern void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Output   = -1;
+    fNaive   = 0;
+    fVerbose = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "Onvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'O':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-O\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            Output = atoi(argv[util_optind]);
+            util_optind++;
+            if ( Output < 0 ) 
+                goto usage;
+            break;
+        case 'n':
+            fNaive ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" );
+        return 1;
+    }
+
+
+    Abc_NtkAutoPrint( pNtk, Output, fNaive, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: print_auto [-O num] [-nvh]\n" );
+    fprintf( pErr, "\t         computes autosymmetries of the PO functions\n" );
+    fprintf( pErr, "\t-O num : (optional) the 0-based number of the output [default = all]\n");
+    fprintf( pErr, "\t-n     : enable naive BDD-based computation [default = %s].\n", fNaive? "yes": "no" );  
+    fprintf( pErr, "\t-v     : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -894,7 +1052,7 @@ int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     extern void Abc_NodePrintKMap( Abc_Obj_t * pNode, int fUseRealNames );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -981,7 +1139,7 @@ int Abc_CommandPrintGates( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     extern void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -1044,7 +1202,7 @@ int Abc_CommandPrintSharing( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     extern void Abc_NtkPrintSharing( Abc_Ntk_t * pNtk );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -1106,7 +1264,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     extern void Abc_NodeShowBdd( Abc_Obj_t * pNode );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -1194,7 +1352,7 @@ int Abc_CommandShowCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nConeSizeMax;
     extern void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -1295,7 +1453,7 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Abc_NtkShowAig( Abc_Ntk_t * pNtk );
     extern void Abc_NtkShowMulti( Abc_Ntk_t * pNtk );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -1369,7 +1527,7 @@ int Abc_CommandShowNtk( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fGateNames;
     extern void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -1432,7 +1590,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -1506,7 +1664,7 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fAllNodes;
     int fCleanup;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -1573,22 +1731,27 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes, * pNtkTemp;
     int c;
-    int fDuplicate;
+    bool fDuplicate;
+    bool fSelective;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
     fDuplicate = 0;
+    fSelective = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "dh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "dsh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'd':
             fDuplicate ^= 1;
             break;
+        case 's':
+            fSelective ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -1610,7 +1773,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
     // get the new network
     if ( Abc_NtkIsStrash(pNtk) )
     {
-        pNtkRes = Abc_NtkBalance( pNtk, fDuplicate );
+        pNtkRes = Abc_NtkBalance( pNtk, fDuplicate, fSelective );
     }
     else
     {
@@ -1620,7 +1783,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "Strashing before balancing has failed.\n" );
             return 1;
         }
-        pNtkRes = Abc_NtkBalance( pNtkTemp, fDuplicate );
+        pNtkRes = Abc_NtkBalance( pNtkTemp, fDuplicate, fSelective );
         Abc_NtkDelete( pNtkTemp );
     }
 
@@ -1635,9 +1798,10 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: balance [-dh]\n" );
+    fprintf( pErr, "usage: balance [-dsh]\n" );
     fprintf( pErr, "\t        transforms the current network into a well-balanced AIG\n" );
     fprintf( pErr, "\t-d    : toggle duplication of logic [default = %s]\n", fDuplicate? "yes": "no" );
+    fprintf( pErr, "\t-s    : toggle duplication on the critical paths [default = %s]\n", fSelective? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -1662,7 +1826,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fMulti;
     int fSimple;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -1769,7 +1933,7 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -1824,7 +1988,7 @@ int Abc_CommandSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -1883,7 +2047,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p );
     extern void Abc_NtkFxuFreeInfo( Fxu_Data_t * p );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -2010,7 +2174,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort );
     extern int         Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -2136,7 +2300,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Rwr_Precompute();
     extern int  Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -2233,7 +2397,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
     bool fVerbose;
     extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -2351,7 +2515,7 @@ int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -2420,7 +2584,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fCheck;
     int fComb;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -2491,7 +2655,7 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nFrames;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -2575,7 +2739,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -2635,7 +2799,7 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -2696,7 +2860,7 @@ int Abc_CommandReorder( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerbose;
     extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -2757,7 +2921,7 @@ int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -2825,7 +2989,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerbose;
     int nSeconds;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -2887,7 +3051,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
 */
     if ( Abc_NtkIsStrash(pNtk) )
     {
-        RetValue = Abc_NtkMiterSat2( pNtk, nSeconds, fVerbose );
+        RetValue = Abc_NtkMiterSat( pNtk, nSeconds, fVerbose );
         if ( RetValue == -1 )
             printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
         else if ( RetValue == 0 )
@@ -2899,7 +3063,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Abc_Ntk_t * pTemp;
         pTemp = Abc_NtkStrash( pNtk, 0, 0 );
-        RetValue = Abc_NtkMiterSat2( pTemp, nSeconds, fVerbose );
+        RetValue = Abc_NtkMiterSat( pTemp, nSeconds, fVerbose );
         if ( RetValue == -1 )
             printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
         else if ( RetValue == 0 )
@@ -2939,7 +3103,7 @@ int Abc_CommandExtSeqDcs( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerbose;
     extern int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNet, bool fVerbose );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -3010,7 +3174,7 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fUseAllCis;
     int Output;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -3122,7 +3286,7 @@ int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Obj_t * pNode;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -3202,7 +3366,7 @@ int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -3251,7 +3415,7 @@ int Abc_CommandExdcFree( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -3311,7 +3475,7 @@ int Abc_CommandExdcGet( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -3369,7 +3533,7 @@ int Abc_CommandExdcSet( Abc_Frame_t * pAbc, int argc, char ** argv )
     char * FileName;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -3461,7 +3625,7 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
     extern void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * pCutOracle );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -3591,7 +3755,7 @@ int Abc_CommandScut( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     extern Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -3696,7 +3860,7 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nFaninMax;
     extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -3784,9 +3948,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
-    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
+//    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -3819,7 +3983,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    printf( "This command is currently not used.\n" );
     // run the command
 //    pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
-    pNtkRes = Abc_NtkNewAig( pNtk );
+
+//    pNtkRes = Abc_NtkNewAig( pNtk );
+    pNtkRes = NULL;
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -3859,7 +4025,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fExdc;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -4017,7 +4183,7 @@ int Abc_CommandFraigTrust( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fDuplicate;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -4081,7 +4247,7 @@ int Abc_CommandFraigStore( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fDuplicate;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -4142,7 +4308,7 @@ int Abc_CommandFraigRestore( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fDuplicate;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -4206,7 +4372,7 @@ int Abc_CommandFraigClean( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fDuplicate;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -4258,7 +4424,7 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerbose;
     extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -4345,7 +4511,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fSwitching, int fVerbose );
     extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -4410,7 +4576,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "Strashing before mapping has failed.\n" );
             return 1;
         }
-        pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0 );
+        pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0 );
         Abc_NtkDelete( pNtkRes );
         if ( pNtk == NULL )
         {
@@ -4481,7 +4647,7 @@ int Abc_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     extern int Abc_NtkUnmap( Abc_Ntk_t * pNtk );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -4542,7 +4708,7 @@ int Abc_CommandAttach( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     extern int Abc_NtkUnmap( Abc_Ntk_t * pNtk );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -4605,7 +4771,7 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -4678,7 +4844,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     extern Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int fSwitching, int fVerbose );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -4740,7 +4906,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
             return 1;
         }
-        pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0 );
+        pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0 );
         Abc_NtkDelete( pNtkRes );
         if ( pNtk == NULL )
         {
@@ -4806,7 +4972,7 @@ int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     extern Abc_Ntk_t * Abc_NtkPga( Pga_Params_t * pParams );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -4863,7 +5029,7 @@ int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
             return 1;
         }
-        pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0 );
+        pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0 );
         Abc_NtkDelete( pNtkRes );
         if ( pNtk == NULL )
         {
@@ -4931,7 +5097,7 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fRandom;
     int fDontCare;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -5039,7 +5205,7 @@ int Abc_CommandPipe( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nLatches;
     extern void Abc_NtkLatchPipe( Abc_Ntk_t * pNtk, int nLatches );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -5115,7 +5281,7 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -5192,7 +5358,7 @@ int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fShare;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -5269,7 +5435,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fInitial;
     int fVerbose;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -5395,7 +5561,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c, nMaxIters;
     int fVerbose;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -5459,7 +5625,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
 
-        pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0 );
+        pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0, 0 );
         Abc_NtkDelete( pNtkRes );
         if ( pNtkNew == NULL )
         {
@@ -5519,7 +5685,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c, nMaxIters;
     int fVerbose;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -5583,7 +5749,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
 
-        pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0 );
+        pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0, 0 );
         Abc_NtkDelete( pNtkRes );
         if ( pNtkNew == NULL )
         {
@@ -5649,7 +5815,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose );
     extern Abc_Ntk_t * Abc_NtkVanImp( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose );
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -5756,7 +5922,7 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -5822,7 +5988,7 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose );
 
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -5914,7 +6080,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose );
 
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c
new file mode 100644
index 00000000..752943c3
--- /dev/null
+++ b/src/base/abci/abcAuto.c
@@ -0,0 +1,229 @@
+/**CFile****************************************************************
+
+  FileName    [abcAuto.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Computation of autosymmetries.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcAuto.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int nOutputs, char * pInputNames[], char * pOutputNames[], int fNaive );
+static void Abc_NtkAutoPrintOne( DdManager * dd, int nInputs, DdNode * pbOutputs[], int Output, char * pInputNames[], char * pOutputNames[], int fNaive );
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
+{
+    DdManager * dd;         // the BDD manager used to hold shared BDDs
+    DdNode ** pbGlobal;     // temporary storage for global BDDs
+    char ** pInputNames;    // pointers to the CI names
+    char ** pOutputNames;   // pointers to the CO names
+    int nOutputs, nInputs, i;
+
+    // compute the global BDDs
+    if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
+        return;
+
+    // get information about the network
+    nInputs  = Abc_NtkCiNum(pNtk);
+    nOutputs = Abc_NtkCoNum(pNtk);
+    dd       = pNtk->pManGlob;
+    pbGlobal = (DdNode **)Vec_PtrArray( pNtk->vFuncsGlob );
+
+    // get the network names
+    pInputNames = Abc_NtkCollectCioNames( pNtk, 0 );
+    pOutputNames = Abc_NtkCollectCioNames( pNtk, 1 );
+
+    // print the size of the BDDs
+    if ( fVerbose )
+        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+
+    // allocate additional variables
+    for ( i = 0; i < nInputs; i++ )
+        Cudd_bddNewVar( dd );
+    assert( Cudd_ReadSize(dd) == 2 * nInputs );
+
+    // create ZDD variables in the manager
+    Cudd_zddVarsFromBddVars( dd, 2 );
+
+    // perform the analysis of the primary output functions for auto-symmetry
+    if ( Output == -1 )
+        Abc_NtkAutoPrintAll( dd, nInputs, pbGlobal, nOutputs, pInputNames, pOutputNames, fNaive );
+    else
+        Abc_NtkAutoPrintOne( dd, nInputs, pbGlobal, Output, pInputNames, pOutputNames, fNaive );
+
+    // deref the PO functions
+    Abc_NtkFreeGlobalBdds( pNtk );
+    // stop the global BDD manager
+    Extra_StopManager( pNtk->pManGlob );
+    pNtk->pManGlob = NULL;
+    free( pInputNames );
+    free( pOutputNames );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int nOutputs, char * pInputNames[], char * pOutputNames[], int fNaive )
+{
+    DdNode * bSpace1, * bSpace2, * bCanVars, * bReduced, * zEquations;
+    double nMints; 
+    int nSupp, SigCounter, o;
+
+    int nAutos;
+    int nAutoSyms;
+    int nAutoSymsMax;
+    int nAutoSymsMaxSupp;
+    int nAutoSymOuts;
+    int nSuppSizeMax;
+    int clk;
+    
+    nAutoSymOuts = 0;
+    nAutoSyms    = 0;
+    nAutoSymsMax = 0;
+    nAutoSymsMaxSupp = 0;
+    nSuppSizeMax = 0;
+    clk = clock();
+
+    SigCounter = 0;
+    for ( o = 0; o < nOutputs; o++ )
+    {
+        bSpace1  = Extra_bddSpaceFromFunctionFast( dd, pbOutputs[o] );           Cudd_Ref( bSpace1 );
+//        bSpace1  = Extra_bddSpaceFromFunction( dd, pbOutputs[o], pbOutputs[o] ); Cudd_Ref( bSpace1 );
+        bCanVars = Extra_bddSpaceCanonVars( dd, bSpace1 );                       Cudd_Ref( bCanVars );
+        bReduced = Extra_bddSpaceReduce( dd, pbOutputs[o], bCanVars );           Cudd_Ref( bReduced );
+        zEquations = Extra_bddSpaceEquations( dd, bSpace1 );                     Cudd_Ref( zEquations );
+
+        nSupp  = Cudd_SupportSize( dd, bSpace1 );
+        nMints = Cudd_CountMinterm( dd, bSpace1, nSupp );
+        nAutos = Extra_Base2LogDouble(nMints);
+        printf( "Output #%3d: Inputs = %2d. AutoK = %2d.\n", o, nSupp, nAutos );
+
+        if ( nAutos > 0 )
+        {
+            nAutoSymOuts++;
+            nAutoSyms += nAutos;
+            if ( nAutoSymsMax < nAutos )
+            {
+                nAutoSymsMax = nAutos;
+                nAutoSymsMaxSupp = nSupp;
+            }
+        }
+        if ( nSuppSizeMax < nSupp )
+            nSuppSizeMax = nSupp;
+
+
+//PRB( dd, bCanVars );
+//PRB( dd, bReduced );
+//Cudd_PrintMinterm( dd, bReduced );
+//printf( "The equations are:\n" );
+//Cudd_zddPrintCover( dd, zEquations );
+//printf( "\n" );
+//fflush( stdout );
+
+        bSpace2 = Extra_bddSpaceFromMatrixPos( dd, zEquations );   Cudd_Ref( bSpace2 );
+//PRB( dd, bSpace1 );
+//PRB( dd, bSpace2 );
+        if ( bSpace1 != bSpace2 )
+            printf( "Spaces are NOT EQUAL!\n" );
+//        else
+//            printf( "Spaces are equal.\n" );
+    
+        Cudd_RecursiveDeref( dd, bSpace1 );
+        Cudd_RecursiveDeref( dd, bSpace2 );
+        Cudd_RecursiveDeref( dd, bCanVars );
+        Cudd_RecursiveDeref( dd, bReduced );
+        Cudd_RecursiveDerefZdd( dd, zEquations );
+    }
+
+    printf( "The cumulative statistics for all outputs:\n" );
+    printf( "Ins=%3d ",      nInputs );
+    printf( "InMax=%3d   ",  nSuppSizeMax );
+    printf( "Outs=%3d ",     nOutputs );
+    printf( "Auto=%3d   ",   nAutoSymOuts );
+    printf( "SumK=%3d ",     nAutoSyms );
+    printf( "KMax=%2d ",     nAutoSymsMax );
+    printf( "Supp=%3d   ",   nAutoSymsMaxSupp );
+    printf( "Time=%4.2f ", (float)(clock() - clk)/(float)(CLOCKS_PER_SEC) );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkAutoPrintOne( DdManager * dd, int nInputs, DdNode * pbOutputs[], int Output, char * pInputNames[], char * pOutputNames[], int fNaive )
+{
+    DdNode * bSpace1, * bCanVars, * bReduced, * zEquations;
+    double nMints; 
+    int nSupp, SigCounter;
+    int nAutos;
+
+    SigCounter = 0;
+    bSpace1  = Extra_bddSpaceFromFunctionFast( dd, pbOutputs[Output] );                Cudd_Ref( bSpace1 );
+//    bSpace1  = Extra_bddSpaceFromFunction( dd, pbOutputs[Output], pbOutputs[Output] ); Cudd_Ref( bSpace1 );
+    bCanVars = Extra_bddSpaceCanonVars( dd, bSpace1 );                                 Cudd_Ref( bCanVars );
+    bReduced = Extra_bddSpaceReduce( dd, pbOutputs[Output], bCanVars );                Cudd_Ref( bReduced );
+    zEquations = Extra_bddSpaceEquations( dd, bSpace1 );                               Cudd_Ref( zEquations );
+
+    nSupp  = Cudd_SupportSize( dd, bSpace1 );
+    nMints = Cudd_CountMinterm( dd, bSpace1, nSupp );
+    nAutos = Extra_Base2LogDouble(nMints);
+    printf( "Output #%3d: Inputs = %2d. AutoK = %2d.\n", Output, nSupp, nAutos );
+
+    Cudd_RecursiveDeref( dd, bSpace1 );
+    Cudd_RecursiveDeref( dd, bCanVars );
+    Cudd_RecursiveDeref( dd, bReduced );
+    Cudd_RecursiveDerefZdd( dd, zEquations );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index fed89dbb..effae853 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -24,10 +24,11 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
  
-static void        Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate );
-static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, bool fDuplicate );
-static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int Level, int fDuplicate );
-static int         Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate );
+static void        Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate, bool fSelective );
+static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, bool fDuplicate, bool fSelective );
+static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int Level, int fDuplicate, bool fSelective );
+static int         Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate, bool fSelective );
+static void        Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -44,14 +45,26 @@ static int         Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSupe
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate )
+Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective )
 {
     Abc_Ntk_t * pNtkAig;
     assert( Abc_NtkIsStrash(pNtk) );
+    // compute the required times
+    if ( fSelective )
+    {
+        Abc_NtkStartReverseLevels( pNtk );
+        Abc_NtkMarkCriticalNodes( pNtk );
+    }
     // perform balancing
     pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
-    Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate );
+    Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate, fSelective );
     Abc_NtkFinalize( pNtk, pNtkAig );
+    // undo the required times
+    if ( fSelective )
+    {
+        Abc_NtkStopReverseLevels( pNtk );
+        Abc_NtkCleanMarkA( pNtk );
+    }
     if ( pNtk->pExdc )
         pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
     // make sure everything is okay
@@ -75,7 +88,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate )
+void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate, bool fSelective )
 {
     int fCheck = 1;
     ProgressBar * pProgress;
@@ -94,7 +107,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         // strash the driver node
         pDriver = Abc_ObjFanin0(pNode);
-        Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, 0, fDuplicate );
+        Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, 0, fDuplicate, fSelective );
     }
     Extra_ProgressBarStop( pProgress );
     Vec_VecFree( vStorage );
@@ -147,7 +160,7 @@ void Abc_NodeBalanceRandomize( Vec_Ptr_t * vSuper )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, int Level, bool fDuplicate )
+Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, int Level, bool fDuplicate, bool fSelective )
 {
     Abc_Aig_t * pMan = pNtkNew->pManFunc;
     Abc_Obj_t * pNodeNew, * pNode1, * pNode2;
@@ -159,7 +172,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
         return pNodeOld->pCopy;
     assert( Abc_ObjIsNode(pNodeOld) );
     // get the implication supergate
-    vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, Level, fDuplicate );
+    vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, Level, fDuplicate, fSelective );
     if ( vSuper->nSize == 0 )
     { // it means that the supergate contains two nodes in the opposite polarity
         pNodeOld->pCopy = Abc_ObjNot(Abc_NtkConst1(pNtkNew));
@@ -168,7 +181,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
     // for each old node, derive the new well-balanced node
     for ( i = 0; i < vSuper->nSize; i++ )
     {
-        pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, Level + 1, fDuplicate );
+        pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, Level + 1, fDuplicate, fSelective );
         vSuper->pArray[i] = Abc_ObjNotCond( pNodeNew, Abc_ObjIsComplement(vSuper->pArray[i]) );
     }
     if ( vSuper->nSize < 2 )
@@ -207,7 +220,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, int fDuplicate )
+Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, int fDuplicate, bool fSelective )
 {
     Vec_Ptr_t * vNodes;
     int RetValue, i;
@@ -219,7 +232,7 @@ Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Le
     vNodes = Vec_VecEntry( vStorage, Level );
     Vec_PtrClear( vNodes );
     // collect the nodes in the implication supergate
-    RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, fDuplicate );
+    RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, fDuplicate, fSelective );
     assert( vNodes->nSize > 1 );
     // unmark the visited nodes
     for ( i = 0; i < vNodes->nSize; i++ )
@@ -245,7 +258,7 @@ Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Le
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate )
+int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate, bool fSelective )
 {
     int RetValue1, RetValue2, i;
     // check if the node is visited
@@ -263,7 +276,7 @@ int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst,
         return 0;
     }
     // if the new node is complemented or a PI, another gate begins
-    if ( !fFirst && (Abc_ObjIsComplement(pNode) || !Abc_ObjIsNode(pNode) || !fDuplicate && (Abc_ObjFanoutNum(pNode) > 1)) )
+    if ( !fFirst && (Abc_ObjIsComplement(pNode) || !Abc_ObjIsNode(pNode) || !fDuplicate && !fSelective && (Abc_ObjFanoutNum(pNode) > 1)) )
     {
         Vec_PtrPush( vSuper, pNode );
         Abc_ObjRegular(pNode)->fMarkB = 1;
@@ -272,8 +285,8 @@ int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst,
     assert( !Abc_ObjIsComplement(pNode) );
     assert( Abc_ObjIsNode(pNode) );
     // go through the branches
-    RetValue1 = Abc_NodeBalanceCone_rec( Abc_ObjChild0(pNode), vSuper, 0, fDuplicate );
-    RetValue2 = Abc_NodeBalanceCone_rec( Abc_ObjChild1(pNode), vSuper, 0, fDuplicate );
+    RetValue1 = Abc_NodeBalanceCone_rec( Abc_ObjChild0(pNode), vSuper, 0, fDuplicate, fSelective );
+    RetValue2 = Abc_NodeBalanceCone_rec( Abc_ObjChild1(pNode), vSuper, 0, fDuplicate, fSelective );
     if ( RetValue1 == -1 || RetValue2 == -1 )
         return -1;
     // return 1 if at least one branch has a duplicate
@@ -315,7 +328,7 @@ Vec_Ptr_t * Abc_NodeFindCone_rec( Abc_Obj_t * pNode )
     else
     {
         // collect the nodes in the implication supergate
-        RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, 1 );
+        RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, 1, 0 );
         assert( vNodes->nSize > 1 );
         // unmark the visited nodes
         Vec_PtrForEachEntry( vNodes, pNode, i )
@@ -442,6 +455,28 @@ void Abc_NtkBalanceLevel( Abc_Ntk_t * pNtk )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Marks the nodes on the critical and near critical paths.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i, Counter = 0;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( Abc_NodeReadRequiredLevel(pNode) - pNode->Level <= 1 )
+            pNode->fMarkA = 1, Counter++;
+    printf( "The number of nodes on the critical paths = %6d  (%5.2f %%)\n", Counter, 100.0 * Counter / Abc_NtkNodeNum(pNtk) );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 5c7f0d48..a73ab2b5 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -172,6 +172,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
     int i, nNodesDsd;
 
     // save the CI nodes in the DSD nodes
+    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NtkConst1(pNtk)->pCopy );
     Abc_NtkForEachCi( pNtk, pNode, i )
     {
         pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 39bf15aa..128e054a 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -105,7 +105,7 @@ clk = clock();
         Map_ManFree( pMan );
         return NULL;
     }
-//    Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), clock()-clk );
+    Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), clock()-clk );
 
     // reconstruct the network after mapping
     pNtkNew = Abc_NtkFromMap( pMan, pNtk );
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index c1f83e1f..ea2f808c 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -173,6 +173,8 @@ Abc_Obj_t * Abc_NtkRenode_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
     assert( !Abc_NodeIsConst(pNodeOld) );
     assert( pNodeOld->fMarkA );
 
+//printf( "%d ", Abc_NodeMffcSizeSupp(pNodeOld) );
+
     // collect the renoding cone
     vCone = Vec_PtrAlloc( 10 );
     Abc_NtkRenodeCone( pNodeOld, vCone );
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index f7b9892e..9c650aa9 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -29,6 +29,8 @@ static int  Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t *
 
 static solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk );
 
+static Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
+
 static nMuxes;
 
 ////////////////////////////////////////////////////////////////////////
@@ -46,7 +48,7 @@ static nMuxes;
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
+int Abc_NtkMiterSat_OldAndRusty( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
 {
     solver * pSat;
     lbool   status;
@@ -317,7 +319,7 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMiterSat2( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
+int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
 {
     solver * pSat;
     lbool   status;
@@ -376,7 +378,8 @@ int Abc_NtkMiterSat2( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
     // if the problem is SAT, get the counterexample
     if ( status == l_True )
     {
-        Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
+//        Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
+        Vec_Int_t * vCiIds = Abc_NtkGetCiSatVarNums( pNtk );
         pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize );
         Vec_IntFree( vCiIds );
     }
@@ -385,6 +388,28 @@ int Abc_NtkMiterSat2( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of CI IDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk )
+{
+    Vec_Int_t * vCiIds;
+    Abc_Obj_t * pObj;
+    int i;
+    vCiIds = Vec_IntAlloc( Abc_NtkCiNum(pNtk) );
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        Vec_IntPush( vCiIds, (int)pObj->pCopy );
+    return vCiIds;
+}
+
 
 
  
diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c
new file mode 100644
index 00000000..08a42623
--- /dev/null
+++ b/src/base/abci/abcUnate.c
@@ -0,0 +1,150 @@
+/**CFile****************************************************************
+
+  FileName    [abcUnate.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcUnate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose );
+static void Abc_NtkPrintUnateSat( Abc_Ntk_t * pNtk, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Detects unate variables of the multi-output function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintUnate( Abc_Ntk_t * pNtk, int fUseBdds, int fUseNaive, int fVerbose )
+{
+    if ( fUseBdds || fUseNaive )
+        Abc_NtkPrintUnateBdd( pNtk, fUseNaive, fVerbose );
+    else
+        Abc_NtkPrintUnateSat( pNtk, fVerbose );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Detects unate variables using BDDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose )
+{
+    Abc_Obj_t * pNode;
+    Extra_UnateInfo_t * p;
+    DdManager * dd;         // the BDD manager used to hold shared BDDs
+    DdNode ** pbGlobal;     // temporary storage for global BDDs
+    int TotalSupps = 0;
+    int TotalUnate = 0;
+    int i, clk = clock();
+    int clkBdd, clkUnate;
+
+    // compute the global BDDs
+    if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
+        return;
+clkBdd = clock() - clk;
+
+    // get information about the network
+    dd       = pNtk->pManGlob;
+    pbGlobal = (DdNode **)Vec_PtrArray( pNtk->vFuncsGlob );
+
+    // print the size of the BDDs
+    printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+
+    // perform naive BDD-based computation
+    if ( fUseNaive )
+    {
+        Abc_NtkForEachCo( pNtk, pNode, i )
+        {
+            p = Extra_UnateComputeSlow( dd, pbGlobal[i] );
+            if ( fVerbose )
+                Extra_UnateInfoPrint( p );
+            TotalSupps += p->nVars;
+            TotalUnate += p->nUnate;
+            Extra_UnateInfoDissolve( p );
+        }
+    }
+    // perform smart BDD-based computation
+    else 
+    {
+        // create ZDD variables in the manager
+        Cudd_zddVarsFromBddVars( dd, 2 );
+        Abc_NtkForEachCo( pNtk, pNode, i )
+        {
+            p = Extra_UnateComputeFast( dd, pbGlobal[i] );
+            if ( fVerbose )
+                Extra_UnateInfoPrint( p );
+            TotalSupps += p->nVars;
+            TotalUnate += p->nUnate;
+            Extra_UnateInfoDissolve( p );
+        }
+    }
+clkUnate = clock() - clk - clkBdd;
+
+    // print stats
+    printf( "Ins/Outs = %4d/%4d.  Total supp = %5d.  Total unate = %5d.\n",
+        Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), TotalSupps, TotalUnate );
+    PRT( "Glob BDDs", clkBdd );
+    PRT( "Unateness", clkUnate );
+    PRT( "Total    ", clock() - clk );
+
+    // deref the PO functions
+    Abc_NtkFreeGlobalBdds( pNtk );
+    // stop the global BDD manager
+    Extra_StopManager( pNtk->pManGlob );
+    pNtk->pManGlob = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Detects unate variables using SAT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintUnateSat( Abc_Ntk_t * pNtk, int fVerbose )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index b30a6452..99392e48 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -148,9 +148,9 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     Fraig_ParamsSetDefault( &Params );
     Params.fVerbose = fVerbose;
     Params.nSeconds = nSeconds;
-    Params.fFuncRed = 0;
-    Params.nPatsRand = 0;
-    Params.nPatsDyna = 0;
+//    Params.fFuncRed = 0;
+//    Params.nPatsRand = 0;
+//    Params.nPatsDyna = 0;
     pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
     Fraig_ManProveMiter( pMan );
 
@@ -328,9 +328,9 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
     Fraig_ParamsSetDefault( &Params );
     Params.fVerbose = fVerbose;
     Params.nSeconds = nSeconds;
-    Params.fFuncRed = 0;
-    Params.nPatsRand = 0;
-    Params.nPatsDyna = 0;
+//    Params.fFuncRed = 0;
+//    Params.nPatsRand = 0;
+//    Params.nPatsDyna = 0;
     pMan = Abc_NtkToFraig( pFrames, &Params, 0, 0 ); 
     Fraig_ManProveMiter( pMan );
 
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 660aee63..5b15641b 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -1,5 +1,6 @@
 SRC +=    src/base/abci/abc.c \
     src/base/abci/abcAttach.c \
+    src/base/abci/abcAuto.c \
     src/base/abci/abcBalance.c \
     src/base/abci/abcCollapse.c \
     src/base/abci/abcCut.c \
@@ -21,6 +22,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcSweep.c \
     src/base/abci/abcSymm.c \
     src/base/abci/abcTiming.c \
+    src/base/abci/abcUnate.c \
     src/base/abci/abcUnreach.c \
     src/base/abci/abcVanEijk.c \
     src/base/abci/abcVanImp.c \
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index f20855ab..b2a90806 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1204,7 +1204,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
     char * pSisName;
     int i;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
@@ -1340,7 +1340,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
     char * pMvsisName;
     int i;
 
-    pNtk = Abc_FrameReadNet(pAbc);
+    pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
diff --git a/src/base/io/io.h b/src/base/io/io.h
index 286b570c..fe5c237f 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -69,6 +69,7 @@ extern Abc_Obj_t *        Io_ReadCreateNode( Abc_Ntk_t * pNtk, char * pNameOut,
 extern Abc_Obj_t *        Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 );
 extern Abc_Obj_t *        Io_ReadCreateInv( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut );
 extern Abc_Obj_t *        Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut );
+extern FILE *             Io_FileOpen( const char * FileName, const char * PathVar, const char * Mode, int fVerbose );
 /*=== abcWriteBaf.c ==========================================================*/
 extern void               Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
 /*=== abcWriteBlif.c ==========================================================*/
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index d8ad8f71..1cb0ae5d 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -47,7 +47,7 @@ Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck )
     Abc_Ntk_t * pNtk;
 
     // start the file
-    p = Extra_FileReaderAlloc( pFileName, "#", "\n", " \t\r,()=" );
+    p = Extra_FileReaderAlloc( pFileName, "#", "\n\r", " \t,()=" );
     if ( p == NULL )
         return NULL;
 
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index b8a2ed01..c05f444e 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -135,7 +135,8 @@ Io_ReadBlif_t * Io_ReadBlifFile( char * pFileName )
     Io_ReadBlif_t * p;
 
     // start the reader
-    pReader = Extra_FileReaderAlloc( pFileName, "#", "\n", " \t\r" );
+    pReader = Extra_FileReaderAlloc( pFileName, "#", "\n\r", " \t" );
+
     if ( pReader == NULL )
         return NULL;
 
diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c
index a2a2f527..f100a45f 100644
--- a/src/base/io/ioReadEdif.c
+++ b/src/base/io/ioReadEdif.c
@@ -47,7 +47,7 @@ Abc_Ntk_t * Io_ReadEdif( char * pFileName, int fCheck )
     Abc_Ntk_t * pNtk;
 
     // start the file
-    p = Extra_FileReaderAlloc( pFileName, "#", "\n", " \t\r()" );
+    p = Extra_FileReaderAlloc( pFileName, "#", "\n\r", " \t()" );
     if ( p == NULL )
         return NULL;
 
diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c
index 387f8730..0413dc8f 100644
--- a/src/base/io/ioReadPla.c
+++ b/src/base/io/ioReadPla.c
@@ -47,7 +47,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck )
     Abc_Ntk_t * pNtk;
 
     // start the file
-    p = Extra_FileReaderAlloc( pFileName, "#", "\n", " \t\r|" );
+    p = Extra_FileReaderAlloc( pFileName, "#", "\n\r", " \t|" );
     if ( p == NULL )
         return NULL;
 
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index 342dfbaf..e817bee8 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -194,6 +194,61 @@ Abc_Obj_t * Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut
     return pNet;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Provide an fopen replacement with path lookup]
+
+  Description [Provide an fopen replacement where the path stored
+               in pathvar MVSIS variable is used to look up the path
+               for name. Returns NULL if file cannot be opened.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+FILE * Io_FileOpen( const char * FileName, const char * PathVar, const char * Mode, int fVerbose )
+{
+    char * t = 0, * c = 0, * i;
+    extern char * Abc_FrameReadFlag( char * pFlag ); 
+
+    if ( PathVar == 0 )
+    {
+        return fopen( FileName, Mode );
+    }
+    else
+    {
+        if ( c = Abc_FrameReadFlag( (char*)PathVar ) )
+        {
+            char ActualFileName[4096];
+            FILE * fp = 0;
+            t = util_strsav( c );
+            for (i = strtok( t, ":" ); i != 0; i = strtok( 0, ":") )
+            {
+#ifdef WIN32
+                _snprintf ( ActualFileName, 4096, "%s/%s", i, FileName );
+#else
+                snprintf ( ActualFileName, 4096, "%s/%s", i, FileName );
+#endif
+                if ( ( fp = fopen ( ActualFileName, Mode ) ) )
+                {
+                    if ( fVerbose )
+                    fprintf ( stdout, "Using file %s\n", ActualFileName );
+                    free( t );
+                    return fp;
+                }
+            }
+            free( t );
+            return 0;
+        }
+        else
+        {
+            return fopen( FileName, Mode );
+        }
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/module.make b/src/base/io/module.make
index 21579266..8693c8eb 100644
--- a/src/base/io/module.make
+++ b/src/base/io/module.make
@@ -16,4 +16,5 @@ SRC +=  src/base/io/io.c \
     src/base/io/ioWriteEqn.c \
     src/base/io/ioWriteGml.c \
     src/base/io/ioWriteList.c \
-    src/base/io/ioWritePla.c
+    src/base/io/ioWritePla.c \
+    src/base/io/ioWriteVerilog.c
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 4c572a07..a9f27bf8 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -217,7 +217,7 @@ int main( int argc, char * argv[] )
                 break;
         }
     }
-     
+      
     // if the memory should be freed, quit packages
     if ( fStatus < 0 ) 
     {
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 4280808d..c5f311aa 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -78,7 +78,7 @@ extern void            Abc_Start();
 extern void            Abc_Stop();
 
 /*=== mainFrame.c ===========================================================*/
-extern Abc_Ntk_t *     Abc_FrameReadNet( Abc_Frame_t * p );
+extern Abc_Ntk_t *     Abc_FrameReadNtk( Abc_Frame_t * p );
 extern FILE *          Abc_FrameReadOut( Abc_Frame_t * p );
 extern FILE *          Abc_FrameReadErr( Abc_Frame_t * p );
 extern bool            Abc_FrameReadMode( Abc_Frame_t * p );
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index f75df49e..e9e243af 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -164,7 +164,7 @@ void Abc_FrameRestart( Abc_Frame_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_FrameReadNet( Abc_Frame_t * p )
+Abc_Ntk_t * Abc_FrameReadNtk( Abc_Frame_t * p )
 {
     return p->pNtkCur;
 }
diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c
index b1f66721..ed2a33fc 100644
--- a/src/base/seq/seqAigCore.c
+++ b/src/base/seq/seqAigCore.c
@@ -351,11 +351,13 @@ int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int
     printf( "The number of ANDs in the AIG = %5d.\n", Abc_NtkNodeNum(pNtkMiter) );
 
     // transform the miter into a logic network for efficient CNF construction
-    pNtkCnf = Abc_NtkRenode( pNtkMiter, 0, 100, 1, 0, 0 );
-    Abc_NtkDelete( pNtkMiter );
+//    pNtkCnf = Abc_NtkRenode( pNtkMiter, 0, 100, 1, 0, 0 );
+//    Abc_NtkDelete( pNtkMiter );
+    pNtkCnf = pNtkMiter;
 
     // solve the miter
 clk = clock();
+//    RetValue = Abc_NtkMiterSat_OldAndRusty( pNtkCnf, 30, 0 );
     RetValue = Abc_NtkMiterSat( pNtkCnf, 30, 0 );
 if ( fVerbose )
 if ( clock() - clk > 100 )