summaryrefslogtreecommitdiffstats
path: root/src/bdd/reo/reoTransfer.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/reo/reoTransfer.c')
-rw-r--r--src/bdd/reo/reoTransfer.c199
1 files changed, 0 insertions, 199 deletions
diff --git a/src/bdd/reo/reoTransfer.c b/src/bdd/reo/reoTransfer.c
deleted file mode 100644
index 65d31d01..00000000
--- a/src/bdd/reo/reoTransfer.c
+++ /dev/null
@@ -1,199 +0,0 @@
-/**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 ///
-////////////////////////////////////////////////////////////////////////
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-04 05:44:05 +0000