diff options
Diffstat (limited to 'src/base/abci/abc.c')
| -rw-r--r-- | src/base/abci/abc.c | 22 |
1 files changed, 17 insertions, 5 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7058de3e..a2db62a1 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -32876,13 +32876,24 @@ usage: ***********************************************************************/ int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, int fVerbose ); - int c, nTimeOut = 1, nIterMax = 0, LookAhead = 1, fVerbose = 0; + extern Gia_Man_t * Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose ); + int c, nProcs = 1, nTimeOut = 1, nIterMax = 0, LookAhead = 1, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "TILvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PTILvh" ) ) != EOF ) { switch ( c ) { + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by a positive integer.\n" ); + goto usage; + } + nProcs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nProcs <= 0 ) + goto usage; + break; case 'T': if ( globalUtilOptind >= argc ) { @@ -32938,12 +32949,13 @@ int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9SplitProve(): The problem is sequential.\n" ); return 1; } - Cec_GiaSplitTest( pAbc->pGia, nTimeOut, nIterMax, LookAhead, fVerbose ); + Cec_GiaSplitTest( pAbc->pGia, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: &splitprove [-TIL num] [-vh]\n" ); + Abc_Print( -2, "usage: &splitprove [-PTIL num] [-vh]\n" ); Abc_Print( -2, "\t proves CEC problem by case-splitting\n" ); + Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", nProcs ); Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut ); Abc_Print( -2, "\t-I num : the max number of iterations (0 = infinity) [default = %d]\n", nIterMax ); Abc_Print( -2, "\t-L num : maximum look-ahead during cofactoring [default = %d]\n", LookAhead ); |