diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-21 16:40:56 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-21 16:40:56 -0700 |
| commit | bfe7333f4105442a7df530c68ed1cf1b7da7edda (patch) | |
| tree | 295068e63d3e63b94e401ebef9ce85c341f5d72a /src/proof/cec/cecCore.c | |
| parent | aa3d8a65b43d8fb526721b8f40d8296b9c2db7a7 (diff) | |
| download | abc-bfe7333f4105442a7df530c68ed1cf1b7da7edda.tar.gz abc-bfe7333f4105442a7df530c68ed1cf1b7da7edda.tar.bz2 abc-bfe7333f4105442a7df530c68ed1cf1b7da7edda.zip | |
Adding new command 'dump_equiv'.
Diffstat (limited to 'src/proof/cec/cecCore.c')
| -rw-r--r-- | src/proof/cec/cecCore.c | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c index c9e9f67a..ed5c4ab7 100644 --- a/src/proof/cec/cecCore.c +++ b/src/proof/cec/cecCore.c @@ -236,7 +236,7 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars ) Gia_Man_t * pNew; Cec_ManPat_t * pPat; pPat = Cec_ManPatStart(); - Cec_ManSatSolve( pPat, pAig, pPars ); + Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL ); // pNew = Gia_ManDupDfsSkip( pAig ); pNew = Gia_ManDup( pAig ); Cec_ManPatStop( pPat ); @@ -351,6 +351,12 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil pIni = Gia_ManDup(pAig); pIni->pReprs = pAig->pReprs; pAig->pReprs = NULL; pIni->pNexts = pAig->pNexts; pAig->pNexts = NULL; + if ( pPars->fUseOrigIds ) + { + Gia_ManOrigIdsInit( pIni ); + Vec_IntFreeP( &pAig->vIdsEquiv ); + pAig->vIdsEquiv = Vec_IntAlloc( 1000 ); + } // prepare the managers // SAT sweeping @@ -429,7 +435,7 @@ clk = Abc_Clock(); if ( pPars->fRunCSat ) Cec_ManSatSolveCSat( pPat, pSrm, pParsSat ); else - Cec_ManSatSolve( pPat, pSrm, pParsSat ); + Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv ); p->timeSat += Abc_Clock() - clk; if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) ) { |