diff options
Diffstat (limited to 'src/base/abci/abc.c')
| -rw-r--r-- | src/base/abci/abc.c | 30 |
1 files changed, 28 insertions, 2 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 69e8ed84..0ac0b7cf 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -32439,8 +32439,10 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->TimeOutGlo = 30; pPars->TimeOutLoc = 2; pPars->TimeOutInc = 100; + pPars->TimeOutGap = 0; + pPars->TimePerOut = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "TLMsdvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "TLMGHsdvwh" ) ) != EOF ) { switch ( c ) { @@ -32477,6 +32479,28 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->TimeOutInc <= 0 ) goto usage; break; + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + pPars->TimeOutGap = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->TimeOutGap <= 0 ) + goto usage; + break; + case 'H': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-H\" should be followed by an integer.\n" ); + goto usage; + } + pPars->TimePerOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->TimePerOut <= 0 ) + goto usage; + break; case 's': pPars->fUseSyn ^= 1; break; @@ -32507,11 +32531,13 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &mprove [-TLM num] [-sdvwh]\n" ); + Abc_Print( -2, "usage: &mprove [-TLMGH num] [-sdvwh]\n" ); Abc_Print( -2, "\t proves multi-output testcase by applying several engines\n" ); Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", pPars->TimeOutGlo ); Abc_Print( -2, "\t-L num : approximate local runtime limit in seconds [default = %d]\n", pPars->TimeOutLoc ); Abc_Print( -2, "\t-M num : percentage of local runtime limit increase [default = %d]\n", pPars->TimeOutInc ); + Abc_Print( -2, "\t-G num : approximate gap runtime limit in seconds [default = %d]\n", pPars->TimeOutGap ); + Abc_Print( -2, "\t-H num : timeout per output in miliseconds [default = %d]\n", pPars->TimePerOut ); Abc_Print( -2, "\t-s : toggle using combinational synthesis [default = %s]\n", pPars->fUseSyn? "yes": "no" ); Abc_Print( -2, "\t-d : toggle dumping invariant into a file [default = %s]\n", pPars->fDumpFinal? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); |