From 0d65c49048eea6940e3f5fa9bbf28ee5c6b97102 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 31 Jul 2011 20:22:57 +0700
Subject: Improvements to 'bmc3' (start frame; stop when all POs are SAT; stop
 when 2^nRegs frames are completed).

---
 src/aig/saig/saigBmc3.c | 25 ++++++++++++++++++++++---
 1 file changed, 22 insertions(+), 3 deletions(-)

(limited to 'src/aig/saig')

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 );
-- 
cgit v1.2.3