src/opt/rwr/rwrLib.c File Reference

#include "rwr.h"
Include dependency graph for rwrLib.c:

Go to the source code of this file.

Functions

static Rwr_Node_t * Rwr_ManTryNode (Rwr_Man_t *p, Rwr_Node_t *p0, Rwr_Node_t *p1, int fExor, int Level, int Volume)
static void Rwr_MarkUsed_rec (Rwr_Man_t *p, Rwr_Node_t *pNode)
void Rwr_ManPrecompute (Rwr_Man_t *p)
Rwr_Node_t * Rwr_ManAddNode (Rwr_Man_t *p, Rwr_Node_t *p0, Rwr_Node_t *p1, int fExor, int Level, int Volume)
Rwr_Node_t * Rwr_ManAddVar (Rwr_Man_t *p, unsigned uTruth, int fPrecompute)
void Rwr_Trav_rec (Rwr_Man_t *p, Rwr_Node_t *pNode, int *pVolume)
int Rwr_ManNodeVolume (Rwr_Man_t *p, Rwr_Node_t *p0, Rwr_Node_t *p1)
void Rwr_ManIncTravId (Rwr_Man_t *p)

Function Documentation

Rwr_Node_t* Rwr_ManAddNode ( Rwr_Man_t *  p,
Rwr_Node_t *  p0,
Rwr_Node_t *  p1,
int  fExor,
int  Level,
int  Volume 
)

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 203 of file rwrLib.c.

00204 {
00205     Rwr_Node_t * pNew;
00206     unsigned uTruth;
00207     // compute truth table, leve, volume
00208     p->nConsidered++;
00209     if ( fExor )
00210         uTruth = (p0->uTruth ^ p1->uTruth);
00211     else
00212         uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & 
00213                  (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
00214     // create the new node
00215     pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
00216     pNew->Id     = p->vForest->nSize;
00217     pNew->TravId = 0;
00218     pNew->uTruth = uTruth;
00219     pNew->Level  = Level;
00220     pNew->Volume = Volume;
00221     pNew->fUsed  = 0;
00222     pNew->fExor  = fExor;
00223     pNew->p0     = p0;
00224     pNew->p1     = p1;
00225     pNew->pNext  = NULL;
00226     Vec_PtrPush( p->vForest, pNew );
00227     // do not add if the node is not essential
00228     if ( uTruth != p->puCanons[uTruth] )
00229         return pNew;
00230 
00231     // add to the list
00232     p->nAdded++;
00233     if ( p->pTable[uTruth] == NULL )
00234         p->nClasses++;
00235     Rwr_ListAddToTail( p->pTable + uTruth, pNew );
00236     return pNew;
00237 }

Rwr_Node_t* Rwr_ManAddVar ( Rwr_Man_t *  p,
unsigned  uTruth,
int  fPrecompute 
)

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 250 of file rwrLib.c.

00251 {
00252     Rwr_Node_t * pNew;
00253     pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
00254     pNew->Id     = p->vForest->nSize;
00255     pNew->TravId = 0;
00256     pNew->uTruth = uTruth;
00257     pNew->Level  = 0;
00258     pNew->Volume = 0;
00259     pNew->fUsed  = 1;
00260     pNew->fExor  = 0;
00261     pNew->p0     = NULL;
00262     pNew->p1     = NULL;    
00263     pNew->pNext  = NULL;
00264     Vec_PtrPush( p->vForest, pNew );
00265     if ( fPrecompute )
00266         Rwr_ListAddToTail( p->pTable + uTruth, pNew );
00267     return pNew;
00268 }

void Rwr_ManIncTravId ( Rwr_Man_t *  p  ) 

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 347 of file rwrLib.c.

00348 {
00349     Rwr_Node_t * pNode;
00350     int i;
00351     if ( p->nTravIds++ < 0x8FFFFFFF )
00352         return;
00353     Vec_PtrForEachEntry( p->vForest, pNode, i )
00354         pNode->TravId = 0;
00355     p->nTravIds = 1;
00356 }

int Rwr_ManNodeVolume ( Rwr_Man_t *  p,
Rwr_Node_t *  p0,
Rwr_Node_t *  p1 
)

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 327 of file rwrLib.c.

00328 {
00329     int Volume = 0;
00330     Rwr_ManIncTravId( p );
00331     Rwr_Trav_rec( p, p0, &Volume );
00332     Rwr_Trav_rec( p, p1, &Volume );
00333     return Volume;
00334 }

void Rwr_ManPrecompute ( Rwr_Man_t *  p  ) 

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

Synopsis [Precomputes the forest in the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file rwrLib.c.

00046 {
00047     Rwr_Node_t * p0, * p1;
00048     int i, k, Level, Volume;
00049     int LevelOld = -1;
00050     int nNodes;
00051 
00052     Vec_PtrForEachEntryStart( p->vForest, p0, i, 1 )
00053     Vec_PtrForEachEntryStart( p->vForest, p1, k, 1 )
00054     {
00055         if ( LevelOld < (int)p0->Level )
00056         {
00057             LevelOld = p0->Level;
00058             printf( "Starting level %d  (at %d nodes).\n", LevelOld+1, i );
00059             printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
00060                 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
00061         }
00062 
00063         if ( k == i )
00064             break;
00065 //        if ( p0->Level + p1->Level > 6 ) // hard
00066 //            break;
00067 
00068         if ( p0->Level + p1->Level > 5 ) // easy 
00069             break;
00070 
00071 //        if ( p0->Level + p1->Level > 6 || (p0->Level == 3 && p1->Level == 3) )
00072 //            break;
00073 
00074         // compute the level and volume of the new nodes
00075         Level  = 1 + ABC_MAX( p0->Level, p1->Level );
00076         Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
00077         // try four different AND nodes
00078         Rwr_ManTryNode( p,         p0 ,         p1 , 0, Level, Volume );
00079         Rwr_ManTryNode( p, Rwr_Not(p0),         p1 , 0, Level, Volume );
00080         Rwr_ManTryNode( p,         p0 , Rwr_Not(p1), 0, Level, Volume );
00081         Rwr_ManTryNode( p, Rwr_Not(p0), Rwr_Not(p1), 0, Level, Volume );
00082         // try EXOR
00083         Rwr_ManTryNode( p,         p0 ,         p1 , 1, Level, Volume + 1 );
00084         // report the progress
00085         if ( p->nConsidered % 50000000 == 0 )
00086             printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
00087                 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
00088         // quit after some time
00089         if ( p->vForest->nSize == RWR_LIMIT + 5 )
00090         {
00091             printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
00092                 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
00093             goto save;
00094         }
00095     }
00096 save :
00097 
00098     // mark the relevant ones
00099     Rwr_ManIncTravId( p );
00100     k = 5;
00101     nNodes = 0;
00102     Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 )
00103         if ( p0->uTruth == p->puCanons[p0->uTruth] )
00104         {
00105             Rwr_MarkUsed_rec( p, p0 );
00106             nNodes++;
00107         }
00108 
00109     // compact the array by throwing away non-canonical
00110     k = 5;
00111     Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 )
00112         if ( p0->fUsed )
00113         {
00114             p->vForest->pArray[k] = p0;
00115             p0->Id = k++;
00116         }
00117     p->vForest->nSize = k;
00118     printf( "Total canonical = %4d. Total used = %5d.\n", nNodes, p->vForest->nSize );
00119 }

