summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-12-09 15:12:40 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2012-12-09 15:12:40 -0800
commit9fc1cd0b3f7b149b74048ea2b76cf5a2f4c8cdcc (patch)
tree819626b85a6d494e2640c1c217a8d4254ade2502
parent58d4012a558cbf5f6786dc9fdcadc3f1538bdbe2 (diff)
downloadabc-9fc1cd0b3f7b149b74048ea2b76cf5a2f4c8cdcc.tar.gz
abc-9fc1cd0b3f7b149b74048ea2b76cf5a2f4c8cdcc.tar.bz2
abc-9fc1cd0b3f7b149b74048ea2b76cf5a2f4c8cdcc.zip
Enabling multi-output solving in 'pdr'.
-rw-r--r--src/base/abci/abcDar.c44
-rw-r--r--src/proof/pdr/pdrCore.c23
2 files changed, 43 insertions, 24 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 742f90bb..d45af798 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2145,10 +2145,10 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
else
{
int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
- if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
- Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs );
- else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
+ 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 proved SAT. ",
nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
@@ -2719,23 +2719,37 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
RetValue = Pdr_ManSolve( pMan, pPars );
if ( !pPars->fSilent )
{
- if ( RetValue == 1 )
- Abc_Print( 1, "Property proved. " );
- else if ( RetValue == 0 )
+ if ( pPars->fSolveAll )
{
- if ( pMan->pSeqModel == NULL )
- Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example is not available.\n" );
+ 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 proved SAT. ",
+ nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
+ }
+ else
+ {
+ if ( RetValue == 1 )
+ Abc_Print( 1, "Property proved. " );
+ else if ( RetValue == 0 )
{
- Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
- if ( !Saig_ManVerifyCex( pMan, pMan->pSeqModel ) )
- Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
+ if ( pMan->pSeqModel == NULL )
+ Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example is not available.\n" );
+ else
+ {
+ Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
+ if ( !Saig_ManVerifyCex( pMan, pMan->pSeqModel ) )
+ Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
+ }
}
+ else if ( RetValue == -1 )
+ Abc_Print( 1, "Property UNDECIDED. " );
+ else
+ assert( 0 );
}
- else if ( RetValue == -1 )
- Abc_Print( 1, "Property UNDECIDED. " );
- else
- assert( 0 );
ABC_PRT( "Time", clock() - clk );
}
ABC_FREE( pNtk->pSeqModel );
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 76d6f788..85ad580e 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -606,7 +606,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
else if ( p->pPars->fVerbose )
Abc_Print( 1, "Computation cancelled by the callback.\n" );
p->pPars->iFrame = k;
- return -1;
+ return p->vCexes ? 0 : -1;
}
if ( RetValue == 0 )
{
@@ -620,7 +620,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
else if ( p->pPars->fVerbose )
Abc_Print( 1, "Computation cancelled by the callback.\n" );
p->pPars->iFrame = k;
- return -1;
+ return p->vCexes ? 0 : -1;
}
if ( RetValue == 0 )
{
@@ -676,9 +676,14 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
if ( !p->pPars->fSilent )
- Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
+ {
+ if ( p->timeToStop && clock() > p->timeToStop )
+ Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
+ else
+ Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
+ }
p->pPars->iFrame = k;
- return -1;
+ return p->vCexes ? 0 : -1;
}
if ( RetValue )
{
@@ -689,7 +694,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( !p->pPars->fSilent )
Pdr_ManVerifyInvariant( p );
p->pPars->iFrame = k;
- return 1; // UNSAT
+ return p->vCexes ? 0 : 1; // UNSAT
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 0, clock() - clkStart );
@@ -698,7 +703,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
{
p->pPars->iFrame = k;
- return -1;
+ return p->vCexes ? 0 : -1;
}
if ( p->timeToStop && clock() > p->timeToStop )
{
@@ -712,7 +717,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( !p->pPars->fSilent )
Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
p->pPars->iFrame = k;
- return -1;
+ return p->vCexes ? 0 : -1;
}
if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax )
{
@@ -721,10 +726,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( !p->pPars->fSilent )
Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
p->pPars->iFrame = k;
- return -1;
+ return p->vCexes ? 0 : -1;
}
}
- return RetValue;
+ return p->vCexes ? 0 : RetValue;
}
/**Function*************************************************************