Improving printouts in sharing extraction.

6 files changed, 25 insertions, 17 deletions

diff --git a/src/aig/gia/giaShrink6.c b/src/aig/gia/giaShrink6.c
index 5deb033c..fd01b220 100644
--- a/src/aig/gia/giaShrink6.c
+++ b/src/aig/gia/giaShrink6.c
@@ -135,7 +135,7 @@ Gia_Man_t * Shr_ManFree( Shr_Man_t * p )
     {
         p->pNew = Gia_ManCleanup( pTemp = p->pNew );
         if ( Gia_ManAndNum(p->pNew) != Gia_ManAndNum(pTemp) )
-            printf( "Gia_ManShrink6() node reduction after sweep %6d -> %6d.\n", Gia_ManAndNum(pTemp), Gia_ManAndNum(p->pNew) );
+            printf( "Node reduction after sweep %6d -> %6d.\n", Gia_ManAndNum(pTemp), Gia_ManAndNum(p->pNew) );
         Gia_ManStop( pTemp );
     }
     Gia_ManSetRegNum( p->pNew, Gia_ManRegNum(p->pGia) );
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index b755a0c4..1fb6dbab 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -2666,7 +2666,7 @@ Abc_Ntk_t * Abc_NtkFromPla( char ** pPlas, int nInputs, int nOutputs )
     if ( !Abc_NtkCheck( pNtkSop ) )
         fprintf( stdout, "Abc_NtkFromPla(): Network check has failed.\n" );
     // perform fast_extract
-    Abc_NtkSetDefaultParams( p );
+    Abc_NtkSetDefaultFxParams( p );
     Abc_NtkFastExtract( pNtkSop, p );
     Abc_NtkFxuFreeInfo( p );
     // convert to an AIG
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e62e2c9e..461f4f5d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3632,14 +3632,14 @@ usage:
 ***********************************************************************/
 int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int nLitCountMax, int fVerbose );
+    extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int nLitCountMax, int fVerbose, int fVeryVerbose );
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     Fxu_Data_t Params, * p = &Params;
     int c, fNewAlgo = 1;
     // set the defaults
-    Abc_NtkSetDefaultParams( p );
+    Abc_NtkSetDefaultFxParams( p );
     Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "SDNWMsdzcnvh")) != EOF )
