Added printout of BMC tents in &ps.

10 files changed, 46 insertions, 28 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 23beca19..96cfda34 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -742,7 +742,7 @@ extern void                Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pP
 extern Gia_Man_t *         Gia_ManStart( int nObjsMax ); 
 extern void                Gia_ManStop( Gia_Man_t * p );  
 extern void                Gia_ManStopP( Gia_Man_t ** p );  
-extern void                Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ); 
+extern void                Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch ); 
 extern void                Gia_ManPrintStatsShort( Gia_Man_t * p ); 
 extern void                Gia_ManPrintMiterStatus( Gia_Man_t * p ); 
 extern void                Gia_ManSetRegNum( Gia_Man_t * p, int nRegs );
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index e25ff7fb..2efc73e4 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -292,7 +292,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars )
     Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd );
     Vec_IntFree( vAbsFfsToAdd );
     if ( p->fVerbose )
-        Gia_ManPrintStats( pGia, 0 );
+        Gia_ManPrintStats( pGia, 0, 0 );
     return -1;
 }
 
@@ -365,7 +365,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit
     }
     Aig_ManStop( pAig );
     if ( fVerbose )
-        Gia_ManPrintStats( pGia, 0 );
+        Gia_ManPrintStats( pGia, 0, 0 );
     return RetValue;
 }
 
@@ -409,7 +409,7 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
     Vec_IntFreeP( &vGateClassesOld );
     pGia->vGateClasses = vGateClasses;
     if ( p->fVerbose )
-        Gia_ManPrintStats( pGia, 0 );
+        Gia_ManPrintStats( pGia, 0, 0 );
     return 1;
 }
 
@@ -494,7 +494,7 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver )
         Gia_ManStop( pGiaAbs );
     }
     if ( p->fVerbose )
-        Gia_ManPrintStats( pGia, 0 );
+        Gia_ManPrintStats( pGia, 0, 0 );
     return 1;
 }
 
diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c
index 60dcf3af..49142683 100644
--- a/src/aig/gia/giaCof.c
+++ b/src/aig/gia/giaCof.c
@@ -862,7 +862,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose
     if ( fVerbose )
     { 
         printf( "Cofactoring %d signals.\n", Vec_IntSize(vSigs) );
-        Gia_ManPrintStats( p, 0 );
+        Gia_ManPrintStats( p, 0, 0 );
     }
     if ( Vec_IntSize( vSigs ) > 200 )
     {
@@ -888,7 +888,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose
         if ( fVerbose )
             printf( "Cofactored variable %d.\n", iVar );
         if ( fVerbose )
-            Gia_ManPrintStats( pAig, 0 );
+            Gia_ManPrintStats( pAig, 0, 0 );
     }
     Vec_IntFree( vSigsNew );
     return pAig;
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index e244ef46..3c5ad848 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1686,7 +1686,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
     }
     // (spech)*  where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim
     Gia_ManCleanMark0( pGia );
-    Gia_ManPrintStats( pGia, 0 );
+    Gia_ManPrintStats( pGia, 0, 0 );
     for ( nIter = 0; ; nIter++ )
     {
         if ( Gia_ManHasNoEquivs(pGia) )
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 80fcf896..0e08341c 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -363,7 +363,7 @@ void Gia_ManPrintPlacement( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch )
+void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch )
 {
     if ( p->pName )
         printf( "%-8s : ", p->pName );
@@ -399,6 +399,19 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch )
     Gia_ManPrintFlopClasses( p );
     Gia_ManPrintGateClasses( p );
     Gia_ManPrintObjClasses( p );
