diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-16 14:20:52 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-08-16 14:20:52 +0700 |
| commit | 23d36a8d5665d7a586777c9723c4aa803b253fc1 (patch) | |
| tree | 69210b61d5602dac1dccdea7a62756e813adb1c4 /src/base/abci/abcDar.c | |
| parent | d2747fb2815a4fea35a0bf23cb4941d61a1d99fc (diff) | |
| download | abc-23d36a8d5665d7a586777c9723c4aa803b253fc1.tar.gz abc-23d36a8d5665d7a586777c9723c4aa803b253fc1.tar.bz2 abc-23d36a8d5665d7a586777c9723c4aa803b253fc1.zip | |
Integrating Satoko into 'bmc' and 'bmc2'.
Diffstat (limited to 'src/base/abci/abcDar.c')
| -rw-r--r-- | src/base/abci/abcDar.c | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 147f7c2f..996ae6a2 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -2258,7 +2258,7 @@ static void sigfunc( int signo ) SeeAlso [] ***********************************************************************/ -int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fOrDecomp, int nCofFanLit, int fVerbose, int * piFrames ) +int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fOrDecomp, int nCofFanLit, int fVerbose, int * piFrames, int fUseSatoko ) { Aig_Man_t * pMan; Vec_Int_t * vMap = NULL; @@ -2284,7 +2284,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int if ( fNewAlgo ) // command 'bmc' { int iFrame; - RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame, nCofFanLit ); + RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame, nCofFanLit, fUseSatoko ); if ( piFrames ) *piFrames = iFrame; ABC_FREE( pNtk->pModel ); @@ -2309,7 +2309,7 @@ ABC_PRT( "Time", Abc_Clock() - clk ); } else { - RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames, 0 ); + RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames, 0, fUseSatoko ); ABC_FREE( pNtk->pModel ); ABC_FREE( pNtk->pSeqModel ); pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; @@ -2829,7 +2829,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, i if ( pSecPar->fTryBmc ) { - RetValue = Saig_BmcPerform( pMan, 0, nBmcFramesMax, 2000, 0, nBmcConfMax, 0, pSecPar->fVerbose, 0, &iFrame, 0 ); + RetValue = Saig_BmcPerform( pMan, 0, nBmcFramesMax, 2000, 0, nBmcConfMax, 0, pSecPar->fVerbose, 0, &iFrame, 0, 0 ); if ( RetValue == 0 ) { Abc_Print( 1, "Networks are not equivalent.\n" ); |