diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-23 15:34:49 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-23 15:34:49 -0700 |
commit | 637da8baeaabf6f12aa8d9ec287aa675d9ea5fab (patch) | |
tree | 628e631e30dff964ead2df3ceb74000a2b7f9b3f /src/base/abci/abc.c | |
parent | 3712dd30d0e6152e627b487f7f4f5e4e6f6c5afd (diff) | |
download | abc-637da8baeaabf6f12aa8d9ec287aa675d9ea5fab.tar.gz abc-637da8baeaabf6f12aa8d9ec287aa675d9ea5fab.tar.bz2 abc-637da8baeaabf6f12aa8d9ec287aa675d9ea5fab.zip |
Added switch 'satclp -Z' to control the max size of the cone to work with.
Diffstat (limited to 'src/base/abci/abc.c')
-rw-r--r-- | src/base/abci/abc.c | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2a71fd7a..9b62c622 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3104,6 +3104,7 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes; int nCubeLim = 1000; int nBTLimit = 1000000; + int nCostMax = 20000000; int fCanon = 0; int fReverse = 0; int fVerbose = 0; @@ -3111,7 +3112,7 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CLcrvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CLZcrvh" ) ) != EOF ) { switch ( c ) { @@ -3137,6 +3138,17 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nBTLimit < 0 ) goto usage; break; + case 'Z': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-Z\" should be followed by an integer.\n" ); + goto usage; + } + nCostMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nCostMax < 0 ) + goto usage; + break; case 'c': fCanon ^= 1; break; @@ -3167,11 +3179,11 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the new network if ( Abc_NtkIsStrash(pNtk) ) - pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); + pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose ); else { pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 ); - pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); + pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose ); Abc_NtkDelete( pNtk ); } if ( pNtkRes == NULL ) @@ -3184,10 +3196,11 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: satclp [-CL num] [-crvh]\n" ); + Abc_Print( -2, "usage: satclp [-CLZ num] [-crvh]\n" ); Abc_Print( -2, "\t performs SAT based collapsing\n" ); Abc_Print( -2, "\t-C num : the limit on the SOP size of one output [default = %d]\n", nCubeLim ); Abc_Print( -2, "\t-L num : the limit on the number of conflicts in one SAT call [default = %d]\n", nBTLimit ); + Abc_Print( -2, "\t-Z num : the limit on the cost of the largest output [default = %d]\n", nCostMax ); Abc_Print( -2, "\t-c : toggles using canonical ISOP computation [default = %s]\n", fCanon? "yes": "no" ); Abc_Print( -2, "\t-r : toggles using reverse veriable ordering [default = %s]\n", fReverse? "yes": "no" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); |