Improving CEX minimization.

src/base/io/io.c

@@ -2420,7 +2420,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
                         Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose );
                 }
                 else
-                    pCare = Bmc_CexCareMinimize( pAig, pCex, fCheckCex, fVerbose );
+                    pCare = Bmc_CexCareMinimize( pAig, 0, pCex, fCheckCex, fVerbose );
                 Aig_ManStop( pAig );
             }
             // output flop values (unaffected by the minimization)

src/misc/util/utilCex.c

@@ -272,9 +272,9 @@ void Abc_CexPrintStats( Abc_Cex_t * p )
         p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, 
         Counter, 100.0 * Counter / (p->nBits - p->nRegs) );
 }
-void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs )
+void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nRealPis )
 {
-    int k, Counter = 0, Counter2 = 0;
+    int k, Counter = 0, CounterPi = 0, CounterPpi = 0;
     if ( p == NULL )
     {
         printf( "The counter example is NULL.\n" );
@@ -285,16 +285,27 @@ void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs )
         printf( "The counter example is present but not available (pointer has value \"1\").\n" );
         return;
     }
+    assert( nRealPis <= p->nPis );
     for ( k = 0; k < p->nBits; k++ )
     {
         Counter += Abc_InfoHasBit(p->pData, k);
-        if ( (k - p->nRegs) % p->nPis < nInputs )
-            Counter2 += Abc_InfoHasBit(p->pData, k);
+        if ( nRealPis == p->nPis )
+            continue;
+        if ( (k - p->nRegs) % p->nPis < nRealPis )
+            CounterPi += Abc_InfoHasBit(p->pData, k);
+        else
+            CounterPpi += Abc_InfoHasBit(p->pData, k);
     }
-    printf( "CEX: Po =%4d  Frame =%4d  FF = %d  PI = %d  Bit =%8d  1s =%8d (%5.2f %%) 1sIn =%8d (%5.2f %%)\n", 
+    printf( "CEX: Po =%4d  Fr =%4d  FF = %d  PI = %d  Bit =%7d  1 =%8d (%5.2f %%)", 
         p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, 
-        Counter,  100.0 * Counter  / (p->nBits - p->nRegs), 
-        Counter2, 100.0 * Counter2 / (p->nBits - p->nRegs - (p->iFrame + 1) * (p->nPis - nInputs)) );
+        Counter,  100.0 * Counter    / ((p->iFrame + 1) * p->nPis ) );
+    if ( nRealPis < p->nPis )
+    {
+        printf( " 1pi =%8d (%5.2f %%) 1ppi =%8d (%5.2f %%)", 
+            CounterPi,  100.0 * CounterPi  / ((p->iFrame + 1) * nRealPis ), 
+            CounterPpi, 100.0 * CounterPpi / ((p->iFrame + 1) * (p->nPis - nRealPis)) );
+    }
+    printf( "\n" );
 }
 
 /**Function*************************************************************

src/sat/bmc/bmc.h

@@ -164,7 +164,7 @@ extern int               Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t *
 extern int               Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars );
 /*=== bmcCexCare.c ==========================================================*/
 extern Abc_Cex_t *       Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
-extern Abc_Cex_t *       Bmc_CexCareMinimize( Aig_Man_t * p, Abc_Cex_t * pCex, int fCheck, int fVerbose );
+extern Abc_Cex_t *       Bmc_CexCareMinimize( Aig_Man_t * p, int nPPis, Abc_Cex_t * pCex, int fCheck, int fVerbose );
 extern void              Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
 /*=== bmcCexCut.c ==========================================================*/
 extern Gia_Man_t *       Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
@@ -172,7 +172,7 @@ extern Aig_Man_t *       Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, i
 /*=== bmcCexMin.c ==========================================================*/
 extern Abc_Cex_t *       Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
 /*=== bmcCexTool.c ==========================================================*/
-extern void              Bmc_CexPrint( Abc_Cex_t * pCex, int nInputs, int fVerbose );
+extern void              Bmc_CexPrint( Abc_Cex_t * pCex, int nRealPis, int fVerbose );
 extern int               Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
 /*=== bmcICheck.c ==========================================================*/
 extern void              Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose );

src/sat/bmc/bmcCexTools.c

@@ -304,10 +304,10 @@ void Bmc_CexBuildNetworkTest( Gia_Man_t * p, Abc_Cex_t * pCex )
   SeeAlso     []
 
 ***********************************************************************/
-void Bmc_CexPrint( Abc_Cex_t * pCex, int nInputs, int fVerbose )
+void Bmc_CexPrint( Abc_Cex_t * pCex, int nRealPis, int fVerbose )
 {
     int i, k, Count, iBit = pCex->nRegs;
-    Abc_CexPrintStatsInputs( pCex, nInputs );
+    Abc_CexPrintStatsInputs( pCex, nRealPis );
     if ( !fVerbose )
         return;
 
@@ -315,7 +315,7 @@ void Bmc_CexPrint( Abc_Cex_t * pCex, int nInputs, int fVerbose )
     {
         Count = 0;
         printf( "%3d : ", i );
-        for ( k = 0; k < nInputs; k++ )
+        for ( k = 0; k < nRealPis; k++ )
         {
             Count += Abc_InfoHasBit(pCex->pData, iBit);
             printf( "%d", Abc_InfoHasBit(pCex->pData, iBit++) );