+    while ( (c = Extra_UtilGetopt(argc, argv, "SDNWMsdzcnvwh")) != EOF )
     {
         switch (c)
         {
@@ -3716,6 +3716,9 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
             case 'v':
                 p->fVerbose ^= 1;
                 break;
+            case 'w':
+                p->fVeryVerbose ^= 1;
+                break;
             case 'h':
                 goto usage;
                 break;
@@ -3746,14 +3749,14 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // the nodes to be merged are linked into the special linked list
     if ( fNewAlgo )
-        Abc_NtkFxPerform( pNtk, p->nNodesExt, p->LitCountMax, p->fVerbose );
+        Abc_NtkFxPerform( pNtk, p->nNodesExt, p->LitCountMax, p->fVerbose, p->fVeryVerbose );
     else
         Abc_NtkFastExtract( pNtk, p );
     Abc_NtkFxuFreeInfo( p );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: fx [-SDNWM <num>] [-sdzcnvh]\n");
+    Abc_Print( -2, "usage: fx [-SDNWM <num>] [-sdzcnvwh]\n");
     Abc_Print( -2, "\t           performs unate fast extract on the current network\n");
     Abc_Print( -2, "\t-S <num> : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax );
     Abc_Print( -2, "\t-D <num> : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax );
@@ -3766,6 +3769,7 @@ usage:
     Abc_Print( -2, "\t-c       : use complement in the binary case [default = %s]\n", p->fUseCompl? "yes": "no" );
     Abc_Print( -2, "\t-n       : use new implementation of fast extract [default = %s]\n", fNewAlgo? "yes": "no" );
     Abc_Print( -2, "\t-v       : print verbose information [default = %s]\n", p->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w       : print additional information [default = %s]\n", p->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");
     return 1;
 }
@@ -27414,7 +27418,7 @@ int Abc_CommandAbc9Balance( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fMultiExt    = 0;
     int fSimpleAnd   = 0;
     int fKeepLevel   = 0;
-    int c, fVerbose  = 1;
+    int c, fVerbose  = 0;
     int fVeryVerbose = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Nealvwh" ) ) != EOF )
diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c
index 5d887104..428d42bb 100644
--- a/src/base/abci/abcFx.c
+++ b/src/base/abci/abcFx.c
@@ -299,9 +299,9 @@ int Abc_NtkFxCheck( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int LitCountMax, int fVerbose )
+int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int LitCountMax, int fVerbose, int fVeryVerbose )
 {
-    extern int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fVerbose );
+    extern int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fVerbose, int fVeryVerbose );
     Vec_Wec_t * vCubes;
     assert( Abc_NtkIsSopLogic(pNtk) );
     // check unique fanins
@@ -318,7 +318,7 @@ int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int LitCountMax, int f
     // collect information about the covers
     vCubes = Abc_NtkFxRetrieve( pNtk );
     // call the fast extract procedure
-    if ( Fx_FastExtract( vCubes, Abc_NtkObjNumMax(pNtk), nNewNodesMax, LitCountMax, fVerbose ) > 0 )
+    if ( Fx_FastExtract( vCubes, Abc_NtkObjNumMax(pNtk), nNewNodesMax, LitCountMax, fVerbose, fVeryVerbose ) > 0 )
     {
         // update the network
         Abc_NtkFxInsert( pNtk, vCubes );
@@ -486,6 +486,7 @@ static void Fx_PrintStats( Fx_Man_t * p, abctime clk )
     printf( "Divs  =%7d  ", Hsh_VecSize(p->pHash) );
     printf( "Divs+ =%7d  ", Vec_QueSize(p->vPrio) );
     printf( "Compl =%6d  ", p->nDivMux[1] );
+    printf( "Extr  =%6d  ", p->nDivs );
 //    printf( "DivsS =%6d  ", p->nDivsS );
 //    printf( "PairS =%6d  ", p->nPairsS );
 //    printf( "PairD =%6d  ", p->nPairsD );
@@ -1110,9 +1111,9 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv )
   SeeAlso     []
 
 ***********************************************************************/
-int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fVerbose )
+int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fVerbose, int fVeryVerbose )
 {
-    int fVeryVerbose = 0;
+    int fVeryVeryVerbose = 0;
     int i, iDiv;
     Fx_Man_t * p;
     abctime clk = Abc_Clock();
@@ -1130,12 +1131,14 @@ int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitC
     for ( i = 0; i < nNewNodesMax && Vec_QueTopCost(p->vPrio) > 0.0; i++ )
     {
         iDiv = Vec_QuePop(p->vPrio);
-        if ( fVerbose )
+        if ( fVeryVerbose )
             Fx_PrintDiv( p, iDiv );
         Fx_ManUpdate( p, iDiv );
-        if ( fVeryVerbose )
+        if ( fVeryVeryVerbose )
             Fx_PrintMatrix( p );
     }
+    if ( fVerbose )
+        Fx_PrintStats( p, Abc_Clock() - clk );
     Fx_ManStop( p );
     // return the result
     Vec_WecRemoveEmpty( vCubes );
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index b0106636..15b304b0 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -49,7 +49,7 @@ extern int  Fxu_FastExtract( Fxu_Data_t * pData );
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSetDefaultParams( Fxu_Data_t * p )
+void Abc_NtkSetDefaultFxParams( Fxu_Data_t * p )
 {
     memset( p, 0, sizeof(Fxu_Data_t) );
     p->nSingleMax =  20000;
diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h
index e8ef6586..21eaa85e 100644
--- a/src/opt/fxu/fxu.h
+++ b/src/opt/fxu/fxu.h
@@ -50,6 +50,7 @@ struct FxuDataStruct
     int               fUse0;            // set to 1 to have 0-weight also extracted
     int               fUseCompl;        // set to 1 to have complement taken into account
     int               fVerbose;         // set to 1 to have verbose output
+    int               fVeryVerbose;     // set to 1 to have more verbose output
     int               nNodesExt;        // the number of divisors to extract
     int               nSingleMax;       // the max number of single-cube divisors to consider
     int               nPairsMax;        // the max number of double-cube divisors to consider
@@ -77,7 +78,7 @@ struct FxuDataStruct
 ////////////////////////////////////////////////////////////////////////
 
 /*===== fxu.c ==========================================================*/
-extern void   Abc_NtkSetDefaultParams( Fxu_Data_t * p );
+extern void   Abc_NtkSetDefaultFxParams( Fxu_Data_t * p );
 extern int    Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p );
 extern void   Abc_NtkFxuFreeInfo( Fxu_Data_t * p );