src/aig/fra/fraClass.c File Reference

#include "fra.h"
Include dependency graph for fraClass.c:

Go to the source code of this file.

Functions

static Aig_Obj_t * Fra_ObjNext (Aig_Obj_t **ppNexts, Aig_Obj_t *pObj)
static void Fra_ObjSetNext (Aig_Obj_t **ppNexts, Aig_Obj_t *pObj, Aig_Obj_t *pNext)
Fra_Cla_t * Fra_ClassesStart (Aig_Man_t *pAig)
void Fra_ClassesStop (Fra_Cla_t *p)
void Fra_ClassesCopyReprs (Fra_Cla_t *p, Vec_Ptr_t *vFailed)
int Fra_ClassCount (Aig_Obj_t **pClass)
int Fra_ClassesCountLits (Fra_Cla_t *p)
int Fra_ClassesCountPairs (Fra_Cla_t *p)
void Fra_PrintClass (Aig_Obj_t **pClass)
void Fra_ClassesPrint (Fra_Cla_t *p, int fVeryVerbose)
void Fra_ClassesPrepare (Fra_Cla_t *p, int fLatchCorr)
Aig_Obj_t ** Fra_RefineClassOne (Fra_Cla_t *p, Aig_Obj_t **ppClass)
int Fra_RefineClassLastIter (Fra_Cla_t *p, Vec_Ptr_t *vClasses)
int Fra_ClassesRefine (Fra_Cla_t *p)
int Fra_ClassesRefine1 (Fra_Cla_t *p, int fRefineNewClass, int *pSkipped)
void Fra_ClassesTest (Fra_Cla_t *p, int Id1, int Id2)
void Fra_ClassesLatchCorr (Fra_Man_t *p)
void Fra_ClassesPostprocess (Fra_Cla_t *p)
void Fra_ClassesSelectRepr (Fra_Cla_t *p)
static Aig_Obj_t * Fra_ObjEqu (Aig_Obj_t **ppEquivs, Aig_Obj_t *pObj)
static void Fra_ObjSetEqu (Aig_Obj_t **ppEquivs, Aig_Obj_t *pObj, Aig_Obj_t *pNode)
static Aig_Obj_t * Fra_ObjChild0Equ (Aig_Obj_t **ppEquivs, Aig_Obj_t *pObj)
static Aig_Obj_t * Fra_ObjChild1Equ (Aig_Obj_t **ppEquivs, Aig_Obj_t *pObj)
static void Fra_ClassesDeriveNode (Aig_Man_t *pManFraig, Aig_Obj_t *pObj, Aig_Obj_t **ppEquivs)
Aig_Man_t * Fra_ClassesDeriveAig (Fra_Cla_t *p, int nFramesK)

Function Documentation

int Fra_ClassCount ( Aig_Obj_t **  pClass  ) 

Function*************************************************************

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 142 of file fraClass.c.

00143 {
00144     Aig_Obj_t * pTemp;
00145     int i;
00146     for ( i = 0; pTemp = pClass[i]; i++ );
00147     return i;
00148 }

void Fra_ClassesCopyReprs ( Fra_Cla_t *  p,
Vec_Ptr_t *  vFailed 
)

Function*************************************************************

Synopsis [Starts representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 111 of file fraClass.c.

00112 {
00113     Aig_Obj_t * pObj;
00114     int i;
00115     Aig_ManReprStart( p->pAig, Aig_ManObjNumMax(p->pAig) );
00116     memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) );
00117     if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 )
00118     {
00119         Aig_ManForEachObj( p->pAig, pObj, i )
00120         {
00121             if ( p->pAig->pReprs[i] != NULL )
00122                 printf( "Classes are not cleared!\n" );
00123             assert( p->pAig->pReprs[i] == NULL );
00124         }
00125     }
00126     if ( vFailed )
00127         Vec_PtrForEachEntry( vFailed, pObj, i )
00128             p->pAig->pReprs[pObj->Id] = NULL;
00129 }