Rwr_Node_t * Rwr_ManTryNode ( Rwr_Man_t *  p,
Rwr_Node_t *  p0,
Rwr_Node_t *  p1,
int  fExor,
int  Level,
int  Volume 
) [static]

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

FileName [rwrLib.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
rwrLib.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] DECLARATIONS ///

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 132 of file rwrLib.c.

00133 {
00134     Rwr_Node_t * pOld, * pNew, ** ppPlace;
00135     unsigned uTruth;
00136     // compute truth table, level, volume
00137     p->nConsidered++;
00138     if ( fExor )
00139     {
00140 //        printf( "Considering EXOR of %d and %d.\n", p0->Id, p1->Id );
00141         uTruth = (p0->uTruth ^ p1->uTruth);
00142     }
00143     else
00144         uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & 
00145                  (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
00146     // skip non-practical classes
00147     if ( Level > 2 && !p->pPractical[p->puCanons[uTruth]] )
00148         return NULL;
00149     // enumerate through the nodes with the same canonical form
00150     ppPlace = p->pTable + uTruth;
00151     for ( pOld = *ppPlace; pOld; ppPlace = &pOld->pNext, pOld = pOld->pNext )
00152     {
00153         if ( pOld->Level <  (unsigned)Level && pOld->Volume < (unsigned)Volume )
00154             return NULL;
00155         if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
00156             return NULL;
00157 //        if ( pOld->Level <  (unsigned)Level && pOld->Volume == (unsigned)Volume )
00158 //            return NULL;
00159     }
00160 /*
00161     // enumerate through the nodes with the opposite polarity
00162     for ( pOld = p->pTable[~uTruth & 0xFFFF]; pOld; pOld = pOld->pNext )
00163     {
00164         if ( pOld->Level <  (unsigned)Level && pOld->Volume < (unsigned)Volume )
00165             return NULL;
00166         if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
00167             return NULL;
00168 //        if ( pOld->Level <  (unsigned)Level && pOld->Volume == (unsigned)Volume )
00169 //            return NULL;
00170     }
00171 */
00172     // count the classes
00173     if ( p->pTable[uTruth] == NULL && p->puCanons[uTruth] == uTruth )
00174         p->nClasses++;
00175     // create the new node
00176     pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
00177     pNew->Id     = p->vForest->nSize;
00178     pNew->TravId = 0;
00179     pNew->uTruth = uTruth;
00180     pNew->Level  = Level;
00181     pNew->Volume = Volume;
00182     pNew->fUsed  = 0;
00183     pNew->fExor  = fExor;
00184     pNew->p0     = p0;
00185     pNew->p1     = p1;
00186     pNew->pNext  = NULL;
00187     Vec_PtrPush( p->vForest, pNew );
00188     *ppPlace     = pNew;
00189     return pNew;
00190 }

void Rwr_MarkUsed_rec ( Rwr_Man_t *  p,
Rwr_Node_t *  pNode 
) [static]

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 283 of file rwrLib.c.

00284 {
00285     if ( pNode->fUsed || pNode->TravId == p->nTravIds )
00286         return;
00287     pNode->TravId = p->nTravIds;
00288     pNode->fUsed = 1;
00289     Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p0) );
00290     Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p1) );
00291 }

void Rwr_Trav_rec ( Rwr_Man_t *  p,
Rwr_Node_t *  pNode,
int *  pVolume 
)

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 304 of file rwrLib.c.

00305 {
00306     if ( pNode->fUsed || pNode->TravId == p->nTravIds )
00307         return;
00308     pNode->TravId = p->nTravIds;
00309     (*pVolume)++;
00310     if ( pNode->fExor )
00311         (*pVolume)++;
00312     Rwr_Trav_rec( p, Rwr_Regular(pNode->p0), pVolume );
00313     Rwr_Trav_rec( p, Rwr_Regular(pNode->p1), pVolume );
00314 }

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