diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-13 10:29:31 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-13 10:29:31 -0800 |
commit | 22388f901a88dddfe629dd3c1406b06fafa9675d (patch) | |
tree | 8e99ba4a2e90fd84468738af7ef26dd971f67848 /src/base/abci/abc.c | |
parent | 38d72c43435f70eb8703dc922f3c0630132bffcc (diff) | |
download | abc-22388f901a88dddfe629dd3c1406b06fafa9675d.tar.gz abc-22388f901a88dddfe629dd3c1406b06fafa9675d.tar.bz2 abc-22388f901a88dddfe629dd3c1406b06fafa9675d.zip |
Adding and integrating new SAT solver APIs.
Diffstat (limited to 'src/base/abci/abc.c')
-rw-r--r-- | src/base/abci/abc.c | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2ed1f5ef..8277a0b3 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -36290,6 +36290,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp; int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoG2 = 0; Cec_ManFraSetDefaultParams( pPars ); + pPars->jType = 0; // solver type pPars->fSatSweeping = 1; // conflict limit at a node pPars->nWords = 4; // simulation words pPars->nRounds = 250; // simulation rounds @@ -36299,10 +36300,21 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nCallsRecycle = 500; // calls to perform before recycling SAT solver pPars->nGenIters = 5; // pattern generation iterations Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCPrmdckngxwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCPrmdckngxwvh" ) ) != EOF ) { switch ( c ) { + case 'J': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" ); + goto usage; + } + pPars->jType = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->jType < 0 ) + goto usage; + break; case 'W': if ( globalUtilOptind >= argc ) { @@ -36431,8 +36443,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &fraig [-WRILDCP <num>] [-rmdckngwvh]\n" ); + Abc_Print( -2, "usage: &fraig [-JWRILDCP <num>] [-rmdckngwvh]\n" ); Abc_Print( -2, "\t performs combinational SAT sweeping\n" ); + Abc_Print( -2, "\t-J num : the solver type [default = %d]\n", pPars->jType ); 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 ); Abc_Print( -2, "\t-I num : the number of sweeping iterations [default = %d]\n", pPars->nItersMax ); |