#include "base/abc/abc.h"
#include "opt/cut/cut.h"

Data Structures
struct	Rwr_Man_t_

struct	Rwr_Node_t_

Macros
#define	RWR_LIMIT 1048576/4
	INCLUDES ///. More...

Typedefs
typedef struct Rwr_Man_t_	Rwr_Man_t

typedef struct Rwr_Node_t_	Rwr_Node_t

Functions
static int	Rwr_IsComplement (Rwr_Node_t *p)

static Rwr_Node_t *	Rwr_Regular (Rwr_Node_t *p)

static Rwr_Node_t *	Rwr_Not (Rwr_Node_t *p)

static Rwr_Node_t *	Rwr_NotCond (Rwr_Node_t *p, int c)

void	Rwr_ManPreprocess (Rwr_Man_t *p)
	MACRO DEFINITIONS ///. More...

int	Rwr_NodeRewrite (Rwr_Man_t p, Cut_Man_t pManCut, Abc_Obj_t *pNode, int fUpdateLevel, int fUseZeros, int fPlaceEnable)
	FUNCTION DEFINITIONS ///. More...

void	Rwr_ScoresClean (Rwr_Man_t *p)

void	Rwr_ScoresReport (Rwr_Man_t *p)

void	Rwr_ManPrecompute (Rwr_Man_t *p)
	FUNCTION DEFINITIONS ///. More...

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

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

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

void	Rwr_ManIncTravId (Rwr_Man_t *p)

Rwr_Man_t *	Rwr_ManStart (int fPrecompute)
	DECLARATIONS ///. More...

void	Rwr_ManStop (Rwr_Man_t *p)

void	Rwr_ManPrintStats (Rwr_Man_t *p)

void	Rwr_ManPrintStatsFile (Rwr_Man_t *p)

void *	Rwr_ManReadDecs (Rwr_Man_t *p)

Vec_Ptr_t *	Rwr_ManReadLeaves (Rwr_Man_t *p)

int	Rwr_ManReadCompl (Rwr_Man_t *p)

void	Rwr_ManAddTimeCuts (Rwr_Man_t *p, abctime Time)

void	Rwr_ManAddTimeUpdate (Rwr_Man_t *p, abctime Time)

void	Rwr_ManAddTimeTotal (Rwr_Man_t *p, abctime Time)

void	Rwr_ManPrint (Rwr_Man_t *p)

void	Rwr_ManWriteToArray (Rwr_Man_t *p)
	FUNCTION DEFINITIONS ///. More...

void	Rwr_ManLoadFromArray (Rwr_Man_t *p, int fVerbose)

void	Rwr_ManWriteToFile (Rwr_Man_t p, char pFileName)

void	Rwr_ManLoadFromFile (Rwr_Man_t p, char pFileName)

void	Rwr_ListAddToTail (Rwr_Node_t *ppList, Rwr_Node_t pNode)

char *	Rwr_ManGetPractical (Rwr_Man_t *p)

Macro Definition Documentation

#define RWR_LIMIT 1048576/4

INCLUDES ///.

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

