summaryrefslogtreecommitdiffstats
path: root/abc70930/src/opt/rwr/rwrLib.c
diff options
context:
space:
mode:
Diffstat (limited to 'abc70930/src/opt/rwr/rwrLib.c')
-rw-r--r--abc70930/src/opt/rwr/rwrLib.c362
1 files changed, 0 insertions, 362 deletions
diff --git a/abc70930/src/opt/rwr/rwrLib.c b/abc70930/src/opt/rwr/rwrLib.c
deleted file mode 100644
index 1cdf350e..00000000
--- a/abc70930/src/opt/rwr/rwrLib.c
+++ /dev/null
@@ -1,362 +0,0 @@
-/**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 $]
-
-***********************************************************************/
-
-#include "rwr.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-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 );
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Precomputes the forest in the manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Rwr_ManPrecompute( Rwr_Man_t * p )
-{
- Rwr_Node_t * p0, * p1;
- int i, k, Level, Volume;
- int LevelOld = -1;
- int nNodes;
-
- Vec_PtrForEachEntryStart( p->vForest, p0, i, 1 )
- Vec_PtrForEachEntryStart( 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_MAX( 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( 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( 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 );
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds one node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Rwr_Node_t * Rwr_ManTryNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
-{
- Rwr_Node_t * pOld, * pNew, ** ppPlace;
- unsigned uTruth;
- // compute truth table, level, volume
- p->nConsidered++;
- if ( fExor )
- {
-// printf( "Considering EXOR of %d and %d.\n", p0->Id, p1->Id );
- 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;
- // skip non-practical classes
- if ( Level > 2 && !p->pPractical[p->puCanons[uTruth]] )
- return NULL;
- // enumerate through the nodes with the same canonical form
- ppPlace = p->pTable + uTruth;
- for ( pOld = *ppPlace; pOld; ppPlace = &pOld->pNext, pOld = pOld->pNext )
- {
- if ( pOld->Level < (unsigned)Level && pOld->Volume < (unsigned)Volume )
- return NULL;
- if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
- return NULL;
-// if ( pOld->Level < (unsigned)Level && pOld->Volume == (unsigned)Volume )
-// return NULL;
- }
-/*
- // enumerate through the nodes with the opposite polarity
- for ( pOld = p->pTable[~uTruth & 0xFFFF]; pOld; pOld = pOld->pNext )
- {
- if ( pOld->Level < (unsigned)Level && pOld->Volume < (unsigned)Volume )
- return NULL;
- if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
- return NULL;
-// if ( pOld->Level < (unsigned)Level && pOld->Volume == (unsigned)Volume )
-// return NULL;
- }
-*/
- // count the classes
- if ( p->pTable[uTruth] == NULL && p->puCanons[uTruth] == uTruth )
- p->nClasses++;
- // 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 );
- *ppPlace = pNew;
- return pNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds one node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-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 * 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;
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds one node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Rwr_Node_t * Rwr_ManAddVar( Rwr_Man_t * p, unsigned uTruth, int fPrecompute )
-{
- 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;
-}
-
-
-
-/**Function*************************************************************
-
- Synopsis [Adds one node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Rwr_MarkUsed_rec( Rwr_Man_t * p, Rwr_Node_t * pNode )
-{
- if ( pNode->fUsed || pNode->TravId == p->nTravIds )
- return;
- pNode->TravId = p->nTravIds;
- pNode->fUsed = 1;
- Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p0) );
- Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p1) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds one node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Rwr_Trav_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, int * pVolume )
-{
- if ( pNode->fUsed || pNode->TravId == p->nTravIds )
- return;
- pNode->TravId = p->nTravIds;
- (*pVolume)++;
- if ( pNode->fExor )
- (*pVolume)++;
- Rwr_Trav_rec( p, Rwr_Regular(pNode->p0), pVolume );
- Rwr_Trav_rec( p, Rwr_Regular(pNode->p1), pVolume );
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds one node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Rwr_ManNodeVolume( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 )
-{
- int Volume = 0;
- Rwr_ManIncTravId( p );
- Rwr_Trav_rec( p, p0, &Volume );
- Rwr_Trav_rec( p, p1, &Volume );
- return Volume;
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds one node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Rwr_ManIncTravId( Rwr_Man_t * p )
-{
- Rwr_Node_t * pNode;
- int i;
- if ( p->nTravIds++ < 0x8FFFFFFF )
- return;
- Vec_PtrForEachEntry( p->vForest, pNode, i )
- pNode->TravId = 0;
- p->nTravIds = 1;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-11 09:49:38 +0000