summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c18
-rw-r--r--src/proof/pdr/pdr.h1
-rw-r--r--src/proof/pdr/pdrCore.c8
-rw-r--r--src/sat/bmc/bmc.h1
-rw-r--r--src/sat/bmc/bmcBmc3.c46
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();
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 03:13:50 +0000