FileName [rwr.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:: rwr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 45 of file rwr.h.

Typedef Documentation

typedef struct Rwr_Man_t_ Rwr_Man_t

Definition at line 47 of file rwr.h.

typedef struct Rwr_Node_t_ Rwr_Node_t

Definition at line 48 of file rwr.h.

Function Documentation

static int Rwr_IsComplement ( Rwr_Node_t * p )

inlinestatic

Definition at line 116 of file rwr.h.

116 { return (int )(((ABC_PTRUINT_T)p) & 01); }

void Rwr_ListAddToTail	(	Rwr_Node_t **	ppList,
		Rwr_Node_t *	pNode
	)

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

Synopsis [Adds the node to the end of the list.]

Description []

SideEffects []

SeeAlso []

Definition at line 619 of file rwrUtil.c.

 {
     Rwr_Node_t * pTemp;
     // find the last one
     for ( pTemp = *ppList; pTemp; pTemp = pTemp->pNext )
         ppList = &pTemp->pNext;
     // attach at the end
     *ppList = pNode;
 }

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 206 of file rwrLib.c.

 {
     Rwr_Node_t * pNew;
     unsigned uTruth;
     // compute truth table, leve, volume
     p->nConsidered++;
     if ( fExor )
         uTruth = (p0->uTruth ^ p1->uTruth);
     else
         uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & 
                  (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
     // create the new node
     pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
     pNew->Id     = p->vForest->nSize;
     pNew->TravId = 0;
     pNew->uTruth = uTruth;
     pNew->Level  = Level;
     pNew->Volume = Volume;
     pNew->fUsed  = 0;
     pNew->fExor  = fExor;
     pNew->p0     = p0;
     pNew->p1     = p1;
     pNew->pNext  = NULL;
     Vec_PtrPush( p->vForest, pNew );
     // do not add if the node is not essential
     if ( uTruth != p->puCanons[uTruth] )
         return pNew;
 
     // add to the list
     p->nAdded++;
     if ( p->pTable[uTruth] == NULL )
         p->nClasses++;
     Rwr_ListAddToTail( p->pTable + uTruth, pNew );
     return pNew;
 }

void Rwr_ManAddTimeCuts	(	Rwr_Man_t *	p,
		abctime	Time
	)

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

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 261 of file rwrMan.c.

 {
     p->timeCut += Time;
 }

void Rwr_ManAddTimeTotal	(	Rwr_Man_t *	p,
		abctime	Time
	)

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

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 293 of file rwrMan.c.

 {
     p->timeTotal += Time;
 }

void Rwr_ManAddTimeUpdate	(	Rwr_Man_t *	p,
		abctime	Time
	)

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

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 277 of file rwrMan.c.

 {
     p->timeUpdate += Time;
 }

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

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 253 of file rwrLib.c.

 {
     Rwr_Node_t * pNew;
     pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
     pNew->Id     = p->vForest->nSize;
     pNew->TravId = 0;
     pNew->uTruth = uTruth;
     pNew->Level  = 0;
     pNew->Volume = 0;
     pNew->fUsed  = 1;
     pNew->fExor  = 0;
     pNew->p0     = NULL;
     pNew->p1     = NULL;    
     pNew->pNext  = NULL;
     Vec_PtrPush( p->vForest, pNew );
     if ( fPrecompute )
         Rwr_ListAddToTail( p->pTable + uTruth, pNew );
     return pNew;
 }

char* Rwr_ManGetPractical ( Rwr_Man_t * p )

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

Synopsis [Create practical classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 640 of file rwrUtil.c.

 {
     char * pPractical;
     int i;
     pPractical = ABC_ALLOC( char, p->nFuncs );
     memset( pPractical, 0, sizeof(char) * p->nFuncs );
     pPractical[0] = 1;
     for ( i = 1; ; i++ )
     {
         if ( s_RwrPracticalClasses[i] == 0 )
             break;
         pPractical[ s_RwrPracticalClasses[i] ] = 1;
     }
     return pPractical;
 }

void Rwr_ManIncTravId ( Rwr_Man_t * p )

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

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file rwrLib.c.

 {
     Rwr_Node_t * pNode;
     int i;
     if ( p->nTravIds++ < 0x8FFFFFFF )
         return;
     Vec_PtrForEachEntry( Rwr_Node_t *, p->vForest, pNode, i )
         pNode->TravId = 0;
     p->nTravIds = 1;
 }

void Rwr_ManLoadFromArray	(	Rwr_Man_t *	p,
		int	fVerbose
	)

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

Synopsis [Loads data.]

Description []

SideEffects []

SeeAlso []

Definition at line 472 of file rwrUtil.c.

 {
     unsigned short * pArray = s_RwtAigSubgraphs;
     Rwr_Node_t * p0, * p1;
     unsigned Entry0, Entry1;
     int Level, Volume, nEntries, fExor;
     int i;
     abctime clk = Abc_Clock();
 
     // reconstruct the forest
     for ( i = 0; ; i++ )
     {
         Entry0 = pArray[2*i + 0];
         Entry1 = pArray[2*i + 1];
         if ( Entry0 == 0 && Entry1 == 0 )
             break;
         // get EXOR flag
         fExor = (Entry0 & 1);
         Entry0 >>= 1;
         // get the nodes
         p0 = (Rwr_Node_t *)p->vForest->pArray[Entry0 >> 1];
         p1 = (Rwr_Node_t *)p->vForest->pArray[Entry1 >> 1];
         // compute the level and volume of the new nodes
         Level  = 1 + Abc_MaxInt( p0->Level, p1->Level );
         Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
         // set the complemented attributes
         p0 = Rwr_NotCond( p0, (Entry0 & 1) );
         p1 = Rwr_NotCond( p1, (Entry1 & 1) );
         // add the node
 //        Rwr_ManTryNode( p, p0, p1, Level, Volume );
         Rwr_ManAddNode( p, p0, p1, fExor, Level, Volume + fExor );
     }
     nEntries = i - 1;
     if ( fVerbose )
     {
         printf( "The number of classes = %d. Canonical nodes = %d.\n", p->nClasses, p->nAdded );
         printf( "The number of nodes loaded = %d.  ", nEntries );  ABC_PRT( "Loading", Abc_Clock() - clk );
     }
 }

void Rwr_ManLoadFromFile	(	Rwr_Man_t *	p,
		char *	pFileName
	)

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

Synopsis [Loads data.]

Description []

SideEffects []

SeeAlso []

Definition at line 562 of file rwrUtil.c.

 {
     FILE * pFile;
     Rwr_Node_t * p0, * p1;
     unsigned * pBuffer;
     int Level, Volume, nEntries, fExor;
     int i;
     abctime clk = Abc_Clock();
     int RetValue;
 
     // load the data
     pFile = fopen( pFileName, "rb" );
     if ( pFile == NULL )
     {
         printf( "Rwr_ManLoadFromFile: Cannot open file \"%s\".\n", pFileName );
         return;
     }
     RetValue = fread( &nEntries, sizeof(int), 1, pFile );
     pBuffer = ABC_ALLOC( unsigned, nEntries * 2 );
     RetValue = fread( pBuffer, sizeof(unsigned), nEntries * 2, pFile );
     fclose( pFile );
     // reconstruct the forest
     for ( i = 0; i < nEntries; i++ )
     {
         // get EXOR flag
         fExor = (pBuffer[2*i + 0] & 1);
         pBuffer[2*i + 0] = (pBuffer[2*i + 0] >> 1);
         // get the nodes
         p0 = (Rwr_Node_t *)p->vForest->pArray[pBuffer[2*i + 0] >> 1];
         p1 = (Rwr_Node_t *)p->vForest->pArray[pBuffer[2*i + 1] >> 1];
         // compute the level and volume of the new nodes
         Level  = 1 + Abc_MaxInt( p0->Level, p1->Level );
         Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
         // set the complemented attributes
         p0 = Rwr_NotCond( p0, (pBuffer[2*i + 0] & 1) );
         p1 = Rwr_NotCond( p1, (pBuffer[2*i + 1] & 1) );
         // add the node
 //        Rwr_ManTryNode( p, p0, p1, Level, Volume );
         Rwr_ManAddNode( p, p0, p1, fExor, Level, Volume + fExor );
     }
     ABC_FREE( pBuffer );
     printf( "The number of classes = %d. Canonical nodes = %d.\n", p->nClasses, p->nAdded );
     printf( "The number of nodes loaded = %d.   ", nEntries );  ABC_PRT( "Loading", Abc_Clock() - clk );
 }

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 330 of file rwrLib.c.

 {
     int Volume = 0;
     Rwr_ManIncTravId( p );
     Rwr_Trav_rec( p, p0, &Volume );
     Rwr_Trav_rec( p, p1, &Volume );
     return Volume;
 }

void Rwr_ManPrecompute ( Rwr_Man_t * p )

FUNCTION DEFINITIONS ///.

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

Synopsis [Precomputes the forest in the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file rwrLib.c.

 {
     Rwr_Node_t * p0, * p1;
     int i, k, Level, Volume;
     int LevelOld = -1;
     int nNodes;
 
     Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p0, i, 1 )
     Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p1, k, 1 )
     {
         if ( LevelOld < (int)p0->Level )
         {
             LevelOld = p0->Level;
             printf( "Starting level %d  (at %d nodes).\n", LevelOld+1, i );
             printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
                 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
         }
 
         if ( k == i )
             break;
 //        if ( p0->Level + p1->Level > 6 ) // hard
 //            break;
 
         if ( p0->Level + p1->Level > 5 ) // easy 
             break;
 
 //        if ( p0->Level + p1->Level > 6 || (p0->Level == 3 && p1->Level == 3) )
 //            break;
 
         // compute the level and volume of the new nodes
         Level  = 1 + Abc_MaxInt( p0->Level, p1->Level );
         Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
         // try four different AND nodes
         Rwr_ManTryNode( p,         p0 ,         p1 , 0, Level, Volume );
         Rwr_ManTryNode( p, Rwr_Not(p0),         p1 , 0, Level, Volume );
         Rwr_ManTryNode( p,         p0 , Rwr_Not(p1), 0, Level, Volume );
         Rwr_ManTryNode( p, Rwr_Not(p0), Rwr_Not(p1), 0, Level, Volume );
         // try EXOR
         Rwr_ManTryNode( p,         p0 ,         p1 , 1, Level, Volume + 1 );
         // report the progress
         if ( p->nConsidered % 50000000 == 0 )
             printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
                 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
         // quit after some time
         if ( p->vForest->nSize == RWR_LIMIT + 5 )
         {
             printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
                 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
             goto save;
         }
     }
 save :
 
     // mark the relevant ones
     Rwr_ManIncTravId( p );
     k = 5;
     nNodes = 0;
     Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p0, i, 5 )
         if ( p0->uTruth == p->puCanons[p0->uTruth] )
         {
             Rwr_MarkUsed_rec( p, p0 );
             nNodes++;
         }
 
     // compact the array by throwing away non-canonical
     k = 5;
     Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p0, i, 5 )
         if ( p0->fUsed )
         {
             p->vForest->pArray[k] = p0;
             p0->Id = k++;
         }
     p->vForest->nSize = k;
     printf( "Total canonical = %4d. Total used = %5d.\n", nNodes, p->vForest->nSize );
 }

