diff options
Diffstat (limited to 'src/aig/fra/fraClass.c')
-rw-r--r-- | src/aig/fra/fraClass.c | 225 |
1 files changed, 120 insertions, 105 deletions
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index 3de54453..170fcd27 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -45,6 +45,80 @@ static inline void Fra_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pOb /**Function************************************************************* + Synopsis [Starts representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig ) +{ + Fra_Cla_t * p; + p = ALLOC( Fra_Cla_t, 1 ); + memset( p, 0, sizeof(Fra_Cla_t) ); + p->pAig = pAig; + p->pMemRepr = ALLOC( Aig_Obj_t *, (Aig_ManObjIdMax(pAig) + 1) ); + memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(pAig) + 1) ); + p->vClasses = Vec_PtrAlloc( 100 ); + p->vClasses1 = Vec_PtrAlloc( 100 ); + p->vClassesTemp = Vec_PtrAlloc( 100 ); + p->vClassOld = Vec_PtrAlloc( 100 ); + p->vClassNew = Vec_PtrAlloc( 100 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stop representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassesStop( Fra_Cla_t * p ) +{ + free( p->pMemClasses ); + free( p->pMemRepr ); + if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp ); + if ( p->vClassNew ) Vec_PtrFree( p->vClassNew ); + if ( p->vClassOld ) Vec_PtrFree( p->vClassOld ); + if ( p->vClasses1 ) Vec_PtrFree( p->vClasses1 ); + if ( p->vClasses ) Vec_PtrFree( p->vClasses ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Starts representation of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManReprStart( p->pAig, Aig_ManObjIdMax(p->pAig) + 1 ); + memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p->pAig) + 1) ); + Vec_PtrForEachEntry( vFailed, pObj, i ) + { +// assert( p->pAig->pReprs[pObj->Id] != NULL ); + p->pAig->pReprs[pObj->Id] = NULL; + } +} + +/**Function************************************************************* + Synopsis [Prints simulation classes.] Description [] @@ -75,7 +149,7 @@ void Fra_PrintClass( Aig_Obj_t ** pClass ) SeeAlso [] ***********************************************************************/ -int Fra_CountClass( Aig_Obj_t ** pClass ) +int Fra_ClassCount( Aig_Obj_t ** pClass ) { Aig_Obj_t * pTemp; int i; @@ -94,13 +168,13 @@ int Fra_CountClass( Aig_Obj_t ** pClass ) SeeAlso [] ***********************************************************************/ -int Fra_CountPairsClasses( Fra_Man_t * p ) +int Fra_ClassesCountPairs( Fra_Cla_t * p ) { Aig_Obj_t ** pClass; int i, nNodes, nPairs = 0; Vec_PtrForEachEntry( p->vClasses, pClass, i ) { - nNodes = Fra_CountClass( pClass ); + nNodes = Fra_ClassCount( pClass ); assert( nNodes > 1 ); nPairs += nNodes * (nNodes - 1) / 2; } @@ -109,7 +183,7 @@ int Fra_CountPairsClasses( Fra_Man_t * p ) /**Function************************************************************* - Synopsis [Prints simulation classes.] + Synopsis [Count the number of literals.] Description [] @@ -118,22 +192,23 @@ int Fra_CountPairsClasses( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Fra_PrintClasses( Fra_Man_t * p ) +int Fra_ClassesCountLits( Fra_Cla_t * p ) { Aig_Obj_t ** pClass; - int i; - printf( "Total classes = %d. Total pairs = %d.\n", Vec_PtrSize(p->vClasses), Fra_CountPairsClasses(p) ); + int i, nNodes, nLits = 0; + nLits = Vec_PtrSize( p->vClasses1 ); Vec_PtrForEachEntry( p->vClasses, pClass, i ) { -// printf( "%3d (%3d) : ", Fra_CountClass(pClass) ); -// Fra_PrintClass( pClass ); + nNodes = Fra_ClassCount( pClass ); + assert( nNodes > 1 ); + nLits += nNodes - 1; } - printf( "\n" ); + return nLits; } /**Function************************************************************* - Synopsis [Computes hash value of the node using its simulation info.] + Synopsis [Prints simulation classes.] Description [] @@ -142,70 +217,18 @@ void Fra_PrintClasses( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -unsigned Fra_NodeHash( Fra_Man_t * p, Aig_Obj_t * pObj ) +void Fra_ClassesPrint( Fra_Cla_t * p ) { - static int s_FPrimes[128] = { - 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, - 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, - 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, - 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, - 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, - 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, - 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, - 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, - 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, - 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, - 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, - 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, - 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 - }; - unsigned * pSims; - unsigned uHash; + Aig_Obj_t ** pClass; int i; - assert( p->nSimWords <= 128 ); - uHash = 0; - pSims = Fra_ObjSim(pObj); - for ( i = 0; i < p->nSimWords; i++ ) - uHash ^= pSims[i] * s_FPrimes[i]; - return uHash; -} - -/**Function******************************************************************** - - Synopsis [Returns the next prime >= p.] - - Description [Copied from CUDD, for stand-aloneness.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -unsigned int Cudd_PrimeFra( unsigned int p ) -{ - int i,pn; - - p--; - do { - p++; - if (p&1) { - pn = 1; - i = 3; - while ((unsigned) (i * i) <= p) { - if (p % i == 0) { - pn = 0; - break; - } - i += 2; - } - } else { - pn = 0; + printf( "Total classes = %d. Total pairs = %d.\n", Vec_PtrSize(p->vClasses), Fra_ClassesCountPairs(p) ); + Vec_PtrForEachEntry( p->vClasses, pClass, i ) + { + printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) ); + Fra_PrintClass( pClass ); } - } while (!pn); - return(p); - -} /* end of Cudd_Prime */ - + printf( "\n" ); +} /**Function************************************************************* @@ -218,31 +241,31 @@ unsigned int Cudd_PrimeFra( unsigned int p ) SeeAlso [] ***********************************************************************/ -void Fra_CreateClasses( Fra_Man_t * p ) +void Fra_ClassesPrepare( Fra_Cla_t * p ) { Aig_Obj_t ** ppTable, ** ppNexts; Aig_Obj_t * pObj, * pTemp; int i, k, nTableSize, nEntries, nNodes, iEntry; // allocate the hash table hashing simulation info into nodes - nTableSize = Cudd_PrimeFra( Aig_ManObjIdMax(p->pManAig) + 1 ); + nTableSize = Aig_PrimeCudd( Aig_ManObjIdMax(p->pAig) + 1 ); ppTable = ALLOC( Aig_Obj_t *, nTableSize ); ppNexts = ALLOC( Aig_Obj_t *, nTableSize ); memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize ); // add all the nodes to the hash table Vec_PtrClear( p->vClasses1 ); - Aig_ManForEachObj( p->pManAig, pObj, i ) + Aig_ManForEachObj( p->pAig, pObj, i ) { if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) continue; // hash the node by its simulation info - iEntry = Fra_NodeHash( p, pObj ) % nTableSize; + iEntry = Fra_NodeHashSims( pObj ) % nTableSize; // check if the node belongs to the class of constant 1 - if ( iEntry == 0 && Fra_NodeHasZeroSim( p, pObj ) ) + if ( iEntry == 0 && Fra_NodeHasZeroSim( pObj ) ) { Vec_PtrPush( p->vClasses1, pObj ); - Fra_ObjSetRepr( pObj, Aig_ManConst1(p->pManAig) ); + Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pAig) ); continue; } // add the node to the class @@ -281,7 +304,7 @@ void Fra_CreateClasses( Fra_Man_t * p ) // copy the entries into storage in the topological order Vec_PtrClear( p->vClasses ); nEntries = 0; - Aig_ManForEachObj( p->pManAig, pObj, i ) + Aig_ManForEachObj( p->pAig, pObj, i ) { if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) continue; @@ -304,7 +327,7 @@ void Fra_CreateClasses( Fra_Man_t * p ) pTemp = Fra_ObjNext(ppNexts, pTemp), k++ ) { p->pMemClasses[2*nEntries+nNodes-k] = pTemp; - Fra_ObjSetRepr( pTemp, pObj ); + Fra_ClassObjSetRepr( pTemp, pObj ); } // add as many empty entries // memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Aig_Obj_t *) * nNodes ); @@ -315,7 +338,7 @@ void Fra_CreateClasses( Fra_Man_t * p ) free( ppTable ); free( ppNexts ); // now it is time to refine the classes - Fra_RefineClasses( p ); + Fra_ClassesRefine( p ); } /**Function************************************************************* @@ -329,7 +352,7 @@ void Fra_CreateClasses( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass ) +Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass ) { Aig_Obj_t * pObj, ** ppThis; int i; @@ -337,7 +360,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass ) // check if the class is going to be refined for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ ) - if ( !Fra_NodeCompareSims(p, ppClass[0], pObj) ) + if ( !Fra_NodeCompareSims(ppClass[0], pObj) ) break; if ( pObj == NULL ) return NULL; @@ -346,7 +369,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass ) Vec_PtrClear( p->vClassNew ); Vec_PtrPush( p->vClassOld, ppClass[0] ); for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ ) - if ( Fra_NodeCompareSims(p, ppClass[0], pObj) ) + if ( Fra_NodeCompareSims(ppClass[0], pObj) ) Vec_PtrPush( p->vClassOld, pObj ); else Vec_PtrPush( p->vClassNew, pObj ); @@ -364,7 +387,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass ) { ppClass[i] = pObj; ppClass[Vec_PtrSize(p->vClassOld)+i] = NULL; - Fra_ObjSetRepr( pObj, i? ppClass[0] : NULL ); + Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL ); } ppClass += 2*Vec_PtrSize(p->vClassOld); // put the new nodes into the class memory @@ -372,7 +395,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass ) { ppClass[i] = pObj; ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL; - Fra_ObjSetRepr( pObj, i? ppClass[0] : NULL ); + Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL ); } return ppClass; } @@ -388,7 +411,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass ) SeeAlso [] ***********************************************************************/ -int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses ) +int Fra_RefineClassLastIter( Fra_Cla_t * p, Vec_Ptr_t * vClasses ) { Aig_Obj_t ** pClass, ** pClass2; int nRefis; @@ -423,19 +446,12 @@ int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses ) SeeAlso [] ***********************************************************************/ -int Fra_RefineClasses( Fra_Man_t * p ) +int Fra_ClassesRefine( Fra_Cla_t * p ) { Vec_Ptr_t * vTemp; Aig_Obj_t ** pClass; - int clk, i, nRefis; - // check if some outputs already became non-constant - // this is a special case when computation can be stopped!!! - if ( p->pPars->fProve ) - Fra_CheckOutputSims( p ); - if ( p->pManFraig->pData ) - return 0; + int i, nRefis; // refine the classes -clk = clock(); nRefis = 0; Vec_PtrClear( p->vClassesTemp ); Vec_PtrForEachEntry( p->vClasses, pClass, i ) @@ -449,7 +465,7 @@ clk = clock(); vTemp = p->vClassesTemp; p->vClassesTemp = p->vClasses; p->vClasses = vTemp; -p->timeRef += clock() - clk; + p->fRefinement = (nRefis > 0); return nRefis; } @@ -464,22 +480,21 @@ p->timeRef += clock() - clk; SeeAlso [] ***********************************************************************/ -int Fra_RefineClasses1( Fra_Man_t * p ) +int Fra_ClassesRefine1( Fra_Cla_t * p ) { Aig_Obj_t * pObj, ** ppClass; - int i, k, nRefis, clk; + int i, k, nRefis; // check if there is anything to refine if ( Vec_PtrSize(p->vClasses1) == 0 ) return 0; -clk = clock(); // make sure constant 1 class contains only non-constant nodes - assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pManAig) ); + assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pAig) ); // collect all the nodes to be refined k = 0; Vec_PtrClear( p->vClassNew ); Vec_PtrForEachEntry( p->vClasses1, pObj, i ) { - if ( Fra_NodeHasZeroSim( p, pObj ) ) + if ( Fra_NodeHasZeroSim( pObj ) ) Vec_PtrWriteEntry( p->vClasses1, k++, pObj ); else Vec_PtrPush( p->vClassNew, pObj ); @@ -487,9 +502,10 @@ clk = clock(); Vec_PtrShrink( p->vClasses1, k ); if ( Vec_PtrSize(p->vClassNew) == 0 ) return 0; + p->fRefinement = 1; if ( Vec_PtrSize(p->vClassNew) == 1 ) { - Fra_ObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL ); + Fra_ClassObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL ); return 1; } // create a new class composed of these nodes @@ -499,12 +515,11 @@ clk = clock(); { ppClass[i] = pObj; ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL; - Fra_ObjSetRepr( pObj, i? ppClass[0] : NULL ); + Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL ); } Vec_PtrPush( p->vClasses, ppClass ); // iteratively refine this class nRefis = 1 + Fra_RefineClassLastIter( p, p->vClasses ); -p->timeRef += clock() - clk; return nRefis; } |