diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-09 16:26:28 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-09 16:26:28 -0700 |
commit | 4876f1e21cd395e94435aaafeaeec05839a32181 (patch) | |
tree | 07dc3c5b9416cfae41599b5affcfee8c4dd208bc /src | |
parent | f1cd8797861e5a47d1f7cc9de0616bbc2d532f43 (diff) | |
download | abc-4876f1e21cd395e94435aaafeaeec05839a32181.tar.gz abc-4876f1e21cd395e94435aaafeaeec05839a32181.tar.bz2 abc-4876f1e21cd395e94435aaafeaeec05839a32181.zip |
Added switch '-x' to save CEXes in 'bmc3' and 'pdr' in multi-output mode.
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abc.c | 18 | ||||
-rw-r--r-- | src/proof/pdr/pdr.h | 1 | ||||
-rw-r--r-- | src/proof/pdr/pdrCore.c | 8 | ||||
-rw-r--r-- | src/sat/bmc/bmc.h | 1 | ||||
-rw-r--r-- | src/sat/bmc/bmcBmc3.c | 46 |
5 files changed, 51 insertions, 23 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7f8a6e8c..48bcce4d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -21010,7 +21010,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Saig_ParBmcSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFTGCDJILadruvzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFTGCDJILaxdruvzh" ) ) != EOF ) { switch ( c ) { @@ -21114,6 +21114,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': pPars->fSolveAll ^= 1; break; + case 'x': + pPars->fStoreCex ^= 1; + break; case 'd': pPars->fDropSatOuts ^= 1; break; @@ -21185,7 +21188,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: bmc3 [-SFTGCDJI num] [-L file] [-aduvzh]\n" ); + Abc_Print( -2, "usage: bmc3 [-SFTGCDJI num] [-L file] [-axduvzh]\n" ); Abc_Print( -2, "\t performs bounded model checking with dynamic unrolling\n" ); 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 ); @@ -21197,6 +21200,7 @@ usage: Abc_Print( -2, "\t-I num : the number of PIs to abstract [default = %d]\n", pPars->nPisAbstract ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); Abc_Print( -2, "\t-a : solve all outputs (do not stop when one 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-d : toggle dropping (replacing by 0) SAT outputs [default = %s]\n", pPars->fDropSatOuts? "yes": "no" ); Abc_Print( -2, "\t-u : toggle performing structural OR-decomposition [default = %s]\n", fOrDecomp? "yes": "not" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); @@ -22584,7 +22588,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, "MFCRTGarmsdgvwzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTGaxrmsdgvwzh" ) ) != EOF ) { switch ( c ) { @@ -22657,6 +22661,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': pPars->fSolveAll ^= 1; break; + case 'x': + pPars->fStoreCex ^= 1; + break; case 'r': pPars->fTwoRounds ^= 1; break; @@ -22713,7 +22720,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: pdr [-MFCRTG <num>] [-armsdgvwzh]\n" ); + Abc_Print( -2, "usage: pdr [-MFCRTG <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" ); @@ -22724,6 +22731,7 @@ usage: 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-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" ); 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" ); @@ -31437,7 +31445,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern void Ga2_ManComputeTest( Gia_Man_t * p ); // extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ); // extern void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ); -// extern void Unr_ManTest( Gia_Man_t * pGia ); +// extern void Unr_ManTest( Gia_Man_t * pGia ); // extern void Mig_ManTest( Gia_Man_t * pGia ); // extern int Gia_ManVerify( Gia_Man_t * pGia ); diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index e55eebb6..6e157aad 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -57,6 +57,7 @@ struct Pdr_Par_t_ int fNotVerbose; // not printing line by line progress int fSilent; // totally silent execution 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 iFrame; // explored up to this frame int RunId; // PDR id in this run diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index a7c4dc35..eb21edfc 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -590,7 +590,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); - Vec_PtrWriteEntry( p->vCexes, p->iOutCur, Pdr_ManDeriveCex(p) ); + Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 ); if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) ) return 0; // all SAT p->pPars->timeLastSolved = clock(); @@ -640,7 +640,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) } if ( RetValue == 0 ) { - Abc_Cex_t * pCex; if ( fPrintClauses ) { Abc_Print( 1, "*** Clauses after frame %d:\n", k ); @@ -659,11 +658,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); - pCex = Pdr_ManDeriveCex(p); - Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCex ); + Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 ); if ( !p->pPars->fNotVerbose ) Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n", - nOutDigits, p->iOutCur, pCex->iFrame, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); + nOutDigits, p->iOutCur, k, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) ) return 0; // all SAT Pdr_QueueClean( p ); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index e799bea9..93bfd78a 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -51,6 +51,7 @@ struct Saig_ParBmc_t_ int nTimeOutGap; // approximate timeout in seconds since the last change int nPisAbstract; // the number of PIs to abstract int fSolveAll; // does not stop at the first SAT output + int fStoreCex; // enable storing CEXes in the MO mode int fDropSatOuts; // replace sat outputs by constant 0 int nFfToAddMax; // max number of flops to add during CBA int fSkipRand; // skip random decisions diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 28bb7729..0c828dbd 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1338,6 +1338,33 @@ clock_t Saig_ManBmcTimeToStop( Saig_ParBmc_t * pPars, clock_t nTimeToStopNG ) /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i ) +{ + Aig_Obj_t * pObjPi; + Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), f*Saig_ManPoNum(p->pAig)+i ); + int j, k, iBit = Saig_ManRegNum(p->pAig); + for ( j = 0; j <= f; j++, iBit += Saig_ManPiNum(p->pAig) ) + Saig_ManForEachPi( p->pAig, pObjPi, k ) + { + int iLit = Saig_ManBmcLiteral( p, pObjPi, j ); + if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) ) + Abc_InfoSetBit( pCex->pData, iBit + k ); + } + return pCex; +} + + +/**Function************************************************************* + Synopsis [Bounded model checking engine.] Description [] @@ -1465,7 +1492,10 @@ clkOther += clock() - clk2; nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); - Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 ); + if ( pPars->fStoreCex ) + Vec_PtrWriteEntry( p->vCexes, i, Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ) ); + else + Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 ); RetValue = 0; // reset the timeout pPars->timeLastSolved = clock(); @@ -1506,16 +1536,6 @@ nTimeSat += clock() - clk2; fFirst = 0; if ( !pPars->fSolveAll ) { - Aig_Obj_t * pObjPi; - Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ); - int j, iBit = Saig_ManRegNum(pAig); - for ( j = 0; j <= f; j++, iBit += Saig_ManPiNum(pAig) ) - Saig_ManForEachPi( p->pAig, pObjPi, k ) - { - int iLit = Saig_ManBmcLiteral( p, pObjPi, j ); - if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) ) - Abc_InfoSetBit( pCex->pData, iBit + k ); - } if ( pPars->fVerbose ) { printf( "%4d %s : ", f, fUnfinished ? "-" : "+" ); @@ -1537,7 +1557,7 @@ nTimeSat += clock() - clk2; fflush( stdout ); } ABC_FREE( pAig->pSeqModel ); - pAig->pSeqModel = pCex; + pAig->pSeqModel = Saig_ManGenerateCex( p, f, i ); RetValue = 0; goto finish; } @@ -1547,7 +1567,7 @@ nTimeSat += clock() - clk2; nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); - Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 ); + Vec_PtrWriteEntry( p->vCexes, i, pPars->fStoreCex? Saig_ManGenerateCex( p, f, i ) : (void *)(ABC_PTRINT_T)1 ); RetValue = 0; // reset the timeout pPars->timeLastSolved = clock(); |