void Rwr_ManPreprocess ( Rwr_Man_t * p )

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

MACRO DEFINITIONS ///.

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

Synopsis [Preprocesses computed library of subgraphs.]

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file rwrDec.c.

 {
     Dec_Graph_t * pGraph;
     Rwr_Node_t * pNode;
     int i, k;
     // put the nodes into the structure
     p->pMapInv  = ABC_ALLOC( unsigned short, 222 );
     memset( p->pMapInv, 0, sizeof(unsigned short) * 222 );
     p->vClasses = Vec_VecStart( 222 );
     for ( i = 0; i < p->nFuncs; i++ )
     {
         if ( p->pTable[i] == NULL )
             continue;
         // consider all implementations of this function
         for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
         {
             assert( pNode->uTruth == p->pTable[i]->uTruth );
             assert( p->pMap[pNode->uTruth] < 222 ); // Guaranteed to be >=0 b/c unsigned
             Vec_VecPush( p->vClasses, p->pMap[pNode->uTruth], pNode );
             p->pMapInv[ p->pMap[pNode->uTruth] ] = p->puCanons[pNode->uTruth];
         }
     }
     // compute decomposition forms for each node and verify them
     Vec_VecForEachEntry( Rwr_Node_t *, p->vClasses, pNode, i, k )
     {
         pGraph = Rwr_NodePreprocess( p, pNode );
         pNode->pNext = (Rwr_Node_t *)pGraph;
         assert( pNode->uTruth == (Dec_GraphDeriveTruth(pGraph) & 0xFFFF) );
     }
 }

