Version abc71001

1 files changed, 199 insertions, 0 deletions

diff --git a/src/bdd/reo/reoTransfer.c b/src/bdd/reo/reoTransfer.c
new file mode 100644
index 00000000..65d31d01
--- /dev/null
+++ b/src/bdd/reo/reoTransfer.c
@@ -0,0 +1,199 @@
+/**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"
+
+////////////////////////////////////////////////////////////////////////
+///                        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;
+    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 );
+}
+
+/**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;
+    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 );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                         END OF FILE                              ///
+////////////////////////////////////////////////////////////////////////
+