From bab4c1ddfc3e7bb88d649daed8bd412a98850cf9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 14 Nov 2020 14:23:49 -0800 Subject: Upgrading the SAT solvers. --- src/base/abci/abc.c | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) (limited to 'src/base/abci/abc.c') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b6b3dba5..e7026d74 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -36290,7 +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->jType = 2; // solver type pPars->fSatSweeping = 1; // conflict limit at a node pPars->nWords = 8; // simulation words pPars->nRounds = 10; // simulation rounds @@ -36300,7 +36300,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nCallsRecycle = 500; // calls to perform before recycling SAT solver pPars->nGenIters = 100; // pattern generation iterations Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCPrmdckngxwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxwvh" ) ) != EOF ) { switch ( c ) { @@ -36381,6 +36381,17 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nBTLimit < 0 ) goto usage; break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nCallsRecycle = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nCallsRecycle < 0 ) + goto usage; + break; case 'P': if ( globalUtilOptind >= argc ) { @@ -36443,7 +36454,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &fraig [-JWRILDCP ] [-rmdckngwvh]\n" ); + Abc_Print( -2, "usage: &fraig [-JWRILDCNP ] [-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 ); @@ -36452,6 +36463,7 @@ usage: Abc_Print( -2, "\t-L num : the max number of levels of nodes to consider [default = %d]\n", pPars->nLevelMax ); Abc_Print( -2, "\t-D num : the max number of steps of speculative reduction [default = %d]\n", pPars->nDepthMax ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); + Abc_Print( -2, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle ); Abc_Print( -2, "\t-P num : the number of pattern generation iterations [default = %d]\n", pPars->nGenIters ); Abc_Print( -2, "\t-r : toggle the use of AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" ); Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); -- cgit v1.2.3