abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
reoTransfer.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [reoTransfer.c]
4 
5  PackageName [REO: A specialized DD reordering engine.]
6 
7  Synopsis [Transfering a DD from the CUDD manager into REO"s internal data structures and back.]
8 
9  Author [Alan Mishchenko]
10 
11  Affiliation [UC Berkeley]
12 
13  Date [Ver. 1.0. Started - October 15, 2002.]
14 
15  Revision [$Id: reoTransfer.c,v 1.0 2002/15/10 03:00:00 alanmi Exp $]
16 
17 ***********************************************************************/
18 
19 #include "reo.h"
20 
22 
23 
24 ////////////////////////////////////////////////////////////////////////
25 /// DECLARATIONS ///
26 ////////////////////////////////////////////////////////////////////////
27 
28 ////////////////////////////////////////////////////////////////////////
29 /// FUNCTION DEFINITIONS ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 /**Function*************************************************************
33 
34  Synopsis [Transfers the DD into the internal reordering data structure.]
35 
36  Description [It is important that the hash table is lossless.]
37 
38  SideEffects []
39 
40  SeeAlso []
41 
42 ***********************************************************************/
44 {
45  DdManager * dd = p->dd;
46  reo_unit * pUnit;
47  int HKey = -1; // Suppress "might be used uninitialized"
48  int fComp;
49 
50  fComp = Cudd_IsComplement(F);
51  F = Cudd_Regular(F);
52 
53  // check the hash-table
54  if ( F->ref != 1 )
55  {
56  // search cache - use linear probing
57  for ( HKey = hashKey2(p->Signature,F,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize )
58  if ( p->HTable[HKey].Arg1 == (reo_unit *)F )
59  {
60  pUnit = p->HTable[HKey].Arg2;
61  assert( pUnit );
62  // increment the edge counter
63  pUnit->n++;
64  return Unit_NotCond( pUnit, fComp );
65  }
66  }
67  // the entry in not found in the cache
68 
69  // create a new entry
70  pUnit = reoUnitsGetNextUnit( p );
71  pUnit->n = 1;
72  if ( cuddIsConstant(F) )
73  {
74  pUnit->lev = REO_CONST_LEVEL;
75  pUnit->pE = (reo_unit*)(ABC_PTRUINT_T)(cuddV(F));
76  pUnit->pT = NULL;
77  // check if the diagram that is being reordering has complement edges
78  if ( F != dd->one )
79  p->fThisIsAdd = 1;
80  // insert the unit into the corresponding plane
81  reoUnitsAddUnitToPlane( &(p->pPlanes[p->nSupp]), pUnit ); // increments the unit counter
82  }
83  else
84  {
85  pUnit->lev = p->pMapToPlanes[F->index];
86  pUnit->pE = reoTransferNodesToUnits_rec( p, cuddE(F) );
87  pUnit->pT = reoTransferNodesToUnits_rec( p, cuddT(F) );
88  // insert the unit into the corresponding plane
89  reoUnitsAddUnitToPlane( &(p->pPlanes[pUnit->lev]), pUnit ); // increments the unit counter
90  }
91 
92  // add to the hash table
93  if ( F->ref != 1 )
94  {
95  // the next free entry is already found - it is pointed to by HKey
96  // while we traversed the diagram, the hash entry to which HKey points,
97  // might have been used. Make sure that its signature is different.
98  for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize );
99  p->HTable[HKey].Sign = p->Signature;
100  p->HTable[HKey].Arg1 = (reo_unit *)F;
101  p->HTable[HKey].Arg2 = pUnit;
102  }
103 
104  // increment the counter of nodes
105  p->nNodesCur++;
106  return Unit_NotCond( pUnit, fComp );
107 }
108 
109 /**Function*************************************************************
110 
111  Synopsis [Creates the DD from the internal reordering data structure.]
112 
113  Description [It is important that the hash table is lossless.]
114 
115  SideEffects []
116 
117  SeeAlso []
118 
119 ***********************************************************************/
121 {
122  DdManager * dd = p->dd;
123  DdNode * bRes, * E, * T;
124  int HKey = -1; // Suppress "might be used uninitialized"
125  int fComp;
126 
127  fComp = Cudd_IsComplement(pUnit);
128  pUnit = Unit_Regular(pUnit);
129 
130  // check the hash-table
131  if ( pUnit->n != 1 )
132  {
133  for ( HKey = hashKey2(p->Signature,pUnit,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize )
134  if ( p->HTable[HKey].Arg1 == pUnit )
135  {
136  bRes = (DdNode*) p->HTable[HKey].Arg2;
137  assert( bRes );
138  return Cudd_NotCond( bRes, fComp );
139  }
140  }
141 
142  // treat the case of constants
143  if ( Unit_IsConstant(pUnit) )
144  {
145  bRes = cuddUniqueConst( dd, ((double)((int)(ABC_PTRUINT_T)(pUnit->pE))) );
146  cuddRef( bRes );
147  }
148  else
149  {
150  // split and recur on children of this node
151  E = reoTransferUnitsToNodes_rec( p, pUnit->pE );
152  if ( E == NULL )
153  return NULL;
154  cuddRef(E);
155 
156  T = reoTransferUnitsToNodes_rec( p, pUnit->pT );
157  if ( T == NULL )
158  {
159  Cudd_RecursiveDeref(dd, E);
160  return NULL;
161  }
162  cuddRef(T);
163 
164  // consider the case when Res0 and Res1 are the same node
165  assert( E != T );
166  assert( !Cudd_IsComplement(T) );
167 
168  bRes = cuddUniqueInter( dd, p->pMapToDdVarsFinal[pUnit->lev], T, E );
169  if ( bRes == NULL )
170  {
171  Cudd_RecursiveDeref(dd,E);
172  Cudd_RecursiveDeref(dd,T);
173  return NULL;
174  }
175  cuddRef( bRes );
176  cuddDeref( E );
177  cuddDeref( T );
178  }
179 
180  // do not keep the result if the ref count is only 1, since it will not be visited again
181  if ( pUnit->n != 1 )
182  {
183  // while we traversed the diagram, the hash entry to which HKey points,
184  // might have been used. Make sure that its signature is different.
185  for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize );
186  p->HTable[HKey].Sign = p->Signature;
187  p->HTable[HKey].Arg1 = pUnit;
188  p->HTable[HKey].Arg2 = (reo_unit *)bRes;
189 
190  // add the DD to the referenced DD list in order to be able to store it in cache
191  p->pRefNodes[p->nRefNodes++] = bRes; Cudd_Ref( bRes );
192  // no need to do this, because the garbage collection will not take bRes away
193  // it is held by the diagram in the making
194  }
195  // increment the counter of nodes
196  p->nNodesCur++;
197  cuddDeref( bRes );
198  return Cudd_NotCond( bRes, fComp );
199 }
200 
201 ////////////////////////////////////////////////////////////////////////
202 /// END OF FILE ///
203 ////////////////////////////////////////////////////////////////////////
204 
206 
DdHalfWord ref
Definition: cudd.h:280
#define cuddRef(n)
Definition: cuddInt.h:584
#define hashKey2(a, b, TSIZE)
Definition: extraBdd.h:86
#define cuddDeref(n)
Definition: cuddInt.h:604
short lev
Definition: reo.h:68
int Sign
Definition: reo.h:95
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
static Llb_Mgr_t * p
Definition: llb3Image.c:950
DdNode * reoTransferUnitsToNodes_rec(reo_man *p, reo_unit *pUnit)
Definition: reoTransfer.c:120
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Definition: cuddTable.c:1450
#define Cudd_Regular(node)
Definition: cudd.h:397
DdManager * dd
Definition: reo.h:112
reo_unit * reoUnitsGetNextUnit(reo_man *p)
FUNCTION DEFINITIONS ///.
Definition: reoUnits.c:45
int * pMapToPlanes
Definition: reo.h:137
int Signature
Definition: reo.h:151
int nNodesCur
Definition: reo.h:127
int fThisIsAdd
Definition: reo.h:116
int nSupp
Definition: reo.h:119
reo_unit * Arg2
Definition: reo.h:97
int nRefNodes
Definition: reo.h:156
#define cuddV(node)
Definition: cuddInt.h:668
int * pMapToDdVarsFinal
Definition: reo.h:139
void reoUnitsAddUnitToPlane(reo_plane *pPlane, reo_unit *pUnit)
Definition: reoUnits.c:135
#define Cudd_IsComplement(node)
Definition: cudd.h:425
reo_unit * pT
Definition: reo.h:75
DdNode ** pRefNodes
Definition: reo.h:155
short n
Definition: reo.h:71
reo_unit * pE
Definition: reo.h:74
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
#define cuddIsConstant(node)
Definition: cuddInt.h:620
#define Unit_NotCond(u, c)
Definition: reo.h:176
reo_hash * HTable
Definition: reo.h:149
int nTableSize
Definition: reo.h:150
#define cuddT(node)
Definition: cuddInt.h:636
#define Unit_Regular(u)
Definition: reo.h:174
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
#define Unit_IsConstant(u)
Definition: reo.h:177
reo_plane * pPlanes
Definition: reo.h:142
DdHalfWord index
Definition: cudd.h:279
reo_unit * Arg1
Definition: reo.h:96
DdNode * one
Definition: cuddInt.h:345
Definition: reo.h:66
#define cuddE(node)
Definition: cuddInt.h:652
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
#define assert(ex)
Definition: util_old.h:213
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
#define REO_CONST_LEVEL
Definition: reo.h:40
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
Definition: reo.h:101
ABC_NAMESPACE_IMPL_START reo_unit * reoTransferNodesToUnits_rec(reo_man *p, DdNode *F)
DECLARATIONS ///.
Definition: reoTransfer.c:43