Version abc50905

author: Alan Mishchenko <alanmi@berkeley.edu> 2005-09-05 08:01:00 -0700
committer: Alan Mishchenko <alanmi@berkeley.edu> 2005-09-05 08:01:00 -0700
commit: 1260d20cc05fe2d21088cc047c460e85ccdb3b14 (patch)
tree: f10ccc3333f78b6e2e089a88c8cf61a47b2f2dcd /src/base
parent: 33012d9530c40817e1fc5230b3e663f7690b2e94 (diff)
download: abc-1260d20cc05fe2d21088cc047c460e85ccdb3b14.tar.gz
abc-1260d20cc05fe2d21088cc047c460e85ccdb3b14.tar.bz2
abc-1260d20cc05fe2d21088cc047c460e85ccdb3b14.zip
41 files changed, 424 insertions, 370 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index bff4f9f1..aea5a62d 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -413,6 +413,7 @@ extern int                Abc_NtkAttach( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate );
 /*=== abcCheck.c ==========================================================*/
 extern bool               Abc_NtkCheck( Abc_Ntk_t * pNtk );
+extern bool               Abc_NtkCheckRead( Abc_Ntk_t * pNtk );
 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 ==========================================================*/
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index c5f644d2..1d23d7ed 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -25,6 +25,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
 static bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk );
 static bool Abc_NtkCheckPis( Abc_Ntk_t * pNtk );
 static bool Abc_NtkCheckPos( Abc_Ntk_t * pNtk );
@@ -54,6 +55,38 @@ static bool Abc_NtkCompareLatches( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fCo
 ***********************************************************************/
 bool Abc_NtkCheck( Abc_Ntk_t * pNtk )
 {
+   return !Abc_FrameIsFlagEnabled( "check" ) || Abc_NtkDoCheck( pNtk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks the integrity of the network after reading.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkCheckRead( Abc_Ntk_t * pNtk )
+{
+   return !Abc_FrameIsFlagEnabled( "checkread" ) || Abc_NtkDoCheck( pNtk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks the integrity of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
+{
     Abc_Obj_t * pObj, * pNet, * pNode;
     int i;
 
@@ -402,6 +435,9 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
         }
     }
 
+    if ( !Abc_FrameIsFlagEnabled("checkfio") )
+        return Value;
+
     // make sure fanins are not duplicated
     for ( i = 0; i < pObj->vFanins.nSize; i++ )
         for ( k = i + 1; k < pObj->vFanins.nSize; k++ )
@@ -412,7 +448,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
             }
 
     // save time: do not check large fanout lists
-    if ( pObj->vFanouts.nSize > 20 )
+    if ( pObj->vFanouts.nSize > 100 )
         return Value;
 
     // make sure fanouts are not duplicated
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 77fbeb38..08ee93bb 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -41,7 +41,6 @@
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pFanin;
     int i, k;
@@ -65,7 +64,7 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
     // duplicate EXDC 
     if ( pNtk->pExdc )
         pNtkNew->pExdc = Abc_NtkNetlistToLogic( pNtk->pExdc );
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkNetlistToLogic(): Network check has failed.\n" );
     return pNtkNew;
 }
@@ -146,7 +145,6 @@ Abc_Ntk_t * Abc_NtkLogicToNetlistBench( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pNet, * pDriver, * pFanin;
     char * pNameCo;
@@ -214,7 +212,7 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
     // duplicate EXDC 
     if ( pNtk->pExdc )
         pNtkNew->pExdc = Abc_NtkLogicToNetlist( pNtk->pExdc );
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkLogicSopToNetlist(): Network check has failed.\n" );
     return pNtkNew;
 }
@@ -232,7 +230,6 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pFanin, * pNodeNew;
     int i, k;
@@ -289,7 +286,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
         else
             pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
     }
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkAigToLogicSop(): Network check has failed.\n" );
     return pNtkNew;
 }
@@ -307,7 +304,6 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pFanin;
     Vec_Ptr_t * vNodes;
@@ -360,7 +356,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
     // duplicate the EXDC Ntk
     if ( pNtk->pExdc )
         printf( "Warning: The EXDc network is skipped.\n" );
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkAigToLogicSopBench(): Network check has failed.\n" );
     return pNtkNew;
 }
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index f869abf3..40c6e7a5 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [abcCreate.c]
+  FileName    [abcObj.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: abcCreate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: abcObj.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index ee59cf43..20a64246 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -23,6 +23,7 @@
 #endif
 
 #include "abc.h"
+#include "main.h"
 #include "io.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -195,22 +196,26 @@ void Abc_ShowFile( char * FileNameDot )
     char * FileGeneric;
     char FileNamePs[200];
     char CommandDot[1000];
-#ifndef WIN32
-    char CommandPs[1000];
-#endif
-    char * pProgDotName;
-    char * pProgGsViewName;
+    char * pDotName;
+    char * pDotNameWin = "dot.exe";
+    char * pDotNameUnix = "dot";
+    char * pGsNameWin = "gsview32.exe";
+    char * pGsNameUnix = "gv";
     int RetValue;
 
+    // get DOT names from the resource file
+    if ( Abc_FrameReadFlag("dotwin") )
+        pDotNameWin = Abc_FrameReadFlag("dotwin");
+    if ( Abc_FrameReadFlag("dotunix") )
+        pDotNameUnix = Abc_FrameReadFlag("dotunix");
+
 #ifdef WIN32
-    pProgDotName = "dot.exe";
-    pProgGsViewName = NULL;
+    pDotName = pDotNameWin;
 #else
-    pProgDotName = "dot";
-    pProgGsViewName = "gv";
+    pDotName = pDotNameUnix;
 #endif
 
-    // check that the input file is okay
+    // check if the input DOT file is okay
     if ( (pFile = fopen( FileNameDot, "r" )) == NULL )
     {
         fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
@@ -218,27 +223,20 @@ void Abc_ShowFile( char * FileNameDot )
     }
     fclose( pFile );
 
-    // get the generic file name
-    FileGeneric = Extra_FileNameGeneric( FileNameDot );
     // create the PostScript file name
+    FileGeneric = Extra_FileNameGeneric( FileNameDot );
     sprintf( FileNamePs,  "%s.ps",  FileGeneric ); 
     free( FileGeneric );
 
-    // generate the DOT file
-    sprintf( CommandDot,  "%s -Tps -o %s %s", pProgDotName, FileNamePs, FileNameDot ); 
+    // generate the PostScript file using DOT
+    sprintf( CommandDot,  "%s -Tps -o %s %s", pDotName, FileNamePs, FileNameDot ); 
     RetValue = system( CommandDot );
-#ifdef WIN32
-        _unlink( FileNameDot );
-#else
-        unlink( FileNameDot );
-#endif
     if ( RetValue == -1 )
     {
-        fprintf( stdout, "Cannot find \"%s\".\n", pProgDotName );
+        fprintf( stdout, "Command \"%s\" did not succeed.\n", CommandDot );
         return;
     }
-
-    // check that the input file is okay
+    // check that the input PostScript file is okay
     if ( (pFile = fopen( FileNamePs, "r" )) == NULL )
     {
         fprintf( stdout, "Cannot open intermediate file \"%s\".\n", FileNamePs );
@@ -246,20 +244,33 @@ void Abc_ShowFile( char * FileNameDot )
     }
     fclose( pFile ); 
 
+
+    // get GSVIEW names from the resource file
+    if ( Abc_FrameReadFlag("gsviewwin") )
+        pGsNameWin = Abc_FrameReadFlag("gsviewwin");
+    if ( Abc_FrameReadFlag("gsviewunix") )
+        pGsNameUnix = Abc_FrameReadFlag("gsviewunix");
+
+    // spawn the viewer
 #ifdef WIN32
-    if ( _spawnl( _P_NOWAIT, "gsview32.exe", "gsview32.exe", FileNamePs, NULL ) == -1 )
+    _unlink( FileNameDot );
+    if ( _spawnl( _P_NOWAIT, pGsNameWin, pGsNameWin, FileNamePs, NULL ) == -1 )
         if ( _spawnl( _P_NOWAIT, "C:\\Program Files\\Ghostgum\\gsview\\gsview32.exe", 
             "C:\\Program Files\\Ghostgum\\gsview\\gsview32.exe", FileNamePs, NULL ) == -1 )
         {
-            fprintf( stdout, "Cannot find \"%s\".\n", "gsview32.exe" );
+            fprintf( stdout, "Cannot find \"%s\".\n", pGsNameWin );
             return;
         }
 #else
-    sprintf( CommandPs,  "%s %s &", pProgGsViewName, FileNamePs ); 
-    if ( system( CommandPs ) == -1 )
     {
-        fprintf( stdout, "Cannot execute \"%s\".\n", FileNamePs );
-        return;
+        char CommandPs[1000];
+        unlink( FileNameDot );
+        sprintf( CommandPs,  "%s %s &", pGsNameUnix, FileNamePs ); 
+        if ( system( CommandPs ) == -1 )
+        {
+            fprintf( stdout, "Cannot execute \"%s\".\n", CommandPs );
+            return;
+        }
     }
 #endif
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 30047d23..c9e0df68 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -546,7 +546,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !fProfile && !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "This command works only for AIGs.\n" );
+        fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" );
         return 1;
     }
 
