Skip to content

A
abc
Commit baa944e6 by Alan Mishchenko
Options

Added 'gap timeout' to pdr.

parent 4dc7eb6f
Showing with 61 additions and 43 deletions
src/base/abci/abc.c
......@@ -22404,23 +22404,10 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Pdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTarmsdgvwzh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTGarmsdgvwzh" ) ) != EOF )
{
switch ( c )
{
/*
case 'O':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
goto usage;
}
pPars->iOutput = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->iOutput < 0 )
goto usage;
break;
*/
case 'M':
if ( globalUtilOptind >= argc )
{
......@@ -22476,6 +22463,17 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nTimeOut < 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->nTimeOutGap = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nTimeOutGap < 0 )
goto usage;
break;
case 'a':
pPars->fSolveAll ^= 1;
break;
......@@ -22535,25 +22533,25 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: pdr [-MFCRT<num] [-armsdgvwzh]\n" );
Abc_Print( -2, "usage: pdr [-MFCRTG <num>] [-armsdgvwzh]\n" );
Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" );
Abc_Print( -2, "\t pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" );
Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" );
// Abc_Print( -2, "\t-O num : the zero-based number of the primary output to solve [default = all]\n" );
Abc_Print( -2, "\t-M num : limit on unused vars to trigger SAT solver recycling [default = %d]\n", pPars->nRecycle );
Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n", pPars->nFrameMax );
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-M num : limit on unused vars to trigger SAT solver recycling [default = %d]\n", pPars->nRecycle );
Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n", pPars->nFrameMax );
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-T num : approximate timeout in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut );
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-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" );
Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" );
Abc_Print( -2, "\t-s : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping inductive invariant [default = %s]\n", pPars->fDumpInv? "yes": "no" );
Abc_Print( -2, "\t-g : toggle skipping expensive generalization step [default = %s]\n", pPars->fSkipGeneral? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing detailed stats default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" );
Abc_Print( -2, "\t-T num : approximate timeout in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-G num : approximate 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-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" );
Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" );
Abc_Print( -2, "\t-s : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping inductive invariant [default = %s]\n", pPars->fDumpInv? "yes": "no" );
Abc_Print( -2, "\t-g : toggle skipping expensive generalization step [default = %s]\n", pPars->fSkipGeneral? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing detailed stats default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
......
src/proof/pdr/pdr.h
......@@ -46,6 +46,7 @@ struct Pdr_Par_t_
int nConfLimit; // limit on SAT solver conflicts
int nRestLimit; // limit on the number of proof-obligations
int nTimeOut; // timeout in seconds
int nTimeOutGap; // approximate timeout in seconds since the last change
int fTwoRounds; // use two rounds for generalization
int fMonoCnf; // monolythic CNF
int fDumpInv; // dump inductive invariant
......@@ -60,6 +61,7 @@ struct Pdr_Par_t_
int iFrame; // explored up to this frame
int RunId; // PDR id in this run
int(*pFuncStop)(int); // callback to terminate
clock_t timeLastSolved; // the time when the last output was solved
};
////////////////////////////////////////////////////////////////////////
......
src/proof/pdr/pdrCore.c
......@@ -45,20 +45,22 @@ ABC_NAMESPACE_IMPL_START
void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
{
memset( pPars, 0, sizeof(Pdr_Par_t) );
// pPars->iOutput = -1; // zero-based output number
pPars->nRecycle = 300; // limit on vars for recycling
pPars->nFrameMax = 10000; // limit on number of timeframes
pPars->nTimeOut = 0; // timeout in seconds
pPars->nConfLimit = 0; // limit on SAT solver conflicts
pPars->nRestLimit = 0; // limit on the number of proof-obligations
pPars->fTwoRounds = 0; // use two rounds for generalization
pPars->fMonoCnf = 0; // monolythic CNF
pPars->fDumpInv = 0; // dump inductive invariant
pPars->fShortest = 0; // forces bug traces to be shortest
pPars->fVerbose = 0; // verbose output
pPars->fVeryVerbose = 0; // very verbose output
pPars->fNotVerbose = 0; // not printing line-by-line progress
pPars->iFrame = -1; // explored up to this frame
// pPars->iOutput = -1; // zero-based output number
pPars->nRecycle = 300; // limit on vars for recycling
pPars->nFrameMax = 10000; // limit on number of timeframes
pPars->nTimeOut = 0; // timeout in seconds
pPars->nTimeOutGap = 0; // timeout in seconds since the last solved
pPars->nConfLimit = 0; // limit on SAT solver conflicts
pPars->nRestLimit = 0; // limit on the number of proof-obligations
pPars->fTwoRounds = 0; // use two rounds for generalization
pPars->fMonoCnf = 0; // monolythic CNF
pPars->fDumpInv = 0; // dump inductive invariant
pPars->fShortest = 0; // forces bug traces to be shortest
pPars->fVerbose = 0; // verbose output
pPars->fVeryVerbose = 0; // very verbose output
pPars->fNotVerbose = 0; // not printing line-by-line progress
pPars->iFrame = -1; // explored up to this frame
pPars->timeLastSolved = 0; // last one solved
}
/**Function*************************************************************
......@@ -560,6 +562,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
assert( Vec_PtrSize(p->vSolvers) == 0 );
// create the first timeframe
p->pPars->timeLastSolved = clock();
Pdr_ManCreateSolver( p, (k = 0) );
while ( 1 )
{
......@@ -590,6 +593,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, Pdr_ManDeriveCex(p) );
if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
return 0; // all SAT
p->pPars->timeLastSolved = clock();
continue;
}
// try to solve this output
......@@ -723,6 +727,20 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->pPars->iFrame = k;
return p->vCexes ? 0 : -1;
}
if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
{
if ( fPrintClauses )
{
Abc_Print( 1, "*** Clauses after frame %d:\n", k );
Pdr_ManPrintClauses( p, 0 );
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
if ( !p->pPars->fSilent )
Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOut );
p->pPars->iFrame = k;
return p->vCexes ? 0 : -1;
}
if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax )
{
if ( p->pPars->fVerbose )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment