luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Undoing previous change, which was made by mistake.

This commit is contained in:
Alan Mishchenko 2014-03-31 22:16:47 -07:00
parent 679e38b012
commit 1c56a92a6c
3 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/base/abci/abc.c
View File

@ -21746,7 +21746,7 @@ usage:
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart ); Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-T num : runtime limit, in seconds [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-T num : runtime limit, in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-H num : runtime limit per output, in CLOCKS_PER_SECs (with \"-a\") [default = %d]\n", pPars->nTimeOutOne ); Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne );
Abc_Print( -2, "\t-G num : runtime gap since the last CEX, in seconds [default = %d]\n", pPars->nTimeOutGap ); Abc_Print( -2, "\t-G num : runtime gap since the last CEX, in seconds [default = %d]\n", pPars->nTimeOutGap );
Abc_Print( -2, "\t-C num : max conflicts at an output [default = %d]\n", pPars->nConfLimit ); Abc_Print( -2, "\t-C num : max conflicts at an output [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-D num : max conflicts after jumping (0 = infinity) [default = %d]\n", pPars->nConfLimitJump ); Abc_Print( -2, "\t-D num : max conflicts after jumping (0 = infinity) [default = %d]\n", pPars->nConfLimitJump );
@ -23588,7 +23588,7 @@ usage:
Abc_Print( -2, "\t-C num : limit on conflicts in one SAT call (0 = no limit) [default = %d]\n", pPars->nConfLimit ); Abc_Print( -2, "\t-C num : limit on conflicts in one SAT call (0 = no limit) [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-R num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit ); Abc_Print( -2, "\t-R num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit );
Abc_Print( -2, "\t-T num : runtime limit, in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-T num : runtime limit, in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-H num : runtime limit per output, in CLOCKS_PER_SECs (with \"-a\") [default = %d]\n", pPars->nTimeOutOne ); Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne );
Abc_Print( -2, "\t-G num : runtime gap since the last CEX (0 = no limit) [default = %d]\n", pPars->nTimeOutGap ); Abc_Print( -2, "\t-G num : runtime gap since the last CEX (0 = no limit) [default = %d]\n", pPars->nTimeOutGap );
Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" ); Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" );
Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" ); Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" );

2
src/proof/pdr/pdrMan.c
View File

@ -81,7 +81,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
int i; int i;
p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) ); p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) );
for ( i = 0; i < Saig_ManPoNum(pAig); i++ ) for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
p->pTime4Outs[i] = pPars->nTimeOutOne; p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
} }
if ( pPars->fSolveAll ) if ( pPars->fSolveAll )
{ {

4
src/sat/bmc/bmcBmc3.c
View File

@ -757,7 +757,7 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne )
{ {
p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) ); p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) );
for ( i = 0; i < Saig_ManPoNum(pAig); i++ ) for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
p->pTime4Outs[i] = nTimeOutOne; p->pTime4Outs[i] = nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
} }
return p; return p;
} }
@ -1555,7 +1555,7 @@ clk2 = Abc_Clock();
status = Saig_ManCallSolver( p, Lit ); status = Saig_ManCallSolver( p, Lit );
clkSatRun = Abc_Clock() - clk2; clkSatRun = Abc_Clock() - clk2;
if ( pLogFile ) if ( pLogFile )
fprintf( pLogFile, "Frame %5d Output %5d Time(ms) %8d\n", f, i, Lit < 2 ? 0 : (int)clkSatRun ); fprintf( pLogFile, "Frame %5d Output %5d Time(ms) %8d\n", f, i, Lit < 2 ? 0 : (int)(clkSatRun * 1000 / CLOCKS_PER_SEC) );
if ( p->pTime4Outs ) if ( p->pTime4Outs )
{ {
abctime timeSince = Abc_Clock() - clkOne; abctime timeSince = Abc_Clock() - clkOne;