@@ -597,18 +597,23 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
-    extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk );
+    int fVerbose;
+    extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fVerbose = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -621,26 +626,25 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-
     if ( !Abc_NtkIsComb(pNtk) )
     {
         fprintf( pErr, "This command works only for combinational networks.\n" );
         return 1;
     }
-
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "This command works only for AIGs.\n" );
+        fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" );
         return 1;
     }
-    vSuppFun = Sim_ComputeFunSupp( pNtk );
+    vSuppFun = Sim_ComputeFunSupp( pNtk, fVerbose );
     free( vSuppFun->pArray[0] );
     Vec_PtrFree( vSuppFun );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: print_supp [-h]\n" );
+    fprintf( pErr, "usage: print_supp [-vh]\n" );
     fprintf( pErr, "\t        prints the supports of the CO nodes\n" );
+    fprintf( pErr, "\t-v    : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -706,7 +710,7 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "This command works only for AIGs.\n" );
+        fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" );
         return 1;
     }
     Abc_NtkSymmetries( pNtk, fUseBdds, fNaive, fVerbose );
@@ -715,7 +719,7 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: print_symm [-nbvh]\n" );
     fprintf( pErr, "\t         computes symmetries of the PO functions\n" );
-    fprintf( pErr, "\t-b     : enable efficient BDD-based computation [default = %s].\n", fUseBdds? "yes": "no" );  
+    fprintf( pErr, "\t-b     : toggle BDD-based or SAT-based computations [default = %s].\n", fUseBdds? "bdd": "sat" );  
     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");
@@ -867,7 +871,7 @@ int Abc_CommandShowCut( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Visualizing cuts only works for AIGs.\n" );
+        fprintf( pErr, "Visualizing cuts only works for AIGs (run \"strash\").\n" );
         return 1;
     }
     if ( argc != util_optind + 1 )
@@ -942,7 +946,7 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Visualizing AIG can only be done for AIGs.\n" );
+        fprintf( pErr, "Visualizing AIG can only be done for AIGs (run \"strash\").\n" );
         return 1;
     }
     Abc_NtkShowAig( pNtk );
@@ -1002,7 +1006,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Can only collapse a logic network.\n" );
+        fprintf( pErr, "Can only collapse a logic network or an AIG.\n" );
         return 1;
     }
 
@@ -1262,7 +1266,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Cannot renode a network that is not an AIG.\n" );
+        fprintf( pErr, "Cannot renode a network that is not an AIG (run \"strash\").\n" );
         return 1;
     }
 
@@ -1504,7 +1508,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsLogic(pNtk) )
     {
-        fprintf( pErr, "Fast extract can only be applied to a logic network.\n" );
+        fprintf( pErr, "Fast extract can only be applied to a logic network (run \"renode\").\n" );
         Abc_NtkFxuFreeInfo( p );
         return 1;
     }
@@ -1717,7 +1721,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "This command can only be applied to an AIG.\n" );
+        fprintf( pErr, "This command can only be applied to an AIG (run \"strash\").\n" );
         return 1;
     }
     if ( Abc_NtkGetChoiceNum(pNtk) )
@@ -1826,7 +1830,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "This command can only be applied to an AIG.\n" );
+        fprintf( pErr, "This command can only be applied to an AIG (run \"strash\").\n" );
         return 1;
     }
     if ( Abc_NtkGetChoiceNum(pNtk) )
@@ -2322,7 +2326,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkIsLogic(pNtk) )
     {
-        fprintf( stdout, "This command can only be applied to logic network.\n" );
+        fprintf( stdout, "This command can only be applied to logic network (run \"renode -c\").\n" );
         return 0;
     }
     if ( Abc_NtkIsMappedLogic(pNtk) )
@@ -2397,7 +2401,7 @@ int Abc_CommandExtSeqDcs( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( stdout, "This command works only for AIGs.\n" );
+        fprintf( stdout, "This command works only for AIGs (run \"strash\").\n" );
         return 0;
     }
     if ( !Abc_NtkExtractSequentialDcs( pNtk, fVerbose ) )
@@ -2751,7 +2755,7 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Cut computation is available only for AIGs.\n" );
+        fprintf( pErr, "Cut computation is available only for AIGs (run \"strash\").\n" );
         return 1;
     }
     pCutMan = Abc_NtkCuts( pNtk, pParams );
@@ -3606,7 +3610,7 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Works only for the AIG representation.\n" );
+        fprintf( pErr, "Works only for the AIG representation (run \"strash\").\n" );
         return 1;
     }
 
@@ -3785,7 +3789,7 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Works only for AIG.\n" );
+        fprintf( pErr, "Works only for AIG (run \"strash\").\n" );
         return 1;
     }
 
diff --git a/src/base/abci/abcAttach.c b/src/base/abci/abcAttach.c
index a8e06555..6ee1fb90 100644
--- a/src/base/abci/abcAttach.c
+++ b/src/base/abci/abcAttach.c
@@ -56,7 +56,6 @@ static int s_nPerms;
 ***********************************************************************/
 int Abc_NtkAttach( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
     Mio_Library_t * pGenlib;
     unsigned ** puTruthGates;
     unsigned uTruths[6][2];
@@ -149,7 +148,7 @@ int Abc_NtkAttach( Abc_Ntk_t * pNtk )
     printf( "Library gates are successfully attached to the nodes.\n" );
 
     // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( !Abc_NtkCheck( pNtk ) )
     {
         printf( "Abc_NtkAttach: The network check has failed.\n" );
         return 0;
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index 5042d0d5..40701e41 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -46,7 +46,6 @@ static int         Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSupe
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate )
 {
-    int fCheck = 1;
     Abc_Ntk_t * pNtkAig;
     assert( Abc_NtkIsStrash(pNtk) );
     // perform balancing
@@ -54,7 +53,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate )
     Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate );
     Abc_NtkFinalize( pNtk, pNtkAig );
     // make sure everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkAig ) )
