From 50095be5ac2c1b9830a74c87fd0d8e2edc8b8438 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 3 May 2013 19:58:25 -0700 Subject: Adding runtime limit per output to multi-output DPR (pdr -H ). --- src/base/abci/abc.c | 16 +++++++++++++-- src/base/abci/abcDar.c | 43 ++++++++++++++++++++++++++-------------- src/proof/pdr/pdr.h | 4 ++++ src/proof/pdr/pdrCore.c | 52 +++++++++++++++++++++++++++++++++++++++++++++---- src/proof/pdr/pdrInt.h | 2 ++ src/proof/pdr/pdrInv.c | 2 ++ src/proof/pdr/pdrMan.c | 16 +++++++++++++++ src/sat/bmc/bmcBmc3.c | 4 +++- 8 files changed, 117 insertions(+), 22 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 90d6b454..c19faa52 100644 --- a/src/base/abci/abc.c +++ b/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 ] [-axrmsdgvwzh]\n" ); + Abc_Print( -2, "usage: pdr [-MFCRTGH ] [-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" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index abf08599..c351df45 100644 --- a/src/base/abci/abcDar.c +++ b/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; diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index cfb13356..97a71512 100644 --- a/src/proof/pdr/pdr.h +++ b/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) }; //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 3df1d7de..43cc4527 100644 --- a/src/proof/pdr/pdrCore.c +++ b/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" ); diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index f6d3d170..03d522d3 100644 --- a/src/proof/pdr/pdrInt.h +++ b/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; diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index ee87f262..bb8d110d 100644 --- a/src/proof/pdr/pdrInv.c +++ b/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; diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index 95e7641b..51be5e17 100644 --- a/src/proof/pdr/pdrMan.c +++ b/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 diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 96fff2af..424e08c9 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/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 -- cgit v1.2.3