src/bdd/reo/reoTransfer.c

Go to the documentation of this file.

#include "reo.h"



reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F )
{
        DdManager * dd = p->dd;
        reo_unit * pUnit;
        int HKey, fComp;
        
        fComp = Cudd_IsComplement(F);
        F = Cudd_Regular(F);

        // check the hash-table
        if ( F->ref != 1 )
        {
                // search cache - use linear probing
                for ( HKey = hashKey2(p->Signature,F,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize )
                        if ( p->HTable[HKey].Arg1 == (reo_unit *)F )
                        {
                                pUnit = p->HTable[HKey].Arg2;  
                                assert( pUnit );
                                // increment the edge counter
                                pUnit->n++;
                                return Unit_NotCond( pUnit, fComp );
                        }
        }
        // the entry in not found in the cache
        
        // create a new entry
        pUnit         = reoUnitsGetNextUnit( p );
        pUnit->n      = 1;
        if ( cuddIsConstant(F) )
        {
                pUnit->lev    = REO_CONST_LEVEL;
                pUnit->pE     = (reo_unit*)((int)(cuddV(F)));
                pUnit->pT     = NULL;
                // check if the diagram that is being reordering has complement edges
                if ( F != dd->one )
                        p->fThisIsAdd = 1;
                // insert the unit into the corresponding plane
                reoUnitsAddUnitToPlane( &(p->pPlanes[p->nSupp]), pUnit ); // increments the unit counter
        }
        else
        {
                pUnit->lev    = p->pMapToPlanes[F->index];
                pUnit->pE     = reoTransferNodesToUnits_rec( p, cuddE(F) );
                pUnit->pT     = reoTransferNodesToUnits_rec( p, cuddT(F) );
                // insert the unit into the corresponding plane
                reoUnitsAddUnitToPlane( &(p->pPlanes[pUnit->lev]), pUnit ); // increments the unit counter
        }

        // add to the hash table
        if ( F->ref != 1 )
        {
                // the next free entry is already found - it is pointed to by HKey
                // while we traversed the diagram, the hash entry to which HKey points,
                // might have been used. Make sure that its signature is different.
                for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize );
                p->HTable[HKey].Sign = p->Signature;
                p->HTable[HKey].Arg1 = (reo_unit *)F;
                p->HTable[HKey].Arg2 = pUnit;
        }

        // increment the counter of nodes
        p->nNodesCur++;
        return Unit_NotCond( pUnit, fComp );
}

DdNode * reoTransferUnitsToNodes_rec( reo_man * p, reo_unit * pUnit )
{
        DdManager * dd = p->dd;
        DdNode * bRes, * E, * T;
        int HKey, fComp;

        fComp = Cudd_IsComplement(pUnit);
        pUnit = Unit_Regular(pUnit);

        // check the hash-table
        if ( pUnit->n != 1 )
        {
                for ( HKey = hashKey2(p->Signature,pUnit,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize )
                        if ( p->HTable[HKey].Arg1 == pUnit )
                        {
                                bRes = (DdNode*) p->HTable[HKey].Arg2;  
                                assert( bRes );
                                return Cudd_NotCond( bRes, fComp );
                        }
        }

        // treat the case of constants
        if ( Unit_IsConstant(pUnit) )
        {
                bRes = cuddUniqueConst( dd, ((double)((int)(pUnit->pE))) );
                cuddRef( bRes );
        }
        else
        {
                // split and recur on children of this node
                E = reoTransferUnitsToNodes_rec( p, pUnit->pE );
                if ( E == NULL )
                        return NULL;
                cuddRef(E);

                T = reoTransferUnitsToNodes_rec( p, pUnit->pT );
                if ( T == NULL )
                {
                        Cudd_RecursiveDeref(dd, E);
                        return NULL;
                }
                cuddRef(T);
                
                // consider the case when Res0 and Res1 are the same node
                assert( E != T );
                assert( !Cudd_IsComplement(T) );

                bRes = cuddUniqueInter( dd, p->pMapToDdVarsFinal[pUnit->lev], T, E );
                if ( bRes == NULL ) 
                {
                        Cudd_RecursiveDeref(dd,E);
                        Cudd_RecursiveDeref(dd,T);
                        return NULL;
                }
                cuddRef( bRes );
                cuddDeref( E );
                cuddDeref( T );
        }

        // do not keep the result if the ref count is only 1, since it will not be visited again
        if ( pUnit->n != 1 )
        {
                 // while we traversed the diagram, the hash entry to which HKey points,
                 // might have been used. Make sure that its signature is different.
                 for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize );
                 p->HTable[HKey].Sign = p->Signature;
                 p->HTable[HKey].Arg1 = pUnit;
                 p->HTable[HKey].Arg2 = (reo_unit *)bRes;  

                 // add the DD to the referenced DD list in order to be able to store it in cache
                 p->pRefNodes[p->nRefNodes++] = bRes;  Cudd_Ref( bRes ); 
                 // no need to do this, because the garbage collection will not take bRes away
                 // it is held by the diagram in the making
        }
        // increment the counter of nodes
        p->nNodesCur++;
        cuddDeref( bRes );
        return Cudd_NotCond( bRes, fComp );
}

---