00001
00035 #include "util_hack.h"
00036 #include "cuddInt.h"
00037
00038
00039
00040
00041
00042
00043
00044
00045
00046
00047
00048
00049
00050
00051
00052
00053
00054
00055
00056
00057 #ifndef lint
00058 static char rcsid[] DD_UNUSED = "$Id: cuddZddPort.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $";
00059 #endif
00060
00061
00062
00063
00064
00065
00068
00069
00070
00071
00072 static DdNode * zddPortFromBddStep ARGS((DdManager *dd, DdNode *B, int expected));
00073 static DdNode * zddPortToBddStep ARGS((DdManager *dd, DdNode *f, int depth));
00074
00078
00079
00080
00081
00082
00099 DdNode *
00100 Cudd_zddPortFromBdd(
00101 DdManager * dd,
00102 DdNode * B)
00103 {
00104 DdNode *res;
00105
00106 do {
00107 dd->reordered = 0;
00108 res = zddPortFromBddStep(dd,B,0);
00109 } while (dd->reordered == 1);
00110
00111 return(res);
00112
00113 }
00114
00115
00128 DdNode *
00129 Cudd_zddPortToBdd(
00130 DdManager * dd,
00131 DdNode * f)
00132 {
00133 DdNode *res;
00134
00135 do {
00136 dd->reordered = 0;
00137 res = zddPortToBddStep(dd,f,0);
00138 } while (dd->reordered == 1);
00139
00140 return(res);
00141
00142 }
00143
00144
00145
00146
00147
00148
00149
00150
00151
00152
00153
00165 static DdNode *
00166 zddPortFromBddStep(
00167 DdManager * dd,
00168 DdNode * B,
00169 int expected)
00170 {
00171 DdNode *res, *prevZdd, *t, *e;
00172 DdNode *Breg, *Bt, *Be;
00173 int id, level;
00174
00175 statLine(dd);
00176
00177 if (B == Cudd_Not(DD_ONE(dd)))
00178 return(DD_ZERO(dd));
00179 if (B == DD_ONE(dd)) {
00180 if (expected >= dd->sizeZ) {
00181 return(DD_ONE(dd));
00182 } else {
00183 return(dd->univ[expected]);
00184 }
00185 }
00186
00187 Breg = Cudd_Regular(B);
00188
00189
00190 res = cuddCacheLookup1Zdd(dd,Cudd_zddPortFromBdd,B);
00191 if (res != NULL) {
00192 level = cuddI(dd,Breg->index);
00193
00194 if (expected < level) {
00195
00196 cuddRef(res);
00197 for (level--; level >= expected; level--) {
00198 prevZdd = res;
00199 id = dd->invperm[level];
00200 res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
00201 if (res == NULL) {
00202 Cudd_RecursiveDerefZdd(dd, prevZdd);
00203 return(NULL);
00204 }
00205 cuddRef(res);
00206 Cudd_RecursiveDerefZdd(dd, prevZdd);
00207 }
00208 cuddDeref(res);
00209 }
00210 return(res);
00211 }
00212
00213 if (Cudd_IsComplement(B)) {
00214 Bt = Cudd_Not(cuddT(Breg));
00215 Be = Cudd_Not(cuddE(Breg));
00216 } else {
00217 Bt = cuddT(Breg);
00218 Be = cuddE(Breg);
00219 }
00220
00221 id = Breg->index;
00222 level = cuddI(dd,id);
00223 t = zddPortFromBddStep(dd, Bt, level+1);
00224 if (t == NULL) return(NULL);
00225 cuddRef(t);
00226 e = zddPortFromBddStep(dd, Be, level+1);
00227 if (e == NULL) {
00228 Cudd_RecursiveDerefZdd(dd, t);
00229 return(NULL);
00230 }
00231 cuddRef(e);
00232 res = cuddZddGetNode(dd, id, t, e);
00233 if (res == NULL) {
00234 Cudd_RecursiveDerefZdd(dd, t);
00235 Cudd_RecursiveDerefZdd(dd, e);
00236 return(NULL);
00237 }
00238 cuddRef(res);
00239 Cudd_RecursiveDerefZdd(dd, t);
00240 Cudd_RecursiveDerefZdd(dd, e);
00241
00242 cuddCacheInsert1(dd,Cudd_zddPortFromBdd,B,res);
00243
00244 for (level--; level >= expected; level--) {
00245 prevZdd = res;
00246 id = dd->invperm[level];
00247 res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
00248 if (res == NULL) {
00249 Cudd_RecursiveDerefZdd(dd, prevZdd);
00250 return(NULL);
00251 }
00252 cuddRef(res);
00253 Cudd_RecursiveDerefZdd(dd, prevZdd);
00254 }
00255
00256 cuddDeref(res);
00257 return(res);
00258
00259 }
00260
00261
00273 static DdNode *
00274 zddPortToBddStep(
00275 DdManager * dd ,
00276 DdNode * f ,
00277 int depth )
00278 {
00279 DdNode *one, *zero, *T, *E, *res, *var;
00280 unsigned int index;
00281 unsigned int level;
00282
00283 statLine(dd);
00284 one = DD_ONE(dd);
00285 zero = DD_ZERO(dd);
00286 if (f == zero) return(Cudd_Not(one));
00287
00288 if (depth == dd->sizeZ) return(one);
00289
00290 index = dd->invpermZ[depth];
00291 level = cuddIZ(dd,f->index);
00292 var = cuddUniqueInter(dd,index,one,Cudd_Not(one));
00293 if (var == NULL) return(NULL);
00294 cuddRef(var);
00295
00296 if (level > (unsigned) depth) {
00297 E = zddPortToBddStep(dd,f,depth+1);
00298 if (E == NULL) {
00299 Cudd_RecursiveDeref(dd,var);
00300 return(NULL);
00301 }
00302 cuddRef(E);
00303 res = cuddBddIteRecur(dd,var,Cudd_Not(one),E);
00304 if (res == NULL) {
00305 Cudd_RecursiveDeref(dd,var);
00306 Cudd_RecursiveDeref(dd,E);
00307 return(NULL);
00308 }
00309 cuddRef(res);
00310 Cudd_RecursiveDeref(dd,var);
00311 Cudd_RecursiveDeref(dd,E);
00312 cuddDeref(res);
00313 return(res);
00314 }
00315
00316 res = cuddCacheLookup1(dd,Cudd_zddPortToBdd,f);
00317 if (res != NULL) {
00318 Cudd_RecursiveDeref(dd,var);
00319 return(res);
00320 }
00321
00322 T = zddPortToBddStep(dd,cuddT(f),depth+1);
00323 if (T == NULL) {
00324 Cudd_RecursiveDeref(dd,var);
00325 return(NULL);
00326 }
00327 cuddRef(T);
00328 E = zddPortToBddStep(dd,cuddE(f),depth+1);
00329 if (E == NULL) {
00330 Cudd_RecursiveDeref(dd,var);
00331 Cudd_RecursiveDeref(dd,T);
00332 return(NULL);
00333 }
00334 cuddRef(E);
00335
00336 res = cuddBddIteRecur(dd,var,T,E);
00337 if (res == NULL) {
00338 Cudd_RecursiveDeref(dd,var);
00339 Cudd_RecursiveDeref(dd,T);
00340 Cudd_RecursiveDeref(dd,E);
00341 return(NULL);
00342 }
00343 cuddRef(res);
00344 Cudd_RecursiveDeref(dd,var);
00345 Cudd_RecursiveDeref(dd,T);
00346 Cudd_RecursiveDeref(dd,E);
00347 cuddDeref(res);
00348
00349 cuddCacheInsert1(dd,Cudd_zddPortToBdd,f,res);
00350
00351 return(res);
00352
00353 }
00354
