From 9be1b076934b0410689c857cd71ef7d21a714b5f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 6 Sep 2007 08:01:00 -0700 Subject: Version abc70906 --- src/aig/fra/fraMan.c | 112 +++++++++++++++++++++++++-------------------------- 1 file changed, 56 insertions(+), 56 deletions(-) (limited to 'src/aig/fra/fraMan.c') diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index 97282e98..f505b0c2 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -42,20 +42,20 @@ void Fra_ParamsDefault( Fra_Par_t * pPars ) { memset( pPars, 0, sizeof(Fra_Par_t) ); - pPars->nSimWords = 32; // the number of words in the simulation info - pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached - pPars->fPatScores = 0; // enables simulation pattern scoring - pPars->MaxScore = 25; // max score after which resimulation is used - pPars->fDoSparse = 1; // skips sparse functions -// pPars->dActConeRatio = 0.05; // the ratio of cone to be bumped -// pPars->dActConeBumpMax = 5.0; // the largest bump of activity - pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped - pPars->dActConeBumpMax = 10.0; // the largest bump of activity - pPars->nBTLimitNode = 100; // conflict limit at a node - pPars->nBTLimitMiter = 500000; // conflict limit at an output - pPars->nFramesK = 0; // the number of timeframes to unroll - pPars->fConeBias = 1; - pPars->fRewrite = 0; + pPars->nSimWords = 32; // the number of words in the simulation info + pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached + pPars->fPatScores = 0; // enables simulation pattern scoring + pPars->MaxScore = 25; // max score after which resimulation is used + pPars->fDoSparse = 1; // skips sparse functions +// pPars->dActConeRatio = 0.05; // the ratio of cone to be bumped +// pPars->dActConeBumpMax = 5.0; // the largest bump of activity + pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped + pPars->dActConeBumpMax = 10.0; // the largest bump of activity + pPars->nBTLimitNode = 100; // conflict limit at a node + pPars->nBTLimitMiter = 500000; // conflict limit at an output + pPars->nFramesK = 0; // the number of timeframes to unroll + pPars->fConeBias = 1; + pPars->fRewrite = 0; } /**Function************************************************************* @@ -72,20 +72,20 @@ void Fra_ParamsDefault( Fra_Par_t * pPars ) void Fra_ParamsDefaultSeq( Fra_Par_t * pPars ) { memset( pPars, 0, sizeof(Fra_Par_t) ); - pPars->nSimWords = 1; // the number of words in the simulation info - pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached - pPars->fPatScores = 0; // enables simulation pattern scoring - pPars->MaxScore = 25; // max score after which resimulation is used - pPars->fDoSparse = 1; // skips sparse functions - pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped - pPars->dActConeBumpMax = 10.0; // the largest bump of activity - pPars->nBTLimitNode =10000000; // conflict limit at a node - pPars->nBTLimitMiter = 500000; // conflict limit at an output - pPars->nFramesK = 1; // the number of timeframes to unroll - pPars->fConeBias = 0; - pPars->fRewrite = 0; - pPars->fLatchCorr = 0; -} + pPars->nSimWords = 1; // the number of words in the simulation info + pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached + pPars->fPatScores = 0; // enables simulation pattern scoring + pPars->MaxScore = 25; // max score after which resimulation is used + pPars->fDoSparse = 1; // skips sparse functions + pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped + pPars->dActConeBumpMax = 10.0; // the largest bump of activity + pPars->nBTLimitNode = 10000000; // conflict limit at a node + pPars->nBTLimitMiter = 500000; // conflict limit at an output + pPars->nFramesK = 1; // the number of timeframes to unroll + pPars->fConeBias = 0; + pPars->fRewrite = 0; + pPars->fLatchCorr = 0; +} /**Function************************************************************* @@ -108,7 +108,7 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars ) memset( p, 0, sizeof(Fra_Man_t) ); p->pPars = pPars; p->pManAig = pManAig; - p->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1; + p->nSizeAlloc = Aig_ManObjNumMax( pManAig ); p->nFramesAll = pPars->nFramesK + 1; // allocate storage for sim pattern p->nPatWords = Aig_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) ); @@ -119,10 +119,6 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars ) // allocate other members p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll ); memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); - p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc * p->nFramesAll + 10000 ); - memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nSizeAlloc * p->nFramesAll + 10000 ); - p->pMemSatNums = ALLOC( int, p->nSizeAlloc * p->nFramesAll + 10000 ); - memset( p->pMemSatNums, 0, sizeof(int) * p->nSizeAlloc * p->nFramesAll + 10000 ); // set random number generator srand( 0xABCABC ); // set the pointer to the manager @@ -142,24 +138,24 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -void Fra_ManClean( Fra_Man_t * p ) +void Fra_ManClean( Fra_Man_t * p, int nNodesMax ) { - int i, Limit; - - Limit = Aig_ManObjIdMax(p->pManFraig) + 1; - for ( i = 0; i < Limit; i++ ) + int i; + // remove old arrays + for ( i = 0; i < p->nMemAlloc; i++ ) if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 ) Vec_PtrFree( p->pMemFanins[i] ); - - memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); - memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * Limit ); - memset( p->pMemSatNums, 0, sizeof(int) * Limit ); - - Aig_ManStop( p->pManFraig ); - p->pManFraig = NULL; - - sat_solver_delete( p->pSat ); - p->pSat = NULL; + // realloc for the new size + if ( p->nMemAlloc < nNodesMax ) + { + int nMemAllocNew = nNodesMax + 5000; + p->pMemFanins = REALLOC( Vec_Ptr_t *, p->pMemFanins, nMemAllocNew ); + p->pMemSatNums = REALLOC( int, p->pMemSatNums, nMemAllocNew ); + p->nMemAlloc = nMemAllocNew; + } + // prepare for the new run + memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc ); + memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc ); } /**Function************************************************************* @@ -180,7 +176,8 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p ) int i; assert( p->pManFraig == NULL ); // start the fraig package - pManFraig = Aig_ManStart( Aig_ManObjIdMax(p->pManAig) + 1 ); + pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) ); + pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName ); pManFraig->nRegs = p->pManAig->nRegs; pManFraig->nAsserts = p->pManAig->nAsserts; // set the pointers to the available fraig nodes @@ -190,6 +187,12 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p ) // set the pointers to the manager Aig_ManForEachObj( pManFraig, pObj, i ) pObj->pData = p; + // allocate memory for mapping FRAIG nodes into SAT numbers and fanins + p->nMemAlloc = p->nSizeAlloc; + p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nMemAlloc ); + memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc ); + p->pMemSatNums = ALLOC( int, p->nMemAlloc ); + memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc ); // make sure the satisfying assignment is node assigned assert( pManFraig->pData == NULL ); return pManFraig; @@ -231,7 +234,6 @@ void Fra_ManFinalizeComb( Fra_Man_t * p ) ***********************************************************************/ void Fra_ManStop( Fra_Man_t * p ) { - int i; if ( p->pPars->fVerbose ) Fra_ManPrint( p ); // save mapping from original nodes into FRAIG nodes @@ -242,9 +244,7 @@ void Fra_ManStop( Fra_Man_t * p ) p->pManAig->pObjCopies = p->pMemFraig; p->pMemFraig = NULL; } - for ( i = 0; i < p->nSizeAlloc; i++ ) - if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 ) - Vec_PtrFree( p->pMemFanins[i] ); + Fra_ManClean( p, 0 ); if ( p->vTimeouts ) Vec_PtrFree( p->vTimeouts ); if ( p->vPiVars ) Vec_PtrFree( p->vPiVars ); if ( p->pSat ) sat_solver_delete( p->pSat ); @@ -271,14 +271,14 @@ void Fra_ManStop( Fra_Man_t * p ) ***********************************************************************/ void Fra_ManPrint( Fra_Man_t * p ) { - double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20); + double nMemory = 1.0*Aig_ManObjNumMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20); printf( "SimWord = %d. Round = %d. Mem = %0.2f Mb. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n", p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/(p->nLitsBeg?p->nLitsBeg:1) ); printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. C-lim = %d. ImpRatio = %6.2f %%\n", p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->pPars->nBTLimitNode, Fra_ImpComputeStateSpaceRatio(p) ); 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->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg ); + 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) ); if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat ); PRT( "AIG simulation ", p->pSml->timeSim ); PRT( "AIG traversal ", p->timeTrav ); -- cgit v1.2.3