Version abc70930

1 files changed, 0 insertions, 362 deletions

diff --git a/src/opt/rwr/rwrLib.c b/src/opt/rwr/rwrLib.c
deleted file mode 100644
index 1cdf350e..00000000
--- a/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                                ///
-////////////////////////////////////////////////////////////////////////
-
-