[13] | 1 | /**CFile*********************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [cuddZddPort.c] |
---|
| 4 | |
---|
| 5 | PackageName [cudd] |
---|
| 6 | |
---|
| 7 | Synopsis [Functions that translate BDDs to ZDDs.] |
---|
| 8 | |
---|
| 9 | Description [External procedures included in this module: |
---|
| 10 | <ul> |
---|
| 11 | <li> Cudd_zddPortFromBdd() |
---|
| 12 | <li> Cudd_zddPortToBdd() |
---|
| 13 | </ul> |
---|
| 14 | Internal procedures included in this module: |
---|
| 15 | <ul> |
---|
| 16 | </ul> |
---|
| 17 | Static procedures included in this module: |
---|
| 18 | <ul> |
---|
| 19 | <li> zddPortFromBddStep() |
---|
| 20 | <li> zddPortToBddStep() |
---|
| 21 | </ul> |
---|
| 22 | ] |
---|
| 23 | |
---|
| 24 | SeeAlso [] |
---|
| 25 | |
---|
| 26 | Author [Hyong-kyoon Shin, In-Ho Moon] |
---|
| 27 | |
---|
| 28 | Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado |
---|
| 29 | |
---|
| 30 | All rights reserved. |
---|
| 31 | |
---|
| 32 | Redistribution and use in source and binary forms, with or without |
---|
| 33 | modification, are permitted provided that the following conditions |
---|
| 34 | are met: |
---|
| 35 | |
---|
| 36 | Redistributions of source code must retain the above copyright |
---|
| 37 | notice, this list of conditions and the following disclaimer. |
---|
| 38 | |
---|
| 39 | Redistributions in binary form must reproduce the above copyright |
---|
| 40 | notice, this list of conditions and the following disclaimer in the |
---|
| 41 | documentation and/or other materials provided with the distribution. |
---|
| 42 | |
---|
| 43 | Neither the name of the University of Colorado nor the names of its |
---|
| 44 | contributors may be used to endorse or promote products derived from |
---|
| 45 | this software without specific prior written permission. |
---|
| 46 | |
---|
| 47 | THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
---|
| 48 | "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
---|
| 49 | LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
---|
| 50 | FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
---|
| 51 | COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
---|
| 52 | INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
---|
| 53 | BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
---|
| 54 | LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
---|
| 55 | CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
---|
| 56 | LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
---|
| 57 | ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
---|
| 58 | POSSIBILITY OF SUCH DAMAGE.] |
---|
| 59 | |
---|
| 60 | ******************************************************************************/ |
---|
| 61 | |
---|
| 62 | #include "util.h" |
---|
| 63 | #include "cuddInt.h" |
---|
| 64 | |
---|
| 65 | /*---------------------------------------------------------------------------*/ |
---|
| 66 | /* Constant declarations */ |
---|
| 67 | /*---------------------------------------------------------------------------*/ |
---|
| 68 | |
---|
| 69 | |
---|
| 70 | /*---------------------------------------------------------------------------*/ |
---|
| 71 | /* Stucture declarations */ |
---|
| 72 | /*---------------------------------------------------------------------------*/ |
---|
| 73 | |
---|
| 74 | |
---|
| 75 | /*---------------------------------------------------------------------------*/ |
---|
| 76 | /* Type declarations */ |
---|
| 77 | /*---------------------------------------------------------------------------*/ |
---|
| 78 | |
---|
| 79 | |
---|
| 80 | /*---------------------------------------------------------------------------*/ |
---|
| 81 | /* Variable declarations */ |
---|
| 82 | /*---------------------------------------------------------------------------*/ |
---|
| 83 | |
---|
| 84 | #ifndef lint |
---|
| 85 | static char rcsid[] DD_UNUSED = "$Id: cuddZddPort.c,v 1.13 2004/08/13 18:04:53 fabio Exp $"; |
---|
| 86 | #endif |
---|
| 87 | |
---|
| 88 | /*---------------------------------------------------------------------------*/ |
---|
| 89 | /* Macro declarations */ |
---|
| 90 | /*---------------------------------------------------------------------------*/ |
---|
| 91 | |
---|
| 92 | |
---|
| 93 | /**AutomaticStart*************************************************************/ |
---|
| 94 | |
---|
| 95 | /*---------------------------------------------------------------------------*/ |
---|
| 96 | /* Static function prototypes */ |
---|
| 97 | /*---------------------------------------------------------------------------*/ |
---|
| 98 | |
---|
| 99 | static DdNode * zddPortFromBddStep (DdManager *dd, DdNode *B, int expected); |
---|
| 100 | static DdNode * zddPortToBddStep (DdManager *dd, DdNode *f, int depth); |
---|
| 101 | |
---|
| 102 | /**AutomaticEnd***************************************************************/ |
---|
| 103 | |
---|
| 104 | |
---|
| 105 | /*---------------------------------------------------------------------------*/ |
---|
| 106 | /* Definition of exported functions */ |
---|
| 107 | /*---------------------------------------------------------------------------*/ |
---|
| 108 | |
---|
| 109 | |
---|
| 110 | /**Function******************************************************************** |
---|
| 111 | |
---|
| 112 | Synopsis [Converts a BDD into a ZDD.] |
---|
| 113 | |
---|
| 114 | Description [Converts a BDD into a ZDD. This function assumes that |
---|
| 115 | there is a one-to-one correspondence between the BDD variables and the |
---|
| 116 | ZDD variables, and that the variable order is the same for both types |
---|
| 117 | of variables. These conditions are established if the ZDD variables |
---|
| 118 | are created by one call to Cudd_zddVarsFromBddVars with multiplicity = |
---|
| 119 | 1. Returns a pointer to the resulting ZDD if successful; NULL otherwise.] |
---|
| 120 | |
---|
| 121 | SideEffects [None] |
---|
| 122 | |
---|
| 123 | SeeAlso [Cudd_zddVarsFromBddVars] |
---|
| 124 | |
---|
| 125 | ******************************************************************************/ |
---|
| 126 | DdNode * |
---|
| 127 | Cudd_zddPortFromBdd( |
---|
| 128 | DdManager * dd, |
---|
| 129 | DdNode * B) |
---|
| 130 | { |
---|
| 131 | DdNode *res; |
---|
| 132 | |
---|
| 133 | do { |
---|
| 134 | dd->reordered = 0; |
---|
| 135 | res = zddPortFromBddStep(dd,B,0); |
---|
| 136 | } while (dd->reordered == 1); |
---|
| 137 | |
---|
| 138 | return(res); |
---|
| 139 | |
---|
| 140 | } /* end of Cudd_zddPortFromBdd */ |
---|
| 141 | |
---|
| 142 | |
---|
| 143 | /**Function******************************************************************** |
---|
| 144 | |
---|
| 145 | Synopsis [Converts a ZDD into a BDD.] |
---|
| 146 | |
---|
| 147 | Description [Converts a ZDD into a BDD. Returns a pointer to the resulting |
---|
| 148 | ZDD if successful; NULL otherwise.] |
---|
| 149 | |
---|
| 150 | SideEffects [None] |
---|
| 151 | |
---|
| 152 | SeeAlso [Cudd_zddPortFromBdd] |
---|
| 153 | |
---|
| 154 | ******************************************************************************/ |
---|
| 155 | DdNode * |
---|
| 156 | Cudd_zddPortToBdd( |
---|
| 157 | DdManager * dd, |
---|
| 158 | DdNode * f) |
---|
| 159 | { |
---|
| 160 | DdNode *res; |
---|
| 161 | |
---|
| 162 | do { |
---|
| 163 | dd->reordered = 0; |
---|
| 164 | res = zddPortToBddStep(dd,f,0); |
---|
| 165 | } while (dd->reordered == 1); |
---|
| 166 | |
---|
| 167 | return(res); |
---|
| 168 | |
---|
| 169 | } /* end of Cudd_zddPortToBdd */ |
---|
| 170 | |
---|
| 171 | |
---|
| 172 | /*---------------------------------------------------------------------------*/ |
---|
| 173 | /* Definition of internal functions */ |
---|
| 174 | /*---------------------------------------------------------------------------*/ |
---|
| 175 | |
---|
| 176 | /*---------------------------------------------------------------------------*/ |
---|
| 177 | /* Definition of static functions */ |
---|
| 178 | /*---------------------------------------------------------------------------*/ |
---|
| 179 | |
---|
| 180 | |
---|
| 181 | /**Function******************************************************************** |
---|
| 182 | |
---|
| 183 | Synopsis [Performs the recursive step of Cudd_zddPortFromBdd.] |
---|
| 184 | |
---|
| 185 | Description [] |
---|
| 186 | |
---|
| 187 | SideEffects [None] |
---|
| 188 | |
---|
| 189 | SeeAlso [] |
---|
| 190 | |
---|
| 191 | ******************************************************************************/ |
---|
| 192 | static DdNode * |
---|
| 193 | zddPortFromBddStep( |
---|
| 194 | DdManager * dd, |
---|
| 195 | DdNode * B, |
---|
| 196 | int expected) |
---|
| 197 | { |
---|
| 198 | DdNode *res, *prevZdd, *t, *e; |
---|
| 199 | DdNode *Breg, *Bt, *Be; |
---|
| 200 | int id, level; |
---|
| 201 | |
---|
| 202 | statLine(dd); |
---|
| 203 | /* Terminal cases. */ |
---|
| 204 | if (B == Cudd_Not(DD_ONE(dd))) |
---|
| 205 | return(DD_ZERO(dd)); |
---|
| 206 | if (B == DD_ONE(dd)) { |
---|
| 207 | if (expected >= dd->sizeZ) { |
---|
| 208 | return(DD_ONE(dd)); |
---|
| 209 | } else { |
---|
| 210 | return(dd->univ[expected]); |
---|
| 211 | } |
---|
| 212 | } |
---|
| 213 | |
---|
| 214 | Breg = Cudd_Regular(B); |
---|
| 215 | |
---|
| 216 | /* Computed table look-up. */ |
---|
| 217 | res = cuddCacheLookup1Zdd(dd,Cudd_zddPortFromBdd,B); |
---|
| 218 | if (res != NULL) { |
---|
| 219 | level = cuddI(dd,Breg->index); |
---|
| 220 | /* Adding DC vars. */ |
---|
| 221 | if (expected < level) { |
---|
| 222 | /* Add suppressed variables. */ |
---|
| 223 | cuddRef(res); |
---|
| 224 | for (level--; level >= expected; level--) { |
---|
| 225 | prevZdd = res; |
---|
| 226 | id = dd->invperm[level]; |
---|
| 227 | res = cuddZddGetNode(dd, id, prevZdd, prevZdd); |
---|
| 228 | if (res == NULL) { |
---|
| 229 | Cudd_RecursiveDerefZdd(dd, prevZdd); |
---|
| 230 | return(NULL); |
---|
| 231 | } |
---|
| 232 | cuddRef(res); |
---|
| 233 | Cudd_RecursiveDerefZdd(dd, prevZdd); |
---|
| 234 | } |
---|
| 235 | cuddDeref(res); |
---|
| 236 | } |
---|
| 237 | return(res); |
---|
| 238 | } /* end of cache look-up */ |
---|
| 239 | |
---|
| 240 | if (Cudd_IsComplement(B)) { |
---|
| 241 | Bt = Cudd_Not(cuddT(Breg)); |
---|
| 242 | Be = Cudd_Not(cuddE(Breg)); |
---|
| 243 | } else { |
---|
| 244 | Bt = cuddT(Breg); |
---|
| 245 | Be = cuddE(Breg); |
---|
| 246 | } |
---|
| 247 | |
---|
| 248 | id = Breg->index; |
---|
| 249 | level = cuddI(dd,id); |
---|
| 250 | t = zddPortFromBddStep(dd, Bt, level+1); |
---|
| 251 | if (t == NULL) return(NULL); |
---|
| 252 | cuddRef(t); |
---|
| 253 | e = zddPortFromBddStep(dd, Be, level+1); |
---|
| 254 | if (e == NULL) { |
---|
| 255 | Cudd_RecursiveDerefZdd(dd, t); |
---|
| 256 | return(NULL); |
---|
| 257 | } |
---|
| 258 | cuddRef(e); |
---|
| 259 | res = cuddZddGetNode(dd, id, t, e); |
---|
| 260 | if (res == NULL) { |
---|
| 261 | Cudd_RecursiveDerefZdd(dd, t); |
---|
| 262 | Cudd_RecursiveDerefZdd(dd, e); |
---|
| 263 | return(NULL); |
---|
| 264 | } |
---|
| 265 | cuddRef(res); |
---|
| 266 | Cudd_RecursiveDerefZdd(dd, t); |
---|
| 267 | Cudd_RecursiveDerefZdd(dd, e); |
---|
| 268 | |
---|
| 269 | cuddCacheInsert1(dd,Cudd_zddPortFromBdd,B,res); |
---|
| 270 | |
---|
| 271 | for (level--; level >= expected; level--) { |
---|
| 272 | prevZdd = res; |
---|
| 273 | id = dd->invperm[level]; |
---|
| 274 | res = cuddZddGetNode(dd, id, prevZdd, prevZdd); |
---|
| 275 | if (res == NULL) { |
---|
| 276 | Cudd_RecursiveDerefZdd(dd, prevZdd); |
---|
| 277 | return(NULL); |
---|
| 278 | } |
---|
| 279 | cuddRef(res); |
---|
| 280 | Cudd_RecursiveDerefZdd(dd, prevZdd); |
---|
| 281 | } |
---|
| 282 | |
---|
| 283 | cuddDeref(res); |
---|
| 284 | return(res); |
---|
| 285 | |
---|
| 286 | } /* end of zddPortFromBddStep */ |
---|
| 287 | |
---|
| 288 | |
---|
| 289 | /**Function******************************************************************** |
---|
| 290 | |
---|
| 291 | Synopsis [Performs the recursive step of Cudd_zddPortToBdd.] |
---|
| 292 | |
---|
| 293 | Description [] |
---|
| 294 | |
---|
| 295 | SideEffects [None] |
---|
| 296 | |
---|
| 297 | SeeAlso [] |
---|
| 298 | |
---|
| 299 | ******************************************************************************/ |
---|
| 300 | static DdNode * |
---|
| 301 | zddPortToBddStep( |
---|
| 302 | DdManager * dd /* manager */, |
---|
| 303 | DdNode * f /* ZDD to be converted */, |
---|
| 304 | int depth /* recursion depth */) |
---|
| 305 | { |
---|
| 306 | DdNode *one, *zero, *T, *E, *res, *var; |
---|
| 307 | unsigned int index; |
---|
| 308 | unsigned int level; |
---|
| 309 | |
---|
| 310 | statLine(dd); |
---|
| 311 | one = DD_ONE(dd); |
---|
| 312 | zero = DD_ZERO(dd); |
---|
| 313 | if (f == zero) return(Cudd_Not(one)); |
---|
| 314 | |
---|
| 315 | if (depth == dd->sizeZ) return(one); |
---|
| 316 | |
---|
| 317 | index = dd->invpermZ[depth]; |
---|
| 318 | level = cuddIZ(dd,f->index); |
---|
| 319 | var = cuddUniqueInter(dd,index,one,Cudd_Not(one)); |
---|
| 320 | if (var == NULL) return(NULL); |
---|
| 321 | cuddRef(var); |
---|
| 322 | |
---|
| 323 | if (level > (unsigned) depth) { |
---|
| 324 | E = zddPortToBddStep(dd,f,depth+1); |
---|
| 325 | if (E == NULL) { |
---|
| 326 | Cudd_RecursiveDeref(dd,var); |
---|
| 327 | return(NULL); |
---|
| 328 | } |
---|
| 329 | cuddRef(E); |
---|
| 330 | res = cuddBddIteRecur(dd,var,Cudd_Not(one),E); |
---|
| 331 | if (res == NULL) { |
---|
| 332 | Cudd_RecursiveDeref(dd,var); |
---|
| 333 | Cudd_RecursiveDeref(dd,E); |
---|
| 334 | return(NULL); |
---|
| 335 | } |
---|
| 336 | cuddRef(res); |
---|
| 337 | Cudd_RecursiveDeref(dd,var); |
---|
| 338 | Cudd_RecursiveDeref(dd,E); |
---|
| 339 | cuddDeref(res); |
---|
| 340 | return(res); |
---|
| 341 | } |
---|
| 342 | |
---|
| 343 | res = cuddCacheLookup1(dd,Cudd_zddPortToBdd,f); |
---|
| 344 | if (res != NULL) { |
---|
| 345 | Cudd_RecursiveDeref(dd,var); |
---|
| 346 | return(res); |
---|
| 347 | } |
---|
| 348 | |
---|
| 349 | T = zddPortToBddStep(dd,cuddT(f),depth+1); |
---|
| 350 | if (T == NULL) { |
---|
| 351 | Cudd_RecursiveDeref(dd,var); |
---|
| 352 | return(NULL); |
---|
| 353 | } |
---|
| 354 | cuddRef(T); |
---|
| 355 | E = zddPortToBddStep(dd,cuddE(f),depth+1); |
---|
| 356 | if (E == NULL) { |
---|
| 357 | Cudd_RecursiveDeref(dd,var); |
---|
| 358 | Cudd_RecursiveDeref(dd,T); |
---|
| 359 | return(NULL); |
---|
| 360 | } |
---|
| 361 | cuddRef(E); |
---|
| 362 | |
---|
| 363 | res = cuddBddIteRecur(dd,var,T,E); |
---|
| 364 | if (res == NULL) { |
---|
| 365 | Cudd_RecursiveDeref(dd,var); |
---|
| 366 | Cudd_RecursiveDeref(dd,T); |
---|
| 367 | Cudd_RecursiveDeref(dd,E); |
---|
| 368 | return(NULL); |
---|
| 369 | } |
---|
| 370 | cuddRef(res); |
---|
| 371 | Cudd_RecursiveDeref(dd,var); |
---|
| 372 | Cudd_RecursiveDeref(dd,T); |
---|
| 373 | Cudd_RecursiveDeref(dd,E); |
---|
| 374 | cuddDeref(res); |
---|
| 375 | |
---|
| 376 | cuddCacheInsert1(dd,Cudd_zddPortToBdd,f,res); |
---|
| 377 | |
---|
| 378 | return(res); |
---|
| 379 | |
---|
| 380 | } /* end of zddPortToBddStep */ |
---|
| 381 | |
---|