+    if ( !Abc_NtkCheck( pNtkAig ) )
     {
         printf( "Abc_NtkBalance: The network check has failed.\n" );
         Abc_NtkDelete( pNtkAig );
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index 4e359506..40370eff 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -44,7 +44,6 @@ static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd,
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
 {
-    int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
 
     assert( Abc_NtkIsStrash(pNtk) );
@@ -71,7 +70,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
     Abc_NtkMinimumBase( pNtkNew );
 
     // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkCollapse: The network check has failed.\n" );
         Abc_NtkDelete( pNtkNew );
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 013b7ac4..67665ad6 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -55,7 +55,6 @@ static int             Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int n
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
 {
-    int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
 
     assert( Abc_NtkIsStrash(pNtk) );
@@ -78,7 +77,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
     pNtk->pManGlob = NULL;
 
     // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkDsdGlobal: The network check has failed.\n" );
         Abc_NtkDelete( pNtkNew );
@@ -304,7 +303,6 @@ Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNode
 ***********************************************************************/
 int Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive )
 {
-    int fCheck = 1;
     Dsd_Manager_t * pManDsd;
     DdManager * dd = pNtk->pManFunc;
     Vec_Ptr_t * vNodes;
@@ -328,7 +326,7 @@ int Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive )
     Dsd_ManagerStop( pManDsd );
 
     // make sure everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( !Abc_NtkCheck( pNtk ) )
     {
         printf( "Abc_NtkDsdRecursive: The network check has failed.\n" );
         return 0;
diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c
index f30325c0..55ae23ff 100644
--- a/src/base/abci/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@@ -46,12 +46,11 @@ static Abc_Obj_t *  Abc_NodeFromFpga_rec( Abc_Ntk_t * pNtkNew, Fpga_Node_t * pNo
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fSwitching, int fVerbose )
 {
-    int fCheck = 1;
+    int fShowSwitching = 1;
     Abc_Ntk_t * pNtkNew;
     Fpga_Man_t * pMan;
     Vec_Int_t * vSwitching;
     float * pSwitching = NULL;
-    int fShowSwitching = 0;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
@@ -90,7 +89,7 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fSwitching, int fV
     Abc_NtkMinimumBase( pNtkNew );
 
     // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkFpga: The network check has failed.\n" );
         Abc_NtkDelete( pNtkNew );
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index fbe676a3..e82065fc 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -51,7 +51,6 @@ static Abc_Obj_t *   Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
 {
-    int fCheck = 1;
     Fraig_Params_t * pPars = pParams;
     Abc_Ntk_t * pNtkNew;
     Fraig_Man_t * pMan;
@@ -64,7 +63,7 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
     pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
     Fraig_ManFree( pMan );
     // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkFraig: The network check has failed.\n" );
         Abc_NtkDelete( pNtkNew );
@@ -249,7 +248,6 @@ Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFrai
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
 
     if ( !Abc_NtkIsSopLogic(pNtk) )
@@ -273,7 +271,7 @@ Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
     printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkGetChoiceNum( pNtkNew ) );
 
     // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkFraigTrust: The network check has failed.\n" );
         Abc_NtkDelete( pNtkNew );
@@ -420,7 +418,6 @@ Abc_Obj_t * Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
 ***********************************************************************/
 int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
 {
-    Abc_Frame_t * p;
     Abc_Ntk_t * pStore;
     int nAndsOld;
 
@@ -431,8 +428,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
     }
 
     // get the network currently stored
-    p = Abc_FrameGetGlobalFrame();
-    pStore = Abc_FrameReadNtkStore(p);
+    pStore = Abc_FrameReadNtkStore();
     if ( pStore == NULL )
     {
         // start the stored network
@@ -443,8 +439,8 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
             return 0;
         }
         // save the parameters
-        Abc_FrameSetNtkStore( p, pStore );
-        Abc_FrameSetNtkStoreSize( p, 1 );
+        Abc_FrameSetNtkStore( pStore );
+        Abc_FrameSetNtkStoreSize( 1 );
         nAndsOld = 0;
     }
     else
@@ -457,7 +453,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
             return 0;
         }
         // set the number of networks stored
-        Abc_FrameSetNtkStoreSize( p, Abc_FrameReadNtkStoreSize(p) + 1 );
+        Abc_FrameSetNtkStoreSize( Abc_FrameReadNtkStoreSize() + 1 );
     }
     printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
     return 1;
@@ -476,22 +472,20 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFraigRestore()
 {
-    Abc_Frame_t * p;
     Fraig_Params_t Params;
     Abc_Ntk_t * pStore, * pFraig;
     int nWords1, nWords2, nWordsMin;
 
     // get the stored network
-    p = Abc_FrameGetGlobalFrame();
-    pStore   = Abc_FrameReadNtkStore(p);
-    Abc_FrameSetNtkStore( p, NULL );
+    pStore = Abc_FrameReadNtkStore();
+    Abc_FrameSetNtkStore( NULL );
     if ( pStore == NULL )
     {
         printf( "There are no network currently in storage.\n" );
         return NULL;
     }
     printf( "Currently stored %d networks with %d nodes will be fraiged.\n", 
-        Abc_FrameReadNtkStoreSize(p), Abc_NtkNodeNum(pStore) );
+        Abc_FrameReadNtkStoreSize(), Abc_NtkNodeNum(pStore) );
 
     // to determine the number of simulation patterns
     // use the following strategy
@@ -536,14 +530,12 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
 ***********************************************************************/
 void Abc_NtkFraigStoreClean()
 {
-    Abc_Frame_t * p;
     Abc_Ntk_t * pStore;
     // get the stored network
-    p = Abc_FrameGetGlobalFrame();
-    pStore = Abc_FrameReadNtkStore(p);
+    pStore = Abc_FrameReadNtkStore();
     if ( pStore )
         Abc_NtkDelete( pStore );
-    Abc_FrameSetNtkStore( p, NULL );
+    Abc_FrameSetNtkStore( NULL );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index 0c8994e1..3a70862f 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -52,8 +52,6 @@ static void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p );
 ***********************************************************************/
 bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
 {
-    int fCheck = 1;
-
     assert( Abc_NtkIsLogic(pNtk) );
     // convert nodes to SOPs
     if ( Abc_NtkIsMappedLogic(pNtk) )
@@ -81,7 +79,7 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
         // update the network
         Abc_NtkFxuReconstruct( pNtk, p );
         // make sure everything is okay
-        if ( fCheck && !Abc_NtkCheck( pNtk ) )
+        if ( !Abc_NtkCheck( pNtk ) )
             printf( "Abc_NtkFastExtract: The network check has failed.\n" );
         return 1;
     }
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 45f600ed..ec5352cb 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -56,7 +56,6 @@ static Abc_Obj_t *  Abc_NodeFromMapSuperChoice_rec( Abc_Ntk_t * pNtkNew, Map_Sup
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fSwitching, int fVerbose )
 {
-    int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
     Map_Man_t * pMan;
     Vec_Int_t * vSwitching;
@@ -106,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 );
@@ -115,7 +114,7 @@ clk = clock();
     Map_ManFree( pMan );
 
     // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkMap: The network check has failed.\n" );
         Abc_NtkDelete( pNtkNew );
@@ -440,7 +439,6 @@ int Abc_NtkUnmap( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
 
     Map_Man_t * pMan;
@@ -483,7 +481,7 @@ Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk )
     Map_ManFree( pMan );
 
     // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkMap: The network check has failed.\n" );
         Abc_NtkDelete( pNtkNew );
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 0d75ba1f..68dccd18 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -77,7 +77,6 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 {
-    int fCheck = 1;
     char Buffer[100];
     Abc_Ntk_t * pNtkMiter;
 
@@ -96,7 +95,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
     Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb );
 
     // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkMiter ) )
+    if ( !Abc_NtkCheck( pNtkMiter ) )
     {
         printf( "Abc_NtkMiter: The network check has failed.\n" );
         Abc_NtkDelete( pNtkMiter );
@@ -312,7 +311,6 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 )
 {
-    int fCheck = 1;
     char Buffer[100];
     Abc_Ntk_t * pNtkMiter;
     Abc_Obj_t * pRoot, * pOutput1, * pOutput2, * pMiter;
@@ -357,7 +355,7 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In
     Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
 
     // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkMiter ) )
+    if ( !Abc_NtkCheck( pNtkMiter ) )
     {
         printf( "Abc_NtkMiter: The network check has failed.\n" );
         Abc_NtkDelete( pNtkMiter );
@@ -470,7 +468,6 @@ void Abc_NtkMiterReport( Abc_Ntk_t * pMiter )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
 {
-    int fCheck = 1;
     char Buffer[100];
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkFrames;
@@ -531,7 +528,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
         }
     }
     // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkFrames ) )
+    if ( !Abc_NtkCheck( pNtkFrames ) )
     {
         printf( "Abc_NtkFrames: The network check has failed.\n" );
         Abc_NtkDelete( pNtkFrames );
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 61c1a110..6362a925 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -119,14 +119,13 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo
 ***********************************************************************/
 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 ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkBddToMuxes: The network check has failed.\n" );
         Abc_NtkDelete( pNtkNew );
diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c
index 766c14f3..60a02aed 100644
--- a/src/base/abci/abcReconv.c
+++ b/src/base/abci/abcReconv.c
@@ -1,12 +1,12 @@
 /**CFile****************************************************************
 
-  FileName    [abcRes.c]
+  FileName    [abcReconv.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
   PackageName [Network and node package.]
 
-  Synopsis    [Reconvergence=driven cut computation.]
+  Synopsis    [Computation of reconvergence-driven cuts.]
 
   Author      [Alan Mishchenko]
   
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: abcRes.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: abcReconv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 791d2d53..92d497fc 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -1,12 +1,12 @@
 /**CFile****************************************************************
 
-  FileName    [abcResRef.c]
+  FileName    [abcRefactor.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
   PackageName [Network and node package.]
 
-  Synopsis    [Resynthesis based on refactoring.]
+  Synopsis    [Resynthesis based on collapsing and refactoring.]
 
   Author      [Alan Mishchenko]
   
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: abcResRef.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: abcRefactor.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -82,7 +82,6 @@ static Dec_Graph_t *  Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec
 ***********************************************************************/
 int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUseZeros, bool fUseDcs, bool fVerbose )
 {
-    int fCheck = 1;
     ProgressBar * pProgress;
     Abc_ManRef_t * pManRef;
     Abc_ManCut_t * pManCut;
@@ -110,6 +109,9 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
         // skip the constant node
         if ( Abc_NodeIsConst(pNode) )
             continue;
+        // skip the nodes with many fanouts
+        if ( Abc_ObjFanoutNum(pNode) > 1000 )
+            continue;
         // stop if all nodes have been tried once
         if ( i >= nNodes )
             break;
@@ -140,7 +142,7 @@ pManRef->timeTotal = clock() - clkStart;
     Abc_NtkManRefStop( pManRef );
     Abc_NtkStopReverseLevels( pNtk );
     // check
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( !Abc_NtkCheck( pNtk ) )
     {
         printf( "Abc_NtkRefactor: The network check has failed.\n" );
         return 0;
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index c77c0d70..165777f8 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -6,7 +6,7 @@
 
   PackageName [Network and node package.]
 
-  Synopsis    [Procedures which transform an AIG into the network of nodes.]
+  Synopsis    [Procedures which transform an AIG into the network of SOP logic nodes.]
 
   Author      [Alan Mishchenko]
   
@@ -52,7 +52,6 @@ static void        Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone );
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple )
 {
-    int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
 
     assert( Abc_NtkIsStrash(pNtk) );
@@ -93,7 +92,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn
 //printf( "Maximum fanin = %d.\n", Abc_NtkGetFaninMax(pNtkNew) );
 
     // make sure everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkRenode: The network check has failed.\n" );
         Abc_NtkDelete( pNtkNew );
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 75fe1627..ea221296 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -1,12 +1,12 @@
 /**CFile****************************************************************
 
-  FileName    [abcRes.c]
+  FileName    [abcRewrite.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
   PackageName [Network and node package.]
 
-  Synopsis    [Technology-independent resynthesis of the AIG.]
+  Synopsis    [Technology-independent resynthesis of the AIG based on DAG aware rewriting.]
 
   Author      [Alan Mishchenko]
   
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: abcRes.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: abcRewrite.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -22,6 +22,12 @@
 #include "rwr.h"
 #include "dec.h"
 
+/*
+    The ideas realized in this package are inspired by the paper:
+    Per Bjesse, Arne Boralv, "DAG-aware circuit compression for 
+    formal verification", Proc. ICCAD 2004, pp. 42-49.
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -46,7 +52,6 @@ static void        Abc_NodePrintCuts( Abc_Obj_t * pNode );
 ***********************************************************************/
 int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose )
 {
-    int fCheck = 1;
     int fDrop = 0;
     ProgressBar * pProgress;
     Cut_Man_t * pManCut;
@@ -81,6 +86,9 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
         // skip the constant node
         if ( Abc_NodeIsConst(pNode) )
             continue;
+        // skip the nodes with many fanouts
+        if ( Abc_ObjFanoutNum(pNode) > 1000 )
+            continue;
         // for each cut, try to resynthesize it
         nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUseZeros );
         if ( nGain > 0 || nGain == 0 && fUseZeros )
@@ -104,7 +112,7 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
     pNtk->pManCut = NULL;
     Abc_NtkStopReverseLevels( pNtk );
     // check
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( !Abc_NtkCheck( pNtk ) )
     {
         printf( "Abc_NtkRewrite: The network check has failed.\n" );
         return 0;
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 935f1300..de87a1e9 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -51,7 +51,6 @@ extern char *      Mio_GateReadSop( void * pGate );
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
 {
-    int fCheck = 1;
     Abc_Ntk_t * pNtkAig;
     int nNodes;
 
@@ -74,7 +73,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
     if ( pNtk->pExdc )
         pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0, 1 );
     // make sure everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtkAig ) )
+    if ( !Abc_NtkCheck( pNtkAig ) )
     {
         printf( "Abc_NtkStrash: The network check has failed.\n" );
         Abc_NtkDelete( pNtkAig );
@@ -99,7 +98,6 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
 ***********************************************************************/
 int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
 {
-    int fCheck = 1;
     Abc_Obj_t * pObj;
     int i;
     // the first network should be an AIG
@@ -118,7 +116,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     // add pNtk2 to pNtk1 while strashing
     Abc_NtkStrashPerform( pNtk2, pNtk1, 1 );
     // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtk1 ) )
+    if ( !Abc_NtkCheck( pNtk1 ) )
     {
         printf( "Abc_NtkAppend: The network check has failed.\n" );
         return 0;
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index ca9bd34e..7000ecad 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -56,7 +56,6 @@ static void           Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pF
 ***********************************************************************/
 bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
 {
-    int fCheck = 1;
     Fraig_Params_t Params;
     Abc_Ntk_t * pNtkAig;
     Fraig_Man_t * pMan;
@@ -83,7 +82,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
     // cleanup the dangling nodes
     Abc_NtkCleanup( pNtk, fVerbose );
     // check
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( !Abc_NtkCheck( pNtk ) )
     {
         printf( "Abc_NtkFraigSweep: The network check has failed.\n" );
         return 0;
@@ -394,7 +393,6 @@ int Abc_NodeDroppingCost( Abc_Obj_t * pNode )
 ***********************************************************************/
 int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
 {
-    int fCheck = 1;
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode;
     int i, Counter;
@@ -423,7 +421,7 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
     if ( fVerbose )
         printf( "Cleanup removed %d dangling nodes.\n", Counter );
     // check
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( !Abc_NtkCheck( pNtk ) )
     {
         printf( "Abc_NtkCleanup: The network check has failed.\n" );
         return -1;
@@ -447,7 +445,6 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
 ***********************************************************************/
 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) ); 
@@ -481,7 +478,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
     if ( fVerbose )
         printf( "Sweep removed %d nodes.\n", nSwept );
     // check
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( !Abc_NtkCheck( pNtk ) )
     {
         printf( "Abc_NtkSweep: The network check has failed.\n" );
         return -1;
diff --git a/src/base/abci/abcSymm.c b/src/base/abci/abcSymm.c
index f9229639..f1e427c0 100644
--- a/src/base/abci/abcSymm.c
+++ b/src/base/abci/abcSymm.c
@@ -46,7 +46,7 @@ static void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms )
 ***********************************************************************/
 void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose )
 {
-    if ( fUseBdds || fNaive )
+    if ( fUseBdds )
         Abc_NtkSymmetriesUsingBdds( pNtk, fNaive, fVerbose );
     else
         Abc_NtkSymmetriesUsingSandS( pNtk, fVerbose );
@@ -65,8 +65,8 @@ void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose
 ***********************************************************************/
 void Abc_NtkSymmetriesUsingSandS( Abc_Ntk_t * pNtk, int fVerbose )
 {
-    extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk );
-    int nSymms = Sim_ComputeTwoVarSymms( pNtk );
+    extern int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose );
+    int nSymms = Sim_ComputeTwoVarSymms( pNtk, fVerbose );
     printf( "The total number of symmetries is %d.\n", nSymms );
 }
 
@@ -123,12 +123,14 @@ void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVer
     Abc_Obj_t * pNode;
     DdNode * bFunc;
     int nSymms = 0;
+    int nSupps = 0;
     int i;
 
     // compute symmetry info for each PO
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
         bFunc = pNtk->vFuncsGlob->pArray[i];
+        nSupps += Cudd_SupportSize( dd, bFunc );
         if ( Cudd_IsConstant(bFunc) )
             continue;
         if ( fNaive )
@@ -144,7 +146,8 @@ void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVer
 //Extra_SymmPairsPrint( pSymms );
         Extra_SymmPairsDissolve( pSymms );
     }
-    printf( "The total number of symmetries is %d.\n", nSymms );
+    printf( "Total number of vars in functional supports = %8d.\n", nSupps );
+    printf( "Total number of two-variable symmetries     = %8d.\n", nSymms );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index 0fe3ec63..abc02cc3 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -46,7 +46,6 @@ static Abc_Ntk_t * Abc_NtkConstructExdc     ( DdManager * dd, Abc_Ntk_t * pNtk,
 ***********************************************************************/
 int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
 {
-    int fCheck   = 1;
     int fReorder = 1;
     DdManager * dd;
     DdNode * bRelation, * bInitial, * bUnreach;
@@ -94,7 +93,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
     pNtk->pManGlob = NULL;
 
     // make sure that everything is okay
-    if ( fCheck && !Abc_NtkCheck( pNtk->pExdc ) )
+    if ( !Abc_NtkCheck( pNtk->pExdc ) )
     {
         printf( "Abc_NtkExtractSequentialDcs: The network check has failed.\n" );
         Abc_NtkDelete( pNtk->pExdc );
diff --git a/src/base/abcs/abcSeq.c b/src/base/abcs/abcSeq.c
index d6b1b8e5..a41edac1 100644
--- a/src/base/abcs/abcSeq.c
+++ b/src/base/abcs/abcSeq.c
@@ -60,7 +60,6 @@ static void        Abc_NodeSeqCreateLatches( Abc_Obj_t * pObj, int nLatches );
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
     Abc_Aig_t * pManNew;
     Vec_Ptr_t * vNodes;
@@ -176,7 +175,7 @@ printf( "\n" );
 
     if ( pNtk->pExdc )
         fprintf( stdout, "Warning: EXDC is dropped when converting to sequential AIG.\n" );
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkAigToSeq(): Network check has failed.\n" );
     return pNtkNew;
 }
@@ -194,7 +193,6 @@ printf( "\n" );
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
 {
-    int fCheck = 1;
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pFanin, * pFaninNew;
     int i, k, c;
@@ -233,7 +231,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
     // duplicate the EXDC network
     if ( pNtk->pExdc )
         fprintf( stdout, "Warning: EXDC network is not copied.\n" );
-    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkSeqToLogic(): Network check has failed.\n" );
     return pNtkNew;
 }
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 84c330bf..9195554a 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -29,7 +29,6 @@
 static int CmdCommandTime          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandEcho          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandQuit          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int CmdCommandUsage         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandWhich         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandHistory       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandAlias         ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -70,7 +69,6 @@ void Cmd_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Basic", "time",      CmdCommandTime,           0);
     Cmd_CommandAdd( pAbc, "Basic", "echo",      CmdCommandEcho,           0);
     Cmd_CommandAdd( pAbc, "Basic", "quit",      CmdCommandQuit,           0);
-//    Cmd_CommandAdd( pAbc, "Basic", "usage",     CmdCommandUsage,          0);
     Cmd_CommandAdd( pAbc, "Basic", "history",   CmdCommandHistory,        0);
     Cmd_CommandAdd( pAbc, "Basic", "alias",     CmdCommandAlias,          0);
     Cmd_CommandAdd( pAbc, "Basic", "unalias",   CmdCommandUnalias,        0);
@@ -79,7 +77,7 @@ void Cmd_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Basic", "set",       CmdCommandSetVariable,    0);
     Cmd_CommandAdd( pAbc, "Basic", "unset",     CmdCommandUnsetVariable,  0);
     Cmd_CommandAdd( pAbc, "Basic", "undo",      CmdCommandUndo,           0); 
-//    Cmd_CommandAdd( pAbc, "Basic", "recall",    CmdCommandRecall,         0); 
+    Cmd_CommandAdd( pAbc, "Basic", "recall",    CmdCommandRecall,         0); 
     Cmd_CommandAdd( pAbc, "Basic", "empty",     CmdCommandEmpty,          0); 
 #ifdef WIN32
     Cmd_CommandAdd( pAbc, "Basic", "ls",        CmdCommandLs,             0 );
@@ -275,45 +273,6 @@ int CmdCommandQuit( Abc_Frame_t * pAbc, int argc, char **argv )
   SeeAlso     []
 
 ******************************************************************************/
-int CmdCommandUsage( Abc_Frame_t * pAbc, int argc, char **argv )
-{
-    int c;
-
-    util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-            break;
-        default:
-            goto usage;
-        }
-    }
-
-    if ( argc != util_optind )
-        goto usage;
-    util_print_cpu_stats( pAbc->Out );
-    return 0;
-
-  usage:
-    fprintf( pAbc->Err, "usage: usage [-h]\n" );
-    fprintf( pAbc->Err, "   -h \t\tprint the command usage\n" );
-    return 1;
-}
-
-/**Function********************************************************************
-
-  Synopsis    []
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
 int CmdCommandWhich( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     return 0;
@@ -332,11 +291,9 @@ int CmdCommandWhich( Abc_Frame_t * pAbc, int argc, char **argv )
 ******************************************************************************/
 int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv )
 {
-    int i, num;
-    int size;
-    int c;
-    num = 50;
+    int i, c, num, size;
 
+    num = 20;
     util_getopt_reset();
     while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
     {
@@ -344,23 +301,28 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv )
         {
             case 'h':
                 goto usage;
-            break;
+            default :
+                goto usage;
         }
     }
-
-    if ( argc > 3 )
+    if ( argc > 2 )
         goto usage;
 
+    // get the number of commands to print
+    if ( argc == util_optind + 1 )
+        num = atoi(argv[util_optind]);
+    // print the commands
     size = pAbc->aHistory->nSize;
     num = ( num < size ) ? num : size;
     for ( i = size - num; i < size; i++ )
         fprintf( pAbc->Out, "%s", pAbc->aHistory->pArray[i] );
     return 0;
 
-  usage:
-    fprintf( pAbc->Err, "usage: history [-h] [num]\n" );
-    fprintf( pAbc->Err, "   -h \t\tprint the command usage\n" );
-    fprintf( pAbc->Err, "   num \t\tprint the last num commands\n" );
+usage:
+    fprintf( pAbc->Err, "usage: history [-h] <num>\n" );
+    fprintf( pAbc->Err, "          prints the latest command entered on the command line\n" );
+    fprintf( pAbc->Err, " -h     : print the command usage\n" );
+    fprintf( pAbc->Err, "num     : print the last num commands\n" );
     return ( 1 );
 }
 
@@ -378,7 +340,6 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv )
 int CmdCommandAlias( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char *key, *value;
-    st_generator *gen;
     int c;
 
     util_getopt_reset();
@@ -397,8 +358,7 @@ int CmdCommandAlias( Abc_Frame_t * pAbc, int argc, char **argv )
 
     if ( argc == 1 )
     {
-        st_foreach_item( pAbc->tAliases, gen, &key, &value )
-            CmdCommandAliasPrint( pAbc, ( Abc_Alias * ) value );
+        CmdPrintTable( pAbc->tAliases, 1 );
         return 0;
 
     }
@@ -712,7 +672,6 @@ int CmdCommandSource( Abc_Frame_t * pAbc, int argc, char **argv )
 int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char *flag_value, *key, *value;
-    st_generator *gen;
     int c;
 
     util_getopt_reset();
@@ -722,7 +681,6 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv )
         {
         case 'h':
             goto usage;
-            break;
         default:
             goto usage;
         }
@@ -733,10 +691,7 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv )
     }
     else if ( argc == 1 )
     {
-        st_foreach_item( pAbc->tFlags, gen, &key, &value )
-        {
-            fprintf( pAbc->Out, "%s\t%s\n", key, value );
-        }
+        CmdPrintTable( pAbc->tFlags, 0 );
         return 0;
     }
     else
