Changing the print-out of &iso.

src/aig/gia/gia.h

@@ -951,7 +951,7 @@ extern void                Gia_ManSetIfParsDefault( void * pIfPars );
 extern Gia_Man_t *         Gia_ManPerformMapping( Gia_Man_t * p, void * pIfPars );
 /*=== giaIso.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose );
-extern Gia_Man_t *         Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fDualOut, int fVerbose );
+extern Gia_Man_t *         Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fDualOut, int fVerbose, int fVeryVerbose );
 /*=== giaLogic.c ===========================================================*/
 extern void                Gia_ManTestDistance( Gia_Man_t * p );
 extern void                Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars );

src/aig/gia/giaIso.c

@@ -1080,9 +1080,8 @@ Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose, Vec_Int_
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fDualOut, int fVerbose )
+Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fDualOut, int fVerbose, int fVeryVerbose )
 { 
-    int fVeryVerbose = 0;
     Gia_Man_t * p, * pPart;
     Vec_Ptr_t * vEquivs, * vEquivs2, * vStrings;
     Vec_Int_t * vRemain, * vLevel, * vLevel2;
@@ -1118,8 +1117,8 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_P
             Gia_ManStop( p );
         return NULL;
     }
-//    printf( "Reduced %d outputs to %d outputs.  ", Gia_ManPoNum(p), Vec_PtrSize(vEquivs) );
-//    Abc_PrintTime( 1, "Time", clock() - clk );
+    printf( "Reduced %d outputs to %d candidate classes.  ", Gia_ManPoNum(p), Vec_PtrSize(vEquivs) );
+    Abc_PrintTime( 1, "Time", clock() - clk );
 
     // perform refinement of equivalence classes
     Counter = 0;
@@ -1134,6 +1133,16 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_P
                     printf( "%6d finished...\r", Counter );
             continue;
         }
+
+        if ( fVerbose )
+        {
+            iPo = Vec_IntEntry(vLevel, 0);
+            printf( "%6d %6d %6d : ", i, Vec_IntSize(vLevel), iPo );
+            pPart = Gia_ManDupCones( p, &iPo, 1, 1 );
+            Gia_ManPrintStats(pPart, 0, 0, 0);
+            Gia_ManStop( pPart );
+        }
+
         sStart = Vec_PtrSize( vEquivs2 ); 
         vStrings = Vec_PtrAlloc( 100 );
         Vec_IntForEachEntry( vLevel, iPo, k )
@@ -1283,7 +1292,7 @@ void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
 //Gia_AigerWrite( pDouble, "test.aig", 0, 0 );
 
     // analyze the two-output miter
-    pAig = Gia_ManIsoReduce( pDouble, &vPosEquivs, &vPisPerm, 0, 0 );
+    pAig = Gia_ManIsoReduce( pDouble, &vPosEquivs, &vPisPerm, 0, 0, 0 );
     Vec_VecFree( (Vec_Vec_t *)vPosEquivs );
 
     // given CEX for output 0, derive CEX for output 1

src/base/abci/abc.c

@@ -29808,9 +29808,9 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_Man_t * pAig;
     Vec_Ptr_t * vPosEquivs;
 //    Vec_Ptr_t * vPiPerms;
-    int c, fDualOut = 0, fVerbose = 0;
+    int c, fDualOut = 0, fVerbose = 0, fVeryVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "dvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "dvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -29820,6 +29820,9 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'v':
             fVerbose ^= 1;
             break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -29836,8 +29839,8 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Iso(): The AIG has only one PO. Isomorphism detection is not performed.\n" );
         return 1;
     }
-    pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, NULL, fDualOut, fVerbose );
-//    pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, &vPiPerms, fDualOut, fVerbose );
+    pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, NULL, fDualOut, fVerbose, fVeryVerbose );
+//    pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, &vPiPerms, fDualOut, fVerbose, fVeryVerbose );
 //    Vec_VecFree( (Vec_Vec_t *)vPiPerms );
     if ( pAig == NULL )
     {
@@ -29851,10 +29854,11 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &iso [-dvh]\n" );
+    Abc_Print( -2, "usage: &iso [-dvwh]\n" );
     Abc_Print( -2, "\t         removes POs with isomorphic sequential COI\n" );
     Abc_Print( -2, "\t-d     : treat the current AIG as a dual-output miter [default = %s]\n", fDualOut? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w     : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }