diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-09 13:24:07 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-09 13:24:07 -0800 |
| commit | 40bfe2fb88b4a4dc32fa280e66f66dcefb4a4b1d (patch) | |
| tree | 7d6e9b334e56967c5867e8d90e4f126a5fb914a1 /src/base/abci | |
| parent | 0b89fd387e71aeaf9595190eac2326a796ff6fc6 (diff) | |
| download | abc-40bfe2fb88b4a4dc32fa280e66f66dcefb4a4b1d.tar.gz abc-40bfe2fb88b4a4dc32fa280e66f66dcefb4a4b1d.tar.bz2 abc-40bfe2fb88b4a4dc32fa280e66f66dcefb4a4b1d.zip | |
Experiments with SAT sweeping.
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abc.c | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1f21d931..408c2266 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -36286,14 +36286,15 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Gia_Man_t * Cec2_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); extern Gia_Man_t * Cec3_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); + extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp; - int c, fUseAlgo = 0, fUseAlgoG = 0; + int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoG2 = 0; Cec_ManFraSetDefaultParams( pPars ); pPars->fSatSweeping = 1; pPars->nItersMax = 1000000; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdckngwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdckngxwvh" ) ) != EOF ) { switch ( c ) { @@ -36384,6 +36385,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'g': fUseAlgoG ^= 1; break; + case 'x': + fUseAlgoG2 ^= 1; + break; case 'w': pPars->fVeryVerbose ^= 1; break; @@ -36403,6 +36407,8 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pTemp = Cec2_ManSimulateTest( pAbc->pGia, pPars ); else if ( fUseAlgoG ) pTemp = Cec3_ManSimulateTest( pAbc->pGia, pPars ); + else if ( fUseAlgoG2 ) + pTemp = Cec4_ManSimulateTest( pAbc->pGia, pPars ); else pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars, 0 ); Abc_FrameUpdateGia( pAbc, pTemp ); |