diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-08-12 19:32:42 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-08-12 19:32:42 -0700 |
| commit | 850d39fec30b46b049717ae0a7a5743396b14ecd (patch) | |
| tree | cbdd0b663fd4583bb7a9429a07cb1269eb15147d /src/proof/cec/cecCore.c | |
| parent | b74b7dfc2d2065eebc800c9165a3e15caeb4453d (diff) | |
| download | abc-850d39fec30b46b049717ae0a7a5743396b14ecd.tar.gz abc-850d39fec30b46b049717ae0a7a5743396b14ecd.tar.bz2 abc-850d39fec30b46b049717ae0a7a5743396b14ecd.zip | |
Making &cec use precomputed simulation info.
Diffstat (limited to 'src/proof/cec/cecCore.c')
| -rw-r--r-- | src/proof/cec/cecCore.c | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c index b9529658..9f218dd3 100644 --- a/src/proof/cec/cecCore.c +++ b/src/proof/cec/cecCore.c @@ -360,6 +360,11 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil Vec_IntFreeP( &pAig->vIdsEquiv ); pAig->vIdsEquiv = Vec_IntAlloc( 1000 ); } + if ( pAig->vSimsPi ) + { + pIni->vSimsPi = Vec_WrdDup(pAig->vSimsPi); + pIni->nSimWords = pAig->nSimWords; + } // prepare the managers // SAT sweeping @@ -368,12 +373,12 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil pPars->fColorDiff = 1; // simulation Cec_ManSimSetDefaultParams( pParsSim ); - pParsSim->nWords = pPars->nWords; + pParsSim->nWords = Abc_MaxInt(2*pAig->nSimWords, pPars->nWords); pParsSim->nFrames = pPars->nRounds; pParsSim->fCheckMiter = pPars->fCheckMiter; pParsSim->fDualOut = pPars->fDualOut; pParsSim->fVerbose = pPars->fVerbose; - pSim = Cec_ManSimStart( p->pAig, pParsSim ); + pSim = Cec_ManSimStart( pIni, pParsSim ); // SAT solving Cec_ManSatSetDefaultParams( pParsSat ); pParsSat->nBTLimit = pPars->nBTLimit; @@ -386,7 +391,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil clk = Abc_Clock(); if ( p->pAig->pReprs == NULL ) { - if ( Cec_ManSimClassesPrepare(pSim, -1) || Cec_ManSimClassesRefine(pSim) ) + if ( Cec_ManSimClassesPrepare(pSim, -1) || (!p->pAig->nSimWords && Cec_ManSimClassesRefine(pSim)) ) { Gia_ManStop( p->pAig ); p->pAig = NULL; |