Skip to content

A
abc
Commit 77b5dc26 by Alan Mishchenko
Options

Added restarts to PDR.

parent e0650dce
Showing with 53 additions and 21 deletions
src/base/abci/abc.c
......@@ -20783,7 +20783,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Pdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "OMFCTrmsdgvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "OMFCRTrmsdgvwh" ) ) != EOF )
{
switch ( c )
{
......@@ -20831,6 +20831,17 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nConfLimit < 0 )
goto usage;
break;
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
pPars->nRestLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nRestLimit < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
......@@ -20904,14 +20915,15 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: pdr [-OMFCT<num] [-rmsdgvwh]\n" );
Abc_Print( -2, "\t model checking using property directed reachability (aka ic3)\n" );
Abc_Print( -2, "usage: pdr [-OMFCRT<num] [-rmsdgvwh]\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 : number of unused vars to trigger SAT solver recycling [default = %d]\n", pPars->nRecycle );
Abc_Print( -2, "\t-F num : number of timeframes explored to stop computation [default = %d]\n", pPars->nFrameMax );
Abc_Print( -2, "\t-C num : number of conflicts in a 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-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" );
......
src/proof/pdr/pdr.h
......@@ -44,6 +44,7 @@ struct Pdr_Par_t_
int nRecycle; // limit on vars for recycling
int nFrameMax; // limit on frame count
int nConfLimit; // limit on SAT solver conflicts
int nRestLimit; // limit on the number of proof-obligations
int nTimeOut; // timeout in seconds
int fTwoRounds; // use two rounds for generalization
int fMonoCnf; // monolythic CNF
......
src/proof/pdr/pdrCore.c
......@@ -50,6 +50,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
pPars->nFrameMax = 5000; // limit on number of timeframes
pPars->nTimeOut = 0; // timeout in seconds
pPars->nConfLimit = 100000; // 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
......@@ -429,6 +430,12 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
pThis = Pdr_QueueHead( p );
if ( pThis->iFrame == 0 )
return 0; // SAT
if ( p->nQueLim && p->nQueCur >= p->nQueLim )
{
p->nQueLim = p->nQueLim * 11 / 10;
Pdr_QueueStop( p );
return 1; // restart
}
pThis = Pdr_QueuePop( p );
assert( pThis->iFrame > 0 );
assert( !Pdr_SetIsInit(pThis->pState, -1) );
......@@ -584,12 +591,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->pPars->iFrame = k;
return 0; // SAT
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 0, clock() - clkStart );
}
else
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
// open a new timeframe
p->nQueLim = p->pPars->nRestLimit;
assert( pCube == NULL );
Pdr_ManSetPropertyOutput( p, k );
Pdr_ManCreateSolver( p, ++k );
......@@ -619,7 +629,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 0, clock() - clkStart );
clkStart = clock();
// clkStart = clock();
}
// check the timeout
......@@ -696,6 +706,14 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit,
***********************************************************************/
int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
{
// printf( "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
printf( "VarMax = %d. FrameMax = %d. QueueMax = %d. TimeMax = %d. ",
pPars->nRecycle, pPars->nFrameMax, pPars->nRestLimit, pPars->nTimeOut );
if ( pPars->iOutput >= 0 )
printf( "Output = %d. ", pPars->iOutput );
printf( "MonoCNF = %s. SkipGen = %s.\n",
pPars->fMonoCnf ? "yes" : "no", pPars->fSkipGeneral ? "yes" : "no" );
/*
Vec_Int_t * vPrioInit = NULL;
int RetValue, nTimeOut;
......
src/proof/pdr/pdrInt.h
......@@ -107,6 +107,9 @@ struct Pdr_Man_t_
int nCasesSU;
int nCasesUS;
int nCasesUU;
int nQueCur;
int nQueMax;
int nQueLim;
// runtime
int timeStart;
int timeToStop;
......
src/proof/pdr/pdrInv.c
......@@ -46,7 +46,6 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
{
static int PastSize;
Vec_Ptr_t * vVec;
int i, ThisSize, Length, LengthStart;
if ( Vec_PtrSize(p->vSolvers) < 2 )
......@@ -56,9 +55,9 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
Vec_VecForEachLevel( p->vClauses, vVec, i )
Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
// determine the starting point
LengthStart = Abc_MaxInt( 0, Length - 70 );
LengthStart = Abc_MaxInt( 0, Length - 60 );
printf( "%3d :", Vec_PtrSize(p->vSolvers)-1 );
ThisSize = 6;
ThisSize = 5;
if ( LengthStart > 0 )
{
printf( " ..." );
......@@ -76,18 +75,13 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
ThisSize += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
}
for ( i = ThisSize; i < 70; i++ )
printf( " " );
printf( "%6d", p->nQueMax );
printf(" %8.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC));
printf("%s", fClose ? "\n":"\r" );
if ( fClose )
{
for ( i = 0; i < PastSize - ThisSize; i++ )
printf( " " );
printf( "\n" );
}
else
{
printf( "\r" );
PastSize = ThisSize;
}
// printf(" %.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC));
p->nQueMax = 0;
}
/**Function*************************************************************
......
src/proof/pdr/pdrUtil.c
......@@ -500,6 +500,7 @@ Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p )
return NULL;
p->pQueue = p->pQueue->pLink;
Pdr_OblDeref( pRes );
p->nQueCur--;
return pRes;
}
......@@ -518,6 +519,8 @@ void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl )
{
Pdr_Obl_t * pTemp, ** ppPrev;
p->nObligs++;
p->nQueCur++;
p->nQueMax = Abc_MaxInt( p->nQueMax, p->nQueCur );
Pdr_OblRef( pObl );
if ( p->pQueue == NULL )
{
......@@ -569,6 +572,7 @@ void Pdr_QueueStop( Pdr_Man_t * p )
Pdr_OblDeref( pObl );
}
p->pQueue = NULL;
p->nQueCur = 0;
}
......
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