Skip to content

A
abc
Commit 50095be5 by Alan Mishchenko
Options

Adding runtime limit per output to multi-output DPR (pdr -H <num_sec>).

parent a59968ce
Showing with 117 additions and 22 deletions
src/base/abci/abc.c
......@@ -22641,7 +22641,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, "MFCRTGaxrmsdgvwzh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTGHaxrmsdgvwzh" ) ) != EOF )
{
switch ( c )
{
......@@ -22711,6 +22711,17 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nTimeOutGap < 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->nTimeOutOne = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nTimeOutOne < 0 )
goto usage;
break;
case 'a':
pPars->fSolveAll ^= 1;
break;
......@@ -22773,7 +22784,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: pdr [-MFCRTG <num>] [-axrmsdgvwzh]\n" );
Abc_Print( -2, "usage: pdr [-MFCRTGH <num>] [-axrmsdgvwzh]\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" );
......@@ -22783,6 +22794,7 @@ usage:
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-G num : approximate runtime gap since the last CEX (0 = no limit) [default = %d]\n", pPars->nTimeOutGap );
Abc_Print( -2, "\t-H num : approximate runtime per output (with \"-a\") [default = %d]\n", pPars->nTimeOutOne );
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-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" );
......
src/base/abci/abcDar.c
......@@ -2176,8 +2176,12 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs );
else
Abc_Print( 1, "Some outputs (%d out of %d) are found to be SAT. ",
nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
{
Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
if ( pPars->nDropOuts )
Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
Abc_Print( 1, ". " );
}
if ( pNtk->vSeqModelVec )
Vec_PtrFreeFree( pNtk->vSeqModelVec );
pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
......@@ -2743,22 +2747,15 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
return -1;
}
RetValue = Pdr_ManSolve( pMan, pPars );
pPars->nDropOuts = Saig_ManPoNum(pMan) - pPars->nProveOuts - pPars->nFailOuts;
if ( !pPars->fSilent )
{
if ( RetValue == 1 )
if ( pPars->fSolveAll )
Abc_Print( 1, "Properties: All = %d. Proved = %d. Disproved = %d. Undecided = %d. ",
Saig_ManPoNum(pMan), pPars->nProveOuts, pPars->nFailOuts, pPars->nDropOuts );
else if ( RetValue == 1 )
Abc_Print( 1, "Property proved. " );
else if ( pPars->fSolveAll )
{
int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
Abc_Print( 1, "None of the %d outputs is found to be SAT. ", nOutputs );
else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs );
else
Abc_Print( 1, "Some outputs (%d out of %d) are found to be SAT. ",
nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
}
else
else
{
if ( RetValue == 0 )
{
......@@ -2777,6 +2774,22 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
assert( 0 );
}
ABC_PRT( "Time", clock() - clk );
/*
Abc_Print( 1, "Status: " );
if ( pPars->pOutMap )
{
int i;
for ( i = 0; i < Saig_ManPoNum(pMan); i++ )
if ( pPars->pOutMap[i] == 1 )
Abc_Print( 1, "%d=%s ", i, "unsat" );
else if ( pPars->pOutMap[i] == 0 )
Abc_Print( 1, "%d=%s ", i, "sat" );
else if ( pPars->pOutMap[i] < 0 )
Abc_Print( 1, "%d=%s ", i, "undec" );
else assert( 0 );
}
Abc_Print( 1, "\n" );
*/
}
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel;
......
src/proof/pdr/pdr.h
......@@ -47,6 +47,7 @@ struct Pdr_Par_t_
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 nTimeOutOne; // approximate timeout in seconds per one output
int fTwoRounds; // use two rounds for generalization
int fMonoCnf; // monolythic CNF
int fDumpInv; // dump inductive invariant
......@@ -59,11 +60,14 @@ struct Pdr_Par_t_
int fSolveAll; // do not stop when found a SAT output
int fStoreCex; // enable storing counter-examples in MO mode
int nFailOuts; // the number of failed outputs
int nDropOuts; // the number of timed out outputs
int nProveOuts; // the number of proved outputs
int iFrame; // explored up to this frame
int RunId; // PDR id in this run
int(*pFuncStop)(int); // callback to terminate
int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
clock_t timeLastSolved; // the time when the last output was solved
int * pOutMap; // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided)
};
////////////////////////////////////////////////////////////////////////
......
src/proof/pdr/pdrCore.c
......@@ -60,6 +60,8 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
pPars->fVeryVerbose = 0; // very verbose output
pPars->fNotVerbose = 0; // not printing line-by-line progress
pPars->iFrame = -1; // explored up to this frame
pPars->nFailOuts = 0; // the number of disproved outputs
pPars->nDropOuts = 0; // the number of timed out outputs
pPars->timeLastSolved = 0; // last one solved
}
......@@ -536,6 +538,8 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
return -1;
if ( p->timeToStop && clock() > p->timeToStop )
return -1;
if ( p->timeToStopOne && clock() > p->timeToStopOne )
return -1;
}
return 1;
}
......@@ -558,7 +562,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Aig_Obj_t * pObj;
int k, RetValue = -1;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
clock_t clkStart = clock();
clock_t clkStart = clock(), clkOne = 0;
p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
assert( Vec_PtrSize(p->vSolvers) == 0 );
// create the first timeframe
......@@ -570,9 +574,12 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
assert( k == Vec_PtrSize(p->vSolvers)-1 );
Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
{
// skip solved outputs
// skip disproved outputs
if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) )
continue;
// skip output whose time has run out
if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 )
continue;
// check if the output is trivially solved
if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
continue;
......@@ -585,6 +592,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
return 0; // SAT
}
p->pPars->nFailOuts++;
if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = 0;
Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",
nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
if ( p->vCexes == NULL )
......@@ -600,12 +608,18 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->pPars->iFrame = k;
return -1;
}
if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
return 0; // all SAT
if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) )
return p->pPars->nFailOuts ? 0 : -1; // SAT or UNDEC
p->pPars->timeLastSolved = clock();
continue;
}
// try to solve this output
if ( p->pTime4Outs )
{
assert( p->pTime4Outs[p->iOutCur] > 0 );
clkOne = clock();
p->timeToStopOne = p->pTime4Outs[p->iOutCur] + clock();
}
while ( 1 )
{
if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
......@@ -642,6 +656,12 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
else if ( p->timeToStop && clock() > p->timeToStop )
Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
else if ( p->timeToStopOne && clock() > p->timeToStopOne )
{
Pdr_QueueClean( p );
pCube = NULL;
break; // keep solving
}
else if ( p->pPars->fVerbose )
Abc_Print( 1, "Computation cancelled by the callback.\n" );
p->pPars->iFrame = k;
......@@ -664,6 +684,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
return 0; // SAT
}
p->pPars->nFailOuts++;
if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = 0;
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
......@@ -690,6 +711,18 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Pdr_ManPrintProgress( p, 0, clock() - clkStart );
}
}
if ( p->pTime4Outs )
{
clock_t timeSince = clock() - clkOne;
assert( p->pTime4Outs[p->iOutCur] > 0 );
p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0;
if ( p->pTime4Outs[p->iOutCur] == 0 && p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL )
{
p->pPars->nDropOuts++;
if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = -1;
// printf( "Dropping output %d.\n", p->iOutCur );
}
}
}
if ( p->pPars->fVerbose )
......@@ -729,6 +762,13 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( !p->pPars->fSilent )
Pdr_ManVerifyInvariant( p );
p->pPars->iFrame = k;
// count the number of UNSAT outputs
p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts;
// convert previously 'unknown' into 'unsat'
if ( p->pPars->pOutMap )
for ( k = 0; k < Saig_ManPoNum(p->pAig); k++ )
if ( p->pPars->pOutMap[k] == -2 ) // unknown
p->pPars->pOutMap[k] = 1; // unsat
return p->vCexes ? 0 : 1; // UNSAT
}
if ( p->pPars->fVerbose )
......@@ -798,6 +838,10 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
Pdr_Man_t * p;
int RetValue;
clock_t clk = clock();
if ( pPars->nTimeOutOne )
pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig);
if ( pPars->nTimeOutOne && !pPars->fSolveAll )
pPars->nTimeOutOne = 0;
if ( pPars->fVerbose )
{
// Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
......
src/proof/pdr/pdrInt.h
......@@ -97,6 +97,7 @@ struct Pdr_Man_t_
Vec_Int_t * vRes; // final result
Vec_Int_t * vSuppLits; // support literals
Pdr_Set_t * pCubeJust; // justification
clock_t * pTime4Outs;// timeout per output
// statistics
int nBlocks; // the number of times blockState was called
int nObligs; // the number of proof obligations derived
......@@ -115,6 +116,7 @@ struct Pdr_Man_t_
int nQueLim;
// runtime
time_t timeToStop;
time_t timeToStopOne;
// time stats
clock_t tSat;
clock_t tSatSat;
......
src/proof/pdr/pdrInv.c
......@@ -83,6 +83,8 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, clock_t Time )
Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC );
if ( p->pPars->fSolveAll )
Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts );
if ( p->pPars->nTimeOutOne )
Abc_Print( 1, " T/O =%3d", p->pPars->nDropOuts );
Abc_Print( 1, "%s", fClose ? "\n":"\r" );
if ( fClose )
p->nQueMax = 0;
......
src/proof/pdr/pdrMan.c
......@@ -73,6 +73,21 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
Aig_ManFanoutStart( pAig );
if ( pAig->pTerSimData == NULL )
pAig->pTerSimData = ABC_CALLOC( unsigned, 1 + (Aig_ManObjNumMax(pAig) / 16) );
// time spent on each outputs
if ( pPars->nTimeOutOne )
{
int i;
p->pTime4Outs = ABC_ALLOC( clock_t, Saig_ManPoNum(pAig) );
for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC;
}
if ( pPars->fSolveAll )
{
int i;
pPars->pOutMap = ABC_ALLOC( int, Saig_ManPoNum(pAig) );
for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
pPars->pOutMap[i] = -2; // unknown
}
return p;
}
......@@ -144,6 +159,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
Vec_IntFree( p->vRes ); // final result
Vec_IntFree( p->vSuppLits ); // support literals
ABC_FREE( p->pCubeJust );
ABC_FREE( p->pTime4Outs );
if ( p->vCexes )
Vec_PtrFreeFree( p->vCexes );
// additional AIG data-members
......
src/sat/bmc/bmcBmc3.c
......@@ -1393,10 +1393,12 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
int i, f, k, Lit, status;
clock_t clk, clk2, clkOther = 0, clkTotal = clock();
clock_t nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne;
clock_t nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne = 0;
clock_t nTimeToStopNG, nTimeToStop;
if ( pPars->nTimeOutOne )
pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig);
if ( pPars->nTimeOutOne && !pPars->fSolveAll )
pPars->nTimeOutOne = 0;
nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
// create BMC manager
......
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