int Fra_ClassesCountLits ( Fra_Cla_t *  p  ) 

Function*************************************************************

Synopsis [Count the number of literals.]

Description []

SideEffects []

SeeAlso []

Definition at line 161 of file fraClass.c.

00162 {
00163     Aig_Obj_t ** pClass;
00164     int i, nNodes, nLits = 0;
00165     nLits = Vec_PtrSize( p->vClasses1 );
00166     Vec_PtrForEachEntry( p->vClasses, pClass, i )
00167     {
00168         nNodes = Fra_ClassCount( pClass );
00169         assert( nNodes > 1 );
00170         nLits += nNodes - 1;
00171     }
00172     return nLits;
00173 }

int Fra_ClassesCountPairs ( Fra_Cla_t *  p  ) 

Function*************************************************************

Synopsis [Count the number of pairs.]

Description []

SideEffects []

SeeAlso []

Definition at line 186 of file fraClass.c.

00187 {
00188     Aig_Obj_t ** pClass;
00189     int i, nNodes, nPairs = 0;
00190     Vec_PtrForEachEntry( p->vClasses, pClass, i )
00191     {
00192         nNodes = Fra_ClassCount( pClass );
00193         assert( nNodes > 1 );
00194         nPairs += nNodes * (nNodes - 1) / 2;
00195     }
00196     return nPairs;
00197 }

Aig_Man_t* Fra_ClassesDeriveAig ( Fra_Cla_t *  p,
int  nFramesK 
)

Function*************************************************************

Synopsis [Derives AIG for the partitioned problem.]

Description []

SideEffects []

SeeAlso []

Definition at line 791 of file fraClass.c.

00792 {
00793     Aig_Man_t * pManFraig;
00794     Aig_Obj_t * pObj, * pObjNew;
00795     Aig_Obj_t ** pLatches, ** ppEquivs;
00796     int i, k, f, nFramesAll = nFramesK + 1;
00797     assert( Aig_ManRegNum(p->pAig) > 0 );
00798     assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
00799     assert( nFramesK > 0 );
00800     // start the fraig package
00801     pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll );
00802     pManFraig->pName = Aig_UtilStrsav( p->pAig->pName );
00803     // allocate place for the node mapping
00804     ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
00805     Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
00806     // create latches for the first frame
00807     Aig_ManForEachLoSeq( p->pAig, pObj, i )
00808         Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
00809     // add timeframes
00810     pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
00811     for ( f = 0; f < nFramesAll; f++ )
00812     {
00813         // create PIs for this frame
00814         Aig_ManForEachPiSeq( p->pAig, pObj, i )
00815             Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
00816         // set the constraints on the latch outputs
00817         Aig_ManForEachLoSeq( p->pAig, pObj, i )
00818             Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
00819         // add internal nodes of this frame
00820         Aig_ManForEachNode( p->pAig, pObj, i )
00821         {
00822             pObjNew = Aig_And( pManFraig, Fra_ObjChild0Equ(ppEquivs, pObj), Fra_ObjChild1Equ(ppEquivs, pObj) );
00823             Fra_ObjSetEqu( ppEquivs, pObj, pObjNew );
00824             Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
00825         }
00826         if ( f == nFramesAll - 1 )
00827             break;
00828         if ( f == nFramesAll - 2 )
00829             pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
00830         // save the latch input values
00831         k = 0;
00832         Aig_ManForEachLiSeq( p->pAig, pObj, i )
00833             pLatches[k++] = Fra_ObjChild0Equ( ppEquivs, pObj );
00834         // insert them to the latch output values
00835         k = 0;
00836         Aig_ManForEachLoSeq( p->pAig, pObj, i )
00837             Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] );
00838     }
00839     free( pLatches );
00840     free( ppEquivs );
00841     // mark the asserts
00842     assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 );
00843 printf( "Assert miters = %6d. Output miters = %6d.\n", 
00844        pManFraig->nAsserts, Aig_ManPoNum(pManFraig) - pManFraig->nAsserts );
00845     // remove dangling nodes
00846     Aig_ManCleanup( pManFraig );
00847     return pManFraig;
00848 }