void Rwr_ManPrint ( Rwr_Man_t * p )

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

Synopsis [Prints one rwr node.]

Description []

SideEffects []

SeeAlso []

Definition at line 237 of file rwrPrint.c.

 {
     FILE * pFile;
     Rwr_Node_t * pNode;
     unsigned uTruth;
     int Limit, Counter, Volume, nFuncs, i;
     pFile = fopen( "graph_lib.txt", "w" );
     Counter = 0;
     Limit = (1 << 16);
     for ( i = 0; i < Limit; i++ )
     {
         if ( p->pTable[i] == NULL )
             continue;
         if ( i != p->puCanons[i] )
             continue;
         fprintf( pFile, "\nClass %3d. Func %6d.  ", p->pMap[i], Counter++ );
         Rwr_GetBushVolume( p, i, &Volume, &nFuncs );
         fprintf( pFile, "Roots = %3d. Vol = %3d. Sum = %3d.  ", nFuncs, Volume, Rwr_GetBushSumOfVolumes(p, i) );
         uTruth = i;
         Extra_PrintBinary( pFile, &uTruth, 16 );
         fprintf( pFile, "\n" );
         for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
             if ( pNode->uTruth == p->puCanons[pNode->uTruth] )
                 Rwr_NodePrint( pFile, p, pNode );
     }
     fclose( pFile );
 }

void Rwr_ManPrintStats ( Rwr_Man_t * p )

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

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 143 of file rwrMan.c.

 {
     int i, Counter = 0;
     for ( i = 0; i < 222; i++ )
         Counter += (p->nScores[i] > 0);
 
     printf( "Rewriting statistics:\n" );
     printf( "Total cuts tries  = %8d.\n", p->nCutsGood );
     printf( "Bad cuts found    = %8d.\n", p->nCutsBad );
     printf( "Total subgraphs   = %8d.\n", p->nSubgraphs );
     printf( "Used NPN classes  = %8d.\n", Counter );
     printf( "Nodes considered  = %8d.\n", p->nNodesConsidered );
     printf( "Nodes rewritten   = %8d.\n", p->nNodesRewritten );
     printf( "Gain              = %8d. (%6.2f %%).\n", p->nNodesBeg-p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg );
     ABC_PRT( "Start       ", p->timeStart );
     ABC_PRT( "Cuts        ", p->timeCut );
     ABC_PRT( "Resynthesis ", p->timeRes );
     ABC_PRT( "    Mffc    ", p->timeMffc );
     ABC_PRT( "    Eval    ", p->timeEval );
     ABC_PRT( "Update      ", p->timeUpdate );
     ABC_PRT( "TOTAL       ", p->timeTotal );
 
 /*
     printf( "The scores are:\n" );
     for ( i = 0; i < 222; i++ )
         if ( p->nScores[i] > 0 )
         {
             extern void Ivy_TruthDsdComputePrint( unsigned uTruth );
             printf( "%3d = %8d  canon = %5d  ", i, p->nScores[i], p->pMapInv[i] );
             Ivy_TruthDsdComputePrint( (unsigned)p->pMapInv[i] | ((unsigned)p->pMapInv[i] << 16) );
         }
 */
     printf( "\n" );
 
 }

void Rwr_ManPrintStatsFile ( Rwr_Man_t * p )

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

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 190 of file rwrMan.c.

 {
     FILE * pTable;
     pTable = fopen( "stats.txt", "a+" );
     fprintf( pTable, "%d ", p->nCutsGood );
     fprintf( pTable, "%d ", p->nSubgraphs );
     fprintf( pTable, "%d ", p->nNodesRewritten );
     fprintf( pTable, "%d", p->nNodesGained );
     fprintf( pTable, "\n" );
     fclose( pTable );
 }

int Rwr_ManReadCompl ( Rwr_Man_t * p )

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

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 245 of file rwrMan.c.

 {
     return p->fCompl;
 }

void* Rwr_ManReadDecs ( Rwr_Man_t * p )

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

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 213 of file rwrMan.c.

 {
     return p->pGraph;
 }

Vec_Ptr_t* Rwr_ManReadLeaves ( Rwr_Man_t * p )

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

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 229 of file rwrMan.c.

 {
     return p->vFanins;
 }

Rwr_Man_t* Rwr_ManStart ( int fPrecompute )

DECLARATIONS ///.

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

FileName [rwrMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting package.]

Synopsis [Rewriting manager.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

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

Synopsis [Starts rewriting manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file rwrMan.c.

 {
     Dec_Man_t * pManDec;
     Rwr_Man_t * p;
     abctime clk = Abc_Clock();
 clk = Abc_Clock();
     p = ABC_ALLOC( Rwr_Man_t, 1 );
     memset( p, 0, sizeof(Rwr_Man_t) );
     p->nFuncs = (1<<16);
     pManDec   = (Dec_Man_t *)Abc_FrameReadManDec();
     p->puCanons = pManDec->puCanons; 
     p->pPhases  = pManDec->pPhases; 
     p->pPerms   = pManDec->pPerms; 
     p->pMap     = pManDec->pMap; 
     // initialize practical NPN classes
     p->pPractical  = Rwr_ManGetPractical( p );
     // create the table
     p->pTable = ABC_ALLOC( Rwr_Node_t *, p->nFuncs );
     memset( p->pTable, 0, sizeof(Rwr_Node_t *) * p->nFuncs );
     // create the elementary nodes
     p->pMmNode  = Extra_MmFixedStart( sizeof(Rwr_Node_t) );
     p->vForest  = Vec_PtrAlloc( 100 );
     Rwr_ManAddVar( p, 0x0000, fPrecompute ); // constant 0
     Rwr_ManAddVar( p, 0xAAAA, fPrecompute ); // var A
     Rwr_ManAddVar( p, 0xCCCC, fPrecompute ); // var B
     Rwr_ManAddVar( p, 0xF0F0, fPrecompute ); // var C
     Rwr_ManAddVar( p, 0xFF00, fPrecompute ); // var D
     p->nClasses = 5;
     // other stuff
     p->nTravIds   = 1;
     p->pPerms4    = Extra_Permutations( 4 );
     p->vLevNums   = Vec_IntAlloc( 50 );
     p->vFanins    = Vec_PtrAlloc( 50 );
     p->vFaninsCur = Vec_PtrAlloc( 50 );
     p->vNodesTemp = Vec_PtrAlloc( 50 );
     if ( fPrecompute )
     {   // precompute subgraphs
         Rwr_ManPrecompute( p );
 //        Rwr_ManPrint( p );
         Rwr_ManWriteToArray( p );
     }
     else
     {   // load saved subgraphs
         Rwr_ManLoadFromArray( p, 0 );
 //        Rwr_ManPrint( p );
         Rwr_ManPreprocess( p );
     }
 p->timeStart = Abc_Clock() - clk;
     return p;
 }

void Rwr_ManStop ( Rwr_Man_t * p )

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

Synopsis [Stops rewriting manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 109 of file rwrMan.c.

 {
     if ( p->vClasses )
     {
         Rwr_Node_t * pNode;
         int i, k;
         Vec_VecForEachEntry( Rwr_Node_t *, p->vClasses, pNode, i, k )
             Dec_GraphFree( (Dec_Graph_t *)pNode->pNext );
     }
     if ( p->vClasses )  Vec_VecFree( p->vClasses );
     Vec_PtrFree( p->vNodesTemp );
     Vec_PtrFree( p->vForest );
     Vec_IntFree( p->vLevNums );
     Vec_PtrFree( p->vFanins );
     Vec_PtrFree( p->vFaninsCur );
     Extra_MmFixedStop( p->pMmNode );
     ABC_FREE( p->pMapInv );
     ABC_FREE( p->pTable );
     ABC_FREE( p->pPractical );
     ABC_FREE( p->pPerms4 );
     ABC_FREE( p );
 }

void Rwr_ManWriteToArray ( Rwr_Man_t * p )

FUNCTION DEFINITIONS ///.

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

Synopsis [Writes data.]

Description []

SideEffects []

SeeAlso []

Definition at line 426 of file rwrUtil.c.

 {
     FILE * pFile;
     Rwr_Node_t * pNode;
     unsigned Entry0, Entry1;
     int i, nEntries;
     abctime clk = Abc_Clock();
     // prepare the buffer
     nEntries = p->vForest->nSize - 5;
     pFile = fopen( "npn4_aig_array.txt", "w" );
     fprintf( pFile, "static unsigned short s_RwtAigSubgraphs[] = \n{" );
     for ( i = 0; i < nEntries; i++ )
     {
         if ( i % 5 == 0 )
             fprintf( pFile, "\n    " );
         pNode = (Rwr_Node_t *)p->vForest->pArray[i+5];
         Entry0 = (Rwr_Regular(pNode->p0)->Id << 1) | Rwr_IsComplement(pNode->p0);
         Entry1 = (Rwr_Regular(pNode->p1)->Id << 1) | Rwr_IsComplement(pNode->p1);
         Entry0 = (Entry0 << 1) | pNode->fExor;
         Extra_PrintHex( pFile, &Entry0, 4 );
         fprintf( pFile, "," );
         Extra_PrintHex( pFile, &Entry1, 4 );
         fprintf( pFile, ", " );
     }
     if ( i % 5 == 0 )
         fprintf( pFile, "\n    " );
     Entry0 = 0;
     Extra_PrintHex( pFile, &Entry0, 4 );
     fprintf( pFile, "," );
     Extra_PrintHex( pFile, &Entry0, 4 );
     fprintf( pFile, " \n};\n" );
     fclose( pFile );
     printf( "The number of nodes saved = %d.   ", nEntries );  ABC_PRT( "Saving", Abc_Clock() - clk );
 }

void Rwr_ManWriteToFile	(	Rwr_Man_t *	p,
		char *	pFileName
	)

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

Synopsis [Writes.]

Description []

SideEffects []

SeeAlso []

Definition at line 524 of file rwrUtil.c.

 {
     FILE * pFile;
     Rwr_Node_t * pNode;
     unsigned * pBuffer;
     int i, nEntries;
     abctime clk = Abc_Clock();
     // prepare the buffer
     nEntries = p->vForest->nSize - 5;
     pBuffer = ABC_ALLOC( unsigned, nEntries * 2 );
     for ( i = 0; i < nEntries; i++ )
     {
         pNode = (Rwr_Node_t *)p->vForest->pArray[i+5];
         pBuffer[2*i + 0] = (Rwr_Regular(pNode->p0)->Id << 1) | Rwr_IsComplement(pNode->p0);
         pBuffer[2*i + 1] = (Rwr_Regular(pNode->p1)->Id << 1) | Rwr_IsComplement(pNode->p1);
         // save EXOR flag
         pBuffer[2*i + 0] = (pBuffer[2*i + 0] << 1) | pNode->fExor;
 
     }
     pFile = fopen( pFileName, "wb" );
     fwrite( &nEntries, sizeof(int), 1, pFile );
     fwrite( pBuffer, sizeof(unsigned), nEntries * 2, pFile );
     ABC_FREE( pBuffer );
     fclose( pFile );
     printf( "The number of nodes saved = %d.   ", nEntries );  ABC_PRT( "Saving", Abc_Clock() - clk );
 }

int Rwr_NodeRewrite	(	Rwr_Man_t *	p,
		Cut_Man_t *	pManCut,
		Abc_Obj_t *	pNode,
		int	fUpdateLevel,
		int	fUseZeros,
		int	fPlaceEnable
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Performs rewriting for one node.]

Description [This procedure considers all the cuts computed for the node and tries to rewrite each of them using the "forest" of different AIG structures precomputed and stored in the RWR manager. Determines the best rewriting and computes the gain in the number of AIG nodes in the final network. In the end, p->vFanins contains information about the best cut that can be used for rewriting, while p->pGraph gives the decomposition dag (represented using decomposition graph data structure). Returns gain in the number of nodes or -1 if node cannot be rewritten.]

SideEffects []

SeeAlso []

Definition at line 59 of file rwrEva.c.

 {
     int fVeryVerbose = 0;
     Dec_Graph_t * pGraph;
     Cut_Cut_t * pCut;//, * pTemp;
     Abc_Obj_t * pFanin;
     unsigned uPhase;
     unsigned uTruthBest = 0; // Suppress "might be used uninitialized"
     unsigned uTruth;
     char * pPerm;
     int Required, nNodesSaved;
     int nNodesSaveCur = -1; // Suppress "might be used uninitialized"
     int i, GainCur = -1, GainBest = -1;
     abctime clk, clk2;//, Counter;
 
     p->nNodesConsidered++;
     // get the required times
     Required = fUpdateLevel? Abc_ObjRequiredLevel(pNode) : ABC_INFINITY;
 
     // get the node's cuts
 clk = Abc_Clock();
     pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode, 0, 0 );
     assert( pCut != NULL );
 p->timeCut += Abc_Clock() - clk;
 
 //printf( " %d", Rwr_CutCountNumNodes(pNode, pCut) );
 /*
     Counter = 0;
     for ( pTemp = pCut->pNext; pTemp; pTemp = pTemp->pNext )
         Counter++;
     printf( "%d ", Counter );
 */
     // go through the cuts
 clk = Abc_Clock();
     for ( pCut = pCut->pNext; pCut; pCut = pCut->pNext )
     {
         // consider only 4-input cuts
         if ( pCut->nLeaves < 4 )
             continue;
 //            Cut_CutPrint( pCut, 0 ), printf( "\n" );
 
         // get the fanin permutation
         uTruth = 0xFFFF & *Cut_CutReadTruth(pCut);
         pPerm = p->pPerms4[ (int)p->pPerms[uTruth] ];
         uPhase = p->pPhases[uTruth];
         // collect fanins with the corresponding permutation/phase
         Vec_PtrClear( p->vFaninsCur );
         Vec_PtrFill( p->vFaninsCur, (int)pCut->nLeaves, 0 );
         for ( i = 0; i < (int)pCut->nLeaves; i++ )
         {
             pFanin = Abc_NtkObj( pNode->pNtk, pCut->pLeaves[(int)pPerm[i]] );
             if ( pFanin == NULL )
                 break;
             pFanin = Abc_ObjNotCond(pFanin, ((uPhase & (1<<i)) > 0) );
             Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin );
         }
         if ( i != (int)pCut->nLeaves )
         {
             p->nCutsBad++;
             continue;
         }
         p->nCutsGood++;
 
         {
             int Counter = 0;
             Vec_PtrForEachEntry( Abc_Obj_t *, p->vFaninsCur, pFanin, i )
                 if ( Abc_ObjFanoutNum(Abc_ObjRegular(pFanin)) == 1 )
                     Counter++;
             if ( Counter > 2 )
                 continue;
         }
 
 clk2 = Abc_Clock();
 /*
         printf( "Considering: (" );
         Vec_PtrForEachEntry( Abc_Obj_t *, p->vFaninsCur, pFanin, i )
             printf( "%d ", Abc_ObjFanoutNum(Abc_ObjRegular(pFanin)) );
         printf( ")\n" );
 */
         // mark the fanin boundary 
         Vec_PtrForEachEntry( Abc_Obj_t *, p->vFaninsCur, pFanin, i )
             Abc_ObjRegular(pFanin)->vFanouts.nSize++;
 
         // label MFFC with current ID
         Abc_NtkIncrementTravId( pNode->pNtk );
         nNodesSaved = Abc_NodeMffcLabelAig( pNode );
         // unmark the fanin boundary
         Vec_PtrForEachEntry( Abc_Obj_t *, p->vFaninsCur, pFanin, i )
             Abc_ObjRegular(pFanin)->vFanouts.nSize--;
 p->timeMffc += Abc_Clock() - clk2;
 
         // evaluate the cut
 clk2 = Abc_Clock();
         pGraph = Rwr_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, fPlaceEnable );
 p->timeEval += Abc_Clock() - clk2;
 
         // check if the cut is better than the current best one
         if ( pGraph != NULL && GainBest < GainCur )
         {
             // save this form
             nNodesSaveCur = nNodesSaved;
             GainBest  = GainCur;
             p->pGraph  = pGraph;
             p->fCompl = ((uPhase & (1<<4)) > 0);
             uTruthBest = 0xFFFF & *Cut_CutReadTruth(pCut);
             // collect fanins in the
             Vec_PtrClear( p->vFanins );
             Vec_PtrForEachEntry( Abc_Obj_t *, p->vFaninsCur, pFanin, i )
                 Vec_PtrPush( p->vFanins, pFanin );
         }
     }
 p->timeRes += Abc_Clock() - clk;
 
     if ( GainBest == -1 )
         return -1;
 /*
     if ( GainBest > 0 )
     {
         printf( "Class %d  ", p->pMap[uTruthBest] );
         printf( "Gain = %d. Node %d : ", GainBest, pNode->Id );
         Vec_PtrForEachEntry( Abc_Obj_t *, p->vFanins, pFanin, i )
             printf( "%d ", Abc_ObjRegular(pFanin)->Id );
         Dec_GraphPrint( stdout, p->pGraph, NULL, NULL );
         printf( "\n" );
     }
 */
 
 //    printf( "%d", nNodesSaveCur - GainBest );
 /*
     if ( GainBest > 0 )
     {
         if ( Rwr_CutIsBoolean( pNode, p->vFanins ) )
             printf( "b" );
         else
         {
             printf( "Node %d : ", pNode->Id );
             Vec_PtrForEachEntry( Abc_Obj_t *, p->vFanins, pFanin, i )
                 printf( "%d ", Abc_ObjRegular(pFanin)->Id );
             printf( "a" );
         }
     }
 */
 /*
     if ( GainBest > 0 )
         if ( p->fCompl )
             printf( "c" );
         else
             printf( "." );
 */
 
     // copy the leaves
     Vec_PtrForEachEntry( Abc_Obj_t *, p->vFanins, pFanin, i )
         Dec_GraphNode((Dec_Graph_t *)p->pGraph, i)->pFunc = pFanin;
 /*
     printf( "(" );
     Vec_PtrForEachEntry( Abc_Obj_t *, p->vFanins, pFanin, i )
         printf( " %d", Abc_ObjRegular(pFanin)->vFanouts.nSize - 1 );
     printf( " )  " );
 */
 //    printf( "%d ", Rwr_NodeGetDepth_rec( pNode, p->vFanins ) );
 
     p->nScores[p->pMap[uTruthBest]]++;
     p->nNodesGained += GainBest;
     if ( fUseZeros || GainBest > 0 )
     {
         p->nNodesRewritten++;
     }
 
     // report the progress
     if ( fVeryVerbose && GainBest > 0 )
     {
         printf( "Node %6s :   ", Abc_ObjName(pNode) );
         printf( "Fanins = %d. ", p->vFanins->nSize );
         printf( "Save = %d.  ", nNodesSaveCur );
         printf( "Add = %d.  ",  nNodesSaveCur-GainBest );
         printf( "GAIN = %d.  ", GainBest );
         printf( "Cone = %d.  ", p->pGraph? Dec_GraphNodeNum((Dec_Graph_t *)p->pGraph) : 0 );
         printf( "Class = %d.  ", p->pMap[uTruthBest] );
         printf( "\n" );
     }
     return GainBest;
 }

