diff options
Diffstat (limited to 'src/sat/aig/fraigClass.c')
| -rw-r--r-- | src/sat/aig/fraigClass.c | 320 |
1 files changed, 0 insertions, 320 deletions
diff --git a/src/sat/aig/fraigClass.c b/src/sat/aig/fraigClass.c deleted file mode 100644 index a8df9a72..00000000 --- a/src/sat/aig/fraigClass.c +++ /dev/null @@ -1,320 +0,0 @@ -/**CFile**************************************************************** - - FileName [fraigClass.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [And-Inverter Graph package.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: fraigClass.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "aig.h" -#include "stmm.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Creates the equivalence classes of patterns.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo ) -{ - Vec_Vec_t * vClasses; // equivalence classes - stmm_table * tSim2Node; // temporary hash table hashing key into the class number - Aig_Node_t * pNode; - unsigned uKey; - int i, * pSpot, Entry, ClassNum; - assert( pInfo->Type == 1 ); - // fill in the hash table - tSim2Node = stmm_init_table( stmm_numcmp, stmm_numhash ); - vClasses = Vec_VecAlloc( 100 ); - // enumerate the nodes considered in the equivalence classes -// Aig_ManForEachNode( p, pNode, i ) - Vec_IntForEachEntry( p->vSat2Var, Entry, i ) - { - pNode = Aig_ManNode( p, Entry ); - - if ( Aig_NodeIsPo(pNode) ) - continue; - uKey = Aig_ManHashKey( Aig_SimInfoForNode(pInfo, pNode), pInfo->nWords, pNode->fPhase ); - if ( !stmm_find_or_add( tSim2Node, (char *)uKey, (char ***)&pSpot ) ) // does not exist - *pSpot = (pNode->Id << 1) | 1; // save the node, and do nothing - else if ( (*pSpot) & 1 ) // this is a node - { - // create the class - ClassNum = Vec_VecSize( vClasses ); - Vec_VecPush( vClasses, ClassNum, (void *)((*pSpot) >> 1) ); - Vec_VecPush( vClasses, ClassNum, (void *)pNode->Id ); - // save the class - *pSpot = (ClassNum << 1); - } - else // this is a class - { - ClassNum = ((*pSpot) >> 1); - Vec_VecPush( vClasses, ClassNum, (void *)pNode->Id ); - } - } - stmm_free_table( tSim2Node ); -/* - // print the classes - { - Vec_Ptr_t * vVec; - printf( "PI/PO = %4d/%4d. Nodes = %7d. SatVars = %7d. Non-trivial classes = %5d: \n", - Aig_ManPiNum(p), Aig_ManPoNum(p), - Aig_ManNodeNum(p) - Aig_ManPoNum(p), - Vec_IntSize(p->vSat2Var), Vec_VecSize(vClasses) ); - - Vec_VecForEachLevel( vClasses, vVec, i ) - printf( "%d ", Vec_PtrSize(vVec) ); - printf( "\n" ); - } -*/ - printf( "Classes = %6d. Pairs = %6d.\n", Vec_VecSize(vClasses), Vec_VecSizeSize(vClasses) - Vec_VecSize(vClasses) ); - return vClasses; -} - -/**Function************************************************************* - - Synopsis [Computes the hash key of the simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase ) -{ - static int Primes[10] = { 1009, 2207, 3779, 4001, 4877, 5381, 6427, 6829, 7213, 7919 }; - unsigned uKey; - int i; - uKey = 0; - if ( fPhase ) - for ( i = 0; i < nWords; i++ ) - uKey ^= i * Primes[i%10] * pData[i]; - else - for ( i = 0; i < nWords; 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.] - - Description [Records successful simulation patterns into the pattern - storage.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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++; - } - } -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |