Version abc50905

19 files changed, 90 insertions, 102 deletions

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 );