From 13f52980dae9821b3d7bec9ff6a0fa4e544607d7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 18 Jul 2008 08:01:00 -0700 Subject: Version abc80718 --- src/base/abci/abc.c | 28 ++++++++++++++++++++++++---- src/base/abci/abcDar.c | 4 ++-- src/base/main/main.c | 8 ++------ 3 files changed, 28 insertions(+), 12 deletions(-) (limited to 'src/base') 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,10 +254,8 @@ 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(); -- cgit v1.2.3