diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-04-11 22:12:18 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-04-11 22:12:18 -0700 |
| commit | b1eaf714f2a23eaee74efcafff9a40dd017bb00b (patch) | |
| tree | a3700bc7c5e73b6872f304ebfac4c7708c6ba94c /src/base/abci | |
| parent | 79584f5e201e7388e30df39e6f8fc9b50f34b834 (diff) | |
| download | abc-b1eaf714f2a23eaee74efcafff9a40dd017bb00b.tar.gz abc-b1eaf714f2a23eaee74efcafff9a40dd017bb00b.tar.bz2 abc-b1eaf714f2a23eaee74efcafff9a40dd017bb00b.zip | |
Experiments with SAT sweeping.
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abc.c | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 55e14545..f9f2f2e0 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -12385,7 +12385,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // Cba_PrsReadBlifTest(); } // Abc_NtkComputePaths( Abc_FrameReadNtk(pAbc) ); - Acb_DataReadTest(); +// Acb_DataReadTest(); return 0; usage: Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" ); @@ -32928,7 +32928,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) Cec_ManFraSetDefaultParams( pPars ); pPars->fSatSweeping = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdcnwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdcknwvh" ) ) != EOF ) { switch ( c ) { @@ -33010,6 +33010,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'c': pPars->fRunCSat ^= 1; break; + case 'k': + pPars->fUseCones ^= 1; + break; case 'n': fUseAlgo ^= 1; break; @@ -33036,7 +33039,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdcnwvh]\n" ); + Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdcknwvh]\n" ); Abc_Print( -2, "\t performs combinational SAT sweeping\n" ); Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords ); Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", pPars->nRounds ); @@ -33048,6 +33051,7 @@ usage: Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); Abc_Print( -2, "\t-d : toggle using double output miters [default = %s]\n", pPars->fDualOut? "yes": "no" ); Abc_Print( -2, "\t-c : toggle using circuit-based solver [default = %s]\n", pPars->fRunCSat? "yes": "no" ); + Abc_Print( -2, "\t-k : toggle using logic cones in the SAT solver [default = %s]\n", pPars->fUseCones? "yes": "no" ); Abc_Print( -2, "\t-n : toggle using new implementation [default = %s]\n", fUseAlgo? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); |