static void Fra_ClassesDeriveNode ( Aig_Man_t *  pManFraig,
Aig_Obj_t *  pObj,
Aig_Obj_t **  ppEquivs 
) [inline, static]

Function*************************************************************

Synopsis [Add the node and its constraints to the new AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 755 of file fraClass.c.

00756 {
00757     Aig_Obj_t * pObjNew, * pObjRepr, * pObjReprNew, * pMiter;//, * pObjNew2;
00758     // skip nodes without representative
00759     if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
00760         return;
00761     assert( pObjRepr->Id < pObj->Id );
00762     // get the new node 
00763     pObjNew = Fra_ObjEqu( ppEquivs, pObj );
00764     // get the new node of the representative
00765     pObjReprNew = Fra_ObjEqu( ppEquivs, pObjRepr );
00766     // if this is the same node, no need to add constraints
00767     if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
00768         return;
00769     // these are different nodes - perform speculative reduction
00770 //    pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
00771     // set the new node
00772 //    Fra_ObjSetEqu( ppEquivs, pObj, pObjNew2 );
00773     // add the constraint
00774     pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
00775     pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
00776     pMiter = Aig_Not( pMiter );
00777     Aig_ObjCreatePo( pManFraig, pMiter );
00778 }

void Fra_ClassesLatchCorr ( Fra_Man_t *  p  ) 

Function*************************************************************

Synopsis [Creates latch correspondence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 611 of file fraClass.c.

00612 {
00613     Aig_Obj_t * pObj;
00614     int i, nEntries = 0;
00615     Vec_PtrClear( p->pCla->vClasses1 );
00616     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
00617     {
00618         Vec_PtrPush( p->pCla->vClasses1, pObj );
00619         Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
00620     }
00621     // allocate room for classes
00622     p->pCla->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) );
00623     p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries;
00624 }

void Fra_ClassesPostprocess ( Fra_Cla_t *  p  ) 

Function*************************************************************

Synopsis [Postprocesses the classes by removing half of the less useful.]

Description []

SideEffects []

SeeAlso []

Definition at line 637 of file fraClass.c.

