Reducing memory usage in bmc2 and bmc3.

1 files changed, 19 insertions, 7 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index fa2aa375..9167c54c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -19927,6 +19927,11 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Does not work for combinational networks.\n" );
         return 0;
     }
+    if ( Abc_NtkConstrNum(pNtk) > 0 )
+    {
+        Abc_Print( -1, "Constraints have to be folded (use \"fold\").\n" );
+        return 0;
+    }
     pAbc->Status = Abc_NtkDarBmc3( pNtk, pPars, fOrDecomp );
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
@@ -24162,10 +24167,11 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_ParFra_t Pars, * pPars = &Pars;
     int c;
     int nCofFanLit = 0;
-    int nNewAlgo = 1;
+    int fNewAlgo = 1;
+    int fInitSpecial = 0;
     Gia_ManFraSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FLiavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FLiasvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -24195,7 +24201,10 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
             pPars->fInit ^= 1;
             break;
         case 'a':
-            nNewAlgo ^= 1;
+            fNewAlgo ^= 1;
+            break;
+        case 's':
+            fInitSpecial ^= 1;
             break;
         case 'v':
             pPars->fVerbose ^= 1;
@@ -24216,9 +24225,11 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "The network is combinational.\n" );
         return 0;
     }
-    if ( nCofFanLit )
+    if ( fInitSpecial )
+        pTemp = Gia_ManFramesInitSpecial( pAbc->pGia, pPars->nFrames, pPars->fVerbose );
+    else if ( nCofFanLit )
         pTemp = Gia_ManUnrollAndCofactor( pAbc->pGia, pPars->nFrames, nCofFanLit, pPars->fVerbose );
-    else if ( nNewAlgo )
+    else if ( fNewAlgo )
         pTemp = Gia_ManFrames2( pAbc->pGia, pPars );
     else 
         pTemp = Gia_ManFrames( pAbc->pGia, pPars );
@@ -24226,12 +24237,13 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &frames [-FL <num>] [-aivh]\n" );
+    Abc_Print( -2, "usage: &frames [-FL <num>] [-iasvh]\n" );
     Abc_Print( -2, "\t         unrolls the design for several timeframes\n" );
     Abc_Print( -2, "\t-F num : the number of frames to unroll [default = %d]\n", pPars->nFrames );
     Abc_Print( -2, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit );
     Abc_Print( -2, "\t-i     : toggle initializing registers [default = %s]\n", pPars->fInit? "yes": "no" );
-    Abc_Print( -2, "\t-a     : toggle using new algorithm [default = %s]\n", nNewAlgo? "yes": "no" );
+    Abc_Print( -2, "\t-a     : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggle computing special AIG for BMC [default = %s]\n", fInitSpecial? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;