Skip to content

A
abc
Commit 0ab8cd11 by Alan Mishchenko
Options

Tuning for multi-ouptut solver.

parent 765da3a3
Showing with 2 additions and 0 deletions
src/sat/bmc/bmcMulti.c
...@@ -157,6 +157,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) ...@@ -157,6 +157,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
pParsSim->fSilent = !pPars->fVeryVerbose; pParsSim->fSilent = !pPars->fVeryVerbose;
pParsSim->TimeOut = TimeOutLoc; pParsSim->TimeOut = TimeOutLoc;
pParsSim->nRandSeed = (i * 17) % 500; pParsSim->nRandSeed = (i * 17) % 500;
pParsSim->nWords = 5;
RetValue *= Ssw_RarSimulate( p, pParsSim ); RetValue *= Ssw_RarSimulate( p, pParsSim );
// sort outputs // sort outputs
if ( p->vSeqModelVec ) if ( p->vSeqModelVec )
...@@ -185,6 +186,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) ...@@ -185,6 +186,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
pParsBmc->fNotVerbose = 1; pParsBmc->fNotVerbose = 1;
pParsBmc->fSilent = !pPars->fVeryVerbose; pParsBmc->fSilent = !pPars->fVeryVerbose;
pParsBmc->nTimeOut = TimeOutLoc; pParsBmc->nTimeOut = TimeOutLoc;
pParsBmc->nTimeOutOne = 100;
RetValue *= Saig_ManBmcScalable( p, pParsBmc ); RetValue *= Saig_ManBmcScalable( p, pParsBmc );
if ( pPars->fVeryVerbose ) if ( pPars->fVeryVerbose )
Abc_Print( 1, "Some outputs are SAT (%d out of %d) after %d frames.\n", Abc_Print( 1, "Some outputs are SAT (%d out of %d) after %d frames.\n",
......
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