summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-10-27 12:13:40 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-10-27 12:13:40 -0700
commitb39e09bb734e32aefd52ebf4a4096abdaf71585c (patch)
tree585b4a21dea014cdae0c5b40aa88dcd4e45b2f33
parent72f01030c4449a9292a6776ae528aaa3ab83952d (diff)
downloadabc-b39e09bb734e32aefd52ebf4a4096abdaf71585c.tar.gz
abc-b39e09bb734e32aefd52ebf4a4096abdaf71585c.tar.bz2
abc-b39e09bb734e32aefd52ebf4a4096abdaf71585c.zip
Multi-output property solver.
-rw-r--r--src/sat/bmc/bmcMulti.c11
1 files changed, 6 insertions, 5 deletions
diff --git a/src/sat/bmc/bmcMulti.c b/src/sat/bmc/bmcMulti.c
index 6b60daf9..35029034 100644
--- a/src/sat/bmc/bmcMulti.c
+++ b/src/sat/bmc/bmcMulti.c
@@ -141,6 +141,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
int nTimeToStop = pPars->TimeOutGlo ? pPars->TimeOutGlo * CLOCKS_PER_SEC + Abc_Clock(): 0;
int nTotalPo = Saig_ManPoNum(p);
int nTotalSize = Aig_ManObjNum(p);
+ int TimeOutLoc = pPars->TimeOutLoc;
int i, RetValue = -1;
if ( pPars->fVerbose )
printf( "MultiProve parameters: Global timeout = %d sec. Local timeout = %d sec. Time increase = %d %%.\n", pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc );
@@ -154,7 +155,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
pParsSim->fSolveAll = 1;
pParsSim->fNotVerbose = 1;
pParsSim->fSilent = !pPars->fVeryVerbose;
- pParsSim->TimeOut = pPars->TimeOutLoc;
+ pParsSim->TimeOut = TimeOutLoc;
pParsSim->nRandSeed = (i * 17) % 500;
RetValue *= Ssw_RarSimulate( p, pParsSim );
// sort outputs
@@ -172,7 +173,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart );
// check timeout
- if ( nTimeToStop && pPars->TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop )
+ if ( nTimeToStop && TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop )
{
printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
break;
@@ -183,7 +184,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
pParsBmc->fSolveAll = 1;
pParsBmc->fNotVerbose = 1;
pParsBmc->fSilent = !pPars->fVeryVerbose;
- pParsBmc->nTimeOut = pPars->TimeOutLoc;
+ pParsBmc->nTimeOut = TimeOutLoc;
RetValue *= Saig_ManBmcScalable( p, pParsBmc );
if ( pPars->fVeryVerbose )
Abc_Print( 1, "Some outputs are SAT (%d out of %d) after %d frames.\n",
@@ -203,7 +204,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart );
// check timeout
- if ( nTimeToStop && pPars->TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop )
+ if ( nTimeToStop && TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop )
{
printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
break;
@@ -219,7 +220,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
}
// increase timeout
- pPars->TimeOutLoc += pPars->TimeOutLoc * pPars->TimeOutInc / 100;
+ TimeOutLoc += TimeOutLoc * pPars->TimeOutInc / 100;
}
Vec_IntFree( vOutMap );
if ( pPars->fDumpFinal )