static Rwr_Node_t* Rwr_Not ( Rwr_Node_t * p )

inlinestatic

Definition at line 118 of file rwr.h.

118 { return (Rwr_Node_t *)((ABC_PTRUINT_T)(p) ^ 01); }

Rwr_Node_t_

Definition: rwr.h:98

static Rwr_Node_t* Rwr_NotCond	(	Rwr_Node_t *	p,
		int	c
	)

inlinestatic

Definition at line 119 of file rwr.h.

119 { return (Rwr_Node_t *)((ABC_PTRUINT_T)(p) ^ (c)); }

Rwr_Node_t_

Definition: rwr.h:98

static Rwr_Node_t* Rwr_Regular ( Rwr_Node_t * p )

inlinestatic

Definition at line 117 of file rwr.h.

117 { return (Rwr_Node_t *)((ABC_PTRUINT_T)(p) & ~01); }

Rwr_Node_t_

Definition: rwr.h:98

void Rwr_ScoresClean ( Rwr_Man_t * p )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 504 of file rwrEva.c.

 {
     Vec_Ptr_t * vSubgraphs;
     Rwr_Node_t * pNode;
     int i, k;
     for ( i = 0; i < p->vClasses->nSize; i++ )
     {
         vSubgraphs = Vec_VecEntry( p->vClasses, i );
         Vec_PtrForEachEntry( Rwr_Node_t *, vSubgraphs, pNode, k )
             pNode->nScore = pNode->nGain = pNode->nAdded = 0;
     }
 }

