src/bdd/reo/reo.h File Reference
#include <stdio.h>#include <stdlib.h>#include "extra.h"
Include dependency graph for reo.h:
This graph shows which files directly or indirectly include this file:
Go to the source code of this file.
Define Documentation
| #define REO_REORDER_LIMIT 1.15 |
CFile****************************************************************
FileName [reo.h]
PackageName [REO: A specialized DD reordering engine.]
Synopsis [External and internal declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - October 15, 2002.]
Revision [
- Id
- reo.h,v 1.0 2002/15/10 03:00:00 alanmi Exp
] MACRO DEFINITIONS ///
| #define Unit_IsConstant | ( | u | ) | ((int)((u)->lev == REO_CONST_LEVEL)) |
| #define Unit_Not | ( | u | ) | ((reo_unit *)((unsigned long)(u) ^ 01)) |
| #define Unit_NotCond | ( | u, | |||
| c | ) | ((reo_unit *)((unsigned long)(u) ^ (c))) |
| #define Unit_Regular | ( | u | ) | ((reo_unit *)((unsigned long)(u) & ~01)) |
Typedef Documentation
| typedef struct _reo_plane reo_plane |
Enumeration Type Documentation
| enum reo_min_type |
Definition at line 50 of file reo.h.
00050 { 00051 REO_MINIMIZE_NODES, 00052 REO_MINIMIZE_WIDTH, // may not work for BDDs with complemented edges 00053 REO_MINIMIZE_APL 00054 } reo_min_type;
Function Documentation
Function*************************************************************
Synopsis []
Description [Transfers the ADD into another manager minimizes it and returns the min number of nodes; disposes of the BDD in the new manager. Useful for debugging or comparing the performance of other reordering procedures.]
SideEffects []
SeeAlso []
Definition at line 214 of file reoTest.c.
00215 { 00216 static DdManager * s_ddmin; 00217 DdNode * bF; 00218 DdNode * bFmin; 00219 DdNode * aFmin; 00220 int nNodesBeg; 00221 int nNodesEnd; 00222 int clk1; 00223 00224 if ( s_ddmin == NULL ) 00225 s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0); 00226 00227 // Cudd_ShuffleHeap( s_ddmin, dd->invperm ); 00228 00229 clk1 = clock(); 00230 bF = Cudd_addBddPattern( dd, aF ); Cudd_Ref( bF ); 00231 bFmin = Cudd_bddTransfer( dd, s_ddmin, bF ); Cudd_Ref( bFmin ); 00232 Cudd_RecursiveDeref( dd, bF ); 00233 aFmin = Cudd_BddToAdd( s_ddmin, bFmin ); Cudd_Ref( aFmin ); 00234 Cudd_RecursiveDeref( s_ddmin, bFmin ); 00235 00236 nNodesBeg = Cudd_DagSize( aFmin ); 00237 Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SIFT,1); 00238 // Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SYMM_SIFT,1); 00239 nNodesEnd = Cudd_DagSize( aFmin ); 00240 Cudd_RecursiveDeref( s_ddmin, aFmin ); 00241 00242 printf( "Classical reordering of ADDs: Before = %d. After = %d.\n", nNodesBeg, nNodesEnd ); 00243 printf( "Classical variable reordering time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) ); 00244 return nNodesEnd; 00245 }
Function*************************************************************
Synopsis []
Description [Transfers the BDD into another manager minimizes it and returns the min number of nodes; disposes of the BDD in the new manager. Useful for debugging or comparing the performance of other reordering procedures.]
SideEffects []
SeeAlso []
Definition at line 177 of file reoTest.c.
00178 { 00179 static DdManager * s_ddmin; 00180 DdNode * bFmin; 00181 int nNodes; 00182 // int clk1; 00183 00184 if ( s_ddmin == NULL ) 00185 s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0); 00186 00187 // Cudd_ShuffleHeap( s_ddmin, dd->invperm ); 00188 00189 // clk1 = clock(); 00190 bFmin = Cudd_bddTransfer( dd, s_ddmin, bF ); Cudd_Ref( bFmin ); 00191 Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SIFT,1); 00192 // Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SYMM_SIFT,1); 00193 nNodes = Cudd_DagSize( bFmin ); 00194 Cudd_RecursiveDeref( s_ddmin, bFmin ); 00195 00196 // printf( "Classical variable reordering time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) ); 00197 return nNodes; 00198 }
Function*************************************************************
Synopsis [Performs reordering of the function.]
Description [Returns the DD minimized by variable reordering in the REO engine. Takes the CUDD decision diagram manager (dd) and the function (Func) represented as a BDD or ADD (MTBDD). If the variable array (pOrder) is not NULL, returns the resulting variable permutation. The permutation is such that if the resulting function is permuted by Cudd_(add,bdd)Permute() using pOrder as the permutation array, the initial function (Func) results. Several flag set by other interface functions specify reordering options:
- Remappig can be set by Extra_ReorderSetRemapping(). Then the resulting DD after reordering is remapped into the topmost levels of the DD manager. Otherwise, the resulting DD after reordering is mapped using the same variables, on which it originally depended, only (possibly) permuted as a result of reordering.
- Minimization type can be set by Extra_ReorderSetMinimizationType(). Note that when the BDD is minimized for the total width of the total APL, the number BDD nodes can increase. The total width is defines as sum total of widths on each level. The width on one level is defined as the number of distinct BDD nodes pointed by the nodes situated above the given level.
- The number of iterations of sifting can be set by Extra_ReorderSetIterations(). The decision diagram returned by this procedure is not referenced.]
SideEffects []
SeeAlso []
Definition at line 259 of file reoApi.c.
00260 { 00261 DdNode * FuncRes; 00262 Extra_ReorderArray( p, dd, &Func, &FuncRes, 1, pOrder ); 00263 Cudd_Deref( FuncRes ); 00264 return FuncRes; 00265 }
| void Extra_ReorderArray | ( | reo_man * | p, | |
| DdManager * | dd, | |||
| DdNode * | Funcs[], | |||
| DdNode * | FuncsRes[], | |||
| int | nFuncs, | |||
| int * | pOrder | |||
| ) |
Function*************************************************************
Synopsis [Performs reordering of the array of functions.]
Description [The options are similar to the procedure Extra_Reorder(), except that the user should also provide storage for the resulting DDs, which are returned referenced.]
SideEffects []
SeeAlso []
Definition at line 280 of file reoApi.c.
00281 { 00282 reoReorderArray( p, dd, Funcs, FuncsRes, nFuncs, pOrder ); 00283 }
Function*************************************************************
Synopsis [Reorders the DD using CUDD package.]
Description [Transfers the DD into a temporary manager in such a way that the level correspondence is preserved. Reorders the manager and transfers the DD back into the original manager using the topmost levels of the manager, in such a way that the ordering of levels is preserved. The resulting permutation is returned in the array given by the user.]
SideEffects []
SeeAlso []
Definition at line 106 of file reoTest.c.
00107 { 00108 static DdManager * ddReorder = NULL; 00109 static int * Permute = NULL; 00110 static int * PermuteReo1 = NULL; 00111 static int * PermuteReo2 = NULL; 00112 DdNode * aFuncReorder, * aFuncNew; 00113 int lev, var; 00114 00115 // start the reordering manager 00116 if ( ddReorder == NULL ) 00117 { 00118 Permute = ALLOC( int, dd->size ); 00119 PermuteReo1 = ALLOC( int, dd->size ); 00120 PermuteReo2 = ALLOC( int, dd->size ); 00121 ddReorder = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); 00122 Cudd_AutodynDisable(ddReorder); 00123 } 00124 00125 // determine the permutation of variable to make sure that var order in bFunc 00126 // will not change when this function is transfered into the new manager 00127 for ( lev = 0; lev < dd->size; lev++ ) 00128 { 00129 Permute[ dd->invperm[lev] ] = ddReorder->invperm[lev]; 00130 PermuteReo1[ ddReorder->invperm[lev] ] = dd->invperm[lev]; 00131 } 00132 // transfer this function into the new manager in such a way that ordering of vars does not change 00133 aFuncReorder = Extra_TransferPermute( dd, ddReorder, aFunc, Permute ); Cudd_Ref( aFuncReorder ); 00134 // assert( Cudd_DagSize(aFunc) == Cudd_DagSize(aFuncReorder) ); 00135 00136 // perform the reordering 00137 printf( "Nodes before = %d.\n", Cudd_DagSize(aFuncReorder) ); 00138 Cudd_ReduceHeap( ddReorder, CUDD_REORDER_SYMM_SIFT, 1 ); 00139 printf( "Nodes before = %d.\n", Cudd_DagSize(aFuncReorder) ); 00140 00141 // determine the reverse variable permutation 00142 for ( lev = 0; lev < dd->size; lev++ ) 00143 { 00144 Permute[ ddReorder->invperm[lev] ] = dd->invperm[lev]; 00145 PermuteReo2[ dd->invperm[lev] ] = ddReorder->invperm[lev]; 00146 } 00147 00148 // transfer this function into the new manager in such a way that ordering of vars does not change 00149 aFuncNew = Extra_TransferPermute( ddReorder, dd, aFuncReorder, Permute ); Cudd_Ref( aFuncNew ); 00150 // assert( Cudd_DagSize(aFuncNew) == Cudd_DagSize(aFuncReorder) ); 00151 Cudd_RecursiveDeref( ddReorder, aFuncReorder ); 00152 00153 // derive the resulting variable ordering 00154 if ( pPermuteReo ) 00155 for ( var = 0; var < dd->size; var++ ) 00156 pPermuteReo[var] = PermuteReo1[ PermuteReo2[var] ]; 00157 00158 Cudd_Deref( aFuncNew ); 00159 return aFuncNew; 00160 }
| reo_man* Extra_ReorderInit | ( | int | nDdVarsMax, | |
| int | nNodesMax | |||
| ) |
FUNCTION DECLARATIONS ///
CFile****************************************************************
FileName [reoApi.c]
PackageName [REO: A specialized DD reordering engine.]
Synopsis [Implementation of API functions.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - October 15, 2002.]
Revision [
- Id
- reoApi.c,v 1.0 2002/15/10 03:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Initializes the reordering engine.]
Description [The first argument is the max number of variables in the CUDD DD manager which will be used with the reordering engine (this number of should be the maximum of BDD and ZDD parts). The second argument is the maximum number of BDD nodes in the BDDs to be reordered. These limits are soft. Setting lower limits will later cause the reordering manager to resize internal data structures. However, setting the exact values will make reordering more efficient because resizing will be not necessary.]
SideEffects []
SeeAlso []
Definition at line 47 of file reoApi.c.
00048 { 00049 reo_man * p; 00050 // allocate and clean the data structure 00051 p = ALLOC( reo_man, 1 ); 00052 memset( p, 0, sizeof(reo_man) ); 00053 // resize the manager to meet user's needs 00054 reoResizeStructures( p, nDdVarsMax, nNodesMax, 100 ); 00055 // set the defaults 00056 p->fMinApl = 0; 00057 p->fMinWidth = 0; 00058 p->fRemapUp = 0; 00059 p->fVerbose = 0; 00060 p->fVerify = 0; 00061 p->nIters = 1; 00062 return p; 00063 }
| void Extra_ReorderQuit | ( | reo_man * | p | ) |
Function*************************************************************
Synopsis [Disposes of the reordering engine.]
Description [Removes all memory associated with the reordering engine.]
SideEffects []
SeeAlso []
Definition at line 76 of file reoApi.c.
00077 { 00078 free( p->pTops ); 00079 free( p->pSupp ); 00080 free( p->pOrderInt ); 00081 free( p->pWidthCofs ); 00082 free( p->pMapToPlanes ); 00083 free( p->pMapToDdVarsOrig ); 00084 free( p->pMapToDdVarsFinal ); 00085 free( p->pPlanes ); 00086 free( p->pVarCosts ); 00087 free( p->pLevelOrder ); 00088 free( p->HTable ); 00089 free( p->pRefNodes ); 00090 reoUnitsStopDispenser( p ); 00091 free( p->pMemChunks ); 00092 free( p ); 00093 }
| void Extra_ReorderSetIterations | ( | reo_man * | p, | |
| int | nIters | |||
| ) |
Function*************************************************************
Synopsis [Sets the number of iterations of sifting performed.]
Description [The default is one iteration. But a higher minimization quality is desired, it is possible to set the number of iterations to any number larger than 1. Convergence is often reached after several iterations, so typically it make no sense to set the number of iterations higher than 3.]
SideEffects []
SeeAlso []
Definition at line 189 of file reoApi.c.
00190 { 00191 p->nIters = nIters; 00192 }
| void Extra_ReorderSetMinimizationType | ( | reo_man * | p, | |
| reo_min_type | fMinType | |||
| ) |
Function*************************************************************
Synopsis [Sets the type of DD minimizationl that will be performed.]
Description [Currently, three different types of minimization are supported. It is possible to minimize the number of BDD nodes. This is a classical type of minimization, which is attempting to reduce the total number of nodes in the (shared) BDD of the given Boolean functions. It is also possible to minimize the BDD width, defined as the sum total of the number of cofactors on each level in the (shared) BDD (note that the number of cofactors on the given level may be larger than the number of nodes appearing on the given level). It is also possible to minimize the average path length in the (shared) BDD defined as the sum of products, for all BDD paths from the top node to any terminal node, of the number of minterms on the path by the number of nodes on the path. The default reordering type is minimization for the number of BDD nodes. Calling this function with REO_MINIMIZE_WIDTH or REO_MINIMIZE_APL as the second argument, changes the default minimization option for all the reorder calls performed afterwards.]
SideEffects []
SeeAlso []
Definition at line 119 of file reoApi.c.
00120 { 00121 if ( fMinType == REO_MINIMIZE_NODES ) 00122 { 00123 p->fMinWidth = 0; 00124 p->fMinApl = 0; 00125 } 00126 else if ( fMinType == REO_MINIMIZE_WIDTH ) 00127 { 00128 p->fMinWidth = 1; 00129 p->fMinApl = 0; 00130 } 00131 else if ( fMinType == REO_MINIMIZE_APL ) 00132 { 00133 p->fMinWidth = 0; 00134 p->fMinApl = 1; 00135 } 00136 else 00137 { 00138 assert( 0 ); 00139 } 00140 }
| void Extra_ReorderSetRemapping | ( | reo_man * | p, | |
| int | fRemapUp | |||
| ) |
Function*************************************************************
Synopsis [Sets the type of remapping performed by the engine.]
Description [The remapping refers to the way the resulting BDD is expressed using the elementary variables of the CUDD BDD manager. Currently, two types possibilities are supported: remapping and no remapping. Remapping means that the function(s) after reordering depend on the topmost variables in the manager. No remapping means that the function(s) after reordering depend on the same variables as before. Consider the following example. Suppose the initial four variable function depends on variables 2,4,5, and 9 on the CUDD BDD manager, which may be found anywhere in the current variable order. If remapping is set, the function after ordering depends on the topmost variables in the manager, which may or may not be the same as the variables 2,4,5, and 9. If no remapping is set, then the reordered function depend on the same variables 2,4,5, and 9, but the meaning of each variale has changed according to the new ordering. The resulting ordering is returned in the array "pOrder" filled out by the reordering engine in the call to Extra_Reorder(). The default is no remapping.]
SideEffects []
SeeAlso []
Definition at line 169 of file reoApi.c.
00170 { 00171 p->fRemapUp = fRemapUp; 00172 }
| void Extra_ReorderSetVerbosity | ( | reo_man * | p, | |
| int | fVerbose | |||
| ) |
Function*************************************************************
Synopsis [Sets the verbosity level.]
Description [Setting the level to 1 results in printing statistics before and after the reordering.]
SideEffects []
SeeAlso []
Definition at line 226 of file reoApi.c.
00227 { 00228 p->fVerbose = fVerbose; 00229 }
| void Extra_ReorderSetVerification | ( | reo_man * | p, | |
| int | fVerify | |||
| ) |
Function*************************************************************
Synopsis [Sets the verification mode.]
Description [Setting the level to 1 results in verifying the results of variable reordering. Verification is performed by remapping the resulting functions into the original variable order and comparing them with the original functions given by the user. Enabling verification typically leads to 20-30% increase in the total runtime of REO.]
SideEffects []
SeeAlso []
Definition at line 209 of file reoApi.c.
00210 { 00211 p->fVerify = fVerify; 00212 }
CFile****************************************************************
FileName [reoTest.c]
PackageName [REO: A specialized DD reordering engine.]
Synopsis [Various testing procedures (may be outdated).]
Author [Alan Mishchenko <alanmi@ece.pdx.edu>]
Affiliation [ECE Department. Portland State University, Portland, Oregon.]
Date [Ver. 1.0. Started - October 15, 2002.]
Revision [
- Id
- reoTest.c,v 1.0 2002/15/10 03:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Reorders the DD using REO and CUDD.]
Description [This function can be used to test the performance of the reordering package.]
SideEffects []
SeeAlso []
Definition at line 40 of file reoTest.c.
00041 { 00042 reo_man * pReo; 00043 DdNode * Temp, * Temp1; 00044 int pOrder[1000]; 00045 00046 pReo = Extra_ReorderInit( 100, 100 ); 00047 00048 //Extra_DumpDot( dd, &Func, 1, "beforReo.dot", 0 ); 00049 Temp = Extra_Reorder( pReo, dd, Func, pOrder ); Cudd_Ref( Temp ); 00050 //Extra_DumpDot( dd, &Temp, 1, "afterReo.dot", 0 ); 00051 00052 Temp1 = Extra_ReorderCudd(dd, Func, NULL ); Cudd_Ref( Temp1 ); 00053 printf( "Initial = %d. Final = %d. Cudd = %d.\n", Cudd_DagSize(Func), Cudd_DagSize(Temp), Cudd_DagSize(Temp1) ); 00054 Cudd_RecursiveDeref( dd, Temp1 ); 00055 Cudd_RecursiveDeref( dd, Temp ); 00056 00057 Extra_ReorderQuit( pReo ); 00058 }
| void reoProfileAplPrint | ( | reo_man * | p | ) |
Function********************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 302 of file reoProfile.c.
| void reoProfileAplStart | ( | reo_man * | p | ) |
Function*************************************************************
Synopsis [Start the profile for the APL.]
Description [Computes the total path length. The path length is normalized by dividing it by 2^|supp(f)|. To get the "real" APL, multiply by 2^|supp(f)|. This procedure assumes that Weight field of all nodes has been set to 0.0 before the call, except for the weight of the topmost node, which is set to 1.0 (1.0 is the probability of traversing the topmost node). This procedure assigns the edge weights. Because of the equal probability of selecting 0 and 1 assignment at a node, the edge weights are the same for the node. Instead of storing them, we store the weight of the node, which is the probability of traversing the node (pUnit->Weight) during the top down evalation of the BDD. ]
SideEffects []
SeeAlso []
Definition at line 75 of file reoProfile.c.
00076 { 00077 reo_unit * pER, * pTR; 00078 reo_unit * pUnit; 00079 double Res, Half; 00080 int i; 00081 00082 // clean the weights of all nodes 00083 for ( i = 0; i < p->nSupp; i++ ) 00084 for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next ) 00085 pUnit->Weight = 0.0; 00086 // to assign the node weights (the probability of visiting each node) 00087 // we visit the node after visiting its predecessors 00088 00089 // set the probability of visits to the top nodes 00090 for ( i = 0; i < p->nTops; i++ ) 00091 Unit_Regular(p->pTops[i])->Weight += 1.0; 00092 00093 // to compute the path length (the sum of products of edge weight by edge length) 00094 // we visit the nodes in any order (the above order will do) 00095 Res = 0.0; 00096 for ( i = 0; i < p->nSupp; i++ ) 00097 { 00098 p->pPlanes[i].statsCost = 0.0; 00099 for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next ) 00100 { 00101 pER = Unit_Regular(pUnit->pE); 00102 pTR = Unit_Regular(pUnit->pT); 00103 Half = 0.5 * pUnit->Weight; 00104 pER->Weight += Half; 00105 pTR->Weight += Half; 00106 // add to the path length 00107 p->pPlanes[i].statsCost += pUnit->Weight; 00108 } 00109 Res += p->pPlanes[i].statsCost; 00110 } 00111 p->pPlanes[p->nSupp].statsCost = 0.0; 00112 p->nAplBeg = p->nAplCur = Res; 00113 }
| void reoProfileNodesPrint | ( | reo_man * | p | ) |
Function********************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 286 of file reoProfile.c.
| void reoProfileNodesStart | ( | reo_man * | p | ) |
CFile****************************************************************
FileName [reoProfile.c]
PackageName [REO: A specialized DD reordering engine.]
Synopsis [Procudures that compute variables profiles (nodes, width, APL).]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - October 15, 2002.]
Revision [
- Id
- reoProfile.c,v 1.0 2002/15/10 03:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function********************************************************************
Synopsis [Start the profile for the BDD nodes.]
Description [TopRef is the first level, on this the given node counts towards the width of the BDDs. (In other words, it is the level of the referencing node plus 1.)]
SideEffects []
SeeAlso []
Definition at line 43 of file reoProfile.c.
| void reoProfileWidthPrint | ( | reo_man * | p | ) |
Function********************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 318 of file reoProfile.c.
00319 { 00320 int WidthMax; 00321 int TotalWidth; 00322 int i; 00323 00324 WidthMax = 0; 00325 TotalWidth = 0; 00326 for ( i = 0; i <= p->nSupp; i++ ) 00327 { 00328 // printf( "Level = %2d. Width = %3d.\n", i, p->pProfile[i] ); 00329 if ( WidthMax < p->pPlanes[i].statsWidth ) 00330 WidthMax = p->pPlanes[i].statsWidth; 00331 TotalWidth += p->pPlanes[i].statsWidth; 00332 } 00333 assert( p->nWidthCur == TotalWidth ); 00334 printf( "WIDTH: " ); 00335 printf( "Maximum = %5d. ", WidthMax ); 00336 printf( "Total = %7d. ", p->nWidthCur ); 00337 printf( "Average = %6.2f.\n", TotalWidth / (float)p->nSupp ); 00338 }
| void reoProfileWidthStart | ( | reo_man * | p | ) |
Function********************************************************************
Synopsis [Start the profile for the BDD width. Complexity of the algorithm is O(N + n).]
Description [TopRef is the first level, on which the given node counts towards the width of the BDDs. (In other words, it is the level of the referencing node plus 1.)]
SideEffects []
SeeAlso []
Definition at line 127 of file reoProfile.c.
00128 { 00129 reo_unit * pUnit; 00130 int * pWidthStart; 00131 int * pWidthStop; 00132 int v; 00133 00134 // allocate and clean the storage for starting and stopping levels 00135 pWidthStart = ALLOC( int, p->nSupp + 1 ); 00136 pWidthStop = ALLOC( int, p->nSupp + 1 ); 00137 memset( pWidthStart, 0, sizeof(int) * (p->nSupp + 1) ); 00138 memset( pWidthStop, 0, sizeof(int) * (p->nSupp + 1) ); 00139 00140 // go through the non-constant nodes and set the topmost level of their cofactors 00141 for ( v = 0; v <= p->nSupp; v++ ) 00142 for ( pUnit = p->pPlanes[v].pHead; pUnit; pUnit = pUnit->Next ) 00143 { 00144 pUnit->TopRef = REO_TOPREF_UNDEF; 00145 pUnit->Sign = 0; 00146 } 00147 00148 // add the topmost level of the width profile 00149 for ( v = 0; v < p->nTops; v++ ) 00150 { 00151 pUnit = Unit_Regular(p->pTops[v]); 00152 if ( pUnit->TopRef == REO_TOPREF_UNDEF ) 00153 { 00154 // set the starting level 00155 pUnit->TopRef = 0; 00156 pWidthStart[pUnit->TopRef]++; 00157 // set the stopping level 00158 if ( pUnit->lev != REO_CONST_LEVEL ) 00159 pWidthStop[pUnit->lev+1]++; 00160 } 00161 } 00162 00163 for ( v = 0; v < p->nSupp; v++ ) 00164 for ( pUnit = p->pPlanes[v].pHead; pUnit; pUnit = pUnit->Next ) 00165 { 00166 if ( pUnit->pE->TopRef == REO_TOPREF_UNDEF ) 00167 { 00168 // set the starting level 00169 pUnit->pE->TopRef = pUnit->lev + 1; 00170 pWidthStart[pUnit->pE->TopRef]++; 00171 // set the stopping level 00172 if ( pUnit->pE->lev != REO_CONST_LEVEL ) 00173 pWidthStop[pUnit->pE->lev+1]++; 00174 } 00175 if ( pUnit->pT->TopRef == REO_TOPREF_UNDEF ) 00176 { 00177 // set the starting level 00178 pUnit->pT->TopRef = pUnit->lev + 1; 00179 pWidthStart[pUnit->pT->TopRef]++; 00180 // set the stopping level 00181 if ( pUnit->pT->lev != REO_CONST_LEVEL ) 00182 pWidthStop[pUnit->pT->lev+1]++; 00183 } 00184 } 00185 00186 // verify the top reference 00187 for ( v = 0; v < p->nSupp; v++ ) 00188 reoProfileWidthVerifyLevel( p->pPlanes + v, v ); 00189 00190 // derive the profile 00191 p->nWidthCur = 0; 00192 for ( v = 0; v <= p->nSupp; v++ ) 00193 { 00194 if ( v == 0 ) 00195 p->pPlanes[v].statsWidth = pWidthStart[v] - pWidthStop[v]; 00196 else 00197 p->pPlanes[v].statsWidth = p->pPlanes[v-1].statsWidth + pWidthStart[v] - pWidthStop[v]; 00198 p->pPlanes[v].statsCost = p->pPlanes[v].statsWidth; 00199 p->nWidthCur += p->pPlanes[v].statsWidth; 00200 // printf( "Level %2d: Width = %5d. Correct = %d.\n", v, Temp, p->pPlanes[v].statsWidth ); 00201 } 00202 p->nWidthBeg = p->nWidthCur; 00203 free( pWidthStart ); 00204 free( pWidthStop ); 00205 }
| void reoProfileWidthStart2 | ( | reo_man * | p | ) |
Function********************************************************************
Synopsis [Start the profile for the BDD width. Complexity of the algorithm is O(N * n).]
Description [TopRef is the first level, on which the given node counts towards the width of the BDDs. (In other words, it is the level of the referencing node plus 1.)]
SideEffects []
SeeAlso []
Definition at line 219 of file reoProfile.c.
00220 { 00221 reo_unit * pUnit; 00222 int i, v; 00223 00224 // clean the profile 00225 for ( i = 0; i <= p->nSupp; i++ ) 00226 p->pPlanes[i].statsWidth = 0; 00227 00228 // clean the node structures 00229 for ( v = 0; v <= p->nSupp; v++ ) 00230 for ( pUnit = p->pPlanes[v].pHead; pUnit; pUnit = pUnit->Next ) 00231 { 00232 pUnit->TopRef = REO_TOPREF_UNDEF; 00233 pUnit->Sign = 0; 00234 } 00235 00236 // set the topref to the topmost nodes 00237 for ( i = 0; i < p->nTops; i++ ) 00238 Unit_Regular(p->pTops[i])->TopRef = 0; 00239 00240 // go through the non-constant nodes and set the topmost level of their cofactors 00241 for ( i = 0; i < p->nSupp; i++ ) 00242 for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next ) 00243 { 00244 if ( pUnit->pE->TopRef > i+1 ) 00245 pUnit->pE->TopRef = i+1; 00246 if ( pUnit->pT->TopRef > i+1 ) 00247 pUnit->pT->TopRef = i+1; 00248 } 00249 00250 // verify the top reference 00251 for ( i = 0; i < p->nSupp; i++ ) 00252 reoProfileWidthVerifyLevel( p->pPlanes + i, i ); 00253 00254 // compute the profile for the internal nodes 00255 for ( i = 0; i < p->nSupp; i++ ) 00256 for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next ) 00257 for ( v = pUnit->TopRef; v <= pUnit->lev; v++ ) 00258 p->pPlanes[v].statsWidth++; 00259 00260 // compute the profile for the constant nodes 00261 for ( pUnit = p->pPlanes[p->nSupp].pHead; pUnit; pUnit = pUnit->Next ) 00262 for ( v = pUnit->TopRef; v <= p->nSupp; v++ ) 00263 p->pPlanes[v].statsWidth++; 00264 00265 // get the width cost 00266 p->nWidthCur = 0; 00267 for ( i = 0; i <= p->nSupp; i++ ) 00268 { 00269 p->pPlanes[i].statsCost = p->pPlanes[i].statsWidth; 00270 p->nWidthCur += p->pPlanes[i].statsWidth; 00271 } 00272 p->nWidthBeg = p->nWidthCur; 00273 }
| void reoProfileWidthVerifyLevel | ( | reo_plane * | pPlane, | |
| int | Level | |||
| ) |
Function********************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 351 of file reoProfile.c.
| void reoReorderArray | ( | reo_man * | p, | |
| DdManager * | dd, | |||
| DdNode * | Funcs[], | |||
| DdNode * | FuncsRes[], | |||
| int | nFuncs, | |||
| int * | pOrder | |||
| ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 49 of file reoCore.c.
00050 { 00051 int Counter, i; 00052 00053 // set the initial parameters 00054 p->dd = dd; 00055 p->pOrder = pOrder; 00056 p->nTops = nFuncs; 00057 // get the initial number of nodes 00058 p->nNodesBeg = Cudd_SharingSize( Funcs, nFuncs ); 00059 // resize the internal data structures of the manager if necessary 00060 reoResizeStructures( p, ddMax(dd->size,dd->sizeZ), p->nNodesBeg, nFuncs ); 00061 // compute the support 00062 p->pSupp = Extra_VectorSupportArray( dd, Funcs, nFuncs, p->pSupp ); 00063 // get the number of support variables 00064 p->nSupp = 0; 00065 for ( i = 0; i < dd->size; i++ ) 00066 p->nSupp += p->pSupp[i]; 00067 00068 // if it is the constant function, no need to reorder 00069 if ( p->nSupp == 0 ) 00070 { 00071 for ( i = 0; i < nFuncs; i++ ) 00072 { 00073 FuncsRes[i] = Funcs[i]; Cudd_Ref( FuncsRes[i] ); 00074 } 00075 return; 00076 } 00077 00078 // create the internal variable maps 00079 // go through variable levels in the manager 00080 Counter = 0; 00081 for ( i = 0; i < dd->size; i++ ) 00082 if ( p->pSupp[ dd->invperm[i] ] ) 00083 { 00084 p->pMapToPlanes[ dd->invperm[i] ] = Counter; 00085 p->pMapToDdVarsOrig[Counter] = dd->invperm[i]; 00086 if ( !p->fRemapUp ) 00087 p->pMapToDdVarsFinal[Counter] = dd->invperm[i]; 00088 else 00089 p->pMapToDdVarsFinal[Counter] = dd->invperm[Counter]; 00090 p->pOrderInt[Counter] = Counter; 00091 Counter++; 00092 } 00093 00094 // set the initial parameters 00095 p->nUnitsUsed = 0; 00096 p->nNodesCur = 0; 00097 p->fThisIsAdd = 0; 00098 p->Signature++; 00099 // transfer the function from the CUDD package into REO"s internal data structure 00100 for ( i = 0; i < nFuncs; i++ ) 00101 p->pTops[i] = reoTransferNodesToUnits_rec( p, Funcs[i] ); 00102 assert( p->nNodesBeg == p->nNodesCur ); 00103 00104 if ( !p->fThisIsAdd && p->fMinWidth ) 00105 { 00106 printf( "An important message from the REO reordering engine:\n" ); 00107 printf( "The BDD given to the engine for reordering contains complemented edges.\n" ); 00108 printf( "Currently, such BDDs cannot be reordered for the minimum width.\n" ); 00109 printf( "Therefore, minimization for the number of BDD nodes is performed.\n" ); 00110 fflush( stdout ); 00111 p->fMinApl = 0; 00112 p->fMinWidth = 0; 00113 } 00114 00115 if ( p->fMinWidth ) 00116 reoProfileWidthStart(p); 00117 else if ( p->fMinApl ) 00118 reoProfileAplStart(p); 00119 else 00120 reoProfileNodesStart(p); 00121 00122 if ( p->fVerbose ) 00123 { 00124 printf( "INITIAL: " ); 00125 if ( p->fMinWidth ) 00126 reoProfileWidthPrint(p); 00127 else if ( p->fMinApl ) 00128 reoProfileAplPrint(p); 00129 else 00130 reoProfileNodesPrint(p); 00131 } 00132 00134 // performs the reordering 00135 p->nSwaps = 0; 00136 p->nNISwaps = 0; 00137 for ( i = 0; i < p->nIters; i++ ) 00138 { 00139 reoReorderSift( p ); 00140 // print statistics after each iteration 00141 if ( p->fVerbose ) 00142 { 00143 printf( "ITER #%d: ", i+1 ); 00144 if ( p->fMinWidth ) 00145 reoProfileWidthPrint(p); 00146 else if ( p->fMinApl ) 00147 reoProfileAplPrint(p); 00148 else 00149 reoProfileNodesPrint(p); 00150 } 00151 // if the cost function did not change, stop iterating 00152 if ( p->fMinWidth ) 00153 { 00154 p->nWidthEnd = p->nWidthCur; 00155 assert( p->nWidthEnd <= p->nWidthBeg ); 00156 if ( p->nWidthEnd == p->nWidthBeg ) 00157 break; 00158 } 00159 else if ( p->fMinApl ) 00160 { 00161 p->nAplEnd = p->nAplCur; 00162 assert( p->nAplEnd <= p->nAplBeg ); 00163 if ( p->nAplEnd == p->nAplBeg ) 00164 break; 00165 } 00166 else 00167 { 00168 p->nNodesEnd = p->nNodesCur; 00169 assert( p->nNodesEnd <= p->nNodesBeg ); 00170 if ( p->nNodesEnd == p->nNodesBeg ) 00171 break; 00172 } 00173 } 00174 assert( reoCheckLevels( p ) ); 00176 00177 s_AplBefore = p->nAplBeg; 00178 s_AplAfter = p->nAplEnd; 00179 00180 // set the initial parameters 00181 p->nRefNodes = 0; 00182 p->nNodesCur = 0; 00183 p->Signature++; 00184 // transfer the BDDs from REO's internal data structure to CUDD 00185 for ( i = 0; i < nFuncs; i++ ) 00186 { 00187 FuncsRes[i] = reoTransferUnitsToNodes_rec( p, p->pTops[i] ); Cudd_Ref( FuncsRes[i] ); 00188 } 00189 // undo the DDs referenced for storing in the cache 00190 for ( i = 0; i < p->nRefNodes; i++ ) 00191 Cudd_RecursiveDeref( dd, p->pRefNodes[i] ); 00192 // verify zero refs of the terminal nodes 00193 for ( i = 0; i < nFuncs; i++ ) 00194 { 00195 assert( reoRecursiveDeref( p->pTops[i] ) ); 00196 } 00197 assert( reoCheckZeroRefs( &(p->pPlanes[p->nSupp]) ) ); 00198 00199 // prepare the variable map to return to the user 00200 if ( p->pOrder ) 00201 { 00202 // i is the current level in the planes data structure 00203 // p->pOrderInt[i] is the original level in the planes data structure 00204 // p->pMapToDdVarsOrig[i] is the variable, into which we remap when we construct the BDD from planes 00205 // p->pMapToDdVarsOrig[ p->pOrderInt[i] ] is the original BDD variable corresponding to this level 00206 // Therefore, p->pOrder[ p->pMapToDdVarsFinal[i] ] = p->pMapToDdVarsOrig[ p->pOrderInt[i] ] 00207 // creates the permutation, which remaps the resulting BDD variable into the original BDD variable 00208 for ( i = 0; i < p->nSupp; i++ ) 00209 p->pOrder[ p->pMapToDdVarsFinal[i] ] = p->pMapToDdVarsOrig[ p->pOrderInt[i] ]; 00210 } 00211 00212 if ( p->fVerify ) 00213 { 00214 int fVerification; 00215 DdNode * FuncRemapped; 00216 int * pOrder; 00217 00218 if ( p->pOrder == NULL ) 00219 { 00220 pOrder = ALLOC( int, p->nSupp ); 00221 for ( i = 0; i < p->nSupp; i++ ) 00222 pOrder[ p->pMapToDdVarsFinal[i] ] = p->pMapToDdVarsOrig[ p->pOrderInt[i] ]; 00223 } 00224 else 00225 pOrder = p->pOrder; 00226 00227 fVerification = 1; 00228 for ( i = 0; i < nFuncs; i++ ) 00229 { 00230 // verify the result 00231 if ( p->fThisIsAdd ) 00232 FuncRemapped = Cudd_addPermute( dd, FuncsRes[i], pOrder ); 00233 else 00234 FuncRemapped = Cudd_bddPermute( dd, FuncsRes[i], pOrder ); 00235 Cudd_Ref( FuncRemapped ); 00236 00237 if ( FuncRemapped != Funcs[i] ) 00238 { 00239 fVerification = 0; 00240 printf( "REO: Internal verification has failed!\n" ); 00241 fflush( stdout ); 00242 } 00243 Cudd_RecursiveDeref( dd, FuncRemapped ); 00244 } 00245 if ( fVerification ) 00246 printf( "REO: Internal verification is okay!\n" ); 00247 00248 if ( p->pOrder == NULL ) 00249 free( pOrder ); 00250 } 00251 00252 // recycle the data structure 00253 for ( i = 0; i <= p->nSupp; i++ ) 00254 reoUnitsRecycleUnitList( p, p->pPlanes + i ); 00255 }
| void reoReorderSift | ( | reo_man * | p | ) |
CFile****************************************************************
FileName [reoSift.c]
PackageName [REO: A specialized DD reordering engine.]
Synopsis [Implementation of the sifting algorihtm.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - October 15, 2002.]
Revision [
- Id
- reoSift.c,v 1.0 2002/15/10 03:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Implements the variable sifting algorithm.]
Description [Performs a sequence of adjacent variable swaps known as "sifting". Uses the cost functions determined by the flag.]
SideEffects []
SeeAlso []
Definition at line 41 of file reoSift.c.
00042 { 00043 double CostCurrent; // the cost of the current permutation 00044 double CostLimit; // the maximum increase in cost that can be tolerated 00045 double CostBest; // the best cost 00046 int BestQ; // the best position 00047 int VarCurrent; // the current variable to move 00048 int q; // denotes the current position of the variable 00049 int c; // performs the loops over variables until all of them are sifted 00050 int v; // used for other purposes 00051 00052 assert( p->nSupp > 0 ); 00053 00054 // set the current cost depending on the minimization criteria 00055 if ( p->fMinWidth ) 00056 CostCurrent = p->nWidthCur; 00057 else if ( p->fMinApl ) 00058 CostCurrent = p->nAplCur; 00059 else 00060 CostCurrent = p->nNodesCur; 00061 00062 // find the upper bound on tbe cost growth 00063 CostLimit = 1 + (int)(REO_REORDER_LIMIT * CostCurrent); 00064 00065 // perform sifting for each of p->nSupp variables 00066 for ( c = 0; c < p->nSupp; c++ ) 00067 { 00068 // select the current variable to be the one with the largest number of nodes that is not sifted yet 00069 VarCurrent = -1; 00070 CostBest = -1.0; 00071 for ( v = 0; v < p->nSupp; v++ ) 00072 { 00073 p->pVarCosts[v] = REO_HIGH_VALUE; 00074 if ( !p->pPlanes[v].fSifted ) 00075 { 00076 // VarCurrent = v; 00077 // if ( CostBest < p->pPlanes[v].statsCost ) 00078 if ( CostBest < p->pPlanes[v].statsNodes ) 00079 { 00080 // CostBest = p->pPlanes[v].statsCost; 00081 CostBest = p->pPlanes[v].statsNodes; 00082 VarCurrent = v; 00083 } 00084 00085 } 00086 } 00087 assert( VarCurrent != -1 ); 00088 // mark this variable as sifted 00089 p->pPlanes[VarCurrent].fSifted = 1; 00090 00091 // set the current value 00092 p->pVarCosts[VarCurrent] = CostCurrent; 00093 00094 // set the best cost 00095 CostBest = CostCurrent; 00096 BestQ = VarCurrent; 00097 00098 // determine which way to move the variable first (up or down) 00099 // the rationale is that if we move the shorter way first 00100 // it is more likely that the best position will be found on the longer way 00101 // and the reverse movement (to take the best position) will be faster 00102 if ( VarCurrent < p->nSupp/2 ) // move up first, then down 00103 { 00104 // set the total cost on all levels above the current level 00105 p->pPlanes[0].statsCostAbove = 0; 00106 for ( v = 1; v <= VarCurrent; v++ ) 00107 p->pPlanes[v].statsCostAbove = p->pPlanes[v-1].statsCostAbove + p->pPlanes[v-1].statsCost; 00108 // set the total cost on all levels below the current level 00109 p->pPlanes[p->nSupp].statsCostBelow = 0; 00110 for ( v = p->nSupp - 1; v >= VarCurrent; v-- ) 00111 p->pPlanes[v].statsCostBelow = p->pPlanes[v+1].statsCostBelow + p->pPlanes[v+1].statsCost; 00112 00113 assert( CostCurrent == p->pPlanes[VarCurrent].statsCostAbove + 00114 p->pPlanes[VarCurrent].statsCost + 00115 p->pPlanes[VarCurrent].statsCostBelow ); 00116 00117 // move up 00118 for ( q = VarCurrent-1; q >= 0; q-- ) 00119 { 00120 CostCurrent -= reoReorderSwapAdjacentVars( p, q, 1 ); 00121 // now q points to the position of this var in the order 00122 p->pVarCosts[q] = CostCurrent; 00123 // update the lower bound (assuming that for level q+1 it is set correctly) 00124 p->pPlanes[q].statsCostBelow = p->pPlanes[q+1].statsCostBelow + p->pPlanes[q+1].statsCost; 00125 // check the upper bound 00126 if ( CostCurrent >= CostLimit ) 00127 break; 00128 // check the lower bound 00129 if ( p->pPlanes[q].statsCostBelow + (REO_QUAL_PAR-1)*p->pPlanes[q].statsCostAbove/REO_QUAL_PAR >= CostBest ) 00130 break; 00131 // update the best cost 00132 if ( CostBest > CostCurrent ) 00133 { 00134 CostBest = CostCurrent; 00135 BestQ = q; 00136 // adjust node limit 00137 CostLimit = ddMin( CostLimit, 1 + (int)(REO_REORDER_LIMIT * CostCurrent) ); 00138 } 00139 00140 // when we are reordering for width or APL, it may happen that 00141 // the number of nodes has grown above certain limit, 00142 // in which case we have to resize the data structures 00143 if ( p->fMinWidth || p->fMinApl ) 00144 { 00145 if ( p->nNodesCur >= 2 * p->nNodesMaxAlloc ) 00146 { 00147 // printf( "Resizing data structures. Old size = %6d. New size = %6d.\n", p->nNodesMaxAlloc, p->nNodesCur ); 00148 reoResizeStructures( p, 0, p->nNodesCur, 0 ); 00149 } 00150 } 00151 } 00152 // fix the plane index 00153 if ( q == -1 ) 00154 q++; 00155 // now p points to the position of this var in the order 00156 00157 // move down 00158 for ( ; q < p->nSupp-1; ) 00159 { 00160 CostCurrent -= reoReorderSwapAdjacentVars( p, q, 0 ); 00161 q++; // change q to point to the position of this var in the order 00162 // sanity check: the number of nodes on the back pass should be the same 00163 if ( p->pVarCosts[q] != REO_HIGH_VALUE && fabs( p->pVarCosts[q] - CostCurrent ) > REO_COST_EPSILON ) 00164 printf("reoReorderSift(): Error! On the backward move, the costs are different.\n"); 00165 p->pVarCosts[q] = CostCurrent; 00166 // update the lower bound (assuming that for level q-1 it is set correctly) 00167 p->pPlanes[q].statsCostAbove = p->pPlanes[q-1].statsCostAbove + p->pPlanes[q-1].statsCost; 00168 // check the bounds only if the variable already reached its previous position 00169 if ( q >= BestQ ) 00170 { 00171 // check the upper bound 00172 if ( CostCurrent >= CostLimit ) 00173 break; 00174 // check the lower bound 00175 if ( p->pPlanes[q].statsCostAbove + (REO_QUAL_PAR-1)*p->pPlanes[q].statsCostBelow/REO_QUAL_PAR >= CostBest ) 00176 break; 00177 } 00178 // update the best cost 00179 if ( CostBest >= CostCurrent ) 00180 { 00181 CostBest = CostCurrent; 00182 BestQ = q; 00183 // adjust node limit 00184 CostLimit = ddMin( CostLimit, 1 + (int)(REO_REORDER_LIMIT * CostCurrent) ); 00185 } 00186 00187 // when we are reordering for width or APL, it may happen that 00188 // the number of nodes has grown above certain limit, 00189 // in which case we have to resize the data structures 00190 if ( p->fMinWidth || p->fMinApl ) 00191 { 00192 if ( p->nNodesCur >= 2 * p->nNodesMaxAlloc ) 00193 { 00194 // printf( "Resizing data structures. Old size = %6d. New size = %6d.\n", p->nNodesMaxAlloc, p->nNodesCur ); 00195 reoResizeStructures( p, 0, p->nNodesCur, 0 ); 00196 } 00197 } 00198 } 00199 // move the variable up from the given position (q) to the best position (BestQ) 00200 assert( q >= BestQ ); 00201 for ( ; q > BestQ; q-- ) 00202 { 00203 CostCurrent -= reoReorderSwapAdjacentVars( p, q-1, 1 ); 00204 // sanity check: the number of nodes on the back pass should be the same 00205 if ( fabs( p->pVarCosts[q-1] - CostCurrent ) > REO_COST_EPSILON ) 00206 { 00207 printf("reoReorderSift(): Error! On the return move, the costs are different.\n" ); 00208 fflush(stdout); 00209 } 00210 } 00211 } 00212 else // move down first, then up 00213 { 00214 // set the current number of nodes on all levels above the given level 00215 p->pPlanes[0].statsCostAbove = 0; 00216 for ( v = 1; v <= VarCurrent; v++ ) 00217 p->pPlanes[v].statsCostAbove = p->pPlanes[v-1].statsCostAbove + p->pPlanes[v-1].statsCost; 00218 // set the current number of nodes on all levels below the given level 00219 p->pPlanes[p->nSupp].statsCostBelow = 0; 00220 for ( v = p->nSupp - 1; v >= VarCurrent; v-- ) 00221 p->pPlanes[v].statsCostBelow = p->pPlanes[v+1].statsCostBelow + p->pPlanes[v+1].statsCost; 00222 00223 assert( CostCurrent == p->pPlanes[VarCurrent].statsCostAbove + 00224 p->pPlanes[VarCurrent].statsCost + 00225 p->pPlanes[VarCurrent].statsCostBelow ); 00226 00227 // move down 00228 for ( q = VarCurrent; q < p->nSupp-1; ) 00229 { 00230 CostCurrent -= reoReorderSwapAdjacentVars( p, q, 0 ); 00231 q++; // change q to point to the position of this var in the order 00232 p->pVarCosts[q] = CostCurrent; 00233 // update the lower bound (assuming that for level q-1 it is set correctly) 00234 p->pPlanes[q].statsCostAbove = p->pPlanes[q-1].statsCostAbove + p->pPlanes[q-1].statsCost; 00235 // check the upper bound 00236 if ( CostCurrent >= CostLimit ) 00237 break; 00238 // check the lower bound 00239 if ( p->pPlanes[q].statsCostAbove + (REO_QUAL_PAR-1)*p->pPlanes[q].statsCostBelow/REO_QUAL_PAR >= CostBest ) 00240 break; 00241 // update the best cost 00242 if ( CostBest > CostCurrent ) 00243 { 00244 CostBest = CostCurrent; 00245 BestQ = q; 00246 // adjust node limit 00247 CostLimit = ddMin( CostLimit, 1 + (int)(REO_REORDER_LIMIT * CostCurrent) ); 00248 } 00249 00250 // when we are reordering for width or APL, it may happen that 00251 // the number of nodes has grown above certain limit, 00252 // in which case we have to resize the data structures 00253 if ( p->fMinWidth || p->fMinApl ) 00254 { 00255 if ( p->nNodesCur >= 2 * p->nNodesMaxAlloc ) 00256 { 00257 // printf( "Resizing data structures. Old size = %6d. New size = %6d.\n", p->nNodesMaxAlloc, p->nNodesCur ); 00258 reoResizeStructures( p, 0, p->nNodesCur, 0 ); 00259 } 00260 } 00261 } 00262 00263 // move up 00264 for ( --q; q >= 0; q-- ) 00265 { 00266 CostCurrent -= reoReorderSwapAdjacentVars( p, q, 1 ); 00267 // now q points to the position of this var in the order 00268 // sanity check: the number of nodes on the back pass should be the same 00269 if ( p->pVarCosts[q] != REO_HIGH_VALUE && fabs( p->pVarCosts[q] - CostCurrent ) > REO_COST_EPSILON ) 00270 printf("reoReorderSift(): Error! On the backward move, the costs are different.\n"); 00271 p->pVarCosts[q] = CostCurrent; 00272 // update the lower bound (assuming that for level q+1 it is set correctly) 00273 p->pPlanes[q].statsCostBelow = p->pPlanes[q+1].statsCostBelow + p->pPlanes[q+1].statsCost; 00274 // check the bounds only if the variable already reached its previous position 00275 if ( q <= BestQ ) 00276 { 00277 // check the upper bound 00278 if ( CostCurrent >= CostLimit ) 00279 break; 00280 // check the lower bound 00281 if ( p->pPlanes[q].statsCostBelow + (REO_QUAL_PAR-1)*p->pPlanes[q].statsCostAbove/REO_QUAL_PAR >= CostBest ) 00282 break; 00283 } 00284 // update the best cost 00285 if ( CostBest >= CostCurrent ) 00286 { 00287 CostBest = CostCurrent; 00288 BestQ = q; 00289 // adjust node limit 00290 CostLimit = ddMin( CostLimit, 1 + (int)(REO_REORDER_LIMIT * CostCurrent) ); 00291 } 00292 00293 // when we are reordering for width or APL, it may happen that 00294 // the number of nodes has grown above certain limit, 00295 // in which case we have to resize the data structures 00296 if ( p->fMinWidth || p->fMinApl ) 00297 { 00298 if ( p->nNodesCur >= 2 * p->nNodesMaxAlloc ) 00299 { 00300 // printf( "Resizing data structures. Old size = %6d. New size = %6d.\n", p->nNodesMaxAlloc, p->nNodesCur ); 00301 reoResizeStructures( p, 0, p->nNodesCur, 0 ); 00302 } 00303 } 00304 } 00305 // fix the plane index 00306 if ( q == -1 ) 00307 q++; 00308 // now q points to the position of this var in the order 00309 // move the variable down from the given position (q) to the best position (BestQ) 00310 assert( q <= BestQ ); 00311 for ( ; q < BestQ; q++ ) 00312 { 00313 CostCurrent -= reoReorderSwapAdjacentVars( p, q, 0 ); 00314 // sanity check: the number of nodes on the back pass should be the same 00315 if ( fabs( p->pVarCosts[q+1] - CostCurrent ) > REO_COST_EPSILON ) 00316 { 00317 printf("reoReorderSift(): Error! On the return move, the costs are different.\n" ); 00318 fflush(stdout); 00319 } 00320 } 00321 } 00322 assert( fabs( CostBest - CostCurrent ) < REO_COST_EPSILON ); 00323 00324 // update the cost 00325 if ( p->fMinWidth ) 00326 p->nWidthCur = (int)CostBest; 00327 else if ( p->fMinApl ) 00328 p->nAplCur = CostCurrent; 00329 else 00330 p->nNodesCur = (int)CostBest; 00331 } 00332 00333 // remove the sifted attributes if any 00334 for ( v = 0; v < p->nSupp; v++ ) 00335 p->pPlanes[v].fSifted = 0; 00336 }
| double reoReorderSwapAdjacentVars | ( | reo_man * | p, | |
| int | lev0, | |||
| int | fMovingUp | |||
| ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis []
Description [Takes the level (lev0) of the plane, which should be swapped with the next plane. Returns the gain using the current cost function.]
SideEffects []
SeeAlso []
Definition at line 43 of file reoSwap.c.
00044 { 00045 // the levels in the decision diagram 00046 int lev1 = lev0 + 1, lev2 = lev0 + 2; 00047 // the new nodes on lev0 00048 reo_unit * pLoop, * pUnit; 00049 // the new nodes on lev1 00050 reo_unit * pNewPlane20, * pNewPlane21, * pNewPlane20R; 00051 reo_unit * pUnitE, * pUnitER, * pUnitT; 00052 // the nodes below lev1 00053 reo_unit * pNew1E, * pNew1T, * pNew2E, * pNew2T; 00054 reo_unit * pNew1ER, * pNew2ER; 00055 // the old linked lists 00056 reo_unit * pListOld0 = p->pPlanes[lev0].pHead; 00057 reo_unit * pListOld1 = p->pPlanes[lev1].pHead; 00058 // working planes and one more temporary plane 00059 reo_unit * pListNew0 = NULL, ** ppListNew0 = &pListNew0; 00060 reo_unit * pListNew1 = NULL, ** ppListNew1 = &pListNew1; 00061 reo_unit * pListTemp = NULL, ** ppListTemp = &pListTemp; 00062 // various integer variables 00063 int fComp, fCompT, fFound, nWidthCofs, HKey, fInteract, temp, c; 00064 // statistical variables 00065 int nNodesUpMovedDown = 0; 00066 int nNodesDownMovedUp = 0; 00067 int nNodesUnrefRemoved = 0; 00068 int nNodesUnrefAdded = 0; 00069 int nWidthReduction = 0; 00070 double AplWeightTotalLev0; 00071 double AplWeightTotalLev1; 00072 double AplWeightHalf; 00073 double AplWeightPrev; 00074 double AplWeightAfter; 00075 double nCostGain; 00076 00077 // set the old lists 00078 assert( lev0 >= 0 && lev1 < p->nSupp ); 00079 pListOld0 = p->pPlanes[lev0].pHead; 00080 pListOld1 = p->pPlanes[lev1].pHead; 00081 00082 // make sure the planes have nodes 00083 assert( p->pPlanes[lev0].statsNodes && p->pPlanes[lev1].statsNodes ); 00084 assert( pListOld0 && pListOld1 ); 00085 00086 if ( p->fMinWidth ) 00087 { 00088 // verify that the width parameters are set correctly 00089 reoProfileWidthVerifyLevel( p->pPlanes + lev0, lev0 ); 00090 reoProfileWidthVerifyLevel( p->pPlanes + lev1, lev1 ); 00091 // start the storage for cofactors 00092 nWidthCofs = 0; 00093 } 00094 else if ( p->fMinApl ) 00095 { 00096 AplWeightPrev = p->nAplCur; 00097 AplWeightAfter = p->nAplCur; 00098 AplWeightTotalLev0 = 0.0; 00099 AplWeightTotalLev1 = 0.0; 00100 } 00101 00102 // check if the planes interact 00103 fInteract = 0; // assume that they do not interact 00104 for ( pUnit = pListOld0; pUnit; pUnit = pUnit->Next ) 00105 { 00106 if ( pUnit->pT->lev == lev1 || Unit_Regular(pUnit->pE)->lev == lev1 ) 00107 { 00108 fInteract = 1; 00109 break; 00110 } 00111 // change the level now, this is done for efficiency reasons 00112 pUnit->lev = lev1; 00113 } 00114 00115 // set the new signature for hashing 00116 p->nSwaps++; 00117 if ( !fInteract ) 00118 // if ( 0 ) 00119 { 00120 // perform the swap without interaction 00121 p->nNISwaps++; 00122 00123 // change the levels 00124 if ( p->fMinWidth ) 00125 { 00126 // go through the current lower level, which will become upper 00127 for ( pUnit = pListOld1; pUnit; pUnit = pUnit->Next ) 00128 { 00129 pUnit->lev = lev0; 00130 00131 pUnitER = Unit_Regular(pUnit->pE); 00132 if ( pUnitER->TopRef > lev0 ) 00133 { 00134 if ( pUnitER->Sign != p->nSwaps ) 00135 { 00136 if ( pUnitER->TopRef == lev2 ) 00137 { 00138 pUnitER->TopRef = lev1; 00139 nWidthReduction--; 00140 } 00141 else 00142 { 00143 assert( pUnitER->TopRef == lev1 ); 00144 } 00145 pUnitER->Sign = p->nSwaps; 00146 } 00147 } 00148 00149 pUnitT = pUnit->pT; 00150 if ( pUnitT->TopRef > lev0 ) 00151 { 00152 if ( pUnitT->Sign != p->nSwaps ) 00153 { 00154 if ( pUnitT->TopRef == lev2 ) 00155 { 00156 pUnitT->TopRef = lev1; 00157 nWidthReduction--; 00158 } 00159 else 00160 { 00161 assert( pUnitT->TopRef == lev1 ); 00162 } 00163 pUnitT->Sign = p->nSwaps; 00164 } 00165 } 00166 00167 } 00168 00169 // go through the current upper level, which will become lower 00170 for ( pUnit = pListOld0; pUnit; pUnit = pUnit->Next ) 00171 { 00172 pUnit->lev = lev1; 00173 00174 pUnitER = Unit_Regular(pUnit->pE); 00175 if ( pUnitER->TopRef > lev0 ) 00176 { 00177 if ( pUnitER->Sign != p->nSwaps ) 00178 { 00179 assert( pUnitER->TopRef == lev1 ); 00180 pUnitER->TopRef = lev2; 00181 pUnitER->Sign = p->nSwaps; 00182 nWidthReduction++; 00183 } 00184 } 00185 00186 pUnitT = pUnit->pT; 00187 if ( pUnitT->TopRef > lev0 ) 00188 { 00189 if ( pUnitT->Sign != p->nSwaps ) 00190 { 00191 assert( pUnitT->TopRef == lev1 ); 00192 pUnitT->TopRef = lev2; 00193 pUnitT->Sign = p->nSwaps; 00194 nWidthReduction++; 00195 } 00196 } 00197 } 00198 } 00199 else 00200 { 00201 // for ( pUnit = pListOld0; pUnit; pUnit = pUnit->Next ) 00202 // pUnit->lev = lev1; 00203 for ( pUnit = pListOld1; pUnit; pUnit = pUnit->Next ) 00204 pUnit->lev = lev0; 00205 } 00206 00207 // set the new linked lists, which will be attached to the planes 00208 pListNew0 = pListOld1; 00209 pListNew1 = pListOld0; 00210 00211 if ( p->fMinApl ) 00212 { 00213 AplWeightTotalLev0 = p->pPlanes[lev1].statsCost; 00214 AplWeightTotalLev1 = p->pPlanes[lev0].statsCost; 00215 } 00216 00217 // set the changes in terms of nodes 00218 nNodesUpMovedDown = p->pPlanes[lev0].statsNodes; 00219 nNodesDownMovedUp = p->pPlanes[lev1].statsNodes; 00220 goto finish; 00221 } 00222 p->Signature++; 00223 00224 00225 // two-variable swap is done in three easy steps 00226 // previously I thought that steps (1) and (2) can be merged into one step 00227 // now it is clear that this cannot be done without changing a lot of other stuff... 00228 00229 // (1) walk through the upper level, find units without cofactors in the lower level 00230 // and move them to the new lower level (while adding to the cache) 00231 // (2) walk through the uppoer level, and tranform all the remaning nodes 00232 // while employing cache for the new lower level 00233 // (3) walk through the old lower level, find those nodes whose ref counters are not zero, 00234 // and move them to the new uppoer level, free other nodes 00235 00236 // (1) walk through the upper level, find units without cofactors in the lower level 00237 // and move them to the new lower level (while adding to the cache) 00238 for ( pLoop = pListOld0; pLoop; ) 00239 { 00240 pUnit = pLoop; 00241 pLoop = pLoop->Next; 00242 00243 pUnitE = pUnit->pE; 00244 pUnitER = Unit_Regular(pUnitE); 00245 pUnitT = pUnit->pT; 00246 00247 if ( pUnitER->lev != lev1 && pUnitT->lev != lev1 ) 00248 { 00249 // before after 00250 // 00251 // <p1> 00252 // 0 / \ 1 00253 // / \ 00254 // / \ 00255 // / \ <p2n> 00256 // / \ 0 / \ 1 00257 // / \ / \ 00258 // / \ / \ 00259 // F0 F1 F0 F1 00260 00261 // move to plane-2-new 00262 // nothing changes in the process (cofactors, ref counter, APL weight) 00263 pUnit->lev = lev1; 00264 AddToLinkedList( ppListNew1, pUnit ); 00265 if ( p->fMinApl ) 00266 AplWeightTotalLev1 += pUnit->Weight; 00267 00268 // add to cache - find the cell with different signature (not the current one!) 00269 for ( HKey = hashKey3(p->Signature, pUnitE, pUnitT, p->nTableSize); 00270 p->HTable[HKey].Sign == p->Signature; 00271 HKey = (HKey+1) % p->nTableSize ); 00272 assert( p->HTable[HKey].Sign != p->Signature ); 00273 p->HTable[HKey].Sign = p->Signature; 00274 p->HTable[HKey].Arg1 = pUnitE; 00275 p->HTable[HKey].Arg2 = pUnitT; 00276 p->HTable[HKey].Arg3 = pUnit; 00277 00278 nNodesUpMovedDown++; 00279 00280 if ( p->fMinWidth ) 00281 { 00282 // update the cofactors's top ref 00283 if ( pUnitER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00284 { 00285 assert( pUnitER->TopRef == lev1 ); 00286 pUnitER->TopRefNew = lev2; 00287 if ( pUnitER->Sign != p->nSwaps ) 00288 { 00289 pUnitER->Sign = p->nSwaps; // set the current signature 00290 p->pWidthCofs[ nWidthCofs++ ] = pUnitER; 00291 } 00292 } 00293 if ( pUnitT->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00294 { 00295 assert( pUnitT->TopRef == lev1 ); 00296 pUnitT->TopRefNew = lev2; 00297 if ( pUnitT->Sign != p->nSwaps ) 00298 { 00299 pUnitT->Sign = p->nSwaps; // set the current signature 00300 p->pWidthCofs[ nWidthCofs++ ] = pUnitT; 00301 } 00302 } 00303 } 00304 } 00305 else 00306 { 00307 // add to the temporary plane 00308 AddToLinkedList( ppListTemp, pUnit ); 00309 } 00310 } 00311 00312 00313 // (2) walk through the uppoer level, and tranform all the remaning nodes 00314 // while employing cache for the new lower level 00315 for ( pLoop = pListTemp; pLoop; ) 00316 { 00317 pUnit = pLoop; 00318 pLoop = pLoop->Next; 00319 00320 pUnitE = pUnit->pE; 00321 pUnitER = Unit_Regular(pUnitE); 00322 pUnitT = pUnit->pT; 00323 fComp = (int)(pUnitER != pUnitE); 00324 00325 // count the amount of weight to reduce the APL of the children of this node 00326 if ( p->fMinApl ) 00327 AplWeightHalf = 0.5 * pUnit->Weight; 00328 00329 // determine what situation is this 00330 if ( pUnitER->lev == lev1 && pUnitT->lev == lev1 ) 00331 { 00332 if ( fComp == 0 ) 00333 { 00334 // before after 00335 // 00336 // <p1> <p1n> 00337 // 0 / \ 1 0 / \ 1 00338 // / \ / \ 00339 // / \ / \ 00340 // <p2> <p2> <p2n> <p2n> 00341 // 0 / \ 1 0 / \ 1 0 / \ 1 0 / \ 1 00342 // / \ / \ / \ / \ 00343 // / \ / \ / \ / \ 00344 // F0 F1 F2 F3 F0 F2 F1 F3 00345 // pNew1E pNew1T pNew2E pNew2T 00346 // 00347 pNew1E = pUnitE->pE; // F0 00348 pNew1T = pUnitT->pE; // F2 00349 00350 pNew2E = pUnitE->pT; // F1 00351 pNew2T = pUnitT->pT; // F3 00352 } 00353 else 00354 { 00355 // before after 00356 // 00357 // <p1> <p1n> 00358 // 0 . \ 1 0 / \ 1 00359 // . \ / \ 00360 // . \ / \ 00361 // <p2> <p2> <p2n> <p2n> 00362 // 0 / \ 1 0 / \ 1 0 . \ 1 0 . \ 1 00363 // / \ / \ . \ . \ 00364 // / \ / \ . \ . \ 00365 // F0 F1 F2 F3 F0 F2 F1 F3 00366 // pNew1E pNew1T pNew2E pNew2T 00367 // 00368 pNew1E = Unit_Not(pUnitER->pE); // F0 00369 pNew1T = pUnitT->pE; // F2 00370 00371 pNew2E = Unit_Not(pUnitER->pT); // F1 00372 pNew2T = pUnitT->pT; // F3 00373 } 00374 // subtract ref counters - on the level P2 00375 pUnitER->n--; 00376 pUnitT->n--; 00377 00378 // mark the change in the APL weights 00379 if ( p->fMinApl ) 00380 { 00381 pUnitER->Weight -= AplWeightHalf; 00382 pUnitT->Weight -= AplWeightHalf; 00383 AplWeightAfter -= pUnit->Weight; 00384 } 00385 } 00386 else if ( pUnitER->lev == lev1 ) 00387 { 00388 if ( fComp == 0 ) 00389 { 00390 // before after 00391 // 00392 // <p1> <p1n> 00393 // 0 / \ 1 0 / \ 1 00394 // / \ / \ 00395 // / \ / \ 00396 // <p2> \ <p2n> <p2n> 00397 // 0 / \ 1 \ 0 / \ 1 0 / \ 1 00398 // / \ \ / \ / \ 00399 // / \ \ / \ / \ 00400 // F0 F1 F3 F0 F3 F1 F3 00401 // pNew1E pNew1T pNew2E pNew2T 00402 // 00403 pNew1E = pUnitER->pE; // F0 00404 pNew1T = pUnitT; // F3 00405 00406 pNew2E = pUnitER->pT; // F1 00407 pNew2T = pUnitT; // F3 00408 } 00409 else 00410 { 00411 // before after 00412 // 00413 // <p1> <p1n> 00414 // 0 . \ 1 0 / \ 1 00415 // . \ / \ 00416 // . \ / \ 00417 // <p2> \ <p2n> <p2n> 00418 // 0 / \ 1 \ 0 . \ 1 0 . \ 1 00419 // / \ \ . \ . \ 00420 // / \ \ . \ . \ 00421 // F0 F1 F3 F0 F3 F1 F3 00422 // pNew1E pNew1T pNew2E pNew2T 00423 // 00424 pNew1E = Unit_Not(pUnitER->pE); // F0 00425 pNew1T = pUnitT; // F3 00426 00427 pNew2E = Unit_Not(pUnitER->pT); // F1 00428 pNew2T = pUnitT; // F3 00429 } 00430 // subtract ref counter - on the level P2 00431 pUnitER->n--; 00432 // subtract ref counter - on other levels 00433 pUnitT->n--; 00434 00435 // mark the change in the APL weights 00436 if ( p->fMinApl ) 00437 { 00438 pUnitER->Weight -= AplWeightHalf; 00439 AplWeightAfter -= AplWeightHalf; 00440 } 00441 } 00442 else if ( pUnitT->lev == lev1 ) 00443 { 00444 // before after 00445 // 00446 // <p1> <p1n> 00447 // 0 / \ 1 0 / \ 1 00448 // / \ / \ 00449 // / \ / \ 00450 // / <p2> <p2n> <p2n> 00451 // / 0 / \ 1 0 / \ 1 0 / \ 1 00452 // / / \ / \ / \ 00453 // / / \ / \ / \ 00454 // F0 F2 F3 F0 F2 F0 F3 00455 // pNew1E pNew1T pNew2E pNew2T 00456 // 00457 pNew1E = pUnitE; // F0 00458 pNew1T = pUnitT->pE; // F2 00459 00460 pNew2E = pUnitE; // F0 00461 pNew2T = pUnitT->pT; // F3 00462 00463 // subtract incoming edge counter - on the level P2 00464 pUnitT->n--; 00465 // subtract ref counter - on other levels 00466 pUnitER->n--; 00467 00468 // mark the change in the APL weights 00469 if ( p->fMinApl ) 00470 { 00471 pUnitT->Weight -= AplWeightHalf; 00472 AplWeightAfter -= AplWeightHalf; 00473 } 00474 } 00475 else 00476 { 00477 assert( 0 ); // should never happen 00478 } 00479 00480 00481 // consider all the cases except the last one 00482 if ( pNew1E == pNew1T ) 00483 { 00484 pNewPlane20 = pNew1T; 00485 00486 if ( p->fMinWidth ) 00487 { 00488 // update the cofactors's top ref 00489 if ( pNew1T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00490 { 00491 pNew1T->TopRefNew = lev1; 00492 if ( pNew1T->Sign != p->nSwaps ) 00493 { 00494 pNew1T->Sign = p->nSwaps; // set the current signature 00495 p->pWidthCofs[ nWidthCofs++ ] = pNew1T; 00496 } 00497 } 00498 } 00499 } 00500 else 00501 { 00502 // pNew1T can be complemented 00503 fCompT = Cudd_IsComplement(pNew1T); 00504 if ( fCompT ) 00505 { 00506 pNew1E = Unit_Not(pNew1E); 00507 pNew1T = Unit_Not(pNew1T); 00508 } 00509 00510 // check the hash-table 00511 fFound = 0; 00512 for ( HKey = hashKey3(p->Signature, pNew1E, pNew1T, p->nTableSize); 00513 p->HTable[HKey].Sign == p->Signature; 00514 HKey = (HKey+1) % p->nTableSize ) 00515 if ( p->HTable[HKey].Arg1 == pNew1E && p->HTable[HKey].Arg2 == pNew1T ) 00516 { // the entry is present 00517 // assign this entry 00518 pNewPlane20 = p->HTable[HKey].Arg3; 00519 assert( pNewPlane20->lev == lev1 ); 00520 fFound = 1; 00521 p->HashSuccess++; 00522 break; 00523 } 00524 00525 if ( !fFound ) 00526 { // create the new entry 00527 pNewPlane20 = reoUnitsGetNextUnit( p ); // increments the unit counter 00528 pNewPlane20->pE = pNew1E; 00529 pNewPlane20->pT = pNew1T; 00530 pNewPlane20->n = 0; // ref will be added later 00531 pNewPlane20->lev = lev1; 00532 if ( p->fMinWidth ) 00533 { 00534 pNewPlane20->TopRef = lev1; 00535 pNewPlane20->Sign = 0; 00536 } 00537 // set the weight of this node 00538 if ( p->fMinApl ) 00539 pNewPlane20->Weight = 0.0; 00540 00541 // increment ref counters of children 00542 pNew1ER = Unit_Regular(pNew1E); 00543 pNew1ER->n++; // 00544 pNew1T->n++; // 00545 00546 // insert into the data structure 00547 AddToLinkedList( ppListNew1, pNewPlane20 ); 00548 00549 // add this entry to cache 00550 assert( p->HTable[HKey].Sign != p->Signature ); 00551 p->HTable[HKey].Sign = p->Signature; 00552 p->HTable[HKey].Arg1 = pNew1E; 00553 p->HTable[HKey].Arg2 = pNew1T; 00554 p->HTable[HKey].Arg3 = pNewPlane20; 00555 00556 nNodesUnrefAdded++; 00557 00558 if ( p->fMinWidth ) 00559 { 00560 // update the cofactors's top ref 00561 if ( pNew1ER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00562 { 00563 if ( pNew1ER->Sign != p->nSwaps ) 00564 { 00565 pNew1ER->TopRefNew = lev2; 00566 if ( pNew1ER->Sign != p->nSwaps ) 00567 { 00568 pNew1ER->Sign = p->nSwaps; // set the current signature 00569 p->pWidthCofs[ nWidthCofs++ ] = pNew1ER; 00570 } 00571 } 00572 // otherwise the level is already set correctly 00573 else 00574 { 00575 assert( pNew1ER->TopRefNew == lev1 || pNew1ER->TopRefNew == lev2 ); 00576 } 00577 } 00578 // update the cofactors's top ref 00579 if ( pNew1T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00580 { 00581 if ( pNew1T->Sign != p->nSwaps ) 00582 { 00583 pNew1T->TopRefNew = lev2; 00584 if ( pNew1T->Sign != p->nSwaps ) 00585 { 00586 pNew1T->Sign = p->nSwaps; // set the current signature 00587 p->pWidthCofs[ nWidthCofs++ ] = pNew1T; 00588 } 00589 } 00590 // otherwise the level is already set correctly 00591 else 00592 { 00593 assert( pNew1T->TopRefNew == lev1 || pNew1T->TopRefNew == lev2 ); 00594 } 00595 } 00596 } 00597 } 00598 00599 if ( p->fMinApl ) 00600 { 00601 // increment the weight of this node 00602 pNewPlane20->Weight += AplWeightHalf; 00603 // mark the change in the APL weight 00604 AplWeightAfter += AplWeightHalf; 00605 // update the total weight of this level 00606 AplWeightTotalLev1 += AplWeightHalf; 00607 } 00608 00609 if ( fCompT ) 00610 pNewPlane20 = Unit_Not(pNewPlane20); 00611 } 00612 00613 if ( pNew2E == pNew2T ) 00614 { 00615 pNewPlane21 = pNew2T; 00616 00617 if ( p->fMinWidth ) 00618 { 00619 // update the cofactors's top ref 00620 if ( pNew2T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00621 { 00622 pNew2T->TopRefNew = lev1; 00623 if ( pNew2T->Sign != p->nSwaps ) 00624 { 00625 pNew2T->Sign = p->nSwaps; // set the current signature 00626 p->pWidthCofs[ nWidthCofs++ ] = pNew2T; 00627 } 00628 } 00629 } 00630 } 00631 else 00632 { 00633 assert( !Cudd_IsComplement(pNew2T) ); 00634 00635 // check the hash-table 00636 fFound = 0; 00637 for ( HKey = hashKey3(p->Signature, pNew2E, pNew2T, p->nTableSize); 00638 p->HTable[HKey].Sign == p->Signature; 00639 HKey = (HKey+1) % p->nTableSize ) 00640 if ( p->HTable[HKey].Arg1 == pNew2E && p->HTable[HKey].Arg2 == pNew2T ) 00641 { // the entry is present 00642 // assign this entry 00643 pNewPlane21 = p->HTable[HKey].Arg3; 00644 assert( pNewPlane21->lev == lev1 ); 00645 fFound = 1; 00646 p->HashSuccess++; 00647 break; 00648 } 00649 00650 if ( !fFound ) 00651 { // create the new entry 00652 pNewPlane21 = reoUnitsGetNextUnit( p ); // increments the unit counter 00653 pNewPlane21->pE = pNew2E; 00654 pNewPlane21->pT = pNew2T; 00655 pNewPlane21->n = 0; // ref will be added later 00656 pNewPlane21->lev = lev1; 00657 if ( p->fMinWidth ) 00658 { 00659 pNewPlane21->TopRef = lev1; 00660 pNewPlane21->Sign = 0; 00661 } 00662 // set the weight of this node 00663 if ( p->fMinApl ) 00664 pNewPlane21->Weight = 0.0; 00665 00666 // increment ref counters of children 00667 pNew2ER = Unit_Regular(pNew2E); 00668 pNew2ER->n++; // 00669 pNew2T->n++; // 00670 00671 // insert into the data structure 00672 // reoUnitsAddUnitToPlane( &P2new, pNewPlane21 ); 00673 AddToLinkedList( ppListNew1, pNewPlane21 ); 00674 00675 // add this entry to cache 00676 assert( p->HTable[HKey].Sign != p->Signature ); 00677 p->HTable[HKey].Sign = p->Signature; 00678 p->HTable[HKey].Arg1 = pNew2E; 00679 p->HTable[HKey].Arg2 = pNew2T; 00680 p->HTable[HKey].Arg3 = pNewPlane21; 00681 00682 nNodesUnrefAdded++; 00683 00684 00685 if ( p->fMinWidth ) 00686 { 00687 // update the cofactors's top ref 00688 if ( pNew2ER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00689 { 00690 if ( pNew2ER->Sign != p->nSwaps ) 00691 { 00692 pNew2ER->TopRefNew = lev2; 00693 if ( pNew2ER->Sign != p->nSwaps ) 00694 { 00695 pNew2ER->Sign = p->nSwaps; // set the current signature 00696 p->pWidthCofs[ nWidthCofs++ ] = pNew2ER; 00697 } 00698 } 00699 // otherwise the level is already set correctly 00700 else 00701 { 00702 assert( pNew2ER->TopRefNew == lev1 || pNew2ER->TopRefNew == lev2 ); 00703 } 00704 } 00705 // update the cofactors's top ref 00706 if ( pNew2T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00707 { 00708 if ( pNew2T->Sign != p->nSwaps ) 00709 { 00710 pNew2T->TopRefNew = lev2; 00711 if ( pNew2T->Sign != p->nSwaps ) 00712 { 00713 pNew2T->Sign = p->nSwaps; // set the current signature 00714 p->pWidthCofs[ nWidthCofs++ ] = pNew2T; 00715 } 00716 } 00717 // otherwise the level is already set correctly 00718 else 00719 { 00720 assert( pNew2T->TopRefNew == lev1 || pNew2T->TopRefNew == lev2 ); 00721 } 00722 } 00723 } 00724 } 00725 00726 if ( p->fMinApl ) 00727 { 00728 // increment the weight of this node 00729 pNewPlane21->Weight += AplWeightHalf; 00730 // mark the change in the APL weight 00731 AplWeightAfter += AplWeightHalf; 00732 // update the total weight of this level 00733 AplWeightTotalLev1 += AplWeightHalf; 00734 } 00735 } 00736 // in all cases, the node will be added to the plane-1 00737 // this should be the same node (pUnit) as was originally there 00738 // because it is referenced by the above nodes 00739 00740 assert( !Cudd_IsComplement(pNewPlane21) ); 00741 // should be the case; otherwise reordering is not a local operation 00742 00743 pUnit->pE = pNewPlane20; 00744 pUnit->pT = pNewPlane21; 00745 assert( pUnit->lev == lev0 ); 00746 // reference counter remains the same; the APL weight remains the same 00747 00748 // increment ref counters of children 00749 pNewPlane20R = Unit_Regular(pNewPlane20); 00750 pNewPlane20R->n++; 00751 pNewPlane21->n++; 00752 00753 // insert into the data structure 00754 AddToLinkedList( ppListNew0, pUnit ); 00755 if ( p->fMinApl ) 00756 AplWeightTotalLev0 += pUnit->Weight; 00757 } 00758 00759 // (3) walk through the old lower level, find those nodes whose ref counters are not zero, 00760 // and move them to the new uppoer level, free other nodes 00761 for ( pLoop = pListOld1; pLoop; ) 00762 { 00763 pUnit = pLoop; 00764 pLoop = pLoop->Next; 00765 if ( pUnit->n ) 00766 { 00767 assert( !p->fMinApl || pUnit->Weight > 0.0 ); 00768 // the node should be added to the new level 00769 // no need to check the hash table 00770 pUnit->lev = lev0; 00771 AddToLinkedList( ppListNew0, pUnit ); 00772 if ( p->fMinApl ) 00773 AplWeightTotalLev0 += pUnit->Weight; 00774 00775 nNodesDownMovedUp++; 00776 00777 if ( p->fMinWidth ) 00778 { 00779 pUnitER = Unit_Regular(pUnit->pE); 00780 pUnitT = pUnit->pT; 00781 00782 // update the cofactors's top ref 00783 if ( pUnitER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00784 { 00785 pUnitER->TopRefNew = lev1; 00786 if ( pUnitER->Sign != p->nSwaps ) 00787 { 00788 pUnitER->Sign = p->nSwaps; // set the current signature 00789 p->pWidthCofs[ nWidthCofs++ ] = pUnitER; 00790 } 00791 } 00792 if ( pUnitT->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00793 { 00794 pUnitT->TopRefNew = lev1; 00795 if ( pUnitT->Sign != p->nSwaps ) 00796 { 00797 pUnitT->Sign = p->nSwaps; // set the current signature 00798 p->pWidthCofs[ nWidthCofs++ ] = pUnitT; 00799 } 00800 } 00801 } 00802 } 00803 else 00804 { 00805 assert( !p->fMinApl || pUnit->Weight == 0.0 ); 00806 // decrement reference counters of children 00807 pUnitER = Unit_Regular(pUnit->pE); 00808 pUnitT = pUnit->pT; 00809 pUnitER->n--; 00810 pUnitT->n--; 00811 // the node should be thrown away 00812 reoUnitsRecycleUnit( p, pUnit ); 00813 nNodesUnrefRemoved++; 00814 } 00815 } 00816 00817 finish: 00818 00819 // attach the new levels to the planes 00820 p->pPlanes[lev0].pHead = pListNew0; 00821 p->pPlanes[lev1].pHead = pListNew1; 00822 00823 // swap the sift status 00824 temp = p->pPlanes[lev0].fSifted; 00825 p->pPlanes[lev0].fSifted = p->pPlanes[lev1].fSifted; 00826 p->pPlanes[lev1].fSifted = temp; 00827 00828 // swap variables in the variable map 00829 if ( p->pOrderInt ) 00830 { 00831 temp = p->pOrderInt[lev0]; 00832 p->pOrderInt[lev0] = p->pOrderInt[lev1]; 00833 p->pOrderInt[lev1] = temp; 00834 } 00835 00836 // adjust the node profile 00837 p->pPlanes[lev0].statsNodes -= (nNodesUpMovedDown - nNodesDownMovedUp); 00838 p->pPlanes[lev1].statsNodes -= (nNodesDownMovedUp - nNodesUpMovedDown) + nNodesUnrefRemoved - nNodesUnrefAdded; 00839 p->nNodesCur -= nNodesUnrefRemoved - nNodesUnrefAdded; 00840 00841 // adjust the node profile on this level 00842 if ( p->fMinWidth ) 00843 { 00844 for ( c = 0; c < nWidthCofs; c++ ) 00845 { 00846 if ( p->pWidthCofs[c]->TopRefNew < p->pWidthCofs[c]->TopRef ) 00847 { 00848 p->pWidthCofs[c]->TopRef = p->pWidthCofs[c]->TopRefNew; 00849 nWidthReduction--; 00850 } 00851 else if ( p->pWidthCofs[c]->TopRefNew > p->pWidthCofs[c]->TopRef ) 00852 { 00853 p->pWidthCofs[c]->TopRef = p->pWidthCofs[c]->TopRefNew; 00854 nWidthReduction++; 00855 } 00856 } 00857 // verify that the profile is okay 00858 reoProfileWidthVerifyLevel( p->pPlanes + lev0, lev0 ); 00859 reoProfileWidthVerifyLevel( p->pPlanes + lev1, lev1 ); 00860 00861 // compute the total gain in terms of width 00862 nCostGain = (nNodesDownMovedUp - nNodesUpMovedDown + nNodesUnrefRemoved - nNodesUnrefAdded) + nWidthReduction; 00863 // adjust the width on this level 00864 p->pPlanes[lev1].statsWidth -= (int)nCostGain; 00865 // set the cost 00866 p->pPlanes[lev1].statsCost = p->pPlanes[lev1].statsWidth; 00867 } 00868 else if ( p->fMinApl ) 00869 { 00870 // compute the total gain in terms of APL 00871 nCostGain = AplWeightPrev - AplWeightAfter; 00872 // make sure that the ALP is updated correctly 00873 // assert( p->pPlanes[lev0].statsCost + p->pPlanes[lev1].statsCost - nCostGain == 00874 // AplWeightTotalLev0 + AplWeightTotalLev1 ); 00875 // adjust the profile 00876 p->pPlanes[lev0].statsApl = AplWeightTotalLev0; 00877 p->pPlanes[lev1].statsApl = AplWeightTotalLev1; 00878 // set the cost 00879 p->pPlanes[lev0].statsCost = p->pPlanes[lev0].statsApl; 00880 p->pPlanes[lev1].statsCost = p->pPlanes[lev1].statsApl; 00881 } 00882 else 00883 { 00884 // compute the total gain in terms of the number of nodes 00885 nCostGain = nNodesUnrefRemoved - nNodesUnrefAdded; 00886 // adjust the profile (adjusted above) 00887 // set the cost 00888 p->pPlanes[lev0].statsCost = p->pPlanes[lev0].statsNodes; 00889 p->pPlanes[lev1].statsCost = p->pPlanes[lev1].statsNodes; 00890 } 00891 00892 return nCostGain; 00893 }
| void reoResizeStructures | ( | reo_man * | p, | |
| int | nDdVarsMax, | |||
| int | nNodesMax, | |||
| int | nFuncs | |||
| ) |
Function*************************************************************
Synopsis [Resizes the internal manager data structures.]
Description []
SideEffects []
SeeAlso []
Definition at line 268 of file reoCore.c.
00269 { 00270 // resize data structures depending on the number of variables in the DD manager 00271 if ( p->nSuppAlloc == 0 ) 00272 { 00273 p->pSupp = ALLOC( int, nDdVarsMax + 1 ); 00274 p->pOrderInt = ALLOC( int, nDdVarsMax + 1 ); 00275 p->pMapToPlanes = ALLOC( int, nDdVarsMax + 1 ); 00276 p->pMapToDdVarsOrig = ALLOC( int, nDdVarsMax + 1 ); 00277 p->pMapToDdVarsFinal = ALLOC( int, nDdVarsMax + 1 ); 00278 p->pPlanes = CALLOC( reo_plane, nDdVarsMax + 1 ); 00279 p->pVarCosts = ALLOC( double, nDdVarsMax + 1 ); 00280 p->pLevelOrder = ALLOC( int, nDdVarsMax + 1 ); 00281 p->nSuppAlloc = nDdVarsMax + 1; 00282 } 00283 else if ( p->nSuppAlloc < nDdVarsMax ) 00284 { 00285 free( p->pSupp ); 00286 free( p->pOrderInt ); 00287 free( p->pMapToPlanes ); 00288 free( p->pMapToDdVarsOrig ); 00289 free( p->pMapToDdVarsFinal ); 00290 free( p->pPlanes ); 00291 free( p->pVarCosts ); 00292 free( p->pLevelOrder ); 00293 00294 p->pSupp = ALLOC( int, nDdVarsMax + 1 ); 00295 p->pOrderInt = ALLOC( int, nDdVarsMax + 1 ); 00296 p->pMapToPlanes = ALLOC( int, nDdVarsMax + 1 ); 00297 p->pMapToDdVarsOrig = ALLOC( int, nDdVarsMax + 1 ); 00298 p->pMapToDdVarsFinal = ALLOC( int, nDdVarsMax + 1 ); 00299 p->pPlanes = CALLOC( reo_plane, nDdVarsMax + 1 ); 00300 p->pVarCosts = ALLOC( double, nDdVarsMax + 1 ); 00301 p->pLevelOrder = ALLOC( int, nDdVarsMax + 1 ); 00302 p->nSuppAlloc = nDdVarsMax + 1; 00303 } 00304 00305 // resize the data structures depending on the number of nodes 00306 if ( p->nRefNodesAlloc == 0 ) 00307 { 00308 p->nNodesMaxAlloc = nNodesMax; 00309 p->nTableSize = 3*nNodesMax + 1; 00310 p->nRefNodesAlloc = 3*nNodesMax + 1; 00311 p->nMemChunksAlloc = (10*nNodesMax + 1)/REO_CHUNK_SIZE + 1; 00312 00313 p->HTable = CALLOC( reo_hash, p->nTableSize ); 00314 p->pRefNodes = ALLOC( DdNode *, p->nRefNodesAlloc ); 00315 p->pWidthCofs = ALLOC( reo_unit *, p->nRefNodesAlloc ); 00316 p->pMemChunks = ALLOC( reo_unit *, p->nMemChunksAlloc ); 00317 } 00318 else if ( p->nNodesMaxAlloc < nNodesMax ) 00319 { 00320 void * pTemp; 00321 int nMemChunksAllocPrev = p->nMemChunksAlloc; 00322 00323 p->nNodesMaxAlloc = nNodesMax; 00324 p->nTableSize = 3*nNodesMax + 1; 00325 p->nRefNodesAlloc = 3*nNodesMax + 1; 00326 p->nMemChunksAlloc = (10*nNodesMax + 1)/REO_CHUNK_SIZE + 1; 00327 00328 free( p->HTable ); 00329 free( p->pRefNodes ); 00330 free( p->pWidthCofs ); 00331 p->HTable = CALLOC( reo_hash, p->nTableSize ); 00332 p->pRefNodes = ALLOC( DdNode *, p->nRefNodesAlloc ); 00333 p->pWidthCofs = ALLOC( reo_unit *, p->nRefNodesAlloc ); 00334 // p->pMemChunks should be reallocated because it contains pointers currently in use 00335 pTemp = ALLOC( reo_unit *, p->nMemChunksAlloc ); 00336 memmove( pTemp, p->pMemChunks, sizeof(reo_unit *) * nMemChunksAllocPrev ); 00337 free( p->pMemChunks ); 00338 p->pMemChunks = pTemp; 00339 } 00340 00341 // resize the data structures depending on the number of functions 00342 if ( p->nTopsAlloc == 0 ) 00343 { 00344 p->pTops = ALLOC( reo_unit *, nFuncs ); 00345 p->nTopsAlloc = nFuncs; 00346 } 00347 else if ( p->nTopsAlloc < nFuncs ) 00348 { 00349 free( p->pTops ); 00350 p->pTops = ALLOC( reo_unit *, nFuncs ); 00351 p->nTopsAlloc = nFuncs; 00352 } 00353 }
CFile****************************************************************
FileName [reoTransfer.c]
PackageName [REO: A specialized DD reordering engine.]
Synopsis [Transfering a DD from the CUDD manager into REOs 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
] 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 []
Definition at line 40 of file reoTransfer.c.
00041 { 00042 DdManager * dd = p->dd; 00043 reo_unit * pUnit; 00044 int HKey, fComp; 00045 00046 fComp = Cudd_IsComplement(F); 00047 F = Cudd_Regular(F); 00048 00049 // check the hash-table 00050 if ( F->ref != 1 ) 00051 { 00052 // search cache - use linear probing 00053 for ( HKey = hashKey2(p->Signature,F,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize ) 00054 if ( p->HTable[HKey].Arg1 == (reo_unit *)F ) 00055 { 00056 pUnit = p->HTable[HKey].Arg2; 00057 assert( pUnit ); 00058 // increment the edge counter 00059 pUnit->n++; 00060 return Unit_NotCond( pUnit, fComp ); 00061 } 00062 } 00063 // the entry in not found in the cache 00064 00065 // create a new entry 00066 pUnit = reoUnitsGetNextUnit( p ); 00067 pUnit->n = 1; 00068 if ( cuddIsConstant(F) ) 00069 { 00070 pUnit->lev = REO_CONST_LEVEL; 00071 pUnit->pE = (reo_unit*)((int)(cuddV(F))); 00072 pUnit->pT = NULL; 00073 // check if the diagram that is being reordering has complement edges 00074 if ( F != dd->one ) 00075 p->fThisIsAdd = 1; 00076 // insert the unit into the corresponding plane 00077 reoUnitsAddUnitToPlane( &(p->pPlanes[p->nSupp]), pUnit ); // increments the unit counter 00078 } 00079 else 00080 { 00081 pUnit->lev = p->pMapToPlanes[F->index]; 00082 pUnit->pE = reoTransferNodesToUnits_rec( p, cuddE(F) ); 00083 pUnit->pT = reoTransferNodesToUnits_rec( p, cuddT(F) ); 00084 // insert the unit into the corresponding plane 00085 reoUnitsAddUnitToPlane( &(p->pPlanes[pUnit->lev]), pUnit ); // increments the unit counter 00086 } 00087 00088 // add to the hash table 00089 if ( F->ref != 1 ) 00090 { 00091 // the next free entry is already found - it is pointed to by HKey 00092 // while we traversed the diagram, the hash entry to which HKey points, 00093 // might have been used. Make sure that its signature is different. 00094 for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize ); 00095 p->HTable[HKey].Sign = p->Signature; 00096 p->HTable[HKey].Arg1 = (reo_unit *)F; 00097 p->HTable[HKey].Arg2 = pUnit; 00098 } 00099 00100 // increment the counter of nodes 00101 p->nNodesCur++; 00102 return Unit_NotCond( pUnit, fComp ); 00103 }
Function*************************************************************
Synopsis [Creates the DD from the internal reordering data structure.]
Description [It is important that the hash table is lossless.]
SideEffects []
SeeAlso []
Definition at line 116 of file reoTransfer.c.
00117 { 00118 DdManager * dd = p->dd; 00119 DdNode * bRes, * E, * T; 00120 int HKey, fComp; 00121 00122 fComp = Cudd_IsComplement(pUnit); 00123 pUnit = Unit_Regular(pUnit); 00124 00125 // check the hash-table 00126 if ( pUnit->n != 1 ) 00127 { 00128 for ( HKey = hashKey2(p->Signature,pUnit,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize ) 00129 if ( p->HTable[HKey].Arg1 == pUnit ) 00130 { 00131 bRes = (DdNode*) p->HTable[HKey].Arg2; 00132 assert( bRes ); 00133 return Cudd_NotCond( bRes, fComp ); 00134 } 00135 } 00136 00137 // treat the case of constants 00138 if ( Unit_IsConstant(pUnit) ) 00139 { 00140 bRes = cuddUniqueConst( dd, ((double)((int)(pUnit->pE))) ); 00141 cuddRef( bRes ); 00142 } 00143 else 00144 { 00145 // split and recur on children of this node 00146 E = reoTransferUnitsToNodes_rec( p, pUnit->pE ); 00147 if ( E == NULL ) 00148 return NULL; 00149 cuddRef(E); 00150 00151 T = reoTransferUnitsToNodes_rec( p, pUnit->pT ); 00152 if ( T == NULL ) 00153 { 00154 Cudd_RecursiveDeref(dd, E); 00155 return NULL; 00156 } 00157 cuddRef(T); 00158 00159 // consider the case when Res0 and Res1 are the same node 00160 assert( E != T ); 00161 assert( !Cudd_IsComplement(T) ); 00162 00163 bRes = cuddUniqueInter( dd, p->pMapToDdVarsFinal[pUnit->lev], T, E ); 00164 if ( bRes == NULL ) 00165 { 00166 Cudd_RecursiveDeref(dd,E); 00167 Cudd_RecursiveDeref(dd,T); 00168 return NULL; 00169 } 00170 cuddRef( bRes ); 00171 cuddDeref( E ); 00172 cuddDeref( T ); 00173 } 00174 00175 // do not keep the result if the ref count is only 1, since it will not be visited again 00176 if ( pUnit->n != 1 ) 00177 { 00178 // while we traversed the diagram, the hash entry to which HKey points, 00179 // might have been used. Make sure that its signature is different. 00180 for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize ); 00181 p->HTable[HKey].Sign = p->Signature; 00182 p->HTable[HKey].Arg1 = pUnit; 00183 p->HTable[HKey].Arg2 = (reo_unit *)bRes; 00184 00185 // add the DD to the referenced DD list in order to be able to store it in cache 00186 p->pRefNodes[p->nRefNodes++] = bRes; Cudd_Ref( bRes ); 00187 // no need to do this, because the garbage collection will not take bRes away 00188 // it is held by the diagram in the making 00189 } 00190 // increment the counter of nodes 00191 p->nNodesCur++; 00192 cuddDeref( bRes ); 00193 return Cudd_NotCond( bRes, fComp ); 00194 }
Function*************************************************************
Synopsis [Adds one unit to the list of units which constitutes the plane.]
Description []
SideEffects []
SeeAlso []
Definition at line 131 of file reoUnits.c.
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Extract the next unit from the free unit list.]
Description []
SideEffects []
SeeAlso []
Definition at line 42 of file reoUnits.c.
00043 { 00044 reo_unit * pUnit; 00045 // check there are stil units to extract 00046 if ( p->pUnitFreeList == NULL ) 00047 reoUnitsAddToFreeUnitList( p ); 00048 // extract the next unit from the linked list 00049 pUnit = p->pUnitFreeList; 00050 p->pUnitFreeList = pUnit->Next; 00051 p->nUnitsUsed++; 00052 return pUnit; 00053 }
Function*************************************************************
Synopsis [Returns the unit to the free unit list.]
Description []
SideEffects []
SeeAlso []
Definition at line 66 of file reoUnits.c.
00067 { 00068 pUnit->Next = p->pUnitFreeList; 00069 p->pUnitFreeList = pUnit; 00070 p->nUnitsUsed--; 00071 }
Function*************************************************************
Synopsis [Returns the list of units to the free unit list.]
Description []
SideEffects []
SeeAlso []
Definition at line 84 of file reoUnits.c.
00085 { 00086 reo_unit * pUnit; 00087 reo_unit * pTail; 00088 00089 if ( pPlane->pHead == NULL ) 00090 return; 00091 00092 // find the tail 00093 for ( pUnit = pPlane->pHead; pUnit; pUnit = pUnit->Next ) 00094 pTail = pUnit; 00095 pTail->Next = p->pUnitFreeList; 00096 p->pUnitFreeList = pPlane->pHead; 00097 memset( pPlane, 0, sizeof(reo_plane) ); 00098 }
| void reoUnitsStopDispenser | ( | reo_man * | p | ) |
Function*************************************************************
Synopsis [Stops the unit dispenser.]
Description []
SideEffects []
SeeAlso []
Definition at line 111 of file reoUnits.c.
00112 { 00113 int i; 00114 for ( i = 0; i < p->nMemChunks; i++ ) 00115 free( p->pMemChunks[i] ); 00116 // printf("\nThe number of chunks used is %d, each of them %d units\n", p->nMemChunks, REO_CHUNK_SIZE ); 00117 p->nMemChunks = 0; 00118 }
