Counter-example analysis and optimization.

src/base/abci/abc.c

@@ -28865,7 +28865,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9CexInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex );
+    extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose );
     int c, fDualOut = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "dvh" ) ) != EOF )
@@ -28894,12 +28894,12 @@ int Abc_CommandAbc9CexInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9CexInfo(): There is no CEX.\n" );
         return 1;
     }
-    Bmc_CexTest( pAbc->pGia, pAbc->pCex );
+    Bmc_CexTest( pAbc->pGia, pAbc->pCex, fVerbose );
     return 0;
 
 usage:
     Abc_Print( -2, "usage: &cexinfo [-vh]\n" );
-    Abc_Print( -2, "\t         prints information about counter-examples\n" );
+    Abc_Print( -2, "\t         prints information about the current counter-example\n" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -30192,8 +30192,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern int Gia_ManSuppSizeTest( Gia_Man_t * p );
 //    extern void Gia_VtaTest( Gia_Man_t * p, int nFramesStart, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose );
 //    extern void Gia_IsoTest( Gia_Man_t * p, int fVerbose );
-    extern void Ga2_ManComputeTest( Gia_Man_t * p );
-    extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex );
+//    extern void Ga2_ManComputeTest( Gia_Man_t * p );
+//    extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose );
 
 
     Extra_UtilGetoptReset();
@@ -30239,7 +30239,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Gia_VtaTest( pAbc->pGia, 10, 100000, 0, 0, 1 );
 //    Gia_IsoTest( pAbc->pGia, fVerbose );
 //    Ga2_ManComputeTest( pAbc->pGia );
-    Bmc_CexTest( pAbc->pGia, pAbc->pCex );
+//    Bmc_CexTest( pAbc->pGia, pAbc->pCex, fVerbose );
     return 0;
 usage:
     Abc_Print( -2, "usage: &test [-svh]\n" );

src/sat/bmc/bmcCexTools.c

@@ -48,10 +48,11 @@ static inline int  Bmc_CexSim( Vec_Wrd_t * vSims, int iObj, int i )
   SeeAlso     []
 
 ***********************************************************************/
-void Bmc_CexPrint( Abc_Cex_t * pCex, int nInputs )
+void Bmc_CexPrint( Abc_Cex_t * pCex, int nInputs, int fVerbose )
 {
     int i, k, Count, iBit = 0;
     Abc_CexPrintStatsInputs( pCex, nInputs );
+    if ( !fVerbose )
         return;
 
     for ( i = 0; i <= pCex->iFrame; i++ )
@@ -128,7 +129,7 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Cex_t * Bmc_CexInnerStates( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t ** ppCexImpl )
+Abc_Cex_t * Bmc_CexInnerStates( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t ** ppCexImpl, int fVerbose )
 {
     Abc_Cex_t * pNew, * pNew2;
     Gia_Obj_t * pObj, * pObjRo, * pObjRi;
@@ -210,9 +211,9 @@ Abc_Cex_t * Bmc_CexInnerStates( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t ** pp
     assert( Gia_ManPo(p, pCex->iPo)->fMark0 == 1 );
 
     printf( "Inner states: " );
-    Bmc_CexPrint( pNew, Gia_ManPiNum(p) );
+    Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
     printf( "Implications: " );
-    Bmc_CexPrint( pNew2, Gia_ManPiNum(p) );
+    Bmc_CexPrint( pNew2, Gia_ManPiNum(p), fVerbose );
     if ( ppCexImpl )
         *ppCexImpl = pNew2;
     else
@@ -290,7 +291,7 @@ void Bmc_CexCareBits2_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
             Bmc_CexCareBits2_rec( p, Gia_ObjFanin1(pObj) );
     }
 }
-Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexImpl, Abc_Cex_t * pCexEss, int fFindAll )
+Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexImpl, Abc_Cex_t * pCexEss, int fFindAll, int fVerbose )
 {
     Abc_Cex_t * pNew;
     Gia_Obj_t * pObj;
@@ -365,8 +366,11 @@ Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * p
                     Abc_InfoSetBit(pNew->pData, pNew->nPis * i + k);
             }
     }
+    if ( pCexEss )
+        printf( "Minimized:    " );
+    else
         printf( "Care bits:    " );
-    Bmc_CexPrint( pNew, Gia_ManPiNum(p) );
+    Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
     return pNew;
 }
 
@@ -472,7 +476,7 @@ void Bmc_CexEssentialBitTest( Gia_Man_t * p, Abc_Cex_t * pCexState )
         if ( b % 100 )
             continue;
         pNew = Bmc_CexEssentialBitOne( p, pCexState, b, NULL, NULL );
-        Bmc_CexPrint( pNew, Gia_ManPiNum(p) );
+        Bmc_CexPrint( pNew, Gia_ManPiNum(p), 0 );
 
         if ( Gia_ManPo(p, pCexState->iPo)->fMark1 )
             printf( "Not essential\n" );
@@ -494,7 +498,7 @@ void Bmc_CexEssentialBitTest( Gia_Man_t * p, Abc_Cex_t * pCexState )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexCare )
+Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexCare, int fVerbose )
 {
     Abc_Cex_t * pNew, * pTemp, * pPrev = NULL;
     int b, fEqual = 0, fPrevStatus = 0;
@@ -527,7 +531,7 @@ Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_
                 Abc_InfoSetBit( pNew->pData, b );
             continue;
         }
-//        Bmc_CexPrint( pTemp, Gia_ManPiNum(p) );
+//        Bmc_CexPrint( pTemp, Gia_ManPiNum(p), fVerbose );
         Abc_CexFree( pPrev );
         pPrev = pTemp;
 
@@ -539,7 +543,7 @@ Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_
     Abc_CexFreeP( &pPrev );
 //    Abc_PrintTime( 1, "Time", clock() - clk );
     printf( "Essentials:   " );
-    Bmc_CexPrint( pNew, Gia_ManPiNum(p) );
+    Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
     return pNew;
 }
  
@@ -619,19 +623,19 @@ void Bmc_CexDumpStats( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare, Ab
   SeeAlso     []
 
 ***********************************************************************/
-void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex )
+void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
 {
     clock_t clk = clock();
     Abc_Cex_t * pCexImpl   = NULL;
-    Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl );
-    Abc_Cex_t * pCexCare   = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1 );
+    Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose );
+    Abc_Cex_t * pCexCare   = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose );
     Abc_Cex_t * pCexEss, * pCexMin;
 
     if ( !Bmc_CexVerify( p, pCex, pCexCare ) )
         printf( "Counter-example care-set verification has failed.\n" );
 
-    pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare );
-    pCexMin = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0 );
+    pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare, fVerbose );
+    pCexMin = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0, fVerbose );
 
     if ( !Bmc_CexVerify( p, pCex, pCexMin ) )
         printf( "Counter-example min-set verification has failed.\n" );