Improvements to 'bmc3' (start frame; stop when all POs are SAT; stop when 2^nRegs frames are completed).

2 files changed, 26 insertions, 9 deletions

diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index 453ea918..508a46c1 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -1098,6 +1098,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     Gia_ManBmc_t * p;
     Aig_Obj_t * pObj;
     int RetValue = -1, fFirst = 1;
+    int nOutDigits = Aig_Base10Log( Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) );
     int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock();
     if ( pPars->fVerbose && Aig_ManConstrNum(pAig) > 0 )
         printf( "Performing BMC with constraints...\n" );
@@ -1119,6 +1120,19 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     Saig_ManBmcMarkPis( pAig, pPars->nPisAbstract );
     for ( f = 0; f < pPars->nFramesMax; f++ )
     {
+        // stop BMC after exploring all reachable states
+        if ( Aig_ManRegNum(pAig) < 30 && f == (1 << Aig_ManRegNum(pAig)) )
+        {
+            Saig_Bmc3ManStop( p );
+            return pPars->nFailOuts ? 0 : 1;
+        }
+        // stop BMC if all targets are solved
+        if ( pPars->fSolveAll && pPars->nFailOuts == Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) )
+        {
+            Saig_Bmc3ManStop( p );
+            return 0;
+        }
+        // consider the next timeframe
         pPars->iFrame = f;
         // resize the array
         Vec_IntFillExtra( p->vPiVars, (f+1)*Saig_ManPiNum(p->pAig), 0 );
@@ -1158,8 +1172,10 @@ clkOther += clock() - clk2;
                 return 1;
             }
         }
+        if ( pPars->nStart && f < pPars->nStart )
+            continue;
         // solve SAT
-        clk = clock();
+        clk = clock(); 
         Saig_ManForEachPo( pAig, pObj, i )
         {
             if ( i >= Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) )
@@ -1176,15 +1192,17 @@ clkOther += clock() - clk2;
             if ( Lit == 1 )
             {
                 Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
-                printf( "Output %d is trivially SAT in frame %d.\n", i, f );
                 if ( !pPars->fSolveAll )
                 {
+                    printf( "Output %d is trivially SAT in frame %d.\n", i, f );
                     ABC_FREE( pAig->pSeqModel );
                     pAig->pSeqModel = pCex;
                     Saig_Bmc3ManStop( p );
                     return 0;
                 }
                 pPars->nFailOuts++;
+                printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
+                    nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) );
                 if ( p->vCexes == NULL )
                     p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
                 Vec_PtrWriteEntry( p->vCexes, i, pCex );
@@ -1231,7 +1249,8 @@ clkOther += clock() - clk2;
                     return 0;
                 }
                 pPars->nFailOuts++;
-                printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n",  i, f );
+                printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
+                    nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) );
                 if ( p->vCexes == NULL )
                     p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
                 Vec_PtrWriteEntry( p->vCexes, i, pCex );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index c0822ba9..064529cc 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1805,8 +1805,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
     pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     if ( RetValue == 1 )
     {
-//        printf( "No output asserted in %d frames. ", pPars->iFrame );
-        printf( "Incorrect return value.  " );
+        printf( "Explored all reachable states after completing %d frames.  ", 1<<Aig_ManRegNum(pMan) );
     }
     else if ( RetValue == -1 )
     {
@@ -1839,8 +1838,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
         }
         else
         {
-            printf( "Incorrect return value.  " );
-//            printf( "At least one output asserted (out=%d, frame=%d). ", pCex->iPo, pCex->iFrame );
+            printf( "All %d outputs are proved SAT.    ", Saig_ManPoNum(pMan) - pMan->nConstrs );
         }
     }
     ABC_PRT( "Time", clock() - clk );
@@ -3044,8 +3042,8 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize,
     }
     else
     {
-        printf( "Simulation of %d frames with %d words did not assert the outputs.    ", 
-            nFrames, nWords );
+//        printf( "Simulation of %d frames with %d words did not assert the outputs.    ", 
+//            nFrames, nWords );
     }
     ABC_PRT( "Time", clock() - clk );
     Aig_ManStop( pMan );