00638 {
00639     int Ratio = 2;
00640     Fra_Sml_t * pComb;
00641     Aig_Obj_t * pObj, * pRepr, ** ppClass;
00642     int * pWeights, WeightMax = 0, i, k, c;
00643     // perform combinational simulation
00644     pComb = Fra_SmlSimulateComb( p->pAig, 32 );
00645     // compute the weight of each node in the classes
00646     pWeights = ALLOC( int, Aig_ManObjNumMax(p->pAig) );
00647     memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
00648     Aig_ManForEachObj( p->pAig, pObj, i )
00649     { 
00650         pRepr = Fra_ClassObjRepr( pObj );
00651         if ( pRepr == NULL )
00652             continue;
00653         pWeights[i] = Fra_SmlNodeNotEquWeight( pComb, pRepr->Id, pObj->Id );
00654         WeightMax = AIG_MAX( WeightMax, pWeights[i] );
00655     }
00656     Fra_SmlStop( pComb );
00657     printf( "Before: Const = %6d. Class = %6d.  ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
00658     // remove nodes from classes whose weight is less than WeightMax/Ratio
00659     k = 0;
00660     Vec_PtrForEachEntry( p->vClasses1, pObj, i )
00661     {
00662         if ( pWeights[pObj->Id] >= WeightMax/Ratio )
00663             Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
00664         else
00665             Fra_ClassObjSetRepr( pObj, NULL );
00666     }
00667     Vec_PtrShrink( p->vClasses1, k );
00668     // in each class, compact the nodes
00669     Vec_PtrForEachEntry( p->vClasses, ppClass, i )
00670     {
00671         k = 1;
00672         for ( c = 1; ppClass[c]; c++ )
00673         {
00674             if ( pWeights[ppClass[c]->Id] >= WeightMax/Ratio )
00675                 ppClass[k++] = ppClass[c];
00676             else
00677                 Fra_ClassObjSetRepr( ppClass[c], NULL );
00678         }
00679         ppClass[k] = NULL;
00680     }
00681     // remove classes with only repr
00682     k = 0;
00683     Vec_PtrForEachEntry( p->vClasses, ppClass, i )
00684         if ( ppClass[1] != NULL )
00685             Vec_PtrWriteEntry( p->vClasses, k++, ppClass );
00686     Vec_PtrShrink( p->vClasses, k );
00687     printf( "After: Const = %6d. Class = %6d. \n", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
00688     free( pWeights );
00689 }

void Fra_ClassesPrepare ( Fra_Cla_t *  p,
int  fLatchCorr 
)

Function*************************************************************

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 273 of file fraClass.c.

00274 {
00275     Aig_Obj_t ** ppTable, ** ppNexts;
00276     Aig_Obj_t * pObj, * pTemp;
00277     int i, k, nTableSize, nEntries, nNodes, iEntry;
00278 
00279     // allocate the hash table hashing simulation info into nodes
00280     nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig) );
00281     ppTable = ALLOC( Aig_Obj_t *, nTableSize ); 
00282     ppNexts = ALLOC( Aig_Obj_t *, nTableSize ); 
00283     memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );
00284 
00285     // add all the nodes to the hash table
00286     Vec_PtrClear( p->vClasses1 );
00287     Aig_ManForEachObj( p->pAig, pObj, i )
00288     {
00289         if ( fLatchCorr )
00290         {
00291             if ( !Aig_ObjIsPi(pObj) )
00292                 continue;
00293         }
00294         else
00295         {
00296             if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
00297                 continue;
00298             // skip the node with more that the given number of levels
00299 //            if ( pObj->Level > 3 )
00300 //                continue;
00301         }
00302         // hash the node by its simulation info
00303         iEntry = p->pFuncNodeHash( pObj, nTableSize );
00304         // check if the node belongs to the class of constant 1
00305         if ( p->pFuncNodeIsConst( pObj ) )
00306         {
00307             Vec_PtrPush( p->vClasses1, pObj );
00308             Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pAig) );
00309             continue;
00310         }
00311         // add the node to the class
00312         if ( ppTable[iEntry] == NULL )
00313         {
00314             ppTable[iEntry] = pObj;
00315             Fra_ObjSetNext( ppNexts, pObj, pObj );
00316         }
00317         else
00318         {
00319             Fra_ObjSetNext( ppNexts, pObj, Fra_ObjNext(ppNexts,ppTable[iEntry]) );
00320             Fra_ObjSetNext( ppNexts, ppTable[iEntry], pObj );
00321         }
00322     }
00323 
00324     // count the total number of nodes in the non-trivial classes
00325     // mark the representative nodes of each equivalence class
00326     nEntries = 0;
00327     for ( i = 0; i < nTableSize; i++ )
00328         if ( ppTable[i] && ppTable[i] != Fra_ObjNext(ppNexts, ppTable[i]) )
00329         {
00330             for ( pTemp = Fra_ObjNext(ppNexts, ppTable[i]), k = 1; 
00331                   pTemp != ppTable[i]; 
00332                   pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
00333             assert( k > 1 );
00334             nEntries += k;
00335             // mark the node
00336             assert( ppTable[i]->fMarkA == 0 );
00337             ppTable[i]->fMarkA = 1;
00338         }
00339 
00340     // allocate room for classes
00341     p->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
00342     p->pMemClassesFree = p->pMemClasses + 2*nEntries;
00343  
00344     // copy the entries into storage in the topological order
00345     Vec_PtrClear( p->vClasses );
00346     nEntries = 0;
00347     Aig_ManForEachObj( p->pAig, pObj, i )
00348     {
00349         if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
00350             continue;
00351         // skip the nodes that are not representatives of non-trivial classes
00352         if ( pObj->fMarkA == 0 )
00353             continue;
00354         pObj->fMarkA = 0;
00355         // add the class of nodes
00356         Vec_PtrPush( p->vClasses, p->pMemClasses + 2*nEntries );
00357         // count the number of entries in this class
00358         for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 
00359               pTemp != pObj; 
00360               pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
00361         nNodes = k;
00362         assert( nNodes > 1 );
00363         // add the nodes to the class in the topological order
00364         p->pMemClasses[2*nEntries] = pObj;
00365         for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 
00366               pTemp != pObj; 
00367               pTemp = Fra_ObjNext(ppNexts, pTemp), k++ )
00368         {
00369             p->pMemClasses[2*nEntries+nNodes-k] = pTemp;
00370             Fra_ClassObjSetRepr( pTemp, pObj );
00371         }
00372         // add as many empty entries
00373         p->pMemClasses[2*nEntries + nNodes] = NULL;
00374         // increment the number of entries
00375         nEntries += k;
00376     }
00377     free( ppTable );
00378     free( ppNexts );
00379     // now it is time to refine the classes
00380     Fra_ClassesRefine( p );
00381 }

