diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-04 22:30:27 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-04 22:30:27 -0800 |
| commit | a1d2ba0fcc4748e6b6181c74d684c5d06d8209f1 (patch) | |
| tree | 41cb2ed2db32d0f5643b45c2dbc5e6d4a5a79f27 /src/base/abci | |
| parent | 0ab8cd1191bfecefdbd62738d5b15af53979fd2a (diff) | |
| download | abc-a1d2ba0fcc4748e6b6181c74d684c5d06d8209f1.tar.gz abc-a1d2ba0fcc4748e6b6181c74d684c5d06d8209f1.tar.bz2 abc-a1d2ba0fcc4748e6b6181c74d684c5d06d8209f1.zip | |
Tuning for multi-ouptut solver.
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abc.c | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 69e8ed84..d94adf08 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -32439,8 +32439,9 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->TimeOutGlo = 30; pPars->TimeOutLoc = 2; pPars->TimeOutInc = 100; + pPars->TimePerOut = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "TLMsdvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "TLMHsdvwh" ) ) != EOF ) { switch ( c ) { @@ -32477,6 +32478,17 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->TimeOutInc <= 0 ) goto usage; break; + case 'H': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" 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; @@ -32512,6 +32524,7 @@ usage: 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-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" ); |