diff options
Diffstat (limited to 'src/sat/aig/fraigClass.c')
-rw-r--r-- | src/sat/aig/fraigClass.c | 182 |
1 files changed, 178 insertions, 4 deletions
diff --git a/src/sat/aig/fraigClass.c b/src/sat/aig/fraigClass.c index 2f2d3e0c..a8df9a72 100644 --- a/src/sat/aig/fraigClass.c +++ b/src/sat/aig/fraigClass.c @@ -80,7 +80,7 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo ) } } stmm_free_table( tSim2Node ); - +/* // print the classes { Vec_Ptr_t * vVec; @@ -93,6 +93,8 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo ) printf( "%d ", Vec_PtrSize(vVec) ); printf( "\n" ); } +*/ + printf( "Classes = %6d. Pairs = %6d.\n", Vec_VecSize(vClasses), Vec_VecSizeSize(vClasses) - Vec_VecSize(vClasses) ); return vClasses; } @@ -115,14 +117,86 @@ unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase ) uKey = 0; if ( fPhase ) for ( i = 0; i < nWords; i++ ) - uKey ^= Primes[i%10] * pData[i]; + uKey ^= i * Primes[i%10] * pData[i]; else for ( i = 0; i < nWords; i++ ) - uKey ^= Primes[i%10] * ~pData[i]; + uKey ^= i * Primes[i%10] * ~pData[i]; return uKey; } + +/**Function************************************************************* + + Synopsis [Splits the equivalence class.] + + Description [Given an equivalence class (vClass) and the simulation info, + split the class into two based on the info.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManSplitClass( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Int_t * vClass, Vec_Int_t * vClass2, Aig_Pattern_t * pPat ) +{ + int NodeId, i, k, w; + Aig_Node_t * pRoot, * pTemp; + unsigned * pRootData, * pTempData; + assert( Vec_IntSize(vClass) > 1 ); + assert( pInfo->nPatsCur == pPat->nBits ); +// printf( "Class = %5d. --> ", Vec_IntSize(vClass) ); + // clear storage for the new classes + Vec_IntClear( vClass2 ); + // get the root member of the class + pRoot = Aig_ManNode( p, Vec_IntEntry(vClass, 0) ); + pRootData = Aig_SimInfoForNode( pInfo, pRoot ); + // sort the class members: + // (1) with the same siminfo as pRoot remain in vClass + // (2) nodes with other siminfo go to vClass2 + k = 1; + Vec_IntForEachEntryStart( vClass, NodeId, i, 1 ) + { + NodeId = Vec_IntEntry(vClass, i); + pTemp = Aig_ManNode( p, NodeId ); + pTempData = Aig_SimInfoForNode( pInfo, pTemp ); + if ( pRoot->fPhase == pTemp->fPhase ) + { + for ( w = 0; w < pInfo->nWords; w++ ) + if ( pRootData[w] != pTempData[w] ) + break; + if ( w == pInfo->nWords ) // the same info + Vec_IntWriteEntry( vClass, k++, NodeId ); + else + { + Vec_IntPush( vClass2, NodeId ); + // record the diffs if they are not distinguished by the first pattern + if ( ((pRootData[0] ^ pTempData[0]) & 1) == 0 ) + for ( w = 0; w < pInfo->nWords; w++ ) + pPat->pData[w] |= (pRootData[w] ^ pTempData[w]); + } + } + else + { + for ( w = 0; w < pInfo->nWords; w++ ) + if ( pRootData[w] != ~pTempData[w] ) + break; + if ( w == pInfo->nWords ) // the same info + Vec_IntWriteEntry( vClass, k++, NodeId ); + else + { + Vec_IntPush( vClass2, NodeId ); + // record the diffs if they are not distinguished by the first pattern + if ( ((pRootData[0] ^ ~pTempData[0]) & 1) == 0 ) + for ( w = 0; w < pInfo->nWords; w++ ) + pPat->pData[w] |= (pRootData[w] ^ ~pTempData[w]); + } + } + } + Vec_IntShrink( vClass, k ); +// printf( "Class1 = %5d. Class2 = %5d.\n", Vec_IntSize(vClass), Vec_IntSize(vClass2) ); +} + /**Function************************************************************* Synopsis [Updates the equivalence classes using the simulation info.] @@ -135,8 +209,108 @@ unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase ) SeeAlso [] ***********************************************************************/ -void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses ) +int Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses, Aig_Pattern_t * pPatMask ) +{ + Vec_Ptr_t * vClass; + int i, k, fSplit = 0; + assert( Vec_VecSize(vClasses) > 0 ); + // collect patterns that lead to changes + Aig_PatternClean( pPatMask ); + // split the classes using the new symmetry info + Vec_VecForEachLevel( vClasses, vClass, i ) + { + if ( i == 0 ) + continue; + // split vClass into two parts (vClass and vClassTemp) + Aig_ManSplitClass( p, pInfo, (Vec_Int_t *)vClass, p->vClassTemp, pPatMask ); + // check if there is any splitting + if ( Vec_IntSize(p->vClassTemp) > 0 ) + fSplit = 1; + // skip the new class if it is empty or trivial + if ( Vec_IntSize(p->vClassTemp) < 2 ) + continue; + // consider replacing the current class with the new one + if ( Vec_PtrSize(vClass) == 1 ) + { + assert( vClasses->pArray[i] == vClass ); + vClasses->pArray[i] = p->vClassTemp; + p->vClassTemp = (Vec_Int_t *)vClass; + i--; + continue; + } + // add the new non-trival class in the end + Vec_PtrPush( (Vec_Ptr_t *)vClasses, p->vClassTemp ); + p->vClassTemp = Vec_IntAlloc( 10 ); + } + // free trivial classes + k = 0; + Vec_VecForEachLevel( vClasses, vClass, i ) + { + assert( Vec_PtrSize(vClass) > 0 ); + if ( Vec_PtrSize(vClass) == 1 ) + Vec_PtrFree(vClass); + else + vClasses->pArray[k++] = vClass; + } + Vec_PtrShrink( (Vec_Ptr_t *)vClasses, k ); + // catch the patterns which led to splitting + printf( "Classes = %6d. Pairs = %6d. Patterns = %3d.\n", + Vec_VecSize(vClasses), + Vec_VecSizeSize(vClasses) - Vec_VecSize(vClasses), + Vec_PtrSize(p->vPats) ); + return fSplit; +} + +/**Function************************************************************* + + Synopsis [Collects useful patterns.] + + Description [If the flag fAddToVector is 1, creates and adds new patterns + to the internal storage of patterns.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManCollectPatterns( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Aig_Pattern_t * pMask, Vec_Ptr_t * vPats ) { + Aig_SimInfo_t * pInfoRes = p->pInfo; + Aig_Pattern_t * pPatNew; + Aig_Node_t * pNode; + int i, k; + + assert( Aig_InfoHasBit(pMask->pData, 0) == 0 ); + for ( i = 0; i < pMask->nBits; i++ ) + { + if ( vPats && Vec_PtrSize(vPats) >= p->nPatsMax ) + break; + if ( i == 0 || Aig_InfoHasBit(pMask->pData, i) ) + { + // expand storage if needed + if ( pInfoRes->nPatsCur == pInfoRes->nPatsMax ) + Aig_SimInfoResize( pInfoRes ); + // create a new pattern + if ( vPats ) + { + pPatNew = Aig_PatternAlloc( Aig_ManPiNum(p) ); + Aig_PatternClean( pPatNew ); + } + // go through the PIs + Aig_ManForEachPi( p, pNode, k ) + { + if ( Aig_InfoHasBit( Aig_SimInfoForNode(pInfo, pNode), i ) ) + { + Aig_InfoSetBit( Aig_SimInfoForPi(pInfoRes, k), pInfoRes->nPatsCur ); + if ( vPats ) Aig_InfoSetBit( pPatNew->pData, k ); + } + } + // store the new pattern + if ( vPats ) Vec_PtrPush( vPats, pPatNew ); + // increment the number of patterns stored + pInfoRes->nPatsCur++; + } + } } //////////////////////////////////////////////////////////////////////// |