diff options
Diffstat (limited to 'src/aig/cgt/cgtMan.c')
-rw-r--r-- | src/aig/cgt/cgtMan.c | 50 |
1 files changed, 28 insertions, 22 deletions
diff --git a/src/aig/cgt/cgtMan.c b/src/aig/cgt/cgtMan.c index 9615d2e6..a3385228 100644 --- a/src/aig/cgt/cgtMan.c +++ b/src/aig/cgt/cgtMan.c @@ -53,7 +53,19 @@ Cgt_Man_t * Cgt_ManCreate( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPar p->pAig = pAig; p->vGatesAll = Vec_VecStart( Saig_ManRegNum(pAig) ); p->vFanout = Vec_PtrAlloc( 1000 ); + p->vVisited = Vec_PtrAlloc( 1000 ); p->nPattWords = 16; + if ( pCare == NULL ) + return p; + // check out the constraints + if ( Aig_ManPiNum(pCare) != Aig_ManPiNum(pAig) ) + { + printf( "The PI count of care (%d) and AIG (%d) differ. Careset is not used.\n", + Aig_ManPiNum(pCare), Aig_ManPiNum(pAig) ); + return p; + } + p->pCare = pCare; + p->vSuppsInv = (Vec_Vec_t *)Aig_ManSupportsInverse( p->pCare ); return p; } @@ -106,27 +118,16 @@ void Cgt_ManClean( Cgt_Man_t * p ) ***********************************************************************/ void Cgt_ManPrintStats( Cgt_Man_t * p ) { + printf( "Params: LevMax = %d. CandMax = %d. OdcMax = %d. ConfMax = %d. VarMin = %d. FlopMin = %d.\n", + p->pPars->nLevelMax, p->pPars->nCandMax, p->pPars->nOdcMax, + p->pPars->nConfMax, p->pPars->nVarsMin, p->pPars->nFlopsMin ); + printf( "SAT : Calls = %d. Unsat = %d. Sat = %d. Fails = %d. Recycles = %d. ", + p->nCalls, p->nCallsUnsat, p->nCallsSat, p->nCallsUndec, p->nRecycles ); + PRT( "Time", p->timeTotal ); /* - double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20); - - printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f Mb.\n", - p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory ); - printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n", - Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), - 0/p->pPars->nIters ); - printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n", - p->nSatProof, p->nSatCallsSat, p->nSatFailsReal, Cgt_ManCountEquivs(p) ); - printf( "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n", - p->nVarsMax, p->nCallsMax, p->nRecyclesTotal, p->nSimRounds ); - printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", - p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), - p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) ); - - p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat; - PRTP( "BMC ", p->timeBmc, p->timeTotal ); - PRTP( "Spec reduce", p->timeReduce, p->timeTotal ); - PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal ); - PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal ); + p->timeOther = p->timeTotal-p->timeAig-p->timePrepare-p->timeSat-p->timeDecision; + PRTP( "AIG ", p->timeAig, p->timeTotal ); + PRTP( "Prepare ", p->timePrepare, p->timeTotal ); PRTP( "SAT solving", p->timeSat, p->timeTotal ); PRTP( " unsat ", p->timeSatUnsat, p->timeTotal ); PRTP( " sat ", p->timeSatSat, p->timeTotal ); @@ -155,8 +156,13 @@ void Cgt_ManStop( Cgt_Man_t * p ) Aig_ManStop( p->pFrame ); Cgt_ManClean( p ); Vec_PtrFree( p->vFanout ); - Vec_PtrFree( p->vGates ); - Vec_VecFree( p->vGatesAll ); + Vec_PtrFree( p->vVisited ); + if ( p->vGates ) + Vec_PtrFree( p->vGates ); + if ( p->vGatesAll ) + Vec_VecFree( p->vGatesAll ); + if ( p->vSuppsInv ) + Vec_VecFree( p->vSuppsInv ); free( p ); } |