void Fra_ClassesPrint ( Fra_Cla_t *  p,
int  fVeryVerbose 
)

Function*************************************************************

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 233 of file fraClass.c.

00234 {
00235     Aig_Obj_t ** pClass;
00236     Aig_Obj_t * pObj;
00237     int i;
00238 
00239     printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
00240         Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
00241     if ( p->vImps && Vec_IntSize(p->vImps) > 0 )
00242         printf( "Imp = %5d. ", Vec_IntSize(p->vImps) );
00243     printf( "\n" );
00244 
00245     if ( fVeryVerbose )
00246     {
00247         Vec_PtrForEachEntry( p->vClasses1, pObj, i )
00248             assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) );
00249         printf( "Constants { " );
00250         Vec_PtrForEachEntry( p->vClasses1, pObj, i )
00251             printf( "%d ", pObj->Id );
00252         printf( "}\n" );
00253         Vec_PtrForEachEntry( p->vClasses, pClass, i )
00254         {
00255             printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
00256             Fra_PrintClass( pClass );
00257         }
00258         printf( "\n" );
00259     }
00260 }

int Fra_ClassesRefine ( Fra_Cla_t *  p  ) 

Function*************************************************************

Synopsis [Refines the classes after simulation.]

Description [Assumes that simulation info is assigned. Returns the number of classes refined.]

SideEffects []

SeeAlso []

Definition at line 489 of file fraClass.c.

00490 {
00491     Vec_Ptr_t * vTemp;
00492     Aig_Obj_t ** pClass;
00493     int i, nRefis;
00494     // refine the classes
00495     nRefis = 0;
00496     Vec_PtrClear( p->vClassesTemp );
00497     Vec_PtrForEachEntry( p->vClasses, pClass, i )
00498     {
00499         // add the class to the new array
00500         assert( pClass[0] != NULL );
00501         Vec_PtrPush( p->vClassesTemp, pClass );
00502         // refine the class iteratively
00503         nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp );
00504     }
00505     // exchange the class representation
00506     vTemp = p->vClassesTemp;
00507     p->vClassesTemp = p->vClasses;
00508     p->vClasses = vTemp;
00509     return nRefis;
00510 }

int Fra_ClassesRefine1 ( Fra_Cla_t *  p,
int  fRefineNewClass,
int *  pSkipped 
)

Function*************************************************************

Synopsis [Refines constant 1 equivalence class.]

Description []

SideEffects []

SeeAlso []

Definition at line 523 of file fraClass.c.