void Rwr_ScoresReport ( Rwr_Man_t * p )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 550 of file rwrEva.c.

 {
     extern void Ivy_TruthDsdComputePrint( unsigned uTruth );
     int Perm[222];
     Vec_Ptr_t * vSubgraphs;
     Rwr_Node_t * pNode;
     int i, iNew, k;
     unsigned uTruth;
     // collect total gains
     assert( p->vClasses->nSize == 222 );
     for ( i = 0; i < p->vClasses->nSize; i++ )
     {
         Perm[i] = i;
         Gains[i] = 0;
         vSubgraphs = Vec_VecEntry( p->vClasses, i );
         Vec_PtrForEachEntry( Rwr_Node_t *, vSubgraphs, pNode, k )
             Gains[i] += pNode->nGain;
     }
     // sort the gains
     qsort( Perm, 222, sizeof(int), (int (*)(const void *, const void *))Rwr_ScoresCompare );
 
     // print classes
     for ( i = 0; i < p->vClasses->nSize; i++ )
     {
         iNew = Perm[i];
         if ( Gains[iNew] == 0 )
             break;
         vSubgraphs = Vec_VecEntry( p->vClasses, iNew );
         printf( "CLASS %3d: Subgr = %3d. Total gain = %6d.  ", iNew, Vec_PtrSize(vSubgraphs), Gains[iNew] );
         uTruth = (unsigned)p->pMapInv[iNew];
         Extra_PrintBinary( stdout, &uTruth, 16 );
         printf( "  " );
         Ivy_TruthDsdComputePrint( (unsigned)p->pMapInv[iNew] | ((unsigned)p->pMapInv[iNew] << 16) );
         Vec_PtrForEachEntry( Rwr_Node_t *, vSubgraphs, pNode, k )
         {
             if ( pNode->nScore == 0 )
                 continue;
             printf( "    %2d: S=%5d. A=%5d. G=%6d. ", k, pNode->nScore, pNode->nAdded, pNode->nGain );
             Dec_GraphPrint( stdout, (Dec_Graph_t *)pNode->pNext, NULL, NULL );
         }
     }
 }

Data Structures

Macros

Typedefs

Functions

Macro Definition Documentation

Typedef Documentation

Function Documentation