Version abc80718

3 files changed, 28 insertions, 12 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d1aa2c82..cb3d2d86 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -15343,12 +15343,14 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
     int nBTLimit;
+    int nFramesMax;
     int fRewrite;
     int fTransLoop;
     int fUsePudlak;
+    int fCheckInd;
     int fVerbose;
 
-    extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose );
+    extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -15356,12 +15358,14 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nBTLimit   = 20000;
+    nFramesMax = 40;
     fRewrite   = 0;
     fTransLoop = 1;
     fUsePudlak = 0;
+    fCheckInd  = 0;
     fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Crtpvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpivh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -15376,6 +15380,17 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nBTLimit < 0 ) 
                 goto usage;
             break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFramesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFramesMax < 0 ) 
+                goto usage;
+            break;
         case 'r':
             fRewrite ^= 1;
             break;
@@ -15385,6 +15400,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             fUsePudlak ^= 1;
             break;
+        case 'i':
+            fCheckInd ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -15414,16 +15432,18 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
         return 0;
     }
-    Abc_NtkDarBmcInter( pNtk, nBTLimit, fRewrite, fTransLoop, fUsePudlak, fVerbose );
+    Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: int [-C num] [-rtpvh]\n" );
+    fprintf( pErr, "usage: int [-CF num] [-rtpivh]\n" );
     fprintf( pErr, "\t         uses interpolation to prove the property\n" );
     fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit );
+    fprintf( pErr, "\t-F num : the limit on number of frames to unroll [default = %d]\n", nFramesMax );
     fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
     fprintf( pErr, "\t-t     : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" );
     fprintf( pErr, "\t-p     : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" );
+    fprintf( pErr, "\t-i     : toggle inductive containment checking [default = %s]\n", fCheckInd? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index a691a205..e47582e9 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1270,7 +1270,7 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose )
+int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose )
 {
     Aig_Man_t * pMan;
     int RetValue, Depth, clk = clock();
@@ -1282,7 +1282,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTra
         return -1;
     }
     assert( pMan->nRegs > 0 );
-    RetValue = Saig_Interpolate( pMan, nConfLimit, fRewrite, fTransLoop, fUsePudlak, fVerbose, &Depth );
+    RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fVerbose, &Depth );
     if ( RetValue == 1 )
         printf( "Property proved.  " );
     else if ( RetValue == 0 )
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 6f2e1d11..bfa91ddc 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -55,11 +55,9 @@ int main( int argc, char * argv[] )
     bool fBatch, fInitSource, fInitRead, fFinalWrite;
 
     // added to detect memory leaks:
-#ifdef _DEBUG
-#ifdef ABC_CHECK_LEAKS
+#if defined(_DEBUG) && defined(_MSC_VER) && (_MSC_VER <= 1200) // 1200 = MSVC 6.0
     _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
 #endif
-#endif
     
 //    Npn_Experiment();
 //    Npn_Generate();
@@ -256,11 +254,9 @@ void Abc_Start()
 {
     Abc_Frame_t * pAbc;
     // added to detect memory leaks:
-#ifdef _DEBUG
-#ifdef ABC_CHECK_LEAKS
+#if defined(_DEBUG) && defined(_MSC_VER) && (_MSC_VER <= 1200) // 1200 = MSVC 6.0
     _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
 #endif
-#endif
     // start the glocal frame
     pAbc = Abc_FrameGetGlobalFrame();
     // source the resource file