@@ -749,25 +704,18 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv )
         }
 
         flag_value = argc == 2 ? util_strsav( "" ) : util_strsav( argv[2] );
-
-        ( void ) st_insert( pAbc->tFlags, util_strsav( argv[1] ),
-                             flag_value );
+//        flag_value = argc == 2 ? NULL : util_strsav(argv[2]);
+        st_insert( pAbc->tFlags, util_strsav(argv[1]), flag_value );
 
         if ( strcmp( argv[1], "abcout" ) == 0 )
         {
             if ( pAbc->Out != stdout )
-            {
-                ( void ) fclose( pAbc->Out );
-            }
+                fclose( pAbc->Out );
             if ( strcmp( flag_value, "" ) == 0 )
-            {
                 flag_value = "-";
-            }
             pAbc->Out = CmdFileOpen( pAbc, flag_value, "w", NIL( char * ), 0 );
             if ( pAbc->Out == NULL )
-            {
                 pAbc->Out = stdout;
-            }
 #if HAVE_SETVBUF
             setvbuf( pAbc->Out, ( char * ) NULL, _IOLBF, 0 );
 #endif
@@ -775,18 +723,12 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv )
         if ( strcmp( argv[1], "abcerr" ) == 0 )
         {
             if ( pAbc->Err != stderr )
-            {
-                ( void ) fclose( pAbc->Err );
-            }
+                fclose( pAbc->Err );
             if ( strcmp( flag_value, "" ) == 0 )
-            {
                 flag_value = "-";
-            }
             pAbc->Err = CmdFileOpen( pAbc, flag_value, "w", NIL( char * ), 0 );
             if ( pAbc->Err == NULL )
-            {
                 pAbc->Err = stderr;
-            }
 #if HAVE_SETVBUF
             setvbuf( pAbc->Err, ( char * ) NULL, _IOLBF, 0 );
 #endif
@@ -794,28 +736,21 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv )
         if ( strcmp( argv[1], "history" ) == 0 )
         {
             if ( pAbc->Hst != NIL( FILE ) )
-            {
-                ( void ) fclose( pAbc->Hst );
-            }
+                fclose( pAbc->Hst );
             if ( strcmp( flag_value, "" ) == 0 )
-            {
                 pAbc->Hst = NIL( FILE );
-            }
             else
             {
-                pAbc->Hst =
-                    CmdFileOpen( pAbc, flag_value, "w", NIL( char * ), 0 );
+                pAbc->Hst = CmdFileOpen( pAbc, flag_value, "w", NIL( char * ), 0 );
                 if ( pAbc->Hst == NULL )
-                {
                     pAbc->Hst = NIL( FILE );
-                }
             }
         }
         return 0;
     }
 
   usage:
-    fprintf( pAbc->Err, "usage: set [-h] [name] [value]\n" );
+    fprintf( pAbc->Err, "usage: set [-h] <name> <value>\n" );
     fprintf( pAbc->Err, "\t        sets the value of parameter <name>\n" );
     fprintf( pAbc->Err, "\t-h    : print the command usage\n" );
     return 1;
@@ -870,8 +805,9 @@ int CmdCommandUnsetVariable( Abc_Frame_t * pAbc, int argc, char **argv )
 
 
   usage:
-    fprintf( pAbc->Err, "usage: unset [-h] variables \n" );
-    fprintf( pAbc->Err, "   -h \t\tprint the command usage\n" );
+    fprintf( pAbc->Err, "usage: unset [-h] <name> \n" );
+    fprintf( pAbc->Err, "\t        removes the value of parameter <name>\n" );
+    fprintf( pAbc->Err, "\t-h    : print the command usage\n" );
     return 1;
 }
 
@@ -1014,9 +950,10 @@ int CmdCommandRecall( Abc_Frame_t * pAbc, int argc, char **argv )
 
 usage:
 
-    fprintf( pAbc->Err, "usage: recall <num>\n" );
+    fprintf( pAbc->Err, "usage: recall -h <num>\n" );
     fprintf( pAbc->Err, "         set the current network to be one of the previous networks\n" );
     fprintf( pAbc->Err, "<num> :  level to return to [default = previous]\n" );
