Updates for the new BMC engine.

src/base/abci/abc.c

@@ -31619,6 +31619,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nFramesMax    =    0;  // maximum number of timeframes 
     pPars->nConfLimit    =    0;  // maximum number of conflicts at a node
     pPars->fLoadCnf      =    0;  // dynamic CNF loading
+    pPars->fDumpFrames   =    0;  // dump unrolled timeframes
     pPars->fVerbose      =    0;  // verbose 
     pPars->fVeryVerbose  =    0;  // very verbose 
     pPars->fNotVerbose   =    0;  // skip line-by-line print-out 
@@ -31626,7 +31627,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nFailOuts     =    0;  // the number of failed outputs
     pPars->nDropOuts     =    0;  // the number of dropped outputs
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SFcvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFcdvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -31655,6 +31656,9 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             pPars->fLoadCnf ^= 1;
             break;
+        case 'd':
+            pPars->fDumpFrames ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -31677,12 +31681,13 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &bmc [-SF num] [-cvwh]\n" );
+    Abc_Print( -2, "usage: &bmc [-SF num] [-cdvwh]\n" );
     Abc_Print( -2, "\t         performs bounded model checking\n" );
-    Abc_Print( -2, "\t-S num : the starting timeframe [default = %d]\n",              pPars->nStart );
-    Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n",    pPars->nFramesMax );
-    Abc_Print( -2, "\t-c     : toggle dynamic CNF loading [default = %s]\n",          pPars->fLoadCnf? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-S num : the starting timeframe [default = %d]\n",                      pPars->nStart );
+    Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n",            pPars->nFramesMax );
+    Abc_Print( -2, "\t-c     : toggle dynamic CNF loading [default = %s]\n",                  pPars->fLoadCnf? "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle dumping unfolded timeframes [default = %s]\n",          pPars->fDumpFrames? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",         pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing information about unfolding [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;

src/sat/bmc/bmc.h

@@ -79,6 +79,7 @@ struct Bmc_AndPar_t_
     int         nFramesMax;     // maximum number of timeframes 
     int         nConfLimit;     // maximum number of conflicts at a node
     int         fLoadCnf;       // dynamic CNF loading
+    int         fDumpFrames;    // dump unrolled timeframes
     int         fVerbose;       // verbose 
     int         fVeryVerbose;   // very verbose 
     int         fNotVerbose;    // skip line-by-line print-out