diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-19 16:03:15 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-19 16:03:15 +0700 |
| commit | 19ce8396f03df14028219b9d4efd93a852f30219 (patch) | |
| tree | ea9de12b0d6556954f5fc08a3b1c94c31f458b50 /src/base/abci | |
| parent | 397bebf8a55da132304a941968b3c32df8939e6f (diff) | |
| download | abc-19ce8396f03df14028219b9d4efd93a852f30219.tar.gz abc-19ce8396f03df14028219b9d4efd93a852f30219.tar.bz2 abc-19ce8396f03df14028219b9d4efd93a852f30219.zip | |
New abstraction code.
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abc.c | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 8bd9e5ae..5b77f5b0 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28888,7 +28888,7 @@ usage: int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv ) { Saig_ParBmc_t Pars, * pPars = &Pars; - int c, fUseCnf = 1; + int c, fNaiveCnf = 0; Saig_ParBmcSetDefaultParams( pPars ); pPars->nStart = 0; //(pAbc->nFrames >= 0) ? pAbc->nFrames : 0; pPars->nFramesMax = 50; //pPars->nStart + 10; @@ -28954,7 +28954,7 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; break; case 'c': - fUseCnf ^= 1; + fNaiveCnf ^= 1; break; case 'v': pPars->fVerbose ^= 1; @@ -28975,7 +28975,7 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "The network is combinational.\n" ); return 0; } - pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fUseCnf ); + pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fNaiveCnf ); if ( pPars->nStart == 0 ) pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); @@ -28990,7 +28990,7 @@ usage: Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit ); Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax ); Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut ); - Abc_Print( -2, "\t-c : toggle using smarter CNF computation [default = %s]\n", fUseCnf? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle using naive CNF computation [default = %s]\n", fNaiveCnf? "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; |