00524 {
00525     Aig_Obj_t * pObj, ** ppClass;
00526     int i, k, nRefis = 1;
00527     // check if there is anything to refine
00528     if ( Vec_PtrSize(p->vClasses1) == 0 )
00529         return 0;
00530     // make sure constant 1 class contains only non-constant nodes
00531     assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pAig) );
00532     // collect all the nodes to be refined
00533     k = 0;
00534     Vec_PtrClear( p->vClassNew );
00535     Vec_PtrForEachEntry( p->vClasses1, pObj, i )
00536     {
00537         if ( p->pFuncNodeIsConst( pObj ) )
00538             Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
00539         else 
00540             Vec_PtrPush( p->vClassNew, pObj );
00541     }
00542     Vec_PtrShrink( p->vClasses1, k );
00543     if ( Vec_PtrSize(p->vClassNew) == 0 )
00544         return 0;
00545 /*
00546     printf( "Refined const-1 class: {" );
00547     Vec_PtrForEachEntry( p->vClassNew, pObj, i )
00548         printf( " %d", pObj->Id );
00549     printf( " }\n" );
00550 */
00551     if ( Vec_PtrSize(p->vClassNew) == 1 )
00552     {
00553         Fra_ClassObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL );
00554         return 1;
00555     }
00556     // create a new class composed of these nodes
00557     ppClass = p->pMemClassesFree;
00558     p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew);
00559     Vec_PtrForEachEntry( p->vClassNew, pObj, i )
00560     {
00561         ppClass[i] = pObj;
00562         ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
00563         Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
00564     }
00565     assert( ppClass[0] != NULL );
00566     Vec_PtrPush( p->vClasses, ppClass );
00567     // iteratively refine this class
00568     if ( fRefineNewClass )
00569         nRefis += Fra_RefineClassLastIter( p, p->vClasses );
00570     else if ( pSkipped )
00571         (*pSkipped)++;
00572     return nRefis;
00573 }

void Fra_ClassesSelectRepr ( Fra_Cla_t *  p  ) 

Function*************************************************************

Synopsis [Postprocesses the classes by selecting representative lowest in top order.]

Description []

SideEffects []

SeeAlso []

Definition at line 702 of file fraClass.c.

00703 {
00704     Aig_Obj_t ** pClass, * pNodeMin;
00705     int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur;
00706     // reassign representatives in each class
00707     Vec_PtrForEachEntry( p->vClasses, pClass, i )
00708     {
00709         // collect support sizes and find the min-support node
00710         pNodeMin = NULL;
00711         nSuppSizeMin = AIG_INFINITY;
00712         for ( c = 0; pClass[c]; c++ )
00713         {
00714             nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] );
00715 //            nSuppSizeCur = 1;
00716             if ( nSuppSizeMin > nSuppSizeCur || 
00717                 (nSuppSizeMin == nSuppSizeCur && pNodeMin->Level > pClass[c]->Level) )
00718             {
00719                 nSuppSizeMin = nSuppSizeCur;
00720                 pNodeMin = pClass[c];
00721                 cMinSupp = c; 
00722             }
00723         }
00724         // skip the case when the repr did not change
00725         if ( cMinSupp == 0 )
00726             continue;
00727         // make the new node the representative of the class
00728         pClass[cMinSupp] = pClass[0];
00729         pClass[0] = pNodeMin;
00730         // set the representative
00731         for ( c = 0; pClass[c]; c++ )
00732             Fra_ClassObjSetRepr( pClass[c], c? pClass[0] : NULL );
00733     }
00734 }

