rwrLib.c File Reference

#include "rwr.h"

Include dependency graph for rwrLib.c:

Go to the source code of this file.

Functions
void	Rwr_ManPrecompute (Rwr_Man_t *p)
	FUNCTION DEFINITIONS ///.
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_ManAddNode()

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Rwr_ManAddVar()

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Rwr_ManIncTravId()

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;
}

Here is the caller graph for this function:

Rwr_ManNodeVolume()

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Rwr_ManPrecompute()

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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Rwr_Trav_rec()

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

{
    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 );
}

Here is the call graph for this function:

Here is the caller graph for this function: