diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2006-04-07 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2006-04-07 08:01:00 -0700 |
| commit | 3f4fc5e4507f7fb9df431fc116529b4c209ab97c (patch) | |
| tree | d468f472a10aa98499f98c639447b7838e495476 /src/base/abci/abcVerify.c | |
| parent | 8e5398c501a873dffcb562a11bc19e630872c931 (diff) | |
| download | abc-3f4fc5e4507f7fb9df431fc116529b4c209ab97c.tar.gz abc-3f4fc5e4507f7fb9df431fc116529b4c209ab97c.tar.bz2 abc-3f4fc5e4507f7fb9df431fc116529b4c209ab97c.zip | |
Version abc60407
Diffstat (limited to 'src/base/abci/abcVerify.c')
| -rw-r--r-- | src/base/abci/abcVerify.c | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 5456693b..e0c65058 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -85,7 +85,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI } // solve the CNF using the SAT solver - RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0 ); + RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0, 0 ); if ( RetValue == -1 ) printf( "Networks are undecided (SAT solver timed out).\n" ); else if ( RetValue == 0 ) @@ -112,6 +112,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI ***********************************************************************/ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose ) { + Prove_Params_t Params, * pParams = &Params; // Fraig_Params_t Params; // Fraig_Man_t * pMan; Abc_Ntk_t * pMiter; @@ -171,7 +172,9 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV Abc_NtkDelete( pMiter ); */ // solve the CNF using the SAT solver - RetValue = Abc_NtkMiterProve( &pMiter, 0, 0, 1, 1, 0 ); + Prove_ParamsSetDefault( pParams ); + pParams->nItersMax = 5; + RetValue = Abc_NtkMiterProve( &pMiter, pParams ); if ( RetValue == -1 ) printf( "Networks are undecided (resource limits is reached).\n" ); else if ( RetValue == 0 ) @@ -254,7 +257,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI } // solve the CNF using the SAT solver - RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0 ); + RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0, 0 ); if ( RetValue == -1 ) printf( "Networks are undecided (SAT solver timed out).\n" ); else if ( RetValue == 0 ) |