Fra_Cla_t* Fra_ClassesStart ( Aig_Man_t *  pAig  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Starts representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 57 of file fraClass.c.

00058 {
00059     Fra_Cla_t * p;
00060     p = ALLOC( Fra_Cla_t, 1 );
00061     memset( p, 0, sizeof(Fra_Cla_t) );
00062     p->pAig = pAig;
00063     p->pMemRepr  = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
00064     memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) );
00065     p->vClasses     = Vec_PtrAlloc( 100 );
00066     p->vClasses1    = Vec_PtrAlloc( 100 );
00067     p->vClassesTemp = Vec_PtrAlloc( 100 );
00068     p->vClassOld    = Vec_PtrAlloc( 100 );
00069     p->vClassNew    = Vec_PtrAlloc( 100 );
00070     p->pFuncNodeHash      = Fra_SmlNodeHash;
00071     p->pFuncNodeIsConst   = Fra_SmlNodeIsConst;
00072     p->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
00073     return p;
00074 }

void Fra_ClassesStop ( Fra_Cla_t *  p  ) 

Function*************************************************************

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file fraClass.c.

00088 {
00089     FREE( p->pMemClasses );
00090     FREE( p->pMemRepr );
00091     if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
00092     if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
00093     if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
00094     if ( p->vClasses1 )    Vec_PtrFree( p->vClasses1 );
00095     if ( p->vClasses )     Vec_PtrFree( p->vClasses );
00096     if ( p->vImps )        Vec_IntFree( p->vImps );
00097     free( p );
00098 }

void Fra_ClassesTest ( Fra_Cla_t *  p,
int  Id1,
int  Id2 
)

Function*************************************************************

Synopsis [Starts representation of equivalence classes with one class.]

Description []

SideEffects []

SeeAlso []

Definition at line 586 of file fraClass.c.

00587 {
00588     Aig_Obj_t ** pClass;
00589     p->pMemClasses = ALLOC( Aig_Obj_t *, 4 );
00590     pClass = p->pMemClasses;
00591     assert( Id1 < Id2 );
00592     pClass[0] = Aig_ManObj( p->pAig, Id1 );
00593     pClass[1] = Aig_ManObj( p->pAig, Id2 );
00594     pClass[2] = NULL;
00595     pClass[3] = NULL;
00596     Fra_ClassObjSetRepr( pClass[1], pClass[0] );
00597     Vec_PtrPush( p->vClasses, pClass );
00598 }

static Aig_Obj_t* Fra_ObjChild0Equ ( Aig_Obj_t **  ppEquivs,
Aig_Obj_t *  pObj 
) [inline, static]

Definition at line 741 of file fraClass.c.

00741 { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj));  }

static Aig_Obj_t* Fra_ObjChild1Equ ( Aig_Obj_t **  ppEquivs,
Aig_Obj_t *  pObj 
) [inline, static]

Definition at line 742 of file fraClass.c.

00742 { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj));  }

static Aig_Obj_t* Fra_ObjEqu ( Aig_Obj_t **  ppEquivs,
Aig_Obj_t *  pObj 
) [inline, static]

Definition at line 738 of file fraClass.c.

00738 { return ppEquivs[pObj->Id];  }

static Aig_Obj_t* Fra_ObjNext ( Aig_Obj_t **  ppNexts,
Aig_Obj_t *  pObj 
) [inline, static]

CFile****************************************************************

FileName [fraClass.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id
fraClass.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

] DECLARATIONS ///

Definition at line 39 of file fraClass.c.

00039 { return ppNexts[pObj->Id];  }

static void Fra_ObjSetEqu ( Aig_Obj_t **  ppEquivs,
Aig_Obj_t *  pObj,
Aig_Obj_t *  pNode 
) [inline, static]

Definition at line 739 of file fraClass.c.

00739 { ppEquivs[pObj->Id] = pNode; }

static void Fra_ObjSetNext ( Aig_Obj_t **  ppNexts,
Aig_Obj_t *  pObj,
Aig_Obj_t *  pNext 
) [inline, static]

Definition at line 40 of file fraClass.c.

00040 { ppNexts[pObj->Id] = pNext; }

void Fra_PrintClass ( Aig_Obj_t **  pClass  ) 

Function*************************************************************

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 210 of file fraClass.c.