+    fprintf( pAbc->Err, "   -h :  print the command usage\n");
     return 1;
 }
 
@@ -1260,7 +1197,9 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     FILE * pFile;
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkNew;
+    Abc_Ntk_t * pNtk, * pNtkNew, * pNetlist;
+    char * pNameWin = "sis.exe";
+    char * pNameUnix = "sis";
     char Command[1000], Buffer[100];
     char * pSisName;
     int i;
@@ -1288,23 +1227,28 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
     if ( strcmp( argv[1], "-?" ) == 0 )
         goto usage;
 
+    // get the names from the resource file
+    if ( Cmd_FlagReadByName(pAbc, "siswin") )
+        pNameWin = Cmd_FlagReadByName(pAbc, "siswin");
+    if ( Cmd_FlagReadByName(pAbc, "sisunix") )
+        pNameUnix = Cmd_FlagReadByName(pAbc, "sisunix");
+
     // check if SIS is available
-    if ( (pFile = fopen( "sis.exe", "r" )) )
-        pSisName = "sis.exe";
-    else if ( (pFile = fopen( "sis", "r" )) )
-        pSisName = "sis";
+    if ( (pFile = fopen( pNameWin, "r" )) )
+        pSisName = pNameWin;
+    else if ( (pFile = fopen( pNameUnix, "r" )) )
+        pSisName = pNameUnix;
     else if ( pFile == NULL )
     {
-        fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", "sis.exe", "sis" );
+        fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", pNameWin, pNameUnix );
         goto usage;
     }
     fclose( pFile );
 
-    if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
-
     // write out the current network
-    Io_WriteBlifLogic( pNtk, "_sis_in.blif", 1 );
+    pNetlist = Abc_NtkLogicToNetlist(pNtk);
+    Io_WriteBlif( pNetlist, "_sis_in.blif", 1 );
+    Abc_NtkDelete( pNetlist );
 
     // create the file for sis
     sprintf( Command, "%s -x -c ", pSisName );
@@ -1383,8 +1327,10 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     FILE * pFile;
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkNew;
+    Abc_Ntk_t * pNtk, * pNtkNew, * pNetlist;
     char Command[1000], Buffer[100];
+    char * pNameWin = "mvsis.exe";
+    char * pNameUnix = "mvsis";
     char * pMvsisName;
     int i;
 
@@ -1411,23 +1357,29 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
     if ( strcmp( argv[1], "-?" ) == 0 )
         goto usage;
 
+    // get the names from the resource file
+    if ( Cmd_FlagReadByName(pAbc, "mvsiswin") )
+        pNameWin = Cmd_FlagReadByName(pAbc, "mvsiswin");
+    if ( Cmd_FlagReadByName(pAbc, "mvsisunix") )
+        pNameUnix = Cmd_FlagReadByName(pAbc, "mvsisunix");
+
     // check if MVSIS is available
-    if ( (pFile = fopen( "mvsis.exe", "r" )) )
-        pMvsisName = "mvsis.exe";
-    else if ( (pFile = fopen( "mvsis", "r" )) )
-        pMvsisName = "mvsis";
+    if ( (pFile = fopen( pNameWin, "r" )) )
+        pMvsisName = pNameWin;
+    else if ( (pFile = fopen( pNameUnix, "r" )) )
+        pMvsisName = pNameUnix;
     else if ( pFile == NULL )
     {
-        fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", "mvsis.exe", "mvsis" );
+        fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", pNameWin, pNameUnix );
         goto usage;
     }
     fclose( pFile );
 
-    if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
 
     // write out the current network
-    Io_WriteBlifLogic( pNtk, "_mvsis_in.blif", 1 );
+    pNetlist = Abc_NtkLogicToNetlist(pNtk);
+    Io_WriteBlif( pNetlist, "_mvsis_in.blif", 1 );
+    Abc_NtkDelete( pNetlist );
 
     // create the file for MVSIS
     sprintf( Command, "%s -x -c ", pMvsisName );
