glu-2.2: src/cuBdd/cuddCompose.c Source File

00001 
00085 #include "util.h"
00086 #include "cuddInt.h"
00087 
00088 
00089 /*---------------------------------------------------------------------------*/
00090 /* Constant declarations                                                     */
00091 /*---------------------------------------------------------------------------*/
00092 
00093 /*---------------------------------------------------------------------------*/
00094 /* Stucture declarations                                                     */
00095 /*---------------------------------------------------------------------------*/
00096 
00097 /*---------------------------------------------------------------------------*/
00098 /* Type declarations                                                         */
00099 /*---------------------------------------------------------------------------*/
00100 
00101 /*---------------------------------------------------------------------------*/
00102 /* Variable declarations                                                     */
00103 /*---------------------------------------------------------------------------*/
00104 
00105 #ifndef lint
00106 static char rcsid[] DD_UNUSED = "$Id: cuddCompose.c,v 1.45 2004/08/13 18:04:47 fabio Exp $";
00107 #endif
00108 
00109 #ifdef DD_DEBUG
00110 static int addPermuteRecurHits;
00111 static int bddPermuteRecurHits;
00112 static int bddVectorComposeHits;
00113 static int addVectorComposeHits;
00114 
00115 static int addGeneralVectorComposeHits;
00116 #endif
00117 
00118 /*---------------------------------------------------------------------------*/
00119 /* Macro declarations                                                        */
00120 /*---------------------------------------------------------------------------*/
00121 
00122 
00125 /*---------------------------------------------------------------------------*/
00126 /* Static function prototypes                                                */
00127 /*---------------------------------------------------------------------------*/
00128 
00129 static DdNode * cuddAddPermuteRecur (DdManager *manager, DdHashTable *table, DdNode *node, int *permut);
00130 static DdNode * cuddBddPermuteRecur (DdManager *manager, DdHashTable *table, DdNode *node, int *permut);
00131 static DdNode * cuddBddVarMapRecur (DdManager *manager, DdNode *f);
00132 static DdNode * cuddAddVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest);
00133 static DdNode * cuddAddNonSimComposeRecur (DdManager *dd, DdNode *f, DdNode **vector, DdNode *key, DdNode *cube, int lastsub);
00134 static DdNode * cuddBddVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest);
00135 DD_INLINE static int ddIsIthAddVar (DdManager *dd, DdNode *f, unsigned int i);
00136 
00137 static DdNode * cuddAddGeneralVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vectorOn, DdNode **vectorOff, int deepest);
00138 DD_INLINE static int ddIsIthAddVarPair (DdManager *dd, DdNode *f, DdNode *g, unsigned int i);
00139 
00143 /*---------------------------------------------------------------------------*/
00144 /* Definition of exported functions                                          */
00145 /*---------------------------------------------------------------------------*/
00146 
00147 
00162 DdNode *
00163 Cudd_bddCompose(
00164   DdManager * dd,
00165   DdNode * f,
00166   DdNode * g,
00167   int  v)
00168 {
00169     DdNode *proj, *res;
00170 
00171     /* Sanity check. */
00172     if (v < 0 || v >= dd->size) return(NULL);
00173 
00174     proj =  dd->vars[v];
00175     do {
00176         dd->reordered = 0;
00177         res = cuddBddComposeRecur(dd,f,g,proj);
00178     } while (dd->reordered == 1);
00179     return(res);
00180 
00181 } /* end of Cudd_bddCompose */
00182 
00183 
00199 DdNode *
00200 Cudd_addCompose(
00201   DdManager * dd,
00202   DdNode * f,
00203   DdNode * g,
00204   int  v)
00205 {
00206     DdNode *proj, *res;
00207 
00208     /* Sanity check. */
00209     if (v < 0 || v >= dd->size) return(NULL);
00210 
00211     proj =  dd->vars[v];
00212     do {
00213         dd->reordered = 0;
00214         res = cuddAddComposeRecur(dd,f,g,proj);
00215     } while (dd->reordered == 1);
00216     return(res);
00217 
00218 } /* end of Cudd_addCompose */
00219 
00220 
00237 DdNode *
00238 Cudd_addPermute(
00239   DdManager * manager,
00240   DdNode * node,
00241   int * permut)
00242 {
00243     DdHashTable         *table;
00244     DdNode              *res;
00245 
00246     do {
00247         manager->reordered = 0;
00248         table = cuddHashTableInit(manager,1,2);
00249         if (table == NULL) return(NULL);
00250         /* Recursively solve the problem. */
00251         res = cuddAddPermuteRecur(manager,table,node,permut);
00252         if (res != NULL) cuddRef(res);
00253         /* Dispose of local cache. */
00254         cuddHashTableQuit(table);
00255     } while (manager->reordered == 1);
00256 
00257     if (res != NULL) cuddDeref(res);
00258     return(res);
00259 
00260 } /* end of Cudd_addPermute */
00261 
00262 
00278 DdNode *
00279 Cudd_addSwapVariables(
00280   DdManager * dd,
00281   DdNode * f,
00282   DdNode ** x,
00283   DdNode ** y,
00284   int  n)
00285 {
00286     DdNode *swapped;
00287     int  i, j, k;
00288     int  *permut;
00289 
00290     permut = ALLOC(int,dd->size);
00291     if (permut == NULL) {
00292         dd->errorCode = CUDD_MEMORY_OUT;
00293         return(NULL);
00294     }
00295     for (i = 0; i < dd->size; i++) permut[i] = i;
00296     for (i = 0; i < n; i++) {
00297         j = x[i]->index;
00298         k = y[i]->index;
00299         permut[j] = k;
00300         permut[k] = j;
00301     }
00302 
00303     swapped = Cudd_addPermute(dd,f,permut);
00304     FREE(permut);
00305 
00306     return(swapped);
00307 
00308 } /* end of Cudd_addSwapVariables */
00309 
00310 
00327 DdNode *
00328 Cudd_bddPermute(
00329   DdManager * manager,
00330   DdNode * node,
00331   int * permut)
00332 {
00333     DdHashTable         *table;
00334     DdNode              *res;
00335 
00336     do {
00337         manager->reordered = 0;
00338         table = cuddHashTableInit(manager,1,2);
00339         if (table == NULL) return(NULL);
00340         res = cuddBddPermuteRecur(manager,table,node,permut);
00341         if (res != NULL) cuddRef(res);
00342         /* Dispose of local cache. */
00343         cuddHashTableQuit(table);
00344 
00345     } while (manager->reordered == 1);
00346 
00347     if (res != NULL) cuddDeref(res);
00348     return(res);
00349 
00350 } /* end of Cudd_bddPermute */
00351 
00352 
00368 DdNode *
00369 Cudd_bddVarMap(
00370   DdManager * manager /* DD manager */,
00371   DdNode * f /* function in which to remap variables */)
00372 {
00373     DdNode *res;
00374 
00375     if (manager->map == NULL) return(NULL);
00376     do {
00377         manager->reordered = 0;
00378         res = cuddBddVarMapRecur(manager, f);
00379     } while (manager->reordered == 1);
00380 
00381     return(res);
00382 
00383 } /* end of Cudd_bddVarMap */
00384 
00385 
00411 int
00412 Cudd_SetVarMap (
00413   DdManager *manager /* DD manager */,
00414   DdNode **x /* first array of variables */,
00415   DdNode **y /* second array of variables */,
00416   int n /* length of both arrays */)
00417 {
00418     int i;
00419 
00420     if (manager->map != NULL) {
00421         cuddCacheFlush(manager);
00422     } else {
00423         manager->map = ALLOC(int,manager->maxSize);
00424         if (manager->map == NULL) {
00425             manager->errorCode = CUDD_MEMORY_OUT;
00426             return(0);
00427         }
00428         manager->memused += sizeof(int) * manager->maxSize;
00429     }
00430     /* Initialize the map to the identity. */
00431     for (i = 0; i < manager->size; i++) {
00432         manager->map[i] = i;
00433     }
00434     /* Create the map. */
00435     for (i = 0; i < n; i++) {
00436         manager->map[x[i]->index] = y[i]->index;
00437         manager->map[y[i]->index] = x[i]->index;
00438     }
00439     return(1);
00440 
00441 } /* end of Cudd_SetVarMap */
00442 
00443 
00459 DdNode *
00460 Cudd_bddSwapVariables(
00461   DdManager * dd,
00462   DdNode * f,
00463   DdNode ** x,
00464   DdNode ** y,
00465   int  n)
00466 {
00467     DdNode *swapped;
00468     int  i, j, k;
00469     int  *permut;
00470 
00471     permut = ALLOC(int,dd->size);
00472     if (permut == NULL) {
00473         dd->errorCode = CUDD_MEMORY_OUT;
00474         return(NULL);
00475     }
00476     for (i = 0; i < dd->size; i++) permut[i] = i;
00477     for (i = 0; i < n; i++) {
00478         j = x[i]->index;
00479         k = y[i]->index;
00480         permut[j] = k;
00481         permut[k] = j;
00482     }
00483 
00484     swapped = Cudd_bddPermute(dd,f,permut);
00485     FREE(permut);
00486 
00487     return(swapped);
00488 
00489 } /* end of Cudd_bddSwapVariables */
00490 
00491 
00507 DdNode *
00508 Cudd_bddAdjPermuteX(
00509   DdManager * dd,
00510   DdNode * B,
00511   DdNode ** x,
00512   int  n)
00513 {
00514     DdNode *swapped;
00515     int  i, j, k;
00516     int  *permut;
00517 
00518     permut = ALLOC(int,dd->size);
00519     if (permut == NULL) {
00520         dd->errorCode = CUDD_MEMORY_OUT;
00521         return(NULL);
00522     }
00523     for (i = 0; i < dd->size; i++) permut[i] = i;
00524     for (i = 0; i < n-2; i += 3) {
00525         j = x[i]->index;
00526         k = x[i+1]->index;
00527         permut[j] = k;
00528         permut[k] = j;
00529     }
00530 
00531     swapped = Cudd_bddPermute(dd,B,permut);
00532     FREE(permut);
00533 
00534     return(swapped);
00535 
00536 } /* end of Cudd_bddAdjPermuteX */
00537 
00538 
00558 DdNode *
00559 Cudd_addVectorCompose(
00560   DdManager * dd,
00561   DdNode * f,
00562   DdNode ** vector)
00563 {
00564     DdHashTable         *table;
00565     DdNode              *res;
00566     int                 deepest;
00567     int                 i;
00568 
00569     do {
00570         dd->reordered = 0;
00571         /* Initialize local cache. */
00572         table = cuddHashTableInit(dd,1,2);
00573         if (table == NULL) return(NULL);
00574 
00575         /* Find deepest real substitution. */
00576         for (deepest = dd->size - 1; deepest >= 0; deepest--) {
00577             i = dd->invperm[deepest];
00578             if (!ddIsIthAddVar(dd,vector[i],i)) {
00579                 break;
00580             }
00581         }
00582 
00583         /* Recursively solve the problem. */
00584         res = cuddAddVectorComposeRecur(dd,table,f,vector,deepest);
00585         if (res != NULL) cuddRef(res);
00586 
00587         /* Dispose of local cache. */
00588         cuddHashTableQuit(table);
00589     } while (dd->reordered == 1);
00590 
00591     if (res != NULL) cuddDeref(res);
00592     return(res);
00593 
00594 } /* end of Cudd_addVectorCompose */
00595 
00596 
00616 DdNode *
00617 Cudd_addGeneralVectorCompose(
00618   DdManager * dd,
00619   DdNode * f,
00620   DdNode ** vectorOn,
00621   DdNode ** vectorOff)
00622 {
00623     DdHashTable         *table;
00624     DdNode              *res;
00625     int                 deepest;
00626     int                 i;
00627 
00628     do {
00629         dd->reordered = 0;
00630         /* Initialize local cache. */
00631         table = cuddHashTableInit(dd,1,2);
00632         if (table == NULL) return(NULL);
00633 
00634         /* Find deepest real substitution. */
00635         for (deepest = dd->size - 1; deepest >= 0; deepest--) {
00636             i = dd->invperm[deepest];
00637             if (!ddIsIthAddVarPair(dd,vectorOn[i],vectorOff[i],i)) {
00638                 break;
00639             }
00640         }
00641 
00642         /* Recursively solve the problem. */
00643         res = cuddAddGeneralVectorComposeRecur(dd,table,f,vectorOn,
00644                                                vectorOff,deepest);
00645         if (res != NULL) cuddRef(res);
00646 
00647         /* Dispose of local cache. */
00648         cuddHashTableQuit(table);
00649     } while (dd->reordered == 1);
00650 
00651     if (res != NULL) cuddDeref(res);
00652     return(res);
00653 
00654 } /* end of Cudd_addGeneralVectorCompose */
00655 
00656 
00677 DdNode *
00678 Cudd_addNonSimCompose(
00679   DdManager * dd,
00680   DdNode * f,
00681   DdNode ** vector)
00682 {
00683     DdNode              *cube, *key, *var, *tmp, *piece;
00684     DdNode              *res;
00685     int                 i, lastsub;
00686 
00687     /* The cache entry for this function is composed of three parts:
00688     ** f itself, the replacement relation, and the cube of the
00689     ** variables being substituted.
00690     ** The replacement relation is the product of the terms (yi EXNOR gi).
00691     ** This apporach allows us to use the global cache for this function,
00692     ** with great savings in memory with respect to using arrays for the
00693     ** cache entries.
00694     ** First we build replacement relation and cube of substituted
00695     ** variables from the vector specifying the desired composition.
00696     */
00697     key = DD_ONE(dd);
00698     cuddRef(key);
00699     cube = DD_ONE(dd);
00700     cuddRef(cube);
00701     for (i = (int) dd->size - 1; i >= 0; i--) {
00702         if (ddIsIthAddVar(dd,vector[i],(unsigned int)i)) {
00703             continue;
00704         }
00705         var = Cudd_addIthVar(dd,i);
00706         if (var == NULL) {
00707             Cudd_RecursiveDeref(dd,key);
00708             Cudd_RecursiveDeref(dd,cube);
00709             return(NULL);
00710         }
00711         cuddRef(var);
00712         /* Update cube. */
00713         tmp = Cudd_addApply(dd,Cudd_addTimes,var,cube);
00714         if (tmp == NULL) {
00715             Cudd_RecursiveDeref(dd,key);
00716             Cudd_RecursiveDeref(dd,cube);
00717             Cudd_RecursiveDeref(dd,var);
00718             return(NULL);
00719         }
00720         cuddRef(tmp);
00721         Cudd_RecursiveDeref(dd,cube);
00722         cube = tmp;
00723         /* Update replacement relation. */
00724         piece = Cudd_addApply(dd,Cudd_addXnor,var,vector[i]);
00725         if (piece == NULL) {
00726             Cudd_RecursiveDeref(dd,key);
00727             Cudd_RecursiveDeref(dd,var);
00728             return(NULL);
00729         }
00730         cuddRef(piece);
00731         Cudd_RecursiveDeref(dd,var);
00732         tmp = Cudd_addApply(dd,Cudd_addTimes,key,piece);
00733         if (tmp == NULL) {
00734             Cudd_RecursiveDeref(dd,key);
00735             Cudd_RecursiveDeref(dd,piece);
00736             return(NULL);
00737         }
00738         cuddRef(tmp);
00739         Cudd_RecursiveDeref(dd,key);
00740         Cudd_RecursiveDeref(dd,piece);
00741         key = tmp;
00742     }
00743 
00744     /* Now try composition, until no reordering occurs. */
00745     do {
00746         /* Find real substitution with largest index. */
00747         for (lastsub = dd->size - 1; lastsub >= 0; lastsub--) {
00748             if (!ddIsIthAddVar(dd,vector[lastsub],(unsigned int)lastsub)) {
00749                 break;
00750             }
00751         }
00752 
00753         /* Recursively solve the problem. */
00754         dd->reordered = 0;
00755         res = cuddAddNonSimComposeRecur(dd,f,vector,key,cube,lastsub+1);
00756         if (res != NULL) cuddRef(res);
00757 
00758     } while (dd->reordered == 1);
00759 
00760     Cudd_RecursiveDeref(dd,key);
00761     Cudd_RecursiveDeref(dd,cube);
00762     if (res != NULL) cuddDeref(res);
00763     return(res);
00764 
00765 } /* end of Cudd_addNonSimCompose */
00766 
00767 
00786 DdNode *
00787 Cudd_bddVectorCompose(
00788   DdManager * dd,
00789   DdNode * f,
00790   DdNode ** vector)
00791 {
00792     DdHashTable         *table;
00793     DdNode              *res;
00794     int                 deepest;
00795     int                 i;
00796 
00797     do {
00798         dd->reordered = 0;
00799         /* Initialize local cache. */
00800         table = cuddHashTableInit(dd,1,2);
00801         if (table == NULL) return(NULL);
00802 
00803         /* Find deepest real substitution. */
00804         for (deepest = dd->size - 1; deepest >= 0; deepest--) {
00805             i = dd->invperm[deepest];
00806             if (vector[i] != dd->vars[i]) {
00807                 break;
00808             }
00809         }
00810 
00811         /* Recursively solve the problem. */
00812         res = cuddBddVectorComposeRecur(dd,table,f,vector, deepest);
00813         if (res != NULL) cuddRef(res);
00814 
00815         /* Dispose of local cache. */
00816         cuddHashTableQuit(table);
00817     } while (dd->reordered == 1);
00818 
00819     if (res != NULL) cuddDeref(res);
00820     return(res);
00821 
00822 } /* end of Cudd_bddVectorCompose */
00823 
00824 
00825 /*---------------------------------------------------------------------------*/
00826 /* Definition of internal functions                                          */
00827 /*---------------------------------------------------------------------------*/
00828 
00829 
00845 DdNode *
00846 cuddBddComposeRecur(
00847   DdManager * dd,
00848   DdNode * f,
00849   DdNode * g,
00850   DdNode * proj)
00851 {
00852     DdNode      *F, *G, *f1, *f0, *g1, *g0, *r, *t, *e;
00853     unsigned int v, topf, topg, topindex;
00854     int         comple;
00855 
00856     statLine(dd);
00857     v = dd->perm[proj->index];
00858     F = Cudd_Regular(f);
00859     topf = cuddI(dd,F->index);
00860 
00861     /* Terminal case. Subsumes the test for constant f. */
00862     if (topf > v) return(f);
00863 
00864     /* We solve the problem for a regular pointer, and then complement
00865     ** the result if the pointer was originally complemented.
00866     */
00867     comple = Cudd_IsComplement(f);
00868 
00869     /* Check cache. */
00870     r = cuddCacheLookup(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj);
00871     if (r != NULL) {
00872         return(Cudd_NotCond(r,comple));
00873     }
00874 
00875     if (topf == v) {
00876         /* Compose. */
00877         f1 = cuddT(F);
00878         f0 = cuddE(F);
00879         r = cuddBddIteRecur(dd, g, f1, f0);
00880         if (r == NULL) return(NULL);
00881     } else {
00882         /* Compute cofactors of f and g. Remember the index of the top
00883         ** variable.
00884         */
00885         G = Cudd_Regular(g);
00886         topg = cuddI(dd,G->index);
00887         if (topf > topg) {
00888             topindex = G->index;
00889             f1 = f0 = F;
00890         } else {
00891             topindex = F->index;
00892             f1 = cuddT(F);
00893             f0 = cuddE(F);
00894         }
00895         if (topg > topf) {
00896             g1 = g0 = g;
00897         } else {
00898             g1 = cuddT(G);
00899             g0 = cuddE(G);
00900             if (g != G) {
00901                 g1 = Cudd_Not(g1);
00902                 g0 = Cudd_Not(g0);
00903             }
00904         }
00905         /* Recursive step. */
00906         t = cuddBddComposeRecur(dd, f1, g1, proj);
00907         if (t == NULL) return(NULL);
00908         cuddRef(t);
00909         e = cuddBddComposeRecur(dd, f0, g0, proj);
00910         if (e == NULL) {
00911             Cudd_IterDerefBdd(dd, t);
00912             return(NULL);
00913         }
00914         cuddRef(e);
00915 
00916         r = cuddBddIteRecur(dd, dd->vars[topindex], t, e);
00917         if (r == NULL) {
00918             Cudd_IterDerefBdd(dd, t);
00919             Cudd_IterDerefBdd(dd, e);
00920             return(NULL);
00921         }
00922         cuddRef(r);
00923         Cudd_IterDerefBdd(dd, t); /* t & e not necessarily part of r */
00924         Cudd_IterDerefBdd(dd, e);
00925         cuddDeref(r);
00926     }
00927 
00928     cuddCacheInsert(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj,r);
00929 
00930     return(Cudd_NotCond(r,comple));
00931 
00932 } /* end of cuddBddComposeRecur */
00933 
00934 
00947 DdNode *
00948 cuddAddComposeRecur(
00949   DdManager * dd,
00950   DdNode * f,
00951   DdNode * g,
00952   DdNode * proj)
00953 {
00954     DdNode *f1, *f0, *g1, *g0, *r, *t, *e;
00955     unsigned int v, topf, topg, topindex;
00956 
00957     statLine(dd);
00958     v = dd->perm[proj->index];
00959     topf = cuddI(dd,f->index);
00960 
00961     /* Terminal case. Subsumes the test for constant f. */
00962     if (topf > v) return(f);
00963 
00964     /* Check cache. */
00965     r = cuddCacheLookup(dd,DD_ADD_COMPOSE_RECUR_TAG,f,g,proj);
00966     if (r != NULL) {
00967         return(r);
00968     }
00969 
00970     if (topf == v) {
00971         /* Compose. */
00972         f1 = cuddT(f);
00973         f0 = cuddE(f);
00974         r = cuddAddIteRecur(dd, g, f1, f0);
00975         if (r == NULL) return(NULL);
00976     } else {
00977         /* Compute cofactors of f and g. Remember the index of the top
00978         ** variable.
00979         */
00980         topg = cuddI(dd,g->index);
00981         if (topf > topg) {
00982             topindex = g->index;
00983             f1 = f0 = f;
00984         } else {
00985             topindex = f->index;
00986             f1 = cuddT(f);
00987             f0 = cuddE(f);
00988         }
00989         if (topg > topf) {
00990             g1 = g0 = g;
00991         } else {
00992             g1 = cuddT(g);
00993             g0 = cuddE(g);
00994         }
00995         /* Recursive step. */
00996         t = cuddAddComposeRecur(dd, f1, g1, proj);
00997         if (t == NULL) return(NULL);
00998         cuddRef(t);
00999         e = cuddAddComposeRecur(dd, f0, g0, proj);
01000         if (e == NULL) {
01001             Cudd_RecursiveDeref(dd, t);
01002             return(NULL);
01003         }
01004         cuddRef(e);
01005 
01006         if (t == e) {
01007             r = t;
01008         } else {
01009             r = cuddUniqueInter(dd, (int) topindex, t, e);
01010             if (r == NULL) {
01011                 Cudd_RecursiveDeref(dd, t);
01012                 Cudd_RecursiveDeref(dd, e);
01013                 return(NULL);
01014             }
01015         }
01016         cuddDeref(t);
01017         cuddDeref(e);
01018     }
01019 
01020     cuddCacheInsert(dd,DD_ADD_COMPOSE_RECUR_TAG,f,g,proj,r);
01021 
01022     return(r);
01023 
01024 } /* end of cuddAddComposeRecur */
01025 
01026 
01027 /*---------------------------------------------------------------------------*/
01028 /* Definition of static functions                                            */
01029 /*---------------------------------------------------------------------------*/
01030 
01031 
01052 static DdNode *
01053 cuddAddPermuteRecur(
01054   DdManager * manager /* DD manager */,
01055   DdHashTable * table /* computed table */,
01056   DdNode * node /* ADD to be reordered */,
01057   int * permut /* permutation array */)
01058 {
01059     DdNode      *T,*E;
01060     DdNode      *res,*var;
01061     int         index;
01062     
01063     statLine(manager);
01064     /* Check for terminal case of constant node. */
01065     if (cuddIsConstant(node)) {
01066         return(node);
01067     }
01068 
01069     /* If problem already solved, look up answer and return. */
01070     if (node->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) {
01071 #ifdef DD_DEBUG
01072         addPermuteRecurHits++;
01073 #endif
01074         return(res);
01075     }
01076 
01077     /* Split and recur on children of this node. */
01078     T = cuddAddPermuteRecur(manager,table,cuddT(node),permut);
01079     if (T == NULL) return(NULL);
01080     cuddRef(T);
01081     E = cuddAddPermuteRecur(manager,table,cuddE(node),permut);
01082     if (E == NULL) {
01083         Cudd_RecursiveDeref(manager, T);
01084         return(NULL);
01085     }
01086     cuddRef(E);
01087 
01088     /* Move variable that should be in this position to this position
01089     ** by creating a single var ADD for that variable, and calling
01090     ** cuddAddIteRecur with the T and E we just created.
01091     */
01092     index = permut[node->index];
01093     var = cuddUniqueInter(manager,index,DD_ONE(manager),DD_ZERO(manager));
01094     if (var == NULL) return(NULL);
01095     cuddRef(var);
01096     res = cuddAddIteRecur(manager,var,T,E);
01097     if (res == NULL) {
01098         Cudd_RecursiveDeref(manager,var);
01099         Cudd_RecursiveDeref(manager, T);
01100         Cudd_RecursiveDeref(manager, E);
01101         return(NULL);
01102     }
01103     cuddRef(res);
01104     Cudd_RecursiveDeref(manager,var);
01105     Cudd_RecursiveDeref(manager, T);
01106     Cudd_RecursiveDeref(manager, E);
01107 
01108     /* Do not keep the result if the reference count is only 1, since
01109     ** it will not be visited again.
01110     */
01111     if (node->ref != 1) {
01112         ptrint fanout = (ptrint) node->ref;
01113         cuddSatDec(fanout);
01114         if (!cuddHashTableInsert1(table,node,res,fanout)) {
01115             Cudd_RecursiveDeref(manager, res);
01116             return(NULL);
01117         }
01118     }
01119     cuddDeref(res);
01120     return(res);
01121 
01122 } /* end of cuddAddPermuteRecur */
01123 
01124 
01145 static DdNode *
01146 cuddBddPermuteRecur(
01147   DdManager * manager /* DD manager */,
01148   DdHashTable * table /* computed table */,
01149   DdNode * node /* BDD to be reordered */,
01150   int * permut /* permutation array */)
01151 {
01152     DdNode      *N,*T,*E;
01153     DdNode      *res;
01154     int         index;
01155 
01156     statLine(manager);
01157     N = Cudd_Regular(node);
01158 
01159     /* Check for terminal case of constant node. */
01160     if (cuddIsConstant(N)) {
01161         return(node);
01162     }
01163 
01164     /* If problem already solved, look up answer and return. */
01165     if (N->ref != 1 && (res = cuddHashTableLookup1(table,N)) != NULL) {
01166 #ifdef DD_DEBUG
01167         bddPermuteRecurHits++;
01168 #endif
01169         return(Cudd_NotCond(res,N != node));
01170     }
01171 
01172     /* Split and recur on children of this node. */
01173     T = cuddBddPermuteRecur(manager,table,cuddT(N),permut);
01174     if (T == NULL) return(NULL);
01175     cuddRef(T);
01176     E = cuddBddPermuteRecur(manager,table,cuddE(N),permut);
01177     if (E == NULL) {
01178         Cudd_IterDerefBdd(manager, T);
01179         return(NULL);
01180     }
01181     cuddRef(E);
01182 
01183     /* Move variable that should be in this position to this position
01184     ** by retrieving the single var BDD for that variable, and calling
01185     ** cuddBddIteRecur with the T and E we just created.
01186     */
01187     index = permut[N->index];
01188     res = cuddBddIteRecur(manager,manager->vars[index],T,E);
01189     if (res == NULL) {
01190         Cudd_IterDerefBdd(manager, T);
01191         Cudd_IterDerefBdd(manager, E);
01192         return(NULL);
01193     }
01194     cuddRef(res);
01195     Cudd_IterDerefBdd(manager, T);
01196     Cudd_IterDerefBdd(manager, E);
01197 
01198     /* Do not keep the result if the reference count is only 1, since
01199     ** it will not be visited again.
01200     */
01201     if (N->ref != 1) {
01202         ptrint fanout = (ptrint) N->ref;
01203         cuddSatDec(fanout);
01204         if (!cuddHashTableInsert1(table,N,res,fanout)) {
01205             Cudd_IterDerefBdd(manager, res);
01206             return(NULL);
01207         }
01208     }
01209     cuddDeref(res);
01210     return(Cudd_NotCond(res,N != node));
01211 
01212 } /* end of cuddBddPermuteRecur */
01213 
01214 
01227 static DdNode *
01228 cuddBddVarMapRecur(
01229   DdManager *manager /* DD manager */,
01230   DdNode *f /* BDD to be remapped */)
01231 {
01232     DdNode      *F, *T, *E;
01233     DdNode      *res;
01234     int         index;
01235 
01236     statLine(manager);
01237     F = Cudd_Regular(f);
01238 
01239     /* Check for terminal case of constant node. */
01240     if (cuddIsConstant(F)) {
01241         return(f);
01242     }
01243 
01244     /* If problem already solved, look up answer and return. */
01245     if (F->ref != 1 &&
01246         (res = cuddCacheLookup1(manager,Cudd_bddVarMap,F)) != NULL) {
01247         return(Cudd_NotCond(res,F != f));
01248     }
01249 
01250     /* Split and recur on children of this node. */
01251     T = cuddBddVarMapRecur(manager,cuddT(F));
01252     if (T == NULL) return(NULL);
01253     cuddRef(T);
01254     E = cuddBddVarMapRecur(manager,cuddE(F));
01255     if (E == NULL) {
01256         Cudd_IterDerefBdd(manager, T);
01257         return(NULL);
01258     }
01259     cuddRef(E);
01260 
01261     /* Move variable that should be in this position to this position
01262     ** by retrieving the single var BDD for that variable, and calling
01263     ** cuddBddIteRecur with the T and E we just created.
01264     */
01265     index = manager->map[F->index];
01266     res = cuddBddIteRecur(manager,manager->vars[index],T,E);
01267     if (res == NULL) {
01268         Cudd_IterDerefBdd(manager, T);
01269         Cudd_IterDerefBdd(manager, E);
01270         return(NULL);
01271     }
01272     cuddRef(res);
01273     Cudd_IterDerefBdd(manager, T);
01274     Cudd_IterDerefBdd(manager, E);
01275 
01276     /* Do not keep the result if the reference count is only 1, since
01277     ** it will not be visited again.
01278     */
01279     if (F->ref != 1) {
01280         cuddCacheInsert1(manager,Cudd_bddVarMap,F,res);
01281     }
01282     cuddDeref(res);
01283     return(Cudd_NotCond(res,F != f));
01284 
01285 } /* end of cuddBddVarMapRecur */
01286 
01287 
01299 static DdNode *
01300 cuddAddVectorComposeRecur(
01301   DdManager * dd /* DD manager */,
01302   DdHashTable * table /* computed table */,
01303   DdNode * f /* ADD in which to compose */,
01304   DdNode ** vector /* functions to substitute */,
01305   int  deepest /* depth of deepest substitution */)
01306 {
01307     DdNode      *T,*E;
01308     DdNode      *res;
01309 
01310     statLine(dd);
01311     /* If we are past the deepest substitution, return f. */
01312     if (cuddI(dd,f->index) > deepest) {
01313         return(f);
01314     }
01315 
01316     if ((res = cuddHashTableLookup1(table,f)) != NULL) {
01317 #ifdef DD_DEBUG
01318         addVectorComposeHits++;
01319 #endif
01320         return(res);
01321     }
01322 
01323     /* Split and recur on children of this node. */
01324     T = cuddAddVectorComposeRecur(dd,table,cuddT(f),vector,deepest);
01325     if (T == NULL)  return(NULL);
01326     cuddRef(T);
01327     E = cuddAddVectorComposeRecur(dd,table,cuddE(f),vector,deepest);
01328     if (E == NULL) {
01329         Cudd_RecursiveDeref(dd, T);
01330         return(NULL);
01331     }
01332     cuddRef(E);
01333 
01334     /* Retrieve the 0-1 ADD for the current top variable and call
01335     ** cuddAddIteRecur with the T and E we just created.
01336     */
01337     res = cuddAddIteRecur(dd,vector[f->index],T,E);
01338     if (res == NULL) {
01339         Cudd_RecursiveDeref(dd, T);
01340         Cudd_RecursiveDeref(dd, E);
01341         return(NULL);
01342     }
01343     cuddRef(res);
01344     Cudd_RecursiveDeref(dd, T);
01345     Cudd_RecursiveDeref(dd, E);
01346 
01347     /* Do not keep the result if the reference count is only 1, since
01348     ** it will not be visited again
01349     */
01350     if (f->ref != 1) {
01351         ptrint fanout = (ptrint) f->ref;
01352         cuddSatDec(fanout);
01353         if (!cuddHashTableInsert1(table,f,res,fanout)) {
01354             Cudd_RecursiveDeref(dd, res);
01355             return(NULL);
01356         }
01357     }
01358     cuddDeref(res);
01359     return(res);
01360 
01361 } /* end of cuddAddVectorComposeRecur */
01362 
01363 
01375 static DdNode *
01376 cuddAddGeneralVectorComposeRecur(
01377   DdManager * dd /* DD manager */,
01378   DdHashTable * table /* computed table */,
01379   DdNode * f /* ADD in which to compose */,
01380   DdNode ** vectorOn /* functions to substitute for x_i */,
01381   DdNode ** vectorOff /* functions to substitute for x_i' */,
01382   int  deepest /* depth of deepest substitution */)
01383 {
01384     DdNode      *T,*E,*t,*e;
01385     DdNode      *res;
01386 
01387     /* If we are past the deepest substitution, return f. */
01388     if (cuddI(dd,f->index) > deepest) {
01389         return(f);
01390     }
01391 
01392     if ((res = cuddHashTableLookup1(table,f)) != NULL) {
01393 #ifdef DD_DEBUG
01394         addGeneralVectorComposeHits++;
01395 #endif
01396         return(res);
01397     }
01398 
01399     /* Split and recur on children of this node. */
01400     T = cuddAddGeneralVectorComposeRecur(dd,table,cuddT(f),
01401                                          vectorOn,vectorOff,deepest);
01402     if (T == NULL)  return(NULL);
01403     cuddRef(T);
01404     E = cuddAddGeneralVectorComposeRecur(dd,table,cuddE(f),
01405                                          vectorOn,vectorOff,deepest);
01406     if (E == NULL) {
01407         Cudd_RecursiveDeref(dd, T);
01408         return(NULL);
01409     }
01410     cuddRef(E);
01411 
01412     /* Retrieve the compose ADDs for the current top variable and call
01413     ** cuddAddApplyRecur with the T and E we just created.
01414     */
01415     t = cuddAddApplyRecur(dd,Cudd_addTimes,vectorOn[f->index],T);
01416     if (t == NULL) {
01417       Cudd_RecursiveDeref(dd,T);
01418       Cudd_RecursiveDeref(dd,E);
01419       return(NULL);
01420     }
01421     cuddRef(t);
01422     e = cuddAddApplyRecur(dd,Cudd_addTimes,vectorOff[f->index],E);
01423     if (e == NULL) {
01424       Cudd_RecursiveDeref(dd,T);
01425       Cudd_RecursiveDeref(dd,E);
01426       Cudd_RecursiveDeref(dd,t);
01427       return(NULL);
01428     }
01429     cuddRef(e);
01430     res = cuddAddApplyRecur(dd,Cudd_addPlus,t,e);
01431     if (res == NULL) {
01432       Cudd_RecursiveDeref(dd,T);
01433       Cudd_RecursiveDeref(dd,E);
01434       Cudd_RecursiveDeref(dd,t);
01435       Cudd_RecursiveDeref(dd,e);
01436       return(NULL);
01437     }
01438     cuddRef(res);
01439     Cudd_RecursiveDeref(dd,T);
01440     Cudd_RecursiveDeref(dd,E);
01441     Cudd_RecursiveDeref(dd,t);
01442     Cudd_RecursiveDeref(dd,e);
01443 
01444     /* Do not keep the result if the reference count is only 1, since
01445     ** it will not be visited again
01446     */
01447     if (f->ref != 1) {
01448         ptrint fanout = (ptrint) f->ref;
01449         cuddSatDec(fanout);
01450         if (!cuddHashTableInsert1(table,f,res,fanout)) {
01451             Cudd_RecursiveDeref(dd, res);
01452             return(NULL);
01453         }
01454     }
01455     cuddDeref(res);
01456     return(res);
01457 
01458 } /* end of cuddAddGeneralVectorComposeRecur */
01459 
01460 
01472 static DdNode *
01473 cuddAddNonSimComposeRecur(
01474   DdManager * dd,
01475   DdNode * f,
01476   DdNode ** vector,
01477   DdNode * key,
01478   DdNode * cube,
01479   int  lastsub)
01480 {
01481     DdNode *f1, *f0, *key1, *key0, *cube1, *var;
01482     DdNode *T,*E;
01483     DdNode *r;
01484     unsigned int top, topf, topk, topc;
01485     unsigned int index;
01486     int i;
01487     DdNode **vect1;
01488     DdNode **vect0;
01489 
01490     statLine(dd);
01491     /* If we are past the deepest substitution, return f. */
01492     if (cube == DD_ONE(dd) || cuddIsConstant(f)) {
01493         return(f);
01494     }
01495 
01496     /* If problem already solved, look up answer and return. */
01497     r = cuddCacheLookup(dd,DD_ADD_NON_SIM_COMPOSE_TAG,f,key,cube);
01498     if (r != NULL) {
01499         return(r);
01500     }
01501 
01502     /* Find top variable. we just need to look at f, key, and cube,
01503     ** because all the varibles in the gi are in key.
01504     */
01505     topf = cuddI(dd,f->index);
01506     topk = cuddI(dd,key->index);
01507     top = ddMin(topf,topk);
01508     topc = cuddI(dd,cube->index);
01509     top = ddMin(top,topc);
01510     index = dd->invperm[top];
01511 
01512     /* Compute the cofactors. */
01513     if (topf == top) {
01514         f1 = cuddT(f);
01515         f0 = cuddE(f);
01516     } else {
01517         f1 = f0 = f;
01518     }
01519     if (topc == top) {
01520         cube1 = cuddT(cube);
01521         /* We want to eliminate vector[index] from key. Otherwise
01522         ** cache performance is severely affected. Hence we
01523         ** existentially quantify the variable with index "index" from key.
01524         */
01525         var = Cudd_addIthVar(dd, (int) index);
01526         if (var == NULL) {
01527             return(NULL);
01528         }
01529         cuddRef(var);
01530         key1 = cuddAddExistAbstractRecur(dd, key, var);
01531         if (key1 == NULL) {
01532             Cudd_RecursiveDeref(dd,var);
01533             return(NULL);
01534         }
01535         cuddRef(key1);
01536         Cudd_RecursiveDeref(dd,var);
01537         key0 = key1;
01538     } else {
01539         cube1 = cube;
01540         if (topk == top) {
01541             key1 = cuddT(key);
01542             key0 = cuddE(key);
01543         } else {
01544             key1 = key0 = key;
01545         }
01546         cuddRef(key1);
01547     }
01548 
01549     /* Allocate two new vectors for the cofactors of vector. */
01550     vect1 = ALLOC(DdNode *,lastsub);
01551     if (vect1 == NULL) {
01552         dd->errorCode = CUDD_MEMORY_OUT;
01553         Cudd_RecursiveDeref(dd,key1);
01554         return(NULL);
01555     }
01556     vect0 = ALLOC(DdNode *,lastsub);
01557     if (vect0 == NULL) {
01558         dd->errorCode = CUDD_MEMORY_OUT;
01559         Cudd_RecursiveDeref(dd,key1);
01560         FREE(vect1);
01561         return(NULL);
01562     }
01563 
01564     /* Cofactor the gi. Eliminate vect1[index] and vect0[index], because
01565     ** we do not need them.
01566     */
01567     for (i = 0; i < lastsub; i++) {
01568         DdNode *gi = vector[i];
01569         if (gi == NULL) {
01570             vect1[i] = vect0[i] = NULL;
01571         } else if (gi->index == index) {
01572             vect1[i] = cuddT(gi);
01573             vect0[i] = cuddE(gi);
01574         } else {
01575             vect1[i] = vect0[i] = gi;
01576         }
01577     }
01578     vect1[index] = vect0[index] = NULL;
01579 
01580     /* Recur on children. */
01581     T = cuddAddNonSimComposeRecur(dd,f1,vect1,key1,cube1,lastsub);
01582     FREE(vect1);
01583     if (T == NULL) {
01584         Cudd_RecursiveDeref(dd,key1);
01585         FREE(vect0);
01586         return(NULL);
01587     }
01588     cuddRef(T);
01589     E = cuddAddNonSimComposeRecur(dd,f0,vect0,key0,cube1,lastsub);
01590     FREE(vect0);
01591     if (E == NULL) {
01592         Cudd_RecursiveDeref(dd,key1);
01593         Cudd_RecursiveDeref(dd,T);
01594         return(NULL);
01595     }
01596     cuddRef(E);
01597     Cudd_RecursiveDeref(dd,key1);
01598 
01599     /* Retrieve the 0-1 ADD for the current top variable from vector,
01600     ** and call cuddAddIteRecur with the T and E we just created.
01601     */
01602     r = cuddAddIteRecur(dd,vector[index],T,E);
01603     if (r == NULL) {
01604         Cudd_RecursiveDeref(dd,T);
01605         Cudd_RecursiveDeref(dd,E);
01606         return(NULL);
01607     }
01608     cuddRef(r);
01609     Cudd_RecursiveDeref(dd,T);
01610     Cudd_RecursiveDeref(dd,E);
01611     cuddDeref(r);
01612 
01613     /* Store answer to trim recursion. */
01614     cuddCacheInsert(dd,DD_ADD_NON_SIM_COMPOSE_TAG,f,key,cube,r);
01615 
01616     return(r);
01617 
01618 } /* end of cuddAddNonSimComposeRecur */
01619 
01620 
01632 static DdNode *
01633 cuddBddVectorComposeRecur(
01634   DdManager * dd /* DD manager */,
01635   DdHashTable * table /* computed table */,
01636   DdNode * f /* BDD in which to compose */,
01637   DdNode ** vector /* functions to be composed */,
01638   int deepest /* depth of the deepest substitution */)
01639 {
01640     DdNode      *F,*T,*E;
01641     DdNode      *res;
01642 
01643     statLine(dd);
01644     F = Cudd_Regular(f);
01645 
01646     /* If we are past the deepest substitution, return f. */
01647     if (cuddI(dd,F->index) > deepest) {
01648         return(f);
01649     }
01650 
01651     /* If problem already solved, look up answer and return. */
01652     if ((res = cuddHashTableLookup1(table,F)) != NULL) {
01653 #ifdef DD_DEBUG
01654         bddVectorComposeHits++;
01655 #endif
01656         return(Cudd_NotCond(res,F != f));
01657     }
01658 
01659     /* Split and recur on children of this node. */
01660     T = cuddBddVectorComposeRecur(dd,table,cuddT(F),vector, deepest);
01661     if (T == NULL) return(NULL);
01662     cuddRef(T);
01663     E = cuddBddVectorComposeRecur(dd,table,cuddE(F),vector, deepest);
01664     if (E == NULL) {
01665         Cudd_IterDerefBdd(dd, T);
01666         return(NULL);
01667     }
01668     cuddRef(E);
01669 
01670     /* Call cuddBddIteRecur with the BDD that replaces the current top
01671     ** variable and the T and E we just created.
01672     */
01673     res = cuddBddIteRecur(dd,vector[F->index],T,E);
01674     if (res == NULL) {
01675         Cudd_IterDerefBdd(dd, T);
01676         Cudd_IterDerefBdd(dd, E);
01677         return(NULL);
01678     }
01679     cuddRef(res);
01680     Cudd_IterDerefBdd(dd, T);
01681     Cudd_IterDerefBdd(dd, E);   
01682 
01683     /* Do not keep the result if the reference count is only 1, since
01684     ** it will not be visited again.
01685     */
01686     if (F->ref != 1) {
01687         ptrint fanout = (ptrint) F->ref;
01688         cuddSatDec(fanout);
01689         if (!cuddHashTableInsert1(table,F,res,fanout)) {
01690             Cudd_IterDerefBdd(dd, res);
01691             return(NULL);
01692         }
01693     }
01694     cuddDeref(res);
01695     return(Cudd_NotCond(res,F != f));
01696 
01697 } /* end of cuddBddVectorComposeRecur */
01698 
01699 
01712 DD_INLINE
01713 static int
01714 ddIsIthAddVar(
01715   DdManager * dd,
01716   DdNode * f,
01717   unsigned int  i)
01718 {
01719     return(f->index == i && cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd));
01720 
01721 } /* end of ddIsIthAddVar */
01722 
01723 
01737 DD_INLINE
01738 static int
01739 ddIsIthAddVarPair(
01740   DdManager * dd,
01741   DdNode * f,
01742   DdNode * g,
01743   unsigned int  i)
01744 {
01745     return(f->index == i && g->index == i && 
01746            cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd) &&
01747            cuddT(g) == DD_ZERO(dd) && cuddE(g) == DD_ONE(dd));
01748 
01749 } /* end of ddIsIthAddVarPair */