diff options
-rw-r--r-- | src/base/abci/abc.c | 5 | ||||
-rw-r--r-- | src/proof/cec/cecCec.c | 5 | ||||
-rw-r--r-- | src/proof/cec/cecClass.c | 33 | ||||
-rw-r--r-- | src/proof/cec/cecCore.c | 11 |
4 files changed, 42 insertions, 12 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d1ed5901..3219cd9e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -37156,6 +37156,11 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" ); Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0, 0 ); } + if ( pGias[0]->vSimsPi ) + { + pMiter->vSimsPi = Vec_WrdDup(pGias[0]->vSimsPi); + pMiter->nSimWords = pGias[0]->nSimWords; + } pAbc->Status = Cec_ManVerify( pMiter, pPars ); Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb ); Gia_ManStop( pMiter ); diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index ee45aa6c..d450cead 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -349,6 +349,11 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) Gia_ManStop( p ); return RetValue; } + if ( pInit->vSimsPi ) + { + p->vSimsPi = Vec_WrdDup(pInit->vSimsPi); + p->nSimWords = pInit->nSimWords; + } // sweep for equivalences Cec_ManFraSetDefaultParams( pParsFra ); pParsFra->nItersMax = 1000; diff --git a/src/proof/cec/cecClass.c b/src/proof/cec/cecClass.c index 2d820c39..be88b9be 100644 --- a/src/proof/cec/cecClass.c +++ b/src/proof/cec/cecClass.c @@ -878,19 +878,34 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax ) if ( pObj->Value ) Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 ); // perform simulation - p->nWords = 1; - do { + if ( p->pAig->nSimWords ) + { + p->nWords = 2*p->pAig->nSimWords; + assert( Vec_WrdSize(p->pAig->vSimsPi) == Gia_ManCiNum(p->pAig) * p->pAig->nSimWords ); + //Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo ); + for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ ) + memmove( Vec_PtrEntry(p->vCiSimInfo, i), Vec_WrdEntryP(p->pAig->vSimsPi, i*p->pAig->nSimWords), sizeof(word)*p->pAig->nSimWords ); + if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) ) + return 1; if ( p->pPars->fVerbose ) Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) ); - for ( i = 0; i < 4; i++ ) - { - Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo ); - if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) ) - return 1; + } + else + { + p->nWords = 1; + do { + if ( p->pPars->fVerbose ) + Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) ); + for ( i = 0; i < 4; i++ ) + { + Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo ); + if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) ) + return 1; + } + p->nWords = 2 * p->nWords + 1; } - p->nWords = 2 * p->nWords + 1; + while ( p->nWords <= p->pPars->nWords ); } - while ( p->nWords <= p->pPars->nWords ); return 0; } 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; |