diff --git a/src/base/cmd/cmdAlias.c b/src/base/cmd/cmdAlias.c
index 37220ef0..59a8b87e 100644
--- a/src/base/cmd/cmdAlias.c
+++ b/src/base/cmd/cmdAlias.c
@@ -68,7 +68,7 @@ void CmdCommandAliasAdd( Abc_Frame_t * pAbc, char * sName, int argc, char ** arg
 void CmdCommandAliasPrint( Abc_Frame_t * pAbc, Abc_Alias * pAlias )
 {
     int i;
-    fprintf(pAbc->Out, "%s\t", pAlias->sName);
+    fprintf(pAbc->Out, "%-15s", pAlias->sName);
     for(i = 0; i < pAlias->argc; i++) 
         fprintf( pAbc->Out, " %s", pAlias->argv[i] );
     fprintf( pAbc->Out, "\n" );
diff --git a/src/base/cmd/cmdFlag.c b/src/base/cmd/cmdFlag.c
index 96f1f251..63a0389d 100644
--- a/src/base/cmd/cmdFlag.c
+++ b/src/base/cmd/cmdFlag.c
@@ -43,14 +43,10 @@
 ******************************************************************************/
 char * Cmd_FlagReadByName( Abc_Frame_t * pAbc, char * flag )
 {
-  char *value;
-
-  if (st_lookup(pAbc->tFlags, flag, &value)) {
-    return value;
-  }
-  else {
-    return NIL(char);
-  }
+    char * value;
+    if ( st_lookup(pAbc->tFlags, flag, &value) )
+        return value;
+    return NULL;
 }
 
 
@@ -65,19 +61,17 @@ char * Cmd_FlagReadByName( Abc_Frame_t * pAbc, char * flag )
 ******************************************************************************/
 void Cmd_FlagUpdateValue( Abc_Frame_t * pAbc, char * key, char * value )
 {
-  char *oldValue, *newValue;
-
-  if (!key)
-    return;
-  if (value)
-    newValue = util_strsav(value);
-  else
-    newValue = util_strsav("");
-
-  if (st_delete(pAbc->tFlags, &key, &oldValue))
-    FREE(oldValue);
-
-  st_insert(pAbc->tFlags, key, newValue);
+    char * oldValue, * newValue;
+    if ( !key )
+        return;
+    if ( value )
+        newValue = util_strsav(value);
+    else
+        newValue = util_strsav("");
+//        newValue = NULL;
+    if ( st_delete(pAbc->tFlags, &key, &oldValue) )
+        FREE(oldValue);
+    st_insert( pAbc->tFlags, key, newValue );
 }
 
 
@@ -92,15 +86,14 @@ void Cmd_FlagUpdateValue( Abc_Frame_t * pAbc, char * key, char * value )
 ******************************************************************************/
 void Cmd_FlagDeleteByName( Abc_Frame_t * pAbc, char * key )
 {
-  char *value;
-
-  if (!key)
-    return;
-
-  if (st_delete(pAbc->tFlags, &key, &value)) {
-    FREE(key);
-    FREE(value);
-  }
+    char *value;
+    if ( !key )
+        return;
+    if ( st_delete( pAbc->tFlags, &key, &value ) ) 
+    {
+        FREE(key);
+        FREE(value);
+    }
 }
 
 
diff --git a/src/base/cmd/cmdInt.h b/src/base/cmd/cmdInt.h
index f0289ad4..d110b634 100644
--- a/src/base/cmd/cmdInt.h
+++ b/src/base/cmd/cmdInt.h
@@ -73,6 +73,7 @@ extern FILE *     CmdFileOpen( Abc_Frame_t * pAbc, char * sFileName, char * sMod
 extern void       CmdFreeArgv( int argc, char ** argv );
 extern void       CmdCommandFree( Abc_Command * pCommand );
 extern void       CmdCommandPrint( Abc_Frame_t * pAbc, bool fPrintAll );
+extern void       CmdPrintTable( st_table * tTable, int fAliases );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c
index 67a290a2..71396d3e 100644
--- a/src/base/cmd/cmdUtils.c
+++ b/src/base/cmd/cmdUtils.c
@@ -110,7 +110,7 @@ int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv )
     // get the backup network if the command is going to change the network
     if ( pCommand->fChange ) 
     {
-        if ( pAbc->pNtkCur )
+        if ( pAbc->pNtkCur && Abc_FrameIsFlagEnabled( "backup" ) )
         {
             pNetCopy = Abc_NtkDup( pAbc->pNtkCur );
             Abc_FrameSetCurrentNetwork( pAbc, pNetCopy );
@@ -122,15 +122,10 @@ int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv )
 
     // execute the command
     clk = util_cpu_time();
-    pFunc = ( int (*)( Abc_Frame_t *, int, char ** ) ) pCommand->pFunc;
+    pFunc = (int (*)(Abc_Frame_t *, int, char **))pCommand->pFunc;
     fError = (*pFunc)( pAbc, argc, argv );
     pAbc->TimeCommand += (util_cpu_time() - clk);
 
-//    if ( !fError && pCommand->fChange && pAbc->pNtkCur ) 
-//    {
-//    Cmd_HistoryAddSnapshot(pAbc, pAbc->pNet);
-//    }
-
     // automatic execution of arbitrary command after each command 
     // usually this is a passive command ... 
     if ( fError == 0 && !pAbc->fAutoexac )
@@ -592,6 +587,62 @@ int CmdCommandPrintCompare( Abc_Command ** ppC1, Abc_Command ** ppC2 )
     assert( 0 );
     return 0;
 }
+ 
+/**Function*************************************************************
+
+  Synopsis    [Comparision function used for sorting commands.]
+
+  Description []
+                
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int CmdNamePrintCompare( char ** ppC1, char ** ppC2 )
+{
+    return strcmp( *ppC1, *ppC2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparision function used for sorting commands.]
+
+  Description []
+                
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CmdPrintTable( st_table * tTable, int fAliases )
+{
+    st_generator * gen;
+    char ** ppNames;
+    char * key, * value;
+    int nNames, i;
+
+    // collect keys in the array
+    ppNames = ALLOC( char *, st_count(tTable) );
+    nNames = 0;
+    st_foreach_item( tTable, gen, &key, &value )
+        ppNames[nNames++] = key;
+
+    // sort array by name
+    qsort( (void *)ppNames, nNames, sizeof(char *), 
+        (int (*)(const void *, const void *))CmdNamePrintCompare );
+
+    // print in this order
+    for ( i = 0; i < nNames; i++ )
+    {
+        st_lookup( tTable, ppNames[i], &value );
+        if ( fAliases )
+            CmdCommandAliasPrint( Abc_FrameGetGlobalFrame(), (Abc_Alias *)value );
+        else
+            fprintf( stdout, "%-15s %-15s\n", ppNames[i], value );
+    }
+    free( ppNames );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index dd571f91..393b2216 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -58,7 +58,7 @@ Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck )
         return NULL;
 
     // make sure that everything is okay with the network structure
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
     {
         printf( "Io_ReadBench: The network check has failed.\n" );
         Abc_NtkDelete( pNtk );
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index b5dc2fa8..946de42b 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -109,7 +109,7 @@ Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck )
     Io_ReadBlifFree( p );
 
     // make sure that everything is okay with the network structure
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
     {
         printf( "Io_ReadBlif: The network check has failed.\n" );
         Abc_NtkDelete( pNtk );
diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c
index 172849bd..48a1722b 100644
--- a/src/base/io/ioReadEdif.c
+++ b/src/base/io/ioReadEdif.c
@@ -58,7 +58,7 @@ Abc_Ntk_t * Io_ReadEdif( char * pFileName, int fCheck )
         return NULL;
 
     // make sure that everything is okay with the network structure
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
     {
         printf( "Io_ReadEdif: The network check has failed.\n" );
         Abc_NtkDelete( pNtk );
diff --git a/src/base/io/ioReadEqn.c b/src/base/io/ioReadEqn.c
index 54890729..20d30a1a 100644
--- a/src/base/io/ioReadEqn.c
+++ b/src/base/io/ioReadEqn.c
@@ -61,7 +61,7 @@ Abc_Ntk_t * Io_ReadEqn( char * pFileName, int fCheck )
         return NULL;
 
     // make sure that everything is okay with the network structure
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
     {
         printf( "Io_ReadEqn: The network check has failed.\n" );
         Abc_NtkDelete( pNtk );
diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c
index c4b4084c..1e54db5f 100644
--- a/src/base/io/ioReadPla.c
+++ b/src/base/io/ioReadPla.c
@@ -58,7 +58,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck )
         return NULL;
 
     // make sure that everything is okay with the network structure
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
     {
         printf( "Io_ReadPla: The network check has failed.\n" );
         Abc_NtkDelete( pNtk );
diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c
index 53299a0c..f4855dde 100644
--- a/src/base/io/ioReadVerilog.c
+++ b/src/base/io/ioReadVerilog.c
@@ -150,7 +150,7 @@ Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck )
         return NULL;
 
     // make sure that everything is okay with the network structure
-    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    if ( fCheck && !Abc_NtkCheckRead( pNtk ) )
     {
         printf( "Io_ReadVerilog: The network check has failed.\n" );
         Abc_NtkDelete( pNtk );
diff --git a/src/base/main/main.c b/src/base/main/main.c
index a3fd979a..0622a3bd 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -231,29 +231,22 @@ usage:
 
   Synopsis    [Returns 1 if s is a file type recognized, else returns 0.]
 
-  Description [Returns 1 if s is a file type recognized by VIS, else returns
-  0. Recognized types are "blif", "blif_mv", "blif_mvs", and "none".]
+  Description [Returns 1 if s is a file type recognized by ABC, else returns 0. 
+  Recognized types are "blif", "bench", "pla", and "none".]
 
   SideEffects []
 
 ******************************************************************************/
-static int
-TypeCheck(
-    Abc_Frame_t * pAbc,
-    char       * s)
+static int TypeCheck( Abc_Frame_t * pAbc, char * s )
 {
-    if (strcmp(s, "blif") == 0) {
+    if (strcmp(s, "blif") == 0)
         return 1;
-    }
-    else if (strcmp(s, "blif_mv") == 0) {
+    else if (strcmp(s, "bench") == 0)
         return 1;
-    }
-    else if (strcmp(s, "blif_mvs") == 0) {
+    else if (strcmp(s, "pla") == 0)
         return 1;
-    }
-    else if (strcmp(s, "none") == 0) {
+    else if (strcmp(s, "none") == 0)
         return 1;
-    }
     else {
         fprintf( pAbc->Err, "unknown type %s\n", s );
         return 0;
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 72eec599..0d47dec5 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -90,21 +90,22 @@ extern void            Abc_FrameDeleteAllNetworks( Abc_Frame_t * p );
 extern void               Abc_FrameSetGlobalFrame( Abc_Frame_t * p );
 extern Abc_Frame_t *   Abc_FrameGetGlobalFrame();
 
-extern Abc_Ntk_t *     Abc_FrameReadNtkStore       ( Abc_Frame_t * pFrame );
-extern int             Abc_FrameReadNtkStoreSize   ( Abc_Frame_t * pFrame );
-extern void            Abc_FrameSetNtkStore        ( Abc_Frame_t * pFrame, Abc_Ntk_t * pNtk );
-extern void            Abc_FrameSetNtkStoreSize    ( Abc_Frame_t * pFrame, int nStored  );
-
-extern void *          Abc_FrameReadLibLut         ( Abc_Frame_t * pFrame );
-extern void *          Abc_FrameReadLibGen         ( Abc_Frame_t * pFrame );
-extern void *          Abc_FrameReadLibSuper       ( Abc_Frame_t * pFrame );
-extern void            Abc_FrameSetLibLut          ( Abc_Frame_t * pFrame, void * pLib );
-extern void            Abc_FrameSetLibGen          ( Abc_Frame_t * pFrame, void * pLib );
-extern void            Abc_FrameSetLibSuper        ( Abc_Frame_t * pFrame, void * pLib );
-
-extern void *          Abc_FrameReadManDd          ( Abc_Frame_t * pFrame );
-extern void *          Abc_FrameReadManDec         ( Abc_Frame_t * pFrame );
-
+extern Abc_Ntk_t *     Abc_FrameReadNtkStore();                  
+extern int             Abc_FrameReadNtkStoreSize();              
+extern void *          Abc_FrameReadLibLut();                    
+extern void *          Abc_FrameReadLibGen();                    
+extern void *          Abc_FrameReadLibSuper();                  
+extern void *          Abc_FrameReadManDd();                     
+extern void *          Abc_FrameReadManDec();                    
+extern char *          Abc_FrameReadFlag( char * pFlag ); 
+extern bool            Abc_FrameIsFlagEnabled( char * pFlag );
+
+extern void            Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ); 
+extern void            Abc_FrameSetNtkStoreSize( int nStored );  
+extern void            Abc_FrameSetLibLut( void * pLib );        
+extern void            Abc_FrameSetLibGen( void * pLib );        
+extern void            Abc_FrameSetLibSuper( void * pLib );      
+extern void            Abc_FrameSetFlag( char * pFlag, char * pValue );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 09a750ea..77c9f579 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -26,7 +26,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Abc_Frame_t * Abc_FrameGlobalFrame = 0;
+static Abc_Frame_t * s_GlobalFrame = NULL;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -34,6 +34,57 @@ static Abc_Frame_t * Abc_FrameGlobalFrame = 0;
 
 /**Function*************************************************************
 
+  Synopsis    [APIs to access parameters in the flobal frame.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_FrameReadNtkStore()                  { return s_GlobalFrame->pStored;      } 
+int         Abc_FrameReadNtkStoreSize()              { return s_GlobalFrame->nStored;      }
+void *      Abc_FrameReadLibLut()                    { return s_GlobalFrame->pLibLut;      } 
+void *      Abc_FrameReadLibGen()                    { return s_GlobalFrame->pLibGen;      } 
+void *      Abc_FrameReadLibSuper()                  { return s_GlobalFrame->pLibSuper;    } 
+void *      Abc_FrameReadManDd()                     { return s_GlobalFrame->dd;           } 
+void *      Abc_FrameReadManDec()                    { return s_GlobalFrame->pManDec;      } 
+char *      Abc_FrameReadFlag( char * pFlag )        { return Cmd_FlagReadByName( s_GlobalFrame, pFlag );  } 
+
+void        Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ) { s_GlobalFrame->pStored  = pNtk;     } 
+void        Abc_FrameSetNtkStoreSize( int nStored )  { s_GlobalFrame->nStored  = nStored;  }
+void        Abc_FrameSetLibLut( void * pLib )        { s_GlobalFrame->pLibLut   = pLib;    } 
+void        Abc_FrameSetLibGen( void * pLib )        { s_GlobalFrame->pLibGen   = pLib;    } 
+void        Abc_FrameSetLibSuper( void * pLib )      { s_GlobalFrame->pLibSuper = pLib;    } 
+void        Abc_FrameSetFlag( char * pFlag, char * pValue )  { Cmd_FlagUpdateValue( s_GlobalFrame, pFlag, pValue );  } 
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the flag is enabled without value or with value 1.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_FrameIsFlagEnabled( char * pFlag )
+{
+    char * pValue;
+    // if flag is not defined, it is not enabled
+    pValue = Abc_FrameReadFlag( pFlag );
+    if ( pValue == NULL )
+        return 0;
+    // if flag is defined but value is not empty (no parameter) or "1", it is not enabled
+    if ( strcmp(pValue, "") && strcmp(pValue, "1") )
+        return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -311,7 +362,7 @@ void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtk )
         return;
 
     // transfer the parameters to the new network
-    if ( p->pNtkCur )
+    if ( p->pNtkCur && Abc_FrameIsFlagEnabled( "backup" ) )
     {
         Abc_NtkSetBackup( pNtk, Abc_NtkBackup(p->pNtkCur) );
         Abc_NtkSetStep( pNtk, Abc_NtkStep(p->pNtkCur) );
@@ -322,6 +373,9 @@ void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtk )
     {
         Abc_NtkSetBackup( pNtk, NULL );
         Abc_NtkSetStep( pNtk, ++p->nSteps );
+        // delete the current network if present but backup is disabled
+        if ( p->pNtkCur )
+            Abc_NtkDelete( p->pNtkCur );
     }
     // set the new current network
     p->pNtkCur = pNtk;
@@ -385,7 +439,7 @@ void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p )
 ***********************************************************************/
 void Abc_FrameSetGlobalFrame( Abc_Frame_t * p )
 {
-    Abc_FrameGlobalFrame = p;
+    s_GlobalFrame = p;
 }
 
 /**Function*************************************************************
@@ -401,43 +455,17 @@ void Abc_FrameSetGlobalFrame( Abc_Frame_t * p )
 ***********************************************************************/
 Abc_Frame_t * Abc_FrameGetGlobalFrame()
 {
-    if ( Abc_FrameGlobalFrame == 0 )
+    if ( s_GlobalFrame == 0 )
     {
         // start the framework
-        Abc_FrameGlobalFrame = Abc_FrameAllocate();
+        s_GlobalFrame = Abc_FrameAllocate();
         // perform initializations
-        Abc_FrameInit( Abc_FrameGlobalFrame );
+        Abc_FrameInit( s_GlobalFrame );
     }
-    return Abc_FrameGlobalFrame;
+    return s_GlobalFrame;
 }
 
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_FrameReadNtkStore       ( Abc_Frame_t * pFrame )                     { return pFrame->pStored;    } 
-int         Abc_FrameReadNtkStoreSize   ( Abc_Frame_t * pFrame )                     { return pFrame->nStored;    }
-void        Abc_FrameSetNtkStore        ( Abc_Frame_t * pFrame, Abc_Ntk_t * pNtk )   { pFrame->pStored  = pNtk;   } 
-void        Abc_FrameSetNtkStoreSize    ( Abc_Frame_t * pFrame, int nStored )        { pFrame->nStored  = nStored;}
-
-void *      Abc_FrameReadLibLut         ( Abc_Frame_t * pFrame )                     { return pFrame->pLibLut;    } 
-void *      Abc_FrameReadLibGen         ( Abc_Frame_t * pFrame )                     { return pFrame->pLibGen;    } 
-void *      Abc_FrameReadLibSuper       ( Abc_Frame_t * pFrame )                     { return pFrame->pLibSuper;  } 
-void        Abc_FrameSetLibLut          ( Abc_Frame_t * pFrame, void * pLib )        { pFrame->pLibLut   = pLib;  } 
-void        Abc_FrameSetLibGen          ( Abc_Frame_t * pFrame, void * pLib )        { pFrame->pLibGen   = pLib;  } 
-void        Abc_FrameSetLibSuper        ( Abc_Frame_t * pFrame, void * pLib )        { pFrame->pLibSuper = pLib;  } 
-
-void *      Abc_FrameReadManDd          ( Abc_Frame_t * pFrame )                     { return pFrame->dd;         } 
-void *      Abc_FrameReadManDec         ( Abc_Frame_t * pFrame )                     { return pFrame->pManDec;    } 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 95d5b22d..6b929854 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -32,7 +32,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 // the current version
-#define ABC_VERSION "UC Berkeley, ABC 1.0"
+#define ABC_VERSION "UC Berkeley, ABC 1.01"
 
 // the maximum length of an input line 
 #define MAX_STR     32768
@@ -53,8 +53,8 @@ struct Abc_Frame_t_
     // the functionality
     Abc_Ntk_t *     pNtkCur;     // the current network
     int             nSteps;      // the counter of different network processed
-    // when this flag is 1, the current command is executed in autoexec mode
-    int             fAutoexac;  
+    int             fAutoexac;   // marks the autoexec mode
+    int                fBatchMode;     // are we invoked in batch mode?
     // output streams
     FILE *          Out;
     FILE *          Err;
@@ -62,14 +62,13 @@ struct Abc_Frame_t_
     // used for runtime measurement
     int             TimeCommand; // the runtime of the last command
     int             TimeTotal;   // the total runtime of all commands
-    int                fBatchMode;     // are we invoked in batch mode?
     // temporary storage for structural choices
     Abc_Ntk_t *     pStored;     // the stored networks
     int             nStored;     // the number of stored networks
     // decomposition package
-    DdManager *     dd;          // temporary BDD package
     void *          pManDec;     // decomposition manager
-
+    DdManager *     dd;          // temporary BDD package
+    // libraries for mapping
     void *          pLibLut;     // the current LUT library
     void *          pLibGen;     // the current genlib
     void *          pLibSuper;   // the current supergate library
diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c
index 35d3c364..9d1201fa 100644
--- a/src/base/main/mainUtils.c
+++ b/src/base/main/mainUtils.c
@@ -161,8 +161,14 @@ void Abc_UtilsSource( Abc_Frame_t * pAbc )
     Cmd_CommandExecute( pAbc, "source -s abc.rc" );
     }
 #endif //WIN32
-
-    return;
+    {
+        // reset command history
+        char * pName; 
+        int i;
+        Vec_PtrForEachEntry( pAbc->aHistory, pName, i )
+            free( pName );
+        pAbc->aHistory->nSize = 0;
+    }
 }
 
 /**Function********************************************************************
author	Alan Mishchenko <alanmi@berkeley.edu>	2005-09-05 08:01:00 -0700
committer	Alan Mishchenko <alanmi@berkeley.edu>	2005-09-05 08:01:00 -0700
commit	1260d20cc05fe2d21088cc047c460e85ccdb3b14 (patch)
tree	f10ccc3333f78b6e2e089a88c8cf61a47b2f2dcd /src/base
parent	33012d9530c40817e1fc5230b3e663f7690b2e94 (diff)
download	abc-1260d20cc05fe2d21088cc047c460e85ccdb3b14.tar.gz abc-1260d20cc05fe2d21088cc047c460e85ccdb3b14.tar.bz2 abc-1260d20cc05fe2d21088cc047c460e85ccdb3b14.zip