00211 {
00212     Aig_Obj_t * pTemp;
00213     int i;
00214     for ( i = 1; pTemp = pClass[i]; i++ )
00215         assert( Fra_ClassObjRepr(pTemp) == pClass[0] );
00216     printf( "{ " );
00217     for ( i = 0; pTemp = pClass[i]; i++ )
00218         printf( "%d(%d) ", pTemp->Id, pTemp->Level );
00219     printf( "}\n" );
00220 }

int Fra_RefineClassLastIter ( Fra_Cla_t *  p,
Vec_Ptr_t *  vClasses 
)

Function*************************************************************

Synopsis [Iteratively refines the classes after simulation.]

Description [Returns the number of refinements performed.]

SideEffects []

SeeAlso []

Definition at line 453 of file fraClass.c.

00454 {
00455     Aig_Obj_t ** pClass, ** pClass2;
00456     int nRefis;
00457     pClass = Vec_PtrEntryLast( vClasses );
00458     for ( nRefis = 0; pClass2 = Fra_RefineClassOne( p, pClass ); nRefis++ )
00459     {
00460         // if the original class is trivial, remove it
00461         if ( pClass[1] == NULL )
00462             Vec_PtrPop( vClasses );
00463         // if the new class is trivial, stop
00464         if ( pClass2[1] == NULL )
00465         {
00466             nRefis++;
00467             break;
00468         }
00469         // othewise, add the class and continue
00470         assert( pClass2[0] != NULL );
00471         Vec_PtrPush( vClasses, pClass2 );
00472         pClass = pClass2;
00473     }
00474     return nRefis;
00475 }

Aig_Obj_t** Fra_RefineClassOne ( Fra_Cla_t *  p,
Aig_Obj_t **  ppClass 
)

Function*************************************************************

Synopsis [Refines one class using simulation info.]

Description [Returns the new class if refinement happened.]

SideEffects []

SeeAlso []

Definition at line 394 of file fraClass.c.

00395 {
00396     Aig_Obj_t * pObj, ** ppThis;
00397     int i;
00398     assert( ppClass[0] != NULL && ppClass[1] != NULL );
00399 
00400     // check if the class is going to be refined
00401     for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )        
00402         if ( !p->pFuncNodesAreEqual(ppClass[0], pObj) )
00403             break;
00404     if ( pObj == NULL )
00405         return NULL;
00406     // split the class
00407     Vec_PtrClear( p->vClassOld );
00408     Vec_PtrClear( p->vClassNew );
00409     Vec_PtrPush( p->vClassOld, ppClass[0] );
00410     for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )        
00411         if ( p->pFuncNodesAreEqual(ppClass[0], pObj) )
00412             Vec_PtrPush( p->vClassOld, pObj );
00413         else
00414             Vec_PtrPush( p->vClassNew, pObj );
00415 /*
00416     printf( "Refining class (" );
00417     Vec_PtrForEachEntry( p->vClassOld, pObj, i )
00418         printf( "%d,", pObj->Id );
00419     printf( ") + (" );
00420     Vec_PtrForEachEntry( p->vClassNew, pObj, i )
00421         printf( "%d,", pObj->Id );
00422     printf( ")\n" );
00423 */
00424     // put the nodes back into the class memory
00425     Vec_PtrForEachEntry( p->vClassOld, pObj, i )
00426     {
00427         ppClass[i] = pObj;
00428         ppClass[Vec_PtrSize(p->vClassOld)+i] = NULL;
00429         Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
00430     }
00431     ppClass += 2*Vec_PtrSize(p->vClassOld);
00432     // put the new nodes into the class memory
00433     Vec_PtrForEachEntry( p->vClassNew, pObj, i )
00434     {
00435         ppClass[i] = pObj;
00436         ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
00437         Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
00438     }
00439     return ppClass;
00440 }

Generated on Tue Jan 5 12:18:19 2010 for abc70930 by  doxygen 1.6.1