Commit 0f29c62e by Alan Mishchenko

Tuning for multi-ouptut solver.

parent ed11db17
...@@ -166,7 +166,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) ...@@ -166,7 +166,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
Vec_Ptr_t * vCexes; Vec_Ptr_t * vCexes;
Aig_Man_t * pTemp; Aig_Man_t * pTemp;
abctime clkStart = Abc_Clock(); abctime clkStart = Abc_Clock();
int nTimeToStop = pPars->TimeOutGlo ? pPars->TimeOutGlo * CLOCKS_PER_SEC + Abc_Clock(): 0; abctime nTimeToStop = pPars->TimeOutGlo ? Abc_Clock() + pPars->TimeOutGlo * CLOCKS_PER_SEC : 0;
int nTotalPo = Saig_ManPoNum(p); int nTotalPo = Saig_ManPoNum(p);
int nTotalSize = Aig_ManObjNum(p); int nTotalSize = Aig_ManObjNum(p);
int TimeOutLoc = pPars->TimeOutLoc; int TimeOutLoc = pPars->TimeOutLoc;
...@@ -202,7 +202,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) ...@@ -202,7 +202,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart ); Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart );
// check timeout // check timeout
if ( nTimeToStop && TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop ) if ( nTimeToStop && Abc_Clock() + TimeOutLoc * CLOCKS_PER_SEC > nTimeToStop )
{ {
printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo ); printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
break; break;
...@@ -234,7 +234,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) ...@@ -234,7 +234,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart ); Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart );
// check timeout // check timeout
if ( nTimeToStop && TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop ) if ( nTimeToStop && Abc_Clock() + TimeOutLoc * CLOCKS_PER_SEC > nTimeToStop )
{ {
printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo ); printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
break; break;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment