00001
00062 #include "util.h"
00063 #include "cuddInt.h"
00064
00065
00066
00067
00068
00069
00070
00071
00072
00073
00074
00075
00076
00077
00078
00079
00080
00081
00082
00083
00084 #ifndef lint
00085 static char rcsid[] DD_UNUSED = "$Id: cuddZddPort.c,v 1.13 2004/08/13 18:04:53 fabio Exp $";
00086 #endif
00087
00088
00089
00090
00091
00092
00095
00096
00097
00098
00099 static DdNode * zddPortFromBddStep (DdManager *dd, DdNode *B, int expected);
00100 static DdNode * zddPortToBddStep (DdManager *dd, DdNode *f, int depth);
00101
00105
00106
00107
00108
00109
00126 DdNode *
00127 Cudd_zddPortFromBdd(
00128 DdManager * dd,
00129 DdNode * B)
00130 {
00131 DdNode *res;
00132
00133 do {
00134 dd->reordered = 0;
00135 res = zddPortFromBddStep(dd,B,0);
00136 } while (dd->reordered == 1);
00137
00138 return(res);
00139
00140 }
00141
00142
00155 DdNode *
00156 Cudd_zddPortToBdd(
00157 DdManager * dd,
00158 DdNode * f)
00159 {
00160 DdNode *res;
00161
00162 do {
00163 dd->reordered = 0;
00164 res = zddPortToBddStep(dd,f,0);
00165 } while (dd->reordered == 1);
00166
00167 return(res);
00168
00169 }
00170
00171
00172
00173
00174
00175
00176
00177
00178
00179
00180
00192 static DdNode *
00193 zddPortFromBddStep(
00194 DdManager * dd,
00195 DdNode * B,
00196 int expected)
00197 {
00198 DdNode *res, *prevZdd, *t, *e;
00199 DdNode *Breg, *Bt, *Be;
00200 int id, level;
00201
00202 statLine(dd);
00203
00204 if (B == Cudd_Not(DD_ONE(dd)))
00205 return(DD_ZERO(dd));
00206 if (B == DD_ONE(dd)) {
00207 if (expected >= dd->sizeZ) {
00208 return(DD_ONE(dd));
00209 } else {
00210 return(dd->univ[expected]);
00211 }
00212 }
00213
00214 Breg = Cudd_Regular(B);
00215
00216
00217 res = cuddCacheLookup1Zdd(dd,Cudd_zddPortFromBdd,B);
00218 if (res != NULL) {
00219 level = cuddI(dd,Breg->index);
00220
00221 if (expected < level) {
00222
00223 cuddRef(res);
00224 for (level--; level >= expected; level--) {
00225 prevZdd = res;
00226 id = dd->invperm[level];
00227 res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
00228 if (res == NULL) {
00229 Cudd_RecursiveDerefZdd(dd, prevZdd);
00230 return(NULL);
00231 }
00232 cuddRef(res);
00233 Cudd_RecursiveDerefZdd(dd, prevZdd);
00234 }
00235 cuddDeref(res);
00236 }
00237 return(res);
00238 }
00239
00240 if (Cudd_IsComplement(B)) {
00241 Bt = Cudd_Not(cuddT(Breg));
00242 Be = Cudd_Not(cuddE(Breg));
00243 } else {
00244 Bt = cuddT(Breg);
00245 Be = cuddE(Breg);
00246 }
00247
00248 id = Breg->index;
00249 level = cuddI(dd,id);
00250 t = zddPortFromBddStep(dd, Bt, level+1);
00251 if (t == NULL) return(NULL);
00252 cuddRef(t);
00253 e = zddPortFromBddStep(dd, Be, level+1);
00254 if (e == NULL) {
00255 Cudd_RecursiveDerefZdd(dd, t);
00256 return(NULL);
00257 }
00258 cuddRef(e);
00259 res = cuddZddGetNode(dd, id, t, e);
00260 if (res == NULL) {
00261 Cudd_RecursiveDerefZdd(dd, t);
00262 Cudd_RecursiveDerefZdd(dd, e);
00263 return(NULL);
00264 }
00265 cuddRef(res);
00266 Cudd_RecursiveDerefZdd(dd, t);
00267 Cudd_RecursiveDerefZdd(dd, e);
00268
00269 cuddCacheInsert1(dd,Cudd_zddPortFromBdd,B,res);
00270
00271 for (level--; level >= expected; level--) {
00272 prevZdd = res;
00273 id = dd->invperm[level];
00274 res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
00275 if (res == NULL) {
00276 Cudd_RecursiveDerefZdd(dd, prevZdd);
00277 return(NULL);
00278 }
00279 cuddRef(res);
00280 Cudd_RecursiveDerefZdd(dd, prevZdd);
00281 }
00282
00283 cuddDeref(res);
00284 return(res);
00285
00286 }
00287
00288
00300 static DdNode *
00301 zddPortToBddStep(
00302 DdManager * dd ,
00303 DdNode * f ,
00304 int depth )
00305 {
00306 DdNode *one, *zero, *T, *E, *res, *var;
00307 unsigned int index;
00308 unsigned int level;
00309
00310 statLine(dd);
00311 one = DD_ONE(dd);
00312 zero = DD_ZERO(dd);
00313 if (f == zero) return(Cudd_Not(one));
00314
00315 if (depth == dd->sizeZ) return(one);
00316
00317 index = dd->invpermZ[depth];
00318 level = cuddIZ(dd,f->index);
00319 var = cuddUniqueInter(dd,index,one,Cudd_Not(one));
00320 if (var == NULL) return(NULL);
00321 cuddRef(var);
00322
00323 if (level > (unsigned) depth) {
00324 E = zddPortToBddStep(dd,f,depth+1);
00325 if (E == NULL) {
00326 Cudd_RecursiveDeref(dd,var);
00327 return(NULL);
00328 }
00329 cuddRef(E);
00330 res = cuddBddIteRecur(dd,var,Cudd_Not(one),E);
00331 if (res == NULL) {
00332 Cudd_RecursiveDeref(dd,var);
00333 Cudd_RecursiveDeref(dd,E);
00334 return(NULL);
00335 }
00336 cuddRef(res);
00337 Cudd_RecursiveDeref(dd,var);
00338 Cudd_RecursiveDeref(dd,E);
00339 cuddDeref(res);
00340 return(res);
00341 }
00342
00343 res = cuddCacheLookup1(dd,Cudd_zddPortToBdd,f);
00344 if (res != NULL) {
00345 Cudd_RecursiveDeref(dd,var);
00346 return(res);
00347 }
00348
00349 T = zddPortToBddStep(dd,cuddT(f),depth+1);
00350 if (T == NULL) {
00351 Cudd_RecursiveDeref(dd,var);
00352 return(NULL);
00353 }
00354 cuddRef(T);
00355 E = zddPortToBddStep(dd,cuddE(f),depth+1);
00356 if (E == NULL) {
00357 Cudd_RecursiveDeref(dd,var);
00358 Cudd_RecursiveDeref(dd,T);
00359 return(NULL);
00360 }
00361 cuddRef(E);
00362
00363 res = cuddBddIteRecur(dd,var,T,E);
00364 if (res == NULL) {
00365 Cudd_RecursiveDeref(dd,var);
00366 Cudd_RecursiveDeref(dd,T);
00367 Cudd_RecursiveDeref(dd,E);
00368 return(NULL);
00369 }
00370 cuddRef(res);
00371 Cudd_RecursiveDeref(dd,var);
00372 Cudd_RecursiveDeref(dd,T);
00373 Cudd_RecursiveDeref(dd,E);
00374 cuddDeref(res);
00375
00376 cuddCacheInsert1(dd,Cudd_zddPortToBdd,f,res);
00377
00378 return(res);
00379
00380 }
00381