+    if ( fTents )
+    {
+        int k, Entry, Prev = 1;
+        Vec_Int_t * vLimit = Vec_IntAlloc( 1000 );
+        Gia_Man_t * pNew = Gia_ManUnrollDup( p, vLimit );
+        printf( "Tents:  " );
+        Vec_IntForEachEntryStart( vLimit, Entry, k, 1 )
+            printf( "%d = %d  ", k, Entry-Prev ), Prev = Entry;
+        printf( " Unused = %d.", Gia_ManObjNum(p) - Gia_ManObjNum(pNew) );
+        printf( "\n" );
+        Vec_IntFree( vLimit );
+        Gia_ManStop( pNew );
+    }
 }
 
 /**Function*************************************************************
diff --git a/src/aig/gia/giaReparam.c b/src/aig/gia/giaReparam.c
index 10294671..59a45477 100644
--- a/src/aig/gia/giaReparam.c
+++ b/src/aig/gia/giaReparam.c
@@ -147,7 +147,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose )
     if ( fVerbose )
     {
         printf( "Original AIG:\n" );
-        Gia_ManPrintStats( p, 0 );
+        Gia_ManPrintStats( p, 0, 0 );
     }
 
     // perform input trimming
@@ -155,7 +155,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose )
     if ( fVerbose )
     {
         printf( "After PI trimming:\n" );
-        Gia_ManPrintStats( pNew, 0 );
+        Gia_ManPrintStats( pNew, 0, 0 );
     }
     // transform GIA
     pNew = Gia_ManDupIn2Ff( pTmp = pNew );
@@ -163,7 +163,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose )
     if ( fVerbose )
     {
         printf( "After PI-2-FF transformation:\n" );
-        Gia_ManPrintStats( pNew, 0 );
+        Gia_ManPrintStats( pNew, 0, 0 );
     }
 
     // derive AIG
@@ -178,7 +178,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose )
     if ( fVerbose )
     {
         printf( "After min-area retiming:\n" );
-        Gia_ManPrintStats( pNew, 0 );
+        Gia_ManPrintStats( pNew, 0, 0 );
     }
 
     // transform back
@@ -187,7 +187,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose )
     if ( fVerbose )
     {
         printf( "After FF-2-PI tranformation:\n" );
-        Gia_ManPrintStats( pNew, 0 );
+        Gia_ManPrintStats( pNew, 0, 0 );
     }
     return pNew;
 }
diff --git a/src/base/abc/abcHieCec.c b/src/base/abc/abcHieCec.c
index 3210ad48..b3a3718f 100644
--- a/src/base/abc/abcHieCec.c
+++ b/src/base/abc/abcHieCec.c
@@ -402,7 +402,7 @@ Gia_Man_t * Abc_NtkDeriveFlatGia2Derive( Abc_Ntk_t * pNtk, Vec_Ptr_t * vOrder )
     Gia_ManStop( pGiaBox );
 
     printf( "%8d -> ", Abc_NtkCountAndNodes(vOrder) );
-    Gia_ManPrintStats( pGia, 0 );
+    Gia_ManPrintStats( pGia, 0, 0 );
     return pGia;
 }
 /*
@@ -721,7 +721,7 @@ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose )
         clk = clock();
         pGia = Abc_NtkDeriveFlatGia2( pNtk, vOrder );
         Abc_PrintTime( 1, "Deriving GIA", clock() - clk );
-        Gia_ManPrintStats( pGia, 0 );
+        Gia_ManPrintStats( pGia, 0, 0 );
     //    Gia_ManStop( pGia );
  
         Vec_PtrFree( vOrder );
@@ -737,7 +737,7 @@ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose )
         clk = clock();
         pGia = Abc_NtkDeriveFlatGia( pNtk );
         Abc_PrintTime( 1, "Deriving GIA", clock() - clk );
-        Gia_ManPrintStats( pGia, 0 );
+        Gia_ManPrintStats( pGia, 0, 0 );
 
         // clean nodes/boxes of all nodes
         Vec_PtrForEachEntry( Abc_Ntk_t *, vMods, pModel, i )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8bf1c60e..15e314db 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -22031,11 +22031,15 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     int c;
     int fSwitch = 0;
+    int fTents = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ph" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "tph" ) ) != EOF )
     {
         switch ( c )
         {
+        case 't':
+            fTents ^= 1;
+            break;
         case 'p':
             fSwitch ^= 1;
             break;
@@ -22050,12 +22054,13 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Ps(): There is no AIG.\n" );
         return 1;
     } 
-    Gia_ManPrintStats( pAbc->pGia, fSwitch );
+    Gia_ManPrintStats( pAbc->pGia, fTents, fSwitch );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &ps [-ph]\n" );
+    Abc_Print( -2, "usage: &ps [-tph]\n" );
     Abc_Print( -2, "\t        prints stats of the current AIG\n" );
+    Abc_Print( -2, "\t-t    : toggle printing BMC tents [default = %s]\n", fTents? "yes": "no" );
     Abc_Print( -2, "\t-p    : toggle printing switching activity [default = %s]\n", fSwitch? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
diff --git a/src/misc/util/utilSort.c b/src/misc/util/utilSort.c
index 380a8885..eb2b32c3 100644
--- a/src/misc/util/utilSort.c
+++ b/src/misc/util/utilSort.c
@@ -509,7 +509,7 @@ void Abc_QuickSort1( word * pData, int nSize, int fDecrease )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Iso_SelectSortInc( word * pData, int nSize )
+static inline void Abc_SelectSortInc( word * pData, int nSize )
 {
     int i, j, best_i;
     for ( i = 0; i < nSize-1; i++ )
@@ -521,7 +521,7 @@ static inline void Iso_SelectSortInc( word * pData, int nSize )
         ABC_SWAP( word, pData[i], pData[best_i] );
     }
 }
-static inline void Iso_SelectSortDec( word * pData, int nSize )
+static inline void Abc_SelectSortDec( word * pData, int nSize )
 {
     int i, j, best_i;
     for ( i = 0; i < nSize-1; i++ )
@@ -543,7 +543,7 @@ void Abc_QuickSort2Inc_rec( word * pData, int l, int r )
     assert( l < r );
     if ( r - l < 10 )
     {
-        Iso_SelectSortInc( pData + l, r - l + 1 );
+        Abc_SelectSortInc( pData + l, r - l + 1 );
         return;
     }
     while ( 1 )
@@ -569,7 +569,7 @@ void Abc_QuickSort2Dec_rec( word * pData, int l, int r )
     assert( l < r );
     if ( r - l < 10 )
     {
-        Iso_SelectSortDec( pData + l, r - l + 1 );
+        Abc_SelectSortDec( pData + l, r - l + 1 );
         return;
     }
     while ( 1 )
@@ -596,7 +596,7 @@ void Abc_QuickSort3Inc_rec( word * pData, int l, int r )
     assert( l < r );
     if ( r - l < 10 )
     {
-        Iso_SelectSortInc( pData + l, r - l + 1 );
+        Abc_SelectSortInc( pData + l, r - l + 1 );
         return;
     }
     while ( 1 )
@@ -631,7 +631,7 @@ void Abc_QuickSort3Dec_rec( word * pData, int l, int r )
     assert( l < r );
     if ( r - l < 10 )
     {
-        Iso_SelectSortDec( pData + l, r - l + 1 );
+        Abc_SelectSortDec( pData + l, r - l + 1 );
         return;
     }
     while ( 1 )
@@ -678,7 +678,7 @@ void Abc_QuickSort2( word * pData, int nSize, int fDecrease )
 }
 void Abc_QuickSort3( word * pData, int nSize, int fDecrease )
 {
-    int i, fVerify = 0;
+    int i, fVerify = 1;
     if ( fDecrease )
     {
         Abc_QuickSort2Dec_rec( pData, 0, nSize - 1 );
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index bf41304b..65c4b970 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -400,7 +400,7 @@ p->timeSim += clock() - clk;
 //        Gia_WriteAiger( pSrm, "gia_srm.aig", 0, 0 );
 
         if ( pPars->fVeryVerbose )
-            Gia_ManPrintStats( pSrm, 0 );
+            Gia_ManPrintStats( pSrm, 0, 0 );
         if ( Gia_ManCoNum(pSrm) == 0 )
         {
             Gia_ManStop( pSrm );