reoTransfer.c 6.8 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
/**CFile****************************************************************

  FileName    [reoTransfer.c]

  PackageName [REO: A specialized DD reordering engine.]

  Synopsis    [Transfering a DD from the CUDD manager into REO"s internal data structures and back.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - October 15, 2002.]

  Revision    [$Id: reoTransfer.c,v 1.0 2002/15/10 03:00:00 alanmi Exp $]

***********************************************************************/

#include "reo.h"

21 22 23
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                    FUNCTION DEFINITIONS                          ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Transfers the DD into the internal reordering data structure.]

  Description [It is important that the hash table is lossless.]

  SideEffects []

  SeeAlso     []

***********************************************************************/
reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F )
{
    DdManager * dd = p->dd;
    reo_unit * pUnit;
Alan Mishchenko committed
47 48
    int HKey = -1; // Suppress "might be used uninitialized"
        int fComp;
Alan Mishchenko committed
49 50 51 52 53 54 55 56 57
    
    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 )
Alan Mishchenko committed
58
            if ( p->HTable[HKey].Arg1 == (reo_unit *)F )
Alan Mishchenko committed
59
            {
Alan Mishchenko committed
60
                pUnit = p->HTable[HKey].Arg2;  
Alan Mishchenko committed
61 62 63 64 65 66 67 68 69 70 71 72 73 74
                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;
75
        pUnit->pE     = (reo_unit*)(ABC_PTRUINT_T)(cuddV(F));
Alan Mishchenko committed
76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94
        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 )
    {
95
        // the next free entry is already found - it is pointed to by HKey
Alan Mishchenko committed
96 97 98 99
        // 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;
Alan Mishchenko committed
100 101
        p->HTable[HKey].Arg1 = (reo_unit *)F;
        p->HTable[HKey].Arg2 = pUnit;
Alan Mishchenko committed
102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123
    }

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

/**Function*************************************************************

  Synopsis    [Creates the DD from the internal reordering data structure.]

  Description [It is important that the hash table is lossless.]

  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * reoTransferUnitsToNodes_rec( reo_man * p, reo_unit * pUnit )
{
    DdManager * dd = p->dd;
    DdNode * bRes, * E, * T;
Alan Mishchenko committed
124 125
    int HKey = -1; // Suppress "might be used uninitialized"
        int fComp;
Alan Mishchenko committed
126 127 128 129 130 131 132 133

    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 )
Alan Mishchenko committed
134
            if ( p->HTable[HKey].Arg1 == pUnit )
Alan Mishchenko committed
135 136 137 138 139 140 141 142 143 144
            {
                bRes = (DdNode*) p->HTable[HKey].Arg2;  
                assert( bRes );
                return Cudd_NotCond( bRes, fComp );
            }
    }

    // treat the case of constants
    if ( Unit_IsConstant(pUnit) )
    {
Alan Mishchenko committed
145
        bRes = cuddUniqueConst( dd, ((double)((int)(ABC_PTRUINT_T)(pUnit->pE))) );
Alan Mishchenko committed
146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186
        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;
Alan Mishchenko committed
187 188
         p->HTable[HKey].Arg1 = pUnit;
         p->HTable[HKey].Arg2 = (reo_unit *)bRes;  
Alan Mishchenko committed
189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204

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

////////////////////////////////////////////////////////////////////////
///                         END OF FILE                              ///
////////////////////////////////////////////////////////////////////////

205 206
ABC_NAMESPACE_IMPL_END