diff options
Diffstat (limited to 'src/aig/cec')
-rw-r--r-- | src/aig/cec/cecCec.c | 3 | ||||
-rw-r--r-- | src/aig/cec/cecClass.c | 26 | ||||
-rw-r--r-- | src/aig/cec/cecCore.c | 12 | ||||
-rw-r--r-- | src/aig/cec/cecCorr.c | 148 | ||||
-rw-r--r-- | src/aig/cec/cecIso.c | 4 | ||||
-rw-r--r-- | src/aig/cec/cecPat.c | 22 | ||||
-rw-r--r-- | src/aig/cec/cecSeq.c | 16 | ||||
-rw-r--r-- | src/aig/cec/cecSolve.c | 6 | ||||
-rw-r--r-- | src/aig/cec/cecSweep.c | 6 |
9 files changed, 185 insertions, 58 deletions
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c index 82df6008..ee9f6d3c 100644 --- a/src/aig/cec/cecCec.c +++ b/src/aig/cec/cecCec.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "cecInt.h" +#include "giaAig.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -44,7 +45,7 @@ void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues ) int i; assert( p->pCexComb == NULL ); p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char, - sizeof(Gia_Cex_t) + sizeof(unsigned) * Aig_BitWordNum(Gia_ManCiNum(p)) ); + sizeof(Gia_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p)) ); p->pCexComb->iPo = iOut; p->pCexComb->nPis = Gia_ManCiNum(p); p->pCexComb->nBits = Gia_ManCiNum(p); diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c index 49930836..5a52e913 100644 --- a/src/aig/cec/cecClass.c +++ b/src/aig/cec/cecClass.c @@ -111,14 +111,14 @@ int Cec_ManSimCompareConstFirstBit( unsigned * p, int nWords ) { for ( w = 0; w < nWords; w++ ) if ( p[w] != ~0 ) - return 32*w + Aig_WordFindFirstBit( ~p[w] ); + return 32*w + Gia_WordFindFirstBit( ~p[w] ); return -1; } else { for ( w = 0; w < nWords; w++ ) if ( p[w] != 0 ) - return 32*w + Aig_WordFindFirstBit( p[w] ); + return 32*w + Gia_WordFindFirstBit( p[w] ); return -1; } } @@ -141,14 +141,14 @@ int Cec_ManSimCompareEqualFirstBit( unsigned * p0, unsigned * p1, int nWords ) { for ( w = 0; w < nWords; w++ ) if ( p0[w] != p1[w] ) - return 32*w + Aig_WordFindFirstBit( p0[w] ^ p1[w] ); + return 32*w + Gia_WordFindFirstBit( p0[w] ^ p1[w] ); return -1; } else { for ( w = 0; w < nWords; w++ ) if ( p0[w] != ~p1[w] ) - return 32*w + Aig_WordFindFirstBit( p0[w] ^ ~p1[w] ); + return 32*w + Gia_WordFindFirstBit( p0[w] ^ ~p1[w] ); return -1; } } @@ -467,7 +467,7 @@ void Cec_ManSimProcessRefined( Cec_ManSim_t * p, Vec_Int_t * vRefined ) int * pTable, nTableSize, i, k, Key; if ( Vec_IntSize(vRefined) == 0 ) return; - nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 ); + nTableSize = Gia_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 ); pTable = ABC_CALLOC( int, nTableSize ); Vec_IntForEachEntry( vRefined, i, k ) { @@ -519,15 +519,15 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat ) assert( p->pCexComb == NULL ); assert( iPat >= 0 && iPat < 32 * p->nWords ); p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char, - sizeof(Gia_Cex_t) + sizeof(unsigned) * Aig_BitWordNum(Gia_ManCiNum(p->pAig)) ); + sizeof(Gia_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p->pAig)) ); p->pCexComb->iPo = p->iOut; p->pCexComb->nPis = Gia_ManCiNum(p->pAig); p->pCexComb->nBits = Gia_ManCiNum(p->pAig); for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ ) { pInfo = Vec_PtrEntry( p->vCiSimInfo, i ); - if ( Aig_InfoHasBit( pInfo, iPat ) ) - Aig_InfoSetBit( p->pCexComb->pData, i ); + if ( Gia_InfoHasBit( pInfo, iPat ) ) + Gia_InfoSetBit( p->pCexComb->pData, i ); } } @@ -560,8 +560,8 @@ void Cec_ManSimFindBestPattern( Cec_ManSim_t * p ) for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) { pInfo = Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i ); - if ( Aig_InfoHasBit(p->pBestState->pData, i) != Aig_InfoHasBit(pInfo, iPatBest) ) - Aig_InfoXorBit( p->pBestState->pData, i ); + if ( Gia_InfoHasBit(p->pBestState->pData, i) != Gia_InfoHasBit(pInfo, iPatBest) ) + Gia_InfoXorBit( p->pBestState->pData, i ); } p->pBestState->iPo = ScoreBest; } @@ -686,7 +686,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * else { for ( w = 1; w <= p->nWords; w++ ) - pRes[w] = Aig_ManRandom( 0 ); + pRes[w] = Gia_ManRandom( 0 ); } // make sure the first pattern is always zero pRes[1] ^= (pRes[1] & 1); @@ -798,7 +798,7 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v { pRes0 = Vec_PtrEntry( vInfoCis, i ); for ( w = 0; w < p->nWords; w++ ) - pRes0[w] = Aig_ManRandom( 0 ); + pRes0[w] = Gia_ManRandom( 0 ); } for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) { @@ -814,7 +814,7 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v { pRes0 = Vec_PtrEntry( vInfoCis, i ); for ( w = 0; w < p->nWords; w++ ) - pRes0[w] = Aig_ManRandom( 0 ); + pRes0[w] = Gia_ManRandom( 0 ); } } } diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c index 7759428e..ca0a3665 100644 --- a/src/aig/cec/cecCore.c +++ b/src/aig/cec/cecCore.c @@ -246,7 +246,7 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars ) if ( pPars->fSeqSimulate ) printf( "Performing sequential simulation of %d frames with %d words.\n", pPars->nRounds, pPars->nWords ); - Aig_ManRandom( 1 ); + Gia_ManRandom( 1 ); pSim = Cec_ManSimStart( pAig, pPars ); if ( pAig->pReprs == NULL ) RetValue = Cec_ManSimClassesPrepare( pSim ); @@ -283,7 +283,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) double clkTotal = clock(); // duplicate AIG and transfer equivalence classes - Aig_ManRandom( 1 ); + Gia_ManRandom( 1 ); pIni = Gia_ManDup(pAig); pIni->pReprs = pAig->pReprs; pAig->pReprs = NULL; pIni->pNexts = pAig->pNexts; pAig->pNexts = NULL; @@ -420,7 +420,8 @@ p->timeSat += clock() - clk; printf( "Switching into reduced mode.\n" ); pPars->fColorDiff = 0; } - if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 ) +// if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 ) + else if ( pPars->fDualOut && (Gia_ManAndNum(p->pAig) < 20000 || p->nAllProved + p->nAllDisproved < 10) ) { if ( p->pPars->fVerbose ) printf( "Switching into normal mode.\n" ); @@ -431,6 +432,11 @@ p->timeSat += clock() - clk; finalize: if ( p->pPars->fVerbose ) { + printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", + Gia_ManAndNum(pAig), Gia_ManAndNum(p->pAig), + 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(p->pAig))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), + Gia_ManRegNum(pAig), Gia_ManRegNum(p->pAig), + 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(p->pAig))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) ); ABC_PRTP( "Sim ", p->timeSim, clock() - (int)clkTotal ); ABC_PRTP( "Sat ", p->timeSat-pPat->timeTotalSave, clock() - (int)clkTotal ); ABC_PRTP( "Pat ", p->timePat+pPat->timeTotalSave, clock() - (int)clkTotal ); diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c index 05259bc7..dccd90b0 100644 --- a/src/aig/cec/cecCorr.c +++ b/src/aig/cec/cecCorr.c @@ -49,6 +49,11 @@ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_ Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f ); return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) ); } + if ( f == 0 ) + { + assert( Gia_ObjIsRo(p, pObj) ); + return Gia_ObjCopyF(p, f, pObj); + } assert( f && Gia_ObjIsRo(p, pObj) ); pObj = Gia_ObjRoToRi( p, pObj ); Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1 ); @@ -107,7 +112,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) ); Gia_ManSetPhase( p ); pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 ); Gia_ManForEachRo( p, pObj, i ) @@ -202,6 +207,74 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I /**Function************************************************************* + Synopsis [Derives SRM for signal correspondence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pRepr; + Vec_Int_t * vXorLits; + int f, i, iPrevNew, iObjNew; + assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) ); + assert( Gia_ManRegNum(p) > 0 ); + assert( p->pReprs != NULL ); + p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) ); + Gia_ManSetPhase( p ); + pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); + pNew->pName = Gia_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManForEachRo( p, pObj, i ) + { + Gia_ManAppendCi(pNew); + Gia_ObjSetCopyF( p, 0, pObj, 0 ); + } + for ( f = 0; f < nFrames+fScorr; f++ ) + { + Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); + Gia_ManForEachPi( p, pObj, i ) + Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) ); + } + *pvOutputs = Vec_IntAlloc( 1000 ); + vXorLits = Vec_IntAlloc( 1000 ); + for ( f = 0; f < nFrames; f++ ) + { + Gia_ManForEachObj1( p, pObj, i ) + { + pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); + if ( pRepr == NULL ) + continue; + iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f ); + iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f ); + iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); + if ( iPrevNew != iObjNew ) + { + Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) ); + Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) ); + Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) ); + } + } + } + Vec_IntForEachEntry( vXorLits, iObjNew, i ) + Gia_ManAppendCo( pNew, iObjNew ); + Vec_IntFree( vXorLits ); + Gia_ManHashStop( pNew ); + ABC_FREE( p->pCopies ); +//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); + pNew = Gia_ManCleanup( pTemp = pNew ); +//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Initializes simulation info for lcorr/scorr counter-examples.] Description [] @@ -227,7 +300,7 @@ void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops ) { pInfo = Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) - pInfo[w] = Aig_ManRandom( 0 ); + pInfo[w] = Gia_ManRandom( 0 ); } } @@ -351,17 +424,17 @@ int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBi { pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - if ( Aig_InfoHasBit( pPres, iBit ) && - Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) + if ( Gia_InfoHasBit( pPres, iBit ) && + Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) return 0; } for ( i = 0; i < nLits; i++ ) { pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - Aig_InfoSetBit( pPres, iBit ); - if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) - Aig_InfoXorBit( pInfo, iBit ); + Gia_InfoSetBit( pPres, iBit ); + if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) + Gia_InfoXorBit( pInfo, iBit ); } return 1; } @@ -403,7 +476,7 @@ int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iS for ( k = 1; k < nBits; k++ ) if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) ) break; - kMax = AIG_MAX( kMax, k ); + kMax = ABC_MAX( kMax, k ); if ( k == nBits-1 ) break; } @@ -443,8 +516,8 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i { iLit = Vec_IntEntry( vCexStore, iStart++ ); pInfo = Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) ); - if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) ) - Aig_InfoXorBit( pInfo, iBit ); + if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) ) + Gia_InfoXorBit( pInfo, iBit ); } if ( ++iBit == nBits ) break; @@ -591,7 +664,11 @@ void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int } CounterX -= Gia_ManCoNum(p); nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; - printf( "%3d : c =%8d cl =%7d lit =%8d ", iIter, Counter0, Counter, nLits ); + if ( iIter == -1 ) + printf( "BMC : " ); + else + printf( "%3d : ", iIter ); + printf( "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits ); if ( vStatus ) Vec_StrForEachEntry( vStatus, Entry, i ) { @@ -638,7 +715,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" ); return NULL; } - Aig_ManRandom( 1 ); + Gia_ManRandom( 1 ); // prepare simulation manager Cec_ManSimSetDefaultParams( pParsSim ); pParsSim->nWords = pPars->nWords; @@ -704,14 +781,57 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Vec_IntFree( vOutputs ); //Gia_ManEquivPrintClasses( pAig, 1, 0 ); } + // check the base case + if ( !pPars->fLatchCorr || pPars->nFrames > 1 ) + { + int fChanges = 1; + while ( fChanges ) + { + int clkBmc = clock(); + fChanges = 0; + pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); + if ( Gia_ManPoNum(pSrm) == 0 ) + { + Gia_ManStop( pSrm ); + Vec_IntFree( vOutputs ); + break; + } + pParsSat->nBTLimit *= 10; + if ( pPars->fUseCSat ) + vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); + else + vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); + // refine classes with these counter-examples + if ( Vec_IntSize(vCexStore) ) + { + clk2 = clock(); + RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames ); + clkSim += clock() - clk2; + Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); + fChanges = 1; + } + if ( pPars->fVerbose ) + Cec_ManLCorrPrintStats( pAig, vStatus, -1, clock() - clkBmc ); + // recycle + Vec_IntFree( vCexStore ); + Vec_StrFree( vStatus ); + Gia_ManStop( pSrm ); + Vec_IntFree( vOutputs ); + } + } + else + { + if ( pPars->fVerbose ) + Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk ); + } + // check the overflow if ( r == 100000 ) printf( "The refinement was not finished. The result may be incorrect.\n" ); Cec_ManSimStop( pSim ); clkTotal = clock() - clkTotal; - if ( pPars->fVerbose ) - Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk ); // derive reduced AIG Gia_ManSetProvedNodes( pAig ); + Gia_ManEquivImprove( pAig ); pNew = Gia_ManEquivReduce( pAig, 0, 0, 0 ); //Gia_WriteAiger( pNew, "reduced.aig", 0, 0 ); pNew = Gia_ManSeqCleanup( pTemp = pNew ); diff --git a/src/aig/cec/cecIso.c b/src/aig/cec/cecIso.c index ddb539c2..d9aa5240 100644 --- a/src/aig/cec/cecIso.c +++ b/src/aig/cec/cecIso.c @@ -125,7 +125,7 @@ static inline void Gia_ManIsoRandom( int Id, unsigned * pStore, int nWords ) unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Id ); int w; for ( w = 0; w < nWords; w++ ) - pInfo0[w] = Aig_ManRandom( 0 ); + pInfo0[w] = Gia_ManRandom( 0 ); } /**Function************************************************************* @@ -314,7 +314,7 @@ int * Cec_ManDetectIsomorphism( Gia_Man_t * p ) // start simulation info pStore = ABC_ALLOC( unsigned, Gia_ManObjNum(p) * nWords ); // simulate and create table - nTableSize = Aig_PrimeCudd( 100 + Gia_ManObjNum(p)/2 ); + nTableSize = Gia_PrimeCudd( 100 + Gia_ManObjNum(p)/2 ); pTable = ABC_CALLOC( int, nTableSize ); Gia_ManCleanValue( p ); Gia_ManForEachObj1( p, pObj, i ) diff --git a/src/aig/cec/cecPat.c b/src/aig/cec/cecPat.c index a5be4c1c..8537fe4a 100644 --- a/src/aig/cec/cecPat.c +++ b/src/aig/cec/cecPat.c @@ -414,17 +414,17 @@ int Cec_ManPatCollectTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * { pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - if ( Aig_InfoHasBit( pPres, iBit ) && - Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) + if ( Gia_InfoHasBit( pPres, iBit ) && + Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) return 0; } for ( i = 0; i < nLits; i++ ) { pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - Aig_InfoSetBit( pPres, iBit ); - if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) - Aig_InfoXorBit( pInfo, iBit ); + Gia_InfoSetBit( pPres, iBit ); + if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) + Gia_InfoXorBit( pInfo, iBit ); } return 1; } @@ -450,7 +450,7 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nW int nBits = 32 * nWords; int clk = clock(); vInfo = Vec_PtrAllocSimInfo( nInputs, nWords ); - Aig_ManRandomInfo( vInfo, 0, 0, nWords ); + Gia_ManRandomInfo( vInfo, 0, 0, nWords ); vPres = Vec_PtrAllocSimInfo( nInputs, nWords ); Vec_PtrCleanSimInfo( vPres, 0, nWords ); while ( pMan->iStart < Vec_StrSize(pMan->vStorage) ) @@ -460,11 +460,11 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nW for ( k = 1; k < nBits; k++, k += ((k % (32 * nWordsInit)) == 0) ) if ( Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) ) break; - kMax = AIG_MAX( kMax, k ); + kMax = ABC_MAX( kMax, k ); if ( k == nBits-1 ) { Vec_PtrReallocSimInfo( vInfo ); - Aig_ManRandomInfo( vInfo, 0, nWords, 2*nWords ); + Gia_ManRandomInfo( vInfo, 0, nWords, 2*nWords ); Vec_PtrReallocSimInfo( vPres ); Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords ); nWords *= 2; @@ -511,7 +511,7 @@ Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nReg vInfo = Vec_PtrAllocSimInfo( nInputs, nWords ); Vec_PtrCleanSimInfo( vInfo, 0, nWords ); - Aig_ManRandomInfo( vInfo, nRegs, 0, nWords ); + Gia_ManRandomInfo( vInfo, nRegs, 0, nWords ); vPres = Vec_PtrAllocSimInfo( nInputs, nWords ); Vec_PtrCleanSimInfo( vPres, 0, nWords ); @@ -538,12 +538,12 @@ Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nReg // RetValue = Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ); // assert( RetValue == 1 ); - kMax = AIG_MAX( kMax, k ); + kMax = ABC_MAX( kMax, k ); if ( k == nBits-1 ) { Vec_PtrReallocSimInfo( vInfo ); Vec_PtrCleanSimInfo( vInfo, nWords, 2*nWords ); - Aig_ManRandomInfo( vInfo, nRegs, nWords, 2*nWords ); + Gia_ManRandomInfo( vInfo, nRegs, nWords, 2*nWords ); Vec_PtrReallocSimInfo( vPres ); Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords ); diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c index 3d05172f..28f3a637 100644 --- a/src/aig/cec/cecSeq.c +++ b/src/aig/cec/cecSeq.c @@ -51,7 +51,7 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t { pInfo = Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) - pInfo[w] = Aig_InfoHasBit( pCex->pData, k )? ~0 : 0; + pInfo[w] = Gia_InfoHasBit( pCex->pData, k )? ~0 : 0; } */ for ( k = 0; k < Gia_ManRegNum(pAig); k++ ) @@ -65,16 +65,16 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t { pInfo = Vec_PtrEntry( vInfo, k++ ); for ( w = 0; w < nWords; w++ ) - pInfo[w] = Aig_ManRandom(0); + pInfo[w] = Gia_ManRandom(0); // set simulation pattern and make sure it is second (first will be erased during simulation) - pInfo[0] = (pInfo[0] << 1) | Aig_InfoHasBit( pCex->pData, i ); + pInfo[0] = (pInfo[0] << 1) | Gia_InfoHasBit( pCex->pData, i ); pInfo[0] <<= 1; } for ( ; k < Vec_PtrSize(vInfo); k++ ) { pInfo = Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) - pInfo[w] = Aig_ManRandom(0); + pInfo[w] = Gia_ManRandom(0); } } @@ -100,14 +100,14 @@ void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Ce { pInfo = Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) - pInfo[w] = (pCex && Aig_InfoHasBit(pCex->pData, k))? ~0 : 0; + pInfo[w] = (pCex && Gia_InfoHasBit(pCex->pData, k))? ~0 : 0; } for ( ; k < Vec_PtrSize(vInfo); k++ ) { pInfo = Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) - pInfo[w] = Aig_ManRandom( 0 ); + pInfo[w] = Gia_ManRandom( 0 ); } } @@ -229,7 +229,7 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex } if ( pPars->fVerbose ) printf( "Resimulating %d timeframes.\n", pPars->nRounds + pCex->iFrame + 1 ); - Aig_ManRandom( 1 ); + Gia_ManRandom( 1 ); vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + Gia_ManPiNum(pAig) * (pPars->nRounds + pCex->iFrame + 1), 1 ); Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex ); @@ -275,7 +275,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) printf( "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" ); return -1; } - Aig_ManRandom( 1 ); + Gia_ManRandom( 1 ); // prepare starting pattern pState = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), 0, 0 ); pState->iFrame = -1; diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c index fc2d5d7f..5f032b59 100644 --- a/src/aig/cec/cecSolve.c +++ b/src/aig/cec/cecSolve.c @@ -369,7 +369,7 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p ) Vec_PtrForEachEntry( p->vUsedNodes, pObj, i ) Cec_ObjSetSatNum( p, pObj, 0 ); Vec_PtrClear( p->vUsedNodes ); -// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) ); +// memset( p->pSatVars, 0, sizeof(int) * Gia_ManObjNumMax(p->pAigTotal) ); sat_solver_delete( p->pSat ); } p->pSat = sat_solver_new(); @@ -636,8 +636,8 @@ void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pOb if ( Gia_ObjIsCi(pObj) ) { unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) ); - if ( Cec_ObjSatVarValue( pSat, pObj ) != Aig_InfoHasBit( pInfo, iPat ) ) - Aig_InfoXorBit( pInfo, iPat ); + if ( Cec_ObjSatVarValue( pSat, pObj ) != Gia_InfoHasBit( pInfo, iPat ) ) + Gia_InfoXorBit( pInfo, iPat ); pSat->nCexLits++; // Vec_IntPush( pSat->vCex, Gia_Var2Lit( Gia_ObjCioId(pObj), !Cec_ObjSatVarValue(pSat, pObj) ) ); return; diff --git a/src/aig/cec/cecSweep.c b/src/aig/cec/cecSweep.c index f5e5bd06..1b68efe0 100644 --- a/src/aig/cec/cecSweep.c +++ b/src/aig/cec/cecSweep.c @@ -50,7 +50,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p ) if ( p->pPars->nLevelMax ) Gia_ManLevelNum( p->pAig ); pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) ); - pNew->pName = Aig_UtilStrsav( p->pAig->pName ); + pNew->pName = Gia_UtilStrsav( p->pAig->pName ); Gia_ManHashAlloc( pNew ); piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) ); pDepths = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) ); @@ -70,7 +70,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p ) iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) ); iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) ); iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 ); - pDepths[i] = AIG_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] ); + pDepths[i] = ABC_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] ); if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID || Gia_ObjFailed(p->pAig, i) ) continue; assert( Gia_ObjRepr(p->pAig, i) < i ); @@ -109,7 +109,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p ) Vec_IntPush( p->vXorNodes, Gia_ObjRepr(p->pAig, i) ); Vec_IntPush( p->vXorNodes, i ); // add to the depth of this node - pDepths[i] = 1 + AIG_MAX( pDepths[i], pDepths[Gia_ObjRepr(p->pAig, i)] ); + pDepths[i] = 1 + ABC_MAX( pDepths[i], pDepths[Gia_ObjRepr(p->pAig, i)] ); if ( p->pPars->nDepthMax && pDepths[i] >= p->pPars->nDepthMax ) piCopies[i] = -1; } |